Modules dans COQ\!\!\!\!

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

4 files changed, 100 insertions, 0 deletions

diff --git a/lib/rtree.ml b/lib/rtree.ml
index 9361a2858..593f73479 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -61,6 +61,26 @@ let rec subst_rtree_rec depth sub = function
 
 let subst_rtree sub t = subst_rtree_rec 0 sub t
 
+let rec map f t = match t with
+    Param i -> Param i
+  | Node (a,sons) -> Node (f a, Array.map (map f) sons)
+  | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
+
+let rec smartmap f t = match t with
+    Param i -> t
+  | Node (a,sons) -> 
+      let a'=f a and sons' = Util.array_smartmap (map f) sons in
+	if a'==a && sons'==sons then
+	  t
+	else
+	  Node (a',sons')
+  | Rec(j,defs) -> 
+      let defs' = Util.array_smartmap (map f) defs in
+	if defs'==defs then
+	  t
+	else
+	  Rec(j,defs')
+
 (* To avoid looping, we must check that every body introduces a node 
    or a parameter *)
 let rec expand_rtree = function
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 5a34c819e..cb8fe0303 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -23,6 +23,11 @@ val mk_rec   : 'a t array -> 'a t array
    to avoid captures when a tree appears under mk_rec *) 
 val lift : int -> 'a t -> 'a t
 
+val map : ('a -> 'b) -> 'a t -> 'b t
+
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+
 (* Destructors (recursive calls are expanded) *)
 val dest_param : 'a t -> int
 val dest_node  : 'a t -> 'a * 'a t array
diff --git a/lib/util.ml b/lib/util.ml
index 3354bba53..98defb6fd 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -20,6 +20,8 @@ exception UserError of string * std_ppcmds (* User errors *)
 let error string = raise (UserError(string, str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
+let todo s = prerr_string ("TODO: "^s^"\n")
+
 (* raising located exceptions *)
 type loc = int * int
 type 'a located = loc * 'a
@@ -123,6 +125,13 @@ let list_assign l n e =
   in 
   assrec [] (l,n)
 
+let rec list_smartmap f l = match l with
+    [] -> l
+  | h::tl -> 
+      let h' = f h and tl' = list_smartmap f tl in
+	if h'==h && tl'==tl then l
+	else h'::tl'
+
 let list_map_left f = (* ensures the order in case of side-effects *)
   let rec map_rec = function
     | [] -> [] 
@@ -302,6 +311,23 @@ let list_share_tails l1 l2 =
 
 let list_join_map f l = List.flatten (List.map f l)
 
+let rec list_fold_map f e = function 
+  |  []  -> (e,[])
+  |  h::t -> 
+       let e',h' = f e h in
+       let e'',t' = list_fold_map f e' t in
+	 e'',h'::t'
+
+(* (* tail-recursive version of the above function *)
+let list_fold_map f e l = 
+  let g (e,b') h = 
+    let (e',h') = f e h in
+      (e',h'::b') 
+  in
+  let (e',lrev) = List.fold_left g (e,[]) l in
+    (e',List.rev lrev)
+*)
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -410,6 +436,35 @@ let array_chop n v =
   if n > vlen then failwith "array_chop";
   (Array.sub v 0 n, Array.sub v n (vlen-n))
 
+exception Local of int
+
+(* If none of the elements is changed by f we return ar itself.
+   The for loop looks for the first such an element.
+   If found it is temporarily stored in a ref and the new array is produced, 
+   but f is not re-applied to elements that are already checked *)
+let array_smartmap f ar = 
+  let ar_size = Array.length ar in
+  let aux = ref None in
+  try
+    for i = 0 to ar_size-1 do
+      let a = ar.(i) in
+      let a' = f a in
+	if a != a' then (* pointer (in)equality *) begin
+	  aux := Some a';
+	  raise (Local i)
+	end
+    done;
+    ar
+  with
+      Local i -> 
+	let copy j = 
+	  if j<i then ar.(j) 
+	  else if j=i then 
+	    match !aux with Some a' -> a' | None -> failwith "Error"
+	  else f (ar.(j))
+	in
+	  Array.init ar_size copy
+
 let array_map2 f v1 v2 =
   if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
   if Array.length v1 == 0 then 
@@ -508,6 +563,10 @@ let option_compare f a b = match (a,b) with
   | Some a', Some b' -> f a' b'
   | _ -> failwith "option_compare"
 
+let option_smartmap f a = match a with
+  | None -> a
+  | Some x -> let x' = f x in if x'==x then a else Some x'
+
 let map_succeed f = 
   let rec map_f = function 
     | [] -> []
diff --git a/lib/util.mli b/lib/util.mli
index e9cd97a7c..80b841b2b 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -26,6 +26,12 @@ exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
 
+(* [todo] is for running of an incomplete code its implementation is
+   "do nothing" (or print a message), but this function should not be
+   used in a released code *)
+
+val todo : string -> unit
+
 type loc = int * int
 type 'a located = loc * 'a
 
@@ -67,6 +73,10 @@ val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+
+(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+   [ f ai == ai], then [list_smartmap f l==l] *)
+val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
 val list_map_left : ('a -> 'b) -> 'a list -> 'b list
 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_map2_i : 
@@ -98,6 +108,10 @@ val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
+(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+   where [(e_i,k_i)=f e_{i-1} l_i] *)
+val list_fold_map : 
+  ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list 
 
 (*s Arrays. *)
 
@@ -123,6 +137,7 @@ val array_app_tl : 'a array -> 'a list -> 'a list
 val array_list_of_tl : 'a array -> 'a list
 val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list
 val array_chop : int -> 'a array -> 'a array * 'a array
+val array_smartmap : ('a -> 'a) -> 'a array -> 'a array
 val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 val array_map3 : 
@@ -159,6 +174,7 @@ val in_some : 'a -> 'a option
 val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option
 val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
+val option_smartmap : ('a -> 'a) -> 'a option -> 'a option
 
 (* In [map_succeed f l] an element [a] is removed if [f a] raises *)
 (* [Failure _] otherwise behaves as [List.map f l] *)