diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 15 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 22 | ||||
| -rw-r--r-- | pretyping/vernacexpr.ml | 12 |
3 files changed, 31 insertions, 18 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 30ddeffa69..e73a78fb84 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions @@ -73,7 +80,7 @@ type typeclass = { cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list; cl_strict : bool; @@ -85,7 +92,7 @@ type typeclasses = typeclass Refmap.t type instance = { is_class: global_reference; - is_info: Vernacexpr.hint_info_expr; + is_info: hint_info_expr; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; @@ -96,7 +103,7 @@ type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let hint_priority is = is.is_info.Vernacexpr.hint_priority +let hint_priority is = is.is_info.hint_priority let new_instance cl info glob impl = let global = @@ -266,8 +273,6 @@ let check_instance env sigma c = not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false -open Vernacexpr - let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b80c287117..e50d90b156 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,13 @@ open Environ type direction = Forward | Backward +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + (** This module defines type-classes *) type typeclass = { (** The toplevel universe quantification in which the typeclass lives. In @@ -37,7 +44,7 @@ type typeclass = { 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.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; + cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -55,8 +62,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> - global_reference -> instance +val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -123,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state val add_instance_hint_hook : (global_reference_or_constr -> global_reference list -> - bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t + bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t val remove_instance_hint_hook : (global_reference -> unit) Hook.t val add_instance_hint : global_reference_or_constr -> global_reference list -> - bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit + bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit +val declare_instance : hint_info_expr option -> bool -> global_reference -> unit (** Build the subinstances hints for a given typeclass object. @@ -140,5 +146,5 @@ val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_refere subinstances and add only the missing ones. *) val build_subclasses : check:bool -> env -> evar_map -> global_reference -> - Vernacexpr.hint_info_expr -> - (global_reference list * Vernacexpr.hint_info_expr * constr) list + hint_info_expr -> + (global_reference list * hint_info_expr * constr) list diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 4e1c986f16..f0e5f5746f 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -115,14 +115,16 @@ type hint_mode = | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) -type 'a hint_info_gen = +type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] -type hint_info_expr = constr_pattern_expr hint_info_gen +type hint_info_expr = Typeclasses.hint_info_expr +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -362,12 +364,12 @@ type nonrec vernac_expr = local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) - hint_info_expr + Typeclasses.hint_info_expr | VernacContext of local_binder_expr list | VernacDeclareInstances of - (reference * hint_info_expr) list (* instances names, priorities and patterns *) + (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) | VernacDeclareClass of reference (* inductive or definition name *) |