From 956dcf75b88dc86c6f3a51ed61bb098a818fd0f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Mon, 27 Jan 2025 15:14:22 +0100
Subject: [PATCH] tests/OK/natural.lp: add builtins for printing Peano numbers
 in decimal notation (#1186)

---
 src/core/print.ml                   |  1 +
 tests/OK/natural.lp                 | 11 ++++++++---
 tests/OK/perf_rw_fib-nonRightLin.lp |  2 +-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/core/print.ml b/src/core/print.ml
index 17bd36c66..27dd428b9 100644
--- a/src/core/print.ml
+++ b/src/core/print.ml
@@ -107,6 +107,7 @@ let var : 'a Bindlib.var pp = fun ppf x -> uid ppf (Bindlib.name_of x)
 
 (** Exception raised when trying to convert a term into a nat. *)
 exception Not_a_nat
+
 let builtin name =
   try StrMap.find name (!sig_state).builtins with Not_found -> raise Not_a_nat
 
diff --git a/tests/OK/natural.lp b/tests/OK/natural.lp
index 06a021ffb..b7819ddef 100644
--- a/tests/OK/natural.lp
+++ b/tests/OK/natural.lp
@@ -27,7 +27,7 @@ with (s $m) × $n     ↪ $n + $m × $n
 with _      × z      ↪ z
 with $m     × (s $n) ↪ $m + $m × $n;
 
-// Enabling decimal notation
+// Enabling parsing of decimal notation
 
 symbol n1 ≔ s z;
 symbol n2 ≔ s n1;
@@ -57,14 +57,19 @@ builtin "*" ≔ ×;
 
 symbol forty_two ≔ 42;
 
-//print forty_two;
-
 assert ⊢ forty_two
   ≡ let two ≔ s(s z) in
     let four ≔ two + two in
     let ten ≔ four + four + two in
     four × ten + two;
 
+// Enabling printing of decimal notation
+
+builtin "nat_zero" ≔ z;
+builtin "nat_succ" ≔ s;
+
+compute 4 + 5;
+
 // Doubling function.
 
 symbol double n ≔ n × 2;
diff --git a/tests/OK/perf_rw_fib-nonRightLin.lp b/tests/OK/perf_rw_fib-nonRightLin.lp
index 5b91fc616..a151f30b2 100644
--- a/tests/OK/perf_rw_fib-nonRightLin.lp
+++ b/tests/OK/perf_rw_fib-nonRightLin.lp
@@ -13,4 +13,4 @@ with fib3 (s (s (s $x))) ↪ (fib3 ($x + 2)) + (fib3 ($x + 1)) + (fib3 $x);
 
 assert ⊢ fib 15 ≡ 610;
 compute fib 24; // ≡ 46368;
-compute fib3 21;
+//compute fib3 21;