From 20e70a2cdbafd0c720e1e6682e0497e6ed964439 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 10 May 2012 14:18:17 +0000 Subject: [PATCH] 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). --- matita/components/ng_kernel/nCicTypeChecker.ml | 11 ++++++----- matita/components/ng_refiner/nCicMetaSubst.ml | 5 +++++ matita/matita/applyTransformation.ml | 10 +++++----- 3 files changed, 16 insertions(+), 10 deletions(-) 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 -- 2.39.2