From mininix Require Export res evallang.operational_props.
From stdpp Require Import options.

Module Import evallang.
Export evallang.

Inductive thunk := Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
Add Printing Constructor thunk.
Notation env := (gmap string thunk).

Inductive val :=
  | VString (s : string)
  | VClo (x : string) (E : env) (e : expr).

Global Instance maybe_VString : Maybe VString := λ v,
  if v is VString s then Some s else None.
Global Instance maybe_VClo : Maybe3 VClo := λ v,
  if v is VClo x E e then Some (x, E, e) else None.

Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
  match e with
  | EString s =>
      mret (VString s)
  | EId ds x =>
      t ← Res $ (E !! x) ∪ (Thunk ∅ <$> ds);
      interp (thunk_env t) (thunk_expr t)
  | EEval ds e =>
      v ← interp E e;
      s ← Res $ maybe VString v;
      e ← Res $ parse s;
      interp (E ∪ (Thunk ∅ <$> ds)) e
  | EAbs ex e =>
      v ← interp E ex;
      x ← Res $ maybe VString v;
      mret (VClo x E e)
  | EApp e1 e2 =>
      v1 ← interp E e1;
      '(x, E', e') ← Res (maybe3 VClo v1);
      interp (<[x:=Thunk E e2]> E') e'
  end.

Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
  match n with
  | O => NoFuel
  | S n => interp1 (interp n) E e
  end.

Global Opaque interp.

End evallang.

Add Printing Constructor evallang.thunk.