Module `Mod_subst`Source

`Mod_subst`

Delta resolver

Sourcetype delta_resolver

A delta resolver is a renaming of kernames and modpaths. Objects on which the resolver acts non-trivially must share a common modpath prefix called the root of the resolver.

Sourceval empty_delta_resolver : Names.ModPath.t -> delta_resolver

Given a root, build a resolver.

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

Source

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

add_mp_delta_resolver mp v reso assumes that root(reso) ⊆ mp.

Source

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

add_kn_delta_resolver kn v reso assumes that root(reso) ⊆ modpath(kn).

Source

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

add_inline_delta_resolver kn v reso assumes that root(reso) ⊆ modpath(kn).

Sourceval add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

add_delta_resolver reso1 reso2 merges two renamings, assuming that root(reso2) ⊆ root(reso1). Note that this is asymmetrical. The root of the result is root(reso2).

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

Assuming mp ⊆ root(delta), upcast_delta_resolver mp delta allows seeing delta as a resolver with root = mp.

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

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

mp_is_alias reso mp tells whether reso makes mp equivalent to some other modpath. Note that both this and mp_of_delta take prefixes into account: a module is equivalent to another one as soon as one of its ancestors is.

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 for inductive names

Sourceval mind_of_delta_kn : 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

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)

Source

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

subst_dom_delta_resolver mpfrom mpto delta substitutes the root of the resolver delta from mpfrom to mpto, i.e. performs α-equivalence.

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-project
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-project Dependency

Authors

Maintainers

Sources

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

Module Mod_substSource

Mod_subst

Delta resolver

Substitution

dune-project
Dependency

Module `Mod_subst`Source

`Mod_subst`