`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`