Important: added special variable "Z" for zero.

[fireball-separation.git] / ocaml / parser.ml

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 902da8d38bfdb8473d14f05dd5fbedee2e55da51..abd4309f5fd591d5208109bcd82e0f2cd422d86a 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -148,11 +148,13 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
    let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in\r
    let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in\r
    let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in\r
+   let n_z = try Util.index_of "Z" free with Not_found -> min_int in\r
    let fix lev v =\r
     if v = lev + n_bot then failwith "Example with `Bottom"\r
      else if v = lev + n_pac then failwith "Example with `Pacman"\r
       else if v = lev + n_bomb then failwith "Example with `Bomb"\r
-       else `Var(v,1) in (* 1 by default when variable not applied *)\r
+       else if v = lev + n_z then `Var(lev, 0) (* FIXME why zero? *)\r
+         else `Var(v,1) in (* 1 by default when variable not applied *)\r
    (* Fix arity *)\r
    let open Num in\r
    let rec aux lev : nf -> nf = function\r