lang.v 16.7 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. *)
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 *)
37 38 39
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
40 41
  (* Base types and their operations *)
  | Lit (l : base_lit)
42 43 44
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
45
  (* Products *)
46 47 48
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
49
  (* Sums *)
50 51 52
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
53
  (* Concurrency *)
54
  | Fork (e : expr)
55
  (* Heap *)
56 57 58 59
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
60

61 62
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
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
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
95 96 97 98
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.
99

100
Inductive val :=
101
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
102
  | LitV (l : base_lit)
103 104
  | PairV (v1 v2 : val)
  | InjLV (v : val)
105
  | InjRV (v : val).
106

107 108
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
109 110 111
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
112

113
Fixpoint of_val (v : val) : expr :=
114
  match v with
115
  | RecV f x e _ => Rec f x e
116
  | LitV l => Lit l
117 118 119
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
120
  end.
121

122
Fixpoint to_val (e : expr) : option val :=
123
  match e with
124 125
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
126
  | Lit l => Some (LitV l)
127 128 129
  | 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
130
  | _ => None
131 132
  end.

133 134
(** The state: heaps of vals. *)
Definition state := gmap loc val.
135

136
(** Evaluation contexts *)
137
Inductive ectx_item :=
138
  | AppLCtx (e2 : expr)
139
  | AppRCtx (v1 : val)
140
  | UnOpCtx (op : un_op)
141
  | BinOpLCtx (op : bin_op) (e2 : expr)
142
  | BinOpRCtx (op : bin_op) (v1 : val)
143 144
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
145 146 147 148 149
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
150
  | CaseCtx (e1 : expr) (e2 : expr)
151 152
  | AllocCtx
  | LoadCtx
153
  | StoreLCtx (e2 : expr)
154
  | StoreRCtx (v1 : val)
155 156
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
157
  | CasRCtx (v0 : val) (v1 : val).
158

159
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
160 161 162
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
163 164 165 166
  | 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
167 168 169 170 171 172
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
173
  | CaseCtx e1 e2 => Case e e1 e2
174 175
  | AllocCtx => Alloc e
  | LoadCtx => Load e
176
  | StoreLCtx e2 => Store e e2 
177
  | StoreRCtx v1 => Store (of_val v1) e
178 179 180
  | 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
181 182
  end.

183
(** Substitution *)
184 185 186
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
187
  | Rec f y e =>
188 189
     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)
190
  | Lit l => Lit l
191 192 193 194 195 196 197 198 199 200 201 202 203 204
  | 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)
205
  end.
206

207
Definition subst' (mx : binder) (es : expr) : expr  expr :=
208
  match mx with BNamed x => subst x es | BAnon => id end.
209

210
(** The stepping relation *)
211 212
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
213
  | NegOp, LitBool b => Some (LitBool (negb b))
214
  | MinusUnOp, LitInt n => Some (LitInt (- n))
215 216 217 218 219
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
220 221 222 223 224
  | 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)
225 226 227
  | _, _, _ => None
  end.

228
Inductive head_step : expr  state  expr  state  option (expr)  Prop :=
229
  | BetaS f x e1 e2 v2 e' σ :
230
     to_val e2 = Some v2 
231
     Closed (f :b: x :b: []) e1 
232 233
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
234
  | UnOpS op l l' σ :
235 236
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
237
  | BinOpS op l1 l2 l' σ :
238 239 240
     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
241
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
242
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
243
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
244 245 246 247 248 249
  | 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
250
  | CaseLS e0 v0 e1 e2 σ :
251
     to_val e0 = Some v0 
252 253
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
254
     to_val e0 = Some v0 
255
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
256
  | ForkS e σ:
257
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
258 259
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
260
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
261 262
  | LoadS l v σ :
     σ !! l = Some v 
263
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
264 265
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
266
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
267 268 269
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
270
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
271 272 273
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
274
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
275

276
(** Atomic expressions *)
277
Definition atomic (e: expr) : bool :=
278
  match e with
279 280 281 282 283
  | 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
284
  (* Make "skip" atomic *)
285 286
  | App (Rec _ _ (Lit _)) (Lit _) => true
  | _ => false
287
  end.
288

289 290
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
291 292 293
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
294

295
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
296
Proof.
297
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
298
Qed.
299

300
Instance of_val_inj : Inj (=) (=) of_val.
301
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
302

303
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
304
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
305

306 307 308
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.
309

310
Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
311
Proof. destruct 1; naive_solver. Qed.
312

313
Lemma atomic_not_val e : atomic e  to_val e = None.
314
Proof. by destruct e. Qed.
315

316 317
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
318
  intros. destruct Ki; simplify_eq/=; destruct_and?;
319
    repeat (simpl || case_match || contradiction); eauto.
320 321
Qed.

322
Lemma atomic_step e1 σ1 e2 σ2 ef :
323
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
324
Proof.
325
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
326
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
327
Qed.
328

