Problems pass, but still missing computation of arities of fresh applicative vars

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index f71f36005f220d09bdea65baf15aed2f181181bd..8a5cc37f12e4abdf075cf96b9dd52f58eda46905 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -448,8 +448,8 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
 let instantiate p x n =
  (if hd_of_i_var (cast_to_i_var !bomb) = x
    then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
- (* ACL FIXME compute arity of x correctly below! *)
- let arity_of_x = -666 in
+ 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 p,vars = make_fresh_vars p arities in
@@ -481,7 +481,10 @@ let auto_instantiate (n,p) =
     | [], y::_ ->
       prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
     | [], [] ->
-     let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
+     let heads =
+      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
      (match heads with
          [] -> assert false
        | x::_ ->
@@ -494,7 +497,7 @@ 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) (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);
@@ -757,7 +760,7 @@ let magic_conv ~div ~conv ~nums cmds =
   let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
   (* casts *)
   let div = option_map cast_to_i_var div in
-  let conv = List.map cast_to_i_n_var conv in
+  let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in
   let tms = List.map cast_to_i_n_var tms in
 
   let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *)