Do another pass on the typeclasses code. Correct globalization of class

names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code. 
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class. 
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].


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

6 files changed, 118 insertions, 98 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 3406d06aa..0d462f793 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -141,13 +141,16 @@ let clenv_conv_leq env sigma t c bound =
   check_evars env sigma evars (applist (c,args));
   args
 
-let mk_clenv_from_n gls n (c,cty) =
-  let evd = create_goal_evar_defs gls.sigma in
+let mk_clenv_from_env environ sigma n (c,cty) =
+  let evd = create_goal_evar_defs sigma in
   let (env,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     evd = env;
-    env = Global.env_of_context gls.it.evar_hyps }
+    env = environ }
+
+let mk_clenv_from_n gls n (c,cty) =
+  mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 1697bb3c2..6a7038a07 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -54,6 +54,7 @@ val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_from_n :
   evar_info sigma -> int option -> constr * types -> clausenv
 val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
 (***************************************************************)
 (* linking of clenvs *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 47be84460..9d837df0e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,22 +30,22 @@ type rels = constr list
 
 (* This module defines type-classes *)
 type typeclass = {
-  (* Name of the class. FIXME: should not necessarily be globally unique. *)
-  cl_name : identifier;
+  (* The class implementation *)
+  cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : ((identifier * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * named_declaration) list; 
 
   cl_params: int;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : named_context;
-
-  (* The class implementation: a record parameterized by the context with defs in it. *)
-  cl_impl : inductive; 
+  
+  (* The method implementaions as projections. *)
+  cl_projs : constant list;
 }
 
-type typeclasses = (identifier, typeclass) Gmap.t
+type typeclasses = (global_reference, typeclass) Gmap.t
 
 type instance = {
   is_class: typeclass;
@@ -53,11 +53,11 @@ type instance = {
   is_impl: constant; 
 }
 
-type instances = (identifier, instance list) Gmap.t
+type instances = (global_reference, instance list) Gmap.t
     
 let classes : typeclasses ref = ref Gmap.empty
 
-let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty
+let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty
   
 let instances : instances ref = ref Gmap.empty
   
@@ -124,47 +124,64 @@ open Libobject
 let subst (_,subst,(cl,m,inst)) = 
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst c = Mod_subst.subst_mps subst c
-  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+  and do_subst_gr gr = fst (subst_global subst gr)
   in
   let do_subst_named ctx = 
-    List.map (fun (na, b, t) ->
+    list_smartmap (fun (na, b, t) ->
       (na, Option.smartmap do_subst b, do_subst t))
       ctx
   in
   let do_subst_ctx ctx = 
-    List.map (fun (cl, (na, b, t)) ->
-      (cl, (na, Option.smartmap do_subst b, do_subst t)))
+    list_smartmap (fun (cl, (na, b, t)) ->
+      (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl,
+      (na, Option.smartmap do_subst b, do_subst t)))
       ctx
   in
-  let subst_class cl = 
-    let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl;
+  let do_subst_projs projs = list_smartmap do_subst_con projs in
+  let subst_class k cl classes = 
+    let k = do_subst_gr k in
+    let cl' = { cl with cl_impl = k;
 		cl_context = do_subst_ctx cl.cl_context;
-		cl_props = do_subst_named cl.cl_props; }
-    in if cl' = cl then cl else cl'
+		cl_props = do_subst_named cl.cl_props;
+		cl_projs = do_subst_projs cl.cl_projs; }
+    in 
+    let cl' = if cl' = cl then cl else cl' in
+      Gmap.add k cl' classes
   in
-  let subst_inst classes insts =
-    List.map (fun is -> 
-      let is' = 
-	{ is_class = Gmap.find is.is_class.cl_name classes; 
-	  is_pri = is.is_pri;
-	  is_impl = do_subst_con is.is_impl }
-      in if is' = is then is else is') insts
+  let classes = Gmap.fold subst_class cl Gmap.empty in
+  let subst_inst k insts instances =
+    let k = do_subst_gr k in
+    let cl = Gmap.find k classes in
+    let insts' = 
+      list_smartmap (fun is -> 
+	let is' = 
+	  { is_class = cl; 
+	    is_pri = is.is_pri;
+	    is_impl = do_subst_con is.is_impl }
+	in if is' = is then is else is') insts
+    in  Gmap.add k insts' instances
   in
-  let classes = Gmap.map subst_class cl in
-  let instances = Gmap.map (subst_inst classes) inst in
+  let instances = Gmap.fold subst_inst inst Gmap.empty in
     (classes, m, instances)
 
 let discharge (_,(cl,m,inst)) =
-  let subst_class cl = 
-    { cl with cl_impl = Lib.discharge_inductive cl.cl_impl }
+  let discharge_named (cl, r) =
+    Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r
   in
-  let subst_inst classes insts =
-    List.map (fun is -> { is_impl = Lib.discharge_con is.is_impl;
-			  is_pri = is.is_pri;
-			  is_class = Gmap.find is.is_class.cl_name classes; }) insts
+  let subst_class cl = 
+    { cl with cl_impl = Lib.discharge_global cl.cl_impl;
+      cl_context = list_smartmap discharge_named cl.cl_context;
+      cl_projs = list_smartmap Lib.discharge_con cl.cl_projs }
   in
   let classes = Gmap.map subst_class cl in
-  let instances = Gmap.map (subst_inst classes) inst in
+  let subst_inst insts =
+    List.map (fun is ->
+      { is_impl = Lib.discharge_con is.is_impl;
+	is_pri = is.is_pri;
+	is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; })
+      insts
+  in
+  let instances = Gmap.map subst_inst inst in
     Some (classes, m, instances)
   
 let (input,output) = 
@@ -181,24 +198,20 @@ let (input,output) =
 let update () = 
   Lib.add_anonymous_leaf (input (!classes, !methods, !instances))
 
-let class_methods cl =
-  List.map (function (x, _, _) -> x) cl.cl_props
-
 let add_class c = 
-  classes := Gmap.add c.cl_name c !classes;
-  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c);
+  classes := Gmap.add c.cl_impl c !classes;
+  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_impl acc) !methods c.cl_projs;
   update ()
     
 let class_info c = 
