Module Dalton_sig.GROUND.Lb

module Lb: sig  end
The module Lb specifies the set of constant lower bounds.

type t
The type of constant lower bound.

val bottom : t
bottom is a distinguished lower bound. It is the bottom element of the semi-lattice.
val is_bottom : t -> bool
is_bottom lb must return true if and only if lb is bottom.
val union : t -> t -> t
union lb1 lb2 gives the union (according to the semi-lattice structure) of the lower bounds lb1 and lb2.
val leq : t -> t -> bool
leq env lb1 lb2 tells wether lb1 is less than or equal to lb2 in the semi-lattice of constant lower bounds, i.e.: for all alpha, lb2 < alpha implies lb1 < alpha.
val compare : t -> t -> int
A comparison function on constant lower bounds has to be provided. It is just used for computation and has no semantical meaning.
val normalize : t -> t
normalize lb internally normalizes the lower bound lb.
val fprint : Format.formatter -> t -> unit
fprint ppf lb pretty-prints the constant lower bound lb on the formatter ppf. (This function is used for printing of constants in constraints.)
val fprint_in_term : int -> Format.formatter -> t -> unit
fprint_in_term ppf lb is used to prints the constant lower bound lb on the formatter ppf when it appears in a term, in place of a non-negative variable which has no predecessor.

An usual implementation may be: let fprint_in_term _ ppf lb = Format.fprintf ppf "> %a" fprint lb

val draw : t -> string list