X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.ml;h=ea885d20434283ce72f1405487c8826d9af02a19;hb=9223a25e0e3079058d498ad21da17296bd6edc82;hp=2b0e04dd0104ad79b71ca9a55c20030c31050e5f;hpb=6fc1858e757263b4e651f92fa8aaa3ecee1ab626;p=fireball-separation.git

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 2b0e04d..ea885d2 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 =