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 ` |

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.