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