author | paulson |
Tue, 21 Jun 2005 13:34:24 +0200 | |
changeset 16515 | 7896ea4f3a87 |
parent 15774 | 9df37a0e935d |
child 16902 | 1cc75f32a2fd |
permissions | -rw-r--r-- |
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 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
11 |
val flat_noDup : ''a list list -> ''a list |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
12 |
val helper_path : string -> string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
13 |
val list2str_sep : string -> string list -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
14 |
val list_to_string : string list -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
15 |
val list_to_string' : string list -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
16 |
val no_BDD : string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
17 |
val no_blanks : string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
18 |
val no_blanks_dots : string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
19 |
val no_blanks_dots_dashes : string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
20 |
val no_dots : string -> string |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
21 |
val no_rep_add : ''a -> ''a list -> ''a list |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
22 |
val no_rep_app : ''a list -> ''a list -> ''a list |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
23 |
val pair_ins : 'a -> 'b list -> ('a * 'b) list |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
24 |
val rm_rep : ''a list -> ''a list |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
25 |
val write_strs : TextIO.outstream -> TextIO.vector list -> unit |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
26 |
val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit |
15347 | 27 |
end; |
28 |
||
29 |
||
30 |
structure ResLib : RES_LIB = |
|
31 |
struct |
|
32 |
||
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
33 |
(* convert a list of strings into one single string; surrounded by brackets *) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
34 |
fun list_to_string strings = |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
35 |
let |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
36 |
fun str_of [s] = s |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
37 |
| str_of (s1::ss) = s1 ^ "," ^ (str_of ss) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
38 |
| str_of _ = "" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
39 |
in |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
40 |
"(" ^ str_of strings ^ ")" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
41 |
end; |
15347 | 42 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
43 |
fun list_to_string' strings = |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
44 |
let |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
45 |
fun str_of [s] = s |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
46 |
| str_of (s1::ss) = s1 ^ "," ^ (str_of ss) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
47 |
| str_of _ = "" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
48 |
in |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
49 |
"[" ^ str_of strings ^ "]" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
50 |
end; |
15347 | 51 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
52 |
(* remove some chars (not allowed by TPTP format) from a string *) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
53 |
fun no_blanks " " = "_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
54 |
| no_blanks c = c; |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
55 |
|
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
56 |
fun no_dots "." = "_dot_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
57 |
| no_dots c = c; |
15347 | 58 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
59 |
fun no_blanks_dots " " = "_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
60 |
| no_blanks_dots "." = "_dot_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
61 |
| no_blanks_dots c = c; |
15347 | 62 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
63 |
fun no_blanks_dots_dashes " " = "_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
64 |
| no_blanks_dots_dashes "." = "_dot_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
65 |
| no_blanks_dots_dashes "'" = "_da_" |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
66 |
| no_blanks_dots_dashes c = c; |
15347 | 67 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
68 |
fun no_BDD cs = |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
69 |
implode (map no_blanks_dots_dashes (explode cs)); |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
70 |
|
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
71 |
fun no_rep_add x [] = [x] |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
72 |
| no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z); |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
73 |
|
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
74 |
fun no_rep_app l1 [] = l1 |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
75 |
| no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y; |
15347 | 76 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
77 |
fun rm_rep [] = [] |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
78 |
| rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y); |
15347 | 79 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
80 |
fun flat_noDup [] = [] |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
81 |
| flat_noDup (x::y) = no_rep_app x (flat_noDup y); |
15347 | 82 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
83 |
fun list2str_sep delim [] = delim |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
84 |
| list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss); |
15347 | 85 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
86 |
fun write_strs _ [] = () |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
87 |
| write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss); |
15347 | 88 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
89 |
fun writeln_strs _ [] = () |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
90 |
| writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss); |
15347 | 91 |
|
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
92 |
(* pair the first argument with each element in the second input list *) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
93 |
fun pair_ins x [] = [] |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
94 |
| pair_ins x (y::ys) = (x, y) :: (pair_ins x ys); |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
95 |
|
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
96 |
(*Return the path to a "helper" like SPASS or tptp2X, first checking that |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
97 |
it exists. --lcp *) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
98 |
fun helper_path evar base = |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
99 |
case getenv evar of |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
100 |
"" => error ("Isabelle environment variable " ^ evar ^ " not defined") |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
101 |
| home => |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
102 |
let val path = home ^ "/" ^ base |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
103 |
in if File.exists (File.unpack_platform_path path) then path |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
104 |
else error ("Could not find the file " ^ path) |
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
15774
diff
changeset
|
105 |
end; |
15347 | 106 |
|
15604 | 107 |
end; |