Fixed computation of arity for top-level inerts

(cherry picked from commit 5682bf463b89edb7756020fe7b838eb846d6c771)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 8a5797ce1297491837bec242c6565b7a7481c767..9c92c712a7b38263c21bc919405ea2bc45f63a18 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
   @ [""])
 ;;
 

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 8ba2fbd7ae9a3f6770146f83ded59e5e151d9dc7..79650955de2f5c5f7fa73606dee2e68a9613f73d 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -172,7 +172,7 @@ let problem_of_string s =
  (* Fix arity *)\r
  let open Num in\r
  let rec aux lev : nf -> nf = function\r
- | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> aux lev t) args)\r
+ | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (aux lev) args)\r
  | `Var(n,_) -> fix lev n\r
  | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
  | `Match _ | `N _ -> assert false in\r