Library iris.proofmode.intro_patterns

From iris.prelude Require Export strings.

Inductive intro_pat :=
  | IName : string → intro_pat
  | IAnom : intro_pat
  | IAnomPure : intro_pat
  | IDrop : intro_pat
  | IFrame : intro_pat
  | IRelevant : intro_pat → intro_pat
  | IList : list (list intro_pat) → intro_pat
  | ISimpl : intro_pat
  | IAlways : intro_pat
  | IAffine : intro_pat
  | INext : intro_pat
  | IForall : intro_pat
  | IAll : intro_pat
  | IClear : list (bool × string) → intro_pat.
Module intro_pat.
Inductive token :=
  | TName : string → token
  | TAnom : token
  | TAnomPure : token
  | TDrop : token
  | TFrame : token
  | TRelevant : token
  | TAffine : token
  | TBar : token
  | TBracketL : token
  | TBracketR : token
  | TAmp : token
  | TParenL : token
  | TParenR : token
  | TSimpl : token
  | TAlways : token
  | TNext : token
  | TClearL : token
  | TClearR : token
  | TForall : token
  | TAll : token.

Fixpoint cons_name (kn : string) (k : list token) : list token :=
  match kn with "" ⇒ k | _ ⇒ TName (string_rev kn) :: k end.
Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
  match s with
  | "" ⇒ rev (cons_name kn k)
  | String " " s ⇒ tokenize_go s (cons_name kn k) ""
  | String "?" s ⇒ tokenize_go s (TAnom :: cons_name kn k) ""
  | String "%" s ⇒ tokenize_go s (TAnomPure :: cons_name kn k) ""
  | String "_" s ⇒ tokenize_go s (TDrop :: cons_name kn k) ""
  | String "$" s ⇒ tokenize_go s (TFrame :: cons_name kn k) ""
  | String "#" s ⇒ tokenize_go s (TRelevant :: cons_name kn k) ""
  | String "[" s ⇒ tokenize_go s (TBracketL :: cons_name kn k) ""
  | String "]" s ⇒ tokenize_go s (TBracketR :: cons_name kn k) ""
  | String "|" s ⇒ tokenize_go s (TBar :: cons_name kn k) ""
  | String "(" s ⇒ tokenize_go s (TParenL :: cons_name kn k) ""
  | String ")" s ⇒ tokenize_go s (TParenR :: cons_name kn k) ""
  | String "&" s ⇒ tokenize_go s (TAmp :: cons_name kn k) ""
  | String "!" s ⇒ tokenize_go s (TAlways :: cons_name kn k) ""
  | String "@" s ⇒ tokenize_go s (TAffine :: cons_name kn k) ""
  | String ">" s ⇒ tokenize_go s (TNext :: cons_name kn k) ""
  | String "{" s ⇒ tokenize_go s (TClearL :: cons_name kn k) ""
  | String "}" s ⇒ tokenize_go s (TClearR :: cons_name kn k) ""
  | String "/" (String "=" s) ⇒ tokenize_go s (TSimpl :: cons_name kn k) ""
  | String "*" (String "*" s) ⇒ tokenize_go s (TAll :: cons_name kn k) ""
  | String "*" s ⇒ tokenize_go s (TForall :: cons_name kn k) ""
  | String a s ⇒ tokenize_go s k (String a kn)
  end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".

Inductive stack_item :=
  | SPat : intro_pat → stack_item
  | SRelevant : stack_item
  | SList : stack_item
  | SConjList : stack_item
  | SBar : stack_item
  | SAmp : stack_item.
Notation stack := (list stack_item).

