Module Hax_engine.Concrete_ident

This module provides the global concrete identifiers.

module Fresh_module : sig ... end
module View : module type of Concrete_ident_view
module T : sig ... end
include module type of T with type t = T.t
type t = T.t

A concrete identifier.

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val equal : t -> t -> Ppx_deriving_runtime.bool
include Ppx_yojson_conv_lib.Yojsonable.S with type t := t
val t_of_yojson : Yojson.Safe.t -> t
val yojson_of_t : t -> Yojson.Safe.t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Sexplib0.Sexpable.S with type t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
type reserved_suffix = [
  1. | `Cast
  2. | `Pre
  3. | `Post
]

A concrete identifier can have a reserved suffix: this is useful to derive new identifiers from existing identifiers.

val pp_reserved_suffix : Ppx_deriving_runtime.Format.formatter -> reserved_suffix -> Ppx_deriving_runtime.unit
val show_reserved_suffix : reserved_suffix -> Ppx_deriving_runtime.string
val equal_reserved_suffix : reserved_suffix -> reserved_suffix -> Ppx_deriving_runtime.bool
val yojson_of_reserved_suffix : reserved_suffix -> Ppx_yojson_conv_lib.Yojson.Safe.t
val reserved_suffix_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> reserved_suffix
val __reserved_suffix_of_yojson__ : Ppx_yojson_conv_lib.Yojson.Safe.t -> reserved_suffix
val compare_reserved_suffix : reserved_suffix -> reserved_suffix -> int
val sexp_of_reserved_suffix : reserved_suffix -> Sexplib0.Sexp.t
val reserved_suffix_of_sexp : Sexplib0.Sexp.t -> reserved_suffix
val __reserved_suffix_of_sexp__ : Sexplib0.Sexp.t -> reserved_suffix
val hash_fold_reserved_suffix : Ppx_hash_lib.Std.Hash.state -> reserved_suffix -> Ppx_hash_lib.Std.Hash.state
val hash_reserved_suffix : reserved_suffix -> Ppx_hash_lib.Std.Hash.hash_value
val of_def_id : ?suffix:reserved_suffix option -> value:bool -> Types.def_id -> t

of_def_id ?suffix ~value def_id a concrete identifier out of a Rust identifier def_id. value is a flag that decides whether def_id refers to a value or not.

value is important only for constructors: i.e. the identifier for the type of a struct should be created with value set to false while the identifier for the constructor of a struct should be create with value set to true. For more information, please read the documentation of module Explicit_def_id.

A enumeration of static concrete identifiers useful inside the engine.

val pp_name : Ppx_deriving_runtime.Format.formatter -> name -> Ppx_deriving_runtime.unit
val show_name : name -> Ppx_deriving_runtime.string
val equal_name : name -> name -> Ppx_deriving_runtime.bool
val yojson_of_name : name -> Ppx_yojson_conv_lib.Yojson.Safe.t
val name_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> name
val compare_name : name -> name -> int
val sexp_of_name : name -> Sexplib0.Sexp.t
val name_of_sexp : Sexplib0.Sexp.t -> name
val hash_fold_name : Ppx_hash_lib.Std.Hash.state -> name -> Ppx_hash_lib.Std.Hash.state
val hash_name : name -> Ppx_hash_lib.Std.Hash.hash_value
val of_name : value:bool -> name -> t

Creates an identifier given a name. value has the same meaning as in function of_def_id.

val eq_name : name -> t -> bool

eq_name name identifier is true whenever identifier is name.

val to_debug_string : t -> string

Format an identifier as a (ppx) debug string. The default debug pretty prints the identifier.

val fresh_module : label:string -> t list -> Fresh_module.t

fresh_module ~label hints creates a fresh module given a non-empty list of existing identifiers and a label. The generated module name will be unique, will be close to the identifiers found in hints, and will include the label.

val move_to_fresh_module : Fresh_module.t -> t -> t

Creates a fresh identifier under a given fresh module and given an existing identifier.

val with_suffix : reserved_suffix -> t -> t

Creates an identifier out of an existing one, adding a suffix.

val to_view : t -> Concrete_ident_view.t

Compute a view for a given identifier.

val map_path_strings : f:(string -> string) -> t -> t

This function maps any string found in the inner representation of hax. This is a hack for Import_thir so that we can generically produce identifiers for any integer type, please do not use it elsewhere.

  • alert unsafe This function should be only used in Import_thir!
val is_constructor : t -> bool

Returns true if the ident represents a constructor.

type comparator_witness
val comparator : (t, comparator_witness) Base.Comparator.comparator
module RenderSig : sig ... end
module type RENDER_API = RenderSig.RENDER_API
module type NAME_POLICY = Concrete_ident_render_sig.NAME_POLICY
module ImplInfoStore : sig ... end
val matches_namespace : Types.namespace -> t -> bool