Up

Module Blang = Core_kernel.Blang

Signature

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.

val t_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a t
val sexp_of_t : ('a -> Sexplib.Sexp.t) -> 'a t -> Sexplib.Sexp.t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val bin_read_t : 'a Bin_prot.Read.reader -> 'a t Bin_prot.Read.reader
val __bin_read_t__ : 'a Bin_prot.Read.reader -> (int -> 'a t) Bin_prot.Read.reader
val bin_size_t : 'a Bin_prot.Size.sizer -> 'a t Bin_prot.Size.sizer
val bin_write_t : 'a Bin_prot.Write.writer -> 'a t Bin_prot.Write.writer
smart constructors that simplify away constants whenever possible
val base : 'a -> 'a t
val true_ : _ t
val false_ : _ t
val constant : bool -> _ t

function true -> true_ | false -> false_

val not_ : 'a t -> 'a t

function true -> true_ | false -> false_

val and_ : 'a t list -> 'a t

n-ary And

val or_ : 'a t list -> 'a t

n-ary And

n-ary Or

val if_ : 'a t -> 'a t -> 'a t -> 'a t

n-ary Or

if_ if then else

val constant_value : 'a t -> bool option

constant_value t = Some b iff t = constant b

val gather_conjuncts : 'a t -> 'a t list

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 list

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
include Core_kernel.Container.S1 with type 'a t := 'a t
type 'a t
val mem : ?equal:('a -> 'a -> bool) -> 'a t -> 'a -> bool

Checks whether the provided element is there, using polymorphic compare if equal is not provided

val length : 'a t -> int
val is_empty : 'a t -> bool
val iter : 'a t -> f:('a -> unit) -> unit
val fold : 'a t -> init:'accum -> f:('accum -> 'a -> 'accum) -> 'accum

fold t ~init ~f returns f (... f (f (f init e1) e2) e3 ...) en, where e1..en are the elements of t

val exists : 'a t -> f:('a -> bool) -> bool

Returns 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) -> bool

Returns 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) -> int

Returns the number of elements for which the provided function evaluates to true.

val sum : (module Commutative_group.S with type t = 'sum) -> 'a t -> f:('a -> 'sum) -> 'sum

Returns the sum of f i for i in the container

val find : 'a t -> f:('a -> bool) -> 'a option

Returns as an option the first element for which f evaluates to true.

val find_map : 'a t -> f:('a -> 'b option) -> 'b option

Returns the first evaluation of f that returns Some, and returns None if there is no such element.

val to_list : 'a t -> 'a list
val to_array : 'a t -> 'a array
val min_elt : 'a t -> cmp:('a -> 'a -> int) -> 'a option

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.

val max_elt : 'a t -> cmp:('a -> 'a -> int) -> 'a option
include Core_kernel.Std_internal.Monad with type 'a t := 'a t
type 'a t
include Monad_intf.S_without_syntax with type 'a t := 'a t
type 'a t

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.

include Monad_intf.Infix with type 'a t := 'a t
type 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t

t >>= f returns a computation that sequences the computations represented by two monad elements. The resulting computation first does t to yield a value v, and then runs the computation returned by f v.

val (>>|) : 'a t -> ('a -> 'b) -> 'b t

t >>| f is t >>= (fun a -> return (f a)).

module Monad_infix : Monad_intf.Infix with type 'a t := 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t

bind t f = t >>= f

val return : 'a -> 'a t

return v returns the (trivial) computation that returns v.

val map : 'a t -> f:('a -> 'b) -> 'b t

map t ~f is t >>| f.

val join : 'a t t -> 'a t

join t is t >>= (fun t' -> t').

val ignore_m : 'a t -> unit t

ignore_m t is map t ~f:(fun _ -> ()). ignore_m used to be called ignore, but we decided that was a bad name, because it shadowed the widely used Pervasives.ignore. Some monads still do let ignore = ignore_m for historical reasons.

val all : 'a t list -> 'a list t
val all_ignore : unit t list -> unit t
include Monad_intf.Syntax with type 'a t := 'a t
type 'a t
module Let_syntax : sig .. end
val values : 'a t -> 'a list

values t forms the list containing every v for which Base v is a subexpression of t

val eval : 'a t -> ('a -> bool) -> bool

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) Core_kernel.Std_internal.Set.t Core_kernel.Std_internal.Lazy.t -> ('a -> ('elt, 'comparator) Core_kernel.Std_internal.Set.t) -> 'a t -> ('elt, 'comparator) Core_kernel.Std_internal.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 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.

val specialize : 'a t -> ('a -> [
| `Known of bool
| `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)
  • 
        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
val invariant : 'a t -> unit
module Stable : sig .. end