Patch to improve the pretty-printing of error messages.

Moreover, when a delift creates an ill-typed term, a more
informative error message is printed (even if later
backtracking makes it irrelevant).

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 0a73358e004ad243f18d3f27f4c1d0ab311309d0..d2ad6a55f799015fc044550953dd18bf1d649887 100644 (file)
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -698,15 +698,16 @@ and eat_prods status ~subst ~metasenv context he ty_he args_with_ty =
           if R.are_convertible status ~metasenv ~subst context ty_arg s then
             aux (S.subst status ~avoid_beta_redexes:true arg t) tl
           else
+           let indent s = "   " ^ (Str.global_replace (Str.regexp "\n") "\n   " s) in
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the argument %s has type"^^
+                  ("Appl: wrong application of\n%s\nThe argument\n%s\nhas type"^^
                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
-                  (status#ppterm ~subst ~metasenv ~context he)
-                  (status#ppterm ~subst ~metasenv ~context arg)
-                  (status#ppterm ~subst ~metasenv ~context ty_arg)
-                  (status#ppterm ~subst ~metasenv ~context s)
+                  (indent (status#ppterm ~subst ~metasenv ~context he))
+                  (indent (status#ppterm ~subst ~metasenv ~context arg))
+                  (indent (status#ppterm ~subst ~metasenv ~context ty_arg))
+                  (indent (status#ppterm ~subst ~metasenv ~context s))
                   (status#ppcontext ~subst ~metasenv context))))
        | _ ->
           raise 

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 57f12a458fd160bb3a1917bbad2079101aad7e00..e3ee8d60e0bdb48025c46a84da36e107d7f8e42f 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -515,6 +515,11 @@ let delift status ~unify metasenv subst context n l t =
         NCicUtils.Meta_not_found _ ->
          (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
          assert (n = -1); res
+      | NCicTypeChecker.TypeCheckerFailure msg ->
+         HLog.error "----------- Problem with Dependent Types ----------";
+         HLog.error (Lazy.force msg) ;
+         HLog.error "---------------------------------------------------";
+         raise (NotFound `NotWellTyped)
       | TypeNotGood
       | NCicTypeChecker.AssertFailure _
       | NCicReduction.AssertFailure _

diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 705ef7936df0b993176d11093c6f03b7104004c7..df366a9ae633bd032ed2363ea25679c85c8a953c 100644 (file)
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -76,23 +76,23 @@ class status =
   inherit Interpretations.status
   inherit TermContentPres.status
   method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
-   snd (ntxt_of_cic_term ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+   snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
     ~context t)
 
   method ppcontext ?sep ~subst ~metasenv context =
-   snd (ntxt_of_cic_context ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+   snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
     context)
 
   method ppsubst ~metasenv ?use_subst subst =
-   snd (ntxt_of_cic_subst ~map_unicode_to_tex:true 80 self ~metasenv ?use_subst
+   snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
     subst)
 
   method ppmetasenv ~subst metasenv =
    String.concat "\n"
     (List.map
-      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
+      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:false 80 self
         ~metasenv ~subst m)) metasenv)
 
   method ppobj obj =
-   snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj)
+   snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj)
  end