Mlsem_common.EidIdentifiers for expressions.
Every node of an AST carries one, and several analyses are indexed by it (Mlsem_system.Refinement.Refinements, Mlsem_system.Analyzer), so distinct nodes of a same term must carry distinct ids: a program transformation that duplicates a sub-expression must refresh the ids of the copies. Each id also records a source location and whether the analyzer may report notices about it, so that generated code is not blamed for problems the user cannot see.
val dummy : tPlaceholder id, for expressions that do not correspond to any source location. It has no location and no notices, and refresh dummy is dummy.
val unique : unit -> tFresh id for generated code: no source location, and notices disabled. Only appropriate on nodes that cannot be blamed for a type error.
val unique_with_pos : Position.t -> tFresh id located at pos, with notices enabled.
val generated_with_pos : Position.t -> tFresh id located at pos, with notices disabled.
Fresh id inheriting the location and the notice flag of its argument. This is how a duplicated sub-expression keeps its diagnostics while getting the distinct ids the analyses require. Refreshed ids form an equivalence class, accessible by calling eq_class.
val eq_class : t -> Set.tEquivalence class of an id (cf. refresh).
val loc : t -> Position.tval show_notices : t -> boolWhether the analyzer may report notices and unreachability warnings about this expression.
val hash : t -> intval pp : Stdlib.Format.formatter -> t -> unit