From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 25 Jul 2017 12:25:56 +0000 (+0200)
Subject: Debugging information improved
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=632f83a9f7fbf8a09e323314dde76189692d6f07;p=fireball-separation.git

Debugging information improved
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 44ca43b..6a534cd 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -346,7 +346,7 @@ and dangerous_inert_conv p arities showstoppers k args match_args more_args =
  if List.mem k showstoppers then raise Dangerous else
   try
    let arity = arity_of arities k in
-prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args);
+(* prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args); *)
    if more_args > 0 (* match argument*) && List.length args = arity then raise (TriggerMatchReduction k)
     else if List.length all_args + more_args > arity then raise Dangerous else ()
   with
@@ -378,9 +378,6 @@ let rec edible p arities showstoppers =
    let showstoppers = sort_uniq (aux (dangerous arities) showstoppers p.ps p.ps) in
    let dangerous_conv = sort_uniq (aux (dangerous_conv p arities) showstoppers p.conv p.conv) in
 
-prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-prerr_endline (String.concat " " (List.map (string_of_var p.var_names) dangerous_conv));
-
     let showstoppers' = showstoppers @ dangerous_conv in
     let showstoppers' = sort_uniq (match p.div with
      | None -> showstoppers'
@@ -435,8 +432,8 @@ let critical_showstoppers p =
   let showstoppers_eat = List.filter
     (fun x -> not (List.mem x showstoppers_step))
     showstoppers_eat in
-  List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-  List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+prerr_endline ("DANGEROUS STEP: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_step));
+prerr_endline ("DANGEROUS EAT: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_eat));
   p, showstoppers_step, showstoppers_eat
   ;;
 
@@ -446,7 +443,7 @@ let eat p =
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
   let inedible = edible p arities showstoppers in
-  prerr_endline ("showstoppers (in eat)" ^ String.concat " " (List.map (string_of_var p.var_names) (inedible)));
+  prerr_endline ("showstoppers (in eat)" ^ String.concat " " (List.map (string_of_var p.var_names) inedible));
   let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
   let new_sigma = List.map (fun (pos,hd,nargs) ->
    let v = if pos = -1 then `Bottom else `N pos in