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