Module Flambda2_nominal.Renaming
Handling of permutations and import freshening upon all kinds of bindable names and other identifiers (e.g. constants).
We use permutations instead of substitutions because they cannot accidentally disturb the binding structure of terms. See Name_abstraction.
Unlike Name_occurrences this module does not segregate names according to where they occur (e.g. in terms or in types).
module Simple = Flambda2_identifiers.Int_ids.Simpleval empty : Flambda2_nominal.Renaming.tval print : Stdlib.Format.formatter -> Flambda2_nominal.Renaming.t -> unitval is_identity : Flambda2_nominal.Renaming.t -> boolval create_import_map :
symbols:Flambda2_identifiers.Symbol.t Flambda2_identifiers.Symbol.Map.t ->
variables:Flambda2_identifiers.Variable.t Flambda2_identifiers.Variable.Map.t ->
simples:Simple.t Simple.Map.t ->
consts:
Flambda2_identifiers.Reg_width_const.t
Flambda2_identifiers.Reg_width_const.Map.t ->
code_ids:Flambda2_identifiers.Code_id.t Flambda2_identifiers.Code_id.Map.t ->
continuations:
Flambda2_identifiers.Continuation.t Flambda2_identifiers.Continuation.Map.t ->
used_value_slots:Flambda2_identifiers.Value_slot.Set.t ->
original_compilation_unit:Compilation_unit.t ->
Flambda2_nominal.Renaming.tval has_import_map : Flambda2_nominal.Renaming.t -> boolval compose :
second:Flambda2_nominal.Renaming.t ->
first:Flambda2_nominal.Renaming.t ->
Flambda2_nominal.Renaming.tNote that compose is not commutative on the permutation component. The permutation in the result of compose ~second ~first is that permutation acting initially like first then subsequently like second. second must not hold any import map.
val add_variable :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Variable.t ->
Flambda2_identifiers.Variable.t ->
Flambda2_nominal.Renaming.tval add_fresh_variable :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Variable.t ->
guaranteed_fresh:Flambda2_identifiers.Variable.t ->
Flambda2_nominal.Renaming.tval apply_variable :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Variable.t ->
Flambda2_identifiers.Variable.tval apply_variable_set :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Variable.Set.t ->
Flambda2_identifiers.Variable.Set.tval add_symbol :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Symbol.t ->
Flambda2_identifiers.Symbol.t ->
Flambda2_nominal.Renaming.tval add_fresh_symbol :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Symbol.t ->
guaranteed_fresh:Flambda2_identifiers.Symbol.t ->
Flambda2_nominal.Renaming.tval apply_symbol :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Symbol.t ->
Flambda2_identifiers.Symbol.tval apply_symbol_set :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Symbol.Set.t ->
Flambda2_identifiers.Symbol.Set.tval apply_name :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Name.t ->
Flambda2_identifiers.Name.tval add_continuation :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Continuation.t ->
Flambda2_identifiers.Continuation.t ->
Flambda2_nominal.Renaming.tval add_fresh_continuation :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Continuation.t ->
guaranteed_fresh:Flambda2_identifiers.Continuation.t ->
Flambda2_nominal.Renaming.tval apply_continuation :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Continuation.t ->
Flambda2_identifiers.Continuation.tval add_code_id :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Code_id.t ->
Flambda2_identifiers.Code_id.t ->
Flambda2_nominal.Renaming.tval add_fresh_code_id :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Code_id.t ->
guaranteed_fresh:Flambda2_identifiers.Code_id.t ->
Flambda2_nominal.Renaming.tval apply_code_id :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Code_id.t ->
Flambda2_identifiers.Code_id.tval apply_const :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Reg_width_const.t ->
Flambda2_identifiers.Reg_width_const.tval apply_simple : Flambda2_nominal.Renaming.t -> Simple.t -> Simple.tval value_slot_is_used :
Flambda2_nominal.Renaming.t ->
Flambda2_identifiers.Value_slot.t ->
bool