From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 17:41:33 +0000 (+0000)
Subject: list_iter2_default_value moved to HExtlib. 1 euro to the first one that will
X-Git-Tag: make_still_working~5204
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6ba6011b7c8cadb8fe328812e0134e27909fb308;p=helm.git

list_iter2_default_value moved to HExtlib. 1 euro to the first one that will
re-use it (not artificially)
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index cdf26c5c7..2f388c0b5 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -148,6 +148,13 @@ let list_mapi f l =
      aux 0 l
 ;;
 
+let rec list_iter_default2 f l1 def l2 = 
+  match l1,l2 with
+    | [], _ -> ()
+    | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb 
+    | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
+;;
+
 let sharing_map f l =
   let unchanged = ref true in
   let rec aux b = function
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 6316fa11c..22139c291 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -92,6 +92,11 @@ val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
 val list_last: 'a list -> 'a
 val list_mapi: ('a -> int -> 'b) -> 'a list -> 'b list
 val sharing_map: ('a -> 'a) -> 'a list -> 'a list
+(* Iters in parallel on two lists until the first list is empty.
+   The second one can be shorter and is padded with a default value.
+   This function cannot fail. *)
+val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit
+
 
   (** split_nth n l
    * @returns two list, the first contains at least n elements, the second the
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f43c3a592..dea9d32c6 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -52,6 +52,7 @@ let get_fixed_args i l =
 
 let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;;
 
+(* for debugging only
 let string_of_recfuns ~subst ~metasenv ~context l = 
   let pp = PP.ppterm ~subst ~metasenv ~context in
   let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in
@@ -67,6 +68,7 @@ let string_of_recfuns ~subst ~metasenv ~context l =
      (function (i,Evil rno)->pp(C.Rel i)^"/"^string_of_int rno
      | _ -> assert false) dang)
 ;;
+*)
 
 let fixed_args bos j n nn =
  let rec aux k acc = function
@@ -87,13 +89,6 @@ let fixed_args bos j n nn =
    (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
 ;;
 
-let rec list_iter_default2 f l1 def l2 = 
-  match l1,l2 with
-    | [], _ -> ()
-    | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb 
-    | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
-;;
-
 let rec split_prods ~subst context n te =
   match (n, R.whd ~subst context te) with
    | (0, _) -> context,te
@@ -754,7 +749,8 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
        List.iter (aux k) tl
   | 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
+       HExtlib.list_iter_default2
+        (fun x b -> if not b then aux k x) tl false fixed_args
   | C.Rel m ->
      (match List.nth context (m-1) with 
      | _,C.Decl _ -> ()
@@ -773,7 +769,8 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
       let ctx_len = List.length context in
         (* we may look for fixed params not only up to j ... *)
       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; 
+      HExtlib.list_iter_default2
+       (fun x b -> if not b then aux k x) args false fa; 
       let context = context@ctx_tys in
       let ctx_len = List.length context in
       let extra_recfuns =