From 5682bf463b89edb7756020fe7b838eb846d6c771 Mon Sep 17 00:00:00 2001 From: acondolu Date: Sat, 22 Jul 2017 21:00:26 +0200 Subject: [PATCH] Fixed computation of arity for top-level inerts --- ocaml/lambda4.ml | 16 +++++++++------- ocaml/parser.ml | 2 +- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index b15c360..2e96fc3 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -70,16 +70,18 @@ let all_terms p = @ p.ps ;; -let sum_arities p = +let measure_of_term, measure_of_terms = let rec aux = function | `N _ | `Bottom | `Pacman -> 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 :> nf list) - | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many (args :> nf list) + | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many (args :> nf list) 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 problem_measure p = sum_arities p;; let string_of_measure = string_of_int;; @@ -96,10 +98,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 -> 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 4b02b12..6bcb70d 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -189,7 +189,7 @@ let problem_of_string s = | #nf_nob as t -> t | `Bottom -> raise (ParsingError "Input term not in normal form") in let rec aux_nob lev : nf_nob -> nf = function - | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args) + | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args) | `Var(n,_) -> fix lev n | `Lam(_,t) -> `Lam (true, aux (lev+1) t) | `Match _ | `N _ -> assert false -- 2.39.2