lang.v 17.1 KB
Newer Older
1
From iris.program_logic Require Export ectx_language ectxi_language.
2
From iris.algebra Require Export cofe.
3
4
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
5

6
Module heap_lang.
7
8
Open Scope Z_scope.

9
(** Expressions and vals. *)
10
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
11

12
Inductive base_lit : Set :=
13
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
14
Inductive un_op : Set :=
15
  | NegOp | MinusUnOp.
16
17
18
Inductive bin_op : Set :=
  | PlusOp | MinusOp | LeOp | LtOp | EqOp.

19
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
20
21
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
22
23
24
25
26
27
28
29
30
31
32
33
34
Definition cons_binder (mx : binder) (X : list string) : list string :=
  match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x  X) P  SetUnfold (x  mx :b: X) (BNamed x = mx  P).
Proof.
  constructor. rewrite -(set_unfold (x  X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.

35
Inductive expr :=
36
  (* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
37
38
39
40
41
42
43
      (* Var is the only place where the terms contain a proof. The fact that they
       contain a proof at all is suboptimal, since this means two seeminlgy
       convertible terms could differ in their proofs. However, this also has
       some advantages:
       * We can make the [X] an index, so we can do non-dependent match.
       * In expr_weaken, we can push the proof all the way into Var, making
         sure that proofs never block computation. *)
44
45
46
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
47
48
  (* Base types and their operations *)
  | Lit (l : base_lit)
49
50
51
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
52
  (* Products *)
53
54
55
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
56
  (* Sums *)
57
58
59
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
60
  (* Concurrency *)
61
  | Fork (e : expr)
62
  (* Heap *)
63
64
65
66
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
67

68
69
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
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
Arguments Rec _ _ _%E.
Arguments App _%E _%E.
Arguments Lit _.
Arguments UnOp _ _%E.
Arguments BinOp _ _%E _%E.
Arguments If _%E _%E _%E.
Arguments Pair _%E _%E.
Arguments Fst _%E.
Arguments Snd _%E.
Arguments InjL _%E.
Arguments InjR _%E.
Arguments Case _%E _%E _%E.
Arguments Fork _%E.
Arguments Alloc _%E.
Arguments Load _%E.
Arguments Store _%E _%E.
Arguments CAS _%E _%E _%E.

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Section closed.
  Set Typeclasses Unique Instances.
  Class Closed (X : list string) (e : expr) := closed : is_closed X e.
End closed.

Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
110

111
Inductive val :=
112
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
113
  | LitV (l : base_lit)
114
115
  | PairV (v1 v2 : val)
  | InjLV (v : val)
116
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
117

118
119
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
120
121
122
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
123

124
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
125
  match v with
126
  | RecV f x e _ => Rec f x e
127
  | LitV l => Lit l
128
129
130
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
Ralf Jung's avatar
Ralf Jung committed
131
  end.
132

133
Fixpoint to_val (e : expr) : option val :=
134
  match e with
135
136
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
137
  | Lit l => Some (LitV l)
138
139
140
  | Pair e1 e2 => v1  to_val e1; v2  to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
Ralf Jung's avatar
Ralf Jung committed
141
  | _ => None
142
143
  end.

144
145
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
146

147
(** Evaluation contexts *)
148
Inductive ectx_item :=
149
  | AppLCtx (e2 : expr)
150
  | AppRCtx (v1 : val)
151
  | UnOpCtx (op : un_op)
152
  | BinOpLCtx (op : bin_op) (e2 : expr)
153
  | BinOpRCtx (op : bin_op) (v1 : val)
154
155
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
156
157
158
159
160
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
161
  | CaseCtx (e1 : expr) (e2 : expr)
162
163
  | AllocCtx
  | LoadCtx
164
  | StoreLCtx (e2 : expr)
165
  | StoreRCtx (v1 : val)
166
167
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
168
  | CasRCtx (v0 : val) (v1 : val).
169

170
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
171
172
173
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
174
175
176
177
  | UnOpCtx op => UnOp op e
  | BinOpLCtx op e2 => BinOp op e e2
  | BinOpRCtx op v1 => BinOp op (of_val v1) e
  | IfCtx e1 e2 => If e e1 e2
178
179
180
181
182
183
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
184
  | CaseCtx e1 e2 => Case e e1 e2
185
186
  | AllocCtx => Alloc e
  | LoadCtx => Load e
187
  | StoreLCtx e2 => Store e e2 
188
  | StoreRCtx v1 => Store (of_val v1) e
189
190
191
  | CasLCtx e1 e2 => CAS e e1 e2
  | CasMCtx v0 e2 => CAS (of_val v0) e e2
  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
192
193
  end.

194
(** Substitution *)
195
196
197
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
198
  | Rec f y e =>
199
200
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
201
  | Lit l => Lit l
202
203
204
205
206
207
208
209
210
211
212
213
214
215
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
216
  end.
217

218
Definition subst' (mx : binder) (es : expr) : expr  expr :=
219
  match mx with BNamed x => subst x es | BAnon => id end.
220

221
(** The stepping relation *)
222
223
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
224
  | NegOp, LitBool b => Some (LitBool (negb b))
225
  | MinusUnOp, LitInt n => Some (LitInt (- n))
226
227
228
229
230
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
231
232
233
234
235
  | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
  | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
  | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)
  | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
236
237
238
  | _, _, _ => None
  end.

239
Inductive head_step : expr  state  expr  state  option (expr)  Prop :=
240
  | BetaS f x e1 e2 v2 e' σ :
241
     to_val e2 = Some v2 
242
     Closed (f :b: x :b: []) e1 
243
244
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
245
  | UnOpS op l l' σ :
246
247
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
248
  | BinOpS op l1 l2 l' σ :
249
250
251
     bin_op_eval op l1 l2 = Some l'  
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
  | IfTrueS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
252
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
253
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
254
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
255
256
257
258
259
260
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Fst (Pair e1 e2)) σ e1 σ None
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Snd (Pair e1 e2)) σ e2 σ None
261
  | CaseLS e0 v0 e1 e2 σ :
