diff options
author | Rutger Broekhoff | 2024-06-26 20:50:18 +0200 |
---|---|---|
committer | Rutger Broekhoff | 2024-06-26 20:50:18 +0200 |
commit | 73df1945b31c0beee88cf4476df4ccd09d31403b (patch) | |
tree | ed00db26b711442e643f38b66888a3df56e33ebd /interpreter.v | |
download | mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.tar.gz mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.zip |
Import Coq project
Diffstat (limited to 'interpreter.v')
-rw-r--r-- | interpreter.v | 103 |
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 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import fin_maps. | ||
3 | From mininix Require Import binop expr maptools matching. | ||
4 | |||
5 | Open Scope string_scope. | ||
6 | |||
7 | Definition 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 | |||
90 | Fixpoint 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 *) | ||
101 | Global Opaque eval. | ||
102 | Lemma eval_S n : eval (S n) = eval1 (eval n). | ||
103 | Proof. done. Qed. | ||