ajout dyn; divers fonctions util

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

5 files changed, 141 insertions, 0 deletions

diff --git a/lib/coqast.mli b/lib/coqast.mli
new file mode 100644
index 0000000000..5c7453412e
--- /dev/null
+++ b/lib/coqast.mli
@@ -0,0 +1,17 @@
+
+(* $Id$^*)
+
+type loc = int * int
+
+type t =
+  | Node of loc * string * t list
+  | Nvar of loc * string
+  | Slam of loc * string option * t
+  | Num of loc * int
+  | Id of loc * string
+  | Str of loc * string
+  | Path of loc * string list* string
+  | Dynamic of loc * Dyn.t
+
+val hcons_ast: (string -> string) -> (t -> t) * (loc -> loc)
+
diff --git a/lib/dyn.ml b/lib/dyn.ml
new file mode 100644
index 0000000000..92fa14f6d4
--- /dev/null
+++ b/lib/dyn.ml
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+open Util
+
+(* Dynamics, programmed with DANGER !!! *)
+
+type t = string * Obj.t
+
+let dyntab = ref ([] : string list)
+
+let create s =
+  if List.mem s !dyntab then anomaly "Dyn.create: already declared dynamic";
+  dyntab := s :: !dyntab;
+  ((fun v -> (s,Obj.repr v)),
+   (fun (s',rv) ->
+      if s = s' then Obj.magic rv else failwith "dyn_out"))
+
+let tag (s,_) = s
diff --git a/lib/dyn.mli b/lib/dyn.mli
new file mode 100644
index 0000000000..2f2bb7b802
--- /dev/null
+++ b/lib/dyn.mli
@@ -0,0 +1,9 @@
+
+(* $Id$ *)
+
+(* Dynamics. Use with extreme care. Not for kids. *)
+
+type t
+
+val create : string -> ('a -> t) * (t -> 'a)
+val tag : t -> string
diff --git a/lib/util.ml b/lib/util.ml
index d28b0c25f3..adf3c757a1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -69,6 +69,78 @@ let intersect l1 l2 =
 let subtract l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
 
+(* Arrays *)
+
+let array_exists f v = 
+  let rec exrec = function
+    | -1 -> false
+    | n -> (f v.(n)) || (exrec (n-1))
+  in 
+  exrec ((Array.length v)-1) 
+
+let array_for_all2 f v1 v2 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 && allrec (pred lv1) 
+
+let array_tl v = 
+  match Array.length v with
+    | 0 -> failwith "array_tl"
+    | n -> Array.sub v 1 (pred n)
+
+let array_hd v = 
+  match Array.length v with
+    | 0 -> failwith "array_hd"
+    | _ -> v.(0)
+
+let array_cons e v = Array.append [|e|] v
+
+let array_fold_left_from n f a v = 
+  let rec fold a n =
+    if n >= Array.length v then a else fold (f a v.(n)) (succ n)
+  in 
+  fold a n
+
+let array_fold_right_from n f v a = 
+  let rec fold n =
+    if n >= Array.length v then a else f v.(n) (fold (succ n))
+  in 
+  fold n
+
+let array_app_tl v l = 
+  if Array.length v = 0 then 
+    invalid_arg "array_app_tl"
+  else 
+    array_fold_right_from 1 (fun e l -> e::l) v l
+
+let array_list_of_tl v =
+  if Array.length v = 0 then 
+    invalid_arg "array_list_of_tl"
+  else 
+    array_fold_right_from 1 (fun e l -> e::l) v []
+
+let array_map_to_list f v =
+  List.map f (Array.to_list v)
+
+(* Functions *)
+
+let compose f g x = f (g x)
+
+let iterate f = 
+  let rec iterate_f n x =
+    if n <= 0 then x else iterate_f (pred n) (f x)
+  in 
+  iterate_f
+ 
+(* Misc *)
+
+type ('a,'b) union = Inl of 'a | Inr of 'b
+
+module Intset = Set.Make(struct type t = int let compare = compare end)
+
 (* Pretty-printing *)
   
 let pr_spc () = [< 'sPC >];;
diff --git a/lib/util.mli b/lib/util.mli
index 5d4c706b9a..4e92b46b80 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -25,6 +25,30 @@ 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
 
+(* Arrays *)
+
+val array_exists : ('a -> bool) -> 'a array -> bool
+val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
+val array_hd : 'a array -> 'a
+val array_tl : 'a array -> 'a array
+val array_cons : 'a -> 'a array -> 'a array
+val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
+val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+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
+
+(* Functions *)
+
+val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val iterate : ('a -> 'a) -> int -> 'a -> 'a
+
+(* Misc *)
+
+type ('a,'b) union = Inl of 'a | Inr of 'b
+
+module Intset : Set.S with type elt = int
+
 (* Pretty-printing *)
 
 val pr_spc : unit -> std_ppcmds