diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 60 |
1 files changed, 22 insertions, 38 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index a3118053..fdbb78a9 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeclasses.mli 11161 2008-06-21 14:32:47Z msozeau $ i*) +(*i $Id: typeclasses.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -30,12 +30,10 @@ type typeclass = { (* 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 : ((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. *) + cl_context : ((global_reference * bool) option * rel_declaration) list; (* Context of definitions and properties on defs, will not be shared *) - cl_props : named_context; + cl_props : rel_context; (* The methods implementations of the typeclass as projections. *) cl_projs : (identifier * constant) list; @@ -43,33 +41,32 @@ type typeclass = { type instance -val instance_impl : instance -> constant - -val new_instance : typeclass -> int option -> bool -> constant -> instance - val instances : global_reference -> instance list val typeclasses : unit -> typeclass list +val all_instances : unit -> instance list + val add_class : typeclass -> unit -val add_instance : instance -> unit -val register_add_instance_hint : (constant -> int option -> unit) -> unit -val add_instance_hint : constant -> int option -> unit +val new_instance : typeclass -> int option -> bool -> constant -> instance +val add_instance : instance -> unit 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 *) +val instance_impl : instance -> constant + +val is_class : global_reference -> bool val is_instance : global_reference -> bool val is_method : constant -> bool +val is_implicit_arg : hole_kind -> bool + (* 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 * 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 resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool +val instance_constructor : typeclass -> constr list -> constr * types (* Use evar_extra for marking resolvable evars. *) val bool_in : bool -> Dyn.t @@ -78,28 +75,15 @@ val bool_out : Dyn.t -> bool val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map +val is_class_evar : evar_info -> bool -val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs - -val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref -val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref - -type substitution = (identifier * constr) list +val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> + env -> evar_defs -> evar_defs +val resolve_one_typeclass : env -> evar_map -> types -> constr -val substitution_of_named_context : - evar_defs ref -> env -> identifier -> int -> - substitution -> named_context -> substitution - -val nf_substitution : evar_map -> substitution -> substitution - -val is_implicit_arg : hole_kind -> bool - -(* debug *) +val register_add_instance_hint : (constant -> int option -> unit) -> unit +val add_instance_hint : constant -> int option -> unit -(* 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 *) +val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref +val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref |