X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b74d4029680c7349872672cd4372ec8ba6652c52;hb=185bfc8f9c9ba49308477ee6769701f3e2977115;hp=620f66f1831a4ec598178645201dd7686c47c7d7;hpb=ba3903b2c712d2a6d60c0da59b26c882b8ed6c7c;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 620f66f18..b74d40296 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -58,7 +58,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,19 +81,80 @@ 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 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 + let subst, metasenv, ugraph = + CicUnification.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 + | _ -> 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 @@ -110,7 +171,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 @@ -345,7 +407,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion c -> let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion + avoid_double_coercion context subst metasenv ugraph (Cic.Appl[c;t]) coercion_tgt in @@ -389,7 +451,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match boh with | CoercGraph.SomeCoercion c -> let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion + avoid_double_coercion context subst' metasenv' ugraph1 (Cic.Appl[c;s']) coercion_tgt in @@ -452,7 +514,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t eat_prods true subst'' metasenv'' context 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) -> @@ -851,19 +913,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 *) @@ -1059,7 +1108,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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" + debug_print + (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" (CicPp.ppterm hetype) (CicPp.ppterm hetype') (CicMetaSubst.ppmetasenv [] metasenv) @@ -1113,7 +1163,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> let newt, _, subst, metasenv, ugraph = - avoid_double_coercion + avoid_double_coercion context subst metasenv ugraph (Cic.Appl[c;hete]) tgt_carr in try @@ -1365,6 +1415,158 @@ 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 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 as t -> + 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) + | 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 [] 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.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 + in + ((i,ctx,pack_coercion conjectures 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 =