wip

Author: fblanqui

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
 

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