src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 36167 c1a35be8e476
parent 35963 943e2582dc87
child 36168 0a6ed065683d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Apr 14 21:22:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
     1.5  struct
     1.6  
     1.7 +open Sledgehammer_Util
     1.8  open Sledgehammer_FOL_Clause
     1.9  open Sledgehammer_Fact_Preprocessor
    1.10  
    1.11 @@ -453,20 +454,26 @@
    1.12  
    1.13  fun write_tptp_file full_types file clauses =
    1.14    let
    1.15 +    fun section _ [] = []
    1.16 +      | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    1.17      val (conjectures, axclauses, _, helper_clauses,
    1.18        classrel_clauses, arity_clauses) = clauses
    1.19      val (cma, cnh) = count_constants clauses
    1.20      val params = (full_types, cma, cnh)
    1.21      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    1.22      val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
    1.23 +    val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" (Date.fromTimeLocal (Time.now ()))
    1.24      val _ =
    1.25        File.write_list file (
    1.26 -        map (#1 o (clause2tptp params)) axclauses @
    1.27 -        tfree_clss @
    1.28 -        tptp_clss @
    1.29 -        map tptp_classrel_clause classrel_clauses @
    1.30 -        map tptp_arity_clause arity_clauses @
    1.31 -        map (#1 o (clause2tptp params)) helper_clauses)
    1.32 +        "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
    1.33 +        "% " ^ timestamp ^ "\n" ::
    1.34 +        section "Relevant fact" (map (#1 o (clause2tptp params)) axclauses) @
    1.35 +        section "Type variable" tfree_clss @
    1.36 +        section "Class relationship"
    1.37 +                (map tptp_classrel_clause classrel_clauses) @
    1.38 +        section "Arity declaration" (map tptp_arity_clause arity_clauses) @
    1.39 +        section "Helper fact" (map (#1 o (clause2tptp params)) helper_clauses) @
    1.40 +        section "Conjecture" tptp_clss)
    1.41      in (length axclauses + 1, length tfree_clss + length tptp_clss)
    1.42    end;
    1.43  
    1.44 @@ -492,17 +499,17 @@
    1.45          string_of_descrip probname ::
    1.46          string_of_symbols (string_of_funcs funcs)
    1.47            (string_of_preds (cl_preds @ ty_preds)) ::
    1.48 -        "list_of_clauses(axioms,cnf).\n" ::
    1.49 +        "list_of_clauses(axioms, cnf).\n" ::
    1.50          axstrs @
    1.51          map dfg_classrel_clause classrel_clauses @
    1.52          map dfg_arity_clause arity_clauses @
    1.53          helper_clauses_strs @
    1.54 -        ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
    1.55 +        ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
    1.56          tfree_clss @
    1.57          dfg_clss @
    1.58          ["end_of_list.\n\n",
    1.59          (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
    1.60 -         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
    1.61 +         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
    1.62           "end_problem.\n"])
    1.63  
    1.64      in (length axclauses + length classrel_clauses + length arity_clauses +