lang.v 17.7 KB
Newer Older
1 2
From iris.algebra Require Import ofe.
From iris.program_logic Require Export language.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.program_logic Require Export ectx_language ectxi_language.
Dan Frumin's avatar
Dan Frumin committed
4
From iris_logrel.prelude Require Export base.
5
From iris_logrel.F_mu_ref_conc Require Export binder.
6

7
Module lang.
8
  (** * Syntax and syntactic categories *)
9 10
  Definition loc := positive.

11
  Instance loc_dec_eq : EqDecision loc := _.
12

Dan Frumin's avatar
Dan Frumin committed
13
  (** ** Expressions *)
Dan Frumin's avatar
Dan Frumin committed
14 15
  Inductive binop := Add | Sub | Eq | Le | Lt | Xor.
  
16
  Instance binop_dec_eq : EqDecision binop.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  Proof. solve_decision. Defined.
18

19 20
  Inductive literal := Unit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc).

21
  Inductive expr :=
22
  | Var (x : string)
23
  (* λ-rec *)
24
  | Rec (f x : binder) (e : expr)
25
  | App (e1 e2 : expr)
26
  (* Constants *)
27
  | Lit (l : literal)
28
  | BinOp (op : binop) (e1 e2 : expr)
29 30
  (* If then else *)
  | If (e0 e1 e2 : expr)
31 32 33 34 35 36 37
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
38
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
39 40 41 42 43 44
  (* Recursive Types *)
  | Fold (e : expr)
  | Unfold (e : expr)
  (* Polymorphic Types *)
  | TLam (e : expr)
  | TApp (e : expr)
45 46
  (* Existential types *)
  | Pack (e : expr)
47
  | Unpack (e : expr) (e' : expr)
48 49 50 51 52 53 54 55
  (* Concurrency *)
  | Fork (e : expr)
  (* Reference Types *)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  (* Compare and swap used for fine-grained concurrency *)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
56
  Bind Scope expr_scope with expr.
57

58
  Instance literal_dec_eq : EqDecision literal.
59
  Proof. solve_decision. Defined.
60

61
  Instance expr_dec_eq : EqDecision expr.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof. solve_decision. Defined.
63

Dan Frumin's avatar
Dan Frumin committed
64
  (** ** Closed expressions *)
65
  Fixpoint is_closed (X : stringset) (e : expr) : bool :=
66 67 68
    match e with
    | Var x => bool_decide (x  X)
    | Rec f x e => is_closed (x :b: f :b: X) e
69
    | Lit _ => true
70 71 72 73 74 75 76 77 78 79 80 81
    | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Fold e | Unfold e | TLam e | TApp e | Pack 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 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
    | Case e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 
                     && is_closed X e2      
    | Unpack e e1 => is_closed X e && is_closed X e1
    end.

82
  Class Closed (X : stringset) (e : expr) := closed : is_closed X e.
83 84 85 86 87 88 89 90 91 92
  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.
  Instance: Proper (() ==> (=) ==> (=)) is_closed.
  Proof.
    intros X Y HXY e e' Hee'. 
    fold_leibniz. by subst.
  Defined.  

Dan Frumin's avatar
Dan Frumin committed
93
  (** ** Values *)
94
  Inductive val :=
95
  | RecV (f x : binder) (e : expr) `{!Closed (x :b: f :b: ) e}
Dan Frumin's avatar
Dan Frumin committed
96
  | TLamV (e : expr) `{!Closed  e} (* only closed lambdas are values *)
97
  | LitV (l : literal)
98 99 100 101
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val)
  | FoldV (v : val)
102
  | PackV (v : val).
103 104
  Bind Scope val_scope with val.

105
  (* Notation for bool and nat *)
Dan Frumin's avatar
Dan Frumin committed
106 107
  Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val :=
    match op,v1,v2 with