-  Gmap.find c !classes
+  try Gmap.find c !classes
+  with _ -> not_a_class (Global.env()) (constr_of_global c)
 
-let class_of_inductive ind = 
-  let res = Gmap.fold 
-    (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc)
-    !classes None
-  in match res with
-      None -> raise Not_found
-    | Some cl -> cl
+let instance_constructor cl = 
+  match cl.cl_impl with
+    | IndRef ind -> (fun args -> applistc (mkConstruct (ind, 1)) args), mkInd ind
+    | ConstRef cst -> list_last, mkConst cst
+    | _ -> assert false
 
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
 
@@ -210,25 +223,16 @@ let gmapl_add x y m =
     Gmap.add x [y] m
 
 let instances_of c = 
-  try Gmap.find c.cl_name !instances with Not_found -> []
+  try Gmap.find c.cl_impl !instances with Not_found -> []
 
 let add_instance i =
-  try
-    let cl = Gmap.find i.is_class.cl_name !classes in
-      instances := gmapl_add cl.cl_name { i with is_class = cl } !instances;
-      add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
-      update ()
-  with Not_found -> unbound_class (Global.env ()) (dummy_loc, i.is_class.cl_name)
-
-open Libnames
-      
-let id_of_reference r = 
-  let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id
+  let cl = Gmap.find i.is_class.cl_impl !classes in
+    instances := gmapl_add cl.cl_impl { i with is_class = cl } !instances;
+    add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
+    update ()
 
 let instances r = 
-  let id = id_of_reference r in
-    try let cl = class_info id in instances_of cl
-    with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
+  let cl = class_info r in instances_of cl
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
 let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false)
@@ -273,12 +277,11 @@ let resolve_one_typeclass_evd env evd types =
 let method_typeclass ref = 
   match ref with 
     | ConstRef c -> 
-	let (_, _, l) = Names.repr_con c in
-	  class_info (Gmap.find (Names.id_of_label l) !methods)
+	class_info (Gmap.find c !methods)
     | _ -> raise Not_found
       
-let is_class ind = 
-  Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false
+let is_class gr = 
+  Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
   
 let is_implicit_arg k = 
   match k with
