blob: b0fa366709a8a3ab20cd2ceeb0e80635a276d0cc (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
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.
|
