aboutsummaryrefslogtreecommitdiffstats
path: root/theories/lambda/interp.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/lambda/interp.v')
-rw-r--r--theories/lambda/interp.v44
1 files changed, 44 insertions, 0 deletions
diff --git a/theories/lambda/interp.v b/theories/lambda/interp.v
new file mode 100644
index 0000000..5bc60d1
--- /dev/null
+++ b/theories/lambda/interp.v
@@ -0,0 +1,44 @@
1From mininix Require Export res lambda.operational_props.
2From stdpp Require Import options.
3
4Module Import lambda.
5Export lambda.
6
7Inductive thunk :=
8 Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
9Add Printing Constructor thunk.
10Notation env := (gmap string thunk).
11
12Inductive val :=
13 | VString (s : string)
14 | VClo (x : string) (E : env) (e : expr).
15
16Global Instance maybe_VClo : Maybe3 VClo := λ v,
17 if v is VClo x E e then Some (x, E, e) else None.
18
19Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
20 match e with
21 | EString s =>
22 mret (VString s)
23 | EId x =>
24 t ← Res (E !! x);
25 interp (thunk_env t) (thunk_expr t)
26 | EAbs x e =>
27 mret (VClo x E e)
28 | EApp e1 e2 =>
29 v1 ← interp E e1;
30 '(x, E', e') ← Res (maybe3 VClo v1);
31 interp (<[x:=Thunk E e2]> E') e'
32 end.
33
34Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
35 match n with
36 | O => NoFuel
37 | S n => interp1 (interp n) E e
38 end.
39
40Global Opaque interp.
41
42End lambda.
43
44Add Printing Constructor lambda.thunk.