262
     to_val e0 = Some v0 
263
264
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
265
     to_val e0 = Some v0 
266
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
267
  | ForkS e σ:
268
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
269
270
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
271
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
272
273
  | LoadS l v σ :
     σ !! l = Some v 
274
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
275
276
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
277
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
278
279
280
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
281
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
282
283
284
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
285
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
286

287
(** Atomic expressions *)
288
Definition atomic (e: expr) : bool :=
289
  match e with
290
291
292
293
294
  | Alloc e => bool_decide (is_Some (to_val e))
  | Load e => bool_decide (is_Some (to_val e))
  | Store e1 e2 => bool_decide (is_Some (to_val e1)  is_Some (to_val e2))
  | CAS e0 e1 e2 =>
    bool_decide (is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2))
Ralf Jung's avatar
Ralf Jung committed
295
  (* Make "skip" atomic *)
296
297
  | App (Rec _ _ (Lit _)) (Lit _) => true
  | _ => false
298
  end.
299

300
(** Substitution *)
301
302
Lemma is_closed_weaken X Y e : is_closed X e  X `included` Y  is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
303

304
Instance of_val_closed X v : Closed X (of_val v).
305
Proof.
306
307
  apply is_closed_weaken with []; last set_solver.
  induction v; simpl; auto.
308
309
Qed.

310
Lemma closed_subst X e x es : Closed X e  x  X  subst x es e = e.
311
Proof.
312
313
314
  rewrite /Closed. revert X.
  induction e; intros; simpl; try case_decide; f_equal/=; try naive_solver.
 naive_solver (eauto; set_solver).
315
316
Qed.

317
318
Lemma closed_nil_subst e x es : Closed [] e  subst x es e = e.
Proof. intros. apply closed_subst with []; set_solver. Qed.
319

320
321
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
322
323
324
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
325

326
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
327
Proof.
328
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
329
Qed.
330

331
Instance of_val_inj : Inj (=) (=) of_val.
332
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
333

334
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
335
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
336

337
338
339
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
340

341
Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
342
Proof. destruct 1; naive_solver. Qed.
343

344
Lemma atomic_not_val e : atomic e  to_val e = None.
345
Proof. by destruct e. Qed.
346

347
348
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
349
  intros. destruct Ki; simplify_eq/=; destruct_and?;
350
    repeat (simpl || case_match || contradiction); eauto.
351
352
Qed.

353
Lemma atomic_step e1 σ1 e2 σ2 ef :
354
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
355
Proof.
356
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
357
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
358
Qed.
359

360
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
361
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
362
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
363

364
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
365
  to_val e1 = None  to_val e2 = None 
366
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
367
Proof.
368
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
369
    repeat match goal with
370
371
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
372
Qed.
373

374
375
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
376
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
377
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
378

