tactics.v 3.21 KB
Newer Older
1 2
From iris.heap_lang Require Export substitution.
From iris.prelude Require Import fin_maps.
3 4
Import heap_lang.

5
(** The tactic [inv_head_step] performs inversion on hypotheses of the
6 7 8 9
shape [head_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
to values, and finite map operations. This tactic is slightly ad-hoc
and tuned for proving our lifting lemmas. *)
10
Ltac inv_head_step :=
11
  repeat match goal with
12
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
13 14 15
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
  | H : head_step ?e _ _ _ _ |- _ =>
16
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
17 18 19 20
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

21 22 23
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
24 25 26 27
Ltac reshape_val e tac :=
  let rec go e :=
  match e with
  | of_val ?v => v
28
  | wexpr' ?e => reshape_val e tac
29 30 31 32 33 34 35 36
  | Rec ?f ?x ?e => constr:(RecV f x e)
  | Lit ?l => constr:(LitV l)
  | Pair ?e1 ?e2 =>
    let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
  | InjL ?e => let v := reshape_val e in constr:(InjLV v)
  | InjR ?e => let v := reshape_val e in constr:(InjRV v)
  end in let v := go e in first [tac v | fail 2].

37 38 39 40
Ltac reshape_expr e tac :=
  let rec go K e :=
  match e with
  | _ => tac (reverse K) e
41 42 43
  | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
  | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
  | UnOp ?op ?e => go (UnOpCtx op :: K) e
44
  | BinOp ?op ?e1 ?e2 =>
45 46
     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
47
  | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
48 49
  | Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
  | Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
50 51 52 53 54 55 56
  | Fst ?e => go (FstCtx :: K) e
  | Snd ?e => go (SndCtx :: K) e
  | InjL ?e => go (InjLCtx :: K) e
  | InjR ?e => go (InjRCtx :: K) e
  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
  | Alloc ?e => go (AllocCtx :: K) e
  | Load ?e => go (LoadCtx :: K) e
57 58
  | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
59
  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
60 61
     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
     | go (CasMCtx v0 e2 :: K) e1 ])
62
  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
63 64
  end in go (@nil ectx_item) e.

65 66 67 68
(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
[head_step] by performing a reduction step and uses [tac] to solve any
side-conditions generated by individual steps. *)
Tactic Notation "do_head_step" tactic3(tac) :=
69
  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
70 71
  simpl;
  match goal with
72 73
  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
     first [apply alloc_fresh|econstructor];
74 75
       (* solve [to_val] side-conditions *)
       first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
76
  end.