--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Jun 21 11:08:31 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Jun 21 13:34:24 2005 +0200
@@ -66,11 +66,9 @@
(a_lhs = x_rhs) andalso (a_rhs = x_lhs)
end
-fun equal_pair (a,b) = equal a b
-
fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
-fun var_equiv vars (a,b) = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
+fun var_equiv vars (a,b) = a=b orelse (is_var_pair (a,b) vars)
fun all_true [] = false
| all_true xs = let val falselist = List.filter (equal false ) xs
--- a/src/HOL/Tools/ATP/watcher.ML Tue Jun 21 11:08:31 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Jun 21 13:34:24 2005 +0200
@@ -262,17 +262,9 @@
File.platform_path wholefile])
val dfg_dir = File.tmp_path (Path.basic "dfg");
- (*** check if the directory exists and, if not, create it***)
- val dfg_create =
- if File.exists dfg_dir then warning("dfg dir exists")
- else File.mkdir dfg_dir;
val dfg_path = File.platform_path dfg_dir;
- val tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X"
-
-
- (*** need to check here if the directory exists and, if not, create it***)
-
+ val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"
(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
val probID = List.last(explode probfile)
@@ -281,33 +273,26 @@
(*** only include problem and clasimp for the moment, not sure how to refer to ***)
(*** hyps/local axioms just now ***)
val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)])
- val dfg_create =
+ (*** check if the directory exists and, if not, create it***)
+ val _ =
if !SpassComm.spass
then
- if File.exists dfg_dir
- then
- ((warning("dfg dir exists"));())
- else
- File.mkdir dfg_dir
+ if File.exists dfg_dir then warning("dfg dir exists")
+ else File.mkdir dfg_dir
else
- (warning("not converting to dfg");())
- val dfg_path = File.platform_path dfg_dir;
+ warning("not converting to dfg")
- val bar = if !SpassComm.spass then system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^
- (File.platform_path wholefile)^" -d "^dfg_path)
- else
- 7
-
+ val _ = if !SpassComm.spass then
+ system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
+ File.platform_path wholefile)
+ else 7
val newfile = if !SpassComm.spass
then
dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
else
(File.platform_path wholefile)
-
- val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));
- val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))
- val _ = TextIO.closeOut outfile
-
+ val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
+ (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
in
(prover,thmstring,goalstring, proverCmd, settings,newfile)
end;
@@ -804,121 +789,95 @@
end
-fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
- val streams =snd mychild
- val childin = fst streams
- val childout = snd streams
- val childpid = fst mychild
- val sign = sign_of_thm thm
- val prems = prems_of thm
- val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
- val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
- fun vampire_proofHandler (n) =
- (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
-
-
-fun spass_proofHandler (n) = (
- let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
- val _ = TextIO.output (outfile, ("In signal handler now\n"))
- val _ = TextIO.closeOut outfile
- val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
- val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
-
- val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
- val _ = TextIO.closeOut outfile
- in (* if a proof has been found and sent back as a reconstruction proof *)
- if ( (substring (reconstr, 0,1))= "[")
- then
+fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
+ let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
+ val streams =snd mychild
+ val childin = fst streams
+ val childout = snd streams
+ val childpid = fst mychild
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
+ fun vampire_proofHandler (n) =
+ (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))
- (
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Recon_Transfer.apply_res_thm reconstr goalstring;
- Pretty.writeln(Pretty.str (oct_char "361"));
-
- goals_being_watched := ((!goals_being_watched) - 1);
-
- if ((!goals_being_watched) = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end)
- else
- ()
- )
- (* if there's no proof, but a message from Spass *)
- else if ((substring (reconstr, 0,5))= "SPASS")
- then
- (
- goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end )
- else
- ()
- )
- (* print out a list of rules used from clasimpset*)
- else if ((substring (reconstr, 0,5))= "Rules")
- then
- (
- goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^reconstr));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout);()
- end )
- else
- ()
- )
-
- (* if proof translation failed *)
- else if ((substring (reconstr, 0,5)) = "Proof")
- then
- (
- goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end )
- else
- ()
- )
-
-
- else (* add something here ?*)
- ()
-
- end)
-
-
-
- in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
- IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
- (childin, childout, childpid)
+ fun spass_proofHandler (n) =
+ let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
+ val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
+ val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
+ ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
+ in (* if a proof has been found and sent back as a reconstruction proof *)
+ if ( (substring (reconstr, 0,1))= "[")
+ then
+ (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Recon_Transfer.apply_res_thm reconstr goalstring;
+ Pretty.writeln(Pretty.str (oct_char "361"));
+
+ goals_being_watched := ((!goals_being_watched) - 1);
+
+ if ((!goals_being_watched) = 0)
+ then
+ let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
+ ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end
+ else ()
+ )
+ (* if there's no proof, but a message from Spass *)
+ else if ((substring (reconstr, 0,5))= "SPASS")
+ then
+ (goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
+ ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
+ else ()
+ )
+ (* print out a list of rules used from clasimpset*)
+ else if ((substring (reconstr, 0,5))= "Rules")
+ then
+ (goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
+ ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
+ killWatcher (childpid); reapWatcher (childpid,childin, childout);())
+ else ()
+ )
+
+ (* if proof translation failed *)
+ else if ((substring (reconstr, 0,5)) = "Proof")
+ then
+ (goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
+ ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
+ else
+ ()
+ )
+ else (* add something here ?*)
+ ()
+
+ end
+
+ in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+ IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
+ (childin, childout, childpid)
end
--- a/src/HOL/Tools/res_atp.ML Tue Jun 21 11:08:31 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Jun 21 13:34:24 2005 +0200
@@ -153,18 +153,15 @@
(* should be modified to allow other provers to be called *)
(*********************************************************************)
(* now passing in list of skolemized thms and list of sgterms to go with them *)
-fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = let
+fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n =
+ let
val axfile = (File.platform_path axiom_file)
val hypsfile = (File.platform_path hyps_file)
val clasimpfile = (File.platform_path clasimp_file)
- val spass_home = getenv "SPASS_HOME"
- val spass = spass_home ^ "/SPASS"
- val _ = if File.exists (File.unpack_platform_path spass) then ()
- else error ("Could not find the file " ^ spass)
fun make_atp_list [] sign n = []
| make_atp_list ((sko_thm, sg_term)::xs) sign n =
- let
+ let
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm)
val thmproofstr = proofstring ( skothmstr)
val no_returns =List.filter not_newline ( thmproofstr)
@@ -178,26 +175,32 @@
val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
- val _ = (warning ("prob file in cal_res_tac is: "^probfile))
-in
- if !SpassComm.spass
- then if !full_spass
- then
+ val _ = (warning ("prob file in cal_res_tac is: "^probfile))
+ in
+ if !SpassComm.spass
+ then
+ let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
+ in (*We've checked that SPASS is there for ATP/spassshell to run.*)
+ if !full_spass
+ then (*Allow SPASS to run in Auto mode, using all its inference rules*)
([("spass", thmstr, goalstring (*,spass_home*),
- getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),
+ getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
"-DocProof%-TimeLimit=60",
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
- else
+ else (*Restrict SPASS to a small set of rules that we can parse*)
([("spass", thmstr, goalstring (*,spass_home*),
getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),
"-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60",
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
+ end
else
- ([("vampire", thmstr, goalstring (*,spass_home*),
- "/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*),
- "-t 300%-m 100000",
- clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
-end
+ let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
+ in
+ ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000",
+ clasimpfile, axfile, hypsfile, probfile)] @
+ (make_atp_list xs sign (n+1)))
+ end
+ end
val thms_goals = ListPair.zip( thms, sg_terms)
val atp_list = make_atp_list thms_goals sign 1
@@ -228,14 +231,14 @@
fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms =
- if (equal n 0) then
- (call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
- else
-
- ( SELECT_GOAL
- (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
- get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms);dummy_tac))]) n thm )
+ if n=0 then
+ (call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
+ else
+
+ ( SELECT_GOAL
+ (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
+ METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
+ get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms);dummy_tac))]) n thm )
@@ -246,21 +249,19 @@
(**********************************************)
fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) =
-
- (let val prems = prems_of thm
- (*val sg_term = get_nth k prems*)
- val sign = sign_of_thm thm
- val thmstring = string_of_thm thm
- in
-
- (warning("in isar_atp_goal'"));
- (warning("thmstring in isar_atp_goal': "^thmstring));
- (* go and call callResProvers with this subgoal *)
- (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *)
- (* recursive call to pick up the remaining subgoals *)
- (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *)
- get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []
- end);
+ let val prems = prems_of thm
+ (*val sg_term = get_nth k prems*)
+ val sign = sign_of_thm thm
+ val thmstring = string_of_thm thm
+ in
+ warning("in isar_atp_goal'");
+ warning("thmstring in isar_atp_goal': "^thmstring);
+ (* go and call callResProvers with this subgoal *)
+ (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *)
+ (* recursive call to pick up the remaining subgoals *)
+ (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *)
+ get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []
+ end ;
(*fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) =
(if (!debug) then warning (string_of_thm thm)
--- 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;