Implemented parsing of "nominal" variables (`@`)

Each occurrence of `@` is parsed as a fresh free variable

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