X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5ce1386aeb0b16a9aca5a0f4abbde42270d3afe9;hb=988cf01c5bd740d6e75767327f201a3c43d635ed;hp=34cb4ee2fa5812311d6e8270d40300206828efc0;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml
index 34cb4ee2f..5ce1386ae 100644
--- a/matitaB/components/disambiguation/disambiguate.ml
+++ b/matitaB/components/disambiguation/disambiguate.ml
@@ -525,8 +525,8 @@ let bfvisit ~pp_term top_split test t =
   | [] -> None
   | (ctx0,t0 as hd)::tl ->
 (*      prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
-      prerr_endline ("visiting t0 = " ^ pp_term t0); 
-      if test t0 then (prerr_endline "t0 is ambiguous"; Some hd)
+      debug_print (lazy ("visiting t0 = " ^ pp_term t0)); 
+      if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd)
       else 
       (*
          (prerr_endline ("splitting not ambiguous t0:");
@@ -590,7 +590,7 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe
     in match (refine_profiler.HExtlib.profile foo ()) with
     | Ko x ->
         let _,err = Lazy.force x in
-        prerr_endline ("test_interpr error: " ^ err); 
+        debug_print (lazy ("test_interpr error: " ^ err)); 
         false
     | _ -> true
   with
@@ -625,8 +625,8 @@ let rec disambiguate_list
     let res =
       Environment.find item universe 
     in
-    prerr_endline (Printf.sprintf "choices for %s :\n%s"
-      (d2s item) (String.concat ", " (List.map a2s res)));
+    debug_print (lazy (Printf.sprintf "choices for %s :\n%s"
+      (d2s item) (String.concat ", " (List.map a2s res))));
     res
   in
 
@@ -641,7 +641,7 @@ let rec disambiguate_list
   match ts with
   | [] -> None
   | t0 :: tl ->
-      prerr_endline ("disambiguate_list: t0 = " ^ pp_thing t0); 
+      debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); 
       let is_ambiguous = function
       | Ast.Ident (_,`Ambiguous)
       | Ast.Num (_,None)
@@ -658,21 +658,21 @@ let rec disambiguate_list
       (* get first ambiguous subterm (or return disambiguated term) *)
       match visit ~pp_term is_ambiguous t0 with
       | None -> 
-          prerr_endline ("visit -- not ambiguous node:\n" ^ pp_thing t0);
+          debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0));
           Some (t0,tl)
       | Some (ctx, t) -> 
-        prerr_endline ("visit -- found ambiguous node: " ^ astpp t ^
-        "\nin " ^ pp_thing (ctx t));
+        debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^
+        "\nin " ^ pp_thing (ctx t)));
         (* get possible instantiations of t *)
         let instances = get_instances ctx t in
-        prerr_endline ("-- possible instances:");
+        debug_print (lazy "-- possible instances:");
         List.iter 
-         (fun u0 -> prerr_endline ("-- instance: " ^ (pp_thing u0))) instances;
+         (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances;
         (* perforate ambiguous subterms and test refinement *)
-        prerr_endline ("-- survivors:");
+        debug_print (lazy "-- survivors:");
         let survivors = List.filter test_interpr instances in
         List.iter 
-         (fun u0 -> prerr_endline ("-- survivor: " ^ (pp_thing u0))) survivors;
+         (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors;
         disambiguate_list (survivors@tl) 
 ;;
 
@@ -703,29 +703,30 @@ let disambiguate_thing
 
   let refine t = 
     let localization_tbl = mk_localization_tbl 503 in
-    prerr_endline "before interpretate_thing";
+    debug_print (lazy "before interpretate_thing");
     let t' = 
       interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl
     in 
-    prerr_endline "after interpretate_thing";
+    debug_print (lazy "after interpretate_thing");
      match refine_thing metasenv subst context uri ~use_coercions t' expty
           base_univ ~localization_tbl with
     | Ok (t',m',s',u') -> t,m',s',t',u'
     | Uncertain x ->
         let _,err = Lazy.force x in
-        prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+        debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
         assert false
     | _ -> assert false
   in
   if not (test_interpr thing) then 
-    (prerr_endline ("preliminary test fail: " ^ pp_thing thing);
+    (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
      raise (NoWellTypedInterpretation (0,[])))
   else
     let res = aux [thing] in
     let res =
       HExtlib.filter_map (fun t -> 
         try Some (refine t) 
-        with _ -> prerr_endline ("can't interpretate/refine " ^ (pp_thing t));None) res
+        with _ -> 
+          debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res
     in
     match res with
     | [] -> raise (NoWellTypedInterpretation (0,[]))