Allow comments (#) at the end of terms

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 34b62ba99aa3808b3f14c5084731350f1026ef80..2b0e04dd0104ad79b71ca9a55c20030c31050e5f 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -23,9 +23,10 @@ let mk_app' = function
 ;;\r
 \r
 let explode s =\r
+ let len = String.length s in\r
   let rec aux i l =\r
-    if i < 0 then l else aux (i - 1) (s.[i] :: l)\r
-  in aux (String.length s - 1) []\r
+    if i >= len || s.[i] = '#' then l else aux (i+1) (s.[i] :: l)\r
+  in List.rev (aux 0 [])\r
 ;;\r
 \r
 let implode l =\r
@@ -122,7 +123,7 @@ let parse_many strs =
   let f (x, y) z = match read_smt y (explode z) with\r
   | Some[tm], [], vars -> (tm :: x, vars)\r
   | _, _, _ -> assert false\r
-  in let aux = List.fold_left f ([], ([], [])) (* index zero is reserved *)\r
+  in let aux = List.fold_left f ([], ([], []))\r
   in let (tms, (_, free)) = aux strs\r
   in (List.rev tms, free)\r
 ;;\r