Simplified arity_of, precompute_edible_data, critical_showsteppers

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 2e96fc3dc0ef658c05b87cd55bdca9e196baf73d..dfe0da1b8c927a96c3591d1f1711c4b74db57af6 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -284,10 +284,9 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
 
 exception Dangerous
 
-let arity_of arities k =
- let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in
- let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in
- arity + if pos = -1 then - 1 else 0
+let arity_of arities hd =
+ let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in
+ nargs + if pos = -1 then - 1 else 0
 ;;
 
 let rec dangerous arities showstoppers =
@@ -388,11 +387,14 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
 ;;
 
 let precompute_edible_data {ps; div} xs =
- (match div with None -> [] | Some div -> [hd_of_i_var div, -1, (div :> i_n_var)]) @
-  List.map (fun hd ->
+ let aux t = match t with `Var _ -> 0 | `I(_, args) -> Listx.length args | `N _ -> assert false in
+ (fun l -> match div with
+  | None -> l
+  | Some div -> (-1, hd_of_i_var div, aux div) :: l)
+  (List.map (fun hd ->
    let i, tm = Util.findi (fun y -> hd_of y = Some hd) ps in
-    hd, i, tm
-   ) xs
+    i, hd, aux tm
+   ) xs)
 ;;
 
 let critical_showstoppers p =
@@ -434,23 +436,21 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv =
-   edible p arities showstoppers in
-  let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
+  let showstoppers, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
   let p =
-  List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else
-   let n = match xx with `I(_,args) -> Listx.length args | _ -> 0 in
+  List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
    let v = `N(pos) in
-   let inst = make_lams v n in
-prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst);
-   { p with sigma = p.sigma @ [x,inst] }
+   let inst = make_lams v nargs in
+prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
+   { p with sigma = p.sigma @ [hd,inst] }
    ) p l in
   (* to avoid applied numbers in safe positions that
      trigger assert failures subst_in_problem x inst p*)
  let ps =
   List.map (fun t ->
    try
-    let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in
+    let j,_,_ = List.find (fun (_,hd,_) -> hd_of t = Some hd) l in
     `N j
    with Not_found -> t
   ) ps in