added check on all bodies, only the one we actually encountered is applied to all...

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 55a3a6d7f927608c9546abf72dcf5b173516ff0e..99829c4a7c67e62a6a5dc84e9d5d3e354879d0d9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -68,7 +68,7 @@ let string_of_recfuns ~subst ~metasenv ~context l =
      | _ -> assert false) dang)
 ;;
 
-let fixed_args bo j n nn =
+let fixed_args bos j n nn =
  let rec aux k acc = function
   | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn ->
       (try 
@@ -79,7 +79,8 @@ let fixed_args bo j n nn =
         (* se sono meno di j, fino a j deduco, dopo false *)
   | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t    
  in
-   aux 0 (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bo
+  List.fold_left (aux 0) 
+   (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
 ;;
 
 let rec list_iter_default2 f l1 def l2 = 
@@ -965,19 +966,20 @@ and eat_lambdas ~subst ~metasenv context n te =
         (NCicPp.ppterm ~subst ~metasenv ~context te))))
 
 and eat_or_subst_lambdas 
- ~subst ~metasenv n te to_be_subst args (context, recfuns, x as k) 
+ ~subst ~metasenv app_all_args n te to_be_subst args (context, recfuns, x as k) 
 =
   match n, R.whd ~subst context te, to_be_subst, args with
-  | (0, _,_,[]) -> te, k
+  | (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 
+      eat_or_subst_lambdas ~subst ~metasenv app_all_args
        (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 
+      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, _, []) -> te, k
+  | (n, te, _, _) when args = [] || not app_all_args -> te, k
   | (n, te, _, _::_) -> C.Appl (te::args), k
+  | (_,_,_,[]) -> assert false (* caml thinks is missing *)
 
 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
@@ -1017,29 +1019,32 @@ 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,j))) as r)::args) ->
+  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,_))) 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
       let ctx_tys, bos = 
         List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
       in
-      let bo = List.nth bos i in
       let fl_len = List.length fl in
-      let bo = debruijn uri fl_len context bo in
+      let bos = List.map (debruijn uri fl_len context) bos in
+      let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in
       let ctx_len = List.length context in
         (* we may look for fixed params not only up to j ... *)
-      let fa = fixed_args bo j ctx_len (ctx_len + fl_len) in
+      let fa = fixed_args bos j ctx_len (ctx_len + fl_len) in
       list_iter_default2 (fun x b -> if not b then aux k x) args false fa; 
       let context = context@ctx_tys in
-      let k = context, recfuns, x in
-      let bo, k = 
-        (* we should enrich k with infos regarding args that are safe but not
-         * fixed *)
-        eat_or_subst_lambdas ~subst ~metasenv j bo fa args k
+      let ctx_len = List.length context in
+      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 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
       in
-      let k = context, (List.length context - i,UnfFix fa) :: recfuns, x in
-       aux k bo
+       List.iter (fun (bo,k) -> aux k bo) bos_and_ks
   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->