Module `Typeclasses`Source

Sourcetype 'a hint_info_gen = {

hint_priority : int option;
hint_pattern : 'a option;

}

Sourcetype hint_info = (Names.Id.Set.t * Pattern.constr_pattern) hint_info_gen

Sourcetype class_method = {

meth_name : Names.Name.t;
meth_info : hint_info option;
meth_const : Names.Constant.t option;

}

Sourcetype typeclass = {

cl_univs : UVars.AbstractContext.t;
(*
The toplevel universe quantification in which the typeclass lives. In particular, cl_props and cl_context are quantified over it.
*)
cl_impl : Names.GlobRef.t;
(*
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_context : Constr.rel_context;
(*
Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
*)
cl_props : Constr.rel_context;
(*
Context of definitions and properties on defs, will not be shared
*)
cl_projs : class_method 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_strict : bool;
(*
Whether we use matching or full unification during resolution
*)
cl_unique : bool;
(*
Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution.
*)

}

This module defines type-classes

Sourcetype instance = {

is_class : Names.GlobRef.t;
is_info : hint_info;
is_impl : Names.GlobRef.t;

}

Sourceval instances : Names.GlobRef.t -> instance list option

None if not a class

Source

val instances_exn : 
  Environ.env ->
  Evd.evar_map ->
  Names.GlobRef.t ->
  instance list

raise TypeClassError if not a class

Sourceval typeclasses : unit -> typeclass list

Sourceval all_instances : unit -> instance list

Sourceval load_class : typeclass -> unit

Sourceval load_instance : instance -> unit

Sourceval remove_instance : instance -> unit

Sourceval class_info : Names.GlobRef.t -> typeclass option

None if not a class

Source

val class_info_exn : 
  Environ.env ->
  Evd.evar_map ->
  Names.GlobRef.t ->
  typeclass

raise TypeClassError if not a class

Source

val dest_class_app : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (typeclass * EConstr.EInstance.t) * Constr.constr list

These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance.

Sourceval typeclass_univ_instance : typeclass UVars.puniverses -> typeclass

Get the instantiated typeclass structure for a given universe instance.

Source

val class_of_constr : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (EConstr.rel_context
   * ((typeclass * EConstr.EInstance.t) * Constr.constr list))
    option

Just return None if not a class

Sourceval instance_impl : instance -> Names.GlobRef.t

Sourceval hint_priority : instance -> int option

Sourceval is_class : Names.GlobRef.t -> bool

Returns the term and type for the given instance of the parameters and fields of the type class.

Source

val instance_constructor : 
  typeclass EConstr.puniverses ->
  EConstr.t list ->
  EConstr.t option * EConstr.t

Sourcetype evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool

Filter which evars to consider for resolution.

Sourceval all_evars : evar_filter

Sourceval all_goals : evar_filter

Sourceval no_goals : evar_filter

Sourceval no_goals_or_obligations : evar_filter

Resolvability. Only undefined evars can be marked or checked for resolvability. They represent type-class search roots.

A resolvable evar is an evar the type-class engine may try to solve An unresolvable evar is an evar the type-class engine will NOT try to solve

Sourceval make_unresolvables : (Evar.t -> bool) -> Evd.evar_map -> Evd.evar_map

Sourceval is_class_evar : Evd.evar_map -> Evd.undefined Evd.evar_info -> bool

Sourceval is_class_type : Evd.evar_map -> EConstr.types -> bool

Source

val resolve_typeclasses : 
  ?filter:evar_filter ->
  ?unique:bool ->
  ?fail:bool ->
  Environ.env ->
  Evd.evar_map ->
  Evd.evar_map

Sourceval get_filtered_typeclass_evars : evar_filter -> Evd.evar_map -> Evar.Set.t

Sourceval error_unresolvable : Environ.env -> Evd.evar_map -> Evar.Set.t -> 'a

Source

val set_solve_all_instances : 
  (Environ.env -> Evd.evar_map -> evar_filter -> bool -> bool -> Evd.evar_map) ->
  unit

A plugin can override the TC resolution engine by calling these two APIs. Beware this action is not registed in the summary (the Undo system) so it is up to the plugin to do so.

Sourceval get_typeclasses_unique_solutions : unit -> bool

Source

val resolve_one_typeclass : 
  ?unique:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Evd.evar_map * EConstr.constr

deprecated (9.0) Use Class_tactics.resolve_one_typeclass ("unique" argument was ignored)

Source

val set_solve_one_instance : 
  (Environ.env ->
    Evd.evar_map ->
    EConstr.types ->
    Evd.evar_map * EConstr.constr) ->
  unit

deprecated (9.0) For internal use only

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Typeclasses/index.html

Module `Typeclasses`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Typeclasses/index.html

Module TypeclassesSource

Module `Typeclasses`Source