From: Enrico Tassi Date: Thu, 30 Aug 2007 16:25:17 +0000 (+0000) Subject: refactoring of all coercions code and add a check to not perform a coercion check... X-Git-Tag: make_still_working~6085 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf631c30a99da7137628d43ded7c097647e16f35;p=helm.git refactoring of all coercions code and add a check to not perform a coercion check if it is not needed --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index ad5ae94dc..a73313eba 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -416,37 +416,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - (try - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty' ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - | Uncertain _ | RefineFailure _ -> - let exn = - RefineFailure (lazy ("(3)The term " ^ - CicMetaSubst.ppterm_in_context metasenv'' subst'' te' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context metasenv'' - subst'' inferredty context ^ - " but is here used with type " ^ - CicMetaSubst.ppterm_in_context - metasenv'' subst'' ty' context)) - in - try - let (te, ty), subst, metasenv, ugraph = - coerce_to_something te' inferredty ty' - subst'' metasenv'' context exn ugraph2 - in - C.Cast (te, ty'), ty', subst, metasenv, ugraph - with exn -> enrich localization_tbl te' exn) + let (te', ty'), subst''',metasenv''',ugraph3 = + coerce_to_something true localization_tbl te' inferredty ty' + subst'' metasenv'' context ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let s',sort1,subst', metasenv',ugraph1 = - coerce_to_sort true (Cic.Type(CicUniv.fresh())) + coerce_to_sort localization_tbl s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (name,(C.Decl s')))::context) in @@ -455,7 +435,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context_for_t t ugraph1 in let t',sort2,subst'',metasenv'',ugraph2 = - coerce_to_sort false (Cic.Type(CicUniv.fresh())) + coerce_to_sort localization_tbl t' sort2 subst'' context_for_t metasenv'' ugraph2 in let sop,subst''',metasenv''',ugraph3 = @@ -468,7 +448,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context s ugraph in let s',sort1,subst',metasenv',ugraph1 = - coerce_to_sort true (Cic.Type(CicUniv.fresh())) + coerce_to_sort localization_tbl s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (n,(C.Decl s')))::context) in @@ -1333,33 +1313,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | (hete, hety)::tl -> match (CicReduction.whd ~subst context hetype) with | Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph1 = - try - (try - let subst,metasenv,ugraph1 = - fo_unif_subst_eat_prods2 - subst context metasenv hety s ugraph - in - (hete,hety),subst,metasenv,ugraph1 - with RefineFailure _ | Uncertain _ as exn - when allow_coercions && !insert_coercions -> - coerce_to_something - hete hety s subst metasenv context exn ugraph) - with exn -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("(2)The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context - ~metasenv subst s context - (* "\nReason: " ^ Printexc.to_string exn*)))) exn - in - eat_prods_and_args pristinemenv metasenv subst context pristinehe he - (CicSubstitution.subst (fst arg) t) - ugraph1 (newargs@[arg]) tl + let arg,subst,metasenv,ugraph = + coerce_to_something allow_coercions localization_tbl + hete hety s subst metasenv context ugraph in + eat_prods_and_args + pristinemenv metasenv subst context pristinehe he + (CicSubstitution.subst (fst arg) t) + ugraph (newargs@[arg]) tl | _ -> try let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = @@ -1368,7 +1328,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (newargs@[hete,hety]@tl) ugraph in eat_prods_and_args metasenv - metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty + metasenv subst context pristinehe he hetype' + ugraph [] args_bo_and_ty with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) more_args_than_expected localization_tbl metasenv @@ -1395,106 +1356,126 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in he,(List.map fst coerced_args),t,subst,metasenv,ugraph - and coerce_to_something t infty expty subst metasenv context exn ugraph = - if not !insert_coercions then - raise exn - else - let clean t subst context = - CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t) - in - let infty = clean infty subst context in - let expty = clean expty subst context in - match infty, expty with - | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> - (* covariant part *) - let name_con = Cic.Name "name_con" in - let name_t, ty_s_bo, bo = - match t with - | Cic.Lambda (name, src, bo) -> name, src, bo - | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1] - in - let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in - let (bo, _), subst, metasenv, ugraph = - coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph - in - (* contravariant part *) - let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2) - (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn - ugraph - in - let coerced = - Cic.Lambda (name_t,src2, - CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo)) - in - (coerced, expty), subst, metasenv, ugraph - | _ -> - coerce_atom_to_something t infty expty subst metasenv context exn ugraph - - and coerce_atom_to_something t infty expty subst metasenv context exn ugraph = - let coer = - CoercGraph.look_for_coercion metasenv subst context infty expty - in + and coerce_to_something + allow_coercions localization_tbl t infty expty subst metasenv context ugraph + = + let coerce_atom_to_something t infty expty subst metasenv context ugraph = + let coer = + CoercGraph.look_for_coercion metasenv subst context infty expty + in match coer with - | CoercGraph.NotMetaClosed -> - (match exn with - | RefineFailure s -> raise (Uncertain s) - | HExtlib.Localized _ -> assert false - | _ -> raise exn) + | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy + "coerce_atom_to_something fails since not meta closed")) | CoercGraph.NoCoercion | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> - raise exn + | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + "coerce_atom_to_something fails since no coercions found")) | CoercGraph.SomeCoercion candidates -> + let uncertain = ref false in let selected = HExtlib.list_findopt (fun (metasenv,last,c) -> try let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last t - ugraph in + fo_unif_subst subst context metasenv last t ugraph in let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - c ugraph - in + type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt expty + avoid_double_coercion context subst metasenv ugraph newt expty in let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety expty ugraph - in + fo_unif_subst subst context metasenv newhety expty ugraph in Some ((newt,newty), subst, metasenv, ugraph) - with Uncertain _ | RefineFailure _ -> None) + with + | Uncertain _ -> uncertain := true; None + | RefineFailure _ -> None) candidates in match selected with | Some x -> x - | None -> raise exn + | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails")) + | None -> raise (RefineFailure (lazy "coerce_atom fails")) + in + let rec coerce_to_something_aux + t infty expty subst metasenv context ugraph + = + try + let subst, metasenv, ugraph = + 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 + let clean t subst context = + CicReduction.whd + ~delta:false context (CicMetaSubst.apply_subst subst t) + in + let infty = clean infty subst context in + let expty = clean expty subst context in + match infty, expty with + | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> + (* covariant part *) + let name_con = Cic.Name "name_con" in + let name_t, ty_s_bo, bo = + match t with + | Cic.Lambda (name, src, bo) -> name, src, bo + | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1] + in + let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in + let (bo, _), subst, metasenv, ugraph = + coerce_to_something_aux + bo ty ty2 subst metasenv context_bo ugraph + in + (* contravariant part *) + let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux + (Cic.Rel 1) (CicSubstitution.lift 1 src2) + (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph + in + let coerced = + Cic.Lambda (name_t,src2, + CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo)) + in + (coerced, expty), subst, metasenv, ugraph + | _ -> + coerce_atom_to_something t infty expty subst metasenv context ugraph + in + try + coerce_to_something_aux t infty expty subst metasenv context ugraph + with Uncertain _ | RefineFailure _ -> + let exn = + RefineFailure (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst t context ^ + " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst + infty context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context metasenv subst expty context)) + in + enrich localization_tbl t exn - and coerce_to_sort - in_source tgt_sort t type_to_coerce subst context metasenv uragph = - match CicReduction.whd ~subst:subst context type_to_coerce with - | Cic.Meta _ | Cic.Sort _ -> - t,type_to_coerce, subst, metasenv, ugraph - | src -> - let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - let exn = - RefineFailure (lazy ("(7)The term " ^ + and coerce_to_sort localization_tbl t infty subst context metasenv uragph = + match CicReduction.whd ~subst:subst context infty with + | Cic.Meta _ | Cic.Sort _ -> + t,infty, subst, metasenv, ugraph + | src -> + let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in + try + let (t, ty_t), subst, metasenv, ugraph = + coerce_to_something true + localization_tbl t src tgt subst metasenv context ugraph + in + t, ty_t, subst, metasenv, ugraph + with HExtlib.Localized (_, exn) -> + let f _ = + lazy ("(7)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst src context - ^ " that is not a sort")) + ^ " that is not a sort") in - try - let (t, ty_t), subst, metasenv, ugraph = - coerce_to_something t src tgt - subst metasenv context exn ugraph - in - t, ty_t, subst, metasenv, ugraph - with exn -> enrich localization_tbl t exn + enrich localization_tbl ~f t exn in (* eat prods ends here! *)