From 9419ec5ca289873f14c3c80428cdaf0a6936e68a Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 11 Sep 2024 12:03:05 +0200
Subject: [PATCH] Add zarith in opam file + some misc fixes

---
 dolmen_loop.opam                           |  1 +
 src/languages/smtlib2/poly/print.ml        | 27 ++++++++++----------
 src/languages/smtlib2/v2.6/script/print.ml | 29 +++++++++++-----------
 3 files changed, 28 insertions(+), 29 deletions(-)

diff --git a/dolmen_loop.opam b/dolmen_loop.opam
index a1d528e06..79683e47b 100644
--- a/dolmen_loop.opam
+++ b/dolmen_loop.opam
@@ -14,6 +14,7 @@ depends: [
   "dolmen_type" {= version }
   "dune" { >= "3.0" }
   "gen"
+  "zarith" { >= "1.10" }
   "pp_loc" { >= "2.0.0" }
   "odoc" { with-doc }
   "mdx" { with-test & >= "2.0.0" }
diff --git a/src/languages/smtlib2/poly/print.ml b/src/languages/smtlib2/poly/print.ml
index 4492dc874..e057bd125 100644
--- a/src/languages/smtlib2/poly/print.ml
+++ b/src/languages/smtlib2/poly/print.ml
@@ -520,18 +520,7 @@ module Make
     (* Matching *)
     match V.Term.Cst.builtin head with
 
-    (* Base + Algebraic datatypes *)
-    | B.Base ->
-      begin match find_named env head with
-        | None ->
-          let poly () = if term_cst_poly env head then Some t_ty else None in
-          p ~poly Term (Env.Term_cst.name env head)
-        | Some expr ->
-          assert (args = []);
-          let f_id = Dolmen_std.Id.create Term (Env.Term_cst.name env head) in
-          Format.fprintf fmt "(! %a@ :named %a)"
-            (term env) expr (id ~allow_keyword:false env) f_id
-      end
+    (* Algebraic datatypes *)
     | B.Constructor _ | B.Destructor _ ->
       let poly () = if term_cst_poly env head then Some t_ty else None in
       p ~poly Term (Env.Term_cst.name env head)
@@ -748,8 +737,18 @@ module Make
     | B.Re_power n -> p Term (N.indexed "re.^" [int n])
     | B.Re_loop (n1, n2) -> p Term (N.indexed "re.loop" [int n1; int n2])
 
-    (* fallback *)
-    | _ -> _cannot_print "unknown term builtin"
+    (* generic case + fallback *)
+    | B.Base | _ ->
+      begin match find_named env head with
+        | None ->
+          let poly () = if term_cst_poly env head then Some t_ty else None in
+          p ~poly Term (Env.Term_cst.name env head)
+        | Some expr ->
+          assert (args = []);
+          let f_id = Dolmen_std.Id.create Term (Env.Term_cst.name env head) in
+          Format.fprintf fmt "(! %a@ :named %a)"
+            (term env) expr (id ~allow_keyword:false env) f_id
+      end
 
   and letin env fmt (l, body) =
     (* reset some env state *)
diff --git a/src/languages/smtlib2/v2.6/script/print.ml b/src/languages/smtlib2/v2.6/script/print.ml
index e4ec6e598..980b2435c 100644
--- a/src/languages/smtlib2/v2.6/script/print.ml
+++ b/src/languages/smtlib2/v2.6/script/print.ml
@@ -525,19 +525,7 @@ module Make
     (* Matching *)
     match V.Term.Cst.builtin head with
 
-    (* Base + Algebraic datatypes *)
-    | B.Base ->
-      begin match find_named env head with
-        | None ->
-          let poly () = if term_cst_poly env head then Some t_ty else None in
-          let h = Env.Term_cst.name env head in
-          p ~poly Term h
-        | Some expr ->
-          assert (args = []);
-          let f_id = Dolmen_std.Id.create Term (Env.Term_cst.name env head) in
-          Format.fprintf fmt "(! %a@ :named %a)"
-            (term env) expr (id ~allow_keyword:false env) f_id
-      end
+    (* Algebraic datatypes *)
     | B.Constructor _ | B.Destructor _ ->
       let poly () = if term_cst_poly env head then Some t_ty else None in
       p ~poly Term (Env.Term_cst.name env head)
@@ -754,8 +742,19 @@ module Make
     | B.Re_power n -> p Term (N.indexed "re.^" [int n])
     | B.Re_loop (n1, n2) -> p Term (N.indexed "re.loop" [int n1; int n2])
 
-    (* fallback *)
-    | _ -> _cannot_print "unknown term builtin"
+    (* generic case + fallback *)
+    | B.Base | _ ->
+      begin match find_named env head with
+        | None ->
+          let poly () = if term_cst_poly env head then Some t_ty else None in
+          let h = Env.Term_cst.name env head in
+          p ~poly Term h
+        | Some expr ->
+          assert (args = []);
+          let f_id = Dolmen_std.Id.create Term (Env.Term_cst.name env head) in
+          Format.fprintf fmt "(! %a@ :named %a)"
+            (term env) expr (id ~allow_keyword:false env) f_id
+      end
 
   and letin env fmt (l, body) =
     (* reset some env state *)