X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=c627151eeb5e7f98764b8d98c6ef3e9a852427af;hb=edc8a9dacfdf59bc23570756f7d346f9cd28ae6b;hp=f71f36005f220d09bdea65baf15aed2f181181bd;hpb=dc3d76330323f0eba348377062934481c763d450;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index f71f360..c627151 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -448,10 +448,11 @@ 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 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 *)
@@ -481,7 +482,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 +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) (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);
@@ -730,7 +736,7 @@ in
 
 (********************** problems *******************)
 
-let zero = `Var(0,-1);;
+let zero = `Var(0,0);;
 
 let append_zero =
  function
@@ -757,7 +763,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 *)