# HG changeset patch # User immler@in.tum.de # Date 1246194088 -7200 # Node ID 607a984b70e3b7def0881a922cb54f1f5e49389c # Parent a50de97f1b08a089f58d2b562799e624573f5c41 use structure File instead of TextIO; removed comments diff -r a50de97f1b08 -r 607a984b70e3 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 15:01:28 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 15:01:28 2009 +0200 @@ -75,20 +75,16 @@ (* write out problem file and call prover *) val probfile = prob_pathname subgoalno - val fname = File.platform_path probfile - val _ = writer fname clauses - val cmdline = - if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args - else error ("Bad executable: " ^ Path.implode cmd) - val (proof, rc) = system_out (cmdline ^ " " ^ fname) + val _ = writer probfile clauses + val (proof, rc) = system_out ( + if File.exists cmd then + space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile] + else error ("Bad executable: " ^ Path.implode cmd)) (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) val _ = - if destdir' = "" then OS.FileSys.remove fname - else - let val out = TextIO.openOut (fname ^ "_proof") - val _ = TextIO.output (out, proof) - in TextIO.closeOut out end + if destdir' = "" then File.rm probfile + else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof (* check for success and print out some information on failure *) val failure = find_failure proof diff -r a50de97f1b08 -r 607a984b70e3 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Sun Jun 28 15:01:28 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Sun Jun 28 15:01:28 2009 +0200 @@ -57,7 +57,6 @@ val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table val init_functab: int Symtab.table - val writeln_strs: TextIO.outstream -> string list -> unit val dfg_sign: bool -> string -> string val dfg_of_typeLit: bool -> type_literal -> string val gen_dfg_cls: int * string * kind * string list * string list * string list -> string @@ -441,8 +440,6 @@ fun string_of_type_clsname (cls_id,ax_name,idx) = string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); -fun writeln_strs os = List.app (fn s => TextIO.output (os, s)); - (**** Producing DFG files ****) diff -r a50de97f1b08 -r 607a984b70e3 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Sun Jun 28 15:01:28 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Sun Jun 28 15:01:28 2009 +0200 @@ -26,18 +26,18 @@ val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL - val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *) + val make_conjecture_clauses: bool -> theory -> thm list -> clause list val make_axiom_clauses: bool -> theory -> - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *) + (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list val get_helper_clauses: bool -> theory -> bool -> clause list * (thm * (axiom_name * clause_id)) list * string list -> clause list - val tptp_write_file: bool -> string -> + val tptp_write_file: bool -> Path.T -> clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit - val dfg_write_file: bool -> string -> + val dfg_write_file: bool -> Path.T -> clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit end @@ -469,59 +469,56 @@ (* tptp format *) -fun tptp_write_file t_full filename clauses = +fun tptp_write_file t_full file clauses = let val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) - val out = TextIO.openOut filename in - List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses; - RC.writeln_strs out tfree_clss; - RC.writeln_strs out tptp_clss; - List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; - List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses; - TextIO.closeOut out + File.write_list file ( + map (#1 o (clause2tptp params)) axclauses @ + tfree_clss @ + tptp_clss @ + map RC.tptp_classrelClause classrel_clauses @ + map RC.tptp_arity_clause arity_clauses @ + map (#1 o (clause2tptp params)) helper_clauses) end; (* dfg format *) -fun dfg_write_file t_full filename clauses = +fun dfg_write_file t_full file clauses = let val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) - and probname = Path.implode (Path.base (Path.explode filename)) + and probname = Path.implode (Path.base file) val axstrs = map (#1 o (clause2dfg params)) axclauses val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) - val out = TextIO.openOut filename val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses in - TextIO.output (out, RC.string_of_start probname); - TextIO.output (out, RC.string_of_descrip probname); - TextIO.output (out, RC.string_of_symbols - (RC.string_of_funcs funcs) - (RC.string_of_preds (cl_preds @ ty_preds))); - TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); - RC.writeln_strs out axstrs; - List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; - RC.writeln_strs out helper_clauses_strs; - TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); - RC.writeln_strs out tfree_clss; - RC.writeln_strs out dfg_clss; - TextIO.output (out, "end_of_list.\n\n"); - (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) - TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); - TextIO.output (out, "end_problem.\n"); - TextIO.closeOut out + File.write_list file ( + RC.string_of_start probname :: + RC.string_of_descrip probname :: + RC.string_of_symbols (RC.string_of_funcs funcs) + (RC.string_of_preds (cl_preds @ ty_preds)) :: + "list_of_clauses(axioms,cnf).\n" :: + axstrs @ + map RC.dfg_classrelClause classrel_clauses @ + map RC.dfg_arity_clause arity_clauses @ + helper_clauses_strs @ + ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ + tfree_clss @ + dfg_clss @ + ["end_of_list.\n\n", + (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) + "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n", + "end_problem.\n"]) end; end