15604
|
1 |
(* Title: HOL/Tools/res_lib.ML
|
|
2 |
Author: Jia Meng, Cambridge University Computer Laboratory
|
|
3 |
ID: $Id$
|
|
4 |
Copyright 2004 University of Cambridge
|
15347
|
5 |
|
15604
|
6 |
Some auxiliary functions frequently used by files in this directory.
|
15347
|
7 |
*)
|
|
8 |
|
|
9 |
signature RES_LIB =
|
|
10 |
sig
|
|
11 |
|
15604
|
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
|
15347
|
29 |
|
|
30 |
end;
|
|
31 |
|
|
32 |
|
|
33 |
structure ResLib : RES_LIB =
|
|
34 |
struct
|
|
35 |
|
15604
|
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;
|
15347
|
45 |
|
15604
|
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;
|
15347
|
54 |
|
15604
|
55 |
(* remove some chars (not allowed by TPTP format) from a string *)
|
|
56 |
fun no_blanks " " = "_"
|
|
57 |
| no_blanks c = c;
|
15347
|
58 |
|
15604
|
59 |
fun no_dots "." = "_dot_"
|
|
60 |
| no_dots c = c;
|
15347
|
61 |
|
15604
|
62 |
fun no_blanks_dots " " = "_"
|
|
63 |
| no_blanks_dots "." = "_dot_"
|
|
64 |
| no_blanks_dots c = c;
|
15347
|
65 |
|
15604
|
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;
|
15347
|
70 |
|
15604
|
71 |
fun no_BDD cs =
|
|
72 |
implode (map no_blanks_dots_dashes (explode cs));
|
15347
|
73 |
|
15604
|
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);
|
15347
|
76 |
|
15604
|
77 |
fun no_rep_app l1 [] = l1
|
|
78 |
| no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
|
15347
|
79 |
|
15604
|
80 |
fun rm_rep [] = []
|
|
81 |
| rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
|
15347
|
82 |
|
15604
|
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;
|
15347
|
91 |
|
15604
|
92 |
fun zip [] [] = []
|
|
93 |
| zip (x::xs) (y::ys) = (x, y)::(zip xs ys);
|
15347
|
94 |
|
15604
|
95 |
fun flat_noDup [] = []
|
|
96 |
| flat_noDup (x::y) = no_rep_app x (flat_noDup y);
|
15347
|
97 |
|
15604
|
98 |
fun list2str_sep delim [] = delim
|
|
99 |
| list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
|
15347
|
100 |
|
15604
|
101 |
fun write_strs _ [] = ()
|
|
102 |
| write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
|
15347
|
103 |
|
15604
|
104 |
fun writeln_strs _ [] = ()
|
|
105 |
| writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
|
15347
|
106 |
|
15604
|
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);
|
15347
|
110 |
|
15604
|
111 |
end;
|