src/HOL/TPTP/TPTP_Parser_Test.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 65999 ee4cf96a9406
permissions -rw-r--r--
tuned proofs;
sultana@46844
     1
(*  Title:      HOL/TPTP/TPTP_Parser_Test.thy
sultana@46844
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@46844
     3
sultana@46844
     4
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
blanchet@47558
     5
environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
sultana@46844
     6
*)
sultana@46844
     7
sultana@46844
     8
theory TPTP_Parser_Test
sultana@47518
     9
imports TPTP_Test TPTP_Parser_Example
sultana@46844
    10
begin
sultana@46844
    11
sultana@47528
    12
section "Problem-name parsing tests"
wenzelm@63167
    13
ML \<open>
sultana@47528
    14
local
sultana@47528
    15
  open TPTP_Syntax;
sultana@47528
    16
  open TPTP_Problem_Name;
sultana@47528
    17
sultana@47528
    18
  val name_tests =
sultana@47528
    19
    [("HWV041_4.p",
sultana@47528
    20
        Standard {suffix = Problem ((4, NONE), "p"), prob_form = TFF, prob_domain = "HWV", prob_number = 41}),
sultana@47528
    21
     ("LCL617^1.p",
sultana@47528
    22
        Standard {suffix = Problem ((1, NONE), "p"), prob_form = THF, prob_domain = "LCL", prob_number = 617}),
sultana@47528
    23
     ("LCL831-1.p",
sultana@47528
    24
        Standard {suffix = Problem ((1, NONE), "p"), prob_form = CNF, prob_domain = "LCL", prob_number = 831}),
sultana@47528
    25
     ("HWV045=1.p",
sultana@47528
    26
        Standard {suffix = Problem ((1, NONE), "p"), prob_form = TFF_with_arithmetic, prob_domain = "HWV", prob_number = 45}),
sultana@47528
    27
     ("LCL655+1.010.p",
sultana@47528
    28
        Standard {suffix = Problem ((1, SOME 10), "p"), prob_form = FOF, prob_domain = "LCL", prob_number = 655}),
sultana@47528
    29
     ("OTH123.p",
sultana@47528
    30
        Nonstandard "OTH123.p"),
sultana@47528
    31
     ("other",
sultana@47528
    32
        Nonstandard "other"),
sultana@47528
    33
     ("AAA000£0.axiom",
sultana@47528
    34
        Nonstandard "AAA000£0.axiom"),
sultana@47528
    35
     ("AAA000£0.p",
sultana@47528
    36
        Nonstandard "AAA000£0.p"),
sultana@47528
    37
     ("AAA000.0.p",
sultana@47528
    38
        Nonstandard "AAA000.0.p"),
sultana@47528
    39
     ("AAA000£0.what",
sultana@47528
    40
        Nonstandard "AAA000£0.what"),
sultana@47528
    41
     ("",
sultana@47528
    42
        Nonstandard "")];
sultana@47528
    43
in
sultana@47528
    44
  val _ = map (fn (str, res) =>
sultana@47528
    45
    @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
sultana@47528
    46
end
sultana@47687
    47
sultana@47687
    48
(*test against all TPTP problems*)
sultana@47687
    49
fun problem_names () =
sultana@47687
    50
    map (Path.base #>
sultana@47687
    51
         Path.implode #>
sultana@47687
    52
         TPTP_Problem_Name.parse_problem_name #>
sultana@47687
    53
         TPTP_Problem_Name.mangle_problem_name)
sultana@55595
    54
     (TPTP_Syntax.get_file_list tptp_probs_dir)
wenzelm@63167
    55
\<close>
sultana@47528
    56
sultana@47528
    57
sultana@46844
    58
section "Parser tests"
sultana@46844
    59
wenzelm@63167
    60
ML \<open>
sultana@46844
    61
  TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
sultana@46844
    62
  TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
sultana@46844
    63
  TPTP_Parser.parse_expression ""
sultana@46844
    64
   "thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y))))).";
sultana@46844
    65
  TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true)).";
