From Coq Require Import Ascii.
From mininix Require Export utils.
From stdpp Require Import options.

Module Import evallang.

Inductive expr :=
  | EString (s : string)
  | EId (ds : option expr) (x : string)
  | EEval (ds : gmap string expr) (ee : expr)
  | EAbs (ex e : expr)
  | EApp (e1 e2 : expr).

Module parser.
  Inductive token :=
    | TId (s : string)
    | TString (s : string)
    | TColon
    | TExclamation
    | TParenL
    | TParenR.

  Inductive token_state :=
    TSString (s : string) | TSId (s : string) | TSOther.

  Definition token_state_push (st : token_state) (k : list token) : list token :=
    match st with
    | TSId s => TId (String.rev s) :: k
    | _ => k
    end.

  Fixpoint tokenize_go (sin : string) (st : token_state)
      (k : list token) : option (list token) :=
    match sin, st with
    | "", TSString _ => None (* no closing "" *)
    | "", _ => Some (reverse (token_state_push st k))
    | String "\" (String """" sin), TSString s =>
        tokenize_go sin (TSString (String """" s)) k
    | String """" sin, TSString s =>
        tokenize_go sin TSOther (TString (String.rev s) :: k)
    | String a sin, TSString s => tokenize_go sin (TSString (String a s)) k
    | String ":" sin, _ => tokenize_go sin TSOther (TColon :: token_state_push st k)
    | String "!" sin, _ => tokenize_go sin TSOther (TExclamation :: token_state_push st k)
    | String "(" sin, _ => tokenize_go sin TSOther (TParenL :: token_state_push st k)
    | String ")" sin, _ => tokenize_go sin TSOther (TParenR :: token_state_push st k)
    | String """" sin, _ => tokenize_go sin (TSString "") k
    | String a sin, TSOther =>
       if Ascii.is_space a then tokenize_go sin TSOther k
       else tokenize_go sin (TSId (String a EmptyString)) k
    | String a sin, TSId s =>
       if Ascii.is_space a then tokenize_go sin TSOther (TId (String.rev s) :: k)
       else tokenize_go sin (TSId (String a s)) k
    end.
  Definition tokenize (sin : string) : option (list token) :=
    tokenize_go sin TSOther [].

  Inductive stack_item :=
    | SExpr (e : expr)
    | SAbsR (e : expr)
    | SEval
    | SParenL.

  Definition stack_push (e : expr) (k : list stack_item) : list stack_item :=
    match k with
    | SExpr e1 :: k => SExpr (EApp e1 e) :: k
    | SEval :: k => SExpr (EEval ∅ e) :: k
    | _ => SExpr e :: k
    end.

  Fixpoint stack_pop_go (e : expr)
      (k : list stack_item) : option (expr * list stack_item) :=
    match k with
    | SAbsR e1 :: k => stack_pop_go (EAbs e1 e) k
    | _ => Some (e, k)
    end.

  Definition stack_pop (k : list stack_item) : option (expr * list stack_item) :=
    match k with
    | SExpr e :: k => stack_pop_go e k
    | _ => None
    end.

  Fixpoint parse_go (ts : list token) (k : list stack_item) : option expr :=
    match ts with
    | [] => '(e, k) ← stack_pop k; guard (k = []);; Some e
    | TString x :: ts => parse_go ts (stack_push (EString x) k)
    | TId "eval" :: TExclamation :: ts => parse_go ts (SEval :: k)
    | TId x :: TColon :: ts => parse_go ts (SAbsR (EString x) :: k)
    | TId x :: ts => parse_go ts (stack_push (EId None x) k)
    | TColon :: ts =>
       '(e, k) ← stack_pop k;
       parse_go ts (SAbsR e :: k)
    | TParenL :: ts => parse_go ts (SParenL :: k)
    | TParenR :: ts =>
       '(e, k) ← stack_pop k;
       match k with
       | SParenL :: k => parse_go ts (stack_push e k)
       | _ => None
       end
    | _ => None
    end.

  Definition parse (sin : string) : option expr :=
    ts ← tokenize sin; parse_go ts [].
End parser.

Definition parse := parser.parse.

Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
  match e with
  | EString s => EString s
  | EId ds' x => EId (ds !! x ∪ ds') x
  | EEval ds' ee => EEval (ds ∪ ds') (subst ds ee)
  | EAbs ex e => EAbs (subst ds ex) (subst ds e)
  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
  end.

Reserved Infix "-->" (right associativity, at level 55).
Inductive step : expr → expr → Prop :=
  | Sβ x e1 e2 : EApp (EAbs (EString x) e1) e2 --> subst {[x:=e2]} e1
  | SId e x : EId (Some e) x --> e
  | SEvalString ds s e : parse s = Some e → EEval ds (EString s) --> subst ds e
  | SAbsL ex1 ex1' e : ex1 --> ex1' → EAbs ex1 e --> EAbs ex1' e
  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
  | SEval ds e1 e1' : e1 --> e1' → EEval ds e1 --> EEval ds e1'
where "e1 --> e2" := (step e1 e2).

Infix "-->*" := (rtc step) (right associativity, at level 55).

Definition final (e : expr) : Prop :=
  match e with
  | EString _ => True
  | EAbs (EString _) _ => True
  | _ => False
  end.

Definition stuck (e : expr) : Prop :=
  nf step e ∧ ¬final e.

End evallang.