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.
Usage
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.t_of_sexp
Property.t_of_sexp
(Sexp.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))
.
Blang sexp syntax
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)))
If you want to see the derived sexp, use Raw.sexp_of_t
.
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 below -- there are lots of fancy shortcuts. Also, the sexps for 'a
must not look anything like blang sexps. Otherwise t_of_sexp
will fail. The directly inferred sexps are available via Raw.sexp_of_t
.
include Bin_prot.Binable.S1 with type +'a t := 'a t
val bin_shape_t : Bin_prot__.Shape.t -> Bin_prot__.Shape.t
val bin_size_t : ('a, 'a t) Bin_prot__.Size.sizer1
val bin_write_t : ('a, 'a t) Bin_prot__.Write.writer1
val bin_read_t : ('a, 'a t) Bin_prot__.Read.reader1
val __bin_read_t__ : ('a, int -> 'a t) Bin_prot__.Read.reader1
val bin_writer_t : ('a, 'a t) Bin_prot__.Type_class.S1.writer
val bin_reader_t : ('a, 'a t) Bin_prot__.Type_class.S1.reader
val bin_t : ('a, 'a t) Bin_prot__.Type_class.S1.t
include Ppx_compare_lib.Comparable.S1 with type +'a t := 'a t
val compare :
'a Base__Ppx_compare_lib.compare ->
'a t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S1 with type +'a t := 'a t
val equal : 'a Base__Ppx_compare_lib.equal -> 'a t Base__Ppx_compare_lib.equal
include Ppx_hash_lib.Hashable.S1 with type +'a t := 'a t
val hash_fold_t :
'a Base__Ppx_hash_lib.hash_fold ->
'a t Base__Ppx_hash_lib.hash_fold
include Sexplib0.Sexpable.S1 with type +'a t := 'a t
val t_of_sexp : (Sexplib0__.Sexp.t -> 'a) -> Sexplib0__.Sexp.t -> 'a t
val sexp_of_t : ('a -> Sexplib0__.Sexp.t) -> 'a t -> Sexplib0__.Sexp.t
val t_sexp_grammar : 'a Sexplib0.Sexp_grammar.t -> 'a t Sexplib0.Sexp_grammar.t
include Typerep_lib.Typerepable.S1 with type +'a t := 'a t
val typerep_of_t :
'a Typerep_lib.Std_internal.Typerep.t ->
'a t Typerep_lib.Std_internal.Typerep.t
val typename_of_t : 'a Typerep_lib.Typename.t -> 'a t Typerep_lib.Typename.t
Raw
provides the automatically derived sexp_of_t
, useful in debugging the actual structure of the blang.
Smart constructors that simplify away constants whenever possible
include Constructors
val constant : Base.Bool.t -> _ t
function true -> true_ | false -> false_
val and_ : 'a t Base.List.t -> 'a t
val or_ : 'a t Base.List.t -> 'a t
val if_ : 'a t -> 'a t -> 'a t -> 'a t
val constant_value : 'a t -> Base.Bool.t Base.Option.t
constant_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 Base.List.t
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
val gather_disjuncts : 'a t -> 'a t Base.List.t
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
val mem : 'a t -> 'a -> equal:('a -> 'a -> bool) -> bool
val is_empty : 'a t -> bool
val iter : 'a t -> f:('a -> unit) -> unit
val fold : 'a t -> init:'acc -> f:('acc -> 'a -> 'acc) -> 'acc
val fold_result :
'a t ->
init:'acc ->
f:('acc -> 'a -> ('acc, 'e) Base__.Result.t) ->
('acc, 'e) Base__.Result.t
val fold_until :
'a t ->
init:'acc ->
f:('acc -> 'a -> ('acc, 'final) Base__Container_intf.Continue_or_stop.t) ->
finish:('acc -> 'final) ->
'final
val exists : 'a t -> f:('a -> bool) -> bool
val for_all : 'a t -> f:('a -> bool) -> bool
val count : 'a t -> f:('a -> bool) -> int
val sum :
(module Base__Container_intf.Summable with type t = 'sum) ->
'a t ->
f:('a -> 'sum) ->
'sum
val find : 'a t -> f:('a -> bool) -> 'a option
val find_map : 'a t -> f:('a -> 'b option) -> 'b option
val to_list : 'a t -> 'a list
val to_array : 'a t -> 'a array
val min_elt : 'a t -> compare:('a -> 'a -> int) -> 'a option
val max_elt : 'a t -> compare:('a -> 'a -> int) -> 'a option
include Quickcheckable.S1 with type 'a t := 'a t
val quickcheck_generator :
'a Base_quickcheck.Generator.t ->
'a t Base_quickcheck.Generator.t
val quickcheck_observer :
'a Base_quickcheck.Observer.t ->
'a t Base_quickcheck.Observer.t
val quickcheck_shrinker :
'a Base_quickcheck.Shrinker.t ->
'a t Base_quickcheck.Shrinker.t
Blang.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
.
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val (>>|) : 'a t -> ('a -> 'b) -> 'b t
val bind : 'a t -> f:('a -> 'b t) -> 'b t
val map : 'a t -> f:('a -> 'b) -> 'b t
val join : 'a t t -> 'a t
val ignore_m : 'a t -> unit t
val all : 'a t list -> 'a list t
val all_unit : unit t list -> unit t
val values : 'a t -> 'a Base.List.t
values t
forms the list containing every v
for which Base v
is a subexpression of t
val eval : 'a t -> ('a -> Base.Bool.t) -> Base.Bool.t
eval t f
evaluates the proposition t
relative to an environment f
that assigns truth values to base propositions.
val eval_set :
universe:('elt, 'comparator) Set.t Lazy.t ->
('a -> ('elt, 'comparator) Set.t) ->
'a t ->
('elt, 'comparator) Set.t
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
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 Base.Bool.t | `Unknown ]) -> 'a t
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)
Generalizes some of the blang operations above to work in a monad.
val invariant : 'a t -> Base.Unit.t