still stepping on negative variables

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 8a5cc37f12e4abdf075cf96b9dd52f58eda46905..c627151eeb5e7f98764b8d98c6ef3e9a852427af 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -451,7 +451,8 @@ let instantiate p x n =
  let arity_of_x = max_arity_tms x (all_terms p) in
  (if arity_of_x < 0 then failwithProblem p "step on a var of negative arity");
  (* AC: FIXME compute arities correctly below! *)
- let arities = Array.to_list (Array.make (n+1) 0) in
+ let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) in
+ (* let arities = Array.to_list (Array.make (n+1) 0) in *)
  let p,vars = make_fresh_vars p arities in
  (* let p,zero = make_fresh_var p in *)
  (* let zero = Listx.Nil zero in *)
@@ -497,7 +498,9 @@ let auto_instantiate (n,p) =
 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
 let x =
  try
-  match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0) (all_terms p)) with
+  match hd_of (List.find (fun t ->
+   compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0
+   ) (all_terms p)) with
       None -> assert false
     | Some x ->
        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
@@ -733,7 +736,7 @@ in
 
 (********************** problems *******************)
 
-let zero = `Var(0,-1);;
+let zero = `Var(0,0);;
 
 let append_zero =
  function