aboutsummaryrefslogtreecommitdiffstats
path: root/sem.v
diff options
context:
space:
mode:
Diffstat (limited to 'sem.v')
-rw-r--r--sem.v167
1 files changed, 167 insertions, 0 deletions
diff --git a/sem.v b/sem.v
new file mode 100644
index 0000000..6560b82
--- /dev/null
+++ b/sem.v
@@ -0,0 +1,167 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap.
3From mininix Require Import binop expr matching relations.
4
5Definition attrset := is_Some ∘ maybe V_Attrset.
6
7Reserved Infix "-->base" (right associativity, at level 55).
8
9Inductive base_step : expr → expr → Prop :=
10 | E_Force (sv : strong_value) :
11 X_Force sv -->base sv
12 | E_Closed e :
13 X_Closed e -->base e
14 | E_Placeholder x e :
15 X_Placeholder x e -->base e
16 | E_MSelect bs x ys :
17 X_Select (V_Attrset bs) (nonempty_cons x ys) -->base
18 X_Select (X_Select (V_Attrset bs) (nonempty_singleton x)) ys
19 | E_Select e bs x :
20 X_Select (V_Attrset (<[x := e]>bs)) (nonempty_singleton x) -->base e
21 | E_SelectOr bs x e :
22 X_SelectOr (V_Attrset bs) (nonempty_singleton x) e -->base
23 X_Cond (X_HasAttr (V_Attrset bs) x)
24 (* if true *)
25 (X_Select (V_Attrset bs) (nonempty_singleton x))
26 (* if false *)
27 e
28 | E_MSelectOr bs x ys e :
29 X_SelectOr (V_Attrset bs) (nonempty_cons x ys) e -->base
30 X_Cond (X_HasAttr (V_Attrset bs) x)
31 (* if true *)
32 (X_SelectOr
33 (X_Select (V_Attrset bs) (nonempty_singleton x))
34 ys e)
35 (* if false *)
36 e
37 | E_Rec bs :
38 X_Attrset bs -->base V_Attrset (rec_subst bs)
39 | E_Let e bs :
40 X_LetBinding bs e -->base subst (closed (rec_subst bs)) e
41 | E_With e bs :
42 X_Incl (V_Attrset bs) e -->base subst (placeholders bs) e
43 | E_WithNoAttrset v1 e2 :
44 ¬ attrset v1 →
45 X_Incl v1 e2 -->base e2
46 | E_ApplySimple x e1 e2 :
47 X_Apply (V_Fn x e1) e2 -->base subst {[x := X_Closed e2]} e1
48 | E_ApplyAttrset m e bs bs' :
49 bs ~ m ~> bs' →
50 X_Apply (V_AttrsetFn m e) (V_Attrset bs) -->base
51 X_LetBinding bs' e
52 | E_ApplyFunctor e1 e2 bs :
53 X_Apply (V_Attrset (<["__functor" := e2]>bs)) e1 -->base
54 X_Apply (X_Apply e2 (V_Attrset (<["__functor" := e2]>bs))) e1
55 | E_IfTrue e2 e3 :
56 X_Cond true e2 e3 -->base e2
57 | E_IfFalse e2 e3 :
58 X_Cond false e2 e3 -->base e3
59 | E_Op op v1 v2 u :
60 v1 ⟦op⟧ v2 -⊚-> u →
61 X_Op op v1 v2 -->base u
62 | E_OpHasAttrTrue bs x :
63 is_Some (bs !! x) →
64 X_HasAttr (V_Attrset bs) x -->base true
65 | E_OpHasAttrFalse bs x :
66 bs !! x = None →
67 X_HasAttr (V_Attrset bs) x -->base false
68 | E_OpHasAttrNoAttrset v x :
69 ¬ attrset v →
70 X_HasAttr v x -->base false
71 | E_Assert e2 :
72 X_Assert true e2 -->base e2
73where "e -->base e'" := (base_step e e').
74
75Notation "e '-->base*' e'" := (rtc base_step e e')
76 (right associativity, at level 55).
77
78Hint Constructors base_step : core.
79
80Variant is_ctx_item : bool → bool → (expr → expr) → Prop :=
81 | IsCtxItem_Select uf_ext xs :
82 is_ctx_item uf_ext false (λ e1, X_Select e1 xs)
83 | IsCtxItem_SelectOr uf_ext xs e2 :
84 is_ctx_item uf_ext false (λ e1, X_SelectOr e1 xs e2)
85 | IsCtxItem_Incl uf_ext e2 :
86 is_ctx_item uf_ext false (λ e1, X_Incl e1 e2)
87 | IsCtxItem_ApplyL uf_ext e2 :
88 is_ctx_item uf_ext false (λ e1, X_Apply e1 e2)
89 | IsCtxItem_ApplyAttrsetR uf_ext m e1 :
90 is_ctx_item uf_ext false (λ e2, X_Apply (V_AttrsetFn m e1) e2)
91 | IsCtxItem_CondL uf_ext e2 e3 :
92 is_ctx_item uf_ext false (λ e1, X_Cond e1 e2 e3)
93 | IsCtxItem_AssertL uf_ext e2 :
94 is_ctx_item uf_ext false (λ e1, X_Assert e1 e2)
95 | IsCtxItem_OpL uf_ext op e2 :
96 is_ctx_item uf_ext false (λ e1, X_Op op e1 e2)
97 | IsCtxItem_OpR uf_ext op v1 :
98 is_ctx_item uf_ext false (λ e2, X_Op op (X_V v1) e2)
99 | IsCtxItem_OpHasAttrL uf_ext x :
100 is_ctx_item uf_ext false (λ e, X_HasAttr e x)
101 | IsCtxItem_Force uf_ext :
102 is_ctx_item uf_ext true (λ e, X_Force e)
103 | IsCtxItem_ForceAttrset bs x :
104 is_ctx_item true true (λ e, X_V (V_Attrset (<[x := e]>bs))).
105
106Hint Constructors is_ctx_item : core.
107
108Inductive is_ctx : bool → bool → (expr → expr) → Prop :=
109 | IsCtx_Id uf : is_ctx uf uf id
110 | IsCtx_Compose E1 E2 uf_int uf_aux uf_ext :
111 is_ctx_item uf_ext uf_aux E1 →
112 is_ctx uf_aux uf_int E2 →
113 is_ctx uf_ext uf_int (E1 ∘ E2).
114
115Hint Constructors is_ctx : core.
116
117(* /--> This is required because the standard library definition of "-->"
118 | (in Coq.Classes.Morphisms, for `respectful`) defines that this operator
119 | uses right associativity. Our definition must match exactly, as Coq
120 | will give an error otherwise.
121 \-------------------------------------\
122 | | *)
123Reserved Infix "-->" (right associativity, at level 55).
124
125Variant step : expr → expr → Prop :=
126 E_Ctx e1 e2 E uf_int :
127 is_ctx false uf_int E →
128 e1 -->base e2 →
129 E e1 --> E e2
130where "e --> e'" := (step e e').
131
132Hint Constructors step : core.
133
134Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55).
135
136(** Theories for contexts *)
137
138Lemma is_ctx_once uf_ext uf_int E :
139 is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E.
140Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed.
141
142Lemma is_ctx_item_ext_imp E uf_int :
143 is_ctx_item false uf_int E → is_ctx_item true uf_int E.
144Proof. intros H. inv H; constructor. Qed.
145
146Lemma is_ctx_ext_imp E1 E2 uf_aux uf_int :
147 is_ctx_item false uf_aux E1 →
148 is_ctx uf_aux uf_int E2 →
149 is_ctx true uf_int (E1 ∘ E2).
150Proof.
151 intros H1 H2.
152 revert E1 H1.
153 induction H2; intros.
154 - inv H1; eapply IsCtx_Compose; constructor.
155 - eapply IsCtx_Compose.
156 + by apply is_ctx_item_ext_imp in H1.
157 + by eapply IsCtx_Compose.
158Qed.
159
160Lemma is_ctx_uf_false_impl_true E uf_int :
161 is_ctx false uf_int E →
162 is_ctx true uf_int E ∨ E = id.
163Proof.
164 intros Hctx. inv Hctx.
165 - by right.
166 - left. eapply is_ctx_ext_imp; [apply H | apply H0].
167Qed.