tactics.v 6.1 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stbor.lang Require Export lang.
Ralf Jung's avatar
Ralf Jung committed
2
From stbor.sim Require Export simple.
Ralf Jung's avatar
Ralf Jung committed
3
4
5
6
From stbor.sim Require Import body.

Ltac reshape_expr e tac :=
  (* [vs] is the accumulator *)
Ralf Jung's avatar
Ralf Jung committed
7
  let rec go_call K v vs es :=
Ralf Jung's avatar
Ralf Jung committed
8
    match es with
Ralf Jung's avatar
Ralf Jung committed
9
10
    | (Val ?v) :: ?es => go_call K v (v :: vs) es
    | ?e :: ?es => go (CallRCtx v (reverse vs) es :: K) e
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
15
    end
  (* [K] accumulates the context *)
  with go K e :=
  match e with
  | _ => tac K e
Ralf Jung's avatar
Ralf Jung committed
16
17
  | Call (Val ?v) ?el => go_call K (ValR v) (@nil result) el
  | Call (of_result ?r) ?el => go_call K r (@nil result) el
Ralf Jung's avatar
Ralf Jung committed
18
  | Call ?e ?el => go (CallLCtx el :: K) e
Ralf Jung's avatar
Ralf Jung committed
19
  | EndCall ?e => go (EndCallCtx :: K) e
Ralf Jung's avatar
Ralf Jung committed
20
21
  | BinOp ?op (Val ?v1) ?e2 => go (BinOpRCtx op (ValR v1) :: K) e2
  | BinOp ?op (of_result ?r) ?e2 => go (BinOpRCtx op r :: K) e2
Ralf Jung's avatar
Ralf Jung committed
22
  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
Ralf Jung's avatar
Ralf Jung committed
23
24
25
26
27
  | Proj (Val ?v1) ?e2 => go (ProjRCtx (ValR v1) :: K) e2
  | Proj (of_result ?r1) ?e2 => go (ProjRCtx r1 :: K) e2
  | Proj ?e1 ?e2 => go (ProjLCtx e2 :: K) e1
  | Conc (Val ?v1) ?e2 => go (ConcRCtx (ValR v1) :: K) e2
  | Conc (of_result ?r1) ?e2 => go (ConcRCtx r1 :: K) e2
Ralf Jung's avatar
Ralf Jung committed
28
  | Conc ?e1 ?e2 => go (ConcLCtx e2 :: K) e1
Ralf Jung's avatar
Ralf Jung committed
29
  | Copy ?e => go (CopyCtx :: K) e
Ralf Jung's avatar
Ralf Jung committed
30
31
  | Write (Place ?l1 ?tg ?ty) ?e2 => go (WriteRCtx (PlaceR l1 tg ty) :: K) e2
  | Write (of_result ?r1) ?e2 => go (WriteRCtx r1 :: K) e2
Ralf Jung's avatar
Ralf Jung committed
32
  | Write ?e1 ?e2 => go (WriteLCtx e2 :: K) e1
Ralf Jung's avatar
Ralf Jung committed
33
34
35
36
37
  | Free ?e => go (FreeCtx :: K) e
  | Deref ?e ?T => go (DerefCtx T :: K) e
  | Ref ?e => go (RefCtx :: K) e
  | Retag ?e ?k => go (RetagCtx k :: K) e
  | Let ?x ?e1 ?e2 => go (LetCtx x e2 :: K) e1
Ralf Jung's avatar
Ralf Jung committed
38
  | Case ?e ?el => go (CaseCtx el :: K) e
Ralf Jung's avatar
Ralf Jung committed
39
40
41
  end
  in go (@nil ectx_item) e.