379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
(** Value type class *)
Class Value (e : expr) (v : val) := is_value : to_val e = Some v.
Instance of_val_value v : Value (of_val v) v.
Proof. by rewrite /Value to_of_val. Qed.
Instance rec_value f x e `{!Closed (f :b: x :b: []) e} :
  Value (Rec f x e) (RecV f x e).
Proof.
  rewrite /Value /=; case_decide; last done.
  do 2 f_equal. by apply (proof_irrel).
Qed.
Instance lit_value l : Value (Lit l) (LitV l).
Proof. done. Qed.
Instance pair_value e1 e2 v1 v2 :
  Value e1 v1  Value e2 v2  Value (Pair e1 e2) (PairV v1 v2).
Proof. by rewrite /Value /= => -> /= ->. Qed.
Instance injl_value e v : Value e v  Value (InjL e) (InjLV v).
Proof. by rewrite /Value /= => ->. Qed.
Instance injr_value e v : Value e v  Value (InjR e) (InjRV v).
Proof. by rewrite /Value /= => ->. Qed.

Section closed_slow.
  Notation C := Closed.

  Global Instance closed_of_val X v : C X (of_val v).
  Proof. apply of_val_closed. Qed.

  Lemma closed_var X x : bool_decide (x  X)  C X (Var x).
  Proof. done. Qed.
  Global Instance closed_lit X l : C X (Lit l).
  Proof. done. Qed.
  Global Instance closed_rec X f x e : C (f :b: x :b: X) e  C X (Rec f x e).
  Proof. done. Qed.
  Global Instance closed_unop X op e : C X e  C X (UnOp op e).
  Proof. done. Qed.
  Global Instance closed_fst X e : C X e  C X (Fst e).
  Proof. done. Qed.
  Global Instance closed_snd X e : C X e  C X (Snd e).
  Proof. done. Qed.
  Global Instance closed_injl X e : C X e  C X (InjL e).
  Proof. done. Qed.
  Global Instance closed_injr X e : C X e  C X (InjR e).
  Proof. done. Qed.
  Global Instance closed_fork X e : C X e  C X (Fork e).
  Proof. done. Qed.
  Global Instance closed_load X e : C X e  C X (Load e).
  Proof. done. Qed.
  Global Instance closed_alloc X e : C X e  C X (Alloc e).
  Proof. done. Qed.
  Global Instance closed_app X e1 e2 : C X e1  C X e2  C X (App e1 e2).
  Proof. intros. by apply andb_True. Qed.
  Global Instance closed_binop X op e1 e2 : C X e1  C X e2  C X (BinOp op e1 e2).
  Proof. intros. by apply andb_True. Qed.
  Global Instance closed_pair X e1 e2 : C X e1  C X e2  C X (Pair e1 e2).
  Proof. intros. by apply andb_True. Qed.
  Global Instance closed_store X e1 e2 : C X e1  C X e2  C X (Store e1 e2).
  Proof. intros. by apply andb_True. Qed.
  Global Instance closed_if X e0 e1 e2 : C X e0  C X e1  C X e2  C X (If e0 e1 e2).
  Proof. intros. by rewrite /C /= !andb_True. Qed.
  Global Instance closed_case X e0 e1 e2 : C X e0  C X e1  C X e2  C X (Case e0 e1 e2).
  Proof. intros. by rewrite /C /= !andb_True. Qed.
  Global Instance closed_cas X e0 e1 e2 : C X e0  C X e1  C X e2  C X (CAS e0 e1 e2).
  Proof. intros. by rewrite /C /= !andb_True. Qed.
End closed_slow.

Lemma closed_nil_closed X e : Closed [] e  Closed X e.
Proof. intros. apply is_closed_weaken with []. done. set_solver. Qed.
Hint Immediate closed_nil_closed : typeclass_instances.

Hint Extern 1000 (Closed _ (Var _)) =>
  apply closed_var; vm_compute; exact I : typeclass_instances.

Ralf Jung's avatar
Ralf Jung committed
450
(** Equality and other typeclass stuff *)
451
452
453
454
455
456
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
457
458
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
459
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
460
Proof.
461
462
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
463

464
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Ralf Jung's avatar
Ralf Jung committed
465
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
466
467
468

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
469
Canonical Structure exprC := leibnizC expr.
470
471
472
End heap_lang.

(** Language *)
473
474
Program Instance heap_ectxi_lang :
  EctxiLanguage
475
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
476
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
477
  fill_item := heap_lang.fill_item;
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479
  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
480
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
481
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
482
483
  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
484

485
Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
486

487
(* Prefer heap_lang names over ectx_language names. *)
488
Export heap_lang.