Module Dalton_sig.GROUND.Ub

module Ub: sig  end
The module Ub specifies the set of constant upper bounds.

type t
The type of constant upper bound.

val top : t
top is a distinguished upper bound. It is the top element of the semi-lattice.
val is_top : t -> bool
is_top lb must return true if and only if lb is top.
val inter : t -> t -> t
inter lb1 lb2 gives the intersection (according to the semi-lattice structure) of the lower bounds lb1 and lb2.
val geq : t -> t -> bool
geq lb1 lb2 tells wether lb1 is greater than or equal to lb2 in the semi-lattice of constant upper bounds.
val compare : t -> t -> int
A comparison function on constant upper 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 ub pretty-prints the constant upper bound ub 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 ub is used to print the constant lower bound ub 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 ub = Format.fprintf ppf "< %a" fprint ub

val draw : t -> string list