aboutsummaryrefslogtreecommitdiffstats
path: root/interpreter.v
diff options
context:
space:
mode:
authorLibravatar Rutger Broekhoff2024-06-26 20:50:18 +0200
committerLibravatar Rutger Broekhoff2024-06-26 20:50:18 +0200
commit73df1945b31c0beee88cf4476df4ccd09d31403b (patch)
treeed00db26b711442e643f38b66888a3df56e33ebd /interpreter.v
downloadmininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.tar.gz
mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.zip
Import Coq project
Diffstat (limited to 'interpreter.v')
-rw-r--r--interpreter.v103
1 files changed, 103 insertions, 0 deletions
diff --git a/interpreter.v b/interpreter.v
new file mode 100644
index 0000000..c701b42
--- /dev/null
+++ b/interpreter.v
@@ -0,0 +1,103 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import fin_maps.
3From mininix Require Import binop expr maptools matching.
4
5Open Scope string_scope.
6
7Definition eval1 (go : bool → expr → option value)
8 (uf : bool) (d : expr) : option value :=
9 match d with
10 | X_Id _ => None
11 | X_Force e => go true e
12 | X_Closed e => go uf e
13 | X_Placeholder x e => go uf e
14 | X_V (V_Attrset bs) =>
15 if uf
16 then vs' ← map_mapM (go true) bs;
17 Some (V_Attrset (X_V <$> vs'))
18 else Some (V_Attrset bs)
19 | X_V v => Some v
20 | X_Attrset bs => go uf (V_Attrset (rec_subst bs))
21 | X_LetBinding bs e =>
22 let e' := subst (closed (rec_subst bs)) e
23 in go uf e'
24 | X_Select e (Ne_Cons x ys) =>
25 v' ← go false e;
26 bs ← maybe V_Attrset v';
27 e'' ← bs !! x;
28 match ys with
29 | [] => go uf e''
30 | y :: ys => go uf (X_Select e'' (Ne_Cons y ys))
31 end
32 | X_SelectOr e (Ne_Cons x ys) or =>
33 v' ← go false e;
34 bs ← maybe V_Attrset v';
35 match bs !! x with
36 | Some e'' =>
37 match ys with
38 | [] => go uf e''
39 | y :: ys => go uf (X_SelectOr e'' (Ne_Cons y ys) or)
40 end
41 | None => go uf or
42 end
43 | X_Apply e1 e2 =>
44 v1' ← go false e1;
45 match v1' with
46 | V_Fn x e =>
47 let e' := subst {[x := X_Closed e2]} e
48 in go uf e'
49 | V_AttrsetFn m e =>
50 v2' ← go false e2;
51 bs ← maybe V_Attrset v2';
52 bs' ← matches m bs;
53 go uf (X_LetBinding bs' e)
54 | V_Attrset bs =>
55 f ← bs !! "__functor";
56 go uf (X_Apply (X_Apply f (V_Attrset bs)) e2)
57 | _ => None
58 end
59 | X_Cond e1 e2 e3 =>
60 v1' ← go false e1;
61 b ← maybe V_Bool v1';
62 go uf (if b : bool then e2 else e3)
63 | X_Incl e1 e2 =>
64 v1' ← go false e1;
65 match v1' with
66 | V_Attrset bs => go uf (subst (placeholders bs) e2)
67 | _ => go uf e2
68 end
69 | X_Op op e1 e2 =>
70 e1' ← go false e1;
71 e2' ← go false e2;
72 v' ← binop_eval op e1' e2';
73 go uf (X_V v')
74 | X_HasAttr e x =>
75 v' ← go false e;
76 Some $ V_Bool $
77 match v' with
78 | V_Attrset bs =>
79 bool_decide (is_Some (bs !! x))
80 | _ => false
81 end
82 | X_Assert e1 e2 =>
83 v1' ← go false e1;
84 match v1' with
85 | V_Bool true => go uf e2
86 | _ => None
87 end
88 end.
89
90Fixpoint eval (n : nat) (uf : bool) (e : expr) : option value :=
91 match n with
92 | O => None
93 | S n => eval1 (eval n) uf e
94 end.
95
96(* Don't automatically 'simplify' eval: this can lead to very complicated
97 assumptions and goals. Instead, we define our own lemma which can be used
98 to unfold eval once. This allows us to write proofs in a much more
99 controlled manner, and we can still leverage tactics like simplify_option_eq
100 without everything blowing up uncontrollably *)
101Global Opaque eval.
102Lemma eval_S n : eval (S n) = eval1 (eval n).
103Proof. done. Qed.