diff options
Diffstat (limited to 'shared.v')
-rw-r--r-- | shared.v | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/shared.v b/shared.v new file mode 100644 index 0000000..8e9484f --- /dev/null +++ b/shared.v | |||
@@ -0,0 +1,66 @@ | |||
1 | Require Import Coq.NArith.BinNat. | ||
2 | Require Import Coq.Strings.Ascii. | ||
3 | Require Import Coq.Strings.String. | ||
4 | From stdpp Require Import fin_sets gmap option. | ||
5 | From mininix Require Import expr maptools. | ||
6 | |||
7 | Open Scope string_scope. | ||
8 | Open Scope N_scope. | ||
9 | Open Scope Z_scope. | ||
10 | Open Scope nat_scope. | ||
11 | |||
12 | Definition nonrecs : gmap string b_rhs → gmap string expr := | ||
13 | omap (λ b, match b with B_Nonrec e => Some e | _ => None end). | ||
14 | |||
15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. | ||
16 | Proof. | ||
17 | induction bs using map_ind. | ||
18 | - done. | ||
19 | - unfold nonrecs. | ||
20 | rewrite fmap_insert. | ||
21 | rewrite omap_insert_Some with (y := x); try done. | ||
22 | by f_equal. | ||
23 | Qed. | ||
24 | |||
25 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. | ||
26 | Proof. | ||
27 | unfold rec_subst. | ||
28 | rewrite <-map_fmap_compose. | ||
29 | unfold compose. | ||
30 | by rewrite map_fmap_id. | ||
31 | Qed. | ||
32 | |||
33 | Definition ascii_ltb (c1 c2 : ascii) : bool := | ||
34 | bool_decide (N_of_ascii c1 < N_of_ascii c2)%N. | ||
35 | |||
36 | Fixpoint string_lt (s1 s2 : string) : bool := | ||
37 | match s1, s2 with | ||
38 | | _, EmptyString => false | ||
39 | | EmptyString, String _ _ => true | ||
40 | | String c1 s1', String c2 s2' => ascii_ltb c1 c2 || string_lt s1' s2' | ||
41 | end. | ||
42 | |||
43 | Fixpoint expr_eq (e1 e2 : expr) : bool := | ||
44 | match e1, e2 with | ||
45 | | V_Null, V_Null => false | ||
46 | | V_Bool b1, V_Bool b2 => bool_decide (b1 = b2) | ||
47 | | V_Int n1, V_Int n2 => bool_decide (n1 = n2) | ||
48 | | V_Str s1, V_Str s2 => bool_decide (s1 = s2) | ||
49 | | V_Attrset bs1, V_Attrset bs2 => bool_decide (dom bs1 = dom bs2) && | ||
50 | map_fold (λ x e1' acc, match bs2 !! x with | ||
51 | | None => false | ||
52 | | Some e2' => acc && expr_eq e1' e2' | ||
53 | end) true bs1 | ||
54 | | _, _ => false | ||
55 | end. | ||
56 | |||
57 | Definition prelude : gmap string expr := | ||
58 | {[ "true" := X_V true; | ||
59 | "false" := X_V false; | ||
60 | "null" := X_V V_Null; | ||
61 | "builtins" := X_Attrset | ||
62 | {[ "true" := B_Nonrec true; | ||
63 | "false" := B_Nonrec false; | ||
64 | "null" := B_Nonrec V_Null | ||
65 | ]} | ||
66 | ]}. | ||