X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc;hb=5d8d504eb46d181d7a915b2be154022ea83da4df;hp=b9c5b0c6a642e50210edf3a579e1824da510d8c2;hpb=43ef446ad93ea278245ef529eda398a55516188f;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index b9c5b0c6a..1f92a5fa8 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -118,54 +118,6 @@ let is_a_double_coercion t = | _ -> dummyres) | _ -> dummyres -let avoid_double_coercion context subst metasenv ugraph t ty = - let arity_of con = - try - let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in - let rec count_pi = function - | Cic.Prod (_,_,t) -> 1 + count_pi t - | _ -> 0 - in - count_pi ty - with Invalid_argument _ -> assert false (* all coercions have an uri *) - in - let rec mk_implicits tail = function - | 0 -> [tail] - | n -> Cic.Implicit None :: mk_implicits tail (n-1) - in - 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 c -> - let arity = arity_of c in - let args = mk_implicits head (arity - 1) in - let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in - let newt = Cic.Appl (c_bo::args) in - (try - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in - debug_print - (lazy - ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args)))); - Cic.Appl (c::args), ty, subst, metasenv, ugraph - with - RefineFailure _ -> - prerr_endline ("#### Coercion not packed (Refine_failure): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); - assert false - | Uncertain _ -> - prerr_endline ("#### Coercion not packed (Uncercatin case): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); - assert false) - | _ -> assert false) (* the composite coercion must exist *) - else - t, ty, subst, metasenv, ugraph - let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -395,8 +347,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 _ -> @@ -416,10 +369,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion c -> + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context (Cic.Appl[c;t]) + ugraph in let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context - subst metasenv ugraph - (Cic.Appl[c;t]) coercion_tgt + avoid_double_coercion context subst metasenv ugraph + newt coercion_tgt in newt, tty, subst, metasenv, ugraph) in @@ -456,14 +411,17 @@ 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,_,subst',metasenv',ugraph1 = + type_of_aux subst' metasenv' context (Cic.Appl[c;s']) + ugraph1 in let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion context - subst' metasenv' ugraph1 - (Cic.Appl[c;s']) coercion_tgt + avoid_double_coercion context subst' metasenv' + ugraph1 newt coercion_tgt in newt, tty, subst', metasenv', ugraph1 | CoercGraph.NoCoercion @@ -522,7 +480,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 @@ -1111,6 +1069,43 @@ 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 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)); + newt, ty, subst, metasenv, ugraph + with + RefineFailure _ -> + prerr_endline ("#### Coercion not packed (Refine_failure): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); + assert false + | Uncertain _ -> + prerr_endline ("#### Coercion not packed (Uncerctain case): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); + assert false) + | _ -> assert false) (* the composite coercion must exist *) + else + t, ty, subst, metasenv, ugraph + and eat_prods allow_coercions subst metasenv context he hetype tlbody_and_type ugraph = @@ -1164,7 +1159,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ~f:(fun _ -> (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst he - context ^ "(that has type " ^ + context ^ " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype context ^ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ @@ -1187,7 +1182,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* 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 @@ -1216,20 +1212,20 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> + try + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context + (Cic.Appl[c;hete]) ugraph in let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context - 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 + 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 newt, subst, metasenv, ugraph - with _ -> - enrich localization_tbl hete + with _ -> + enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete @@ -1472,7 +1468,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 @@ -1494,32 +1490,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) @@ -1536,7 +1529,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 @@ -1544,12 +1537,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 @@ -1557,12 +1550,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 = @@ -1572,48 +1565,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 @@ -1649,3 +1646,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;;