From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 25 Jul 2017 08:21:16 +0000 (+0200)
Subject: Implemented parsing of "nominal" variables (`@`)
X-Git-Tag: weak-reduction-separation~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb289306640a1605bd22b539a80710175b763810;p=fireball-separation.git

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 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 =