dcexpr.v 16.2 KB
Newer Older
1
2
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
3
From iris_c.c_translation Require Export translation proofmode.
4

5
Definition known_locs := list cloc.
6

Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
Inductive dloc :=
  | dLoc : nat  dloc
9
  | dLocUnknown : cloc  dloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
13

Global Instance dloc_decision : EqDecision dloc.
Proof. solve_decision. Defined.

14
15
(* This data type is kind of redundant, as long as we don't have symbolic
Booleans and integers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
24
25
26
Inductive dbase_lit : Type :=
  | dLitInt : Z  dbase_lit
  | dLitBool : bool  dbase_lit
  | dLitUnit : dbase_lit
  | dLitUnknown : base_lit  dbase_lit.

Global Instance dlit_decision : EqDecision dbase_lit.
Proof. solve_decision. Defined.

Inductive dval : Type :=
  | dLitV : dbase_lit  dval
27
  | dPairV : dval  dval  dval
28
  | dLocV : dloc  dval
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  | dValUnknown : val  dval.

Global Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.

Inductive doption (A : Type) : Type :=
  | dNone : doption A
  | dSome : A  doption A
  | dUnknown : option A  doption A.

Arguments dNone {_}.
Arguments dSome {_} _.
Arguments dUnknown {_} _.

Global Instance doption_fmap : FMap doption := λ A B f m,
  match m with
  | dNone => dNone
  | dSome x => dSome (f x)
  | dUnknown o => dUnknown (f <$> o)
  end.

50
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  match dl with
52
  | dLoc i => default inhabitant (E !! i)
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
  | dLocUnknown l => l
  end.

56
Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
62
63
  match l with
  | dLitInt x => LitInt x
  | dLitBool b => LitBool b
  | dLitUnit => LitUnit
  | dLitUnknown l => l
  end.

64
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
  match v with
  | dLitV l => LitV (dbase_lit_interp E l)
67
  | dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
68
  | dLocV dl => cloc_to_val (dloc_interp E dl)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  | dValUnknown v => v
  end.

Fixpoint doption_interp {A} (mx : doption A) : option A :=
  match mx with
  | dNone => None
  | dSome x => Some x
  | dUnknown mx => mx
  end.

Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
  match op with
  | PlusOp => dLitInt (n1 + n2)
  | MinusOp => dLitInt (n1 - n2)
  | MultOp => dLitInt (n1 * n2)
  | QuotOp => dLitInt (n1 `quot` n2)
  | RemOp => dLitInt (n1 `rem` n2)
  | AndOp => dLitInt (Z.land n1 n2)
  | OrOp => dLitInt (Z.lor n1 n2)
  | XorOp => dLitInt (Z.lxor n1 n2)
  | ShiftLOp => dLitInt (n1  n2)
  | ShiftROp => dLitInt (n1  n2)
  | LeOp => dLitBool (bool_decide (n1  n2))
  | LtOp => dLitBool (bool_decide (n1 < n2))
  | EqOp => dLitBool (bool_decide (n1 = n2))
  end.

Lemma dbin_op_eval_int_correct E op n1 n2 :
  bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
Proof. by destruct op. Qed.

Definition dbin_op_eval_bool
    (op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
  | AndOp => dSome (dLitBool (b1 && b2))
  | OrOp => dSome (dLitBool (b1 || b2))
  | XorOp => dSome (dLitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => dNone (* Shifts *)
  | LeOp | LtOp => dNone (* InEquality *)
  | EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
  end.

Lemma dbin_op_eval_bool_correct E op b1 b2 w :
  dbin_op_eval_bool op b1 b2 = dSome w 
  bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
Proof. destruct op; simpl; try by inversion 1. Qed.

Definition dbin_op_eval
118
           (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  match dv1,dv2 with
120
  | dPairV _ _, _ | _, dPairV _ _ => dNone
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
  | dValUnknown _, _ | _,dValUnknown _ =>
     dUnknown
      (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
  | dLitV l1, dLitV l2 =>
    if decide (op = EqOp)
    then dSome $ dLitV $ dLitBool
               $ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
    else match l1, l2 with
         | (dLitInt n1), (dLitInt n2) =>
           dSome $ dLitV $ dbin_op_eval_int op n1 n2
         | (dLitBool b1), (dLitBool b2) =>
           dLitV <$> dbin_op_eval_bool op b1 b2
         | dLitUnknown _, _ | _, dLitUnknown _ =>
             dUnknown (dValUnknown <$>
                bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
         | _, _ => dNone
         end
138
  | _, _ => dNone
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
141
142
143
144
145
  end.

Lemma dbin_op_eval_correct E op dv1 dv2 w :
  doption_interp (dbin_op_eval E op dv1 dv2) = Some w 
  bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
  Some (dval_interp E w).
Proof.
Dan Frumin's avatar
Dan Frumin committed
146
147
  destruct dv1 as [dl1 | |v1|]=> //.
  - destruct dv2 as [dl2 | |v2|]=> //.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
152
153
    + unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
      { inversion 1. rewrite /bin_op_eval /=.  f_equal. simplify_eq /=.
         do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
      { rewrite /bin_op_eval; intros; destruct dl1, dl2;
          rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
            try (destruct op; done); simpl.
154
155
        - rewrite /bin_op_eval in H0; case_decide; first done.
          destruct b; simplify_eq /=; f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
        - destruct op; simplify_eq /=; try done.
157
158
159
160
        - case_decide; first done. destruct b0; simplify_eq /=; f_equal.
          destruct op; simplify_eq /=; try done.
        - case_decide; first done. destruct b; simplify_eq /=; f_equal.
        - case_decide; first done; destruct b; simplify_eq /=; f_equal;
Robbert Krebbers's avatar
Robbert Krebbers committed
161
            destruct op; simplify_eq /=; try done.
162
163
164
165
        - case_decide; first done; destruct b; simplify_eq /=; f_equal.
        - case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
            destruct op; simplify_eq /=; try done. }
    + simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) _);
166
        try by inversion 1.
167
168
169
  - simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
      try by inversion 1.
  - simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
      try by inversion 1.
Qed.

173
174
Definition dun_op_eval
     (E : known_locs) (op : un_op) (dv : dval) : doption dval :=
175
  match dv with
176
  | dPairV _ _ => dNone
177
178
179
180
181
182
  | dValUnknown _ => dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
  | dLitV dl =>
    match op, dl with
    | NegOp, dLitBool b => dSome $ dLitV $ dLitBool (negb b)
    | NegOp, dLitInt n => dSome $ dLitV $ dLitInt (Z.lnot n)
    | MinusUnOp, dLitInt n => dSome $ dLitV $ dLitInt (- n)
183
184
    | _, dLitUnknown l =>
      dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
185
186
    | _,_ => dNone
    end
187
  | dLocV _ => dNone
188
189
190
191
192
193
  end.

Lemma dun_op_eval_correct E op dv w :
  doption_interp (dun_op_eval E op dv) = Some w 
  un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
Dan Frumin's avatar
Dan Frumin committed
194
  destruct dv as [dl | |v|]=> //=; last first.
195
196
197
198
199
200
201
202
  - destruct (un_op_eval op v); simpl; by inversion 1.
  - destruct op.
    + destruct dl; simpl; try by inversion 1.
      destruct b; by inversion 1.
    + destruct dl; simpl; try by inversion 1.
      destruct b; by inversion 1.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
(** DCexpr *)
Inductive dcexpr : Type :=
205
206
207
208
209
  | dCRet  : dval  dcexpr
  | dCAlloc : dcexpr  dcexpr
  | dCLoad : dcexpr  dcexpr
  | dCStore : dcexpr  dcexpr  dcexpr
  | dCBinOp : bin_op  dcexpr  dcexpr  dcexpr
Dan Frumin's avatar
Dan Frumin committed
210
  | dCPreBinOp : bin_op  dcexpr  dcexpr  dcexpr
211
  | dCUnOp : un_op  dcexpr  dcexpr
212
  | dCSeq : dcexpr  dcexpr  dcexpr
213
  | dCPar : dcexpr  dcexpr  dcexpr
214
  | dCInvoke  (f: val) (de: dcexpr)
215
  | dCUnknown (e : expr) `{!Closed [] e}.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
220
221
222
223
  match de with
  | dCRet dv => a_ret (dval_interp E dv)
  | dCAlloc de1 => a_alloc (dcexpr_interp E de1)
  | dCLoad de1 => a_load (dcexpr_interp E de1)
  | dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
  | dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
224
225
  | dCPreBinOp op de1 de2 =>
    a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
226
  | dCUnOp op de => a_un_op op (dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  | dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
228
  | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
229
  | dCInvoke fv de => call (fv, dcexpr_interp E de)
Robbert Krebbers's avatar
Robbert Krebbers committed
230
231
232
  | dCUnknown e1 => e1
  end.

233
234
(** Well-foundness of dcexpr w.r.t. known_locs *)

235
Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
236
  match dv with
237
  | dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
238
  | dLocV (dLoc i) => bool_decide (is_Some (E !! i))
239
240
241
242
243
244
  | _  => true
  end.

Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
  match de with
  | dCRet dv => dval_wf E dv
245
246
247
  | dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
  | dCStore de1 de2 | dCBinOp _ de1 de2
  | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
248
249
250
251
252
253
254
255
      dcexpr_wf E de1 && dcexpr_wf E de2
  | dCUnknown _ => true
  end.

(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
  dval_wf E dv  E `prefix_of` E'  dval_wf E' dv.
Proof.
256
  induction dv as [d| | |]; try naive_solver.
257
258
259
  destruct d as [i|]; last done; simplify_eq /=.
  intros Hb Hpre. case_bool_decide; last done.
  clear Hb. generalize dependent E. revert E'. induction i as [| i].
260
261
262
263
264
265
  + intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
    destruct E'. by apply prefix_nil_not in Hpre. naive_solver.
  + intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H.
    * by apply prefix_nil_not in Hpre.
    * by apply is_Some_None in H.
    * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
266
267
268
269
270
Qed.

Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
  dcexpr_wf E de  E `prefix_of` E'  dcexpr_wf E' de.
Proof.
Dan Frumin's avatar
Dan Frumin committed
271
  induction de; simplify_eq /=; try eauto; [ apply dval_wf_mono | | | | |];
272
  naive_solver.
273
274
Qed.

275
276
277

Lemma dun_op_eval_dSome_wf E dv u dw:
  dval_wf E dv  dun_op_eval E u dv = dSome dw  dval_wf E dw.
278
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
279
280
281

Lemma dun_op_eval_dUnknown_wf E dv u w:
  dval_wf E dv  dun_op_eval E u dv =  dUnknown (Some w)  dval_wf E w.
282
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
283
284
285
286

Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
  dval_wf E dv1  dval_wf E dv2 
  dbin_op_eval E op dv1 dv2 = dSome dw  dval_wf E dw.
287
Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
288
289
290

(** / Well-foundness of dcexpr w.r.t. known_locs *)

291
292
293
Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
  dval_wf E dv  E `prefix_of` E'  dval_interp E dv = dval_interp E' dv.
Proof.
Dan Frumin's avatar
Dan Frumin committed
294
295
  induction dv as [d|?|?|?]=>//.
  { simpl. intros. f_equal; naive_solver. }
296
297
298
  destruct d as [i|]; last done; simplify_eq /=.
  intros Hb Hpre. case_bool_decide; last done.
  clear Hb. generalize dependent E. revert E'. induction i as [| i].
299
  + intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
300
    destruct E'. by apply prefix_nil_not in Hpre.
301
302
303
304
305
    by apply prefix_cons_inv_1 in Hpre; subst.
  + intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H.
    * by apply prefix_nil_not in Hpre.
    * by apply is_Some_None in H.
    * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
306
307
308
309
310
311
312
313
314
315
316
317
318
Qed.

Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
   dcexpr_wf E de  E `prefix_of` E'  dcexpr_interp E de = dcexpr_interp E' de.
Proof.
  induction de; simplify_eq /=; intros H Hpre;
    try (by rewrite IHde ) ||
        (apply andb_prop_elim in H as [H1 H2];
         rewrite IHde2; [rewrite IHde1; done | done | done ];
           by rewrite (IHde1 H1 Hpre  (dcexpr_interp E de1))) || eauto.
  do 2 f_equal. by apply dval_interp_mono.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
321
Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
Proof. induction de; simpl; solve_closed. Qed.

322
323
(** * Reification of C syntax *)
(** ** LocLookup *)
324
Class LocLookup (E : known_locs) (l : cloc) (i : nat) :=
325
326
327
328
329
330
331
332
333
  loc_lookup : E !! i = Some l.

Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
Proof. done. Qed.

Global Instance loc_lookup_there l l' E i :
  LocLookup E l i  LocLookup (l' :: E) l (S i).
Proof. done. Qed.

334
335
336
(** ** IntoDBaseLit *)
Class IntoDBaseLit (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
  into_dbase_lit : l = dbase_lit_interp E dl.
337

338
339
Global Instance into_dbase_lit_int E i :
  IntoDBaseLit E (LitInt i) (dLitInt i).
340
341
Proof. split; eauto. Qed.

342
343
Global Instance into_dbase_lit_default E l :
  IntoDBaseLit E l (dLitUnknown l) | 1000.
344
345
346
347
348
349
350
Proof. split; eauto. Qed.

(** ** ExprIntoDVal *)
Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
  { expr_into_dval : e = of_val (dval_interp E dv);
    expr_into_dval_wf : dval_wf E dv }.

351
352
353
354
355
356
357
358
359
360
361
Global Instance expr_into_dval_lit E l dl :
  IntoDBaseLit E l dl  ExprIntoDVal E (Lit l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

Global Instance expr_into_dval_loc E l i :
  LocLookup E l i  ExprIntoDVal E (cloc_to_val l) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.

Global Instance expr_into_dval_loc_unknown E l :
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
362

363
(* TODO: use ValToNat for those two instance below *)
364
365
366
367
368
369
370
Global Instance expr_into_dval_cloc_pos E (l : loc) (o : positive) i :
  LocLookup E (l,Pos.to_nat o) i  ExprIntoDVal E (#l,#(Zpos o)) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi -?positive_nat_Z //. Qed.

Global Instance expr_into_dval_cloc_zero E (l : loc) i :
  LocLookup E (l,0%nat) i  ExprIntoDVal E (#l,#0) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.
371
372
373
374
375
376
377
378
379
380

Global Instance expr_into_dval_default E e v :
  IntoVal e v  ExprIntoDVal E e (dValUnknown v) | 1000.
Proof. done. Qed.

(** ** IntoDVal *)
Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
  { into_dval : v = dval_interp E dv;
    into_dval_wf : dval_wf E dv }.

381
382
383
384
385
386
387
388
389
390
391
Global Instance into_dval_lit E l dl :
  IntoDBaseLit E l dl  IntoDVal E (LitV l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.

Global Instance into_dval_loc E l i :
  LocLookup E l i  IntoDVal E (cloc_to_val l) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi //. Qed.

Global Instance into_dval_loc_unknown E l :
  ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
392
393
394
395
396

Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed.

(** ** IntoDCexpr *)
397
Class IntoDCexpr (E: known_locs) (e: expr) (de: dcexpr) :=
398
399
  { into_dcexpr : e = dcexpr_interp E de;
    into_dcexpr_wf : dcexpr_wf E de }.
Robbert Krebbers's avatar
Robbert Krebbers committed
400
401

Global Instance into_dcexpr_ret E v dv:
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  ExprIntoDVal E v dv 
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  IntoDCexpr E (a_ret v) (dCRet dv).
404
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
406
407
408

Global Instance into_dcexpr_alloc E e de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_alloc e) (dCAlloc de).
409
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
411
412
413

Global Instance into_dcexpr_load E e de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_load e) (dCLoad de).
414
Proof. intros [-> ?]; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416
417
418
419

Global Instance into_dcexpr_store E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
420
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
424
425

Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
426
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
427

Dan Frumin's avatar
Dan Frumin committed
428
429
430
431
432
433
Global Instance into_dcexpr_prebinop E e1 e2 op de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (a_pre_bin_op op e1 e2) (dCPreBinOp op de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.

434
435
436
Global Instance into_dcexpr_unop E e op de:
  IntoDCexpr E e de 
  IntoDCexpr E (a_un_op op e) (dCUnOp op de).
437
Proof. intros [-> ?]; split; auto. Qed.
438

Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
441
Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
Robbert Krebbers's avatar
Robbert Krebbers committed
442
  IntoDCexpr E (e1 ; e2) (dCSeq de1 de2).
443
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
444

445
446
447
448
449
450
Global Instance into_dcexpr_par E e1 e2 de1 de2:
  IntoDCexpr E e1 de1 
  IntoDCexpr E e2 de2 
  IntoDCexpr E (e1 ||| e2) (dCPar de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.

451
452
Global Instance into_dcexpr_invoke E `{Closed [] e1} ef f `{!IntoVal ef f} de1 :
  IntoDCexpr E e1 de1 
453
  IntoDCexpr E (call (ef, e1)) (dCInvoke f de1).
454
455
456
457
458
Proof.
  intros. unfold IntoVal in *. simplify_eq /=.
  split; simpl; auto; f_equal; by inversion H0.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
459
460
Global Instance into_dcexpr_unknown E e `{Closed [] e}:
  IntoDCexpr E e (dCUnknown e) | 100.
461
Proof. done. Qed.