From 4baa950b79589c6617770b5612bd082fde9c9255 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 19 Jan 2019 22:16:06 +0000
Subject: Make prvect tail recursive (fix #9355)

Using a unit test as it's way faster than messing with universes.

You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.

About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.
---
 lib/pp.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index d68f5ac5e3..cdde60f051 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -284,15 +284,12 @@ let pr_vertical_list pr = function
    [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *)
 
 let prvecti_with_sep sep elem v =
-  let rec pr i =
-    if Int.equal i 0 then
-      elem 0 v.(0)
-    else
-      let r = pr (i-1) and s = sep () and e = elem i v.(i) in
-      r ++ s ++ e
+  let v = CArray.mapi (fun i x ->
+      let pp = if i = 0 then mt() else sep() in
+      pp ++ elem i x)
+      v
   in
-  let n = Array.length v in
-  if Int.equal n 0 then mt () else pr (n - 1)
+  seq (Array.to_list v)
 
 (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
 
-- 
cgit v1.2.3