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

Module Import lambda.

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

Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
  match e with
  | EString s => EString s
  | EId x => if ds !! x is Some d then d else EId x
  | EAbs x e => EAbs x (subst (delete x 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 x e1) e2 --> subst {[x:=e2]} e1
  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
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 _ _ => True
  | _ => False
  end.

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

End lambda.