108 109 110 111 112 113 114
    | Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b))
    | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
    | Eq, LitV (Nat a), LitV (Nat b) => Some $ if eq_nat_dec a b then LitV (Bool true) else LitV (Bool false)
    | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
    | Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false)
    | Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false)
    | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
Dan Frumin's avatar
Dan Frumin committed
115
    | _,_,_ => None
116
    end.
Dan Frumin's avatar
Dan Frumin committed
117
  Instance val_inh : Inhabited val := populate (LitV Unit).
118 119 120

  Fixpoint of_val (v : val) : expr :=
    match v with
121 122
    | RecV f x e _ => Rec f x e
    | TLamV e _ => TLam e
Dan Frumin's avatar
Dan Frumin committed
123
    | LitV l => Lit l
124 125 126 127
    | PairV v1 v2 => Pair (of_val v1) (of_val v2)
    | InjLV v => InjL (of_val v)
    | InjRV v => InjR (of_val v)
    | FoldV v => Fold (of_val v)
128
    | PackV v => Pack (of_val v)
129 130 131 132
    end.

  Fixpoint to_val (e : expr) : option val :=
    match e with
133 134 135 136 137 138 139 140
    | Rec f x e =>
      if decide (Closed (x :b: f :b: ) e)
      then Some (RecV f x e)
      else None
    | TLam e => 
      if decide (Closed  e)
      then Some (TLamV e)
      else None
Dan Frumin's avatar
Dan Frumin committed
141
    | Lit l => Some (LitV l)
142 143 144 145
    | 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
    | Fold e => v  to_val e; Some (FoldV v)
146
    | Pack e => v  to_val e; Some (PackV v)
147 148 149
    | _ => None
    end.

150
  Lemma to_of_val v : to_val (of_val v) = Some v.
151
  Proof.
152
      by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
153 154
  Qed.

155
  Lemma of_to_val e v : to_val e = Some v  of_val v = e.
156
  Proof.
157
    revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
158
  Qed.
159 160 161 162

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

163
  Instance val_dec_eq : EqDecision val.
164
  Proof.
165
    refine (fun v v' => cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
166
  Defined.
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

  Instance literal_countable : Countable literal.
  Proof.
    refine (inj_countable' (λ l, match l with
    | Nat n => inl (inl n) | Bool b => inl (inr b)
    | Unit => inr (inl ()) | Loc l => inr (inr l)
    end) (λ l, match l with
    | inl (inl n) => Nat n | inl (inr b) => Bool b
    | inr (inl ()) => Unit | inr (inr l) => Loc l
    end) _); by intros [].
  Qed.

  Instance binop_countable : Countable binop.
  Proof.
   refine (inj_countable' (λ op, match op with
    | Add => 0 | Sub => 1 | Eq => 2 | Le => 3 | Lt => 4 | Xor => 5
    end) (λ n, match n with
    | 0 => Add | 1 => Sub | 2 => Eq | 3 => Le | 4 => Lt | _ => Xor
    end) _); by intros [].
  Qed.

  Instance expr_countable : Countable expr.
  Proof.
    set (enc := fix go e :=
           match e with
           | Var x => GenLeaf (inl (inl x))
           | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
           | App e1 e2 => GenNode 1 [go e1; go e2]
           | Lit l => GenLeaf (inr (inl l))
           | Fold e => GenNode 2 [go e]
           | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr op)); go e1; go e2]
           | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
           | Pair e1 e2 => GenNode 5 [go e1; go e2]
           | Fst e => GenNode 6 [go e]
           | Snd e => GenNode 7 [go e]
           | InjL e => GenNode 8 [go e]
           | InjR e => GenNode 9 [go e]
           | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
           | Fork e => GenNode 11 [go e]
           | Alloc e => GenNode 12 [go e]
           | Load e => GenNode 13 [go e]
           | Store e1 e2 => GenNode 14 [go e1; go e2]
           | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
           | Unfold e => GenNode 16 [go e]
           | TLam e => GenNode 17 [go e]
           | TApp e => GenNode 18 [go e]
           | Pack e => GenNode 19 [go e]
           | Unpack e1 e2 => GenNode 20 [go e1; go e2]
           end).
    set (dec := fix go e :=
           match e with
           | GenLeaf (inl (inl x)) => Var x
           | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
           | GenNode 1 [e1; e2] => App (go e1) (go e2)
           | GenLeaf (inr (inl l)) => Lit l
           | GenNode 2 [e] => Fold (go e)
           | GenNode 3 [GenLeaf (inr (inr op)); e1; e2] => BinOp op (go e1) (go e2)
           | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
           | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
           | GenNode 6 [e] => Fst (go e)
           | GenNode 7 [e] => Snd (go e)
           | GenNode 8 [e] => InjL (go e)
           | GenNode 9 [e] => InjR (go e)
           | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
           | GenNode 11 [e] => Fork (go e)
           | GenNode 12 [e] => Alloc (go e)
           | GenNode 13 [e] => Load (go e)
           | GenNode 14 [e1; e2] => Store (go e1) (go e2)
           | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
           | GenNode 16 [e] => Unfold (go e)
           | GenNode 17 [e] => TLam (go e)
           | GenNode 18 [e] => TApp (go e)
           | GenNode 19 [e] => Pack (go e)
           | GenNode 20 [e1; e2] => Unpack (go e1) (go e2)
           | _ => Lit Unit (* dummy *)
           end).
    refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
  Qed.

  Instance val_countable : Countable val.
  Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

