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 cdf26c5c7d2af6bf082a3a7b4e22b6b166ed45b4..2f388c0b5e83bbad8ca5359f2d0d936d7aedeb38 100644 (file)
--- 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 6316fa11cc2a36497183288188873871284b203b..22139c291da9cd18036f05c1ffc1b46a2d533489 100644 (file)
--- 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 f43c3a592fa769254bc9bd6c7c1a94bbe6786901..dea9d32c6a1cf3100c6f79ee213cc6618704fbe5 100644 (file)
--- 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 =