Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 192 insertions, 113 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4759b6da..b0645744 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: autorewrite.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id$ *)
 
 open Equality
 open Hipattern
@@ -25,83 +25,119 @@ open Tacexpr
 open Mod_subst
 
 (* Rewriting rules *)
-(* the type is the statement of the lemma constr. Used to elim duplicates. *)
-type rew_rule = constr * types * bool * glob_tactic_expr
+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 : rew_rule list Stringmap.t)
+  ref (Stringmap.empty : HintDN.t Stringmap.t)
 
-let _ = 
+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;
-      Summary.survive_module = false;
-      Summary.survive_section   = false }
+      Summary.init_function     = init }
 
-let print_rewrite_hintdb bas =
- try
-  let hints = Stringmap.find bas !rewtab in
-   ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
-    prlist_with_sep Pp.cut
-     (fun (c,typ,d,t) ->
-       str (if d then "rewrite -> " else "rewrite <- ") ++
-       Printer.pr_lconstr c ++ str " of type " ++ Printer.pr_lconstr typ ++
-       str " then use tactic " ++ 
-       Pptactic.pr_glob_tactic (Global.env()) t) hints)
+let find_base bas =
+ try Stringmap.find bas !rewtab
  with
-  Not_found -> 
-   errorlabstrm "AutoRewrite" 
+  Not_found ->
+   errorlabstrm "AutoRewrite"
      (str ("Rewriting base "^(bas)^" does not exist."))
 
-type raw_rew_rule = constr * bool * raw_tactic_expr
+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 =
-    try
-      Stringmap.find bas !rewtab
-    with Not_found ->
-      errorlabstrm "AutoRewrite"
-        (str ("Rewriting base "^(bas)^" does not exist."))
-  in
-  let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
+  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 
-	  (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc)))
+        (tclREPEAT_MAIN
+	    (tclTHENFIRST (general_rewrite_maybe_in dir csr tc) tac_main)))
       tclIDTAC lrul))
 
-
-
 (* The AutoRewrite tactic *)
-let autorewrite tac_main lbas =
+let autorewrite ?(conds=Naive) tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
-    (List.fold_left (fun tac bas -> 
+    (List.fold_left (fun tac bas ->
        tclTHEN tac
-        (one_base (fun dir -> general_rewrite dir all_occurrences)
+        (one_base (fun dir c tac ->
+	  let tac = tac, conds in
+	    general_rewrite dir all_occurrences false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
 
-let autorewrite_multi_in idl tac_main lbas : tactic =
-  fun gl -> 
+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 gl ->
+   fun dir cstr tac gl ->
     let last_hyp_id =
      match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) 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 !id cstr false gl in
+    let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
@@ -125,109 +161,152 @@ let autorewrite_multi_in idl tac_main lbas : tactic =
           | _ -> assert false) (* there must be at least an hypothesis *)
      | _ -> assert false (* rewriting cannot complete a proof *)
  in
- tclMAP (fun id -> 
+ tclMAP (fun id ->
   tclREPEAT_MAIN (tclPROGRESS
-    (List.fold_left (fun tac bas -> 
+    (List.fold_left (fun tac bas ->
        tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas)))
    idl gl
 
-let autorewrite_in id = autorewrite_multi_in [id]
+let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
 
-let gen_auto_multi_rewrite tac_main lbas cl = 
-  let try_do_hyps treat_id l = 
-    autorewrite_multi_in (List.map treat_id l) tac_main lbas
-  in 
+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 
+  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 
+  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 tac_main lbas else tclIDTAC)
-	(match cl.onhyps with 
+	(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 
+	   | 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 = gen_auto_multi_rewrite Refiner.tclIDTAC
+let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC
 
-let auto_multi_rewrite_with tac_main lbas cl gl =
+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 
+  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 tac_main  lbas cl gl
-    | _ -> 
-	    Util.errorlabstrm "autorewrite" 
+	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 l = 
-    try 
-      let oldl = Stringmap.find rbase !rewtab in
-      let lrl =
-       List.map
-        (fun (c,dummy,b,t) ->
-          (* here we substitute the dummy value with the right one *)
-          c,Typing.type_of (Global.env ()) Evd.empty c,b,t) lrl in
-      (List.filter
-          (fun (_,typ,_,_) ->
-            not (List.exists (fun (_,typ',_,_) -> Term.eq_constr typ typ') oldl)
-          ) lrl) @ oldl
-    with
-      | Not_found -> lrl
-  in
-    rewtab:=Stringmap.add rbase l !rewtab
-
-let export_hintrewrite x = Some x
-
-let subst_hintrewrite (_,subst,(rbase,list as node)) = 
-  let subst_first (cst,typ,b,t as pair) = 
-    let cst' = subst_mps subst cst in
-    let typ' =
-     (* here we do not have the environment and Global.env () is not the
-        one where cst' lives in. Thus we can just put a dummy value and
-        override it in cache_hintrewrite *)
-     typ (* dummy value, it will be recomputed by cache_hintrewrite *) in
-    let t' = Tacinterp.subst_tactic subst t in
-      if cst == cst' && t == t' then pair else
-	(cst',typ',b,t')
-  in
-  let list' = list_smartmap subst_first list in
+  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
+
+let classify_hintrewrite x = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let (inHintRewrite,outHintRewrite)=
+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;
-       Libobject.export_function = export_hintrewrite }
+    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 true env Reduction.CONV x y evd); 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.rev_map
-    (fun (c,b,t) ->
-      (c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t)
-    ) lrul
-  in
-   Lib.add_anonymous_leaf (inHintRewrite (base,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))
+