X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=d10e177d02d61b3aa783353a5582fa134f06dad4;hb=91f15c0bab1f2e11ef2bf77b5091c52daf64669b;hp=3d58e9acf8522950a911499122c1abb464ed5cd6;hpb=2a12ea82de3c63b05b06e3a21e434dd56b427568;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 3d58e9acf..d10e177d0 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -141,17 +141,17 @@ let is_a_double_coercion t = | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> let sib2,head = last_of tl2 in true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl - (c2::sib2@[Cic.Implicit None])]) + (c2::sib2@[imp])]) | _ -> dummyres) | _ -> 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 @@ -321,8 +321,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = + 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 = Cic.Appl[c;t] in + let coerced = + match c with + C.Appl l2 -> C.Appl (l2@[t]) + | _ -> C.Appl [c;t] + in try let newt,_,subst,metasenv,ugraph = type_of_aux subst metasenv context coerced ugraph @@ -334,9 +341,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t with | RefineFailure _ | Uncertain _ -> None in - let module C = Cic in - let module S = CicSubstitution in - let module U = UriManager 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 -> @@ -420,11 +427,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl te' ~f:(fun _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst'' te' + CicMetaSubst.ppterm_in_context metasenv'' subst'' te' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst'' inferredty + CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst'' ty' context)) exn + 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 @@ -453,17 +460,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv 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 ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -478,10 +485,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort")))) in @@ -502,8 +509,8 @@ 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) -> @@ -527,17 +534,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv 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 ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -552,9 +559,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) in @@ -684,11 +691,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl term' exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst 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 @@ -904,11 +911,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl p exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst p + 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 @@ -945,11 +952,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + 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' @@ -998,11 +1005,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + 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' @@ -1061,8 +1068,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | Some t,Some (_,C.Def (ct,_)) -> let subst',metasenv',ugraph' = (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) -> @@ -1073,19 +1081,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (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 = @@ -1118,9 +1126,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 = @@ -1132,7 +1140,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1144,9 +1154,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1165,17 +1178,28 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 + t,ty,subst,metasenv,ugraph + else let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in if b then let source_carr = CoercGraph.source_of c2 in @@ -1216,11 +1240,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | RefineFailure s | Uncertain s -> debug_print s;debug_print (lazy "goon\n"); try + let old_pack_coercions = !pack_coercions in pack_coercions := false; (* to avoid diverging *) let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = type_of_aux subst metasenv context c1_c2_implicit ugraph in - pack_coercions := true; + pack_coercions := old_pack_coercions; let b, _, _, _, _ = is_a_double_coercion refined_c1_c2_implicit in @@ -1292,8 +1317,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* {{{ 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 @@ -1330,7 +1355,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t HExtlib.list_findopt (fun coerc -> let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) @@ -1342,8 +1367,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1361,13 +1386,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None - with Uncertain _ | RefineFailure _ -> None) + with Uncertain _ | 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 *) @@ -1404,24 +1430,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - enrich localization_tbl hete - (RefineFailure + enrich localization_tbl hete exn + ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + 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 + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete - (Uncertain + enrich localization_tbl hete exn + ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + 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 + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -1451,22 +1477,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + 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 + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + 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 + 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 @@ -1483,13 +1509,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1498,7 +1524,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 = @@ -1732,7 +1758,9 @@ let pack_coercion metasenv ctx t = C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) | C.LetIn (name,so,dest) -> let _,ty,metasenv,ugraph = + pack_coercions := false; type_of_aux' metasenv ctx so CicUniv.empty_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) | C.Appl l -> @@ -1748,7 +1776,6 @@ let pack_coercion metasenv ctx t = try type_of_aux' metasenv ctx t ugraph with RefineFailure _ | Uncertain _ -> - prerr_endline (CicPp.ppterm t); t, t, [], ugraph in insert_coercions := old_insert_coercions; @@ -1803,6 +1830,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 @@ -1823,29 +1875,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)