--- a/src/HOL/Tools/res_lib.ML Tue Jun 21 11:08:31 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Tue Jun 21 13:34:24 2005 +0200
@@ -8,90 +8,100 @@
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
-
+val flat_noDup : ''a list list -> ''a list
+val helper_path : string -> string -> string
+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;
+(* 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;
+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;
+(* 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_dots "." = "_dot_"
- | no_dots c = c;
+fun no_blanks_dots " " = "_"
+ | no_blanks_dots "." = "_dot_"
+ | no_blanks_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_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 no_BDD cs =
- implode (map no_blanks_dots_dashes (explode cs));
+fun rm_rep [] = []
+ | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
- 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 flat_noDup [] = []
+ | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
- fun no_rep_app l1 [] = l1
- | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
+fun list2str_sep delim [] = delim
+ | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
- fun rm_rep [] = []
- | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
+fun write_strs _ [] = ()
+ | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
- 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 writeln_strs _ [] = ()
+ | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out 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);
+(* 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);
+
+(*Return the path to a "helper" like SPASS or tptp2X, first checking that
+ it exists. --lcp *)
+fun helper_path evar base =
+ case getenv evar of
+ "" => error ("Isabelle environment variable " ^ evar ^ " not defined")
+ | home =>
+ let val path = home ^ "/" ^ base
+ in if File.exists (File.unpack_platform_path path) then path
+ else error ("Could not find the file " ^ path)
+ end;
end;