A simple boolean domain-specific language
Blang provides infrastructure for writing simple boolean DSLs. All expressions in a Blang language evaluate to a bool. The language is parameterized over another language of base propositions.
The syntax is almost exactly the obvious s-expression syntax, except that:
1. Base elements are not marked explicitly. Thus, if your base language has elements FOO, BAR, etc., then you could write the following Blang s-expressions:
FOO (and FOO BAR) (if FOO BAR BAZ)
and so on. Note that this gets in the way of using the blang "keywords" in your value language.
2. And and Or take a variable number of arguments, so that one can (and probably should) write
(and FOO BAR BAZ QUX)
(and FOO (and BAR (and BAZ QUX)))
|(*||Note that the sexps are not directly inferred from the type above -- there are lots of
fancy shortcuts. Also, the sexps for ||*)|
The following two functions are useful when one wants to pretend
'a t has constructors And and Or of type
'a t list -> 'a t.
The pattern of use is
match t with | ... | And (_, _) as t -> let ts = gather_conjuncts t in ... | Or (_, _) as t -> let ts = gather_disjuncts t in ... | ...
or, in case you also want to handle True (resp. False) as a special case of conjunction (disjunction)
match t with | ... | True | And (_, _) as t -> let ts = gather_conjuncts t in ... | False | Or (_, _) as t -> let ts = gather_disjuncts t in ... | ...
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
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.
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