@@ -332,14 +335,18 @@ let is_independent evm ev =
 (*   in sat (Evarutil.nf_evar_defs evd) *)
   
 let class_of_constr c = 
-  let extract_ind c =
-    match kind_of_term c with
-	Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
-      | _ -> None
+  let extract_cl c =
+    try Some (class_info (global_of_constr c)) with _ -> None
   in
     match kind_of_term c with
-	App (c, _) -> extract_ind c
-      | _ -> extract_ind c
+	App (c, _) -> extract_cl c
+      | _ -> extract_cl c
+
+let dest_class_app c =
+  let cl c = class_info (global_of_constr c) in
+    match kind_of_term c with
+	App (c, args) -> cl c, args
+      | _ -> cl c, [||]
 
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index dba60234b..193f3ae3c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -24,20 +24,21 @@ open Util
 
 (* This module defines type-classes *)
 type typeclass = {
-  (* Name of the class. FIXME: should not necessarily be globally unique. *)
-  cl_name : identifier;
+  (* The class implementation: a record parameterized by the context with defs in it or a definition if 
+     the class is a singleton. This acts as the classe's global identifier. *)
+  cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the 
      typeclass argument is a direct superclass. *)
-  cl_context : ((identifier * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * named_declaration) list; 
 
   cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : named_context;
 
-  (* The class implementation: a record parameterized by the context with defs in it. *)
-  cl_impl : inductive; 
+  (* The methods implementations of the typeclass as projections. *)
+  cl_projs : constant list;
 }
 
 type instance = {
@@ -46,7 +47,7 @@ type instance = {
   is_impl: constant;
 }
   
-val instances : Libnames.reference -> instance list
+val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list
 val add_class : typeclass -> unit
 val add_instance : instance -> unit
@@ -54,16 +55,16 @@ val add_instance : instance -> unit
 val register_add_instance_hint : (reference -> int option -> unit) -> unit
 val add_instance_hint : reference -> int option -> unit
 
-val class_info : identifier -> typeclass (* raises Not_found *)
-val class_of_inductive : inductive -> typeclass (* raises Not_found *)
+val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
+val is_class : global_reference -> bool
+val class_of_constr : constr -> typeclass option
+val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
+
+(* Returns the constructor for the given fields of the class and the type constructor. *)
+val instance_constructor : typeclass -> (constr list -> constr) * types
 
 val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
 val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
-
-val is_class : inductive -> bool
-
-val class_of_constr : constr -> typeclass option
-
 val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
 
 (* Use evar_extra for marking resolvable evars. *)
@@ -88,9 +89,15 @@ val nf_substitution : evar_map -> substitution -> substitution
 
 val is_implicit_arg : hole_kind -> bool
 
+val qualid_of_con : Names.constant -> Libnames.reference
 
-val subst :  'a * Mod_subst.substitution *
-    ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) ->
-    (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t
 
-val qualid_of_con : Names.constant -> Libnames.reference
+(* debug *)
+
+(* val subst :  *)
+(*     'a * Mod_subst.substitution * *)
+(*     ((Libnames.global_reference, typeclass) Gmap.t * 'b * *)
+(*      ('c, instance list) Gmap.t) -> *)
+(*     (Libnames.global_reference, typeclass) Gmap.t * 'b * *)
+(*     ('c, instance list) Gmap.t *)
+
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 980f327cb..1648f667a 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -19,13 +19,14 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
+open Libnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | UnboundClass of identifier located
-    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NotAClass of constr
+    | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
@@ -33,7 +34,7 @@ exception TypeClassError of env * typeclass_error
 
 let typeclass_error env err = raise (TypeClassError (env, err))
 
-let unbound_class env id = typeclass_error env (UnboundClass id)
+let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fbc2f2544..82e37f41d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -19,21 +19,22 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
+open Libnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | UnboundClass of identifier located
-    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NotAClass of constr
+    | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
-val unbound_class : env -> identifier located -> 'a
+val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> identifier -> identifier located -> 'a
+val unbound_method : env -> global_reference -> identifier located -> 'a
 
 val no_instance : env -> identifier located -> constr list -> 'a