From: Claudio Sacerdoti Coen Date: Sat, 18 Feb 2006 12:22:18 +0000 (+0000) Subject: More refinement errors localized. X-Git-Tag: 0.4.95@7852~1656 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4eb17652f80790fef13e10fa754a416e85253150;p=helm.git More refinement errors localized. --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 52b1a1034..3faee32df 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -144,14 +144,24 @@ let avoid_double_coercion context subst metasenv ugraph t ty = let args = mk_implicits head (arity - 1) in let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in let newt = Cic.Appl (c_bo::args) in - let subst, metasenv, ugraph = - CicUnification.fo_unif_subst subst context metasenv newt t ugraph - in - debug_print - (lazy - ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args)))); - Cic.Appl (c::args), ty, subst, metasenv, ugraph + (try + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args)))); + Cic.Appl (c::args), ty, subst, metasenv, ugraph + with + RefineFailure _ -> + prerr_endline ("#### Coercion not packed (Refine_failure): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); + assert false + | Uncertain _ -> + prerr_endline ("#### Coercion not packed (Uncercatin case): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); + assert false) | _ -> assert false) (* the composite coercion must exist *) else t, ty, subst, metasenv, ugraph @@ -779,8 +789,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | None -> raise (Uncertain (lazy "can't solve an higher order unification problem")) | Some candidate -> let subst,metasenv,ugraph = + try fo_unif_subst subst context metasenv candidate outtype ugraph5 + with + exn -> assert false(* unification against a metavariable *) in C.MutCase (uri, i, outtype, term', pl'), CicReduction.head_beta_reduce @@ -806,9 +819,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 in let (subst,metasenv,ugraph6) = - List.fold_left + List.fold_left2 (fun (subst,metasenv,ugraph) - (constructor_args_no,context,instance,args) -> + p (constructor_args_no,context,instance,args) + -> let instance' = let appl = let outtype' = @@ -818,9 +832,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in CicReduction.whd ~subst context appl in - fo_unif_subst subst context metasenv - instance instance' ugraph) - (subst,metasenv,ugraph5) outtypeinstances + try + fo_unif_subst subst context metasenv instance instance' + ugraph + with + exn -> + enrich localization_tbl p exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst p + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst instance' + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst instance + context))) + (subst,metasenv,ugraph5) pl' outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), CicReduction.head_beta_reduce @@ -844,11 +870,23 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph - in + type_of_aux subst metasenv context' bo ugraph in + let expected_ty = CicSubstitution.lift len ty in let subst',metasenv',ugraph' = + try fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) ugraph1 + ty_of_bo expected_ty ugraph1 + with + exn -> + enrich localization_tbl bo exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst bo + context' ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst ty_of_bo + context' ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst expected_ty + context)) in fl @ [bo'] , subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') @@ -885,11 +923,23 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph - in + type_of_aux subst metasenv context' bo ugraph in + let expected_ty = CicSubstitution.lift len ty in let subst',metasenv',ugraph' = + try fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) ugraph1 + ty_of_bo expected_ty ugraph1 + with + exn -> + enrich localization_tbl bo exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst bo + context' ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst ty_of_bo + context' ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst expected_ty + context)) in fl @ [bo'],subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') @@ -1038,7 +1088,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we - * brake the invariant that refine produce only well typed terms *) + * break the invariant that refine produce only well typed terms *) (* TODO if we check the non meta term and if it is a sort then we * are likely to know the exact value of the result e.g. if the rhs * is a Sort (Prop | Set | CProp) then the result is the rhs *)