Boolean expressions.
A blang is a boolean expression built up by applying the usual boolean operations to properties that evaluate to true or false in some context.
For example, imagine writing a config file for an application that filters a stream of
integers. Your goal is to keep only those integers that are multiples of either -3 or
5. Using Blang for this task, the code might look like:
module Property = struct
type t =
| Multiple_of of int
| Positive
| Negative
[@@deriving sexp]
let eval t num =
match t with
| Multiple_of n -> num % n = 0
| Positive -> num > 0
| Negative -> num < 0
end
type config = {
keep : Property.t Blang.t;
} [@@deriving sexp]
let config = {
keep = Blang.of_string "(or (and negative (multiple_of 3)) \
\ (and positive (multiple_of 5)))";
}
let keep config num : bool =
Blang.eval config.keep (fun p -> Property.eval p num)Note how positive and negative and multiple_of become operators in a small,
newly-defined boolean expression language that allows you to write statements like
(and negative (multiple_of 3)).
The blang sexp syntax is almost exactly the derived one, except that:
1. Base properties are not marked explicitly. Thus, if your base property type 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)
instead of
(and FOO (and BAR (and BAZ QUX)))
type 'a t = private | True |
| False |
| And of 'a t * 'a t |
| Or of 'a t * 'a t |
| Not of 'a t |
| If of 'a t * 'a t * 'a t |
| Base of 'a |
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.
include sig ... endval bin_t : 'a Bin_prot.Type_class.t ‑> 'a t Bin_prot.Type_class.tval bin_read_t : 'a Bin_prot.Read.reader ‑> 'a t Bin_prot.Read.readerval __bin_read_t__ : 'a Bin_prot.Read.reader ‑> (Core_kernel__.Import.int ‑> 'a t) Bin_prot.Read.readerval bin_reader_t : 'a Bin_prot.Type_class.reader ‑> 'a t Bin_prot.Type_class.readerval bin_size_t : 'a Bin_prot.Size.sizer ‑> 'a t Bin_prot.Size.sizerval bin_write_t : 'a Bin_prot.Write.writer ‑> 'a t Bin_prot.Write.writerval bin_writer_t : 'a Bin_prot.Type_class.writer ‑> 'a t Bin_prot.Type_class.writerval bin_shape_t : Bin_prot.Shape.t ‑> Bin_prot.Shape.tval compare : ('a ‑> 'a ‑> Core_kernel__.Import.int) ‑> 'a t ‑> 'a t ‑> Core_kernel__.Import.intval hash_fold_t : (Base.Hash.state ‑> 'a ‑> Base.Hash.state) ‑> Base.Hash.state ‑> 'a t ‑> Base.Hash.stateval t_of_sexp : (Base.Sexp.t ‑> 'a) ‑> Base.Sexp.t ‑> 'a tval sexp_of_t : ('a ‑> Base.Sexp.t) ‑> 'a t ‑> Base.Sexp.tmodule type Constructors : sig ... endmodule O : sig ... endval constant_value : 'a t ‑> Core_kernel__.Import.bool Core_kernel__.Import.optionconstant_value t = Some b iff t = constant b
The following two functions are useful when one wants to pretend
that '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 ...
| ...val gather_conjuncts : 'a t ‑> 'a t Core_kernel__.Import.listgather_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 Trueval gather_disjuncts : 'a t ‑> 'a t Core_kernel__.Import.listgather_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 Falseinclude Core_kernel.Container.S1 with type a t := a tval mem : 'a t ‑> 'a ‑> equal:('a ‑> 'a ‑> bool) ‑> boolChecks whether the provided element is there, using equal.
val length : 'a t ‑> intval is_empty : 'a t ‑> boolval iter : 'a t ‑> f:('a ‑> unit) ‑> unitval fold : 'a t ‑> init:'accum ‑> f:('accum ‑> 'a ‑> 'accum) ‑> 'accumfold t ~init ~f returns f (... f (f (f init e1) e2) e3 ...) en, where e1..en
are the elements of t
val fold_result : 'a t ‑> init:'accum ‑> f:('accum ‑> 'a ‑> ('accum, 'e) Base.Result.t) ‑> ('accum, 'e) Base.Result.tfold_result t ~init ~f is a short-circuiting version of fold that runs in the
Result monad. If f returns an Error _, that value is returned without any
additional invocations of f.
val fold_until : 'a t ‑> init:'accum ‑> f:('accum ‑> 'a ‑> ('accum, 'final) Base__.Container_intf.Continue_or_stop.t) ‑> finish:('accum ‑> 'final) ‑> 'finalfold_until t ~init ~f ~finish is a short-circuiting version of fold. If f
returns Stop _ the computation ceases and results in that value. If f returns
Continue _, the fold will proceed. If f never returns Stop _, the final result
is computed by finish.
val exists : 'a t ‑> f:('a ‑> bool) ‑> boolReturns true if and only if there exists an element for which the provided
function evaluates to true. This is a short-circuiting operation.
val for_all : 'a t ‑> f:('a ‑> bool) ‑> boolReturns true if and only if the provided function evaluates to true for all
elements. This is a short-circuiting operation.
val count : 'a t ‑> f:('a ‑> bool) ‑> intReturns the number of elements for which the provided function evaluates to true.
val sum : (module Base.Commutative_group.S with type t = 'sum) ‑> 'a t ‑> f:('a ‑> 'sum) ‑> 'sumReturns the sum of f i for all i in the container.
val find : 'a t ‑> f:('a ‑> bool) ‑> 'a optionReturns as an option the first element for which f evaluates to true.
val find_map : 'a t ‑> f:('a ‑> 'b option) ‑> 'b optionReturns the first evaluation of f that returns Some, and returns None if there
is no such element.
val to_list : 'a t ‑> 'a listval to_array : 'a t ‑> 'a arrayval min_elt : 'a t ‑> compare:('a ‑> 'a ‑> int) ‑> 'a optionReturns a minimum (resp maximum) element from the collection using the provided
compare 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.
val max_elt : 'a t ‑> compare:('a ‑> 'a ‑> int) ‑> 'a optionBlang.t sports a substitution monad:
return v is Base v (think of v as a variable)bind t f replaces every Base v in t with f v
(think of v as a variable and f as specifying the term to
substitute for each variable)Note: bind t f does short-circuiting, so f may not be called on every variable in
t.
include Core_kernel__.Std_internal.Monad with type a t := a tinclude Base__.Monad_intf.S_without_syntax with type a t := a tinclude Base__.Monad_intf.Infix with type a t := a tmodule Monad_infix : Base__.Monad_intf.Infix with type a t := a tval values : 'a t ‑> 'a Core_kernel__.Import.listvalues t forms the list containing every v
for which Base v is a subexpression of t
val eval : 'a t ‑> ('a ‑> Core_kernel__.Import.bool) ‑> Core_kernel__.Import.booleval t f evaluates the proposition t relative to an environment
f that assigns truth values to base propositions.
val eval_set : universe:('elt, 'comparator) Core_kernel.Set.t Core_kernel.Lazy.t ‑> ('a ‑> ('elt, 'comparator) Core_kernel.Set.t) ‑> 'a t ‑> ('elt, 'comparator) Core_kernel.Set.teval_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 represents the elements that are both in set1 and set2, thus in
the intersection of the two sets. Symmetrically, Or set1 set2 represents the union
of set1 and set2.
val specialize : 'a t ‑> ('a ‑> [ `Known of Core_kernel__.Import.bool | `Unknown ]) ‑> 'a tspecialize 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) fval invariant : 'a t ‑> Core_kernel__.Import.unitmodule Stable : sig ... end