summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/error_format.ml7
-rw-r--r--src/jib/jib_smt.ml171
-rw-r--r--src/property.ml121
-rw-r--r--src/property.mli89
-rw-r--r--src/reporting.ml4
-rw-r--r--src/rewrites.ml5
-rw-r--r--src/sail.ml13
-rw-r--r--src/specialize.ml1
-rw-r--r--src/util.ml8
-rw-r--r--src/util.mli2
10 files changed, 325 insertions, 96 deletions
diff --git a/src/error_format.ml b/src/error_format.ml
index 8e00c2b7..672373a2 100644
--- a/src/error_format.ml
+++ b/src/error_format.ml
@@ -50,7 +50,10 @@ let underline_double_from color cnum_from eol =
Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (eol - cnum_from - 1) '-')))
let underline_double_to color cnum_to =
- Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
+ if cnum_to = 0 then
+ Util.(clear (color "^"))
+ else
+ Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
let format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf =
skip_lines in_chan (lnum_from - 1);
@@ -85,7 +88,7 @@ let format_code_double fname lnum_from cnum_from lnum_to cnum_to contents ppf =
begin
try format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf; close_in in_chan
with
- | _ -> close_in_noerr in_chan; ()
+ | exn -> close_in_noerr in_chan; ()
end
with
| _ -> ()
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 23ea6706..af2c7284 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -847,7 +847,7 @@ let smt_instr env =
let checks =
Stack.fold (fun checks -> function (Define_const (name, _, _) as def) -> (name, def) :: checks | _ -> assert false) [] overflow_checks
in
- List.map snd checks @ [Assert (Fn ("and", Var (zencode_name id) :: List.map (fun check -> Var (fst check)) checks))]
+ List.map snd checks @ [Assert (Fn ("and", Fn ("not", [Var (zencode_name id)]) :: List.map (fun check -> Var (fst check)) checks))]
| I_aux (I_clear _, _) -> []
@@ -879,60 +879,6 @@ let rec find_function id = function
find_function id cdefs
| [] -> None
-let smt_cdef stack env all_cdefs = function
- | CDEF_spec (function_id, arg_ctyps, ret_ctyp)
- when string_of_id function_id = "check_sat" ->
- begin match find_function function_id all_cdefs with
- | Some (None, args, instrs) ->
- let open Jib_ssa in
- let smt_args =
- List.map2 (fun id ctyp -> declare_const (Name (id, 0)) ctyp) args arg_ctyps
- in
- push_smt_defs stack smt_args;
-
- let instrs =
- let open Jib_optimize in
- instrs
- (* |> optimize_unit *)
- |> inline all_cdefs (fun _ -> true)
- |> flatten_instrs
- |> remove_pointless_goto
- in
-
- let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
- prerr_endline str;
-
- let start, cfg = ssa instrs in
- let chan = open_out "smt_ssa.gv" in
- make_dot chan cfg;
- close_out chan;
-
- let visit_order = topsort cfg in
-
- List.iter (fun n ->
- begin match get_vertex cfg n with
- | None -> ()
- | Some ((ssanodes, cfnode), preds, succs) ->
- let muxers =
- ssanodes |> List.map (smt_ssanode env cfg preds) |> List.concat
- in
- let basic_block = smt_cfnode all_cdefs env cfnode in
- push_smt_defs stack muxers;
- push_smt_defs stack basic_block;
- end
- ) visit_order
-
- | _ -> failwith "Bad function body"
- end
- | _ -> ()
-
-let rec smt_cdefs stack env ast =
- function
- | cdef :: cdefs ->
- smt_cdef stack env ast cdef;
- smt_cdefs stack env ast cdefs
- | [] -> ()
-
let optimize_smt stack =
let stack' = Stack.create () in
let uses = Hashtbl.create (Stack.length stack) in
@@ -998,7 +944,92 @@ let optimize_smt stack =
Stack.iter constant_propagate stack';
queue
-let generate_smt out_chan env ast =
+(** [smt_header stack cdefs] pushes all the type declarations required
+ for cdefs onto the SMT stack *)
+let smt_header stack cdefs =
+ push_smt_defs stack
+ [declare_datatypes (mk_enum "Unit" ["unit"]);
+ Declare_tuple 2;
+ Declare_tuple 3;
+ Declare_tuple 4;
+ Declare_tuple 5;
+ declare_datatypes (mk_record "Bits" [("len", Bitvec !lbits_index);
+ ("contents", Bitvec (lbits_size ()))])
+
+ ];
+ let smt_type_defs = List.concat (generate_ctype_defs cdefs) in
+ push_smt_defs stack smt_type_defs
+
+let smt_cdef props name_file env all_cdefs = function
+ | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
+ begin match find_function function_id all_cdefs with
+ | Some (None, args, instrs) ->
+ let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in
+
+ let stack = Stack.create () in
+
+ smt_header stack all_cdefs;
+ let smt_args =
+ List.map2 (fun id ctyp -> declare_const (Name (id, 0)) ctyp) args arg_ctyps
+ in
+ push_smt_defs stack smt_args;
+
+ let instrs =
+ let open Jib_optimize in
+ instrs
+ (* |> optimize_unit *)
+ |> inline all_cdefs (fun _ -> true)
+ |> flatten_instrs
+ |> remove_pointless_goto
+ in
+
+ (* let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
+ prerr_endline str; *)
+
+ let open Jib_ssa in
+ let start, cfg = ssa instrs in
+ (* let chan = open_out "smt_ssa.gv" in
+ make_dot chan cfg;
+ close_out chan; *)
+
+ let visit_order = topsort cfg in
+
+ List.iter (fun n ->
+ begin match get_vertex cfg n with
+ | None -> ()
+ | Some ((ssanodes, cfnode), preds, succs) ->
+ let muxers =
+ ssanodes |> List.map (smt_ssanode env cfg preds) |> List.concat
+ in
+ let basic_block = smt_cfnode all_cdefs env cfnode in
+ push_smt_defs stack muxers;
+ push_smt_defs stack basic_block;
+ end
+ ) visit_order;
+
+ let out_chan = open_out (name_file (string_of_id function_id)) in
+ output_string out_chan "(set-logic QF_AUFBVDT)\n";
+
+ (* let stack' = Stack.create () in
+ Stack.iter (fun def -> Stack.push def stack') stack;
+ Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack'; *)
+ let queue = optimize_smt stack in
+ Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
+
+ output_string out_chan "(check-sat)\n"
+
+ | _ -> failwith "Bad function body"
+ end
+ | _ -> ()
+
+let rec smt_cdefs props name_file env ast =
+ function
+ | cdef :: cdefs ->
+ smt_cdef props name_file env ast cdef;
+ smt_cdefs props name_file env ast cdefs
+ | [] -> ()
+
+let generate_smt props name_file env ast =
try
let open Jib_compile in
let ctx =
@@ -1011,33 +1042,7 @@ let generate_smt out_chan env ast =
let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true } ast in
Profile.finish "Compiling to Jib IR" t;
- let stack = Stack.create () in
-
- (* output_string out_chan "(set-option :produce-models true)\n"; *)
- output_string out_chan "(set-logic QF_AUFBVDT)\n";
- push_smt_defs stack
- [declare_datatypes (mk_enum "Unit" ["unit"]);
- Declare_tuple 2;
- Declare_tuple 3;
- Declare_tuple 4;
- Declare_tuple 5;
- declare_datatypes (mk_record "Bits" [("len", Bitvec !lbits_index);
- ("contents", Bitvec (lbits_size ()))])
-
- ];
-
- let smt_type_defs = List.concat (generate_ctype_defs cdefs) in
- push_smt_defs stack smt_type_defs;
-
- smt_cdefs stack env cdefs cdefs;
-
- (* let stack' = Stack.create () in
- Stack.iter (fun def -> Stack.push def stack') stack;
- Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack'; *)
- let queue = optimize_smt stack in
- Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
-
- output_string out_chan "(check-sat)\n"
+ smt_cdefs props name_file env cdefs cdefs
with
| Type_check.Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err));
diff --git a/src/property.ml b/src/property.ml
new file mode 100644
index 00000000..37212098
--- /dev/null
+++ b/src/property.ml
@@ -0,0 +1,121 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+
+let find_properties (Defs defs) =
+ let rec find_prop acc = function
+ | DEF_pragma (("property" | "counterexample") as prop_type, command, l) :: defs ->
+ begin match Util.find_next (function DEF_spec _ -> true | _ -> false) defs with
+ | _, Some (DEF_spec vs, defs) ->
+ find_prop ((prop_type, command, l, vs) :: acc) defs
+ | _, _ ->
+ raise (Reporting.err_general l "Property is not attached to any function signature")
+ end
+ | def :: defs -> find_prop acc defs
+ | [] -> acc
+ in
+ find_prop [] defs
+ |> List.map (fun ((_, _, _, vs) as prop) -> (id_of_val_spec vs, prop))
+ |> List.fold_left (fun m (id, prop) -> Bindings.add id prop m) Bindings.empty
+
+let add_property_guards props (Defs defs) =
+ let open Type_check in
+ let rec add_property_guards' acc = function
+ | (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, e_opt, funcls), fd_aux) as fdef) as def) :: defs ->
+ begin match Bindings.find_opt (id_of_fundef fdef) props with
+ | Some (_, _, pragma_l, VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (quant, _), _), _, _, _), _)) ->
+ begin match quant_split quant with
+ | _, [] -> add_property_guards' (def :: acc) defs
+ | _, constraints ->
+ let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) =
+ let add_guard exp =
+ let exp' = mk_exp (E_if (mk_exp (E_constraint (nc_not (List.fold_left nc_and nc_true constraints))),
+ mk_lit_exp L_true,
+ strip_exp exp)) in
+ try Type_check.check_exp (env_of exp) exp' (typ_of exp) with
+ | Type_error (_, l, err) ->
+ let msg =
+ "\nType error when generating guard for a property.\n\
+ When generating guards we convert type quantifiers from the function signature\n\
+ into runtime checks so it must be possible to reconstruct the quantifier from\n\
+ the function arguments. For example:\n\n\
+ \
+ function f : forall 'n, 'n <= 100. (x: int('n)) -> bool\n\n\
+ \
+ would cause the runtime check x <= 100 to be added to the function body.\n\
+ To fix this error, ensure that all quantifiers have corresponding function arguments.\n"
+ in
+ raise (Reporting.err_typ pragma_l (Type_error.string_of_type_error err ^ msg))
+ in
+ let mk_funcl p = FCL_aux (FCL_Funcl (id, Pat_aux (p, pexp_aux)), fcl_aux) in
+ match pexp with
+ | Pat_exp (pat, exp) ->
+ mk_funcl (Pat_exp (pat, add_guard exp))
+ | Pat_when (pat, guard, exp) ->
+ mk_funcl (Pat_when (pat, guard, add_guard exp))
+ in
+
+ let funcls = List.map add_constraints_to_funcl funcls in
+ let fdef = FD_aux (FD_function (r_opt, t_opt, e_opt, funcls), fd_aux) in
+
+ add_property_guards' (DEF_fundef fdef :: acc) defs
+ end
+ | None -> add_property_guards' (def :: acc) defs
+ end
+
+ | def :: defs -> add_property_guards' (def :: acc) defs
+ | [] -> List.rev acc
+ in
+ Defs (add_property_guards' [] defs)
+
+let rewrite defs =
+ add_property_guards (find_properties defs) defs
diff --git a/src/property.mli b/src/property.mli
new file mode 100644
index 00000000..fa24377a
--- /dev/null
+++ b/src/property.mli
@@ -0,0 +1,89 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+(** This file implements utilities for dealing with $property and
+ $counterexample pragmas. *)
+
+open Ast
+open Ast_util
+open Type_check
+
+(** [find_properties defs] returns a mapping from ids to of 4-tuples of the form
+ (prop_type, command, loc, val_spec), which contains the information
+ from any pragmas of the form
+
+ $prop_type command
+ ...
+ val <val_spec>
+
+ where prop_type is either "counterexample" or "property" and the
+ location loc is the location that was attached to the pragma
+*)
+val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t
+
+(** For a property
+
+ $prop_type val f : forall X, C. T -> bool
+
+ find the function body for id:
+
+ function f(args) = exp
+
+ and rewrite the function body to
+
+ function f(args) = if constraint(not(C)) then true else exp
+
+ The reason we do this is that the type information in T constrained
+ by C might be lost when translating to Jib, as Jib types are
+ simpler and less precise. If we then do random test
+ generation/proving we want to ensure that inputs outside the
+ constraints of the function are ignored.
+*)
+val rewrite : tannot defs -> tannot defs
diff --git a/src/reporting.ml b/src/reporting.ml
index 20e44c57..c85f20ff 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -117,14 +117,14 @@ let rec simp_loc = function
| Parse_ast.Generated l -> simp_loc l
| Parse_ast.Range (p1, p2) -> Some (p1, p2)
| Parse_ast.Documented (_, l) -> simp_loc l
-
+
let short_loc_to_string l =
match simp_loc l with
| None -> "unknown location"
| Some (p1, p2) ->
Printf.sprintf "%s %d:%d - %d:%d"
p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
-
+
let print_err l m1 m2 =
print_err_internal (Loc l) m1 m2
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b9276f93..f7544a7c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4754,7 +4754,8 @@ let all_rewrites = [
("overload_cast", Basic_rewriter rewrite_overload_cast);
("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
("constant_fold", Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls));
- ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)))
+ ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)));
+ ("properties", Basic_rewriter (fun _ -> Property.rewrite));
]
let rewrites_lem = [
@@ -4922,7 +4923,7 @@ let rewrites_target tgt =
| "ocaml" -> rewrites_ocaml
| "c" -> rewrites_c
| "ir" -> rewrites_c
- | "smt" -> rewrites_c
+ | "smt" -> rewrites_c @ [("properties", [])]
| "sail" -> []
| "latex" -> []
| "interpreter" -> rewrites_interpreter
diff --git a/src/sail.ml b/src/sail.ml
index 95da54b0..179c1a67 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -412,17 +412,18 @@ let target name out_name ast type_envs =
if close then close_out output_chan else ()
| Some "smt" ->
+ let open Ast_util in
+ let props = Property.find_properties ast in
+ Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;
let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
(* let ast_smt, type_envs = Specialize.(specialize' 1 int_specialization_with_externs ast_smt type_envs) in *)
- let close, output_chan =
+ let name_file =
match !opt_file_out with
- | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".smt2"))
- | None -> false, stdout
+ | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
+ | None -> fun str -> str ^ ".smt2"
in
Util.opt_warnings := true;
- Jib_smt.generate_smt output_chan type_envs ast_smt;
- flush output_chan;
- if close then close_out output_chan else ()
+ Jib_smt.generate_smt props name_file type_envs ast_smt;
| Some "lem" ->
output "" (Lem_out (!opt_libs_lem)) [(out_name, type_envs, ast)]
diff --git a/src/specialize.ml b/src/specialize.ml
index 1da7208a..3063e4d5 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -485,7 +485,6 @@ let specialize_id_overloads instantiations id (Defs defs) =
let initial_calls = ref (IdSet.of_list
[ mk_id "main";
- mk_id "check_sat";
mk_id "__SetConfig";
mk_id "__ListConfig";
mk_id "execute";
diff --git a/src/util.ml b/src/util.ml
index 5ef9686d..6a2fb9bb 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -386,6 +386,14 @@ let rec take_drop f = function
let (ys, zs) = take_drop f xs in
(x :: ys, zs)
+let find_next f xs =
+ let rec find_next' f acc = function
+ | x :: xs when f x -> List.rev acc, Some (x, xs)
+ | x :: xs -> find_next' f (x :: acc) xs
+ | [] -> List.rev acc, None
+ in
+ find_next' f [] xs
+
let is_none opt = not (is_some opt)
let rec take n xs = match n, xs with
diff --git a/src/util.mli b/src/util.mli
index 06fd5eff..ddc5347f 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -194,6 +194,8 @@ val drop : int -> 'a list -> 'a list
val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
+val find_next : ('a -> bool) -> 'a list -> ('a list * ('a * 'a list) option)
+
val list_init : int -> (int -> 'a) -> 'a list
(** {2 Files} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 06:22:43 +0000