Dan Frumin's avatar
Dan Frumin committed
249
  (** ** Evaluation contexts *)
250 251 252 253 254 255
  Inductive ectx_item :=
  | AppLCtx (e2 : expr)
  | AppRCtx (v1 : val)
  | TAppCtx
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
256 257
  | BinOpLCtx (op : binop) (e2 : expr)
  | BinOpRCtx (op : binop) (v1 : val)
258 259 260 261
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
262 263
  | CaseCtx (e1 : expr) (e2 : expr)
  | IfCtx (e1 : expr) (e2 : expr)
264 265
  | FoldCtx
  | UnfoldCtx
266 267
  | PackCtx
  | UnpackLCtx (e2 : expr)
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
  | AllocCtx
  | LoadCtx
  | StoreLCtx (e2 : expr)
  | StoreRCtx (v1 : val)
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
  | CasRCtx (v0 : val) (v1 : val).

  Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
    match Ki with
    | AppLCtx e2 => App e e2
    | AppRCtx v1 => App (of_val v1) e
    | TAppCtx => TApp e
    | PairLCtx e2 => Pair e e2
    | PairRCtx v1 => Pair (of_val v1) e
283 284
    | BinOpLCtx op e2 => BinOp op e e2
    | BinOpRCtx op v1 => BinOp op (of_val v1) e
285 286 287 288 289
    | FstCtx => Fst e
    | SndCtx => Snd e
    | InjLCtx => InjL e
    | InjRCtx => InjR e
    | CaseCtx e1 e2 => Case e e1 e2
290
    | IfCtx e1 e2 => If e e1 e2
291 292
    | FoldCtx => Fold e
    | UnfoldCtx => Unfold e
293 294
    | PackCtx => Pack e
    | UnpackLCtx e2 => Unpack e e2  
295 296 297 298 299 300 301 302 303
    | AllocCtx => Alloc e
    | LoadCtx => Load e
    | StoreLCtx e2 => Store e e2
    | StoreRCtx v1 => Store (of_val v1) e
    | 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
    end.

304
  (** * Substitutions *)  
Dan Frumin's avatar
Dan Frumin committed
305
  (** Parallel substitutions and some properties are defined in [subst.v] *)
