X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=48ae522f4c9b4b170111a2dabff110e93388d863;hb=7f21c77a04c282e789dfbedf202fe90e15a7fde2;hp=620f66f1831a4ec598178645201dd7686c47c7d7;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 620f66f18..48ae522f4 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -35,6 +35,30 @@ let insert_coercions = ref true let debug_print = fun _ -> () +let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" + +let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods2.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + +let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods" + +let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + let profiler = HExtlib.profile "CicRefine.fo_unif" let fo_unif_subst subst context metasenv t1 t2 ugraph = @@ -58,7 +82,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = Cic.CicHash.find localization_tbl t with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); - assert false + raise exn' in raise (HExtlib.Localized (loc,exn')) @@ -81,20 +105,43 @@ let rec split l n = let exp_impl metasenv subst context = function | Some `Type -> - let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) + let (metasenv', idx) = + CicMkImplicit.mk_implicit_type metasenv subst context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) | Some `Closed -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in - metasenv', Cic.Meta (idx, []) + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) | None -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) | _ -> assert false ;; - +let is_a_double_coercion t = + let last_of l = + let rec aux = function + | x::[] -> x + | x::tl -> aux tl + | [] -> assert false + in + aux l + in + let dummyres = + false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None + in + match t with + | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> + (match last_of tl with + | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + let head = last_of tl2 in + true, c1, c2, head + | _ -> dummyres) + | _ -> dummyres + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -110,7 +157,8 @@ let rec type_of_constant uri ugraph = | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise - (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) + (RefineFailure + (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) and type_of_variable uri ugraph = let module C = Cic in @@ -213,6 +261,19 @@ 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 try_coercion t subst metasenv context ugraph coercion_tgt c = + let coerced = Cic.Appl[c;t] 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 + in + Some (newt, tty, subst, metasenv, ugraph) + with + | RefineFailure _ | Uncertain _ -> None + in let module C = Cic in let module S = CicSubstitution in let module U = UriManager in @@ -323,8 +384,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t t, cast, subst, metasenv, ugraph | term -> let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in + let boh = + CoercGraph.look_for_coercion coercion_src coercion_tgt + in (match boh with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> @@ -343,13 +405,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion c -> - let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion - subst metasenv ugraph - (Cic.Appl[c;t]) coercion_tgt - in - newt, tty, subst, metasenv, ugraph) + | 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 let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -384,16 +458,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 | coercion_src -> let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in + let boh = + CoercGraph.look_for_coercion coercion_src coercion_tgt + in match boh with - | CoercGraph.SomeCoercion c -> - let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion - subst' metasenv' ugraph1 - (Cic.Appl[c;s']) coercion_tgt - in - newt, tty, subst', metasenv', ugraph1 | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl s' @@ -411,6 +479,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " 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"))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -450,9 +536,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in let tl',applty,subst''',metasenv''',ugraph3 = eat_prods true subst'' metasenv'' context - hetype tlbody_and_type ugraph2 + he' hetype tlbody_and_type ugraph2 in - avoid_double_coercion + avoid_double_coercion context subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> @@ -717,8 +803,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 @@ -737,16 +826,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in let _,_,subst,metasenv,ugraph4 = eat_prods false subst metasenv context - outtypety tlbody_and_type ugraph4 + outtype outtypety tlbody_and_type ugraph4 in let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context (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' = @@ -756,9 +846,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 @@ -782,11 +884,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') @@ -823,11 +937,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') @@ -851,19 +977,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t relocalize localization_tbl t t'; res - and avoid_double_coercion subst metasenv ugraph t ty = - match t with - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when - CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> - 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 - with - | CoercGraph.SomeCoercion c -> - Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph - | _ -> assert false) (* the composite coercion must exist *) - | _ -> t, ty, subst, metasenv, ugraph - (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) @@ -989,15 +1102,17 @@ 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 *) let (metasenv,idx) = CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv,ugraph1) = + try fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph + with _ -> assert false (* unification against a metavariable *) in t2'',subst,metasenv,ugraph1 | _,_ -> @@ -1010,8 +1125,47 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2'')))) + and avoid_double_coercion context subst metasenv ugraph t ty = + let b, c1, c2, head = is_a_double_coercion t in + 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 + with + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun c -> + let newt = + match c with + | Cic.Appl l -> Cic.Appl (l @ [head]) + | _ -> Cic.Appl [c;head] + in + (try + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + Some (newt, ty, subst, metasenv, ugraph) + with RefineFailure _ | Uncertain _ -> None)) + candidates + in + (match selected with + | Some x -> x + | None -> + prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t); + assert false) + | _ -> assert false) (* the composite coercion must exist *) + else + t, ty, subst, metasenv, ugraph + and eat_prods - allow_coercions subst metasenv context hetype tlbody_and_type ugraph + allow_coercions subst metasenv context he hetype tlbody_and_type ugraph = let rec mk_prod metasenv context' = function @@ -1054,36 +1208,43 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in metasenv,Cic.Prod (name,meta,target) in - let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in - let (subst, metasenv,ugraph1) = - try - fo_unif_subst subst context metasenv hetype hetype' ugraph - with exn -> - debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" - (CicPp.ppterm hetype) - (CicPp.ppterm hetype') - (CicMetaSubst.ppmetasenv [] metasenv) - (CicMetaSubst.ppsubst subst))); - raise exn - + let ((subst,metasenv,ugraph1),hetype') = + if CicUtil.is_meta_closed hetype then + (subst,metasenv,ugraph),hetype + else + let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in + try + fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype' + with exn -> + enrich localization_tbl he + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst he + context ^ " (that has type " ^ + CicMetaSubst.ppterm_in_context subst hetype + context ^ ") is here applied to " ^ + string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected" + (* "\nReason: " ^ Lazy.force exn*)))) exn in let rec eat_prods metasenv subst context hetype ugraph = function | [] -> [],metasenv,subst,hetype,ugraph | (hete, hety)::tl -> - (match hetype with + (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> let arg,subst,metasenv,ugraph1 = try let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv hety s ugraph + fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 with exn when allow_coercions && !insert_coercions -> (* we search a coercion from hety to s *) let coer, tgt_carr = let carr t subst context = - CicMetaSubst.apply_subst subst t + 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 @@ -1111,29 +1272,40 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion c -> - let newt, _, subst, metasenv, ugraph = - avoid_double_coercion - subst metasenv ugraph - (Cic.Appl[c;hete]) tgt_carr in - try - let newty,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - newt, subst, metasenv, ugraph - with exn -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ + | 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, _, 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, 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) + (* "\nReason: " ^ Lazy.force e*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> @@ -1150,8 +1322,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicSubstitution.subst arg t) ugraph1 tl in arg::coerced_args,metasenv',subst',t',ugraph2 - | _ -> assert false - ) + | _ -> + raise (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst he + context ^ " (that has type " ^ + CicMetaSubst.ppterm_in_context subst hetype' + context ^ ") is here applied to " ^ + string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected")))) in let coerced_args,metasenv,subst,t,ugraph2 = eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type @@ -1206,12 +1385,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; -let type_of_aux' ?localization_tbl metasenv context term ugraph = - try - type_of_aux' ?localization_tbl metasenv context term ugraph - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) - let undebrujin uri typesno tys t = snd (List.fold_right @@ -1365,6 +1538,159 @@ let typecheck metasenv uri obj ~localization_tbl = are_all_occurrences_positive metasenv ugraph uri tys paramsno in Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph +;; + +(* sara' piu' veloce che raffinare da zero? mah.... *) +let pack_coercion metasenv ctx t = + let module C = Cic in + let rec merge_coercions ctx = + let aux = (fun (u,t) -> u,merge_coercions ctx t) in + function + | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t + | C.Meta (n,subst) -> + let subst' = + List.map + (function None -> None | Some t -> Some (merge_coercions ctx t)) subst + in + C.Meta (n,subst') + | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty) + | C.Prod (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.Lambda (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.LetIn (name,so,dest) -> + let ctx' = Some (name,(C.Def (so,None)))::ctx in + C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.Appl l -> + 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 old_insert_coercions = !insert_coercions in + insert_coercions := false; + let newt, _, menv, _ = + 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; + if metasenv <> [] || menv = [] then + newt + else + (prerr_endline "PUO' SUCCEDERE!!!!!";t) + else + t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Var (uri, exp_named_subst) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Const (uri, exp_named_subst) + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutInd (uri,tyno,exp_named_subst) + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutConstruct (uri,tyno,consno,exp_named_subst) + | C.MutCase (uri,tyno,out,te,pl) -> + let pl = List.map (merge_coercions ctx) pl in + C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl) + | C.Fix (fno, fl) -> + let ctx' = + List.fold_left + (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,idx,ty,bo) -> + (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) + fl + in + C.Fix (fno, fl) + | C.CoFix (fno, fl) -> + let ctx' = + List.fold_left + (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,ty,bo) -> + (name, merge_coercions ctx ty, merge_coercions ctx' bo)) + fl + in + C.CoFix (fno, fl) + in + merge_coercions ctx t +;; + +let pack_coercion_obj obj = + let module C = Cic in + match obj with + | C.Constant (id, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] [] body) + in + let ty = pack_coercion [] [] ty in + C.Constant (id, body, ty, params, attrs) + | C.Variable (name, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] [] body) + in + 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 body = pack_coercion conjectures [] body in + let ty = pack_coercion conjectures [] ty in + C.CurrentProof (name, conjectures, body, ty, params, attrs) + | C.InductiveDefinition (indtys, params, leftno, attrs) -> + let indtys = + List.map + (fun (name, ind, arity, cl) -> + let arity = pack_coercion [] [] arity in + let cl = + List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl + in + (name, ind, arity, cl)) + indtys + in + C.InductiveDefinition (indtys, params, leftno, attrs) +;; + (* DEBUGGING ONLY let type_of_aux' metasenv context term = @@ -1393,3 +1719,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph = let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj + +let _ = DoubleTypeInference.pack_coercion := pack_coercion;;