From 9d33336846d9aed507ecec907dd7226951cdf9b0 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 17 Oct 2022 09:57:06 -0400
Subject: [PATCH 1/3] wip: try to fix escaping of identifiers in TPTP output
 (#93)

---
 src/core/Util.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/core/Util.ml b/src/core/Util.ml
index 23a4a795e..c27568e27 100644
--- a/src/core/Util.ml
+++ b/src/core/Util.ml
@@ -281,7 +281,12 @@ let pp_list0 ?(sep=" ") pp_x out = function
 let tstp_needs_escaping s =
   assert (s<>"");
   s.[0] = '_' ||
-  CCString.exists (function ' ' | '#' | '$' | '+' | '-' | '/' -> true | _ -> false) s
+  CCString.exists
+    (function
+      | ' ' | '#' | '$' | '+' | '-' | '/' | '\n'
+      | '\t' | '\r' | '<' | '>' -> true
+      | _ -> false)
+    s
 
 let pp_str_tstp out s =
   CCFormat.string out (if tstp_needs_escaping s then "'" ^ String.escaped s ^ "'" else s)

From 1dd88f9be89c2cc32453cc7b906e51dcb1185dab Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 28 Oct 2022 09:21:24 +0200
Subject: [PATCH 2/3] wip: use regex to escape identifiers in TPTP output (#93)

---
 src/core/Util.ml | 9 ++-------
 src/core/dune    | 2 +-
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/core/Util.ml b/src/core/Util.ml
index c27568e27..52f58b0bc 100644
--- a/src/core/Util.ml
+++ b/src/core/Util.ml
@@ -280,13 +280,8 @@ let pp_list0 ?(sep=" ") pp_x out = function
 
 let tstp_needs_escaping s =
   assert (s<>"");
-  s.[0] = '_' ||
-  CCString.exists
-    (function
-      | ' ' | '#' | '$' | '+' | '-' | '/' | '\n'
-      | '\t' | '\r' | '<' | '>' -> true
-      | _ -> false)
-    s
+  let idregex = Str.regexp "^[a-zA-Z]+[a-zA-Z0-9_]*$" in
+  not (Str.string_match idregex s 0)
 
 let pp_str_tstp out s =
   CCFormat.string out (if tstp_needs_escaping s then "'" ^ String.escaped s ^ "'" else s)
diff --git a/src/core/dune b/src/core/dune
index 3b5886515..ebef74726 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -5,7 +5,7 @@
   (public_name logtk)
   (synopsis "core data structures and algorithms for Logtk")
   (libraries containers containers-data iter oseq
-             unix mtime mtime.clock.os logtk.arith)
+             unix mtime mtime.clock.os logtk.arith str)
   (flags :standard -w -32-50 -open Logtk_arith)
   (c_names util_stubs)
   (c_flags -Wextra -Wno-unused-parameter)

From c4368e28be66fe54cf934efc58c1753f4720525c Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 28 Oct 2022 16:06:15 +0200
Subject: [PATCH 3/3] wip: use ocaml matching for escaping of identifiers in
 TPTP output (#93)

---
 src/core/Util.ml | 10 ++++++++--
 src/core/dune    |  2 +-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/core/Util.ml b/src/core/Util.ml
index 52f58b0bc..0b1e20c6c 100644
--- a/src/core/Util.ml
+++ b/src/core/Util.ml
@@ -280,8 +280,14 @@ let pp_list0 ?(sep=" ") pp_x out = function
 
 let tstp_needs_escaping s =
   assert (s<>"");
-  let idregex = Str.regexp "^[a-zA-Z]+[a-zA-Z0-9_]*$" in
-  not (Str.string_match idregex s 0)
+  match s.[0] with
+  | 'a' .. 'z' | 'A' ..'Z' ->
+    CCString.exists
+      (function
+        | 'a' .. 'z' | 'A' ..'Z' | '0' ..'9' | '_' -> false
+        | _ -> true)
+      s
+  | _ -> true
 
 let pp_str_tstp out s =
   CCFormat.string out (if tstp_needs_escaping s then "'" ^ String.escaped s ^ "'" else s)
diff --git a/src/core/dune b/src/core/dune
index ebef74726..3b5886515 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -5,7 +5,7 @@
   (public_name logtk)
   (synopsis "core data structures and algorithms for Logtk")
   (libraries containers containers-data iter oseq
-             unix mtime mtime.clock.os logtk.arith str)
+             unix mtime mtime.clock.os logtk.arith)
   (flags :standard -w -32-50 -open Logtk_arith)
   (c_names util_stubs)
   (c_flags -Wextra -Wno-unused-parameter)