-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathtokens.v
93 lines (89 loc) · 3.73 KB
/
tokens.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
From iris.proofmode Require Import base.
Set Default Proof Using "Type".
Inductive token :=
| TName : string → token
| TNat : nat → 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
| TDone : token
| TForall : token
| TAll : token
| TMinus : token
| TSep : token
| TArrow : direction → token.
Inductive state :=
| SName : string → state
| SNat : nat → state
| SNone : state.
Definition cons_state (kn : state) (k : list token) : list token :=
match kn with
| SNone => k
| SName s => TName (string_rev s) :: k
| SNat n => TNat n :: k
end.
Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
match s with
| "" => reverse (cons_state kn k)
| String "?" s => tokenize_go s (TAnom :: cons_state kn k) SNone
| String "$" s => tokenize_go s (TFrame :: cons_state kn k) SNone
| String "[" s => tokenize_go s (TBracketL :: cons_state kn k) SNone
| String "]" s => tokenize_go s (TBracketR :: cons_state kn k) SNone
| String "|" s => tokenize_go s (TBar :: cons_state kn k) SNone
| String "(" s => tokenize_go s (TParenL :: cons_state kn k) SNone
| String ")" s => tokenize_go s (TParenR :: cons_state kn k) SNone
| String "&" s => tokenize_go s (TAmp :: cons_state kn k) SNone
| String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
| String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
| String "%" s => tokenize_go s (TPure :: cons_state kn k) SNone
| String "#" s => tokenize_go s (TAlways :: cons_state kn k) SNone
| String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_state kn k) SNone
| String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
| String "/" (String "/" (String "=" s)) =>
tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone
| String "/" (String "/" s) => tokenize_go s (TDone :: cons_state kn k) SNone
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_state kn k) SNone
| String "*" (String "*" s) => tokenize_go s (TAll :: cons_state kn k) SNone
| String "*" s => tokenize_go s (TForall :: cons_state kn k) SNone
| String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
| String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
| String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
| 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_state kn k) SNone
| String a s =>
(* TODO: Complain about invalid characters, to future-proof this
against making more characters special. *)
if is_space a then tokenize_go s (cons_state kn k) SNone else
match kn with
| SNone =>
match is_nat a with
| Some n => tokenize_go s k (SNat n)
| None => tokenize_go s k (SName (String a ""))
end
| SName s' => tokenize_go s k (SName (String a s'))
| SNat n =>
match is_nat a with
| Some n' => tokenize_go s k (SNat (n' + 10 * n))
| None => tokenize_go s (TNat n :: k) (SName (String a ""))
end
end
end.
Definition tokenize (s : string) : list token := tokenize_go s [] SNone.