From 05625e450d69c4850f8c8b61f28073104b88b834 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 24 Apr 2024 13:35:11 +0200
Subject: [PATCH] Fix Array.empty precompilation

Fix #24
---
 src/tac2compiledPrim.ml  | 5 ++---
 src/tac2compiledPrim.mli | 2 +-
 tests/_CoqProject        | 1 +
 tests/compiler_bug_24.v  | 6 ++++++
 4 files changed, 10 insertions(+), 4 deletions(-)
 create mode 100644 tests/compiler_bug_24.v

diff --git a/src/tac2compiledPrim.ml b/src/tac2compiledPrim.ml
index f41b1f7..b7e2fea 100644
--- a/src/tac2compiledPrim.ml
+++ b/src/tac2compiledPrim.ml
@@ -43,9 +43,8 @@ let define name arity f =
   registered := (name,arity) :: !registered;
   f
 
-(* Adds a thunk *)
 let define0 name v =
-  define name 1 (fun (_:valexpr) -> v)
+  define name 0 v
 
 let define1 name r0 f =
   define name 1 (fun x0 -> f (repr_to r0 x0))
@@ -56,7 +55,7 @@ let define2 name r0 r1 f =
 let define3 name r0 r1 r2 f =
   define name 3 (fun x0 x1 x2 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2))
 
-let array_empty = define0 "array_empty" (return (ValBlk (0, [||])))
+let array_empty = define0 "array_empty" (ValBlk (0, [||]))
 
 let array_make = define2 "array_make" int valexpr begin fun n x ->
   if n < 0 || n > Sys.max_array_length then throw err_outofbounds
diff --git a/src/tac2compiledPrim.mli b/src/tac2compiledPrim.mli
index faf915d..cf718be 100644
--- a/src/tac2compiledPrim.mli
+++ b/src/tac2compiledPrim.mli
@@ -11,7 +11,7 @@
 open Ltac2_plugin.Tac2val
 open Proofview
 
-val array_empty : valexpr -> valexpr tactic
+val array_empty : valexpr
 val array_make : valexpr -> valexpr -> valexpr tactic
 val array_length : valexpr -> valexpr tactic
 val array_set : valexpr -> valexpr -> valexpr -> valexpr tactic
diff --git a/tests/_CoqProject b/tests/_CoqProject
index 0c085e1..73e351a 100644
--- a/tests/_CoqProject
+++ b/tests/_CoqProject
@@ -11,6 +11,7 @@ compiler_bug_6.v
 compiler_bug_14.v
 compiler_bug_16.v
 compiler_bug_17.v
+compiler_bug_24.v
 
 -I src
 
diff --git a/tests/compiler_bug_24.v b/tests/compiler_bug_24.v
new file mode 100644
index 0000000..723809e
--- /dev/null
+++ b/tests/compiler_bug_24.v
@@ -0,0 +1,6 @@
+Require Import Ltac2Compiler.Ltac2Compiler.
+From Ltac2 Require Import Array.
+Ltac2 test () := Array.empty.
+Ltac2 Eval Array.length (test ()).
+Ltac2 Compile Array.empty.
+Ltac2 Eval Array.length (test ()).