package core_kernel

  1. Overview
  2. Docs
package core_kernel
Legend:
Library
Module
Module type
Parameter
Class
Class type

A simple boolean domain-specific language

type 'a t = private
  1. | True
  2. | False
  3. | And of 'a t * 'a t
  4. | Or of 'a t * 'a t
  5. | Not of 'a t
  6. | If of 'a t * 'a t * 'a t
  7. | 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 ... end
val bin_t : 'a Bin_prot.Type_class.t -> 'a t Bin_prot.Type_class.t
val bin_read_t : 'a Bin_prot.Read.reader -> 'a t Bin_prot.Read.reader
val __bin_read_t__ : 'a Bin_prot.Read.reader -> (Base.Int.t -> 'a t) Bin_prot.Read.reader
val bin_reader_t : 'a Bin_prot.Type_class.reader -> 'a t Bin_prot.Type_class.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
val bin_writer_t : 'a Bin_prot.Type_class.writer -> 'a t Bin_prot.Type_class.writer
val bin_shape_t : Bin_prot.Shape.t -> Bin_prot.Shape.t
val compare : ('a -> 'a -> Base.Int.t) -> 'a t -> 'a t -> Base.Int.t
val hash_fold_t : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a t -> Ppx_hash_lib.Std.Hash.state
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
smart constructors that simplify away constants whenever possible
include Constructors
val base : 'a -> 'a t
val true_ : _ t
val false_ : _ t
val constant : Base.Bool.t -> _ t

function true -> true_ | false -> false_

val not_ : 'a t -> 'a t
val and_ : 'a t Base.List.t -> 'a t

n-ary And

val or_ : 'a t Base.List.t -> 'a t

n-ary Or

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

if_ if then else

module O : sig ... end
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 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
val fold_result : 'a t -> init:'accum -> f:('accum -> 'a -> ('accum, 'e) Base__.Result.t) -> ('accum, 'e) Base__.Result.t
val fold_until : 'a t -> init:'accum -> f:('accum -> 'a -> ('accum, 'stop) Base.Container_intf.Continue_or_stop.t) -> ('accum, 'stop) Base.Container_intf.Finished_or_stopped_early.t
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__.Commutative_group.S 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 -> cmp:('a -> 'a -> int) -> 'a option
val max_elt : 'a t -> cmp:('a -> 'a -> int) -> 'a option

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
module Monad_infix : sig ... end
val bind : 'a t -> f:('a -> 'b t) -> 'b t
val return : 'a -> 'a 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_ignore : unit t list -> unit t
module Let_syntax : sig ... end
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) Base.Set.t Lazy.t -> ('a -> ('elt, 'comparator) Base.Set.t) -> 'a t -> ('elt, 'comparator) Base.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 set1 and set2. 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)
  • 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 -> Base.Unit.t
module Stable : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct