From: Enrico Tassi Date: Thu, 5 Apr 2007 13:17:08 +0000 (+0000) Subject: many printings added X-Git-Tag: 0.4.95@7852~547 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=481340536d31492773c34d9413122abf7fef7959;p=helm.git many printings added --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 120fed3eb..1490417f1 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -78,8 +78,10 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) + | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg) | Sys.Break -> raise exn - | _ -> assert false in + | _ -> prerr_endline (Printexc.to_string exn); assert false + in let loc = try Cic.CicHash.find localization_tbl t @@ -422,7 +424,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl te' ~f:(fun _ -> - lazy ("The term " ^ + lazy ("(3)The term " ^ CicMetaSubst.ppterm_in_context metasenv'' subst'' te' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty @@ -455,7 +457,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotHandled _ -> enrich localization_tbl t (RefineFailure - (lazy ("The term " ^ + (lazy ("(4)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -463,7 +465,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotMetaClosed -> enrich localization_tbl t (Uncertain - (lazy ("The term " ^ + (lazy ("(5)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -479,7 +481,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | None -> enrich localization_tbl t (RefineFailure - (lazy ("The term " ^ + (lazy ("(6)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ @@ -527,7 +529,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotHandled _ -> enrich localization_tbl s' (RefineFailure - (lazy ("The term " ^ + (lazy ("(7)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -535,7 +537,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotMetaClosed -> enrich localization_tbl s' (Uncertain - (lazy ("The term " ^ + (lazy ("(8)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -551,7 +553,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | None -> enrich localization_tbl s' (RefineFailure - (lazy ("The term " ^ + (lazy ("(9)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -675,15 +677,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context expected_type ugraph1 in let actual_type = CicReduction.whd ~subst context actual_type in + prerr_endline (CicPp.ppterm expected_type'); + prerr_endline (CicPp.ppterm actual_type); let subst,metasenv,ugraph3 = try fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 with exn -> + prerr_endline (CicMetaSubst.ppmetasenv subst metasenv); + prerr_endline (CicMetaSubst.ppsubst subst ~metasenv); enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(10)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type @@ -728,7 +734,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("The term " ^ + lazy ("(11)The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -916,7 +922,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(12)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' @@ -957,7 +963,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(13)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1010,7 +1016,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(14)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1446,7 +1452,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NotHandled _ -> enrich localization_tbl hete exn ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(15)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1456,7 +1462,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NotMetaClosed -> enrich localization_tbl hete exn ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(16)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1492,7 +1498,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | None -> enrich localization_tbl hete ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(1)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1502,7 +1508,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | exn -> enrich localization_tbl hete ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(2)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety