From 34fad691712f60b4cd11510b9f73c09d25eaf125 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Nov 2005 15:48:40 +0000 Subject: [PATCH] * More error messages localized. * Bug fixed: a few Uncertain became RefineFailure in my last commit(s). --- helm/ocaml/cic_unification/cicRefine.ml | 67 +++++++++++++++---------- 1 file changed, 40 insertions(+), 27 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 5f6c1458d..9c78c1aa7 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -309,15 +309,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match coercion_src with | Cic.Sort _ -> t,type_to_coerce,subst,metasenv,ugraph -(* - | Cic.Meta _ as meta when not in_source -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let subst, metasenv, ugraph = - fo_unif_subst - subst context metasenv meta coercion_tgt ugraph - in - t, Cic.Sort tgt_sort, subst, metasenv, ugraph -*) | Cic.Meta _ as meta -> t, meta, subst, metasenv, ugraph | Cic.Cast _ as cast -> @@ -328,10 +319,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let boh = search coercion_src coercion_tgt in (match boh with | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ - | CoercGraph.NotMetaClosed -> + | CoercGraph.NotHandled _ -> enrich localization_tbl t (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl t + (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion c -> Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) in @@ -372,10 +365,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion c -> Cic.Appl [c;s'], coercion_tgt | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ - | CoercGraph.NotMetaClosed -> + | CoercGraph.NotHandled _ -> enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl s' + (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -460,9 +455,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t C.InductiveDefinition (l,expl_params,parsno,_) -> List.nth l i , expl_params, parsno, u | _ -> - raise - (RefineFailure - (lazy ("Unkown mutual inductive definition " ^ + enrich localization_tbl t + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in let rec count_prod t = @@ -498,8 +493,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv,ugraph3 = + try fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 + with + exn -> + enrich localization_tbl term' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst term' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst expected_type' context)) in let rec instantiate_prod t = function @@ -1032,18 +1038,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - let msg _e = - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)) - in - enrich localization_tbl hete ~f:msg exn + enrich localization_tbl hete + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on meta")) + enrich localization_tbl hete + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in -- 2.39.2