# HG changeset patch
# User sultana
# Date 1334701360 -3600
# Node ID a8c2cb501614b2020cc9fb6e28ee075966b6faa4
# Parent  b0a7d235b23bbcb4c97f35a46121ecbdb018ed47
added testing of tptp problem names;

diff -r b0a7d235b23b -r a8c2cb501614 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 23:22:40 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 23:22:40 2012 +0100
@@ -10,6 +10,44 @@
 imports TPTP_Test TPTP_Parser_Example
 begin
 
+section "Problem-name parsing tests"
+ML {*
+local
+  open TPTP_Syntax;
+  open TPTP_Problem_Name;
+
+  val name_tests =
+    [("HWV041_4.p",
+        Standard {suffix = Problem ((4, NONE), "p"), prob_form = TFF, prob_domain = "HWV", prob_number = 41}),
+     ("LCL617^1.p",
+        Standard {suffix = Problem ((1, NONE), "p"), prob_form = THF, prob_domain = "LCL", prob_number = 617}),
+     ("LCL831-1.p",
+        Standard {suffix = Problem ((1, NONE), "p"), prob_form = CNF, prob_domain = "LCL", prob_number = 831}),
+     ("HWV045=1.p",
+        Standard {suffix = Problem ((1, NONE), "p"), prob_form = TFF_with_arithmetic, prob_domain = "HWV", prob_number = 45}),
+     ("LCL655+1.010.p",
+        Standard {suffix = Problem ((1, SOME 10), "p"), prob_form = FOF, prob_domain = "LCL", prob_number = 655}),
+     ("OTH123.p",
+        Nonstandard "OTH123.p"),
+     ("other",
+        Nonstandard "other"),
+     ("AAA000£0.axiom",
+        Nonstandard "AAA000£0.axiom"),
+     ("AAA000£0.p",
+        Nonstandard "AAA000£0.p"),
+     ("AAA000.0.p",
+        Nonstandard "AAA000.0.p"),
+     ("AAA000£0.what",
+        Nonstandard "AAA000£0.what"),
+     ("",
+        Nonstandard "")];
+in
+  val _ = map (fn (str, res) =>
+    @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
+end
+*}
+
+
 section "Parser tests"
 
 ML {*