package logtk

  1. Overview
  2. Docs
On This Page
  1. Constraints
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Precedence.ConstrSource

Constraints

Sourcetype '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.

Sourceval arity : (ID.t -> int) -> [ `partial ] t

decreasing arity constraint (big arity => high in precedence)

Sourceval invfreq : ID.t Iter.t -> [ `partial ] t

symbols with high frequency are smaller. Elements of unknown frequency are assumed to have a frequency of 0.

Sourceval max : ID.t list -> [ `partial ] t

maximal symbols, in decreasing order

Sourceval min : ID.t list -> [ `partial ] t

minimal symbols, in decreasing order

Sourceval alpha : [ `total ] t

alphabetic ordering on symbols, themselves bigger than builtin

Sourceval 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.

Sourceval 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

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

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

OCaml

Innovation. Community. Security.