heap_lang_tactics.v 3.53 KB
Newer Older
1 2 3 4
Require Export barrier.heap_lang.
Require Import prelude.fin_maps.
Import heap_lang.

5 6 7 8 9 10
(** The tactic [inv_step] performs inversion on hypotheses of the shape
[prim_step] and [head_step]. For hypotheses of the shape [prim_step] it will
decompose the evaluation context. 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. *)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
Ltac inv_step :=
  repeat match goal with
  | _ => progress simplify_map_equality' (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
  | H : prim_step _ _ _ _ _ |- _ => destruct H; subst
  | H : _ = fill ?K ?e |- _ =>
     destruct K as [|[]];
     simpl in H; first [subst e|discriminate H|injection' H]
     (* ensure that we make progress for each subgoal *)
  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
    apply values_head_stuck, (fill_not_val K) in H;
    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
  | 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.

30 31 32
(** 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. *)
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
Ltac reshape_expr e tac :=
  let rec go K e :=
  match e with
  | _ => tac (reverse K) e
  | App ?e1 ?e2 =>
     lazymatch e1 with
     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
     end
  | Plus ?e1 ?e2 =>
     lazymatch e1 with
     | of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
     end
  | Le ?e1 ?e2 =>
     lazymatch e1 with
     | of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
     end
  | Pair ?e1 ?e2 =>
     lazymatch e1 with
     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
     end
  | 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
  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
  | Cas ?e0 ?e1 ?e2 =>
     lazymatch e0 with
     | of_val ?v0 =>
        lazymatch e1 with
        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
        | _ => go (CasMCtx v0 e2 :: K) e1
        end
     | _ => go (CasLCtx e1 e2 :: K) e0
     end
  end in go (@nil ectx_item) e.

72 73 74 75 76
(** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step]
and [head_step] by performing a reduction step and uses [tac] to solve any
side-conditions generated by individual steps. In case of goals of the shape
[reducible] and [prim_step], it will try to decompose to expression on the LHS
into an evaluation context and head-redex. *)
77
Ltac do_step tac :=
78
  try match goal with |- language.reducible _ _ => eexists _, _, _ end;
79 80 81 82
  simpl;
  match goal with
  | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
     reshape_expr e1 ltac:(fun K e1' =>
83
       eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
84
       first [apply alloc_fresh|econstructor];
85
       rewrite ?to_of_val; tac; fail)
86 87 88
  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
     first [apply alloc_fresh|econstructor];
     rewrite ?to_of_val; tac; fail
89
  end.