From cc3341c4762822e934e694fed7b7757166fd34f2 Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 24 Jul 2017 16:15:19 +0200 Subject: [PATCH] Logging options to display measure of single terms in string_of_problem --- ocaml/lambda4.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 4726122..340b955 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -11,7 +11,10 @@ let bomb = ref(`Var(-1,-666));; For Scott's encoding, two. *) let num_more_args = 2;; +(* verbosity *) let _very_verbose = false;; +(** Display measure of every term when printing problem *) +let _measure_of_terms = false;; let verbose s = if _very_verbose then prerr_endline s @@ -77,6 +80,7 @@ let problem_measure p = sum_arities p;; let string_of_measure = string_of_int;; let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = + let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in let deltas = String.concat ("\n# ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in let l = p.var_names in String.concat "\n" ([ @@ -88,10 +92,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 ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf)); + (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf)); ] - @ 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 + @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv + @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps @ [""]) ;; -- 2.39.2