X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=ad5ae94dcb350c5772939dc5681343a8be8e6542;hb=396a578b680e7fdb9d262822184e52f0d4d5086b;hp=1f2a8a19ef771005df2135e2db894e046c7aca4a;hpb=3234ad630868fed918d9f3408da53e39e507d3d9;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 1f2a8a19e..ad5ae94dc 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 @@ -136,9 +138,9 @@ let is_a_double_coercion t = let imp = Cic.Implicit None in let dummyres = false,imp, imp,imp,imp in match t with - | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> + | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> let sib2,head = last_of tl2 in true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl (c2::sib2@[imp])]) @@ -146,12 +148,12 @@ let is_a_double_coercion t = | _ -> dummyres let more_args_than_expected - localization_tbl subst he context hetype' tlbody_and_type exn + localization_tbl metasenv subst he context hetype' tlbody_and_type exn = let msg = lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he context ^ - " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ + " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ " arguments that are more than expected") in @@ -324,19 +326,21 @@ 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 metasenv context ugraph coercion_tgt c = - let coerced = C.Appl[c;t] 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 + in try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context coerced ugraph - in let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt coercion_tgt + avoid_double_coercion context subst metasenv ugraph coerced + coercion_tgt in Some (newt, tty, subst, metasenv, ugraph) with | RefineFailure _ | Uncertain _ -> None in +*) let (t',_,_,_,_) as res = match t with (* function *) @@ -395,8 +399,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst', metasenv',ugraph1) | C.Sort (C.Type tno) -> let tno' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt tno' tno ugraph in - t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + (try + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph | C.Implicit infos -> @@ -415,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 ("The term " ^ - CicMetaSubst.ppterm_in_context subst'' te' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst'' inferredty - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context 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 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.NotHandled _ -> - enrich localization_tbl t - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl t - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (try_coercion - t subst metasenv context ugraph coercion_tgt) - candidates - in - match selected with - | Some x -> x - | None -> - enrich localization_tbl t - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context - subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - 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 @@ -502,61 +459,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t t' sort2 subst'' context_for_t metasenv'' ugraph2 in let sop,subst''',metasenv''',ugraph3 = - sort_of_prod subst'' metasenv'' - context (name,s') (sort1,sort2) ugraph2 + sort_of_prod localization_tbl subst'' metasenv'' + context (name,s') t' (sort1,sort2) ugraph2 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 + 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 coercion_src coercion_tgt - in - match boh with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl s' - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl s' - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (try_coercion - s' subst' metasenv' context ugraph1 coercion_tgt) - candidates - in - match selected with - | Some x -> x - | None -> - enrich localization_tbl s' - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - 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 = @@ -683,12 +596,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst term' + lazy ("(10)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst actual_type + CicMetaSubst.ppterm_in_context ~metasenv subst actual_type context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_type' context)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) in let rec instantiate_prod t = function @@ -704,8 +617,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* TODO: check if the sort elimination * is allowed: [(I q1 ... qr)|B] *) let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = - List.fold_left - (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p -> + List.fold_right + (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) -> let constructor = if left_args = [] then (C.MutConstruct (uri,i,j,exp_named_subst)) @@ -720,12 +633,25 @@ 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 - (pl @ [p'],j+1, - outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) - ([],1,[],subst,metasenv,ugraph3) pl + (p'::pl,j-1, + outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) + pl ([],List.length pl,[],subst,metasenv,ugraph3) in (* we are left to check that the outype matches his instances. @@ -833,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 @@ -903,12 +828,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst p + lazy ("(12)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst instance' + CicMetaSubst.ppterm_in_context ~metasenv subst instance' context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst instance + CicMetaSubst.ppterm_in_context ~metasenv subst instance context))) (subst,metasenv,ugraph5) pl' outtypeinstances in @@ -918,17 +843,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 @@ -944,12 +869,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + lazy ("(13)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'] , subst',metasenv',ugraph' @@ -971,17 +896,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 @@ -997,12 +922,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + lazy ("(14)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'],subst',metasenv',ugraph' @@ -1063,7 +988,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (try prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel."); fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -1074,19 +999,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context)))) + (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext ~metasenv subst canonical_context)))) and check_exp_named_subst metasubst metasenv context tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = @@ -1119,9 +1044,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il with _ -> raise (RefineFailure (lazy ("Wrong Explicit Named Substitution: " ^ - CicMetaSubst.ppterm metasubst' typeoft ^ + CicMetaSubst.ppterm metasenv' metasubst' typeoft ^ " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar))) + CicMetaSubst.ppterm metasenv' metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -1133,7 +1058,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il check_exp_named_subst_aux metasubst metasenv [] tl ugraph - and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph = + and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2) + ugraph + = let module C = Cic in let context_for_t2 = (Some (name,C.Decl s))::context in let t1'' = CicReduction.whd ~subst context t1 in @@ -1145,9 +1072,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),subst,metasenv,ugraph2 + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph @@ -1166,15 +1096,23 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il with _ -> assert false (* unification against a metavariable *) in t2'',subst,metasenv,ugraph1 + | (C.Sort _,_) + | (C.Meta _,_) -> + enrich localization_tbl s + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst t context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)))) | _,_ -> - raise - (RefineFailure - (lazy - (sprintf - ("Two sorts were expected, found %s " ^^ - "(that reduces to %s) and %s (that reduces to %s)") - (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2'')))) + enrich localization_tbl t + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst s context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)))) and avoid_double_coercion context subst metasenv ugraph t ty = if not !pack_coercions then @@ -1184,29 +1122,27 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il if b then let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in - (match CoercGraph.look_for_coercion source_carr tgt_carr + (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr with | CoercGraph.SomeCoercion candidates -> - let selected = + let selected = HExtlib.list_findopt - (function + (function (metasenv,last,c) -> + match c with | c when not (CoercGraph.is_composite c) -> debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); None | c -> - let newt = - match c with - | Cic.Appl l -> Cic.Appl (l @ [head]) - | _ -> Cic.Appl [c;head] - in - debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last head ugraph in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); (try debug_print (lazy ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c)); let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in + type_of_aux subst metasenv context c ugraph in debug_print (lazy "tipa..."); let subst, metasenv, ugraph = (* COME MAI C'ERA UN IF su !pack_coercions ??? *) @@ -1297,8 +1233,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ we search a coercion of the head (saturated) to funclass *) let metasenv = pristinemenv in debug_print (lazy - ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ - " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' + ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^ + " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' (* ^ " cause: " ^ Lazy.force s *))); let how_many_args_are_needed = let rec aux n = function @@ -1320,35 +1256,42 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il he in let x,xty,subst,metasenv,ugraph = - type_of_aux subst metasenv context x ugraph + (*CSC: here unsharing is necessary to avoid an unwanted + relocalization. However, this also shows a great source of + inefficiency: "x" is refined twice (once now and once in the + subsequent eat_prods_and_args). Morevoer, how is divergence avoided? + *) + type_of_aux subst metasenv context (Unshare.unshare x) ugraph in let carr_src = CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) in let carr_tgt = CoercDb.Fun 0 in - match CoercGraph.look_for_coercion' carr_src carr_tgt with + match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt - (fun coerc -> - let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + (fun (metasenv,last,coerc) -> + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last x ugraph in + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) let t,tty,subst,metasenv,ugraph = - type_of_aux subst metasenv context t ugraph + type_of_aux subst metasenv context coerc ugraph in try let metasenv, hetype' = mk_prod_of_metas metasenv context subst remainder in debug_print (lazy - (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ - CicMetaSubst.ppterm subst hetype')); + (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ + CicMetaSubst.ppterm ~metasenv subst hetype')); let subst,metasenv,ugraph = fo_unif_subst_eat_prods subst context metasenv tty hetype' ugraph @@ -1356,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 @@ -1366,13 +1307,18 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None - with Uncertain _ | RefineFailure _ -> None) + with + Uncertain _ + | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) (* ritornare None, e' un localized *) candidates with | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> subst,metasenv,ugraph,hetype',he,args_bo_and_ty | None -> - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} end coercion to funclass stuff *) (* }}} end fix_arity *) @@ -1388,91 +1334,28 @@ 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 c_hety c_s, c_s - in - (match coer with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl hete - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (fun c -> - try - let t = Cic.Appl[c;hete] in - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - t 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 ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context 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 ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + (lazy ("(2)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context ^ - "\nReason: " ^ Printexc.to_string exn))) exn - (* }}} end coercion stuff *) + 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) @@ -1488,13 +1371,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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 + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} *) in (* first we check if we are in the simple case of a meta closed term *) let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = - if CicUtil.is_meta_closed hetype then + if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then (* this optimization is to postpone fix_arity (the most common case)*) subst,metasenv,ugraph,hetype,he,args_bo_and_ty else @@ -1503,7 +1386,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il fix_arity metasenv context subst he hetype args_bo_and_ty ugraph with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph = @@ -1511,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! *) @@ -1691,6 +1675,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) -> @@ -1703,7 +1688,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 @@ -1738,7 +1723,7 @@ let pack_coercion metasenv ctx t = | C.LetIn (name,so,dest) -> let _,ty,metasenv,ugraph = pack_coercions := false; - type_of_aux' metasenv ctx so CicUniv.empty_ugraph in + type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in pack_coercions := true; let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) @@ -1746,9 +1731,8 @@ 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.empty_ugraph in + let ugraph = CicUniv.oblivion_ugraph in let old_insert_coercions = !insert_coercions in insert_coercions := false; let newt, _, menv, _ = @@ -1809,6 +1793,31 @@ let pack_coercion metasenv ctx t = merge_coercions ctx t ;; +let pack_coercion_metasenv conjectures = + let module C = Cic in + List.map + (fun (i, ctx, ty) -> + let ctx = + List.fold_right + (fun item ctx -> + let item' = + match item with + Some (name, C.Decl t) -> + Some (name, C.Decl (pack_coercion conjectures ctx t)) + | Some (name, C.Def (t,None)) -> + Some (name,C.Def (pack_coercion conjectures ctx t,None)) + | Some (name, C.Def (t,Some ty)) -> + Some (name, C.Def (pack_coercion conjectures ctx t, + Some (pack_coercion conjectures ctx ty))) + | None -> None + in + item'::ctx + ) ctx [] + in + ((i,ctx,pack_coercion conjectures ctx ty)) + ) conjectures +;; + let pack_coercion_obj obj = let module C = Cic in match obj with @@ -1829,29 +1838,7 @@ let pack_coercion_obj obj = let ty = pack_coercion [] [] ty in C.Variable (name, body, ty, params, attrs) | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> - let conjectures = - List.map - (fun (i, ctx, ty) -> - let ctx = - List.fold_right - (fun item ctx -> - let item' = - match item with - Some (name, C.Decl t) -> - Some (name, C.Decl (pack_coercion conjectures ctx t)) - | Some (name, C.Def (t,None)) -> - Some (name,C.Def (pack_coercion conjectures ctx t,None)) - | Some (name, C.Def (t,Some ty)) -> - Some (name, C.Def (pack_coercion conjectures ctx t, - Some (pack_coercion conjectures ctx ty))) - | None -> None - in - item'::ctx - ) ctx [] - in - ((i,ctx,pack_coercion conjectures ctx ty)) - ) conjectures - in + let conjectures = pack_coercion_metasenv conjectures in let body = pack_coercion conjectures [] body in let ty = pack_coercion conjectures [] ty in C.CurrentProof (name, conjectures, body, ty, params, attrs)