From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 May 2012 14:18:17 +0000 (+0000)
Subject: Patch to improve the pretty-printing of error messages.
X-Git-Tag: make_still_working~1759
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20e70a2cdbafd0c720e1e6682e0497e6ed964439;p=helm.git

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 0a73358e0..d2ad6a55f 100644
--- 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 57f12a458..e3ee8d60e 100644
--- 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 705ef7936..df366a9ae 100644
--- 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