package logtk

You can search for identifiers within the package.

in-package search v0.2.0

Core types and algorithms for logic

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz

md5=e72de75e9f0f87da9e6e8c0a4d4c89f9

sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/logtk/Logtk/Precedence/Constr/index.html

Module `Precedence.Constr`

Constraints

type 'a t = private ID.t -> ID.t -> int constraint 'a = [< `partial | `total ]

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

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 compare_by : constr:'a t -> ID.t -> ID.t -> int

compare_by ~constr a b returns the result of comparing symbols a and b using constr

val make : (ID.t -> ID.t -> int) -> [ `partial ] t

Create a new partial order. CAUTION, this order must respect some properties (see 'at)

On This Page

Constraints