aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/autorewrite.ml
blob: 13f8784f583b5739d23412953ddf0cf6afe52cb0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
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
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Equality
open Hipattern
open Names
open Pp
open Proof_type
open Tacticals
open Tacinterp
open Tactics
open Term
open Termops
open Util
open Glob_term
open Vernacinterp
open Tacexpr
open Mod_subst

(* Rewriting rules *)
type rew_rule = { rew_lemma: constr;
		  rew_type: types;
		  rew_pat: constr;
		  rew_l2r: bool;
		  rew_tac: glob_tactic_expr }

let subst_hint subst hint =
  let cst' = subst_mps subst hint.rew_lemma in
  let typ' = subst_mps subst hint.rew_type in
  let pat' = subst_mps subst hint.rew_pat in
  let t' = Tacinterp.subst_tactic subst hint.rew_tac in
    if hint.rew_lemma == cst' && hint.rew_tac == t' then hint else
      { hint with
	rew_lemma = cst'; rew_type = typ';
	rew_pat = pat';	rew_tac = t' }

module HintIdent =
struct
  type t = int * rew_rule

  let compare (i,t) (i',t') =
    Pervasives.compare i i'
(*     Pervasives.compare t.rew_lemma t'.rew_lemma *)

  let subst s (i,t) = (i,subst_hint s t)

  let constr_of (i,t) = t.rew_pat
end

module HintOpt =
struct
  let reduce c = c
  let direction = true
end

module HintDN = Term_dnet.Make(HintIdent)(HintOpt)

(* Summary and Object declaration *)
let rewtab =
  ref (Stringmap.empty : HintDN.t Stringmap.t)

let _ =
  let init () = rewtab := Stringmap.empty in
  let freeze () = !rewtab in
  let unfreeze fs = rewtab := fs in
  Summary.declare_summary "autorewrite"
    { Summary.freeze_function   = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function     = init }

let find_base bas =
 try Stringmap.find bas !rewtab
 with
  Not_found ->
   errorlabstrm "AutoRewrite"
     (str ("Rewriting base "^(bas)^" does not exist."))

let find_rewrites bas =
  List.rev_map snd (HintDN.find_all (find_base bas))

let find_matches bas pat =
  let base = find_base bas in
  let res = HintDN.search_pattern base pat in
    List.map (fun ((_,rew), esubst, subst) -> rew) res

let print_rewrite_hintdb bas =
  ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
	   prlist_with_sep Pp.cut
	   (fun h ->
	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
	       str " then use tactic " ++
	       Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
	   (find_rewrites bas))

type raw_rew_rule = loc * constr * bool * raw_tactic_expr

(* Applies all the rules of one base *)
let one_base general_rewrite_maybe_in tac_main bas =
  let lrul = find_rewrites bas in
  let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
    tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
      tclTHEN tac
        (tclREPEAT_MAIN
	    (tclTHENFIRST (general_rewrite_maybe_in dir csr tc) tac_main)))
      tclIDTAC lrul))

(* The AutoRewrite tactic *)
let autorewrite ?(conds=Naive) tac_main lbas =
  tclREPEAT_MAIN (tclPROGRESS
    (List.fold_left (fun tac bas ->
       tclTHEN tac
        (one_base (fun dir c tac ->
	  let tac = tac, conds in
	    general_rewrite dir all_occurrences true false ~tac c)
	  tac_main bas))
      tclIDTAC lbas))

