Keep information on which fields are subclasses in class declarations,

in preparation for adding forward reasoning to typeclass resolution.


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

2 files changed, 12 insertions, 8 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 12cccdf0c3..cca7aee1d8 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -51,7 +51,7 @@ type typeclass = {
   cl_props : rel_context;
 
   (* The method implementaions as projections. *)
-  cl_projs : (name * constant option) list;
+  cl_projs : (name * bool * constant option) list;
 }
 module Gmap = Fmap.Make(RefOrdered)
 
@@ -117,7 +117,11 @@ let dest_class_app env c =
   let cl, args = decompose_app c in
     global_class_of_constr env cl, args
 
-let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
+let dest_class_arity env c =
+  let rels, c = decompose_prod_assum c in
+    rels, dest_class_app env c
+
+let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
 
 let rec is_class_type evd c =
   match kind_of_term c with
@@ -147,7 +151,7 @@ let subst_class (subst,cl) =
   let do_subst_context (grs,ctx) =
     list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
     do_subst_ctx ctx in
-  let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in
+  let do_subst_projs projs = list_smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
   { cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
@@ -179,7 +183,7 @@ let discharge_class (_,cl) =
       let newgrs = List.map (fun (_, _, t) -> 
 	match class_of_constr t with
 	| None -> None
-	| Some tc -> Some (tc.cl_impl, true))
+	| Some (_, (tc, _)) -> Some (tc.cl_impl, true))
 	ctx' 
       in
 	list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
@@ -194,7 +198,7 @@ let discharge_class (_,cl) =
     { cl_impl = cl_impl';
       cl_context = context;
       cl_props = props;
-      cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
+      cl_projs = list_smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
 
 let rebuild_class cl = cl
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3fa1981a3c..1fe955b0c0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -34,8 +34,8 @@ type typeclass = {
 
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if 
-      no name is provided. *)
-  cl_projs : (name * constant option) list;
+      no name is provided. The boolean indicates subclasses. *)
+  cl_projs : (name * bool * constant option) list;
 }
 
 type instance
@@ -61,7 +61,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 val dest_class_app : env -> constr -> typeclass * constr list
 
 (** Just return None if not a class *)
-val class_of_constr : constr -> typeclass option
+val class_of_constr : constr -> (rel_context * (typeclass * constr list)) option
   
 val instance_impl : instance -> global_reference