sultana@46844
    66
  payloads_of it;
wenzelm@63167
    67
\<close>
wenzelm@63167
    68
ML \<open>
sultana@46844
    69
  TPTP_Parser.parse_expression "" "thf(bla, type, x : $o).";
sultana@46844
    70
  TPTP_Parser.parse_expression ""
sultana@46844
    71
   "fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A))).";
sultana@46844
    72
  TPTP_Parser.parse_expression ""
sultana@46844
    73
   "fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A)))))).";
wenzelm@63167
    74
\<close>
wenzelm@63167
    75
ML \<open>
sultana@46844
    76
  TPTP_Parser.parse_expression ""
sultana@46844
    77
  ("fof(dt_k4_waybel34,axiom,(" ^
sultana@46844
    78
    "! [A] :" ^
sultana@46844
    79
      "( ~ v1_xboole_0(A)" ^
sultana@46844
    80
     "=> ( ~ v3_struct_0(k4_waybel34(A))" ^
sultana@46844
    81
        "& v2_altcat_1(k4_waybel34(A))" ^
sultana@46844
    82
        "& v6_altcat_1(k4_waybel34(A))" ^
sultana@46844
    83
        "& v11_altcat_1(k4_waybel34(A))" ^
sultana@46844
    84
        "& v12_altcat_1(k4_waybel34(A))" ^
sultana@46844
    85
        "& v2_yellow21(k4_waybel34(A))" ^
sultana@46844
    86
        "& l2_altcat_1(k4_waybel34(A)) ) ) )).")
wenzelm@63167
    87
\<close>
sultana@46844
    88
wenzelm@63167
    89
ML \<open>
sultana@46844
    90
open TPTP_Syntax;
sultana@46844
    91
@{assert}
sultana@46844
    92
  ((TPTP_Parser.parse_expression ""
sultana@46844
    93
   "thf(x,axiom,^ [X] : ^ [Y] : f @ g)."
sultana@46844
    94
   |> payloads_of |> hd)
sultana@46844
    95
  =
sultana@46844
    96
  Fmla (Interpreted_ExtraLogic Apply,
sultana@46844
    97
   [Quant (Lambda, [("X", NONE)],
sultana@46844
    98
      Quant (Lambda, [("Y", NONE)],
sultana@46844
    99
       Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
sultana@46844
   100
    Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
sultana@46844
   101
)
wenzelm@63167
   102
\<close>
sultana@46844
   103
sultana@46844
   104
sultana@46844
   105
text "Parse a specific problem."
wenzelm@63167
   106
ML \<open>
sultana@46844
   107
  map TPTP_Parser.parse_file
blanchet@47558
   108
   ["$TPTP/Problems/FLD/FLD051-1.p",
blanchet@47558
   109
    "$TPTP/Problems/FLD/FLD005-3.p",
blanchet@47558
   110
    "$TPTP/Problems/SWV/SWV567-1.015.p",
blanchet@47558
   111
    "$TPTP/Problems/SWV/SWV546-1.010.p"]
wenzelm@63167
   112
\<close>
wenzelm@63167
   113
ML \<open>
sultana@46844
   114
  parser_test @{context} (situate "DAT/DAT001=1.p");
sultana@46844
   115
  parser_test @{context} (situate "ALG/ALG001^5.p");
sultana@46844
   116
  parser_test @{context} (situate "NUM/NUM021^1.p");
sultana@46844
   117
  parser_test @{context} (situate "SYN/SYN000^1.p")
wenzelm@63167
   118
\<close>
sultana@46844
   119
sultana@46844
   120
text "Run the parser over all problems."
wenzelm@63167
   121
ML \<open>
sultana@47518
   122
  if test_all @{context} then
sultana@47518
   123
    (report @{context} "Testing parser";
sultana@55595
   124
     S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
sultana@47518
   125
  else ()
wenzelm@63167
   126
\<close>
sultana@46844
   127
nipkow@62390
   128
end