- Add pretty-printers for Idpred, Cpred and transparent_state, used for

  debugging and printing hint databases
- Typeclasses unfold now correctly adds _global_ unfold hints.
- New tactic autosimpl to do simplification using the declared unfold
  hints in given hint databases.
- Work on auto-modulo-some-delta (the declared Unfold constants),
  actually used mostly if the goal contains evars, as Hint_db.map_auto
  does not work up-to any conversions (yet).
- Fix GenMul which was using the old semantics of failing early because
  of variance checks, which is not possible in the new implementation.
- Restrict when reflexive_morphism may be used using an extern tactic.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 36 insertions, 8 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2709502c6..66fde8f6b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -543,7 +543,10 @@ let print_applicable_hint () =
   print_hint_term (pf_concl gl)
     
 (* displays the whole hint database db *)
-let print_hint_db db =
+let print_hint_db ((ids, csts),db) =
+  msg (hov 0
+	  (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
+	   str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
   Hint_db.iter 
     (fun head hintlist ->
        msg (hov 0 
@@ -553,14 +556,14 @@ let print_hint_db db =
 
 let print_hint_db_by_name dbname =
   try 
-    let db = snd (searchtable_map dbname) in print_hint_db db
+    let db = searchtable_map dbname in print_hint_db db
   with Not_found -> 
     error (dbname^" : No such Hint database")
   
 (* displays all the hints of all databases *)
 let print_searchtable () =
   Hintdbmap.iter
-    (fun name (_, db) ->
+    (fun name db ->
        msg (str "In the database " ++ str name ++ fnl ());
        print_hint_db db)
     !searchtable
@@ -591,7 +594,7 @@ let auto_unif_flags = {
 let unify_resolve st (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in  
-  h_simplest_apply c gls
+  h_apply true false (c,NoBindings) gls
 
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
@@ -633,6 +636,9 @@ let conclPattern concl pat tac gl =
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
   de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
+let transparent_state_union (xids, xcsts) (yids, ycsts) = 
+  (Idpred.union xids yids, Cpred.union xcsts ycsts)
+
 let rec trivial_fail_db db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
@@ -649,11 +655,16 @@ and my_find_search db_list local_db hdc concl =
   let tacl = 
     if occur_existential concl then 
       list_map_append
-	(fun (st, db) -> List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+	(fun (st, db) -> 
+	  List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> 
-	List.map (fun x -> (st,x)) (Hint_db.map_auto (hdc,concl) db))
+      list_map_append (fun ((ids, csts as st), db) -> 
+	let l = 
+(* 	  if Idpred.is_empty ids && Cpred.is_empty csts *)
+(* 	  then  *)Hint_db.map_auto (hdc,concl) db
+(* 	  else Hint_db.map_all hdc db *)
+	in List.map (fun x -> (st,x)) l)
       	(local_db::db_list)
   in
     List.map 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b79c24df2..d6de5e69d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -414,7 +414,7 @@ let resolve_all_evars debug m env p oevd =
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "unfold" reference_list(cl) ] -> [
-    add_hints true ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
+    add_hints false ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
   ]
 END
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0facf2393..03b29d523 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -384,3 +384,20 @@ TACTIC EXTEND dfs_eauto
       hintbases(db) ] ->
     [ gen_eauto false (true, make_depth p) lems db ]
 END
+
+let autosimpl db cl =
+  let unfold_of_elts constr (b, elts) =
+    if not b then 
+      List.map (fun c -> [], constr c) elts
+    else []
+  in
+  let unfolds = List.concat (List.map (fun dbname -> 
+    let ((ids, csts), _) = searchtable_map dbname in
+      unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
+      unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
+  in unfold_option unfolds cl
+
+TACTIC EXTEND autosimpl
+| [ "autosimpl" hintbases(db) ] ->
+    [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
+END