Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 39 insertions, 24 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 83ae84a5..74ccaf83 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Libnames
 open Decl_kinds
@@ -20,25 +17,28 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
-(*i*)
 
-(* This module defines type-classes *)
+type direction = Forward | Backward
+
+(** This module defines type-classes *)
 type typeclass = {
-  (* The class implementation: a record parameterized by the context with defs in it or a definition if
+  (** 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 class' global identifier. *)
   cl_impl : global_reference;
 
-  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
+  (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
      The boolean indicates if the typeclass argument is a direct superclass and the global reference
      gives a direct link to the class itself. *)
   cl_context : (global_reference * bool) option list * rel_context;
 
-  (* Context of definitions and properties on defs, will not be shared *)
+  (** Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
 
-  (* The methods implementations of the typeclass as projections. Some may be undefinable due to
-     sorting restrictions. *)
-  cl_projs : (identifier * constant option) list;
+  (** The methods implementations of the typeclass as projections. 
+      Some may be undefinable due to sorting restrictions or simply undefined if 
+      no name is provided. The [int option option] indicates subclasses whose hint has
+      the given priority. *)
+  cl_projs : (name * (direction * int option) option * constant option) list;
 }
 
 type instance
@@ -55,15 +55,16 @@ val add_inductive_class : inductive -> unit
 
 val new_instance : typeclass -> int option -> bool -> global_reference -> instance
 val add_instance : instance -> unit
+val remove_instance : instance -> unit
 
-val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
+val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
 
 
-(* These raise a UserError if not a class. *)
+(** These raise a UserError if not a class. *)
 val dest_class_app : env -> constr -> typeclass * constr list
 
-(* Just return None if not a class *)
-val class_of_constr : constr -> typeclass option
+(** Just return None if not a class *)
+val class_of_constr : constr -> (rel_context * (typeclass * constr list)) option
   
 val instance_impl : instance -> global_reference
 
@@ -72,14 +73,13 @@ val is_instance : global_reference -> bool
 
 val is_implicit_arg : hole_kind -> bool
 
-(* Returns the term and type for the given instance of the parameters and fields
+(** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
 val instance_constructor : typeclass -> constr list -> constr option * types
 
-(* Use evar_extra for marking resolvable evars. *)
-val bool_in : bool -> Dyn.t
-val bool_out : Dyn.t -> bool
+(** Resolvability.
+    Only undefined evars could be marked or checked for resolvability. *)
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
@@ -90,11 +90,26 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
-val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
-val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+val register_set_typeclass_transparency : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
-val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
-val add_instance_hint : global_reference -> int option -> unit
+val register_classes_transparent_state : (unit -> transparent_state) -> unit
+val classes_transparent_state : unit -> transparent_state
+
+val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit
+val register_remove_instance_hint : (global_reference -> unit) -> unit
+val add_instance_hint : constr -> bool -> int option -> unit
+val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
+
+val declare_instance : int option -> bool -> global_reference -> unit
+
+
+(** Build the subinstances hints for a given typeclass object.
+    check tells if we should check for existence of the 
+    subinstances and add only the missing ones. *)
+
+val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
+  (int option * constr) list