module Constr: sig .. end
Constraints
type [< `partial | `total ] t = private ID.t -> ID.t -> int
A partial order on symbols, used to make the precedence more
precise.
'a encodes the kind of ordering: partial or total
NOTE: the ordering must partition the set of ALL symbols into
equivalence classes, within which all symbols are equal, but
symbols of distinct equivalence classes are always ordered.
val arity : (ID.t -> int) -> [ `partial ] t
decreasing arity constraint (big arity => high in precedence)
val invfreq : ID.t Sequence.t -> [ `partial ] t
symbols with high frequency are smaller. Elements of unknown
frequency are assumed to have a frequency of 0.
val max : ID.t list -> [ `partial ] t
maximal symbols, in decreasing order
val min : ID.t list -> [ `partial ] t
minimal symbols, in decreasing order
val alpha : [ `total ] t
alphabetic ordering on symbols, themselves bigger than builtin
val compose : [ `partial ] t ->
([< `partial | `total ] as 'a) t -> 'a t
compose a b uses a to compare symbols; if a cannot decide,
then we use b.
val compose_sort : (int * [ `partial ] t) list ->
[ `partial ] t
compose_sort l sorts the list by increasing priority (the lower,
the earlier an ordering is applied, and therefore the more
impact it has) before composing
val make : (ID.t -> ID.t -> int) -> [ `partial ] t
Create a new partial order.
CAUTION, this order must respect some properties (see 'a t)