src/HOL/TPTP/TPTP_Parser_Test.thy
changeset 63167 0909deb8059b
parent 62390 842917225d56
child 65999 ee4cf96a9406
     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  begin
     1.5  
     1.6  section "Problem-name parsing tests"
     1.7 -ML {*
     1.8 +ML \<open>
     1.9  local
    1.10    open TPTP_Syntax;
    1.11    open TPTP_Problem_Name;
    1.12 @@ -52,27 +52,27 @@
    1.13           TPTP_Problem_Name.parse_problem_name #>
    1.14           TPTP_Problem_Name.mangle_problem_name)
    1.15       (TPTP_Syntax.get_file_list tptp_probs_dir)
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  
    1.20  section "Parser tests"
    1.21  
    1.22 -ML {*
    1.23 +ML \<open>
    1.24    TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
    1.25    TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
    1.26    TPTP_Parser.parse_expression ""
    1.27     "thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y))))).";
    1.28    TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true)).";
    1.29    payloads_of it;
    1.30 -*}
    1.31 -ML {*
    1.32 +\<close>
    1.33 +ML \<open>
    1.34    TPTP_Parser.parse_expression "" "thf(bla, type, x : $o).";
    1.35    TPTP_Parser.parse_expression ""
    1.36     "fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A))).";
    1.37    TPTP_Parser.parse_expression ""
    1.38     "fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A)))))).";
    1.39 -*}
    1.40 -ML {*
    1.41 +\<close>
    1.42 +ML \<open>
    1.43    TPTP_Parser.parse_expression ""
    1.44    ("fof(dt_k4_waybel34,axiom,(" ^
    1.45      "! [A] :" ^
    1.46 @@ -84,9 +84,9 @@
    1.47          "& v12_altcat_1(k4_waybel34(A))" ^
    1.48          "& v2_yellow21(k4_waybel34(A))" ^
    1.49          "& l2_altcat_1(k4_waybel34(A)) ) ) )).")
    1.50 -*}
    1.51 +\<close>
    1.52  
    1.53 -ML {*
    1.54 +ML \<open>
    1.55  open TPTP_Syntax;
    1.56  @{assert}
    1.57    ((TPTP_Parser.parse_expression ""
    1.58 @@ -99,30 +99,30 @@
    1.59         Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
    1.60      Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
    1.61  )
    1.62 -*}
    1.63 +\<close>
    1.64  
    1.65  
    1.66  text "Parse a specific problem."
    1.67 -ML {*
    1.68 +ML \<open>
    1.69    map TPTP_Parser.parse_file
    1.70     ["$TPTP/Problems/FLD/FLD051-1.p",
    1.71      "$TPTP/Problems/FLD/FLD005-3.p",
    1.72      "$TPTP/Problems/SWV/SWV567-1.015.p",
    1.73      "$TPTP/Problems/SWV/SWV546-1.010.p"]
    1.74 -*}
    1.75 -ML {*
    1.76 +\<close>
    1.77 +ML \<open>
    1.78    parser_test @{context} (situate "DAT/DAT001=1.p");
    1.79    parser_test @{context} (situate "ALG/ALG001^5.p");
    1.80    parser_test @{context} (situate "NUM/NUM021^1.p");
    1.81    parser_test @{context} (situate "SYN/SYN000^1.p")
    1.82 -*}
    1.83 +\<close>
    1.84  
    1.85  text "Run the parser over all problems."
    1.86 -ML {*
    1.87 +ML \<open>
    1.88    if test_all @{context} then
    1.89      (report @{context} "Testing parser";
    1.90       S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
    1.91    else ()
    1.92 -*}
    1.93 +\<close>
    1.94  
    1.95  end