New algorithm to resolve morphisms, after discussion with Nicolas

Tabareau: 
- first pass: generation of the Morphism constraints with metavariables
  for unspecified relations by one fold over the term. 
  This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
  solution for all the evars at once. 
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.

Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.


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

2 files changed, 59 insertions, 0 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d84fb3e561..92a5dfc8b7 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -492,3 +492,60 @@ let _ =
     (fun env evd ev evi -> 
       Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
       solve_by_tac env evd ev evi (Lazy.force tactic))
+
+let prod = lazy (Coqlib.build_prod ())
+
+let build_conjunction evm =
+  List.fold_left
+    (fun (acc, evs) (ev, evi)  ->
+      if class_of_constr evi.evar_concl <> None then
+	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs
+      else acc, Evd.add evs ev evi)
+    (Coqlib.build_coq_True (), Evd.empty) evm
+
+let destruct_conjunction evm_list evm evm' term =
+  let _, evm =
+    List.fold_right
+      (fun (ev, evi) (term, evs) ->
+	if class_of_constr evi.evar_concl <> None then
+	  match kind_of_term term with
+	    | App (x, [| _ ; _ ; proof ; term |]) ->
+		let evs' = Evd.define evs ev proof in
+		  (term, evs')
+	    | _ -> assert(false)
+	else
+	  match (Evd.find evm' ev).evar_body with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c ->
+		let evs' = Evd.define evs ev c in
+		  (term, evs'))
+      evm_list (term, evm)
+  in evm
+ 
+(* let solve_by_tac env evd evar evi t = *)
+(*   let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
+(*   let (res, valid) = t goal in *)
+(*     if res.it = [] then *)
+(*       let prooftree = valid [] in *)
+(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
+(* 	if obls = [] then *)
+(* 	  let evd' = evars_reset_evd res.sigma evd in *)
+(* 	  let evd' = evar_define evar proofterm evd' in *)
+(* 	    evd', true *)
+(* 	else evd, false *)
+(*     else evd, false *)
+
+let resolve_all_typeclasses env evd =
+  let evm = Evd.evars_of evd in
+  let evm_list = Evd.to_list evm in
+  let goal, typesevm = build_conjunction evm_list in
+  let evars = ref (Evd.create_evar_defs typesevm) in
+  let term = resolve_one_typeclass_evd env evars goal in
+  let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in
+    Evd.create_evar_defs evm'
+
+let _ =
+  Typeclasses.solve_instanciations_problem :=
+    (fun env evd -> 
+      Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
+      resolve_all_typeclasses env evd)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 93fc1b552c..cfe881cb31 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -69,3 +69,5 @@ val push_named_context : named_context -> env -> env
 val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
+
+val resolve_all_typeclasses : env -> evar_defs -> evar_defs