From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Apr 2008 20:50:58 +0000 (+0000)
Subject: fixed_args fixed to accept passing a partially applied fix to a fix that
X-Git-Tag: make_still_working~5272
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63bf7f1e50ca65c2a224e34aa7d232bff10ea934;p=helm.git

fixed_args fixed to accept passing a partially applied fix to a fix that
passes itself partially applied to anothere fix
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 99829c4a7..9b0de30f2 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -71,12 +71,16 @@ let string_of_recfuns ~subst ~metasenv ~context l =
 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 
-        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 *)
+     let rec combine l1 l2 =
+      match l1,l2 with
+         [],[] -> []
+       | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2
+       | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *)
+       | [],_::_ -> assert false
+     in
+     let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in
+      List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) 
+       (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts))
   | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t    
  in
   List.fold_left (aux 0) 
@@ -606,7 +610,7 @@ exception NotGuarded of string Lazy.t;;
 
 let rec typeof ~subst ~metasenv context term =
   let rec typeof_aux context = 
-    fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *)
+    fun t -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*)
     match t with
     | C.Rel n ->
        (try