X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=954c4835bcd05b3d7a126ed7483656f0bcdc08bc;hb=b89690596acb0b24f1fd45da28ac04b4ad217e98;hp=f680b01f1e3cd2a75bc21c2b33729c8c3d8661ff;hpb=edc5e28c59721e358e5d0bc32a7a44d500918386;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index f680b01f1..954c4835b 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -91,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = try Cic.CicHash.find localization_tbl t with Not_found -> - prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); raise exn' in raise (HExtlib.Localized (loc,exn')) @@ -166,7 +166,7 @@ let more_args_than_expected localization_tbl metasenv subst he context hetype' r enrich localization_tbl he ~f:(fun _-> msg) exn ;; -let mk_prod_of_metas metasenv context' subst args = +let mk_prod_of_metas metasenv context subst args = let rec mk_prod metasenv context' = function | [] -> let (metasenv, idx) = @@ -191,14 +191,11 @@ let mk_prod_of_metas metasenv context' subst args = (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in context'. *) let name_hint = - (* Cic.Name "pippo" *) FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context') + (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous ~typ:(CicMetaSubst.apply_subst subst argty) in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name ~subst [] context' name_hint ~typ:(Cic.Sort Cic.Prop) in @@ -207,7 +204,7 @@ let mk_prod_of_metas metasenv context' subst args = in metasenv,Cic.Prod (name,meta,target) in - mk_prod metasenv context' args + mk_prod metasenv context args ;; let rec type_of_constant uri ugraph = @@ -571,7 +568,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("(10)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type @@ -616,7 +613,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("(11)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -803,7 +800,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("(12)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' @@ -844,7 +841,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(13)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -897,7 +894,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(14)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1207,14 +1204,16 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (fun (metasenv,last,coerc) -> let pp t = CicMetaSubst.ppterm_in_context ~metasenv subst t context in - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last he ugraph in - debug_print (lazy ("New head: "^ pp coerc)); try + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last he ugraph in + debug_print (lazy ("New head: "^ pp coerc)); let tty,ugraph = - CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in - debug_print (lazy (" has type: "^ pp tty)); - Some (coerc,tty,subst,metasenv,ugraph) + CicTypeChecker.type_of_aux' ~subst metasenv context coerc + ugraph + in + debug_print (lazy (" has type: "^ pp tty)); + Some (coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1376,10 +1375,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fo_unif_subst subst context metasenv infty expty ugraph in (t, expty), subst, metasenv, ugraph - with Uncertain _ | RefineFailure _ as exn -> - if not allow_coercions || not !insert_coercions then - enrich localization_tbl t exn - else + with (Uncertain _ | RefineFailure _ as exn) + when allow_coercions && !insert_coercions -> let whd = CicReduction.whd ~delta:false in let clean t s c = whd c (CicMetaSubst.apply_subst s t) in let infty = clean infty subst context in @@ -1832,11 +1829,41 @@ let typecheck metasenv uri obj ~localization_tbl = let ugraph = CicUniv.empty_ugraph in match obj with Cic.Constant (name,Some bo,ty,args,attrs) -> + (* CSC: ugly code. Here I need to retrieve in advance the loc of bo + since type_of_aux' destroys localization information (which are + preserved by type_of_aux *) + let loc exn' = + try + Cic.CicHash.find localization_tbl bo + with Not_found -> + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo); + raise exn' in let bo',boty,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] bo ugraph in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let subst,metasenv,ugraph = + try + fo_unif_subst [] [] metasenv boty ty' ugraph + with + RefineFailure _ + | Uncertain _ as exn -> + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ + " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ + " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) + in + let exn' = + match exn with + RefineFailure _ -> RefineFailure msg + | Uncertain _ -> Uncertain msg + | _ -> assert false + in + raise (HExtlib.Localized (loc exn',exn')) + in let bo' = CicMetaSubst.apply_subst subst bo' in let ty' = CicMetaSubst.apply_subst subst ty' in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in