package logtk
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/logtk/Logtk/Precedence/Constr/index.html
Module Precedence.Constr
Constraints
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.
type prec_fun = signature:Signature.t -> ID.t Iter.t -> [ `partial ] t
val arity : prec_fun
decreasing arity constraint (big arity => high in precedence)
val invfreq : prec_fun
symbols with high frequency are smaller. Elements of unknown frequency are assumed to have a frequency of 0.
val max : prec_fun
maximal symbols, in decreasing order
val min : prec_fun
minimal symbols, in decreasing order
val prec_fun_of_str : string -> prec_fun
val alpha : [ `total ] t
alphabetic ordering on symbols, themselves bigger than builtin
compose a b
uses a
to compare symbols; if a
cannot decide, then we use b
.
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
compare_by ~constr a b returns the result of comparing symbols a and b using constr