X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=856c9a58622480d6f938cbeb0e8a25c1ce913473;hb=975ad45cc779a6bee3d450a006347cc23ca3977e;hp=6d26a868b10e956267954ccfe1b9d0029d08f235;hpb=09e7e20a99ff7104fd1da326dc44111f81e3dc89;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 6d26a868b..856c9a586 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 @@ -452,10 +454,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in (match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | 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 +466,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 +482,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 " ^ @@ -509,7 +512,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 | C.Lambda (n,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let s',sort1,subst',metasenv',ugraph1 = @@ -525,10 +527,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | 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 @@ -536,7 +539,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 @@ -552,7 +555,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 @@ -682,9 +685,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -721,8 +726,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context constructor ugraph1 in let outtypeinstance,subst,metasenv,ugraph3 = - check_branch 0 context metasenv subst no_left_params - actual_type constructor' expected_type ugraph2 + try + check_branch 0 context metasenv subst + no_left_params actual_type constructor' expected_type + ugraph2 + with + exn -> + enrich localization_tbl constructor' + ~f:(fun _ -> + lazy ("(11)The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst p' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context metasenv subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context metasenv subst expected_type + context)) exn in (p'::pl,j-1, outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) @@ -904,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' @@ -919,17 +937,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (C.Appl(outtype::right_args@[term]))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1,len = List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> + (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl ty')) :: types, ugraph - ) ([],subst,metasenv,[],ugraph) fl + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) + :: types, ugraph, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl in - let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left @@ -945,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 @@ -972,17 +990,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Fix (i,fl''),ty,subst,metasenv,ugraph2 | C.CoFix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1,len = List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> + (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl ty')) :: types, ugraph1 - ) ([],subst,metasenv,[],ugraph) fl + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) :: + types, ugraph1, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl in - let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left @@ -998,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 @@ -1347,6 +1365,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt @@ -1431,10 +1450,11 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in (match coer with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | 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 @@ -1444,7 +1464,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 @@ -1480,7 +1500,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 @@ -1490,7 +1510,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 @@ -1716,6 +1736,7 @@ let typecheck metasenv uri obj ~localization_tbl = let con_context = List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in (* second phase: we fix only the constructors *) + let saved_menv = metasenv in let metasenv,ugraph,tys = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> @@ -1728,7 +1749,7 @@ let typecheck metasenv uri obj ~localization_tbl = let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in - metasenv,ugraph,(name,ty')::res + metasenv@saved_menv,ugraph,(name,ty')::res ) cl (metasenv,ugraph,[]) in metasenv,ugraph,(name,b,ty,cl')::res