Change implementation of resolution for typeclasses to use a customized

eauto instead of an arbitrary tactic. Export more from eauto to allow
easier debugging.


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

3 files changed, 191 insertions, 111 deletions

diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index b0a6b36c6d..84c1937ea8 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -99,14 +99,6 @@ let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
 
-let resolve_morphism_evd env evd app = 
-  let ev = Evarutil.e_new_evar evd env app in
-  let evd' = resolve_typeclasses ~check:true env (Evd.evars_of !evd) !evd in
-  let evm' = Evd.evars_of evd' in
-    match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with
-	Evd.Evar_empty -> raise Not_found
-      | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; Evarutil.nf_isevar !evd c
-
 let is_equiv env sigma t = 
   isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
 
@@ -139,7 +131,6 @@ let build_signature isevars env m cstrs finalcstr =
 		let rel = mk_relty t None in 
 		  rel, [t, rel]
 	    | Some (t, rel) -> rel, [t, rel])
-      | _, _ -> assert false
   in aux m cstrs
 
 let reflexivity_proof env evars carrier relation x =
@@ -174,31 +165,19 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
 	done;
 	!first
     in
-(*       try  *)
-	let morphargs, morphobjs = array_chop first args in
-	let morphargs', morphobjs' = array_chop first args' in
-	let appm = mkApp(m, morphargs) in
-	let appmtype = Typing.type_of env sigma appm in
-	let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
-	let cl_args = [| appmtype ; signature ; appm |] in
-	let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
-(* 	let morph = resolve_morphism_evd env evars app in *)
-	let morph = Evarutil.e_new_evar evars env app in
-(* 	let evm = Evd.evars_of !evars in *)
-(* 	let sigargs = List.map  *)
-(* 	  (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y)  *)
-(* 	  sigargs  *)
-(* 	in *)
-(* 	let appm = Reductionops.nf_evar evm appm in *)
-(* 	let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in *)
-	let proj = 
-	  mkApp (mkConst morphism_proj, 
-		Array.append cl_args [|morph|])
-	in
-	  morph, proj, sigargs, appm, morphobjs, morphobjs'
-(*       with Reduction.NotConvertible *)
-(* 	| Stdpp.Exc_located (_, Pretype_errors.PretypeError _)  *)
-(* 	| Pretype_errors.PretypeError _ -> raise Not_found *)
+    let morphargs, morphobjs = array_chop first args in
+    let morphargs', morphobjs' = array_chop first args' in
+    let appm = mkApp(m, morphargs) in
+    let appmtype = Typing.type_of env sigma appm in
+    let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
+    let cl_args = [| appmtype ; signature ; appm |] in
+    let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
+    let morph = Evarutil.e_new_evar evars env app in
+    let proj = 
+      mkApp (mkConst morphism_proj, 
+	    Array.append cl_args [|morph|])
+    in
+      morph, proj, sigargs, appm, morphobjs, morphobjs'
   in 
   let projargs, respars, typeargs = 
     array_fold_left2 
@@ -294,7 +273,7 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
     else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
 
 let resolve_all_typeclasses env evd = 
-  Eauto.resolve_all_evars env (fun x -> Typeclasses.class_of_constr x <> None) evd
+  Eauto.resolve_all_evars false (true, 15) env (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
     
 (* let _ =  *)
 (*   Typeclasses.solve_instanciation_problem := *)
@@ -319,9 +298,7 @@ let cl_rewrite_clause c left2right occs clause gl =
   let eq, _ = build_new gl env sigma occs origt newt hypt hypinfo concl (Some cstr) evars in
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
-(* 	  evars := Typeclasses.resolve_typeclasses ~check:false env (Evd.evars_of !evars) !evars; *)
-	  evars := Classes.resolve_all_typeclasses env !evars;
-(* 	  evars := resolve_all_typeclasses env !evars; *)
+	  evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars;
 	  evars := Evarutil.nf_evar_defs !evars;
 	  let p = Evarutil.nf_isevar !evars p in
 	  let newt = Evarutil.nf_isevar !evars newt in
@@ -335,11 +312,11 @@ let cl_rewrite_clause c left2right occs clause gl =
 		  refine term) gl
       | None -> tclIDTAC gl
 	  
+open Genarg
 open Extraargs
 
