# HG changeset patch # User paulson # Date 1119353664 -7200 # Node ID 7896ea4f3a87ef473d3626a74a1460a38f51aac8 # Parent 090c6a98c7047014e2695e48bc30ee873a9a9904 VAMPIRE_HOME, helper_path and various stylistic tweaks diff -r 090c6a98c704 -r 7896ea4f3a87 src/HOL/Tools/ATP/recon_order_clauses.ML --- 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 diff -r 090c6a98c704 -r 7896ea4f3a87 src/HOL/Tools/ATP/watcher.ML --- 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 diff -r 090c6a98c704 -r 7896ea4f3a87 src/HOL/Tools/res_atp.ML --- 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) diff -r 090c6a98c704 -r 7896ea4f3a87 src/HOL/Tools/res_lib.ML --- 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;