diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d8e15895..997b28c1 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 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -24,19 +24,19 @@ open Util (* 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; + 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; + cl_context : (global_reference * bool) option list * rel_context; (* 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 + (* The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions. *) cl_projs : (identifier * constant option) list; } @@ -49,7 +49,11 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> int option -> bool -> constant -> instance +val add_constant_class : constant -> unit + +val add_inductive_class : inductive -> unit + +val new_instance : typeclass -> int option -> bool -> global_reference -> instance val add_instance : instance -> unit val class_info : global_reference -> typeclass (* raises a UserError if not a class *) @@ -61,11 +65,10 @@ val dest_class_app : env -> constr -> typeclass * constr list (* Just return None if not a class *) val class_of_constr : constr -> typeclass option -val instance_impl : instance -> constant +val instance_impl : instance -> global_reference val is_class : global_reference -> bool val is_instance : global_reference -> bool -val is_method : constant -> bool val is_implicit_arg : hole_kind -> bool @@ -81,15 +84,17 @@ 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 is_class_evar : evar_map -> evar_info -> bool -val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> - env -> evar_defs -> evar_defs -val resolve_one_typeclass : env -> evar_map -> types -> constr +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_add_instance_hint : (constant -> int option -> unit) -> unit -val add_instance_hint : constant -> int option -> unit +val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> unit -val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref -val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref +val register_add_instance_hint : (global_reference -> int option -> unit) -> unit +val add_instance_hint : global_reference -> int option -> 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 |