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

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 10da3a4..1dd4b58 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)
 ;;
@@ -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 =