Implementation of guarded_by_destructor is now complete w.r.t. the old kernel:

 a) bug fixed in eat_lambdas_etc: we cannot apply the term to the residual
    arguments since these are not left arguments
 b) when the recursive argument of the nested "let rec" is safe, the formal
    argument can also be considered safe.

TODO:
This implementation of condition b) could be improved by re-writing eat_lambdas
in such a way that it uses a shift_k function to add the context item to the
"context".

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 6f516b8db6eb010aaac1e3a6d449de901843f333..e05f145d32f0a8bd8ce679d574f51aa7eaa5e5c8 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -969,21 +969,17 @@ and eat_lambdas ~subst ~metasenv context n te =
       raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n 
         (NCicPp.ppterm ~subst ~metasenv ~context te))))
 
-and eat_or_subst_lambdas 
- ~subst ~metasenv app_all_args n te to_be_subst args (context, recfuns, x as k) 
+and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
+     (context, recfuns, x as k) 
 =
   match n, R.whd ~subst context te, to_be_subst, args with
-  | (0, _,_,_) when args = [] || not app_all_args -> te, k
-  | (0, _,_,_::_) -> C.Appl (te::args), k
   | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
-      eat_or_subst_lambdas ~subst ~metasenv app_all_args
-       (n - 1) (S.subst arg ta) to_be_subst args k
+      eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
+       to_be_subst args k
   | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
-      eat_or_subst_lambdas ~subst ~metasenv app_all_args
-       (n - 1) ta to_be_subst args (shift_k (name,(C.Decl so)) k)
-  | (n, te, _, _) when args = [] || not app_all_args -> te, k
-  | (n, te, _, _::_) -> C.Appl (te::args), k
-  | (_,_,_,[]) -> assert false (* caml thinks is missing *)
+      eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
+       (shift_k (name,(C.Decl so)) k)
+  | (_, te, _, _) -> te, k
 
 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = 
  let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
@@ -1023,7 +1019,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
      | _,C.Decl _ -> ()
      | _,C.Def (bo,_) -> aux k (S.lift m bo))
   | C.Meta _ -> ()
-  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,_))) as r)::args) ->
+  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) ->
       if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args
       then
       let fl,_,_ = E.get_checked_fixes r in
@@ -1042,11 +1038,33 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
       let extra_recfuns = 
         HExtlib.list_mapi (fun _ i -> ctx_len - i, UnfFix fa) ctx_tys
       in
-      let k = context, extra_recfuns@recfuns, x in
+      let new_k = context, extra_recfuns@recfuns, x in
       let bos_and_ks = 
-        HExtlib.list_mapi (fun bo fno ->
-          (* potrebbe anche aggiungere un arg di cui fa push alle safe *)
-          eat_or_subst_lambdas ~subst ~metasenv (fno=i) j bo fa args k) bos
+        HExtlib.list_mapi
+         (fun bo fno ->
+          let bo_and_k =
+            eat_or_subst_lambdas ~subst ~metasenv j bo fa args new_k
+          in
+           if
+            fno = i &&
+            List.length args > recno &&
+            (*case where the recursive argument is already really_smaller *)
+            is_really_smaller r_uri r_len ~subst ~metasenv k
+             (List.nth args recno)
+           then
+            let bo,(context, _, _ as new_k) = bo_and_k in
+            let bo, context' =
+             eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in
+            let new_context_part,_ =
+             HExtlib.split_nth (List.length context' - List.length context)
+              context' in
+            let k = List.fold_right shift_k new_context_part new_k in
+            let context, recfuns, x = k in
+            let k = context, (1,Safe)::recfuns, x in
+              bo,k
+           else
+            bo_and_k
+         ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->