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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
|
Require Import Coq.Strings.String.
From stdpp Require Import gmap.
(* The Nix Expression Language *)
(** Selected operators from Dolsta and Löh, 2008. Newer definitions at
https://nixos.org/manual/nix/stable/language/operators *)
Variant op : Type :=
| O_Eq (* = *)
| O_Lt (* < *)
| O_Plus (* + *)
| O_Min (* - *)
| O_Div (* / *)
| O_Upd. (* // *)
Hint Constructors op : core.
Variant nonempty A := Ne_Cons (head : A) (tail : list A).
Arguments Ne_Cons {A} _ _.
Hint Constructors nonempty : core.
Inductive expr : Type :=
| X_V (v : value) (* v *)
| X_Id (x : string) (* x *)
| X_Attrset (bs : gmap string b_rhs) (* { bᵣ* } *)
| X_LetBinding (bs : gmap string b_rhs) (e : expr) (* let bᵣ* in e *)
| X_Select (e : expr) (xs : nonempty string) (* e.xs *)
| X_SelectOr (e : expr) (xs : nonempty string) (or : expr) (* e.xs or e *)
| X_Apply (e1 e2 : expr) (* e1 e2 *)
| X_Cond (e1 e2 e3 : expr) (* if e1 then e2 else e3 *)
| X_Incl (e1 e2 : expr) (* with e1; e2 *)
| X_Assert (e1 e2 : expr) (* assert e1; e2 *)
| X_Op (op : op) (e1 e2 : expr) (* e1 <op> e2 *)
| X_HasAttr (e1 : expr) (x : string) (* e ? x *)
| X_Force (e : expr) (* force e *)
| X_Closed (e : expr) (* closed(e) *)
| X_Placeholder (x : string) (e : expr) (* placeholderₓ(e) *)
with b_rhs :=
| B_Rec (e : expr) (* := e *)
| B_Nonrec (e : expr) (* :=ᵣ e *)
with matcher :=
| M_Matcher (ms : gmap string m_rhs) (strict : bool)
with m_rhs :=
| M_Mandatory
| M_Optional (e : expr) (* ? e *)
with value :=
| V_Bool (p : bool) : value (* true | false *)
| V_Null : value (* null *)
| V_Int (n : Z) : value (* n *)
| V_Str (s : string) : value (* s *)
| V_Fn (x : string) (e : expr) : value (* x: e *)
| V_AttrsetFn (m : matcher) (e : expr) : value (* { m }: e *)
| V_Attrset (bs : gmap string expr) : value. (* { b* } *)
Hint Constructors expr : core.
Instance Maybe_X_Attrset : Maybe X_Attrset := λ e,
match e with
| X_Attrset bs => Some bs
| _ => None
end.
Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs,
match rhs with
| B_Nonrec e => Some e
| _ => None
end.
Instance Maybe_B_Rec : Maybe B_Rec := λ rhs,
match rhs with
| B_Rec e => Some e
| _ => None
end.
Lemma maybe_b_rhs_excl b :
is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b) → False.
Proof. intros [e2 Hnonrec] [e1 Hrec]. simplify_option_eq. Qed.
Lemma no_b_nonrec__b_rec b :
¬ is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b).
Proof.
destruct b; try by eauto.
simplify_eq/=. intros contra. apply is_Some_alt. eauto.
Qed.
Lemma no_b_rec__b_nonrec b :
¬ is_Some (maybe B_Rec b) → is_Some (maybe B_Nonrec b).
Proof.
destruct b; try by eauto.
simplify_eq/=. intros contra. apply is_Some_alt. eauto.
Qed.
Instance Maybe_V_Attrset : Maybe V_Attrset := λ e,
match e with
| V_Attrset bs => Some bs
| _ => None
end.
Instance Maybe_V_Bool : Maybe V_Bool := λ e,
match e with
| V_Bool p => Some p
| _ => None
end.
Global Instance B_Nonrec_inj : Inj (=) (=) B_Nonrec.
Proof. intros [] [] ?; by simplify_eq. Qed.
Definition matcher_keys (m : matcher) : gset string :=
match m with M_Matcher ms _ => dom ms end.
Definition matcher_map (f : expr → expr) (m : matcher) : matcher :=
let map_m_rhs := λ rhs,
match rhs with
| M_Optional e => M_Optional (f e)
| _ => rhs
end in
match m with
| M_Matcher ms strict => M_Matcher (map_m_rhs <$> ms) strict
end.
Local Definition map_delete_all {K V} `{Countable K}
(ks : gset K) (m : gmap K V) : gmap K V :=
set_fold (λ k m', map_delete k m') m ks.
Local Definition b_rhs_map (f g : expr → expr) (rhs : b_rhs) : b_rhs :=
match rhs with
| B_Rec e => B_Rec (f e)
| B_Nonrec e => B_Nonrec (g e)
end.
(* See Dolstra (2006), §4.3.3 and fig. 4.6 (p. 75, PDF: p. 83) *)
Fixpoint subst (subs : gmap string expr) (e : expr) : expr :=
let msubst subs' := b_rhs_map (subst subs') (subst subs) in
match e with
| X_V V_Null | X_V (V_Bool _) | X_V (V_Str _) | X_V (V_Int _) => e
| X_Id x | X_Placeholder x _ => default e (subs !! x)
| X_Attrset bs =>
let subs' := map_delete_all (dom bs) subs in
X_Attrset (msubst subs' <$> bs)
| X_V (V_Attrset bs) =>
X_V (V_Attrset (subst subs <$> bs))
| X_LetBinding bs e' =>
let subs' := map_delete_all (dom bs) subs in
X_LetBinding (msubst subs' <$> bs) (subst subs' e')
| X_Select e' x => X_Select (subst subs e') x
| X_SelectOr e' x or => X_SelectOr (subst subs e') x (subst subs or)
| X_V (V_Fn x e') =>
let subs' := map_delete x subs in
X_V (V_Fn x (subst subs' e'))
| X_V (V_AttrsetFn (M_Matcher ms _ as m) e') =>
let subs' := map_delete_all (matcher_keys m) subs in
X_V (V_AttrsetFn (matcher_map (subst subs') m) (subst subs' e'))
| X_Apply e1 e2 => X_Apply (subst subs e1) (subst subs e2)
| X_Cond e1 e2 e3 => X_Cond (subst subs e1) (subst subs e2) (subst subs e3)
| X_Incl e1 e2 => X_Incl (subst subs e1) (subst subs e2)
| X_Op op e1 e2 => X_Op op (subst subs e1) (subst subs e2)
| X_HasAttr e x => X_HasAttr (subst subs e) x
| X_Assert e1 e2 => X_Assert (subst subs e1) (subst subs e2)
| X_Closed e => X_Closed e
| X_Force e => X_Force (subst subs e)
end.
Definition closed (bs : gmap string expr) : gmap string expr :=
X_Closed <$> bs.
Definition placeholders (bs : gmap string expr) : gmap string expr :=
map_imap (λ (x : string) (e : expr), Some (X_Placeholder x e)) bs.
Definition nonempty_singleton {A} (a : A): nonempty A := Ne_Cons a nil.
Definition nonempty_cons {A} (a : A) (l : nonempty A) : nonempty A :=
match l with Ne_Cons head tail => Ne_Cons a (head :: tail) end.
Definition indirect (bs : gmap string b_rhs) : gmap string expr :=
map_imap (λ (x : string) (rhs : b_rhs),
Some (X_Select (X_Attrset bs) (nonempty_singleton x))) bs.
Definition rec_subst (bs : gmap string b_rhs) : gmap string expr :=
let subs := indirect bs
in (λ b, match b with
| B_Rec e => subst (closed subs) e
| B_Nonrec e => e
end) <$> bs.
Inductive strong_value : Type :=
| SV_Bool (b : bool)
| SV_Null
| SV_Int (n : Z)
| SV_Str (s : string)
| SV_Fn (x : string) (e : expr)
| SV_AttrsetFn (m : matcher) (e : expr)
| SV_Attrset (bs : gmap string strong_value).
Fixpoint value_from_strong_value (sv : strong_value) : value :=
match sv with
| SV_Null => V_Null
| SV_Bool b => V_Bool b
| SV_Int n => V_Int n
| SV_Str s => V_Str s
| SV_Fn x e => V_Fn x e
| SV_AttrsetFn m e => V_AttrsetFn m e
| SV_Attrset bs => V_Attrset (X_V ∘ value_from_strong_value <$> bs)
end.
Global Instance X_V_inj : Inj (=) (=) X_V.
Proof. intros [] [] ?; by simplify_eq. Qed.
Definition expr_from_strong_value : strong_value → expr :=
X_V ∘ value_from_strong_value.
(* Based on the fin_maps test from stdpp *)
Fixpoint sv_size (sv : strong_value) : nat :=
match sv with
| SV_Null | SV_Bool _ | SV_Int _ | SV_Str _
| SV_Fn _ _ | SV_AttrsetFn _ _ => 1
| SV_Attrset bs => S (map_fold (λ _ sv', plus (sv_size sv')) 0 bs)
end.
(* Based on the fin_maps test from stdpp *)
Lemma strong_value_ind' :
∀ P : strong_value → Prop,
P SV_Null →
(∀ b : bool, P (SV_Bool b)) →
(∀ n : Z, P (SV_Int n)) →
(∀ s : string, P (SV_Str s)) →
(∀ (x : string) (e : expr), P (SV_Fn x e)) →
(∀ (m : matcher) (e : expr), P (SV_AttrsetFn m e)) →
(∀ bs : gmap string strong_value,
map_Forall (λ i, P) bs → P (SV_Attrset bs)) →
∀ s : strong_value, P s.
Proof.
intros P PNull PBool PInt PStr PFn PAttrsetFn PAttrset sv.
remember (sv_size sv) as n eqn:Hn. revert sv Hn.
induction (lt_wf n) as [n _ IH]; intros [| | | | | | bs] ->; simpl in *; try done.
apply PAttrset. revert bs IH.
apply (map_fold_ind (λ r bs, (∀ n', n' < S r → _) → map_Forall (λ _, P) bs)).
- intros IH. apply map_Forall_empty.
- intros k sv bs r ? IHbs IHsv. apply map_Forall_insert; [done|]. split.
+ eapply IHsv; [|done]; lia.
+ eapply IHbs. intros; eapply IHsv; [|done]; lia.
Qed.
Coercion X_Id : string >-> expr.
Coercion V_Int : Z >-> value.
(* Leaving this out for now: would conflict with X_Id and
therefore cause ambiguity *)
(* Coercion X_StrVal : string >-> expr. *)
Coercion V_Bool : bool >-> value.
Coercion X_V : value >-> expr.
Coercion value_from_strong_value : strong_value >-> value.
|
