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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
Require Import Coq.Strings.String.
From stdpp Require Import gmap.
From mininix Require Import binop expr matching relations.
Definition attrset := is_Some ∘ maybe V_Attrset.
Reserved Infix "-->base" (right associativity, at level 55).
Inductive base_step : expr → expr → Prop :=
| E_Force (sv : strong_value) :
X_Force sv -->base sv
| E_Closed e :
X_Closed e -->base e
| E_Placeholder x e :
X_Placeholder x e -->base e
| E_MSelect bs x ys :
X_Select (V_Attrset bs) (nonempty_cons x ys) -->base
X_Select (X_Select (V_Attrset bs) (nonempty_singleton x)) ys
| E_Select e bs x :
X_Select (V_Attrset (<[x := e]>bs)) (nonempty_singleton x) -->base e
| E_SelectOr bs x e :
X_SelectOr (V_Attrset bs) (nonempty_singleton x) e -->base
X_Cond (X_HasAttr (V_Attrset bs) x)
(* if true *)
(X_Select (V_Attrset bs) (nonempty_singleton x))
(* if false *)
e
| E_MSelectOr bs x ys e :
X_SelectOr (V_Attrset bs) (nonempty_cons x ys) e -->base
X_Cond (X_HasAttr (V_Attrset bs) x)
(* if true *)
(X_SelectOr
(X_Select (V_Attrset bs) (nonempty_singleton x))
ys e)
(* if false *)
e
| E_Rec bs :
X_Attrset bs -->base V_Attrset (rec_subst bs)
| E_Let e bs :
X_LetBinding bs e -->base subst (closed (rec_subst bs)) e
| E_With e bs :
X_Incl (V_Attrset bs) e -->base subst (placeholders bs) e
| E_WithNoAttrset v1 e2 :
¬ attrset v1 →
X_Incl v1 e2 -->base e2
| E_ApplySimple x e1 e2 :
X_Apply (V_Fn x e1) e2 -->base subst {[x := X_Closed e2]} e1
| E_ApplyAttrset m e bs bs' :
bs ~ m ~> bs' →
X_Apply (V_AttrsetFn m e) (V_Attrset bs) -->base
X_LetBinding bs' e
| E_ApplyFunctor e1 e2 bs :
X_Apply (V_Attrset (<["__functor" := e2]>bs)) e1 -->base
X_Apply (X_Apply e2 (V_Attrset (<["__functor" := e2]>bs))) e1
| E_IfTrue e2 e3 :
X_Cond true e2 e3 -->base e2
| E_IfFalse e2 e3 :
X_Cond false e2 e3 -->base e3
| E_Op op v1 v2 u :
v1 ⟦op⟧ v2 -⊚-> u →
X_Op op v1 v2 -->base u
| E_OpHasAttrTrue bs x :
is_Some (bs !! x) →
X_HasAttr (V_Attrset bs) x -->base true
| E_OpHasAttrFalse bs x :
bs !! x = None →
X_HasAttr (V_Attrset bs) x -->base false
| E_OpHasAttrNoAttrset v x :
¬ attrset v →
X_HasAttr v x -->base false
| E_Assert e2 :
X_Assert true e2 -->base e2
where "e -->base e'" := (base_step e e').
Notation "e '-->base*' e'" := (rtc base_step e e')
(right associativity, at level 55).
Hint Constructors base_step : core.
Variant is_ctx_item : bool → bool → (expr → expr) → Prop :=
| IsCtxItem_Select uf_ext xs :
is_ctx_item uf_ext false (λ e1, X_Select e1 xs)
| IsCtxItem_SelectOr uf_ext xs e2 :
is_ctx_item uf_ext false (λ e1, X_SelectOr e1 xs e2)
| IsCtxItem_Incl uf_ext e2 :
is_ctx_item uf_ext false (λ e1, X_Incl e1 e2)
| IsCtxItem_ApplyL uf_ext e2 :
is_ctx_item uf_ext false (λ e1, X_Apply e1 e2)
| IsCtxItem_ApplyAttrsetR uf_ext m e1 :
is_ctx_item uf_ext false (λ e2, X_Apply (V_AttrsetFn m e1) e2)
| IsCtxItem_CondL uf_ext e2 e3 :
is_ctx_item uf_ext false (λ e1, X_Cond e1 e2 e3)
| IsCtxItem_AssertL uf_ext e2 :
is_ctx_item uf_ext false (λ e1, X_Assert e1 e2)
| IsCtxItem_OpL uf_ext op e2 :
is_ctx_item uf_ext false (λ e1, X_Op op e1 e2)
| IsCtxItem_OpR uf_ext op v1 :
is_ctx_item uf_ext false (λ e2, X_Op op (X_V v1) e2)
| IsCtxItem_OpHasAttrL uf_ext x :
is_ctx_item uf_ext false (λ e, X_HasAttr e x)
| IsCtxItem_Force uf_ext :
is_ctx_item uf_ext true (λ e, X_Force e)
| IsCtxItem_ForceAttrset bs x :
is_ctx_item true true (λ e, X_V (V_Attrset (<[x := e]>bs))).
Hint Constructors is_ctx_item : core.
Inductive is_ctx : bool → bool → (expr → expr) → Prop :=
| IsCtx_Id uf : is_ctx uf uf id
| IsCtx_Compose E1 E2 uf_int uf_aux uf_ext :
is_ctx_item uf_ext uf_aux E1 →
is_ctx uf_aux uf_int E2 →
is_ctx uf_ext uf_int (E1 ∘ E2).
Hint Constructors is_ctx : core.
(* /--> This is required because the standard library definition of "-->"
| (in Coq.Classes.Morphisms, for `respectful`) defines that this operator
| uses right associativity. Our definition must match exactly, as Coq
| will give an error otherwise.
\-------------------------------------\
| | *)
Reserved Infix "-->" (right associativity, at level 55).
Variant step : expr → expr → Prop :=
E_Ctx e1 e2 E uf_int :
is_ctx false uf_int E →
e1 -->base e2 →
E e1 --> E e2
where "e --> e'" := (step e e').
Hint Constructors step : core.
Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55).
(** Theories for contexts *)
Lemma is_ctx_once uf_ext uf_int E :
is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E.
Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed.
Lemma is_ctx_item_ext_imp E uf_int :
is_ctx_item false uf_int E → is_ctx_item true uf_int E.
Proof. intros H. inv H; constructor. Qed.
Lemma is_ctx_ext_imp E1 E2 uf_aux uf_int :
is_ctx_item false uf_aux E1 →
is_ctx uf_aux uf_int E2 →
is_ctx true uf_int (E1 ∘ E2).
Proof.
intros H1 H2.
revert E1 H1.
induction H2; intros.
- inv H1; eapply IsCtx_Compose; constructor.
- eapply IsCtx_Compose.
+ by apply is_ctx_item_ext_imp in H1.
+ by eapply IsCtx_Compose.
Qed.
Lemma is_ctx_uf_false_impl_true E uf_int :
is_ctx false uf_int E →
is_ctx true uf_int E ∨ E = id.
Proof.
intros Hctx. inv Hctx.
- by right.
- left. eapply is_ctx_ext_imp; [apply H | apply H0].
Qed.
|
