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