]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/parser.ml
Important: added special variable "Z" for zero.
[fireball-separation.git] / ocaml / parser.ml
index e5a040fd34b15f3f3cbd4569adc5c07c45b2ce62..570809dd6d4a6c952ee0139851bd97bef7be2af1 100644 (file)
@@ -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 `Bottom\r
      else if v = lev + n_pac then `Pacman\r
       else if v = lev + n_bomb then `Lam(true, `Bottom)\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 exclude_bottom = function\r