Module `Coercionops`Source

Sourcetype cl_typ =

| CL_SORT
| CL_FUN
| CL_SECVAR of Names.variable
| CL_CONST of Names.Constant.t
| CL_IND of Names.inductive
| CL_PROJ of Names.Projection.Repr.t

This is the type of class kinds

Sourceval cl_typ_eq : cl_typ -> cl_typ -> bool

Equality over cl_typ

Sourceval subst_cl_typ : Environ.env -> Mod_subst.substitution -> cl_typ -> cl_typ

Sourceval cl_typ_ord : cl_typ -> cl_typ -> int

Comparison of cl_typ

Sourcetype coe_typ = Names.GlobRef.t

This is the type of coercion kinds

Sourcetype coe_info_typ = {

coe_value : Names.GlobRef.t;
coe_local : bool;
coe_reversible : bool;
coe_is_identity : bool;
coe_is_projection : Names.Projection.Repr.t option;
coe_source : cl_typ;
coe_target : cl_typ;
coe_param : int;

}

This is the type of infos for declared coercions

Sourcetype inheritance_path = coe_info_typ list

This is the type of paths from a class to another

Access to classes infos

Sourceval class_exists : cl_typ -> bool

Sourceval class_nparams : cl_typ -> int

raises Not_found
if this type is not a class

Source

val find_class_type : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  cl_typ * EConstr.EInstance.t * EConstr.constr list

find_class_type env sigma c returns the head reference of c, its universe instance and its arguments

Sourceval find_class_glob_type : 'a Glob_term.glob_constr_g -> cl_typ

Source

val class_of : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.types * cl_typ

raises Not_found if not convertible to a class

Source

val class_args_of : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.constr list

Sourceval subst_coercion : Mod_subst.substitution -> coe_info_typ -> coe_info_typ

Source

val declare_coercion : 
  Environ.env ->
  Evd.evar_map ->
  ?update:bool ->
  coe_info_typ ->
  unit

Set update to update an already declared coercion (default false).

Sourceval coercion_exists : coe_typ -> bool

Access to coercions infos

Sourceval coercion_info : coe_typ -> coe_info_typ

Source

val coercion_type : 
  Environ.env ->
  Evd.evar_map ->
  coe_info_typ EConstr.puniverses ->
  EConstr.t

Lookup functions for coercion paths

raises Not_found
in the following functions when no path exists

given one (or two) types these function also return the class (classes) of the type and its class_args_of

Sourceval lookup_path_between_class : (cl_typ * cl_typ) -> inheritance_path

Source

val lookup_path_between : 
  Environ.env ->
  Evd.evar_map ->
  src:EConstr.types ->
  tgt:EConstr.types ->
  inheritance_path

Source

val lookup_path_to_fun_from : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  inheritance_path

Source

val lookup_path_to_sort_from : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  inheritance_path

Source

val lookup_pattern_path_between : 
  Environ.env ->
  (Names.inductive * Names.inductive) ->
  (Names.constructor * int) list

Sourceval path_is_reversible : inheritance_path -> bool

Sourceval string_of_class : cl_typ -> string

This is for printing purpose

Sourceval pr_class : cl_typ -> Pp.t

Sourceval inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list

Sourceval classes : unit -> cl_typ list

Sourceval coercions : unit -> coe_info_typ list

Sourceval hide_coercion : coe_typ -> int option

hide_coercion returns the number of params to skip if the coercion must be hidden, None otherwise; it raises Not_found if not a coercion

module ClTypSet : CSet.ExtS with type elt = cl_typ

Sourceval reachable_from : cl_typ -> ClTypSet.t

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Coercionops`Source

Access to classes infos

Lookup functions for coercion paths

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module CoercionopsSource

Access to classes infos

Lookup functions for coercion paths

Module `Coercionops`Source