better debuggin output

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 1d3408d6b4b1d64c135cb72449a8d37394eccd05..79ed2f03714e36247bd3aa06b0be106365c77f95 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -73,7 +73,6 @@ let _ =
       prerr_endline (HelmLogger.string_of_html_msg html_msg));
   CicParser.impredicative_set := false;
   NCicTypeChecker.set_logger logger;
-  NCicPp.set_ppterm NCicPp.trivial_pp_term;
   Helm_registry.load_from "conf.xml";
   let alluris = 
     try

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 11f90736a23e01ff088d54779c574c7d8dc679f6..51ea8809b5305b09cc616c48eac44d13f0084239 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -68,6 +68,12 @@ let eta_reduce =
 module C = NCic;;
 module Ref = NReference;;
 
+let indent = ref "";;
+let inside c = indent := !indent ^ String.make 1 c;;
+let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+
+let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);;
+
 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
@@ -111,6 +117,9 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg =
     metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
 and beta_expand_many test_equality_only swap metasenv subst context t args =
+(*D*)  inside 'B'; try let rc =
+  pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
+     args) ^ " in " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
   let _, subst, metasenv, hd =
     List.fold_right
       (fun arg (num,subst,metasenv,t) ->
@@ -121,8 +130,10 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
       args (1,subst,metasenv,t) 
   in
     metasenv, subst, hd
+(*D*)  in outside (); rc with exn -> outside (); raise exn
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
+(*D*)  inside 'I'; try let rc = 
   let unify test_eq_only m s c t1 t2 = 
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
@@ -136,6 +147,8 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
   let lty = NCicSubstitution.subst_meta lc ty in
+  pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+    ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t); 
   let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
   let (metasenv, subst), t = 
     NCicMetaSubst.delift metasenv subst context n lc t
@@ -154,12 +167,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
     metasenv, subst
+(*D*)  in outside(); rc with exn -> outside (); raise exn
 
 and unify test_eq_only metasenv subst context t1 t2 =
+(*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst t1 t2 =
-        prerr_endline ("A " ^ 
-          NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm
-          ~metasenv ~subst ~context t2 );
+   (*D*) inside 'F'; try let rc = 
+     pp ("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2);
      if t1 === t2 then
        metasenv, subst
      else
@@ -343,6 +358,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
+    (*D*)  in outside(); rc with exn -> outside (); raise exn
     in
     let height_of is_whd = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
@@ -362,13 +378,14 @@ and unify test_eq_only metasenv subst context t1 t2 =
       NCicReduction.reduce_machine ~delta ~subst context m2,
       if is_whd && flex1 && flex2 then 0 else delta
     in
-    let rec unif_machines metasenv subst = function
+    let rec unif_machines metasenv subst = 
+      function
       | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
-        prerr_endline ("M(" ^ string_of_int delta^ "  " ^ 
-          NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ 
-          " === " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind
-          m2));
-        try
+    (*D*) inside 'M'; try let rc =
+         pp ((if delta > 100 then "∞" else string_of_int delta) ^ " " ^
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
+           " === " ^ 
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
           let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
@@ -395,15 +412,14 @@ and unify test_eq_only metasenv subst context t1 t2 =
                    (NCicReduction.unwind (k1,e1,t1,List.rev l1)) 
                    (NCicReduction.unwind (k2,e2,t2,List.rev l2))
           in
-           check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+        try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
         with UnificationFailure _ | Uncertain _ when delta > 0 ->
 (*
           let delta = delta - 1 in 
           let red = NCicReduction.reduce_machine ~delta ~subst context in
 *)
-        prerr_endline ("RIPARTO RIDUCENDO"^string_of_int delta);
           unif_machines metasenv subst (small_delta_step true m1 m2)
-            | exn -> prerr_endline ")"; raise exn
+     (*D*)  in outside(); rc with exn -> outside (); raise exn
      in
      try fo_unif test_eq_only metasenv subst t1 t2
      with UnificationFailure msg | Uncertain msg as exn -> 
@@ -413,9 +429,12 @@ and unify test_eq_only metasenv subst context t1 t2 =
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
+(*D*)  in outside(); rc with exn -> outside (); raise exn
 ;;
 
-let unify = unify false;;
+let unify = 
+  indent := "";      
+  unify false;;
 
 
 

diff --git a/helm/software/components/ng_refiner/rt.ml b/helm/software/components/ng_refiner/rt.ml
index 3843d5a7800e74e55af4cd9267753bf5eb0a1790..997bc2e3cc38bb1ec612e43b16119874d103fdc8 100644 (file)
--- a/helm/software/components/ng_refiner/rt.ml
+++ b/helm/software/components/ng_refiner/rt.ml
@@ -14,7 +14,6 @@
 let _ =
   Helm_registry.load_from "conf.xml";
   CicParser.impredicative_set := false;
-  NCicPp.set_ppterm NCicPp.trivial_pp_term;
   let u = UriManager.uri_of_string Sys.argv.(1) in
   let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
   prerr_endline "VECCHIO";