# HG changeset patch # User sultana # Date 1335180203 -3600 # Node ID bfbd2d0bb34856fb47e306ea2e539703505b581d # Parent ba064cc165df9608914b4809ff20b9655e9793e8 moved function for testing problem-name parsing; list of TPTP test files not immediately evaluated; diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Parser_Example.thy --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Mon Apr 23 12:23:23 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Mon Apr 23 12:23:23 2012 +0100 @@ -9,7 +9,7 @@ uses "~~/src/HOL/ex/sledgehammer_tactics.ML" begin -import_tptp "$TPTP/Problems/ALG/ALG001^5.p" +import_tptp "$TPTP/Problems/CSR/CSR077+1.p" ML {* val an_fmlas = diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Parser_Test.thy --- a/src/HOL/TPTP/TPTP_Parser_Test.thy Mon Apr 23 12:23:23 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Mon Apr 23 12:23:23 2012 +0100 @@ -44,6 +44,14 @@ val _ = map (fn (str, res) => @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests end + +(*test against all TPTP problems*) +fun problem_names () = + map (Path.base #> + Path.implode #> + TPTP_Problem_Name.parse_problem_name #> + TPTP_Problem_Name.mangle_problem_name) + (test_files ()) *} diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Test.thy --- a/src/HOL/TPTP/TPTP_Test.thy Mon Apr 23 12:23:23 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Test.thy Mon Apr 23 12:23:23 2012 +0100 @@ -35,15 +35,7 @@ |> Path.expand; (*list of files to under test*) - val files = TPTP_Syntax.get_file_list tptp_probs_dir; - -(* (*test problem-name parsing and mangling*) - val problem_names = - map (Path.base #> - Path.implode #> - TPTP_Problem_Name.parse_problem_name #> - TPTP_Problem_Name.mangle_problem_name) - files*) + fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir; *} @@ -82,7 +74,7 @@ let fun f' x = (f x; ()) val time = - Timing.timing (List.app f') files + Timing.timing (List.app f') (test_files ()) |> fst val duration = #elapsed time @@ -90,7 +82,7 @@ |> Real.fromLargeInt val average = (StringCvt.FIX (SOME 3), - (duration / Real.fromInt (length files))) + (duration / Real.fromInt (length (test_files ())))) |-> Real.fmt in report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^