-
-
 TACTIC EXTEND class_rewrite
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ]
@@ -358,16 +335,68 @@ TACTIC EXTEND map_tac
 | [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
 END
 
+let pr_debug _prc _prlc _prt b =
+  if b then Pp.str "debug" else Pp.mt()
 
-(* 
-	  let proj = 
-	    if left2right then 
-	      let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
-	    else 
-	      let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
-	  in
-*)
+ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
+| [ "debug" ] -> [ true ]
+| [ ] -> [ false ]
+END
+
+let pr_mode _prc _prlc _prt m =
+  match m with
+      Some b ->
+	if b then Pp.str "depth-first" else Pp.str "breadth-fist" 
+    | None -> Pp.mt()
+	
+ARGUMENT EXTEND search_mode TYPED AS bool option PRINTED BY pr_mode
+| [ "dfs" ] -> [ Some true ]
+| [ "bfs" ] -> [ Some false ]
+| [] -> [ None ]
+END
+
+let pr_depth _prc _prlc _prt = function
+    Some i -> Util.pr_int i
+  | None -> Pp.mt()
+	
+ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
+| [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
+END
+
+let resolve_argument_typeclasses d p env evd onlyargs all =
+  let pred = 
+    if onlyargs then 
+      (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
+	class_of_constr evi.Evd.evar_concl <> None)
+    else
+      (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
+  in
+    try 
+      Eauto.resolve_all_evars d p env pred evd
+    with e -> 
+      if all then raise e else evd
+	
+VERNAC COMMAND EXTEND Typeclasses_Settings
+| [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ 
+    let mode = match s with Some t -> t | None -> true in
+    let depth = match depth with Some i -> i | None -> 15 in
+      Typeclasses.solve_instanciations_problem :=
+	resolve_argument_typeclasses d (mode, depth) ]
+END
+
+let _ = 
+  Typeclasses.solve_instanciations_problem :=
+    resolve_argument_typeclasses false (true, 15)
+      
+TACTIC EXTEND typeclasses_eauto
+| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl ->
+    let env = pf_env gl in
+    let sigma = project gl in
+      if Evd.dom sigma = [] then Refiner.tclIDTAC gl
+      else
+	let evd = Evd.create_evar_defs sigma in
+	let mode = match s with Some t -> t | None -> true in
+	let depth = match depth with Some i -> i | None -> 15 in
+	let evd' = resolve_argument_typeclasses d (mode, depth) env evd false false in
+	  Refiner.tclEVARS (Evd.evars_of evd') gl ]
+END
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c550dbb283..70ec9d046e 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -214,8 +214,9 @@ and e_trivial_resolve db_list local_db gl =
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd (e_my_find_search db_list local_db 
-		      (List.hd (head_constr_bound gl [])) gl)
+  try List.map snd 
+    (e_my_find_search db_list local_db 
+	(List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
 let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
@@ -226,15 +227,18 @@ let find_first_goal gls =
 (*s The following module [SearchProblem] is used to instantiate the generic
     exploration functor [Explore.Make]. *)
       
+
+type search_state = { 
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma * validation;
+  last_tactic : std_ppcmds;
+  dblist : Auto.Hint_db.t list;
+  localdb :  Auto.Hint_db.t list }
+    
 module SearchProblem = struct
+    
+  type state = search_state
 
-  type state = { 
-    depth : int; (*r depth of search before failing *)
-    tacres : goal list sigma * validation;
-    last_tactic : std_ppcmds;
-    dblist : Auto.Hint_db.t list;
-    localdb :  Auto.Hint_db.t list }
-		 
   let success s = (sig_it (fst s.tacres)) = []
 
   let rec filter_tactics (glls,v) = function
@@ -316,18 +320,18 @@ end
 module Search = Explore.Make(SearchProblem)
 
 let make_initial_state n gl dblist localdb =
-  { SearchProblem.depth = n;
-    SearchProblem.tacres = tclIDTAC gl;
-    SearchProblem.last_tactic = (mt ());
-    SearchProblem.dblist = dblist;
-    SearchProblem.localdb = [localdb] }
-
-let make_initial_state_gls n gls dblist localdb =
-  { SearchProblem.depth = n;
-    SearchProblem.tacres = gls;
-    SearchProblem.last_tactic = (mt ());
-    SearchProblem.dblist = dblist;
-    SearchProblem.localdb = [localdb] }
+  { depth = n;
+    tacres = tclIDTAC gl;
+    last_tactic = (mt ());
+    dblist = dblist;
+    localdb = [localdb] }
+
+let make_initial_state_gls n gls dblist localdbs =
+  { depth = n;
+    tacres = gls;
+    last_tactic = (mt ());
+    dblist = dblist;
+    localdb = localdbs }
 
 let debug_depth_first = Search.debug_depth_first
 
@@ -335,14 +339,14 @@ let e_depth_search debug p db_list local_db gl =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
     let s = tac (make_initial_state p gl db_list local_db) in
-    s.SearchProblem.tacres
+    s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
-let e_depth_search_gls debug p db_list local_db gls =
+let e_depth_search_gls debug p db_list local_dbs gls =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state_gls p gls db_list local_db) in
-    s.SearchProblem.tacres
+    let s = tac (make_initial_state_gls p gls db_list local_dbs) in
+    s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
 let e_breadth_search debug n db_list local_db gl =
@@ -351,16 +355,16 @@ let e_breadth_search debug n db_list local_db gl =
       if debug then Search.debug_breadth_first else Search.breadth_first 
     in
     let s = tac (make_initial_state n gl db_list local_db) in
-    s.SearchProblem.tacres
+    s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_breadth_search_gls debug n db_list local_db gls =
+let e_breadth_search_gls debug n db_list local_dbs gls =
   try
     let tac = 
       if debug then Search.debug_breadth_first else Search.breadth_first 
     in
-    let s = tac (make_initial_state_gls n gls db_list local_db) in
-    s.SearchProblem.tacres
+    let s = tac (make_initial_state_gls n gls db_list local_dbs) in
+    s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (in_depth,p) lems db_list gl = 
@@ -374,11 +378,11 @@ open Evd
 
 let e_search_auto_gls debug (in_depth,p) lems db_list gls = 
   let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
-  let local_db = make_local_hint_db lems ({it = List.hd gls'; sigma = sigma}) in
+  let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in
   if in_depth then 
-    e_depth_search_gls debug p db_list local_db gls
+    e_depth_search_gls debug p db_list local_dbs gls
   else
-    e_breadth_search_gls debug p db_list local_db gls
+    e_breadth_search_gls debug p db_list local_dbs gls
 
 let eauto debug np lems dbnames =
   let db_list =
@@ -470,33 +474,42 @@ open Evd
 
 exception Found of evar_defs
 
-let resolve_all_evars env p evd =
-  let evm = Evd.evars_of evd in
-  let goals, sigma = 
+let valid evm p res_sigma l = 
+  let evd' =
     Evd.fold
       (fun ev evi (gls, sigma) ->
-	if p evi.evar_concl then
-	  (evi :: gls, sigma)
-	else (gls, Evd.add sigma ev evi))
-      evm ([], Evd.empty)
-  in
-  let gls = { it = List.rev goals; sigma = sigma } in
-  let res_sigma = ref sigma in
-  let valid l = 
-    let evd' =
-      Evd.fold
-	(fun ev evi (gls, sigma) ->
-	  if p evi.evar_concl then
-	    match gls with
-		hd :: tl -> 
+	if not (Evd.is_evar evm ev) then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
 		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		  (tl, Evd.evar_define ev cstr sigma)
-	      | [] -> assert(false)
-	  else (gls, sigma))
-	evm (l, evd)
-    in raise (Found (snd evd'))
-  in
-  let gls', valid' = full_eauto_gls true (false, 10) [] (gls, valid) in
-    res_sigma := sig_sig gls';
-    try ignore(valid' []); assert(false) with Found evd' -> evd'
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> ([], sigma)
+	else if not (Evd.is_defined evm ev) && p ev evi then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
+		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> assert(false)
+	else (gls, sigma))
+      !res_sigma (l, Evd.create_evar_defs !res_sigma)
+  in raise (Found (snd evd'))
     
+let resolve_all_evars debug (mode, depth) env p evd =
+  let evm = Evd.evars_of evd in
+  let goals = 
+    Evd.fold
+      (fun ev evi gls ->
+	if evi.evar_body = Evar_empty && p ev evi then
+	  (evi :: gls)
+	else gls)
+      evm []
+  in
+  let gls = { it = List.rev goals; sigma = evm } in
+  let res_sigma = ref evm in
+  let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
+    res_sigma := Evarutil.nf_evars (sig_sig gls');
+    try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 34c4cab78b..940648c2eb 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -14,6 +14,7 @@ open Auto
 open Topconstr
 open Evd
 open Environ
+open Explore
 (*i*)
 
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
@@ -26,10 +27,47 @@ val registered_e_assumption : tactic
 
 val e_give_exact_constr : constr -> tactic
 
+type search_state = { 
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma * validation;
+  last_tactic : Pp.std_ppcmds;
+  dblist : Auto.Hint_db.t list;
+  localdb :  Auto.Hint_db.t list }
+
+module SearchProblem : sig
+  type state = search_state
+      
+  val filter_tactics :     Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a) ->
+    (Tacmach.tactic * Pp.std_ppcmds) list ->
+    ((Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a)) *
+     Pp.std_ppcmds)
+    list
+
+  val compare :  search_state -> search_state -> int
+
+  val branching : state -> state list
+  val success : state -> bool
+  val pp : state -> unit
+end
+
+module Search : sig
+  val depth_first : search_state -> search_state
+  val debug_depth_first : search_state -> search_state
+
+  val breadth_first : search_state -> search_state
+  val debug_breadth_first : search_state -> search_state
+end
+
 val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> 
   goal list sigma * validation
 
-val resolve_all_evars : env -> (constr -> bool) -> evar_defs -> evar_defs
+val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
+  evar_defs
+
+val valid :     Evd.evar_map ->
+    (Evd.evar -> Evd.evar_info -> bool) ->
+    Evd.evar_map ref -> Proof_type.proof_tree list -> 'a
+
 
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic