A simple boolean domain-specific language
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.
Otherwise 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) = tsgather_conjuncts (And (t1, t2)) = gather_conjuncts t1 @ gather_conjuncts t2gather_conjuncts True = [] gather_conjuncts t = [t] when t matches neither And (_, _) nor Truegather_disjuncts t gathers up all toplevel disjuncts in t. For example,
gather_disjuncts (or_ ts) = tsgather_disjuncts (Or (t1, t2)) = gather_disjuncts t1 @ gather_disjuncts t2gather_disjuncts False = [] gather_disjuncts t = [t] when t matches neither Or (_, _) nor FalseChecks whether the provided element is there, using polymorphic compare if equal
is not provided
fold t ~init ~f returns f (... f (f (f init e1) e2) e3 ...) en, where e1..en
are the elements of t
Returns true if and only if there exists an element for which the provided
function evaluates to true. This is a short-circuiting operation.
Returns 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
uses fold so it has the same complexity as fold.
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 v
for which Base v is a subexpression of t
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 e in
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
in universe.
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
perhaps-incomplete assignment f of the values of base propositions.
The following laws (at least partially) characterize its behavior.
specialize t (fun _ -> `Unknown) = tspecialize 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