Module Hax_engine.Concrete_ident_view_types

This modules defines what is the view over a concrete identifiers.

Hax manipulates concrete identifiers (that is global identifiers referring to concrete Rust items -- not built-in operators) as raw Rust identifiers augmented with some metadata.

Rust represents identifiers as a crate and a path. Each chunk of the path is roughly a level of nest in Rust. The path lacks information about definition kinds.

There is two kinds of nesting for items.

This module provides a view to those paths: a path in the view is a list of smaller relational paths. For instance, consider the following piece of code:

mod a {
    impl MyTrait for MyType {
        fn assoc_fn() {
            struct LocalStruct {
                field: u8,
            };
        }
    }
}

Here, the Rust raw definition identifier of LocalStruct is roughly my_crate::a::<Impl 0>::assoc_fn::LocalStruct::field.

The view for LocalStruct looks like: { { path: ["mycrate"; "a"], name_path: [ `AssociatedItem ("assoc_fn", `Impl 0); `Field ("field", `Constructor ("LocalStruct", `Struct "LocalStruct")) ] } }

type disambiguator = Hax_engine.Prelude.Int64.t

A Int64.t disambiguator: this is given by Rust.

val pp_disambiguator : Ppx_deriving_runtime.Format.formatter -> disambiguator -> Ppx_deriving_runtime.unit
val show_disambiguator : disambiguator -> Ppx_deriving_runtime.string
val equal_disambiguator : disambiguator -> disambiguator -> Ppx_deriving_runtime.bool
val map_disambiguator : 'a -> 'b
val compare_disambiguator : disambiguator -> disambiguator -> Prelude.int
val disambiguator_of_sexp : Sexplib0.Sexp.t -> disambiguator
val sexp_of_disambiguator : disambiguator -> Sexplib0.Sexp.t
val hash_fold_disambiguator : Ppx_hash_lib.Std.Hash.state -> disambiguator -> Ppx_hash_lib.Std.Hash.state
val hash_disambiguator : disambiguator -> Ppx_hash_lib.Std.Hash.hash_value
module DisambiguatedString : sig ... end

A string with a disambiguator.

module ModPath : sig ... end

A "module and crate"-only path. This is the longest `mod` suffix of a definition identifier path. This is a list of disambiguated strings.

module RelPath : sig ... end

A relational path is a path composed of relational chunks.

type t = {
  1. mod_path : ModPath.t;
  2. rel_path : RelPath.t;
}

Invariant: name_path is non-empty

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
val compare : t -> t -> Prelude.int
val t_of_sexp : Sexplib0.Sexp.t -> t
val sexp_of_t : t -> Sexplib0.Sexp.t
val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
val hash : t -> Ppx_hash_lib.Std.Hash.hash_value