cicUtil : new test function "is_sober" to test the integrity of a term

[helm.git] / components / cic / cicUtil.ml

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index d26d422d526318b3efedb7786ea0e7e2bc90ca62..dd165219694c2f1bbf1f0dc361f952e709e74532 100644 (file)
--- a/components/cic/cicUtil.ml
+++ b/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,7 +535,8 @@ 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'
@@ -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