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

1 files changed, 24 insertions, 17 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index dba60234bc..193f3ae3c2 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 *)
+