]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/num.ml
Moved parse' from Num to Parser
[fireball-separation.git] / ocaml / num.ml
index 82c4b3803e4a0868e6e96eb58d935b9cae146628..d9cdf379857957bae4a871fd6b119f300f3056eb 100644 (file)
@@ -266,28 +266,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
 
 (************ Parsing ************************************)
 
-let parse' strs =
-  let fix_arity = function
-   | `I((n,_),args) -> `I((n,1+Listx.length args),args)
-   | _ -> assert false in
-  let (tms, free) = Parser.parse_many strs in
-  (* Replace pacmans and bottoms *)
-  let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in
-  let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in
-  let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in
-  let fix lev v =
-   if v = lev + n_bot then `Bottom
-    else if v = lev + n_pac then `Pacman
-     else if v = lev + n_bomb then `Lam(true, `Bottom)
-      else `Var(v,1) in (* 1 by default when variable not applied *)
-  (* Fix arity *)
-  let rec aux lev = function
-   | Parser.Lam t -> `Lam (true, aux (lev+1) t)
-   | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2))
-   | Parser.Var v -> fix lev v in
-  List.map (aux 0) tms, free
-;;
-
 (************** Algorithm(s) ************************)
 
 let eta_compare x y =