From: Enrico Tassi Date: Thu, 30 Aug 2007 13:24:13 +0000 (+0000) Subject: Coercions rework: X-Git-Tag: make_still_working~6089 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6bf40d380bdb66e1cb3315edebb3d276ba7a125;p=helm.git Coercions rework: - new functions: - coerce_to_sort - coerce_to_something - coerce_atom_to_something - added call in Cast - coerce_to_something goes under lambdas in both variant and contravarian positions, to if there are c1: B -> B1 and c2:A1 -> C coercions, you can cast a function f: A -> B to A1 -> B1. --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 856c9a586..ad5ae94dc 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -326,6 +326,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module C = Cic in let module S = CicSubstitution in let module U = UriManager in +(* let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) = let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last t ugraph @@ -339,6 +340,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t with | RefineFailure _ | Uncertain _ -> None in +*) let (t',_,_,_,_) as res = match t with (* function *) @@ -420,76 +422,26 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t inferredty ty' ugraph2 in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - exn -> - enrich localization_tbl te' - ~f:(fun _ -> - 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)) exn - ) - | C.Prod (name,s,t) -> - let carr t subst context = CicMetaSubst.apply_subst subst t in - let coerce_to_sort in_source tgt_sort t type_to_coerce - subst context metasenv uragph - = - if not !insert_coercions then - t,type_to_coerce,subst,metasenv,ugraph - else - let coercion_src = carr type_to_coerce subst context in - match coercion_src with - | Cic.Sort _ -> - t,type_to_coerce,subst,metasenv,ugraph - | Cic.Meta _ as meta -> - t, meta, subst, metasenv, ugraph - | Cic.Cast _ as cast -> - t, cast, subst, metasenv, ugraph - | term -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let boh = - CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt + 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 - (match boh with - | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> - enrich localization_tbl t - (RefineFailure - (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 - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl t - (Uncertain - (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 - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (try_coercion t subst context ugraph coercion_tgt) - candidates - in - match selected with - | Some x -> x - | None -> - enrich localization_tbl t - (RefineFailure - (lazy ("(6)The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv - subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv - subst coercion_src context ^ - " that is not a sort")))) - in + C.Cast (te, ty'), ty', subst, metasenv, ugraph + with exn -> enrich localization_tbl te' exn) + | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in @@ -513,54 +465,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 + type_of_aux subst metasenv context s ugraph + in let s',sort1,subst',metasenv',ugraph1 = - if not !insert_coercions then - s',sort1, subst', metasenv', ugraph1 - else - match CicReduction.whd ~subst:subst' context sort1 with - | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 - | coercion_src -> - let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - let boh = - CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt - in - match boh with - | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> - enrich localization_tbl s' - (RefineFailure - (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 - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl s' - (Uncertain - (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 - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (try_coercion s' subst' context ugraph1 coercion_tgt) - candidates - in - match selected with - | Some x -> x - | None -> - enrich localization_tbl s' - (RefineFailure - (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 - subst coercion_src context ^ - " that is not a sort"))) + coerce_to_sort true (Cic.Type(CicUniv.fresh())) + s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -685,8 +594,6 @@ 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 ("(10)The term " ^ @@ -852,8 +759,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t candidate_oty,ugraph,metasenv,subst with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> + | RefineFailure _ | Uncertain _ -> None,ugraph,metasenv,subst ) (Some instance',ugraph4,metasenv,subst) tl in @@ -1393,9 +1299,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il debug_print (lazy " success!"); Some (subst,metasenv,ugraph,tty,t,remainder) with - | Uncertain _ | RefineFailure _ - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> + | Uncertain _ | RefineFailure _ -> try let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = fix_arity @@ -1430,84 +1334,18 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il match (CicReduction.whd ~subst context hetype) with | Cic.Prod (n,s,t) -> let arg,subst,metasenv,ugraph1 = - try + try + (try let subst,metasenv,ugraph1 = fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph in (hete,hety),subst,metasenv,ugraph1 - (* {{{ we search a coercion from hety to s if fails *) with RefineFailure _ | Uncertain _ as exn when allow_coercions && !insert_coercions -> - let coer, tgt_carr = - let carr t subst context = - CicReduction.whd ~delta:false - context (CicMetaSubst.apply_subst subst t ) - in - let c_hety = carr hety subst context in - let c_s = carr s subst context in - CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s - in - (match coer with - | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> - enrich localization_tbl hete exn - ~f:(fun _ -> - (lazy ("(15)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: " ^ Lazy.force e*)))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete exn - ~f:(fun _ -> - (lazy ("(16)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: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (fun (metasenv,last,c) -> - try - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last hete - ugraph in - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - c ugraph - in - let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt tgt_carr - in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - Some ((newt,newty), subst, metasenv, ugraph) - with Uncertain _ | RefineFailure _ -> None) - candidates - in - (match selected with - | Some x -> x - | None -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("(1)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: " ^ Lazy.force e*)))) exn)) - | exn -> + coerce_to_something + hete hety s subst metasenv context exn ugraph) + with exn -> enrich localization_tbl hete ~f:(fun _ -> (lazy ("(2)The term " ^ @@ -1515,9 +1353,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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 + CicMetaSubst.ppterm_in_context + ~metasenv subst s context (* "\nReason: " ^ Printexc.to_string exn*)))) exn - (* }}} end coercion stuff *) in eat_prods_and_args pristinemenv metasenv subst context pristinehe he (CicSubstitution.subst (fst arg) t) @@ -1556,6 +1394,107 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty 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 + match coer with + | CoercGraph.NotMetaClosed -> + (match exn with + | RefineFailure s -> raise (Uncertain s) + | HExtlib.Localized _ -> assert false + | _ -> raise exn) + | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ + | CoercGraph.NotHandled _ -> + raise exn + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun (metasenv,last,c) -> + try + let subst,metasenv,ugraph = + 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 + let newt, newty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv + ugraph newt expty + in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety expty ugraph + in + Some ((newt,newty), subst, metasenv, ugraph) + with Uncertain _ | RefineFailure _ -> None) + candidates + in + match selected with + | Some x -> x + | None -> raise 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 " ^ + 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")) + 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 in (* eat prods ends here! *) @@ -1792,7 +1731,6 @@ let pack_coercion metasenv ctx t = let l = List.map (merge_coercions ctx) l in let t = C.Appl l in let b,_,_,_,_ = is_a_double_coercion t in - (* prerr_endline "CANDIDATO!!!!"; *) if b then let ugraph = CicUniv.oblivion_ugraph in let old_insert_coercions = !insert_coercions in