From 579d312fed0670e7528e106d2df94d72a18ee277 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 4 Apr 2007 15:01:50 +0000 Subject: [PATCH] alpha equivalence fixed: in the case "meta against meta" we did not recur on theexplicit substitutions. The case "Type against Type" and "Implicit against Implicit" need to be checked. Are we really sure that structural equality is enough? (when we compare universes and implict annotations) --- .../acic_procedural/acic2Procedural.ml | 16 ++++++++++------ helm/software/components/cic/cicUtil.ml | 17 ++++++++++++++++- 2 files changed, 26 insertions(+), 7 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index fb99090e9..bff721a3e 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -26,6 +26,7 @@ module C = Cic module I = CicInspect module D = Deannotate +module S = CicSubstitution module TC = CicTypeChecker module Un = CicUniv module UM = UriManager @@ -183,17 +184,20 @@ let convert st ?name v = match get_inner_types st v with | None -> [] | Some (sty, ety) -> + let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in let csty, cety = cic sty, cic ety in if Ut.alpha_equivalence csty cety then [] else - let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in match name with - | None -> [T.Change (sty, ety, None, e, "")] - | Some id -> + | None -> [T.Change (sty, ety, None, e, "")] + | Some (id, i) -> begin match get_entry st id with | C.Def _ -> [T.ClearBody (id, "")] | C.Decl w -> - if Ut.alpha_equivalence csty w then [] - else [T.Change (sty, ety, Some (id, id), e, "")] + let w = S.lift i w in + if Ut.alpha_equivalence csty w then [] + else + [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w); + T.Change (sty, ety, Some (id, id), e, "")] end let get_intro = function @@ -206,7 +210,7 @@ let mk_intros st script = T.Intros (Some count, List.rev st.intros, "") :: script let mk_arg st = function - | C.ARel (_, _, _, name) as what -> convert st ~name what + | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what | _ -> [] let mk_fwd_rewrite st dtext name tl direction = diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index d79c233df..22dcb298c 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -526,7 +526,22 @@ let alpha_equivalence = ) true fl fl' with Invalid_argument _ -> false) - | _,_ -> false (* we already know that t != t' *) + | C.Meta (i, subst), C.Meta (i', subst') -> + i = i' && + (try + List.fold_left2 + (fun b xt xt' -> match xt,xt' with + | Some t, Some t' -> b && aux t t' + | _ -> b + ) true subst subst' + with + Invalid_argument _ -> false) +(* FG: are we _really_ sure of these? + | C.Sort (C.Type u), C.Sort (C.Type u') -> u = u' + | C.Implicit a, C.Implicit a' -> a = a' + we insert an unused variable below to genarate a warning at compile time +*) + | _,_ -> let fix_alpha_equivalence_please = 0 in false (* we already know that t != t' *) and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = try List.fold_left2 -- 2.39.2