From 19ab1b732deb00ae5568fe1df81ca2c71ade8732 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 16:52:55 +0200
Subject: [PATCH 1/6] type_abbrevs: add type of type paramaters

---
 main.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/main.ml b/main.ml
index 4b475a7..b2052f1 100644
--- a/main.ml
+++ b/main.ml
@@ -1227,7 +1227,11 @@ and command = function
     let decl_type_abbrevs oc =
       let abbrev s (idx,(_d,n)) =
         string oc "symbol type"; int oc idx;
-        for i=0 to n-1 do string oc " a"; int oc i done;
+        if n > 0 then begin
+          string oc " (a0";
+          for i=1 to n-1 do string oc " a"; int oc i done;
+          string oc " : Set)"
+        end;
         string oc " ≔ "; string oc s; string oc ";\n"
       in
       MapStr.iter abbrev map

From e4160fb849ae3d7e181e83b1f6a54728f16b3bc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 16:56:01 +0200
Subject: [PATCH 2/6] wip

---
 main.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/main.ml b/main.ml
index b2052f1..78118b6 100644
--- a/main.ml
+++ b/main.ml
@@ -1224,8 +1224,7 @@ and command = function
     in
     Array.iter gen_sed_file files;
     (* generate [b^"_type_abbrevs.lp"] *)
-    let decl_type_abbrevs oc =
-      let abbrev s (idx,(_d,n)) =
+      let abbrev oc s (idx,(_d,n)) =
         string oc "symbol type"; int oc idx;
         if n > 0 then begin
           string oc " (a0";
@@ -1234,7 +1233,8 @@ and command = function
         end;
         string oc " ≔ "; string oc s; string oc ";\n"
       in
-      MapStr.iter abbrev map
+    let decl_type_abbrevs oc =
+      MapStr.iter (abbrev oc) map
     in
     Xlp.export (b^"_type_abbrevs") [b^"_types"] decl_type_abbrevs
 

From ff8fcabb7fc050a0c8efe44a96eb2dc5fefa88ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 16:56:52 +0200
Subject: [PATCH 3/6] wip

---
 main.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/main.ml b/main.ml
index 78118b6..874a086 100644
--- a/main.ml
+++ b/main.ml
@@ -1224,8 +1224,8 @@ and command = function
     in
     Array.iter gen_sed_file files;
     (* generate [b^"_type_abbrevs.lp"] *)
-      let abbrev oc s (idx,(_d,n)) =
-        string oc "symbol type"; int oc idx;
+      let abbrev f oc s (idx,(_d,n)) =
+        string oc "symbol type"; f oc idx;
         if n > 0 then begin
           string oc " (a0";
           for i=1 to n-1 do string oc " a"; int oc i done;
@@ -1234,7 +1234,7 @@ and command = function
         string oc " ≔ "; string oc s; string oc ";\n"
       in
     let decl_type_abbrevs oc =
-      MapStr.iter (abbrev oc) map
+      MapStr.iter (abbrev int oc) map
     in
     Xlp.export (b^"_type_abbrevs") [b^"_types"] decl_type_abbrevs
 

From 454d493c8529dcbb0498f2c2cd6b32df3f197800 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 16:59:17 +0200
Subject: [PATCH 4/6] wip

---
 main.ml | 11 +----------
 xlp.ml  | 10 ++++++++++
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/main.ml b/main.ml
index 874a086..f3a5f45 100644
--- a/main.ml
+++ b/main.ml
@@ -1224,17 +1224,8 @@ and command = function
     in
     Array.iter gen_sed_file files;
     (* generate [b^"_type_abbrevs.lp"] *)
-      let abbrev f oc s (idx,(_d,n)) =
-        string oc "symbol type"; f oc idx;
-        if n > 0 then begin
-          string oc " (a0";
-          for i=1 to n-1 do string oc " a"; int oc i done;
-          string oc " : Set)"
-        end;
-        string oc " ≔ "; string oc s; string oc ";\n"
-      in
     let decl_type_abbrevs oc =
