From 7f99392e3a8393b04c0cf512c14bcf792afc4086 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Apr 2008 23:12:21 +0000
Subject: [PATCH] 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".
---
 .../components/ng_kernel/nCicTypeChecker.ml   | 50 +++++++++++++------
 1 file changed, 34 insertions(+), 16 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 6f516b8db..e05f145d3 100644
--- 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 ->
-- 
2.39.2