fixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies...

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 63b7765a5fc54bee614df84ddf11a4b254c7ace0..55a3a6d7f927608c9546abf72dcf5b173516ff0e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -71,9 +71,12 @@ let string_of_recfuns ~subst ~metasenv ~context l =
 let fixed_args bo j n nn =
  let rec aux k acc = function
   | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn ->
-      let lefts, _ = HExtlib.split_nth j args in
-      List.map (fun ((b,x),i) -> b && x = NCic.Rel (k+(j-i))) 
-        (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts))
+      (try 
+        let lefts, _ = HExtlib.split_nth j args in
+        List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) 
+          (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts))
+      with Failure "HExtlib.split_nth" -> assert false)
+        (* 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
@@ -990,12 +993,8 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
   match t with
   | C.Rel m as t when is_dangerous m recfuns -> 
       raise (NotGuarded (lazy 
-        (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
-  | C.Rel m ->
-     (match List.nth context (m-1) with 
-     | _,C.Decl _ -> ()
-     | _,C.Def (bo,_) -> aux k (S.lift m bo))
-  | C.Meta _ -> ()
+        (NCicPp.ppterm ~subst ~metasenv ~context t ^ 
+         " is a partial application of a fix")))
   | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns ->
      let rec_no = get_recno m recfuns in
      if not (List.length tl > rec_no) then 
@@ -1013,8 +1012,14 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
   | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns ->
        let fixed_args = get_fixed_args m recfuns in
        list_iter_default2 (fun x b -> if not b then aux k x) tl false fixed_args
-  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) as r)::args) 
-    when List.exists (fun t->try aux k t;false with NotGuarded _->true) args ->
+  | C.Rel m ->
+     (match List.nth context (m-1) with 
+     | _,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) ->
+      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)
@@ -1023,13 +1028,14 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
       let fl_len = List.length fl in
       let bo = debruijn uri fl_len context bo in
       let ctx_len = List.length context in
-        (* cerco i parametri fissi solo fino a j, un po aleatorio *)
+        (* we may look for fixed params not only up to j ... *)
       let fa = fixed_args bo 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 = 
-        (* potrebbe anche aggiungere un arg di cui fa push alle safe *)
+        (* 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
       in
       let k = context, (List.length context - i,UnfFix fa) :: recfuns, x in