306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
  Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
    match e with
    | Var y => if decide (x = y) then es else Var y
    | Rec f y e =>
      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)
    | TLam e => TLam (subst x es e)
    | TApp e => TApp (subst x es e)
    | Lit l => Lit l
    | 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)
    | Fold e => Fold (subst x es e)
    | Unfold e => Unfold (subst x es e)
    | Pack e => Pack (subst x es e)                
    | Unpack e0 e => 
      Unpack (subst x es e0) (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)
  end.
337

338 339 340 341
  Definition subst' (mx : binder) (es : expr) : expr  expr :=
    match mx with BNamed x => subst x es | BAnon => id end.
 
  (** * Reduction semantics *)
342 343
  Definition state : Type := gmap loc val.

Robbert Krebbers's avatar
Robbert Krebbers committed
344
  Inductive head_step : expr  state  expr  state  list expr  Prop :=
345
  (* β *)
346
  | BetaS f x e1 e2 v2 σ e' :
347
      to_val e2 = Some v2 
348 349 350 351
      Closed (x :b: f :b: ) e1 
      (* e' = subst_p (<[x:=e2]>{[f:=(Rec f x e1)]}) e1  *)
      e' = subst' f (Rec f x e1) (subst' x e2 e1) 
      head_step (App (Rec f x e1) e2) σ e' σ []
352 353 354
  (* Products *)
  | FstS e1 v1 e2 v2 σ :
      to_val e1 = Some v1  to_val e2 = Some v2 
Robbert Krebbers's avatar
Robbert Krebbers committed
355
      head_step (Fst (Pair e1 e2)) σ e1 σ []
356 357
  | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1  to_val e2 = Some v2 
Robbert Krebbers's avatar
Robbert Krebbers committed
358
      head_step (Snd (Pair e1 e2)) σ e2 σ []
359
  (* Sums *)
360
  | CaseLS e0 v0 e1 e2 σ e' :
361
      to_val e0 = Some v0 
362 363 364
      e' = App e1 e0 
      head_step (Case (InjL e0) e1 e2) σ e' σ []
  | CaseRS e0 v0 e1 e2 σ e' :
365
      to_val e0 = Some v0 
366 367
      e' = App e2 e0 
      head_step (Case (InjR e0) e1 e2) σ e' σ []
Dan Frumin's avatar
Dan Frumin committed
368 369 370 371 372 373
  (* nat bin op *)
  | BinOpS op e1 e2 v1 v2 v σ :
      to_val e1 = Some v1 
      to_val e2 = Some v2 
      binop_eval op v1 v2 = Some v 
      head_step (BinOp op e1 e2) σ (of_val v) σ []
374 375
  (* If then else *)
  | IfFalse e1 e2 σ :
376
      head_step (If (Lit (Bool false)) e1 e2) σ e2 σ []
377
  | IfTrue e1 e2 σ :
378
      head_step (If (Lit (Bool true)) e1 e2) σ e1 σ []
379 380 381
  (* Recursive Types *)
  | Unfold_Fold e v σ :
      to_val e = Some v 
Robbert Krebbers's avatar
Robbert Krebbers committed
382
      head_step (Unfold (Fold e)) σ e σ []
383 384
  (* Polymorphic Types *)
  | TBeta e σ :
385
      Closed  e 
Robbert Krebbers's avatar
Robbert Krebbers committed
386
      head_step (TApp (TLam e)) σ e σ []
387
  (* Existential types *)
388
  | Unpack_Pack e1 v e2 σ e' :
389
      to_val e1 = Some v 
390 391
      e' = App e2 e1 
      head_step (Unpack (Pack e1) e2) σ e' σ []
392 393
  (* Concurrency *)
  | ForkS e σ:
394
      head_step (Fork e) σ (Lit Unit) σ [e]
395 396 397
  (* Reference Types *)
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
398
     head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) []
399 400
  | LoadS l v σ :
     σ !! l = Some v 
401
     head_step (Load (Lit (Loc l))) σ (of_val v) σ []
402 403
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
404
     head_step (Store (Lit (Loc l)) e) σ (Lit Unit) (<[l:=v]>σ) []
405 406 407 408
  (* Compare and swap *)
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
409
     head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool false)) σ []
