diff options
| author | Matthieu Sozeau | 2014-09-12 21:03:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-15 12:16:52 +0200 |
| commit | fb5d74bb3f5a46e918877bd9c5b14dbcdc220430 (patch) | |
| tree | 1cab041a8b43078d47cbc9375c67b09eacde8ed0 /pretyping/typeclasses.mli | |
| parent | 019c0fc0f996fa349e2d82feb97feddade5ea789 (diff) | |
Rework typeclass resolution and control of backtracking.
Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b1f816e651..447df1da1b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -37,6 +37,10 @@ type typeclass = { (** Whether we use matching or full unification during resolution *) cl_strict : bool; + + (** Whether we can assume that instances are unique, which allows + no backtracking and sharing of resolution. *) + cl_unique : bool; } type instance @@ -47,10 +51,6 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val add_constant_class : constant -> unit - -val add_inductive_class : inductive -> unit - val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> global_reference -> instance val add_instance : instance -> unit @@ -104,9 +104,9 @@ val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> types -> bool -val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool -> - env -> evar_map -> evar_map -val resolve_one_typeclass : env -> evar_map -> types -> open_constr +val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> + ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -122,8 +122,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> bool -> int option -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit -val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref -val solve_instantiation_problem : (env -> evar_map -> types -> open_constr) ref +val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) ref +val solve_instantiation_problem : (env -> evar_map -> types -> bool -> open_constr) ref val declare_instance : int option -> bool -> global_reference -> unit |