From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 4 Apr 2007 15:01:50 +0000 (+0000)
Subject: alpha equivalence fixed: in the case "meta against meta" we did not recur on theexpli... 
X-Git-Tag: 0.4.95@7852~549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8791fd4e018c691d1b22a4fe748bc57f79f1b89;p=helm.git

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)
---

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index fb99090e9..bff721a3e 100644
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/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/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index d79c233df..22dcb298c 100644
--- a/components/cic/cicUtil.ml
+++ b/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