lefts_ad_tys properly sorted, added some metasenv here and there,

recursive args defined in case of appl

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 19db6c5a3449f43764b9ceed5beea4d4a216d15a..df6255e5f045a272f41eadbf3dc123d7bb762f5a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -644,7 +644,7 @@ let fix_lefts_in_constrs ~subst uri paramsno tyl i =
     cl 
   in
   let lefts = fst (split_prods ~subst [] paramsno arity) in
-  tys@lefts, len, cl'
+  lefts@tys, len, cl'
 ;;
 
 exception DoesOccur;;
@@ -1016,7 +1016,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
          " is a partial application of a fix")))
      else
        let rec_arg = List.nth tl rec_no in
-       if not (is_really_smaller ~subst k rec_arg) then 
+       if not (is_really_smaller ~subst ~metasenv k rec_arg) then 
          raise (NotGuarded (lazy 
            (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller")));
        List.iter (aux k) tl
@@ -1032,7 +1032,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
          List.iter (aux k) args; 
          List.iter2
            (fun p (_,_,bruijnedc) ->
-             let rl = recursive_args ~subst c_ctx 0 len bruijnedc in
+             let rl = recursive_args ~subst ~metasenv c_ctx 0 len bruijnedc in
              let p, k = get_new_safes ~subst k p rl in
              aux k p) 
            pl cl
@@ -1084,13 +1084,16 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
 
 and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
 
-and recursive_args ~subst context n nn te =
+and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
-  | C.Rel _ -> []
+  | C.Rel _ | C.Appl _ -> []
   | C.Prod (name,so,de) ->
      (not (does_not_occur ~subst context n nn so)) ::
-      (recursive_args ~subst ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
-  | _ -> raise (AssertFailure (lazy ("recursive_args")))
+      (recursive_args ~subst ~metasenv 
+        ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
+  | t -> 
+     raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst
+     ~metasenv ~context:[] t)))
 
 and get_new_safes ~subst (context, recfuns, x, safes as k) p rl =
   match R.whd ~subst context p, rl with
@@ -1108,7 +1111,7 @@ and split_prods ~subst context n te =
        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
   | _ -> raise (AssertFailure (lazy "split_prods"))
 
-and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
+and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
  match R.whd ~subst context te with
  | C.Rel m when List.mem m safes -> true
  | C.Rel _ -> false
@@ -1121,7 +1124,7 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
     (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
     (*CSC: solo perche' non abbiamo trovato controesempi            *)
     (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
-    is_really_smaller ~subst k he
+    is_really_smaller ~subst ~metasenv k he
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->
@@ -1150,16 +1153,16 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
     | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
         let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in
         if not isinductive then
-          List.for_all (is_really_smaller ~subst k) pl
+          List.for_all (is_really_smaller ~subst ~metasenv k) pl
         else
           let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in
           List.for_all2
            (fun p (_,_,debruijnedte) -> 
-             let rl' = recursive_args ~subst c_ctx 0 len debruijnedte in
+             let rl'=recursive_args ~subst ~metasenv c_ctx 0 len debruijnedte in
              let e, k = get_new_safes ~subst k p rl' in
-             is_really_smaller ~subst k e)
+             is_really_smaller ~subst ~metasenv k e)
            pl cl
-    | _ -> List.for_all (is_really_smaller ~subst k) pl)
+    | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl)
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with