From 9ae100fa57fcb45a32cb601f91c4ee0afcbddea8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 18 Feb 2017 18:58:56 +0100
Subject: [PATCH] Unify tokenizers for intro, spec, and sel patterns.
---
_CoqProject | 1 +
theories/proofmode/intro_patterns.v | 65 +++--------------------------
theories/proofmode/sel_patterns.v | 32 +++++++-------
theories/proofmode/spec_patterns.v | 36 ++--------------
theories/proofmode/tokens.v | 63 ++++++++++++++++++++++++++++
5 files changed, 88 insertions(+), 109 deletions(-)
create mode 100644 theories/proofmode/tokens.v
diff --git a/_CoqProject b/_CoqProject
index dbeb27192..784ef81cb 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index c1cc121e8..84af8d271 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,4 +1,5 @@
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 [].
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index b019b2c53..01581650c 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,4 +1,5 @@
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.
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index a1633aa88..be72220b4 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,4 +1,5 @@
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
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
new file mode 100644
index 000000000..be8d97c4e
--- /dev/null
+++ b/theories/proofmode/tokens.v
@@ -0,0 +1,63 @@
+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 [] "".
--
GitLab