tactics.v 3.29 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
6
7
8
9
(** The tactic [inv_step] performs inversion on hypotheses of the
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
11
Ltac inv_step :=
  repeat match goal with
12
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
13
14
15
16
17
18
19
20
  | 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 _ _ _ _ |- _ =>
     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.

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
  | of_val' ?v => v
29
30
31
32
33
34
35
36
37
  | 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)
  | Loc ?l => constr:(LocV l)
  end in let v := go e in first [tac v | fail 2].

38
39
40
41
Ltac reshape_expr e tac :=
  let rec go K e :=
  match e with
  | _ => tac (reverse K) e
42
43
44
  | 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
45
  | BinOp ?op ?e1 ?e2 =>
46
47
     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
48
  | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
49
50
  | Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
  | Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
51
52
53
54
55
56
57
  | 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
58
59
  | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
60
  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
61
62
     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
     | go (CasMCtx v0 e2 :: K) e1 ])
63
  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
64
65
  end in go (@nil ectx_item) e.

66
67
68
69
(** The tactic [do_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. *)
70
71
Tactic Notation "do_step" tactic3(tac) :=
  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
72
73
  simpl;
  match goal with
74
75
  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
     first [apply alloc_fresh|econstructor];
76
77
78
79
     (* If there is at least one goal left now, then do the last
        goal last -- it may rely on evars being instantiaed elsewhere. *)
     first [ fail
           | rewrite ?to_of_val; [tac..|]; tac; fast_done ]
80
  end.