module Reduction (debut)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 18 insertions, 2 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 625ceed870..77a26062db 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -76,7 +76,21 @@ let list_chop n l =
     | (_, []) -> failwith "chop_list"
   in 
   chop_aux [] (n,l)
- 
+
+let list_tabulate f len = 
+  let rec tabrec n =
+    if n = len then [] else (f n)::(tabrec (n+1))
+  in 
+  tabrec 0
+
+let list_assign l n e = 
+  let rec assrec stk = function
+    | ((h::t), 0) -> List.rev_append stk (e::t)
+    | ((h::t), n) -> assrec (h::stk) (t, n-1)
+    | ([], _) -> failwith "list_assign"
+  in 
+  assrec [] (l,n)
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index 92aabea5d4..c539bdf671 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -24,7 +24,9 @@ val parse_section_path : string -> string list * string * string
 
 val intersect : 'a list -> 'a list -> 'a list
 val subtract : 'a list -> 'a list -> 'a list
-val list_chop  : int -> 'a list -> 'a list * 'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_assign : 'a list -> int -> 'a -> 'a list
 
 (* Arrays *)