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