aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml15
-rw-r--r--lib/util.mli1
2 files changed, 14 insertions, 2 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 77d26ecf4d..59f119a50c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -390,6 +390,16 @@ let rec prlist_with_sep sep elem l = match l with
let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
[< e; s; r >]
+let prvecti elem v =
+ let n = Array.length v in
+ let rec pr i =
+ if i = 0 then
+ elem 0 v.(0)
+ else
+ let r = pr (i-1) and e = elem i v.(i) in [< r; e >]
+ in
+ pr (n-1)
+
let prvect_with_sep sep elem v =
let rec pr n =
if n = 0 then
@@ -397,5 +407,6 @@ let prvect_with_sep sep elem v =
else
let r = pr (n-1) and s = sep() and e = elem v.(n) in
[< r; s; e >]
- in
- if Array.length v = 0 then [< >] else pr (Array.length v - 1)
+ in
+ let n = Array.length v in
+ if n = 0 then [< >] else pr (n - 1)
diff --git a/lib/util.mli b/lib/util.mli
index 30d7bdee79..b8b72da090 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -123,6 +123,7 @@ val pr_str : string -> std_ppcmds
val pr_coma : unit -> std_ppcmds
val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t
+val prvecti : (int -> 'a -> 'b Stream.t) -> 'a array -> 'b Stream.t
val prlist_with_sep :
(unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
val prvect_with_sep :