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