Library iris.proofmode.tokens

From iris.proofmode Require Import base.
Set Default Proof Using "Type".

Inductive token :=
  | TName : string token
  | TNat : nat token
  | TAnon : 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
  | SNonek
  | SName sTName (string_rev s) :: k
  | SNat nTNat n :: k
  end.

Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
  match s with
  | "" ⇒ reverse (cons_state kn k)
  | String "?" stokenize_go s (TAnon :: cons_state kn k) SNone
  | String "$" stokenize_go s (TFrame :: cons_state kn k) SNone
  | String "[" stokenize_go s (TBracketL :: cons_state kn k) SNone
  | String "]" stokenize_go s (TBracketR :: cons_state kn k) SNone
  | String "|" stokenize_go s (TBar :: cons_state kn k) SNone
  | String "(" stokenize_go s (TParenL :: cons_state kn k) SNone
  | String ")" stokenize_go s (TParenR :: cons_state kn k) SNone
  | String "&" stokenize_go s (TAmp :: cons_state kn k) SNone
  | String "{" stokenize_go s (TBraceL :: cons_state kn k) SNone
  | String "}" stokenize_go s (TBraceR :: cons_state kn k) SNone
  | String "%" stokenize_go s (TPure :: cons_state kn k) SNone
  | String "#" stokenize_go s (TAlways :: cons_state kn k) SNone
  | String ">" stokenize_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 "*" stokenize_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 "-" stokenize_go s (TMinus :: cons_state kn k) SNone
  | String (Ascii.Ascii false true false false false true true true)
      (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
     
     if is_space a then tokenize_go s (cons_state kn k) SNone else
     match kn with
     | SNone
        match is_nat a with
        | Some ntokenize_go s k (SNat n)
        | Nonetokenize_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))
        | Nonetokenize_go s (TNat n :: k) (SName (String a ""))
        end
     end
  end.
Definition tokenize (s : string) : list token := tokenize_go s [] SNone.