blob: dcf6b9566fbae1877e85e7832321eba27415a6b1 (
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
42
43
44
45
46
47
48
49
|
From mininix Require Export res dynlang.operational_props.
From stdpp Require Import options.
Module Import dynlang.
Export dynlang.
Inductive thunk := Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
Add Printing Constructor thunk.
Notation env := (gmap string thunk).
Inductive val :=
| VString (s : string)
| VClo (x : string) (E : env) (e : expr).
Global Instance maybe_VString : Maybe VString := λ v,
if v is VString s then Some s else None.
Global Instance maybe_VClo : Maybe3 VClo := λ v,
if v is VClo x E e then Some (x, E, e) else None.
Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
match e with
| EString s =>
mret (VString s)
| EId ds e =>
v ← interp E e;
x ← Res $ maybe VString v;
t ← Res $ (E !! x) ∪ (Thunk ∅ <$> ds !! x);
interp (thunk_env t) (thunk_expr t)
| EAbs ex e =>
v ← interp E ex;
x ← Res $ maybe VString v;
mret (VClo x E e)
| EApp e1 e2 =>
v1 ← interp E e1;
'(x, E', e') ← Res (maybe3 VClo v1);
interp (<[x:=Thunk E e2]> E') e'
end.
Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
match n with
| O => NoFuel
| S n => interp1 (interp n) E e
end.
Global Opaque interp.
End dynlang.
Add Printing Constructor dynlang.thunk.
|
