X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.ml;h=800322677a102f3aa324df8ddb35ca4daa6afcda;hb=9baecd2c43f39dd9c86b5a8f003bda19f821a66a;hp=10da3a40d909fcc2013f8e3e69c26a4306bdcac7;hpb=44d012f1bf971bca4cb9380f42f8fca79d414ece;p=fireball-separation.git

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 10da3a4..8003226 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -10,9 +10,9 @@ let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;
 
 (* FIXME *)
 let mk_var' (bound, free) x =
-  if List.mem x bound
+  if x <> "@" && List.mem x bound
   then free, mk_var (Util.index_of x bound)
-  else if List.mem x free
+  else if x <> "@" && List.mem x free
        then free, mk_var (List.length bound + Util.index_of x free)
        else (free @ [x]), mk_var (List.length bound + List.length free)
 ;;
@@ -30,11 +30,11 @@ let explode s =
 ;;
 
 let implode l =
-  let res = String.create (List.length l) in
+  let res = Bytes.create (List.length l) in
   let rec aux i = function
     | [] -> res
-    | c :: l -> res.[i] <- c; aux (i + 1) l in
-  aux 0 l
+    | c :: l -> Bytes.set res i c; aux (i + 1) l in
+  Bytes.to_string (aux 0 l)
 ;;
 
 let rec strip_spaces = function
@@ -45,7 +45,12 @@ let rec strip_spaces = function
 let read_var s =
   let rec aux = function
   | [] -> None, []
-  | c::cs as x -> if isAlphaNum c
+  | c::cs as x ->
+    if c = '@' then
+     (if cs <> [] && (let hd = List.hd cs in hd = '@' || isAlphaNum hd)
+     then raise (ParsingError ("Unexpected `"^String.make 1 (List.hd cs)^"` after `@`."))
+     else Some['@'], cs)
+    else if isAlphaNum c
     then match aux cs with
          | (Some x), cs' -> Some (c :: x), cs'
          | None, cs' -> (Some [c]), cs'
@@ -60,7 +65,7 @@ let read_var' (bound, free as vars) s =
   | Some varname, cs ->
     let free, v = mk_var' vars varname in
     Some [v], cs, (bound, free)
-  | _, _ -> raise (ParsingError ("Can't read variable"))
+  | None, _ -> raise (ParsingError ("Can't read variable"))
 ;;
 
 let rec read_smt vars =