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