tokens.v 2.43 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From fast_string Require Export fast_string_lib.
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
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
Fixpoint cons_name (kn : list char) (k : list token) : list token :=
  match kn with [] => k | _ => TName (String (reverse kn)) :: k end.
Fixpoint tokenize_go (s : list char) (k : list token) (kn : list char) : list token :=
31
  match s with
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  | [] => reverse (cons_name kn k)
  | "?" :: s => tokenize_go s (TAnom :: cons_name kn k) []
  | "$" :: s => tokenize_go s (TFrame :: cons_name kn k) []
  | "[" :: s => tokenize_go s (TBracketL :: cons_name kn k) []
  | "]" :: s => tokenize_go s (TBracketR :: cons_name kn k) []
  | "|" :: s => tokenize_go s (TBar :: cons_name kn k) []
  | "(" :: s => tokenize_go s (TParenL :: cons_name kn k) []
  | ")" :: s => tokenize_go s (TParenR :: cons_name kn k) []
  | "&" :: s => tokenize_go s (TAmp :: cons_name kn k) []
  | "{" :: s => tokenize_go s (TBraceL :: cons_name kn k) []
  | "}" :: s => tokenize_go s (TBraceR :: cons_name kn k) []
  | "%" :: s => tokenize_go s (TPure :: cons_name kn k) []
  | "#" :: s => tokenize_go s (TAlways :: cons_name kn k) []
  | ">" :: s => tokenize_go s (TModal :: cons_name kn k) []
  | "!" :: "%" :: s => tokenize_go s (TPureIntro :: cons_name kn k) []
  | "!" :: "#" :: s => tokenize_go s (TAlwaysIntro :: cons_name kn k) []
  | "!" :: ">" :: s => tokenize_go s (TModalIntro :: cons_name kn k) []
  | "/" :: "=" :: s => tokenize_go s (TSimpl :: cons_name kn k) []
  | "*" :: "*" :: s => tokenize_go s (TAll :: cons_name kn k) []
  | "*" :: s => tokenize_go s (TForall :: cons_name kn k) []
  | "-" :: s => tokenize_go s (TMinus :: cons_name kn k) []
  | C226 :: C136 :: C151 :: s (* unicode ∗ *) =>
     tokenize_go s (TSep :: cons_name kn k) []
  | a :: s =>
     if is_space a then tokenize_go s (cons_name kn k) []
     else tokenize_go s k (a :: kn)
58
59
  (* TODO: Complain about invalid characters, to future-proof this
  against making more characters special. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
62
  end%char.
Definition tokenize (s : string) : list token :=
  tokenize_go (string_car s) [] [].