329
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
330
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
331
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
332

333
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
334
  to_val e1 = None  to_val e2 = None 
335
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
336
Proof.
337
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
338
    repeat match goal with
339 340
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
341
Qed.
342

343 344
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
345
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
346
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
347

348
(** Value type class *)
Robbert Krebbers's avatar
Robbert Krebbers committed
349 350 351 352 353
Class IntoValue (e : expr) (v : val) := into_value : to_val e = Some v.
Instance into_value_of_val v : IntoValue (of_val v) v.
Proof. by rewrite /IntoValue to_of_val. Qed.
Instance into_value_rec f x e `{!Closed (f :b: x :b: []) e} :
  IntoValue (Rec f x e) (RecV f x e).
354
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
  rewrite /IntoValue /=; case_decide; last done.
356 357
  do 2 f_equal. by apply (proof_irrel).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
Instance into_value_lit l : IntoValue (Lit l) (LitV l).
359
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
Instance into_value_pair e1 e2 v1 v2 :
  IntoValue e1 v1  IntoValue e2 v2  IntoValue (Pair e1 e2) (PairV v1 v2).
Proof. by rewrite /IntoValue /= => -> /= ->. Qed.
Instance into_value_injl e v : IntoValue e v  IntoValue (InjL e) (InjLV v).
Proof. by rewrite /IntoValue /= => ->. Qed.
Instance into_value_injr e v : IntoValue e v  IntoValue (InjR e) (InjRV v).
Proof. by rewrite /IntoValue /= => ->. Qed.

(** Closed expressions *)
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.

Instance of_val_closed X v : Closed X (of_val v).
Proof.
  apply is_closed_weaken with []; last set_solver.
  induction v; simpl; auto.
Qed.

Lemma closed_subst X e x es : Closed X e  x  X  subst x es e = e.
Proof.
  rewrite /Closed. revert X.
  induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
384

Robbert Krebbers's avatar
Robbert Krebbers committed
385 386
Lemma closed_nil_subst e x es : Closed [] e  subst x es e = e.
Proof. intros. apply closed_subst with []; set_solver. Qed.
387

Robbert Krebbers's avatar
Robbert Krebbers committed
388 389 390
Lemma closed_nil_closed X e : Closed [] e  Closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Hint Immediate closed_nil_closed : typeclass_instances.
391

Robbert Krebbers's avatar
Robbert Krebbers committed
392 393 394 395 396 397 398 399 400 401 402 403 404 405
Instance closed_of_val X v : Closed X (of_val v).
Proof. apply of_val_closed. Qed.
Instance closed_rec X f x e : Closed (f :b: x :b: X) e  Closed X (Rec f x e).
Proof. done. Qed.
Lemma closed_var X x : bool_decide (x  X)  Closed X (Var x).
Proof. done. Qed.
Hint Extern 1000 (Closed _ (Var _)) =>
  apply closed_var; vm_compute; exact I : typeclass_instances.

Section closed.
  Context (X : list string).
  Notation C := (Closed X).

  Global Instance closed_lit l : C (Lit l).
406
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
  Global Instance closed_unop op e : C e  C (UnOp op e).
408
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
409
  Global Instance closed_fst e : C e  C (Fst e).
410
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
  Global Instance closed_snd e : C e  C (Snd e).
412
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
  Global Instance closed_injl e : C e  C (InjL e).
414
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
  Global Instance closed_injr e : C e  C (InjR e).
416
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417
  Global Instance closed_fork e : C e  C (Fork e).
418
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
  Global Instance closed_load e : C e  C (Load e).
420
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
  Global Instance closed_alloc e : C e  C (Alloc e).
422
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
  Global Instance closed_app e1 e2 : C e1  C e2  C (App e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_binop op e1 e2 : C e1  C e2  C (BinOp op e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_pair e1 e2 : C e1  C e2  C (Pair e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_store e1 e2 : C e1  C e2  C (Store e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_if e0 e1 e2 : C e0  C e1  C e2  C (If e0 e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_case e0 e1 e2 : C e0  C e1  C e2  C (Case e0 e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
  Global Instance closed_cas e0 e1 e2 : C e0  C e1  C e2  C (CAS e0 e1 e2).
  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
End closed.
438

Ralf Jung's avatar
Ralf Jung committed
439
(** Equality and other typeclass stuff *)
440 441 442 443 444 445
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.
446 447
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
448
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
449
Proof.
450 451
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
452

453
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Ralf Jung's avatar
Ralf Jung committed
454
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
455 456 457

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
458
Canonical Structure exprC := leibnizC expr.
459 460 461
End heap_lang.

(** Language *)
462 463
Program Instance heap_ectxi_lang :
  EctxiLanguage
464
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
465
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
466
  fill_item := heap_lang.fill_item;
467 468
  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
469
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
470
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
471 472
  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
473

474
Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
475

476
(* Prefer heap_lang names over ectx_language names. *)
477
Export heap_lang.