Fixpoint close_list (k : stack)
    (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
  match k with
  | SList :: k ⇒ Some (SPat (IList (ps :: pss)) :: k)
  | SPat pat :: k ⇒ close_list k (pat :: ps) pss
  | SRelevant :: k ⇒
     '(p,ps) ← maybe2 (::) ps; close_list k (IRelevant p :: ps) pss
  | SBar :: k ⇒ close_list k [] (ps :: pss)
  | _ ⇒ None
  end.

Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
  match ps with
  | [] ⇒ IList [[]]
| [p] ⇒ IList [[ p ]]
| [p1;p2] ⇒ IList [[ p1 ; p2 ]]
| p :: ps ⇒ IList [[ p ; big_conj ps ]]
end.

Fixpoint close_conj_list (k : stack)
    (cur : option intro_pat) (ps : list intro_pat) : option stack :=
  match k with
  | SConjList :: k ⇒
     ps ← match cur with
          | None ⇒ guard (ps = []); Some [] | Some p ⇒ Some (p :: ps)
          end;
     Some (SPat (big_conj ps) :: k)
  | SPat pat :: k ⇒ guard (cur = None); close_conj_list k (Some pat) ps
  | SRelevant :: k ⇒ p ← cur; close_conj_list k (Some (IRelevant p)) ps
  | SAmp :: k ⇒ p ← cur; close_conj_list k None (p :: ps)
  | _ ⇒ None
  end.

Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
  match ts with
  | [] ⇒ Some k
  | TName s :: ts ⇒ parse_go ts (SPat (IName s) :: k)
  | TAnom :: ts ⇒ parse_go ts (SPat IAnom :: k)
  | TAnomPure :: ts ⇒ parse_go ts (SPat IAnomPure :: k)
  | TDrop :: ts ⇒ parse_go ts (SPat IDrop :: k)
  | TFrame :: ts ⇒ parse_go ts (SPat IFrame :: k)
  | TRelevant :: ts ⇒ parse_go ts (SRelevant :: k)
  | TBracketL :: ts ⇒ parse_go ts (SList :: k)
  | TBar :: ts ⇒ parse_go ts (SBar :: k)
  | TBracketR :: ts ⇒ close_list k [] [] ≫= parse_go ts
  | TParenL :: ts ⇒ parse_go ts (SConjList :: k)
  | TAmp :: ts ⇒ parse_go ts (SAmp :: k)
  | TParenR :: ts ⇒ close_conj_list k None [] ≫= parse_go ts
  | TSimpl :: ts ⇒ parse_go ts (SPat ISimpl :: k)
  | TAlways :: ts ⇒ parse_go ts (SPat IAlways :: k)
  | TAffine :: ts ⇒ parse_go ts (SPat IAffine :: k)
  | TNext :: ts ⇒ parse_go ts (SPat INext :: k)
  | TAll :: ts ⇒ parse_go ts (SPat IAll :: k)
  | TForall :: ts ⇒ parse_go ts (SPat IForall :: k)
  | TClearL :: ts ⇒ parse_clear ts [] k
  | _ ⇒ None
  end
with parse_clear (ts : list token)
    (ss : list (bool × string)) (k : stack) : option stack :=
  match ts with
  | TFrame :: TName s :: ts ⇒ parse_clear ts ((true,s) :: ss) k
  | TName s :: ts ⇒ parse_clear ts ((false,s) :: ss) k
  | TClearR :: ts ⇒ parse_go ts (SPat (IClear (reverse ss)) :: k)
  | _ ⇒ None
  end.

Definition parse (s : string) : option (list intro_pat) :=
  match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
  | Some [SPat (IList [ps])] ⇒ Some ps
  | _ ⇒ None
  end.

Ltac parse s :=
  lazymatch type of s with
  | list intro_pat ⇒ s
  | list string ⇒
     lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
     | Some ?pats ⇒ pats | _ ⇒ fail "invalid list intro_pat" s
     end
  | string ⇒
     lazymatch eval vm_compute in (parse s) with
     | Some ?pats ⇒ pats | _ ⇒ fail "invalid list intro_pat" s
     end
  end.
Ltac parse_one s :=
  lazymatch type of s with
  | intro_pat ⇒ s
  | string ⇒
     lazymatch eval vm_compute in (parse s) with
     | Some [?pat] ⇒ pat | _ ⇒ fail "invalid intro_pat" s
     end
  end.
End intro_pat.