Module Ord_constraints

module Ord_constraints: sig .. end

A structure representing a set of constraints on ordinal-valued variables. The structure may be queried to test whether the constraint set entails particular relationships between pairs of ordinal variables.

module Elt: sig .. end

include Utilsigs.OrderedContainer

val inconsistent : t -> bool

val tags : t -> Tags.t

val tag_pairs : t -> Tagpairs.t

Return a set of pairs representing the identity function over the tags in the constraint set, to be used as preserving tag pairs.

val subst_tags : Tagpairs.t -> t -> t

val generate : ?avoid:Tags.t -> ?augment:bool -> Tags.elt -> Tags.t -> t

generate avoid t ts returns a constraint set that constitutes an inductive hypothesis corresponding to a case in the unfolding of a predicate tagged with t that recursively depends on predicate instances tagged by labels in ts; any freshly generated labels are not contained in avoid. If the optional argumet augment=true is set to false then, no constraints will be generated in the case that ts is empty.

val remove_schema : t -> Tags.t -> (t * string) option

remove_schema cs used will remove a (nonempty) subset cs' of cs containing tags { t_1, ..., t_n } where at least one t_i does not occur in used such that cs' does not affect the support of cs in the sense that

cs'' |= cs \ cs' if and only if cs'' |= cs for all cs''

The remaining constraint set (i.e. cs \ cs') is returned along with a string that describes the removed set of constraints. If no such set can be found, then None is returned.

Intuitively, this means identifying and removing a tautological schema bounded by some (set of) existential tag(s) (outside of the set used). For example, cs = { t_1 < t, ..., t_n < t } + cs'' where t is an existential tag not occurring in cs'', picks out t as a strict upper bound of the tags t_1, ..., t_n; since such a bound always exists, this is a tautological schema.

val verify_schemas : Tags.t -> t -> bool

verify_schemas ts cs will return true when cs consists entirely of tautological schemas. This is computed by repeatedly trying to remove schemas using remove_schema cs ts until failure; if cs before failure was empty, then true is returned, and false otherwise.

val upper_bounds : ?strict:bool -> Tags.elt -> t -> Tags.t

upper_bounds ?strict t cs returns the set of tags b such that cs contains a constraint of the form t <= b. If the option argument strict=false is set to true then the set of tags b suh that cs contains a constraints of the form t < b is returned.

val close : t -> t

close cs generates the set of all constraints entailed by cs

val all_pairs : t -> Tagpairs.t

all_pairs cs returns all of the tag pairs (a, b) such that a <= b is entailed by some constraint in cs

val prog_pairs : t -> Tagpairs.t

prog_pairs cs returns all of the tag pairs (a, b) such that a <b is entailed by some constraint in cs

val subsumes : t -> t -> bool

subsumes cs cs' checks whether every constraint in cs' also occurs in cs, ignoring any constraints in cs' which are universally valid (e.g. t <= t)

val unify : ?total:bool ->
       ?inverse:bool ->
       ?update_check:Tagpairs.t Unification.state_update Fun.predicate ->
       (Tagpairs.t, 'a, t) Unification.cps_unifier

unify check cs cs' cont init_state calculates a (minimal) extension theta of init_state such that subsumes cs' (subst_tags theta cs) returns true, then passes it to cont and returns the resulting (optional) value. If the value of the optional argument total=false is set to true then subsumes (subst_tags theta cs) cs' will be true of the result also. If the value of the optional argument inverse=false is set to true then theta is returned such that subsumes (subst_tags theta cs') cs is true instead.

val biunify : ?total:bool ->
       ?update_check:(Tagpairs.t * Tagpairs.t) Unification.state_update
                     Fun.predicate ->
       (Tagpairs.t * Tagpairs.t, 'a, t) Unification.cps_unifier

val mk_update_check : (Tagpairs.t * (Tags.Elt.t * Tags.Elt.t)) Fun.predicate ->
       (Tagpairs.t * Tagpairs.t) Fun.predicate

val parse : (t, 'a) MParser.parser

val of_string : string -> t

val to_string_list : t -> string list

val to_string : t -> string

val to_melt : t -> Latex.t