X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=90643164d576bf14b5f309fc4011104bfa1d8b1b;hb=93cc0505102768f7d4337907bafa31d1528a7289;hp=844260480134d42fd61acc3efbae44b755ccd2ef;hpb=27b3610b7add7ee75eb25f8f01e0f1426c278f52;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 844260480..90643164d 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 = @@ -480,7 +504,7 @@ 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 - he hetype tlbody_and_type ugraph2 + he' hetype tlbody_and_type ugraph2 in avoid_double_coercion context subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty @@ -1099,7 +1123,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); assert false | Uncertain _ -> - prerr_endline ("#### Coercion not packed (Uncercatin case): " ^ + prerr_endline ("#### Coercion not packed (Uncerctain case): " ^ CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); assert false) | _ -> assert false) (* the composite coercion must exist *) @@ -1150,39 +1174,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 -> - 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 + 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 @@ -1249,8 +1277,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 @@ -1305,12 +1340,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 @@ -1467,7 +1496,7 @@ let typecheck metasenv uri obj ~localization_tbl = ;; (* sara' piu' veloce che raffinare da zero? mah.... *) -let pack_coercion metasenv t = +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 @@ -1489,32 +1518,29 @@ let pack_coercion metasenv t = | 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 as t -> + | 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!!!!"; *) - let newt = - 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 - in - (match newt with - | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l) - | _ -> assert false) + 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) @@ -1531,7 +1557,7 @@ let pack_coercion metasenv t = 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 = + let ctx' = List.fold_left (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) ctx fl @@ -1539,12 +1565,12 @@ let pack_coercion metasenv t = let fl = List.map (fun (name,idx,ty,bo) -> - (name,idx,merge_coercions ctx ty,merge_coercions ctx bo)) + (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) fl in C.Fix (fno, fl) | C.CoFix (fno, fl) -> - let ctx = + let ctx' = List.fold_left (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) ctx fl @@ -1552,12 +1578,12 @@ let pack_coercion metasenv t = let fl = List.map (fun (name,ty,bo) -> - (name, merge_coercions ctx ty, merge_coercions ctx bo)) + (name, merge_coercions ctx ty, merge_coercions ctx' bo)) fl in C.CoFix (fno, fl) in - merge_coercions [] t + merge_coercions ctx t ;; let pack_coercion_obj obj = @@ -1567,48 +1593,52 @@ let pack_coercion_obj obj = let body = match body with | None -> None - | Some body -> Some (pack_coercion [] body) + | Some body -> Some (pack_coercion [] [] body) in - let ty = pack_coercion [] ty 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) + | Some body -> Some (pack_coercion [] [] body) in - let ty = pack_coercion [] ty 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.map - (function - | Some (name, C.Decl t) -> - Some (name, C.Decl (pack_coercion conjectures t)) - | Some (name, C.Def (t,None)) -> - Some (name, C.Def (pack_coercion conjectures t, None)) - | Some (name, C.Def (t,Some ty)) -> - Some (name, C.Def (pack_coercion conjectures t, - Some (pack_coercion conjectures ty))) - | None -> None) - 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 ty))) - conjectures + ((i,ctx,pack_coercion conjectures ctx ty)) + ) conjectures in - let body = pack_coercion conjectures body in - let ty = pack_coercion conjectures ty 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 arity = pack_coercion [] [] arity in let cl = - List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl + List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl in (name, ind, arity, cl)) indtys @@ -1644,3 +1674,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;;