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

7 files changed, 68 insertions, 40 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 38f13a76e6..419205a198 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -134,8 +134,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		  let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
 		  let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
 		  let (loc, mid) = get_id loc_mid in
-		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) 
-		      (List.assoc (Name mid) k.cl_projs);
+		    List.iter 
+		      (fun (n, _, x) -> 
+			 if n = Name mid then
+			   Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+		      k.cl_projs;
 		    c :: props, rest'
 		with Not_found ->
 		  (CHole (Util.dummy_loc, None) :: props), rest
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
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index e3435191bf..df79bf3eef 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -59,7 +59,7 @@ let proper_class =
 let proper_proxy_class =
   lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy"))))
 
-let proper_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force proper_class).cl_projs))))
+let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
@@ -1387,20 +1387,6 @@ TACTIC EXTEND setoid_rewrite
       [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
 END
 
-(* let occurrences_of l = (true,[]) *)
-
-(* VERNAC COMMAND EXTEND GenRew *)
-(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> *)
-(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ] *)
-(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> *)
-(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ] *)
-(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> *)
-(*     [ cl_rewrite_clause_newtac' c o all_occurrences (Some (snd id)) ] *)
-(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> *)
-(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) None ] *)
-(* | [ "rew" orient(o) glob_constr_with_bindings(c) ] -> [ cl_rewrite_clause_newtac' c o all_occurrences None ] *)
-(* END *)
-
 let cl_rewrite_clause_newtac_tac c o occ cl gl =
   cl_rewrite_clause_newtac' c o occ cl;
   tclIDTAC gl
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 34b023d6f0..2f0bb480f2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -55,7 +55,7 @@ let declare_instance glob g =
   let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some tc -> add_instance (new_instance tc None glob c)
+      | Some (_, (tc, _)) -> add_instance (new_instance tc None glob c)
       | None -> user_err_loc (loc_of_reference g, "declare_instance",
 			     Pp.str "Constant does not build instances of a declared type class.")
 
@@ -211,8 +211,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
 			let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
 			let (loc, mid) = get_id loc_mid in
-			  Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) 
-			    (List.assoc (Name mid) k.cl_projs);
+			  List.iter (fun (n, _, x) -> 
+				       if n = Name mid then
+					 Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+			    k.cl_projs;
 			  c :: props, rest'
 		      with Not_found ->
 			(CHole (Util.dummy_loc, None) :: props), rest
@@ -273,7 +275,41 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context ?(hook=fun _ -> ()) l =
+let string_of_global r =
+ string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
+
+let rec declare_subclasses gr (rels, (tc, args)) =
+  let projs = list_map_filter 
+    (fun (n, b, proj) ->
+       if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
+       else None) tc.cl_projs 
+  in
+  let instapp = appvectc (constr_of_global gr)
+    (Termops.extended_rel_vect 0 rels)
+  in
+  let projargs = 
+    Array.of_list (args @ [instapp])
+  in
+  let declare_proj (n, p) =
+    let ce = {
+      const_entry_body   = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels;
+      const_entry_type   = None;
+      const_entry_opaque = false }
+    in
+    let cst = Declare.declare_constant ~internal:Declare.KernelSilent 
+      (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_") 
+	 (string_of_id n))
+      (DefinitionEntry ce, IsAssumption Logical)
+    in
+    let ty = Typeops.type_of_constant (Global.env ()) cst in
+      match class_of_constr ty with
+      | Some (rels, (tc, args) as cl) ->
+	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
+	  declare_subclasses (ConstRef cst) cl
+      | None -> ()
+  in () (* List.iter declare_proj projs *)
+
+let context l =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let _, ((env', fullctx), impls) = interp_context_evars evars env l in
@@ -289,9 +325,9 @@ let context ?(hook=fun _ -> ()) l =
 	(ParameterEntry (t,None), IsAssumption Logical)
       in
 	match class_of_constr t with
-	| Some tc ->
+	| Some (rels, (tc, args) as cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
-	    hook (ConstRef cst)
+	    declare_subclasses (ConstRef cst) cl
 	| None -> ()
     else (
       let impl = List.exists 
@@ -302,6 +338,6 @@ let context ?(hook=fun _ -> ()) l =
 	  [] impl (* implicit *) None (* inline *) (dummy_loc, id);
 	match class_of_constr t with
 	| None -> ()
-	| Some tc -> hook (VarRef id))
+	| Some tc -> declare_subclasses (VarRef id) tc)
   in List.iter fn (List.rev ctx)
 	
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 95f731ce2a..bc0eb89c08 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -67,8 +67,7 @@ val id_of_class : typeclass -> identifier
 
 (** Context command *)
 
-val context : ?hook:(Libnames.global_reference -> unit) ->
-  local_binder list -> unit
+val context : local_binder list -> unit
 
 (** Forward ref for refine *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0255e6504d..ae09d080f3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -291,7 +291,7 @@ let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some tc -> add_instance (new_instance tc None glob (ConstRef con))
+      | Some (_, (tc, _)) -> add_instance (new_instance tc None glob (ConstRef con))
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
 let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
@@ -331,20 +331,20 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
 	Classes.set_typeclass_transparency (EvalConstRef cst) false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
-	cref, [Name proj_name, Some proj_cst]
+	cref, [Name proj_name, List.hd coers, Some proj_cst]
     | _ ->
 	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
 	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (Termops.new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
-	  IndRef ind, (List.map2 (fun (id, _, _) y -> (id, y))
-			 (List.rev fields) (Recordops.lookup_projections ind))
+	  IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y))
+			 (List.rev fields) coers (Recordops.lookup_projections ind))
   in
   let ctx_context =
     List.map (fun (na, b, t) ->
       match Typeclasses.class_of_constr t with
-      | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+      | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
       | None -> None)
       params, params
   in
@@ -355,7 +355,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
       cl_projs = projs }
   in
     List.iter2 (fun p sub ->
-      if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
+      if sub then match p with (_, _, Some p) -> declare_instance_cst true p | _ -> ())
       k.cl_projs coers;
   add_class k; impl