wip: use ocaml matching for escaping of identifiers in TPTP output (#93)

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

Hide file tree

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