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

Module Import dynlang.

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

Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
  match e with
  | EString s => EString s
  | EId ds' e => EId (ds ∪ ds') (subst ds e)
  | 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
  | SIdString ds x e : ds !! x = Some e → EId ds (EString x) --> 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
  | SId ds e1 e1' : e1 --> e1' → EId ds e1 --> EId 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 dynlang.