From 9223a25e0e3079058d498ad21da17296bd6edc82 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 25 Jul 2017 10:21:16 +0200 Subject: [PATCH] Implemented parsing of "nominal" variables (`@`) Each occurrence of `@` is parsed as a fresh free variable --- ocaml/parser.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) 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 = -- 2.39.2