Module Fact

module Fact: sig .. end

Conjunction of hypotheses.

type parameter = int

module ParameterMap: Map.S  with type key = parameter

type property = fact

type fact = hypothesis Mode.ModeMap.t

type hypothesis =

`\|`	`HFalse`
`\|`	`HConjunction of hypotheses`

type hypotheses = Mode.mode ParameterMap.t

val conjunction : ('a -> hypothesis) -> 'a list -> hypothesis

Conjunction of hypotheses.

val bottom : fact

The least fact is defined as constant Mode.bottom.

val equal : fact -> fact -> bool

Equality.

val leq : fact -> fact -> bool

The lattice ordering.

val join : fact -> fact -> fact

The lattice join (i.e., least upper bound).

val join_many : ('a -> fact) -> 'a list -> fact

val meet : fact -> fact -> fact

The lattice meet. Beware: this operation is defined only when its left-hand argument is a fact of arity zero. (Such a fact is isomorphic to a mode. When both arguments are facts of arity zero, this operation has the same effect as Mode.meet.)

val is_maximal : fact -> bool

Recognition of maximal facts is not performed. This function is provided for the benefit of Fix.

val constant : Mode.mode -> fact

A mode m can be viewed as a fact: every mode m' that is equal to or above m is mapped to true, the empty conjunction, and every mode m' that does not satisfy this is mapped to false.

val implication : Mode.mode -> hypothesis -> fact

implication h m constructs a fact of the form h => m. (More precisely, in this fact, the top mode is mapped to the hypothesis trivial; every (non-top) mode greater than or equal to m is mapped to the hypothesis h; and every other mode is mapped to the hypothesis HFalse.)

val duplicable : hypothesis -> fact

duplicable is implication ModeDuplicable.

val allow_exclusive : fact -> fact

A utility function for extending a fact with the statement ``without any hypotheses, this type is exclusive''.

val disallow_exclusive : fact -> fact

A utility function for removing the possibility that ``this type is exclusive''.

val parameter : parameter -> fact

A fact for a parameter p is a conjunction of implications of the form m p => m, where m ranges over every mode.

val compose : fact -> fact list -> fact

compose fact facts composes a fact of arity n -- i.e. a fact that makes sense in the presence of n parameters -- with n facts about the actual parameters. If these facts have arity k, then the final fact has arity k as well.

val complete : fact -> fact

complete fact completes an incomplete fact (i.e., a mode map whose domain does not contain all modes) so as to obtain a valid fact. Use with caution.

val print : (parameter -> PPrint.document) ->
       PPrint.document -> fact -> PPrint.document

print param head fact is a textual representation of the fact fact. The function param is used to map a parameter to its textual representation. head is a textual representation of the type that appears in the goals.

val internal_print : fact -> PPrint.document

internal_print fact is a textual representation of the fact fact. Parameters are represented by their number, and there is no head. This is for internal use.