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 : option string token
  | TIntuitionistic : token
  | TModal : token
  | TPureIntro : token
  | TIntuitionisticIntro : 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
  | SPure : string state
  | SNone : state.

Definition cons_state (kn : state) (k : list token) : list token :=
  match kn with
  | SNonek
  | SName sTName (string_rev s) :: k
  | SPure sTPure (if String.eqb s "" then None else Some (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 (cons_state kn k) (SPure "")
  | String "#" stokenize_go s (TIntuitionistic :: 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 (TIntuitionisticIntro :: 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'))
     | SPure s'tokenize_go s k (SPure (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.