src/HOL/Tools/res_lib.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15604 6fb06b768f67
child 15774 9df37a0e935d
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/Tools/res_lib.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory
     3     ID:         $Id$
     4     Copyright   2004 University of Cambridge
     5 
     6 Some auxiliary functions frequently used by files in this directory.
     7 *)
     8 
     9 signature RES_LIB =
    10 sig
    11 
    12 	val flat_noDup : ''a list list -> ''a list
    13 	val list2str_sep : string -> string list -> string
    14 	val list_to_string : string list -> string
    15 	val list_to_string' : string list -> string
    16 	val no_BDD : string -> string
    17 	val no_blanks : string -> string
    18 	val no_blanks_dots : string -> string
    19 	val no_blanks_dots_dashes : string -> string
    20 	val no_dots : string -> string
    21 	val no_rep_add : ''a -> ''a list -> ''a list
    22 	val no_rep_app : ''a list -> ''a list -> ''a list
    23 	val pair_ins : 'a -> 'b list -> ('a * 'b) list
    24 	val rm_rep : ''a list -> ''a list
    25 	val unzip : ('a * 'b) list -> 'a list * 'b list
    26 	val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    27 	val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
    28 	val zip : 'a list -> 'b list -> ('a * 'b) list
    29 
    30 end;
    31 
    32 
    33 structure ResLib : RES_LIB =
    34 struct
    35 
    36 	(* convert a list of strings into one single string; surrounded by brackets *)
    37 	fun list_to_string strings =
    38 	let
    39 		fun str_of [s]      = s
    40 		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    41 		  | str_of _        = ""
    42 	in
    43 		"(" ^ str_of strings ^ ")"
    44 	end;
    45 
    46 	fun list_to_string' strings =
    47 	let
    48 		fun str_of [s]      = s
    49 		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    50 		  | str_of _        = ""
    51 	in
    52 		"[" ^ str_of strings ^ "]"
    53 	end;
    54 
    55 	(* remove some chars (not allowed by TPTP format) from a string *)
    56 	fun no_blanks " " = "_"
    57 	  | no_blanks c   = c;
    58 
    59 	fun no_dots "." = "_dot_"
    60 	  | no_dots c   = c;
    61 
    62 	fun no_blanks_dots " " = "_"
    63 	  | no_blanks_dots "." = "_dot_"
    64 	  | no_blanks_dots c   = c;
    65 
    66 	fun no_blanks_dots_dashes " " = "_"
    67 	  | no_blanks_dots_dashes "." = "_dot_"
    68 	  | no_blanks_dots_dashes "'" = "_da_"
    69 	  | no_blanks_dots_dashes c   = c;
    70 
    71 	fun no_BDD cs =
    72 		implode (map no_blanks_dots_dashes (explode cs));
    73 
    74 	fun no_rep_add x []     = [x]
    75 	  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
    76 
    77 	fun no_rep_app l1 []     = l1
    78 	  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
    79 
    80 	fun rm_rep []     = []
    81 	  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
    82 
    83 	fun unzip []             =
    84 		([], [])
    85 	  | unzip ((x1, y1)::zs) =
    86 		let
    87 			val (xs, ys) = unzip zs
    88 		in
    89 			(x1::xs, y1::ys)
    90 		end;
    91 
    92 	fun zip []      []      = []
    93 	  | zip (x::xs) (y::ys) = (x, y)::(zip xs ys);
    94 
    95 	fun flat_noDup []     = []
    96 	  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    97 
    98 	fun list2str_sep delim []      = delim
    99 	  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
   100 
   101 	fun write_strs _   []      = ()
   102 	  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
   103 
   104 	fun writeln_strs _   []      = ()
   105 	  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
   106 
   107 	(* pair the first argument with each element in the second input list *)
   108 	fun pair_ins x []      = []
   109 	  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
   110 
   111 end;