42
43
(** bind if K is not empty. Otherwise do nothing.
Binds cost us steps, so don't waste them! *)
Ralf Jung's avatar
Ralf Jung committed
44
Ltac sim_body_bind_core Ks es Kt et :=
45
46
47
48
  (* Ltac is SUCH a bad language... *)
  match Ks with
  | [] => match Kt with
          | [] => idtac
Ralf Jung's avatar
Ralf Jung committed
49
          | _ => eapply (sim_body_bind _ _ Ks es Kt et)
50
          end
Ralf Jung's avatar
Ralf Jung committed
51
  | _ => eapply (sim_body_bind _ _ Ks es Kt et)
52
  end.
Ralf Jung's avatar
Ralf Jung committed
53
Ltac sim_simple_bind_core Ks es Kt et :=
54
55
56
57
  (* Ltac is SUCH a bad language... *)
  match Ks with
  | [] => match Kt with
          | [] => idtac
Ralf Jung's avatar
Ralf Jung committed
58
          | _ => eapply (sim_simple_bind _ _ Ks es Kt et)
59
          end
Ralf Jung's avatar
Ralf Jung committed
60
  | _ => eapply (sim_simple_bind _ _ Ks es Kt et)
61
62
  end.

Ralf Jung's avatar
Ralf Jung committed
63
64
65
66
67
68
69
Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
  match goal with 
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr es ltac:(fun Ks es =>
      unify es efocs;
      reshape_expr et ltac:(fun Kt et =>
        unify et efoct;
Ralf Jung's avatar
Ralf Jung committed
70
        sim_body_bind_core Ks es Kt et
Ralf Jung's avatar
Ralf Jung committed
71
72
      )
    )
Ralf Jung's avatar
Ralf Jung committed
73
74
75
76
77
  | |- _ ⊨ˢ{_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr es ltac:(fun Ks es =>
      unify es efocs;
      reshape_expr et ltac:(fun Kt et =>
        unify et efoct;
Ralf Jung's avatar
Ralf Jung committed
78
        sim_simple_bind_core Ks es Kt et
Ralf Jung's avatar
Ralf Jung committed
79
80
      )
    )
Ralf Jung's avatar
Ralf Jung committed
81
  end.
Ralf Jung's avatar
Ralf Jung committed
82
83
84
85
86
87

Tactic Notation "sim_apply" open_constr(lem) :=
  match goal with
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr es ltac:(fun Ks es =>
      reshape_expr et ltac:(fun Kt et =>
Ralf Jung's avatar
Ralf Jung committed
88
        sim_body_bind_core Ks es Kt et;
Ralf Jung's avatar
Ralf Jung committed
89
        apply: lem
Ralf Jung's avatar
Ralf Jung committed
90
91
      )
    )
Ralf Jung's avatar
Ralf Jung committed
92
93
94
  | |- _ ⊨ˢ{_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr es ltac:(fun Ks es =>
      reshape_expr et ltac:(fun Kt et =>
Ralf Jung's avatar
Ralf Jung committed
95
        sim_simple_bind_core Ks es Kt et;
Ralf Jung's avatar
Ralf Jung committed
96
        apply: lem
Ralf Jung's avatar
Ralf Jung committed
97
98
      )
    )
Ralf Jung's avatar
Ralf Jung committed
99
  end.
100

101
102
103
104
105
106
107
108
109
110
(* HACK to avoid a bind-left/right rule. Does not work in general (e.g. when
there is an [Alloc T] in eval position on the left), but works for now. *)
Ltac test_pure_head e :=
  match e with
  | of_result _ => idtac
  | Val _ => idtac
  | Place _ _ _ => idtac
  | _ => fail
  end.

Ralf Jung's avatar
Ralf Jung committed
111
112
Tactic Notation "sim_bind_r" open_constr(efoc) :=
  match goal with 
113
114
115
116
117
118
119
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr es ltac:(fun Ks es =>
      test_pure_head es;
      reshape_expr et ltac:(fun Kt et =>
        unify et efoc;
        sim_body_bind_core Ks es Kt et
      )
Ralf Jung's avatar
Ralf Jung committed
120
121
122
123
124
125
    )
  end.

Tactic Notation "sim_apply_r" open_constr(lem) :=
  match goal with
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
126
127
128
129
130
131
    reshape_expr es ltac:(fun Ks es =>
      test_pure_head es;
      reshape_expr et ltac:(fun Kt et =>
        sim_body_bind_core Ks es Kt et;
        apply: lem
      )
Ralf Jung's avatar
Ralf Jung committed
132
133
134
135
136
    )
  end.

Tactic Notation "sim_bind_l" open_constr(efoc) :=
  match goal with 
137
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
Ralf Jung's avatar
Ralf Jung committed
138
139
    reshape_expr es ltac:(fun Ks es =>
      unify es efoc;
140
141
142
143
      reshape_expr et ltac:(fun Kt et =>
        test_pure_head et;
        sim_body_bind_core Ks es Kt et
      )
Ralf Jung's avatar
Ralf Jung committed
144
145
146
147
148
    )
  end.

Tactic Notation "sim_apply_l" open_constr(lem) :=
  match goal with
149
150
151
152
153
154
155
  | |- _ {_,_,_} (?es, _)  (?et, _) : _ =>
    reshape_expr et ltac:(fun Kt et =>
      test_pure_head et;
      reshape_expr es ltac:(fun Ks es =>
        sim_body_bind_core Ks es Kt et;
        apply: lem
      )
Ralf Jung's avatar
Ralf Jung committed
156
157
158
    )
  end.

159
160
161
162
163
164
165
166
167
168
(** The expectation is that lemmas state their resource requirements as
[r  frame  what_lemma_needs].  Users eapply the lemma, and [frame]
becomes an evar. [solve_res] solves such goals. *)
Lemma res_search_descend (R W T F L : resUR) :
  T  L  F  W 
  T  L  R  F  R  W.
Proof. intros ->. rewrite - !assoc. f_equiv. exact: comm. Qed.
Lemma res_search_found_left (F W : resUR) :
  W  F  F  W.
Proof. exact: comm. Qed.
Ralf Jung's avatar
Ralf Jung committed
169
170
171
Lemma res_search_found_unit (F W : resUR) :
  F  F  ε.
Proof. rewrite right_id //. Qed.
172
173
174
Lemma res_search_singleton (R W : resUR) :
  W  ε  W.
Proof. rewrite left_id //. Qed.
Ralf Jung's avatar
Ralf Jung committed
175
176
177
178
179
180
Lemma res_search_from_incl (r1 r2 r3 : resUR) :
  r2  r3  r1 
  r1  r2.
Proof.
  intros EQ. eexists. rewrite EQ [r3  _]comm. done.
Qed.
181
182
183
184
Ltac solve_res :=
  match goal with
  | |- _  _  _ =>
      reflexivity
Ralf Jung's avatar
Ralf Jung committed
185
186
  | |- _  _  ε =>
      exact: res_search_found_unit
187
188
189
190
191
192
193
194
195
196
  | |- _  _  _ =>
      exact: res_search_found_left
  | |- _  _ =>
      exact: res_search_singleton
  | |- _  _  _ =>
    (* The descent lemma makes sure we don't descend below
       the *last* operator. We always want to preserve having
       an operator on the LHS. *)
    simple apply res_search_descend;
    solve_res
Ralf Jung's avatar
Ralf Jung committed
197
198
199
  | |- _  _ =>
    simple eapply res_search_from_incl;
    solve_res
200
end.
Ralf Jung's avatar
Ralf Jung committed
201
202
203

(** For example proofs. *)
Ltac solve_sim := solve [ fast_done | solve_res | done ].