Module `Mod_subst`Source

`Mod_subst`

Delta resolver

Sourcetype delta_resolver

A delta_resolver maps name (constant, inductive, module_path) to canonical name

Sourceval empty_delta_resolver : delta_resolver

val add_mp_delta_resolver : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  delta_resolver ->
  delta_resolver

Source

val add_kn_delta_resolver : 
  Names.KerName.t ->
  Names.KerName.t ->
  delta_resolver ->
  delta_resolver

Source

val add_inline_delta_resolver : 
  Names.KerName.t ->
  (int * Constr.constr UVars.univ_abstracted option) ->
  delta_resolver ->
  delta_resolver

Sourceval add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

Effect of a delta_resolver on a module path, on a kernel name

Sourceval mp_of_delta : delta_resolver -> Names.ModPath.t -> Names.ModPath.t

Sourceval kn_of_delta : delta_resolver -> Names.KerName.t -> Names.KerName.t

Build a constant whose canonical part is obtained via a resolver

Source

val constant_of_delta_kn : 
  delta_resolver ->
  Names.KerName.t ->
  Names.Constant.t

Same, but a 2nd resolver is tried if the 1st one had no effect

Source

val constant_of_deltas_kn : 
  delta_resolver ->
  delta_resolver ->
  Names.KerName.t ->
  Names.Constant.t

Same for inductive names

Sourceval mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t

Source

val mind_of_deltas_kn : 
  delta_resolver ->
  delta_resolver ->
  Names.KerName.t ->
  Names.MutInd.t

Source

val inline_of_delta : 
  int option ->
  delta_resolver ->
  (int * Names.KerName.t) list

Extract the set of inlined constant in the resolver

Does a delta_resolver contains a mp, a constant, an inductive ?

Sourceval mp_in_delta : Names.ModPath.t -> delta_resolver -> bool

Sourceval con_in_delta : Names.Constant.t -> delta_resolver -> bool

Sourceval mind_in_delta : Names.MutInd.t -> delta_resolver -> bool

Substitution

Sourcetype substitution

Sourceval empty_subst : substitution

Sourceval is_empty_subst : substitution -> bool

Source

val add_mbid : 
  Names.MBId.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution ->
  substitution

add_* add arg2/arg1{arg3} to the substitution with no sequential composition. Most often this is not what you want. For sequential composition, try join (map_mbid mp delta) subs *

Source

val add_mp : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution ->
  substitution

Source

val map_mbid : 
  Names.MBId.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution

map_* create a new substitution arg2/arg1{arg3}

Source

val map_mp : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  delta_resolver ->
  substitution

Sourceval join : substitution -> substitution -> substitution

sequential composition: substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)

Sourceval subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the domain of the resolver

Source

val subst_codom_delta_resolver : 
  substitution ->
  delta_resolver ->
  delta_resolver

Apply the substitution on the codomain of the resolver

Source

val subst_dom_codom_delta_resolver : 
  substitution ->
  delta_resolver ->
  delta_resolver

subst_mp sub mp guarantees that whenever the result of the substitution is structutally equal mp, it is equal by pointers as well ==

Sourceval subst_mp : substitution -> Names.ModPath.t -> Names.ModPath.t

Sourceval subst_mind : substitution -> Names.MutInd.t -> Names.MutInd.t

Sourceval subst_ind : substitution -> Names.inductive -> Names.inductive

Sourceval subst_constructor : substitution -> Names.constructor -> Names.constructor

Sourceval subst_pind : substitution -> Constr.pinductive -> Constr.pinductive

Sourceval subst_kn : substitution -> Names.KerName.t -> Names.KerName.t

Source

val subst_con : 
  substitution ->
  Names.Constant.t ->
  Names.Constant.t * Constr.constr UVars.univ_abstracted option

Sourceval subst_pcon : substitution -> Constr.pconstant -> Constr.pconstant

Sourceval subst_constant : substitution -> Names.Constant.t -> Names.Constant.t

Source

val subst_proj_repr : 
  substitution ->
  Names.Projection.Repr.t ->
  Names.Projection.Repr.t

Sourceval subst_proj : substitution -> Names.Projection.t -> Names.Projection.t

Source

val subst_retro_action : 
  substitution ->
  Retroknowledge.action ->
  Retroknowledge.action

Source

val replace_mp_in_kn : 
  Names.ModPath.t ->
  Names.ModPath.t ->
  Names.KerName.t ->
  Names.KerName.t

replace_mp_in_con mp mp' con replaces mp with mp' in con

Sourceval subst_mps : substitution -> Constr.constr -> Constr.constr

subst_mps sub c performs the substitution sub on all kernel names appearing in c

Sourceval subst_mps_list : substitution list -> Constr.constr -> Constr.constr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Mod_subst/index.html

Module `Mod_subst`Source

`Mod_subst`

Delta resolver

Substitution

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Mod_subst/index.html

Module Mod_substSource

Mod_subst

Delta resolver

Substitution

Module `Mod_subst`Source

`Mod_subst`