blob: 34cca7bb894dd02ecf8a4e17d3eeac7271395d70 (
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
39
40
41
|
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.
|
