Fix eauto still using delta when it shouldn't (should make CoRN compile

in reasonable time), add (unfinished) documentation on type classes.
Put some classes into Prop explicitely as singleton inductive types are
no longer in Prop by default even if all the arguments are (is that
really what we want? roconnor says no).


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

3 files changed, 107 insertions, 31 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 816bd61ca0..2c327b71ba 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -591,11 +591,17 @@ let auto_unif_flags = {
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
+let unify_resolve_nodelta (c,clenv) gls = 
+  let clenv' = connect_clenv gls clenv in
+  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in  
+  h_simplest_apply c gls
+
 let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false ~flags clenv' gls in  
   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> *)
 
@@ -648,33 +654,54 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
      (List.map tclCOMPLETE 
        (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
-and my_find_search mod_delta db_list local_db hdc concl =
-  let flags = 
-    if mod_delta then {auto_unif_flags with use_metas_eagerly = true}
-    else auto_unif_flags
+and my_find_search_nodelta db_list local_db hdc concl =
+  let tacl = 
+    if occur_existential concl then 
+      list_map_append
+	(fun (st, db) -> (Hint_db.map_all hdc db))
+	(local_db::db_list)
+    else
+      list_map_append (fun (_, db) -> 
+	Hint_db.map_auto (hdc,concl) db)
+      	(local_db::db_list)
   in
+    List.map 
+      (fun {pri=b; pat=p; code=t} -> 
+	(b,
+	match t with
+	  | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
+	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
+	  | Give_exact c  -> exact_check c
+	  | Res_pf_THEN_trivial_fail (term,cl) -> 
+	      tclTHEN 
+		(unify_resolve_nodelta (term,cl)) 
+		(trivial_fail_db false db_list local_db)
+	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Extern tacast -> 
+	      conclPattern concl (Option.get p) tacast))
+    tacl
+
+and my_find_search mod_delta =
+  if mod_delta then my_find_search_delta
+  else my_find_search_nodelta
+    
+and my_find_search_delta db_list local_db hdc concl =
+  let flags = {auto_unif_flags with use_metas_eagerly = true} in
   let tacl = 
     if occur_existential concl then 
       list_map_append
 	(fun (st, db) -> 
-	  let st = 
-	    if mod_delta then
-	      {flags with modulo_delta = st} 
-	    else flags 
-	  in
+	  let st = {flags with modulo_delta = st} in
 	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else
       list_map_append (fun ((ids, csts as st), db) -> 
 	let st, l = 
-	  if not mod_delta then
-	    flags, Hint_db.map_auto (hdc,concl) db
-	  else 
-	    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 {flags with modulo_delta = st}, l
+	  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 {flags with modulo_delta = st}, l
 	in List.map (fun x -> (st,x)) l)
       	(local_db::db_list)
   in
@@ -682,18 +709,18 @@ and my_find_search mod_delta db_list local_db hdc concl =
       (fun (st, {pri=b; pat=p; code=t}) -> 
 	(b,
 	match t with
-	  | Res_pf (term,cl)  -> unify_resolve st (term,cl)
+	  | Res_pf (term,cl) -> unify_resolve st (term,cl)
 	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
 	  | Give_exact c  -> exact_check c
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
 		(unify_resolve st (term,cl)) 
-		(trivial_fail_db mod_delta db_list local_db)
+		(trivial_fail_db true db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
 	      conclPattern concl (Option.get p) tacast))
-    tacl
-
+      tacl
+      
 and trivial_resolve mod_delta db_list local_db cl = 
   try 
     let hdconstr = List.hd (head_constr_bound cl []) in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 7853235be0..5b151162c4 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -141,6 +141,8 @@ val default_search_depth : int ref
 val auto_unif_flags : Unification.unify_flags
 
 (* Try unification with the precompiled clause, then use registered Apply *)
+val unify_resolve_nodelta : (constr * clausenv) -> tactic
+
 val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 3894dfd1f7..e6172d3df1 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -91,25 +91,72 @@ open Unification
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
+(* no delta yet *)
+
 let unify_e_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false ~flags clenv' gls in
   h_simplest_eapply c gls
 
-let rec e_trivial_fail_db db_list local_db goal =
+let unify_e_resolve_nodelta (c,clenv) gls = 
+  let clenv' = connect_clenv gls clenv in
+  let _ = clenv_unique_resolver false clenv' gls in
+  h_simplest_eapply c gls
+
+let rec e_trivial_fail_db mod_delta db_list local_db goal =
   let tacl = 
     registered_e_assumption ::
     (tclTHEN Tactics.intro 
        (function g'->
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
-          (e_trivial_fail_db db_list
+          (e_trivial_fail_db mod_delta db_list
 	     (add_hint_list hintl local_db) g'))) ::
-    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+    (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
-and e_my_find_search db_list local_db hdc concl = 
+and e_my_find_search mod_delta =
+  if mod_delta then e_my_find_search_delta
+  else e_my_find_search_nodelta
+
+and e_my_find_search_nodelta db_list local_db hdc concl = 
+  let hdc = head_of_constr_reference hdc in
+  let hintl =
+    if occur_existential concl then 
+      list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list)
+    else 
+      list_map_append (fun (st, db) -> 
+	Hint_db.map_auto (hdc,concl) db) (local_db::db_list)
+  in 
+  let tac_of_hint = 
+    fun {pri=b; pat = p; code=t} -> 
+      (b, 
+       let tac =
+	 match t with
+	   | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl)
+	   | Give_exact (c) -> e_give_exact_constr c
+	   | Res_pf_THEN_trivial_fail (term,cl) ->
+               tclTHEN (unify_e_resolve_nodelta (term,cl)) 
+		 (e_trivial_fail_db false db_list local_db)
+	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Extern tacast -> conclPattern concl 
+	       (Option.get p) tacast
+       in 
+       (tac,fmt_autotactic t))
+       (*i
+	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+                     try tac gls
+		     with e when Logic.catchable_exception(e) -> 
+                            (Format.print_string "Fail\n"; 
+			     Format.print_flush (); 
+			     raise e)
+       i*)
+  in 
+  List.map tac_of_hint hintl
+
+and e_my_find_search_delta db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then 
@@ -131,7 +178,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Give_exact (c) -> e_give_exact_constr c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl)) 
-		 (e_trivial_fail_db db_list local_db)
+		 (e_trivial_fail_db true db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [[],c]
 	   | Extern tacast -> conclPattern concl 
 	       (Option.get p) tacast
@@ -148,16 +195,16 @@ and e_my_find_search db_list local_db hdc concl =
   in 
   List.map tac_of_hint hintl
     
-and e_trivial_resolve db_list local_db gl = 
+and e_trivial_resolve mod_delta db_list local_db gl = 
   try 
     Auto.priority 
-      (e_my_find_search db_list local_db 
+      (e_my_find_search mod_delta db_list local_db 
 	 (List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
-let e_possible_resolve db_list local_db gl =
+let e_possible_resolve mod_delta db_list local_db gl =
   try List.map snd 
-    (e_my_find_search db_list local_db 
+    (e_my_find_search mod_delta db_list local_db 
 	(List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
@@ -248,7 +295,7 @@ module SearchProblem = struct
       in
       let rec_tacs = 
 	let l = 
-	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	  filter_tactics s.tacres (e_possible_resolve false s.dblist (List.hd s.localdb) (pf_concl g))
 	in
 	List.map 
 	  (fun ((lgls,_) as res, pp) ->