Mod_subst (rocq-runtime.Mod

`Mod_subst`

Delta resolver

type 'a 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.

Resolvers come in three flavours, statically distinguished by their parameter. All of them map names to other names; they differ in the inlining information they may carry.

Resolvers from module bodies. They contain no inlining data.
Resolvers from module types. They may contain inlining declarations, i.e. the level of a Parameter Inline. Only a module type may declare parameters, hence only a module type resolver may carry such information.
Resolvers from module substitutions. They may contain inlining payloads, which are terms inserted in lieu of the original constant when applying the substitution.

Since a name and the way a field is to be inlined are independent statements, casting between flavours drops the latter and preserves the former in full.

type mod_body = [

| `ModBody

]

type mod_type = [

| `ModType

]

type mod_subst = [

| `ModSubst

]

val forget_inline_delta_resolver : 'a delta_resolver -> 'b delta_resolver

Turn a resolver of any kind into a resolver of any other kind by dropping all inlining information.

val of_body_delta_resolver : mod_body delta_resolver -> 'a delta_resolver

A module body's resolver carries no inlining information by construction, so it can be read at any other kind without losing anything.

val empty_delta_resolver : Names.ModPath.t -> 'a delta_resolver

Given a root, build a resolver.

val has_root_delta_resolver : Names.ModPath.t -> 'a delta_resolver -> bool

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

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

val lift_mp_delta_resolver : 
  Names.ModPath.t ->
  'a delta_resolver ->
  'a delta_resolver

lift_mp_delta_resolver mp reso marks mp as being a bound name that must be left untouched by substitution. This is the semantics of delayed resolvers for functors and module types. Assumes that root(reso) ⊆ mp.

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

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

val add_inline_delta_resolver : 
  Names.KerName.t ->
  int ->
  mod_type delta_resolver ->
  mod_type delta_resolver

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

val add_inline_body_delta_resolver : 
  Names.KerName.t ->
  Constr.constr UVars.univ_abstracted ->
  mod_subst delta_resolver ->
  mod_subst delta_resolver

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

val add_delta_resolver : 
  'a delta_resolver ->
  'a delta_resolver ->
  'a 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).

val upcast_delta_resolver : 
  Names.ModPath.t ->
  'a delta_resolver ->
  'a 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

val mp_of_delta : 'a delta_resolver -> Names.ModPath.t -> Names.ModPath.t

val kn_of_delta : 'a delta_resolver -> Names.KerName.t -> Names.KerName.t

val mp_is_alias : 'a 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

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

Same for inductive names

val mind_of_delta_kn : 'a delta_resolver -> Names.KerName.t -> Names.MutInd.t

val fold_inline_body_delta_resolver : 
  (Names.KerName.t -> Constr.constr UVars.univ_abstracted -> 'b -> 'b) ->
  mod_subst delta_resolver ->
  'b ->
  'b

val inline_of_delta : 
  int option ->
  mod_type delta_resolver ->
  Names.KerName.t list

The fields the resolver declared inlinable, up to the given level

Substitution

type substitution

val empty_subst : substitution

val is_empty_subst : substitution -> bool

val add_mbid : 
  Names.MBId.t ->
  Names.ModPath.t ->
  mod_subst 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 *

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

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

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

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

val join : substitution -> substitution -> substitution

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

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

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

val subst_codom_delta_resolver : 
  substitution ->
  'a delta_resolver ->
  'a delta_resolver

Apply the substitution on the codomain of the resolver

val subst_dom_codom_delta_resolver : 
  substitution ->
  'a delta_resolver ->
  'a 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 ==

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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