src/HOL/Tools/res_lib.ML

Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.

(*  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;