wip: use regex to escape identifiers in TPTP output (#93)

sneeuwballen · Oct 28, 2022 · 1dd88f9 · 1dd88f9
1 parent 9d33336
commit 1dd88f9
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 8 deletions.
diff --git 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
@@ -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)