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.Simple

type t

val empty : t

val print : Format.formatter -> t -> unit

val is_identity : t -> bool

val 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 ->
  t

val has_import_map : t -> bool

val compose : second:t -> first:t -> t

Note 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 : 
  t ->
  Flambda2_identifiers.Variable.t ->
  Flambda2_identifiers.Variable.t ->
  t

val add_fresh_variable : 
  t ->
  Flambda2_identifiers.Variable.t ->
  guaranteed_fresh:Flambda2_identifiers.Variable.t ->
  t

val apply_variable : 
  t ->
  Flambda2_identifiers.Variable.t ->
  Flambda2_identifiers.Variable.t

val apply_variable_set : 
  t ->
  Flambda2_identifiers.Variable.Set.t ->
  Flambda2_identifiers.Variable.Set.t

val add_symbol : 
  t ->
  Flambda2_identifiers.Symbol.t ->
  Flambda2_identifiers.Symbol.t ->
  t

val add_fresh_symbol : 
  t ->
  Flambda2_identifiers.Symbol.t ->
  guaranteed_fresh:Flambda2_identifiers.Symbol.t ->
  t

val apply_symbol : 
  t ->
  Flambda2_identifiers.Symbol.t ->
  Flambda2_identifiers.Symbol.t

val apply_symbol_set : 
  t ->
  Flambda2_identifiers.Symbol.Set.t ->
  Flambda2_identifiers.Symbol.Set.t

val apply_name : 
  t ->
  Flambda2_identifiers.Name.t ->
  Flambda2_identifiers.Name.t

val add_continuation : 
  t ->
  Flambda2_identifiers.Continuation.t ->
  Flambda2_identifiers.Continuation.t ->
  t

val add_fresh_continuation : 
  t ->
  Flambda2_identifiers.Continuation.t ->
  guaranteed_fresh:Flambda2_identifiers.Continuation.t ->
  t

val apply_continuation : 
  t ->
  Flambda2_identifiers.Continuation.t ->
  Flambda2_identifiers.Continuation.t

val add_code_id : 
  t ->
  Flambda2_identifiers.Code_id.t ->
  Flambda2_identifiers.Code_id.t ->
  t

val add_fresh_code_id : 
  t ->
  Flambda2_identifiers.Code_id.t ->
  guaranteed_fresh:Flambda2_identifiers.Code_id.t ->
  t

val apply_code_id : 
  t ->
  Flambda2_identifiers.Code_id.t ->
  Flambda2_identifiers.Code_id.t

val apply_const : 
  t ->
  Flambda2_identifiers.Reg_width_const.t ->
  Flambda2_identifiers.Reg_width_const.t

val apply_simple : t -> Simple.t -> Simple.t

val value_slot_is_used : t -> Flambda2_identifiers.Value_slot.t -> bool

Module Flambda2_nominal.Renaming

Module `Flambda2_nominal.Renaming`