X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUtil.ml;h=dd165219694c2f1bbf1f0dc361f952e709e74532;hb=c036cf8b560ad40dbc06e94530af938e6f994aca;hp=22dcb298cdb929160f3b8f14e5ba5d3bbf36359c;hpb=579d312fed0670e7528e106d2df94d72a18ee277;p=helm.git

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 22dcb298c..dd1652196 100644
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -484,7 +484,7 @@ let alpha_equivalence =
         aux s s' && aux t t'
      | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
         aux s s' && aux t t'
-     | C.Appl l, C.Appl l' ->
+     | C.Appl l, C.Appl l' when List.length l = List.length l' ->
         (try
           List.fold_left2
            (fun b t1 t2 -> b && aux t1 t2) true l l'
@@ -535,13 +535,14 @@ let alpha_equivalence =
 	     | _               -> b
            ) true subst subst'
          with
-          Invalid_argument _ -> false)     
+          Invalid_argument _ -> false)
+     | C.Appl [t], t' | t, C.Appl [t'] -> assert 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' *)
+     | _,_ -> false (* we already know that t != t' *)
   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
    try
      List.fold_left2
@@ -552,3 +553,43 @@ let alpha_equivalence =
      Invalid_argument _ -> false
   in
    aux
+
+let is_sober t =
+   let rec sober_term g = function
+      | C.Rel _ 
+      | C.Sort _  
+      | C.Implicit _                    -> g      
+      | C.Const (_, xnss) 
+      | C.Var (_, xnss) 
+      | C.MutConstruct (_, _, _, xnss)
+      | C.MutInd (_, _, xnss)           -> sober_xnss g xnss
+      | C.Meta (_, xss)                 -> sober_xss g xss
+      | C.LetIn (_, v, t)
+      | C.Lambda (_, v, t)
+      | C.Prod (_, v, t)
+      | C.Cast (t, v)                   -> sober_term (sober_term g t) v
+      | C.Appl []                       
+      | C.Appl [_]                      -> fun b -> false
+      | C.Appl ts                       -> sober_terms g ts
+      | C.MutCase (_, _, t, v, ts)      -> 
+         sober_terms (sober_term (sober_term g t) v) ts
+      | C.Fix (_, ifs)                  -> sober_ifs g ifs
+      | C.CoFix (_, cifs)               -> sober_cifs g cifs
+   and sober_terms g = List.fold_left sober_term g
+   and sober_xnss g =
+      let map g (_, t) = sober_term g t in
+      List.fold_left map g
+   and sober_xss g =
+      let map g = function 
+         | None   -> g
+	 | Some t -> sober_term g t
+      in
+      List.fold_left map g
+   and sober_ifs g =
+      let map g (_, _, t, v) = sober_term (sober_term g t) v in
+      List.fold_left map g
+   and sober_cifs g =
+      let map g (_, t, v) = sober_term (sober_term g t) v in
+      List.fold_left map g
+   in 
+   sober_term (fun b -> b) t true