1.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 23:22:40 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 23:22:40 2012 +0100
     1.3 @@ -10,6 +10,44 @@
     1.4  imports TPTP_Test TPTP_Parser_Example
     1.5  begin
     1.6  
     1.7 +section "Problem-name parsing tests"
     1.8 +ML {*
     1.9 +local
    1.10 +  open TPTP_Syntax;
    1.11 +  open TPTP_Problem_Name;
    1.12 +
    1.13 +  val name_tests =
    1.14 +    [("HWV041_4.p",
    1.15 +        Standard {suffix = Problem ((4, NONE), "p"), prob_form = TFF, prob_domain = "HWV", prob_number = 41}),
    1.16 +     ("LCL617^1.p",
    1.17 +        Standard {suffix = Problem ((1, NONE), "p"), prob_form = THF, prob_domain = "LCL", prob_number = 617}),
    1.18 +     ("LCL831-1.p",
    1.19 +        Standard {suffix = Problem ((1, NONE), "p"), prob_form = CNF, prob_domain = "LCL", prob_number = 831}),
    1.20 +     ("HWV045=1.p",
    1.21 +        Standard {suffix = Problem ((1, NONE), "p"), prob_form = TFF_with_arithmetic, prob_domain = "HWV", prob_number = 45}),
    1.22 +     ("LCL655+1.010.p",
    1.23 +        Standard {suffix = Problem ((1, SOME 10), "p"), prob_form = FOF, prob_domain = "LCL", prob_number = 655}),
    1.24 +     ("OTH123.p",
    1.25 +        Nonstandard "OTH123.p"),
    1.26 +     ("other",
    1.27 +        Nonstandard "other"),
    1.28 +     ("AAA000£0.axiom",
    1.29 +        Nonstandard "AAA000£0.axiom"),
    1.30 +     ("AAA000£0.p",
    1.31 +        Nonstandard "AAA000£0.p"),
    1.32 +     ("AAA000.0.p",
    1.33 +        Nonstandard "AAA000.0.p"),
    1.34 +     ("AAA000£0.what",
    1.35 +        Nonstandard "AAA000£0.what"),
    1.36 +     ("",
    1.37 +        Nonstandard "")];
    1.38 +in
    1.39 +  val _ = map (fn (str, res) =>
    1.40 +    @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
    1.41 +end
    1.42 +*}
    1.43 +
    1.44 +
    1.45  section "Parser tests"
    1.46  
    1.47  ML {*