X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.ml;h=1dd4b583c8886216ee6910392103965253b1be05;hb=3ba5ecfc8372d4c9f380bad5cdf7387f2bbcea6a;hp=ae371c78f5b7efdd269b38ff04e1c6048eb8b71b;hpb=065c617277eb43a75b5a38936700da4e91bd889c;p=fireball-separation.git

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index ae371c7..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)
 ;;
@@ -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 =
@@ -44,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'
@@ -59,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 =
@@ -122,7 +128,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)
 ;;