X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Fnum.ml;h=962feaf3011efa95e31f0e64e0f995a394800350;hb=dfad242808c3525a0d9e3420565551964fcf0832;hp=71f493545df93edce3e4a9b844b838b3b54e2c66;hpb=a104858f2dd754e5d086c3884823f3f39d716691;p=fireball-separation.git

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 71f4935..962feaf 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -172,6 +172,7 @@ let cast_to_i_num_var =
     assert false (* algorithm failed *)
 
 let rec set_arity arity = function
+(* FIXME because onlt variables should be in branches of matches, one day *)
 | `Var(n,_) -> `Var(n,arity)
 | `N _ | `Bottom | `Pacman as t -> t
 | `Lam(false, t) -> `Lam(false, set_arity arity t)
@@ -266,28 +267,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 =
@@ -343,9 +322,9 @@ let rec eta_subterm sub t =
      eta_subterm sub (u :> nf)
      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
      || List.exists (eta_subterm sub) (args :> nf list)
-  | `I(v, args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
-   | `Var v' -> v = v'
-   | `I(v', args') -> v = v'
+  | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+   | `Var(v',_) -> v = v'
+   | `I((v',_), args') -> v = v'
     && Listx.length args' < Listx.length args
     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args :> nf list)) (Listx.to_list args' :> nf list))
    | _ -> false