Module Imandra_surface.Uid

Unique IDs

type unique_id_
type special_tag_
type namespace
type t = private {
name : string;

for printing; not unique

id : unique_id_;
special_tag : special_tag_;
mutable namespace : namespace;
mutable chash : Imandra_util.Chash.t option;
mutable depth : int * int;

depth in the graph of definitions. primitives have depth 1

}
type uid = t
val make : ?⁠chash:Imandra_util.Chash.t -> ?⁠special_tag:string -> string -> t
val makef : ?⁠chash:Imandra_util.Chash.t -> ?⁠special_tag:string -> ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'a
val copy : t -> t

Fresh copy

val name : t -> string
val special_tag : t -> string option
val has_special_tag : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val cached_chash : t -> Imandra_util.Chash.t option
val depth : t -> int * int
val print_name : Stdlib.Format.formatter -> t -> unit

print only the name

val print : Stdlib.Format.formatter -> t -> unit
val to_string : t -> string
val print_as_val : Stdlib.Format.formatter -> t -> unit

Print as a OCaml value that can be evaluated in the toplevel

val print_full : Stdlib.Format.formatter -> t -> unit
val to_string_full : t -> string
val inject_string : t -> string

Injective mapping from UIDs to strings, compatible with SMTLIB. Two distinct IDs yield distinct strings

val inject_string_caml : t -> string

Inject into a unique string that can be used as an OCaml identifier

val print_l : Stdlib.Format.formatter -> t list -> unit
val int_of_unique_id : unique_id_ -> int
module Builtins : sig ... end
val is_nil : t -> bool
val is_cons : t -> bool
val is_none : t -> bool
val is_some : t -> bool
module Tbl : CCHashtbl.S with type Tbl.key = t
module Weak_Tbl : Stdlib.Ephemeron.S with type Weak_Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
val chash_by_name : t Imandra_util.Chash.hasher

hash by name only

val chash_sub_cached : t Imandra_util.Chash.hasher

Uses the cached chash, or does nothing if not present

module Chash_map : sig ... end
val chash : ?⁠local:Chash_map.t -> t Imandra_util.Chash.hasher

hash by name, and also using the hash of its definition (if present)

parameter ignore

set of uids to always hash by name, ignoring their def's hash