Merge pull request #94 from sneeuwballen/wip-escaping-93

try to fix escaping of identifiers in TPTP output (#93)
sneeuwballen · Oct 31, 2022 · defa545 · defa545
2 parents 5792fc3 + c4368e2
commit defa545
Showing 1 changed file with 8 additions and 2 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<>"");
-  s.[0] = '_' ||
-  CCString.exists (function ' ' | '#' | '$' | '+' | '-' | '/' -> true | _ -> false) s
+  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)