From 730836f5f680a068633a202de18a4b586157a85c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 6 Feb 2008 14:59:08 +0000
Subject: 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
---
 pretyping/typeclasses.ml  | 11 +++++++----
 pretyping/typeclasses.mli |  1 +
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index febfb04947..f9ab283ada 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,6 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types =
 	let evm' = Evd.evars_of evd' in
 	  match Evd.evar_body (Evd.find evm' ev) with
 	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
+	    | Evar_defined c -> Evarutil.nf_evar evm' c
       else raise Not_found
   with Exit -> raise Not_found
 
@@ -278,6 +279,8 @@ let destClassApp c =
     | _ -> None
 
 let resolve_typeclasses ?(check=true) env sigma evd =
+(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
+(*   with _ -> *)
   let evm = Evd.evars_of evd in
   let tc_evars = 
     let f ev evi acc =
@@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
 	(fun ev evi acc -> 
 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
 	    resolve_typeclass env ev evi acc 
-	  else acc) 
+	  else acc)
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
       else
 	sat (Evarutil.nf_evar_defs evars')
-  in sat evd
-
+  in sat (Evarutil.nf_evar_defs evd)
+  
 let class_of_constr c = 
   let extract_ind c =
     match kind_of_term c with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ec3350a586..db408c8898 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -64,6 +64,7 @@ val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_def
 val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
+val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref
 
 type substitution = (identifier * constr) list
 
-- 
cgit v1.2.3