let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
  fun gl ->
 (* let's check at once if id exists (to raise the appropriate error) *)
 let _ = List.map (Tacmach.pf_get_hyp gl) idl in
 let general_rewrite_in id =
  let id = ref id in
  let to_be_cleared = ref false in
   fun dir cstr tac gl ->
    let last_hyp_id =
     match Tacmach.pf_hyps gl with
        (last_hyp_id,_,_)::_ -> last_hyp_id
      | _ -> (* even the hypothesis id is missing *)
             error ("No such hypothesis: " ^ (string_of_id !id) ^".")
    in
    let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in
    let gls = gl'.Evd.it in
    match gls with
       g::_ ->
        (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
            (lastid,_,_)::_ ->
              if last_hyp_id <> lastid then
               begin
                let gl'' =
                  if !to_be_cleared then
                   tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl
                  else gl' in
                id := lastid ;
                to_be_cleared := true ;
                gl''
               end
              else
               begin
                to_be_cleared := false ;
                gl'
               end
          | _ -> assert false) (* there must be at least an hypothesis *)
     | _ -> assert false (* rewriting cannot complete a proof *)
 in
 tclMAP (fun id ->
  tclREPEAT_MAIN (tclPROGRESS
    (List.fold_left (fun tac bas ->
       tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas)))
   idl gl

let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]

let gen_auto_multi_rewrite conds tac_main lbas cl =
  let try_do_hyps treat_id l =
    autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
  in
  if cl.concl_occs <> all_occurrences_expr &
     cl.concl_occs <> no_occurrences_expr
  then
    error "The \"at\" syntax isn't available yet for the autorewrite tactic."
  else
    let compose_tac t1 t2 =
      match cl.onhyps with
	| Some [] -> t1
	| _ ->      tclTHENFIRST t1 t2
    in
    compose_tac
	(if cl.concl_occs <> no_occurrences_expr then autorewrite ~conds tac_main lbas else tclIDTAC)
	(match cl.onhyps with
	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
	   | None ->
	       fun gl ->
		 (* try to rewrite in all hypothesis
		    (except maybe the rewritten one) *)
		 let ids =  Tacmach.pf_ids_of_hyps gl
		 in try_do_hyps (fun id -> id)  ids gl)

let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC

let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
  let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in
  match onconcl,cl.Tacexpr.onhyps with
    | false,Some [_] | true,Some [] | false,Some [] ->
	(* autorewrite with .... in clause using tac n'est sur que
	   si clause represente soit le but soit UNE hypothese
	*)
	gen_auto_multi_rewrite conds tac_main lbas cl gl
    | _ ->
	    Util.errorlabstrm "autorewrite"
	      (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")

(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
  let base = try find_base rbase with _ -> HintDN.empty in
  let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
  let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
    rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab


let subst_hintrewrite (subst,(rbase,list as node)) =
  let list' = HintDN.subst subst list in
    if list' == list then node else
      (rbase,list')

let classify_hintrewrite x = Libobject.Substitute x


(* Declaration of the Hint Rewrite library object *)
let inHintRewrite =
  Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
    Libobject.cache_function = cache_hintrewrite;
    Libobject.load_function = (fun _ -> cache_hintrewrite);
    Libobject.subst_function = subst_hintrewrite;
    Libobject.classify_function = classify_hintrewrite }


open Clenv

type hypinfo = {
  hyp_cl : clausenv;
  hyp_prf : constr;
  hyp_ty : types;
  hyp_car : constr;
  hyp_rel : constr;
  hyp_l2r : bool;
  hyp_left : constr;
  hyp_right : constr;
}

let evd_convertible env evd x y =
  try
    ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true 
  (* try ignore(Evarconv.the_conv_x env x y evd); true *)
  with _ -> false

let decompose_applied_relation metas env sigma c ctype left2right =
  let find_rel ty =
    let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
    let eqclause =
      if metas then eqclause
      else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
    in
    let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
    let rec split_last_two = function
      | [c1;c2] -> [],(c1, c2)
      | x::y::z ->
	  let l,res = split_last_two (y::z) in x::l, res
      | _ -> raise Not_found
    in
      try
	let others,(c1,c2) = split_last_two args in
	let ty1, ty2 =
	  Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
	in
(* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* 	  else *)
	    Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
		   hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
		   hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
      with Not_found -> None
  in
    match find_rel ctype with
    | Some c -> Some c
    | None ->
	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
	match find_rel (it_mkProd_or_LetIn t' ctx) with
	| Some c -> Some c
	| None -> None

let find_applied_relation metas loc env sigma c left2right =
  let ctype = Typing.type_of env sigma c in
    match decompose_applied_relation metas env sigma c ctype left2right with
    | Some c -> c
    | None ->
	user_err_loc (loc, "decompose_applied_relation",
		     str"The type" ++ spc () ++ Printer.pr_constr_env env ctype ++
		       spc () ++ str"of this term does not end with an applied relation.")

(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
  let counter = ref 0 in
  let lrul =
    List.fold_left
      (fun dn (loc,c,b,t) ->
	let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
	let pat = if b then info.hyp_left else info.hyp_right in
	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
		    rew_pat = pat; rew_l2r = b;
		    rew_tac = Tacinterp.glob_tactic t}
	in incr counter;
	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
  in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))