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) = ts
gather_conjuncts (And (t1, t2)) = gather_conjuncts t1 @ gather_conjuncts t2
gather_conjuncts True = []
gather_conjuncts t = [t]
when t
matches neither And (_, _)
nor True
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 t
matches neither Or (_, _)
nor False
Checks 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) = 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