src/HOL/TPTP/TPTP_Parser_Test.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47367 97097a58335d
child 47512 b381d428a725
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/TPTP_Parser_Test.thy
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
environment variable TPTP_PROBLEMS_PATH, which should point to the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     6
TPTP-vX.Y.Z/Problems directory.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     7
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
theory TPTP_Parser_Test
47366
f5a304ca037e improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
sultana
parents: 46844
diff changeset
    10
imports TPTP_Parser TPTP_Parser_Example
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
begin
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
  fun S x y z = x z (y z)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    16
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    17
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    18
section "Parser tests"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    19
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
  val payloads_of = map payload_of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    24
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    25
  TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    26
  TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
  TPTP_Parser.parse_expression ""
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
   "thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y))))).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
  TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true)).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    30
  payloads_of it;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
  TPTP_Parser.parse_expression "" "thf(bla, type, x : $o).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
  TPTP_Parser.parse_expression ""
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
   "fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A))).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
  TPTP_Parser.parse_expression ""
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
   "fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A)))))).";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
  TPTP_Parser.parse_expression ""
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
  ("fof(dt_k4_waybel34,axiom,(" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    42
    "! [A] :" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
      "( ~ v1_xboole_0(A)" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
     "=> ( ~ v3_struct_0(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
        "& v2_altcat_1(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    46
        "& v6_altcat_1(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    47
        "& v11_altcat_1(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
        "& v12_altcat_1(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
        "& v2_yellow21(k4_waybel34(A))" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
        "& l2_altcat_1(k4_waybel34(A)) ) ) )).")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
open TPTP_Syntax;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    55
@{assert}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    56
  ((TPTP_Parser.parse_expression ""
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    57
   "thf(x,axiom,^ [X] : ^ [Y] : f @ g)."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    58
   |> payloads_of |> hd)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    59
  =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    60
  Fmla (Interpreted_ExtraLogic Apply,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    61
   [Quant (Lambda, [("X", NONE)],
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    62
      Quant (Lambda, [("Y", NONE)],
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    63
       Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    64
    Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    65
)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
section "Source problems"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    71
  (*problem source*)
47367
sultana
parents: 47366
diff changeset
    72
  val tptp_probs_dir =
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    73
    Path.explode "$TPTP_PROBLEMS_PATH"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    74
    |> Path.expand;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    75
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
  (*list of files to under test*)
47367
sultana
parents: 47366
diff changeset
    77
  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
(*  (*test problem-name parsing and mangling*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
  val problem_names =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
    map (Path.base #>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
         Path.implode #>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    83
         TPTP_Problem_Name.parse_problem_name #>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
         TPTP_Problem_Name.mangle_problem_name)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    85
        files*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    86
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    87
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    88
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
section "Supporting test functions"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    90
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
  fun report ctxt str =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
    let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
      val warning_out = Config.get ctxt warning_out
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
    in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
      if warning_out = "" then warning str
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
      else
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
        let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
          val out_stream = TextIO.openAppend warning_out
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    99
        in (TextIO.output (out_stream, str ^ "\n");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   100
            TextIO.flushOut out_stream;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   101
            TextIO.closeOut out_stream)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   102
        end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   103
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
  fun test_fn ctxt f msg default_val file_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
    let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
    in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
     (f file_name; ())
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
     (*otherwise report exceptions as warnings*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
     handle exn =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
       if Exn.is_interrupt exn then
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
         reraise exn
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
       else
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
          " raised exception: " ^ ML_Compiler.exn_message exn);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
          default_val)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
  fun timed_test ctxt f =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
    let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
      fun f' x = (f x; ())
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
      val time =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
        Timing.timing (List.app f') files
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
        |> fst
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
      val duration =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
        #elapsed time
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
        |> Time.toSeconds
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
        |> Real.fromLargeInt
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   130
      val average =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
        (StringCvt.FIX (SOME 3),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
         (duration / Real.fromInt (length files)))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
        |-> Real.fmt
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
    in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
       "s per problem)")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
subsection "More parser tests"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
ML {*
47367
sultana
parents: 47366
diff changeset
   143
  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
  fun parser_test ctxt = (*FIXME argument order*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
    test_fn ctxt
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
     (fn file_name =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
        Path.implode file_name
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
        |> (fn file =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
             ((*report ctxt file; this is if you want the filename in the log*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
              TPTP_Parser.parse_file file)))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   151
     "parser"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   152
     ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   153
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   154
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   155
declare [[warning_out = ""]]
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   156
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   157
text "Parse a specific problem."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   158
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   159
  map TPTP_Parser.parse_file
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   160
   ["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p",
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   161
    "$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p",
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   162
    "$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p",
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   163
    "$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"]
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   164
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   165
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   166
  parser_test @{context} (situate "DAT/DAT001=1.p");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   167
  parser_test @{context} (situate "ALG/ALG001^5.p");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   168
  parser_test @{context} (situate "NUM/NUM021^1.p");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   169
  parser_test @{context} (situate "SYN/SYN000^1.p")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   170
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   171
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   172
text "Run the parser over all problems."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   173
ML {*report @{context} "Testing parser"*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   174
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   175
(*  val _ = S timed_test parser_test @{context}*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   176
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   177
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   178
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   179
subsection "Interpretation"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   180
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   181
text "Interpret a problem."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   182
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   183
  val (time, ((type_map, const_map, fmlas), thy)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   184
    Timing.timing
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   185
    (TPTP_Interpret.interpret_file
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   186
     false
47367
sultana
parents: 47366
diff changeset
   187
     (Path.dir tptp_probs_dir)
sultana
parents: 47366
diff changeset
   188
    (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   189
     []
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   190
     [])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   191
    @{theory}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   192
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   193
  (*also tried
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   194
     "ALG/ALG001^5.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   195
     "COM/COM003+2.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   196
     "COM/COM003-1.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   197
     "COM/COM024^5.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   198
     "DAT/DAT017=1.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   199
     "NUM/NUM021^1.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   200
     "NUM/NUM858=1.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   201
     "SYN/SYN000^2.p"*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   202
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   203
 (*These take too long
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   204
    "NLP/NLP562+1.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   205
    "SWV/SWV546-1.010.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   206
    "SWV/SWV567-1.015.p"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   207
    "LCL/LCL680+1.020.p"*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   208
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   209
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   210
text "... and display nicely."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   211
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   212
  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   213
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   214
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   215
  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   216
  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   217
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   218
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   219
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   220
text "Run interpretation over all problems. This works only for logics
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   221
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   222
ML {*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   223
  report @{context} "Interpreting all problems.";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   224
  fun interpretation_test timeout ctxt =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   225
    test_fn ctxt
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   226
     (fn file =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   227
      (writeln (Path.implode file);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   228
       TimeLimit.timeLimit (Time.fromSeconds timeout)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   229
       (TPTP_Interpret.interpret_file
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   230
         false
47367
sultana
parents: 47366
diff changeset
   231
         (Path.dir tptp_probs_dir)
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   232
         file
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   233
         []
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   234
         [])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   235
         @{theory}))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   236
     "interpreter"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   237
     ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   238
  val _ = S timed_test (interpretation_test 5) @{context}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   239
*}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   240
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   241
end