The measure finally works on all problems in problems.ml!

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 486af1490d1494daef2fcb56f8a32b3f777493d4..9e164e6e674bed1185175c5460a69ab93da5172e 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -27,7 +27,7 @@ let sum_arities p =
  | `Var(_,ar) -> if ar = min_int then 0 else (assert (ar >= 0); ar)
  | `Lam(_,t) -> aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
- | `Match(u,v,_,_,args) -> (*aux (u :> nf) +*) aux (`Var v) + aux_many args
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
  aux_many (all_terms p :> nf list)
  ;;
@@ -38,7 +38,7 @@ let count_fakevars p =
  | `Var(_,ar) -> if ar = min_int then 1 else 0
  | `Lam(_,t) -> aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
- | `Match(u,v,_,_,args) -> (*aux (u :> nf) +*) aux (`Var v) + aux_many args
+ | `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
  aux_many (all_terms p :> nf list)
 ;;
@@ -191,7 +191,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
           if List.exists (fun (j,_) -> i=j) !bs then
            freshno
           else
-           let freshno,v = freshno+1, `Var (freshno+1, snd orig - 1) in (* make_fresh_var freshno in *)
+           let freshno,v = freshno+1, `Var (freshno+1, -666) in (* make_fresh_var freshno in *)
            bs := !bs @ [i, v] ;
            freshno in
 (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*)
@@ -458,7 +458,7 @@ let instantiate p x n =
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
  (* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,n+2),Listx.map (lift 1) args),(x,666),1,bs,[])) in
+ let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,666),1,bs,[])) in
  let p = {p with deltas=bs::p.deltas} in
  subst_in_problem x inst p
 ;;
@@ -482,7 +482,7 @@ let auto_instantiate (n,p) =
       prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
     | [], [] ->
      let heads =
-      (* Choose only variables still alive (with arity >= 0) *)
+      (* Choose only variables still alive (with arity > 0) *)
       List.sort compare (filter_map (
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
@@ -499,7 +499,7 @@ let auto_instantiate (n,p) =
 let x =
  try
   match hd_of (List.find (fun t ->
-   compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0
+   compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
    ) (all_terms p)) with
       None -> assert false
     | Some x ->