Simplified arity_of, precompute_edible_data, critical_showsteppers

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 8a5797ce1297491837bec242c6565b7a7481c767..e56a496a88cf83cc4eb8727a1f0b59274fd4a7eb 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -46,16 +46,18 @@ let all_terms p =
  @ p.ps
 ;;
 
-let sum_arities p =
+let measure_of_term, measure_of_terms =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
  | `Lam(_,t) -> aux t
- | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
- | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args
+ | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 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)
- ;;
+ (fun t -> aux (t :> nf)), (fun l -> aux_many (l :> nf list))
+;;
+
+let sum_arities p = measure_of_terms (all_terms p)
 
 let count_fakevars p =
  let rec aux = function
@@ -86,10 +88,10 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
    ) else "# ";
   "#";
   "$" ^ p.label;
-  (match div with None -> "# no D" | Some div -> "D " ^ print ~l (div :> nf));
+  (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
   ]
-  @ List.map (fun t -> "C " ^ (if t = convergent_dummy then "#C" else "C " ^ print ~l (t :> nf))) conv
-  @ List.mapi (fun i t -> string_of_int i ^ " " ^ print ~l (t :> nf)) ps
+  @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
+  @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
   @ [""])
 ;;
 
@@ -252,10 +254,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 =
@@ -354,11 +355,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 =
@@ -400,23 +404,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