-      MapStr.iter (abbrev int oc) map
+      MapStr.iter (Xlp.decl_type_abbrev int oc) map
     in
     Xlp.export (b^"_type_abbrevs") [b^"_types"] decl_type_abbrevs
 
diff --git a/xlp.ml b/xlp.ml
index 540b380..7675641 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -115,6 +115,16 @@ let abbrev_typ oc b =
 
 let typ = abbrev_typ;;
 
+let decl_type_abbrev f oc s (idx,(_d,n)) =
+  string oc "symbol type"; f oc idx;
+  if n > 0 then begin
+    string oc " (a0";
+    for i=1 to n-1 do string oc " a"; int oc i done;
+    string oc " : Set)"
+  end;
+  string oc " ≔ "; string oc s; string oc ";\n"
+;;
+
 (* [decl_type_abbrevs oc] outputs on [oc] the type abbreviations. *)
 let decl_type_abbrevs oc =
   let abbrev s (k,n) =

From 0543c4b515a790877b0d036d2d349ede3dcc70ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 17:05:17 +0200
Subject: [PATCH 5/6] wip

---
 main.ml | 11 ++++++++++-
 xlp.ml  | 17 +++++------------
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/main.ml b/main.ml
index f3a5f45..c00a19d 100644
--- a/main.ml
+++ b/main.ml
@@ -1225,7 +1225,16 @@ and command = function
     Array.iter gen_sed_file files;
     (* generate [b^"_type_abbrevs.lp"] *)
     let decl_type_abbrevs oc =
-      MapStr.iter (Xlp.decl_type_abbrev int oc) map
+      let abbrev s (k,(_,n)) =
+        string oc "symbol type"; int oc k;
+        if n > 0 then begin
+          string oc " (a0";
+          for i=1 to n-1 do string oc " a"; int oc i done;
+          string oc " : Set)"
+        end;
+        string oc " ≔ "; string oc s; string oc ";\n"
+      in
+      MapStr.iter abbrev map
     in
     Xlp.export (b^"_type_abbrevs") [b^"_types"] decl_type_abbrevs
 
diff --git a/xlp.ml b/xlp.ml
index 7675641..3c57290 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -115,22 +115,15 @@ let abbrev_typ oc b =
 
 let typ = abbrev_typ;;
 
-let decl_type_abbrev f oc s (idx,(_d,n)) =
-  string oc "symbol type"; f oc idx;
-  if n > 0 then begin
-    string oc " (a0";
-    for i=1 to n-1 do string oc " a"; int oc i done;
-    string oc " : Set)"
-  end;
-  string oc " ≔ "; string oc s; string oc ";\n"
-;;
-
 (* [decl_type_abbrevs oc] outputs on [oc] the type abbreviations. *)
 let decl_type_abbrevs oc =
   let abbrev s (k,n) =
     string oc "symbol type"; digest oc k;
-    for i=0 to n-1 do string oc " a"; int oc i done;
-    (* We can use [raw_typ] here since [b] is canonical. *)
+    if n > 0 then begin
+      string oc " (a0";
+      for i=1 to n-1 do string oc " a"; int oc i done;
+      string oc " : Set)"
+    end;
     string oc " ≔ "; string oc s; string oc ";\n"
   in
   MapStr.iter abbrev !map_typ_abbrev

From 28f0b5d2b7488ec4d4c8136d8772d28a3fee7cc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 17:09:33 +0200
Subject: [PATCH 6/6] wip

---
 main.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/main.ml b/main.ml
index c00a19d..b2052f1 100644
--- a/main.ml
+++ b/main.ml
@@ -1225,8 +1225,8 @@ and command = function
     Array.iter gen_sed_file files;
     (* generate [b^"_type_abbrevs.lp"] *)
     let decl_type_abbrevs oc =
-      let abbrev s (k,(_,n)) =
-        string oc "symbol type"; int oc k;
+      let abbrev s (idx,(_d,n)) =
+        string oc "symbol type"; int oc idx;
         if n > 0 then begin
           string oc " (a0";
           for i=1 to n-1 do string oc " a"; int oc i done;