summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml2
-rw-r--r--lib/bigint.mli2
-rw-r--r--lib/bstack.ml2
-rw-r--r--lib/bstack.mli2
-rw-r--r--lib/dyn.ml2
-rw-r--r--lib/dyn.mli2
-rw-r--r--lib/edit.ml2
-rw-r--r--lib/edit.mli2
-rw-r--r--lib/explore.ml2
-rw-r--r--lib/explore.mli2
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli4
-rw-r--r--lib/gmap.ml2
-rw-r--r--lib/gmap.mli2
-rw-r--r--lib/gmapl.ml2
-rw-r--r--lib/gmapl.mli2
-rw-r--r--lib/gset.ml2
-rw-r--r--lib/gset.mli2
-rw-r--r--lib/hashcons.ml2
-rw-r--r--lib/hashcons.mli2
-rw-r--r--lib/heap.ml2
-rw-r--r--lib/heap.mli2
-rw-r--r--lib/option.ml2
-rw-r--r--lib/option.mli2
-rw-r--r--lib/pp.ml42
-rw-r--r--lib/pp.mli2
-rw-r--r--lib/pp_control.ml2
-rw-r--r--lib/pp_control.mli2
-rw-r--r--lib/predicate.ml2
-rw-r--r--lib/predicate.mli2
-rw-r--r--lib/profile.ml2
-rw-r--r--lib/profile.mli2
-rw-r--r--lib/rtree.ml2
-rw-r--r--lib/rtree.mli2
-rw-r--r--lib/system.ml2
-rw-r--r--lib/system.mli2
-rw-r--r--lib/tlm.ml2
-rw-r--r--lib/tlm.mli2
-rw-r--r--lib/util.ml31
-rw-r--r--lib/util.mli21
40 files changed, 86 insertions, 46 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 084189a8..b33baa83 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: bigint.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(*i*)
open Pp
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 01bfedac..48e36875 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: bigint.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Pp
diff --git a/lib/bstack.ml b/lib/bstack.ml
index 6330afec..4afbe41e 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: bstack.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Queues of a given length *)
diff --git a/lib/bstack.mli b/lib/bstack.mli
index 057bace3..b34d18d7 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: bstack.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 09c9a38c..8a2a467a 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: dyn.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Util
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 290907b1..512baf7f 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: dyn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Dynamics. Use with extreme care. Not for kids. *)
diff --git a/lib/edit.ml b/lib/edit.ml
index 18d8d8dc..edfde186 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: edit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/lib/edit.mli b/lib/edit.mli
index 4274846e..3d6f98ab 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: edit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* The type of editors.
* An editor is a finite map, ['a -> 'b], which knows how to apply
diff --git a/lib/explore.ml b/lib/explore.ml
index c20726aa..c6a40e04 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: explore.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Format
diff --git a/lib/explore.mli b/lib/explore.mli
index b7fe7a5a..f8180577 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: explore.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*s Search strategies. *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 2961d83f..de70b6a6 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: flags.ml 13358 2010-07-29 23:10:17Z herbelin $ i*)
let with_option o f x =
let old = !o in o:=true;
@@ -35,8 +35,6 @@ let dont_load_proofs = ref false
let raw_print = ref false
-let unicode_syntax = ref false
-
(* Compatibility mode *)
type compat_version = V8_2
diff --git a/lib/flags.mli b/lib/flags.mli
index 87c8e792..75cfc96d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: flags.mli 13358 2010-07-29 23:10:17Z herbelin $ i*)
(* Global options of the system. *)
@@ -27,8 +27,6 @@ val dont_load_proofs : bool ref
val raw_print : bool ref
-val unicode_syntax : bool ref
-
type compat_version = V8_2
val compat_version : compat_version option ref
val version_strictly_greater : compat_version -> bool
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 41a57276..1544dacc 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: gmap.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Maps using the generic comparison function of ocaml. Code borrowed from
the ocaml standard library (Copyright 1996, INRIA). *)
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 3e125a60..379aa63f 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: gmap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Maps using the generic comparison function of ocaml. Same interface as
the module [Map] from the ocaml standard library. *)
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 87804bb5..5f539971 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: gmapl.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Util
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index 95a80a29..7c5d0ceb 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: gmapl.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Maps from ['a] to lists of ['b]. *)
diff --git a/lib/gset.ml b/lib/gset.ml
index fca46496..dc88127e 100644
--- a/lib/gset.ml
+++ b/lib/gset.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: gset.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Sets using the generic comparison function of ocaml. Code borrowed from
the ocaml standard library. *)
diff --git a/lib/gset.mli b/lib/gset.mli
index 570ce5e0..911ff3f0 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: gset.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Sets using the generic comparison function of ocaml. Same interface as
the module [Set] from the ocaml standard library. *)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 6841132e..1ebf8773 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: hashcons.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Hash consing of datastructures *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 3fbf3c9b..0ce4d3b9 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: hashcons.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Generic hash-consing. *)
diff --git a/lib/heap.ml b/lib/heap.ml
index 5f70b5f2..47cfb46f 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: heap.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(*s Heaps *)
diff --git a/lib/heap.mli b/lib/heap.mli
index edafef5d..e46f97ac 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: heap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Heaps *)
diff --git a/lib/option.ml b/lib/option.ml
index e5b9ecd3..850d7306 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: option.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Module implementing basic combinators for OCaml option type.
It tries follow closely the style of OCaml standard library.
diff --git a/lib/option.mli b/lib/option.mli
index 03e989d3..c76deb3c 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: option.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
(** Module implementing basic combinators for OCaml option type.
It tries follow closely the style of OCaml standard library.
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 0983e5e7..87c12fba 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: pp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp_control
diff --git a/lib/pp.mli b/lib/pp.mli
index 03aa1f9c..4b8e5a29 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: pp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Pp_control
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 54e8fa0c..507a54a7 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: pp_control.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Parameters of pretty-printing *)
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index c1540e72..bf95bb5e 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: pp_control.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Parameters of pretty-printing. *)
diff --git a/lib/predicate.ml b/lib/predicate.ml
index af66c0f2..506a87c9 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,7 +10,7 @@
(* *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: predicate.ml 12337 2009-09-17 15:58:14Z glondu $ *)
(* Sets over ordered types *)
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 41d5399b..85596fea 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,5 +1,5 @@
-(*i $Id$ i*)
+(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
(* Module [Pred]: sets over infinite ordered types with complement. *)
diff --git a/lib/profile.ml b/lib/profile.ml
index b612f31d..87bfe624 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: profile.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Gc
diff --git a/lib/profile.mli b/lib/profile.mli
index bde8587c..e61aba85 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: profile.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*s This program is a small time and allocation profiler for Objective Caml *)
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 55b00a93..a7428e12 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: rtree.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Util
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 3013199a..17cccfc8 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: rtree.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Type of regular tree with nodes labelled by values of type 'a *)
(* The implementation uses de Bruijn indices, so binding capture
diff --git a/lib/system.ml b/lib/system.ml
index 7e7dfbcb..17d211f8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: system.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/lib/system.mli b/lib/system.mli
index 44314c23..971a5c86 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: system.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*s Files and load paths. Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 098a1247..aad4d363 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: tlm.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 95a788ff..db3d7dd3 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: tlm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Tries. This module implements a data structure [('a,'b) t] mapping lists
of values of type ['a] to sets (as lists) of values of type ['b]. *)
diff --git a/lib/util.ml b/lib/util.ml
index 6d04c3c2..851afc60 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id$ *)
+(* $Id: util.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
open Pp
@@ -43,6 +43,7 @@ let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
@@ -66,6 +67,11 @@ let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a
+(* Projection operator *)
+
+let down_fst f x = f (fst x)
+let down_snd f x = f (snd x)
+
(* Characters *)
let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
@@ -700,6 +706,16 @@ let list_split_when p =
in
split_when_loop []
+(* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
+ [l1] satisfy [p] and elements of [l2] do not *)
+let list_split_by p =
+ let rec split_by_loop = function
+ | [] -> ([],[])
+ | a::l ->
+ let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
+ in
+ split_by_loop
+
let rec list_split3 = function
| [] -> ([], [], [])
| (x,y,z)::l ->
@@ -828,6 +844,13 @@ let list_cartesians op init ll =
let list_combinations l = list_cartesians (fun x l -> x::l) [] l
+let rec list_combine3 x y z =
+ match x, y, z with
+ | [], [], [] -> []
+ | (x :: xs), (y :: ys), (z :: zs) ->
+ (x, y, z) :: list_combine3 xs ys zs
+ | _, _, _ -> raise (Invalid_argument "list_combine3")
+
(* Keep only those products that do not return None *)
let rec list_cartesian_filter op l1 l2 =
@@ -1171,6 +1194,12 @@ let iterate_for a b f x =
let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
iterate a x
+(* Delayed computations *)
+
+type 'a delayed = unit -> 'a
+
+let delayed_force f = f ()
+
(* Misc *)
type ('a,'b) union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index cd8e3135..00c73a1f 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i $Id$ i*)
+(*i $Id: util.mli 13357 2010-07-29 22:59:55Z herbelin $ i*)
(*i*)
open Pp
@@ -52,6 +52,7 @@ val invalid_arg_loc : loc * string -> 'a
val join_loc : loc -> loc -> loc
val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+val down_located : ('a -> 'b) -> 'a located -> 'b
(* Like [Exc_located], but specifies the outermost file read, the
input buffer associated to the location of the error (or the module name
@@ -64,6 +65,11 @@ exception Error_in_file of string * (bool * string * loc) * exn
val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+(* Going down pairs *)
+
+val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
+val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
+
(* Mapping under triple *)
val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
@@ -170,6 +176,7 @@ val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
val list_subset : 'a list -> 'a list -> bool
val list_split_at : int -> 'a list -> 'a list*'a list
val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
val list_firstn : int -> 'a list -> 'a list
@@ -202,7 +209,9 @@ val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
(* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
val list_combinations : 'a list list -> 'a list list
-(* Keep only those products that do not return None *)
+val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+
+(** Keep only those products that do not return None *)
val list_cartesian_filter :
('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
val list_cartesians_filter :
@@ -272,7 +281,13 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
-(*s Misc. *)
+(** {6 Delayed computations. } *)
+
+type 'a delayed = unit -> 'a
+
+val delayed_force : 'a delayed -> 'a
+
+(** {6 Misc. } *)
type ('a,'b) union = Inl of 'a | Inr of 'b
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 05:09:50 +0000