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.
---
 test-suite/unit-tests/lib/pp_big_vect.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/unit-tests/lib/pp_big_vect.ml

(limited to 'test-suite/unit-tests/lib')

diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml
new file mode 100644
index 0000000000..e1cdd290e2
--- /dev/null
+++ b/test-suite/unit-tests/lib/pp_big_vect.ml
@@ -0,0 +1,14 @@
+open OUnit
+open Pp
+
+let pr_big_vect =
+  let n = "pr_big_vect" in
+  n >:: (fun () ->
+      let v = Array.make (1 lsl 20) () in
+      let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in
+      let str = string_of_ppcmds pp in
+      ignore(str))
+
+let tests = [pr_big_vect]
+
+let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests
-- 
cgit v1.2.3