made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;
authorsultana
Wed Feb 19 15:57:02 2014 +0000 (2014-02-19)
changeset 555952e2e9bc7c4c6
parent 55594 eb291b215c73
child 55596 928b9f677165
made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Parser_Test.thy
src/HOL/TPTP/TPTP_Test.thy
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     1.3 @@ -154,7 +154,7 @@
     1.4  ML {*
     1.5    if test_all @{context} then
     1.6      (report @{context} "Interpreting all problems";
     1.7 -     S timed_test (interpretation_test (get_timeout @{context})) @{context})
     1.8 +     S timed_test (interpretation_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
     1.9    else ()
    1.10  *}
    1.11  
     2.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     2.3 @@ -51,7 +51,7 @@
     2.4           Path.implode #>
     2.5           TPTP_Problem_Name.parse_problem_name #>
     2.6           TPTP_Problem_Name.mangle_problem_name)
     2.7 -        (test_files ())
     2.8 +     (TPTP_Syntax.get_file_list tptp_probs_dir)
     2.9  *}
    2.10  
    2.11  
    2.12 @@ -121,7 +121,7 @@
    2.13  ML {*
    2.14    if test_all @{context} then
    2.15      (report @{context} "Testing parser";
    2.16 -     S timed_test parser_test @{context})
    2.17 +     S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
    2.18    else ()
    2.19  *}
    2.20  
     3.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     3.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
     3.3 @@ -33,9 +33,6 @@
     3.4    val tptp_probs_dir =
     3.5      Path.explode "$TPTP/Problems"
     3.6      |> Path.expand;
     3.7 -
     3.8 -  (*list of files to under test*)
     3.9 -  fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
    3.10  *}
    3.11  
    3.12  
    3.13 @@ -70,11 +67,11 @@
    3.14            default_val)
    3.15      end
    3.16  
    3.17 -  fun timed_test ctxt f =
    3.18 +  fun timed_test ctxt f test_files =
    3.19      let
    3.20        fun f' x = (f x; ())
    3.21        val time =
    3.22 -        Timing.timing (List.app f') (test_files ())
    3.23 +        Timing.timing (List.app f') test_files
    3.24          |> fst
    3.25        val duration =
    3.26          #elapsed time
    3.27 @@ -82,7 +79,7 @@
    3.28          |> Real.fromLargeInt
    3.29        val average =
    3.30          (StringCvt.FIX (SOME 3),
    3.31 -         (duration / Real.fromInt (length (test_files ()))))
    3.32 +         (duration / Real.fromInt (length test_files)))
    3.33          |-> Real.fmt
    3.34      in
    3.35        report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^