From 82649c076ae38353aec5333987c80476f27e3775 Mon Sep 17 00:00:00 2001 From: soubiran Date: Fri, 23 Oct 2009 16:19:47 +0000 Subject: First debug... the renaming of librairies was not working and auto/dn were not taking in account equivalent names of inductive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12408 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.ml | 9 +++++---- kernel/modops.ml | 31 +++++++++++++++++-------------- library/declare.ml | 2 +- library/libnames.ml | 9 +++++++++ library/libnames.mli | 1 + pretyping/pattern.ml | 9 ++++----- tactics/dn.ml | 14 +++++++++----- 7 files changed, 46 insertions(+), 29 deletions(-) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a9d4a246d..5f81ddb4d 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -596,6 +596,8 @@ let subst_dom_codom_delta_resolver subst resolver = let update_delta_resolver resolver1 resolver2 = let apply_res key hint res = try + if Deltamap.mem key resolver2 then + res else match hint with Prefix_equiv mp -> let new_hint = @@ -621,7 +623,7 @@ let add_delta_resolver resolver1 resolver2 = resolver2 let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,resolve) = + let apply_subst (sub : substitution) (mp,resolve) = let mp',resolve' = match subst_mp0 sub mp with None -> mp, None @@ -631,13 +633,12 @@ let join (subst1 : substitution) (subst2 : substitution) = match resolve' with Some res -> add_delta_resolver - (subst_dom_codom_delta_resolver sub resolve) - res + (subst_dom_codom_delta_resolver sub resolve) res | None -> subst_codom_delta_resolver sub resolve in mp',resolve'' in - let subst = Umap.mapi (apply_subst subst2) subst1 in + let subst = Umap.map (apply_subst subst2) subst1 in (Umap.fold Umap.add subst2 subst) diff --git a/kernel/modops.ml b/kernel/modops.ml index 8193c02e5..7ee48c352 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -126,8 +126,8 @@ and subst_modtype sub do_delta mtb= let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in let typ_alg' = Option.smartmap - (subst_struct_expr sub (fun x -> x)) mtb.typ_expr_alg in - let mtb_delta = do_delta mtb.typ_delta in + (subst_struct_expr sub (fun x y-> x)) mtb.typ_expr_alg in + let mtb_delta = do_delta mtb.typ_delta sub in if typ_expr'==mtb.typ_expr && typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then mtb @@ -156,7 +156,7 @@ and subst_module sub do_delta mb = let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then add_mp mb.mod_mp mp empty_delta_resolver sub else sub in - let id_delta = (fun x -> x) in + let id_delta = (fun x y-> x) in let mtb',me' = let mtb = subst_struct_expr sub do_delta mb.mod_type in match mb.mod_expr with @@ -168,7 +168,7 @@ and subst_module sub do_delta mb = in let typ_alg' = Option.smartmap (subst_struct_expr sub id_delta) mb.mod_type_alg in - let mb_delta = do_delta mb.mod_delta in + let mb_delta = do_delta mb.mod_delta sub in if mtb'==mb.mod_type && mb.mod_expr == me' && mb_delta == mb.mod_delta && mp == mb.mod_mp then mb else @@ -196,11 +196,11 @@ and subst_struct_expr sub do_delta = function let subst_signature subst = subst_structure subst - (fun resolver -> subst_codom_delta_resolver subst resolver) + (fun resolver subst-> subst_codom_delta_resolver subst resolver) let subst_struct_expr subst = subst_struct_expr subst - (fun resolver -> subst_codom_delta_resolver subst resolver) + (fun resolver subst-> subst_codom_delta_resolver subst resolver) (* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) @@ -272,7 +272,6 @@ let strengthen_const env mp_from l cb resolver = let rec strengthen_mod env mp_from mp_to mb = - assert(mp_from = mb.mod_mp); if mp_in_delta mb.mod_mp mb.mod_delta then mb else @@ -385,7 +384,7 @@ let rec strengthen_and_subst_mod let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in if mb_is_an_alias then subst_module subst - (fun resolver -> subst_dom_delta_resolver subst resolver) mb + (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb else let resolver,new_sig = strengthen_and_subst_struct str subst env @@ -397,8 +396,10 @@ let rec strengthen_and_subst_mod mod_type = SEBstruct(new_sig); mod_delta = add_mp_delta_resolver mp_to mp_from resolver} | SEBfunctor(arg_id,arg_b,body) -> + let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in subst_module subst - (fun resolver -> subst_dom_delta_resolver subst resolver) mb + (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb + | _ -> anomaly "Modops:the evaluation of the structure failed " and strengthen_and_subst_struct @@ -439,7 +440,7 @@ and strengthen_and_subst_struct let mp_to' = MPdot(mp_to,l) in let mb_out = if alias then subst_module subst - (fun resolver -> subst_dom_delta_resolver subst resolver) mb + (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb else strengthen_and_subst_mod mb subst env mp_from' mp_to' env resolver @@ -449,14 +450,16 @@ and strengthen_and_subst_struct let resolve_out,rest' = strengthen_and_subst_struct rest subst env' mp_alias mp_from mp_to alias incl resolver in - add_delta_resolver resolve_out mb_out.mod_delta, + if is_functor mb_out.mod_type then (add_mp_delta_resolver + mp_to' mp_to' resolve_out),item':: rest' else + add_delta_resolver resolve_out mb_out.mod_delta, item':: rest' | (l,SFBmodtype mty) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in let mty = subst_modtype subst' - (fun resolver -> subst_dom_codom_delta_resolver subst' resolver) mty in + (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in let env' = add_modtype mp_from' mty env in let resolve_out,rest' = strengthen_and_subst_struct rest subst env' mp_alias mp_from mp_to alias incl resolver in @@ -491,7 +494,7 @@ let strengthen_and_subst_mb mb mp env include_b = | SEBfunctor(arg_id,argb,body) -> let subst = map_mp mb.mod_mp mp empty_delta_resolver in subst_module subst - (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mb + (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb | _ -> anomaly "Modops:the evaluation of the structure failed " @@ -500,4 +503,4 @@ let subst_modtype_and_resolver mtb mp env = let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in let full_subst = (map_mp mtb.typ_mp mp new_delta) in subst_modtype full_subst - (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mtb + (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb diff --git a/library/declare.ml b/library/declare.ml index 1084aa07d..dd1b12a24 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -163,7 +163,7 @@ let hcons_constant_declaration = function let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in - let c = constant_of_kn kn in + let c = Global.constant_of_delta (constant_of_kn kn) in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); diff --git a/library/libnames.ml b/library/libnames.ml index fad0336fc..9a7135eae 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -57,6 +57,15 @@ let subst_global subst ref = match ref with let c',t = subst_constructor subst c in if c'==c then ref,t else ConstructRef c', t +let canonical_gr = function + | ConstRef con -> + ConstRef(constant_of_kn(canonical_con con)) + | IndRef (kn,i) -> + IndRef(mind_of_kn(canonical_mind kn),i) + | ConstructRef ((kn,i),j )-> + ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | VarRef id -> VarRef id + let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp | Ind ind_sp -> IndRef ind_sp diff --git a/library/libnames.mli b/library/libnames.mli index fd2ca37ae..9ee7d0ab5 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -29,6 +29,7 @@ val isIndRef : global_reference -> bool val isConstructRef : global_reference -> bool val eq_gr : global_reference -> global_reference -> bool +val canonical_gr : global_reference -> global_reference val destVarRef : global_reference -> variable val destConstRef : global_reference -> constant diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index ec4a1260c..9acdd1585 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -102,8 +102,8 @@ let rec pattern_of_constr t = | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a) | Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp))) - | Ind sp -> PRef (IndRef sp) - | Construct sp -> PRef (ConstructRef sp) + | Ind sp -> PRef (canonical_gr (IndRef sp)) + | Construct sp -> PRef (canonical_gr (ConstructRef sp)) | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt) | Case (ci,p,a,br) -> let cip = ci.ci_pp_info in @@ -212,9 +212,8 @@ let rec pat_of_raw metas vars = function with Not_found -> PVar id) | RPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) - | RRef (_,ConstRef con) -> - PRef (ConstRef (constant_of_kn(canonical_con con))) - | RRef (_,r) -> PRef r + | RRef (_,gr) -> + PRef (canonical_gr gr) (* Hack pour ne pas réécrire une interprétation complète des patterns*) | RApp (_, RPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) diff --git a/tactics/dn.ml b/tactics/dn.ml index 8076e252c..a0889ab8f 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -15,15 +15,19 @@ struct match x,y with None,None -> 0 | Some (l,n),Some (l',n') -> - if (Y.compare l l') = 0 && n = n' then 0 - else Pervasives.compare x y - | a,b -> Pervasives.compare a b + let m = Y.compare l l' in + if m = 0 then + n-n' + else m + | Some(l,n),None -> 1 + | None, Some(l,n) -> -1 end module X_tries = struct type t = X.t * Z.t let compare (x1,x2) (y1,y2) = - if (X.compare x1 y1) = 0 && (Z.compare x2 y2)=0 then 0 - else Pervasives.compare (x1,x2) (y1,y2) + let m = (X.compare x1 y1) in + if m = 0 then (Z.compare x2 y2) else + m end module T = Tries.Make(X_tries)(Y_tries) -- cgit v1.2.3