| Not of 'a t
Note that the sexps are not directly inferred from the type above -- there are lots of
fancy shortcuts. Also, the sexps for
'a must not look anything like blang sexps.
t_of_sexp will fail.
function true -> true_ | false -> false_
constant_value t = Some b iff
t = constant b
gather_conjuncts t gathers up all toplevel conjuncts in
t. For example,
gather_conjuncts (and_ ts) = ts
gather_conjuncts (And (t1, t2)) = gather_conjuncts t1 @ gather_conjuncts t2
gather_conjuncts True = 
gather_conjuncts t = [t]when
And (_, _)nor
gather_disjuncts t gathers up all toplevel disjuncts in
t. For example,
gather_disjuncts (or_ ts) = ts
gather_disjuncts (Or (t1, t2)) = gather_disjuncts t1 @ gather_disjuncts t2
gather_disjuncts False = 
gather_disjuncts t = [t]when
Or (_, _)nor
Checks whether the provided element is there, using polymorphic compare if
is not provided
fold t ~init ~f returns
f (... f (f (f init e1) e2) e3 ...) en, where
are the elements of
true if and only if there exists an element for which the provided
function evaluates to
true. This is a short-circuiting operation.
true if and only if the provided function evaluates to
true for all
elements. This is a short-circuiting operation.
Returns the number of elements for which the provided function evaluates to true.
Returns as an
option the first element for which
f evaluates to true.
Returns the first evaluation of
f that returns
Some, and returns
None if there
is no such element.
Returns a minimum (resp maximum) element from the collection using the provided
cmp function, or
None if the collection is empty. In case of a tie, the first
element encountered while traversing the collection is returned. The implementation
fold so it has the same complexity as
A monad is an abstraction of the concept of sequencing of computations. A value of type 'a monad represents a computation that returns a value of type 'a.
return v returns the (trivial) computation that returns v.
values t forms the list containing every
Base v is a subexpression of
eval t f evaluates the proposition
t relative to an environment
f that assigns truth values to base propositions.
eval_set ~universe set_of_base expression returns the subset of elements
universe that satisfy
eval expression (fun base -> Set.mem (set_of_base base) e).
eval_set assumes, but does not verify, that
set_of_base always returns a subset of
universe. If this doesn't hold, then
eval_set's result may contain elements not
And set1 set2 represent the elements that are both in set1 and set2, thus in the
intersection of set1 and set2. Symmetrically,
Or set1 set2 represent the union of
set1 and set2.
specialize t f partially evaluates
t according to a
f of the values of base propositions.
The following laws (at least partially) characterize its behavior.
specialize t (fun _ -> `Unknown) = t
specialize t (fun x -> `Known (f x)) = constant (eval t f)
List.for_all (values (specialize t g)) ~f:(fun x -> g x = `Unknown)
if List.for_all (values t) ~f:(fun x -> match g x with | `Known b -> b = f x | `Unknown -> true) then eval t f = eval (specialize t g) f