tokens.v 3.73 KB
Newer Older
1
From iris.proofmode Require Import base.
2 3 4 5
Set Default Proof Using "Type".

Inductive token :=
  | TName : string  token
6
  | TNat : nat  token
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
  | 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
24
  | TDone : token
25 26 27
  | TForall : token
  | TAll : token
  | TMinus : token
28 29
  | TSep : token
  | TArrow : direction  token.
30

31 32 33 34 35 36 37 38 39 40 41 42 43
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 :=
44
  match s with
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  | "" => 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
62
  | String "/" (String "/" (String "=" s)) =>
63 64 65 66 67
     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
68 69
  | 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
70
  | String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
71 72 73
  | 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)) =>
74
     tokenize_go s (TSep :: cons_state kn k) SNone
75
  | String a s =>
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
     (* 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
92
  end.
93
Definition tokenize (s : string) : list token := tokenize_go s [] SNone.