Module Hax_engine.Explicit_def_id

An ExplicitDefId.t is a Rust Types.def_id tagged with some diambiguation metadata. Explicit definition identifiers are used internally by the concrete names of hax.

Rust raw Types.def_id can be ambiguous: consider the following Rust code: ```rust struct S; fn f() -> S S ``` Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refer to the exact same identifier `mycrate::S`. Yet, they denote two very different objects: a type versus a constructor.

ExplicitDefId.t clears up this ambiguity, making constructors and types two separate things.

Also, an ExplicitDefId.t always points to an item: an ExplicitDefId.t is never pointing to a crate alone.

type t

Representation of explicit definition identifiers.

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_hash_lib.Hashable.S with type t := 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
val of_def_id : ?constructor:Prelude.bool -> Types.def_id -> t Prelude.option

Smart constructor for t. Creates an explicit def id out of a raw Rust definition identifier Types.def_id.

When of_def_id is called with id a Types.def_id, if the kind of id is either Struct or Union, then constructor is mandatory. Otherwise, the argument constructor should be true only if id is a variant.

of_def_id shall not be called on a Rust identifier pointing to a crate root.

This function returns Some only when those condition are met.

val of_def_id_exn : ?constructor:Prelude.bool -> Types.def_id -> t

Exception-throwing variant of of_def_id. This should be used when we know statically that the conditions described in the documentation of of_def_id are met.

For instance, with static Types.def_ids or in Import_thir.

val is_constructor : t -> Prelude.bool

Checks wether a definition identifier id points to a constructor.

is_constructor id returns true when:

  • the kind of id is Struct or Union and the identifier was tagged as a constructor;
  • the kind of id is Variant. Otherwise, is_constructor id returns false.
val parent : t -> t Prelude.option

Looks up the parent of a definition identifier. Note that the parent of the identifier of a field is always a constructor.

Also, a top-level item (e.g. `my_crate::some_item`) has no parent: recall that t represent only items, not crates.

val parents : t -> t Prelude.list

Ordered list of parents for an identifier id, starting with id, up to the top-most parent identifier.

val to_def_id : t -> Types.def_id_contents

Destructor for t.

module State : sig ... end
module ImplInfoStore : sig ... end