src/HOL/Tools/res_lib.ML

isa-migrate ++

(*  Title:      HOL/Tools/res_lib.ML
    Author:     Jia Meng, Cambridge University Computer Laboratory
    ID:         $Id$
    Copyright   2004 University of Cambridge

Some auxiliary functions frequently used 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 write_strs : TextIO.outstream -> TextIO.vector list -> unit
	val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit

end;


structure ResLib : RES_LIB =
struct

	(* convert a list of strings into one single string; surrounded by brackets *)
	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 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 element in the second input list *)
	fun pair_ins x []      = []
	  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);

end;