1) improved (???) debugging, with

  1.1 more messages (good)
  1.2 messages for exceptions (very good)
  1.3 vim folding/unfolding (good or very bad?)
2) bug partially fixed (to be improved/totally fixed):
   when we unify a ?n:? vs a term t, we need to check
   that t is a sort! (or a flexible term??? what to do in that case?)
   otherwise we can get ?n := O and ?1:?2:?n=0 which is a not
   well typed metasenv. Hence boom later.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index cf44ff4708946917e62fd397479caea6af471365..a3c980648f9b87128128a815f9c01a0e85dd1ecb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -78,21 +78,27 @@ let eta_reduce subst t =
 module C = NCic;;
 module Ref = NReference;;
 
+let debug = false;;
 let indent = ref "";;
-let inside c = indent := !indent ^ String.make 1 c;;
-let outside () =
+let pp =
+ if debug then
+  fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+ else 
+  fun _ -> ()
+;;
+let inside c =
+ indent := !indent ^ String.make 1 c;
+ if debug then prerr_endline ("{{{" ^ !indent ^ " ")
+;;
+let outside ok =
+ if debug then prerr_endline "}}}";
+ if not ok then pp (lazy "exception raised!");
  try
   indent := String.sub !indent 0 (String.length !indent -1)
  with
   Invalid_argument _ -> indent := "??"; ()
 ;;
 
-let pp s = 
-  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
-;;
-
-let pp _ = ();;
-
 let ppcontext ~metasenv ~subst c = 
       "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
 ;;
@@ -186,7 +192,38 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   let metasenv, subst, t = 
     match ty with 
     | NCic.Implicit (`Typeof _) -> 
-       metasenv,subst, t
+       (let ty_t =
+         try
+          t (*
+          NCicTypeChecker.typeof ~subst ~metasenv context t*)
+         with
+            NCicTypeChecker.AssertFailure msg ->
+             let exc_to_be =
+              fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
+             pp (lazy "fine typeof (fallimento)");
+             let ft = fix_sorts swap exc_to_be t in
+             if ft == t then 
+               (prerr_endline ( ("ILLTYPED: " ^ 
+                  NCicPp.ppterm ~metasenv ~subst ~context t
+              ^ "\nBECAUSE:" ^ Lazy.force msg ^ 
+              ppcontext ~metasenv ~subst context ^ 
+              ppmetasenv ~subst metasenv
+              ));
+                       assert false)
+             else
+              (try 
+                pp (lazy ("typeof: " ^ 
+                  NCicPp.ppterm ~metasenv ~subst ~context ft));
+                NCicTypeChecker.typeof ~subst ~metasenv context ft
+              with NCicTypeChecker.AssertFailure _ -> 
+                assert false)
+          | NCicTypeChecker.TypeCheckerFailure _ -> assert false
+        in
+         match NCicReduction.whd ~subst context ty_t with
+            NCic.Sort _ -> metasenv,subst, t
+          | NCic.Meta _ -> metasenv,subst,t (* CSC: TO BE IMPLEMENTED *)
+          | _ -> raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
+            (*CSC: TO BE IMPLEMENTED: UnificationFailure of string Lazy.t;; *)
          (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
     | _ ->
        pp (lazy (
@@ -282,7 +319,7 @@ and instantiate rdb 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 
+ (*D*)  in outside true; rc with exn -> outside false; raise exn 
 
 and unify rdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
@@ -541,9 +578,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                 NCicUntrusted.metas_of_term subst context t2 = [] -> 
                   raise (fail_exc metasenv subst context t1 t2)
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
-     (*D*)  in outside(); rc with exn -> outside (); raise exn 
+     (*D*)  in outside true; rc with exn -> outside false; raise exn 
     in
     let try_hints metasenv subst t1 t2 (* exc*) =
+    (*D*) inside 'H'; try let rc =  
 (*
       prerr_endline ("\nProblema:\n" ^
         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
@@ -555,8 +593,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
       let rec cand_iter = function
         | [] -> None (* raise exc *)
         | (metasenv,(c1,c2),premises)::tl -> 
-(*
-            prerr_endline ("\nProvo il candidato:\n" ^ 
+            pp (lazy ("\nProvo il candidato:\n" ^ 
               String.concat "\n"
                 (List.map 
                   (fun (a,b) ->
@@ -564,9 +601,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                    NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
               "\n-------------------------------------------\n"^
               NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " = " ^
-              NCicPp.ppterm ~metasenv ~subst ~context c2);
-*)
+              NCicPp.ppterm ~metasenv ~subst ~context c2));
             try 
+    (*D*) inside 'K'; try let rc =  
               let metasenv,subst = 
                 fo_unif test_eq_only metasenv subst t1 c1 in
               let metasenv,subst = 
@@ -578,11 +615,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                   (metasenv, subst) premises
               in
               Some (metasenv, subst)
+     (*D*)  in outside true; rc with exn -> outside false; raise exn 
             with
               UnificationFailure _ | Uncertain _ ->
                 cand_iter tl
       in
         cand_iter candidates
+     (*D*)  in outside true; rc with exn -> outside false; raise exn 
     in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
@@ -651,7 +690,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           ) (metasenv,subst) todo
         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
            unif_machines metasenv subst (small_delta_step ~subst m1 m2)
-      (*D*)  in outside(); rc with exn -> outside (); raise exn 
+      (*D*)  in outside true; rc with exn -> outside false; raise exn 
      in
      try fo_unif test_eq_only metasenv subst t1 t2
      with 
@@ -672,7 +711,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           with 
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn
- (*D*)  in outside(); rc with exn -> outside (); raise exn 
+ (*D*)  in outside true; rc with exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
   let (metasenv, subst), t =