use structure File instead of TextIO;
authorimmler@in.tum.de
Sun Jun 28 15:01:28 2009 +0200 (2009-06-28)
changeset 31838607a984b70e3
parent 31837 a50de97f1b08
child 31839 26f18ec0e293
use structure File instead of TextIO;
removed comments
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp_wrapper.ML	Sun Jun 28 15:01:28 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Sun Jun 28 15:01:28 2009 +0200
     1.3 @@ -75,20 +75,16 @@
     1.4  
     1.5      (* write out problem file and call prover *)
     1.6      val probfile = prob_pathname subgoalno
     1.7 -    val fname = File.platform_path probfile
     1.8 -    val _ = writer fname clauses
     1.9 -    val cmdline =
    1.10 -      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
    1.11 -      else error ("Bad executable: " ^ Path.implode cmd)
    1.12 -    val (proof, rc) = system_out (cmdline ^ " " ^ fname)
    1.13 +    val _ = writer probfile clauses
    1.14 +    val (proof, rc) = system_out (
    1.15 +      if File.exists cmd then
    1.16 +        space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
    1.17 +      else error ("Bad executable: " ^ Path.implode cmd))
    1.18  
    1.19      (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
    1.20      val _ =
    1.21 -      if destdir' = "" then OS.FileSys.remove fname
    1.22 -      else
    1.23 -        let val out = TextIO.openOut (fname ^ "_proof")
    1.24 -        val _ = TextIO.output (out, proof)
    1.25 -        in TextIO.closeOut out end
    1.26 +      if destdir' = "" then File.rm probfile
    1.27 +      else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
    1.28      
    1.29      (* check for success and print out some information on failure *)
    1.30      val failure = find_failure proof
     2.1 --- a/src/HOL/Tools/res_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     2.3 @@ -57,7 +57,6 @@
     2.4    val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
     2.5    val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
     2.6    val init_functab: int Symtab.table
     2.7 -  val writeln_strs: TextIO.outstream -> string list -> unit
     2.8    val dfg_sign: bool -> string -> string
     2.9    val dfg_of_typeLit: bool -> type_literal -> string
    2.10    val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    2.11 @@ -441,8 +440,6 @@
    2.12  fun string_of_type_clsname (cls_id,ax_name,idx) =
    2.13      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
    2.14  
    2.15 -fun writeln_strs os = List.app (fn s => TextIO.output (os, s));
    2.16 -
    2.17  
    2.18  (**** Producing DFG files ****)
    2.19  
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     3.3 @@ -26,18 +26,18 @@
     3.4    val strip_comb: combterm -> combterm * combterm list
     3.5    val literals_of_term: theory -> term -> literal list * typ list
     3.6    exception TOO_TRIVIAL
     3.7 -  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
     3.8 +  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list
     3.9    val make_axiom_clauses: bool ->
    3.10         theory ->
    3.11 -       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
    3.12 +       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
    3.13    val get_helper_clauses: bool ->
    3.14         theory ->
    3.15         bool ->
    3.16         clause list * (thm * (axiom_name * clause_id)) list * string list ->
    3.17         clause list
    3.18 -  val tptp_write_file: bool -> string ->
    3.19 +  val tptp_write_file: bool -> Path.T ->
    3.20      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    3.21 -  val dfg_write_file: bool -> string -> 
    3.22 +  val dfg_write_file: bool -> Path.T ->
    3.23      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    3.24  end
    3.25  
    3.26 @@ -469,59 +469,56 @@
    3.27  
    3.28  (* tptp format *)
    3.29  
    3.30 -fun tptp_write_file t_full filename clauses =
    3.31 +fun tptp_write_file t_full file clauses =
    3.32    let
    3.33      val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    3.34      val (cma, cnh) = count_constants clauses
    3.35      val params = (t_full, cma, cnh)
    3.36      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    3.37      val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
    3.38 -    val out = TextIO.openOut filename
    3.39    in
    3.40 -    List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses;
    3.41 -    RC.writeln_strs out tfree_clss;
    3.42 -    RC.writeln_strs out tptp_clss;
    3.43 -    List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
    3.44 -    List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
    3.45 -    List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses;
    3.46 -    TextIO.closeOut out
    3.47 +    File.write_list file (
    3.48 +      map (#1 o (clause2tptp params)) axclauses @
    3.49 +      tfree_clss @
    3.50 +      tptp_clss @
    3.51 +      map RC.tptp_classrelClause classrel_clauses @
    3.52 +      map RC.tptp_arity_clause arity_clauses @
    3.53 +      map (#1 o (clause2tptp params)) helper_clauses)
    3.54    end;
    3.55  
    3.56  
    3.57  (* dfg format *)
    3.58  
    3.59 -fun dfg_write_file t_full filename clauses =
    3.60 +fun dfg_write_file t_full file clauses =
    3.61    let
    3.62      val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    3.63      val (cma, cnh) = count_constants clauses
    3.64      val params = (t_full, cma, cnh)
    3.65      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
    3.66 -    and probname = Path.implode (Path.base (Path.explode filename))
    3.67 +    and probname = Path.implode (Path.base file)
    3.68      val axstrs = map (#1 o (clause2dfg params)) axclauses
    3.69      val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
    3.70 -    val out = TextIO.openOut filename
    3.71      val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
    3.72      val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
    3.73      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
    3.74    in
    3.75 -    TextIO.output (out, RC.string_of_start probname);
    3.76 -    TextIO.output (out, RC.string_of_descrip probname);
    3.77 -    TextIO.output (out, RC.string_of_symbols
    3.78 -                          (RC.string_of_funcs funcs)
    3.79 -                          (RC.string_of_preds (cl_preds @ ty_preds)));
    3.80 -    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
    3.81 -    RC.writeln_strs out axstrs;
    3.82 -    List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
    3.83 -    List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
    3.84 -    RC.writeln_strs out helper_clauses_strs;
    3.85 -    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
    3.86 -    RC.writeln_strs out tfree_clss;
    3.87 -    RC.writeln_strs out dfg_clss;
    3.88 -    TextIO.output (out, "end_of_list.\n\n");
    3.89 -    (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
    3.90 -    TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
    3.91 -    TextIO.output (out, "end_problem.\n");
    3.92 -    TextIO.closeOut out
    3.93 +    File.write_list file (
    3.94 +      RC.string_of_start probname ::
    3.95 +      RC.string_of_descrip probname ::
    3.96 +      RC.string_of_symbols (RC.string_of_funcs funcs)
    3.97 +        (RC.string_of_preds (cl_preds @ ty_preds)) ::
    3.98 +      "list_of_clauses(axioms,cnf).\n" ::
    3.99 +      axstrs @
   3.100 +      map RC.dfg_classrelClause classrel_clauses @
   3.101 +      map RC.dfg_arity_clause arity_clauses @
   3.102 +      helper_clauses_strs @
   3.103 +      ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
   3.104 +      tfree_clss @
   3.105 +      dfg_clss @
   3.106 +      ["end_of_list.\n\n",
   3.107 +      (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   3.108 +       "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
   3.109 +       "end_problem.\n"])
   3.110    end;
   3.111  
   3.112  end