package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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

Module TypeclassesSource

Sourcetype 'a hint_info_gen = {
  1. hint_priority : int option;
  2. hint_pattern : 'a option;
}
Sourcetype class_method = {
  1. meth_name : Names.Name.t;
  2. meth_const : Names.Constant.t option;
}
Sourcetype typeclass = {
  1. 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.

    *)
  2. 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.

    *)
  3. cl_context : Constr.rel_context;
    (*

    Context in which the definitions are typed.

    *)
  4. cl_trivial : bool;
    (*

    Class declared with "Class Foo params := {

    }

    ", produces 0 goals in interactive mode.

    *)
  5. cl_props : Constr.rel_context;
    (*

    Context of definitions and properties on defs, used for "Instance := {

    }

    ". If cl_impl is a record this is the arguments of its constructor (without parameters). Otherwise it is a single LocalAssum of type convertible to cl_impl.

    *)
  6. 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. Used for dumpglob in "Instance := {

    }

    " and in elpi.

    *)
  7. cl_strict : bool;
    (*

    Whether we use matching or full unification during resolution

    *)
  8. 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 = {
  1. is_class : Names.GlobRef.t;
  2. is_info : hint_info;
  3. is_impl : Names.GlobRef.t;
}
Sourceval instances : Names.GlobRef.t -> instance list option

None if not a class

Sourceval 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

raise TypeClassError if not a class

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.

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
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
Sourceval 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
Sourceval 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
Sourceval is_maybe_class_type : Evd.evar_map -> EConstr.types -> bool
Sourceval 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)
Sourceval set_solve_one_instance : (Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr) -> unit
  • deprecated (9.0) For internal use only