410 411 412
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
413
     head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool true)) (<[l:=v2]>σ) [].
414

415 416 417 418 419 420 421 422 423 424 425 426 427
  Definition is_atomic (e : expr) : Prop :=
    match e with
    | Alloc e => is_Some (to_val e)
    | Load e =>  is_Some (to_val e)
    | Store e1 e2 => is_Some (to_val e1)  is_Some (to_val e2)
    | CAS e0 e1 e2 => is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
    | Fork _ => True
    | _ => False
    end.

  Canonical Structure stateC := leibnizC state.
  Canonical Structure valC := leibnizC val.
  Canonical Structure exprC := leibnizC expr.
428 429
  Canonical Structure locC := leibnizC loc.
  Canonical Structure ectx_itemC := leibnizC ectx_item.
430

Robbert Krebbers's avatar
Robbert Krebbers committed
431 432 433 434
  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.

435 436 437
  Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
  Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
438
  Lemma val_stuck e1 σ1 e2 σ2 ef :
439 440 441 442 443
    head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
  Proof. destruct 1; naive_solver. Qed.

  Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
    head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
444
  Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
445 446 447 448 449 450 451 452 453 454 455 456

  Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
    to_val e1 = None  to_val e2 = None 
    fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
  Proof.
    destruct Ki1, Ki2; intros; try discriminate; simplify_eq;
    repeat match goal with
           | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
           end; auto.
  Qed.

  Lemma alloc_fresh e v σ :
Dan Frumin's avatar
Dan Frumin committed
457
    let l := fresh (dom (gset loc) σ) in
458
    to_val e = Some v  head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [].
Dan Frumin's avatar
Dan Frumin committed
459
  Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
460 461
End lang.

Dan Frumin's avatar
Dan Frumin committed
462
(** Language instance for Iris *)
Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465
Program Instance heap_ectxi_lang :
  EctxiLanguage
    (lang.expr) lang.val lang.ectx_item lang.state := {|
466
  of_val := lang.of_val; to_val := lang.to_val;
Robbert Krebbers's avatar
Robbert Krebbers committed
467
  fill_item := lang.fill_item; head_step := lang.head_step
468 469
|}.
Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
Robbert Krebbers's avatar
Robbert Krebbers committed
470 471
  lang.val_stuck, lang.fill_item_val, lang.fill_item_no_val_inj,
  lang.head_ctx_step_val.
472

Robbert Krebbers's avatar
Robbert Krebbers committed
473 474 475 476
Canonical Structure lang := ectx_lang (lang.expr).

Export lang.

477 478 479
(* This lemma is helpful for tactics on locked values and for reifying locked values. *)
Lemma of_val_unlock v e : of_val v = e  of_val (locked v) = e.
Proof. by unlock. Qed.
Dan Frumin's avatar
Dan Frumin committed
480 481 482 483

Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
484

Robbert Krebbers's avatar
Robbert Krebbers committed
485
Lemma is_atomic_correct e : is_atomic e  language.atomic e.
486
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
487
  intros ?; apply ectx_language_atomic.
Dan Frumin's avatar
Dan Frumin committed
488
  - destruct 1; simpl; eauto.
489 490
  - apply ectxi_language_sub_values=> /= Ki e' Hfill.
    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
491
                   naive_solver eauto using to_val_is_Some.
492 493
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
494 495 496
Ltac solve_atomic :=
  apply is_atomic_correct; simpl; repeat split;
    rewrite ?to_of_val; eapply mk_is_Some; fast_done.
497

Robbert Krebbers's avatar
Robbert Krebbers committed
498
Hint Extern 0 (language.atomic _) => solve_atomic.
499
Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
500

501 502 503 504 505 506 507 508 509 510 511 512
(* Some other useful tactics *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
  | H : head_step ?e _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.