src/HOL/Tools/res_lib.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_lib.ML	Tue Nov 30 18:25:55 2004 +0100
@@ -0,0 +1,124 @@
+(*  Author: Jia Meng, Cambridge University Computer Laboratory
+    ID: $Id$
+    Copyright 2004 University of Cambridge
+
+some frequently used functions by files in this directory.
+*)
+
+signature RES_LIB =
+sig
+
+val flat_noDup : ''a list list -> ''a list
+val list2str_sep : string -> string list -> string
+val list_to_string : string list -> string
+val list_to_string' : string list -> string
+val no_BDD : string -> string
+val no_blanks : string -> string
+val no_blanks_dots : string -> string
+val no_blanks_dots_dashes : string -> string
+val no_dots : string -> string
+val no_rep_add : ''a -> ''a list -> ''a list
+val no_rep_app : ''a list -> ''a list -> ''a list
+val pair_ins : 'a -> 'b list -> ('a * 'b) list
+val rm_rep : ''a list -> ''a list
+val unzip : ('a * 'b) list -> 'a list * 'b list
+val write_strs : TextIO.outstream -> TextIO.vector list -> unit
+val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
+val zip : 'a list -> 'b list -> ('a * 'b) list
+
+
+end;
+
+
+
+structure ResLib : RES_LIB =
+
+struct
+
+(*** convert a list of strings into one single string; surrounded by backets ***)
+fun list_to_string strings =
+    let fun str_of [s] = s 
+          | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
+          | str_of _ = ""
+    in
+	"(" ^ str_of strings ^ ")"
+    end;
+
+fun list_to_string' strings =
+    let fun str_of [s] = s 
+          | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
+          | str_of _ = ""
+    in
+	"[" ^ str_of strings ^ "]"
+    end;
+
+
+
+(*** remove some chars (not allowed by TPTP format) from a string ***)
+fun no_blanks " " = "_"
+  | no_blanks c   = c;
+
+
+fun no_dots "." = "_dot_"
+  | no_dots c   = c;
+
+
+fun no_blanks_dots " " = "_"
+  | no_blanks_dots "." = "_dot_"
+  | no_blanks_dots c   = c;
+    
+fun no_blanks_dots_dashes " " = "_"
+  | no_blanks_dots_dashes "." = "_dot_"
+  | no_blanks_dots_dashes "'" = "_da_"
+  | no_blanks_dots_dashes c   = c;
+    
+fun no_BDD cs = implode (map no_blanks_dots_dashes (explode cs));
+
+
+
+fun no_rep_add x [] = [x]
+  | no_rep_add x (y :: z) = if (x = y) then (y :: z)
+                             else y :: (no_rep_add x z); 
+
+
+fun no_rep_app l1 [] = l1
+  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
+ 
+
+fun rm_rep [] = []
+  | rm_rep (x::y) = if (x mem y) then rm_rep y else x::(rm_rep y);
+
+
+fun unzip [] = ([],[])
+  | unzip ((x1,y1)::zs) = 
+    let val (xs,ys) = unzip zs
+    in
+        (x1::xs,y1::ys)
+    end;
+
+fun zip [] [] = [] 
+   | zip(x::xs) (y::ys) = (x,y)::(zip xs ys);
+
+
+fun flat_noDup [] = []
+  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
+
+
+
+fun list2str_sep delim [] = delim
+  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
+
+
+
+fun write_strs _ [] = ()
+  | write_strs out (s::ss) = (TextIO.output(out,s);write_strs out ss);
+
+fun writeln_strs _ [] = ()
+  | writeln_strs out (s::ss) = (TextIO.output(out,s);TextIO.output(out,"\n");writeln_strs out ss);
+
+(* pair the first argument with each of the element in the second input list *)
+fun pair_ins x [] = []
+  | pair_ins x (y::ys) = (x,y) :: (pair_ins x ys);
+
+
+end;
\ No newline at end of file