From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 14:15:53 +0000 (+0200)
Subject: Allow comments (#) at the end of terms
X-Git-Tag: weak-reduction-separation~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44d012f1bf971bca4cb9380f42f8fca79d414ece;p=fireball-separation.git

Allow comments (#) at the end of terms
---

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