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