Unify tokenizers for intro, spec, and sel patterns.

_CoqProject

@@ -84,6 +84,7 @@ theories/tests/list_reverse.v
 theories/tests/tree_sum.v
 theories/tests/ipm_paper.v
 theories/proofmode/strings.v
+theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
 theories/proofmode/environments.v
 theories/proofmode/intro_patterns.v

theories/proofmode/intro_patterns.v

 From stdpp Require Export strings.
+From iris.proofmode Require Import tokens.
 Set Default Proof Using "Type".
 
 Inductive intro_pat :=
@@ -20,59 +21,6 @@ Inductive intro_pat :=
   | IClearFrame : string → intro_pat.
 
 Module intro_pat.
-Inductive token :=
-  | TName : string → token
-  | TAnom : token
-  | TFrame : token
-  | TBar : token
-  | TBracketL : token
-  | TBracketR : token
-  | TAmp : token
-  | TParenL : token
-  | TParenR : token
-  | TPureElim : token
-  | TAlwaysElim : token
-  | TModalElim : token
-  | TPureIntro : token
-  | TAlwaysIntro : token
-  | TModalIntro : token
-  | TSimpl : token
-  | TForall : token
-  | TAll : token
-  | TClearL : token
-  | TClearR : 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 (TAnom :: cons_name kn k) ""
-  | String "$" s => tokenize_go s (TFrame :: 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 (TPureElim :: cons_name kn k) ""
-  | String "#" s => tokenize_go s (TAlwaysElim :: cons_name kn k) ""
-  | String ">" s => tokenize_go s (TModalElim :: cons_name kn k) ""
-  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
-  | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
-  | String "!" (String ">" s) => tokenize_go s (TModalIntro :: 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 =>
-     if is_space a then tokenize_go s (cons_name kn k) ""
-     else tokenize_go s k (String a kn)
-  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
-  end.
-Definition tokenize (s : string) : list token := tokenize_go s [] "".
-
 Inductive stack_item :=
   | SPat : intro_pat → stack_item
   | SList : stack_item
@@ -132,23 +80,23 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TParenL :: ts => parse_go ts (SConjList :: k)
   | TAmp :: ts => parse_go ts (SAmp :: k)
   | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
-  | TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
-  | TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
-  | TModalElim :: ts => parse_go ts (SModalElim :: k)
+  | TPure :: ts => parse_go ts (SPat IPureElim :: k)
+  | TAlways :: ts => parse_go ts (SAlwaysElim :: k)
+  | TModal :: ts => parse_go ts (SModalElim :: k)
   | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
   | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
   | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
-  | TClearL :: ts => parse_clear ts k
+  | TBraceL :: ts => parse_clear ts k
   | _ => None
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
   | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
   | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
-  | TClearR :: ts => parse_go ts k
+  | TBraceR :: ts => parse_go ts k
   | _ => None
   end.
 
@@ -161,7 +109,6 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
   | _ => None
   end.
 
-
 Definition parse (s : string) : option (list intro_pat) :=
   k ← parse_go (tokenize s) []; close k [].
 

theories/proofmode/sel_patterns.v

 From stdpp Require Export strings.
+From iris.proofmode Require Import tokens.
 Set Default Proof Using "Type".
 
 Inductive sel_pat :=
@@ -15,28 +16,25 @@ Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
   end.
 
 Module sel_pat.
-Fixpoint cons_name (kn : string) (k : list sel_pat) : list sel_pat :=
-  match kn with "" => k | _ => SelName (string_rev kn) :: k end.
-
-Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat :=
-  match s with
-  | "" => rev (cons_name kn k)
-  | String "%" s => parse_go s (SelPure :: cons_name kn k) ""
-  | String "#" s => parse_go s (SelPersistent :: cons_name kn k) ""
-  | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
-      (String (Ascii.Ascii false false false true false false false true)
-      (String (Ascii.Ascii true true true false true false false true) s)) =>
-     parse_go s (SelSpatial :: cons_name kn k) ""
-  | String a s =>
-     if is_space a then parse_go s (cons_name kn k) ""
-     else parse_go s k (String a kn)
+Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
+  match ts with
+  | [] => Some (reverse k)
+  | TName s :: ts => parse_go ts (SelName s :: k)
+  | TPure :: ts => parse_go ts (SelPure :: k)
+  | TAlways :: ts => parse_go ts (SelPersistent :: k)
+  | TSep :: ts => parse_go ts (SelSpatial :: k)
+  | _ => None
   end.
-Definition parse (s : string) : list sel_pat := parse_go s [] "".
+Definition parse (s : string) : option (list sel_pat) :=
+  parse_go (tokenize s) [].
 
 Ltac parse s :=
   lazymatch type of s with
   | list sel_pat => s
   | list string => eval vm_compute in (SelName <$> s)
-  | string => eval vm_compute in (parse s)
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some ?pats => pats | _ => fail "invalid sel_pat" s
+     end
   end.
 End sel_pat.

theories/proofmode/spec_patterns.v

 From stdpp Require Export strings.
+From iris.proofmode Require Import tokens.
 Set Default Proof Using "Type".
 
 Record spec_goal := SpecGoal {
@@ -19,46 +20,15 @@ Definition spec_pat_modal (p : spec_pat) : bool :=
   match p with SGoal g => spec_goal_modal g | _ => false end.
 
 Module spec_pat.
-Inductive token :=
-  | TName : string → token
-  | TMinus : token
-  | TBracketL : token
-  | TBracketR : token
-  | TPersistent : token
-  | TPure : token
-  | TForall : token
-  | TModal : token
-  | TFrame : 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 (TMinus :: 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 (TPersistent :: cons_name kn k) ""
-  | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
-  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
-  | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
-  | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
-  | String a s =>
-     if is_space a then tokenize_go s (cons_name kn k) ""
-     else tokenize_go s k (String a kn)
-  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
-  end.
-Definition tokenize (s : string) : list token := tokenize_go s [] "".
-
 Inductive state :=
   | StTop : state
   | StAssert : spec_goal → state.
 
 Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
   match ts with
-  | [] => Some (rev k)
+  | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SName s :: k)
-  | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
+  | TBracketL :: TAlways :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
   | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
   | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k

theories/proofmode/tokens.v

+From stdpp Require Export strings.
+Set Default Proof Using "Type".
+
+Inductive token :=
+  | TName : string → token
+  | TAnom : token
+  | TFrame : token
+  | TBar : token
+  | TBracketL : token
+  | TBracketR : token
+  | TAmp : token
+  | TParenL : token
+  | TParenR : token
+  | TBraceL : token
+  | TBraceR : token
+  | TPure : token
+  | TAlways : token
+  | TModal : token
+  | TPureIntro : token
+  | TAlwaysIntro : token
+  | TModalIntro : token
+  | TSimpl : token
+  | TForall : token
+  | TAll : token
+  | TMinus : token
+  | TSep : 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
+  | "" => reverse (cons_name kn k)
+  | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
+  | String "$" s => tokenize_go s (TFrame :: 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 (TBraceL :: cons_name kn k) ""
+  | String "}" s => tokenize_go s (TBraceR :: cons_name kn k) ""
+  | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
+  | String "#" s => tokenize_go s (TAlways :: cons_name kn k) ""
+  | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
+  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
+  | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
+  | String "!" (String ">" s) => tokenize_go s (TModalIntro :: 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 "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
+  | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
+      (String (Ascii.Ascii false false false true false false false true)
+      (String (Ascii.Ascii true true true false true false false true) s)) =>
+     tokenize_go s (TSep :: cons_name kn k) ""
+  | String a s =>
+     if is_space a then tokenize_go s (cons_name kn k) ""
+     else tokenize_go s k (String a kn)
+  (* TODO: Complain about invalid characters, to future-proof this
+  against making more characters special. *)
+  end.
+Definition tokenize (s : string) : list token := tokenize_go s [] "".