src/HOL/TPTP/TPTP_Test.thy
changeset 47687 bfbd2d0bb348
parent 47558 55b42f9af99d
child 55595 2e2e9bc7c4c6
equal deleted inserted replaced
47686:ba064cc165df 47687:bfbd2d0bb348
    33   val tptp_probs_dir =
    33   val tptp_probs_dir =
    34     Path.explode "$TPTP/Problems"
    34     Path.explode "$TPTP/Problems"
    35     |> Path.expand;
    35     |> Path.expand;
    36 
    36 
    37   (*list of files to under test*)
    37   (*list of files to under test*)
    38   val files = TPTP_Syntax.get_file_list tptp_probs_dir;
    38   fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
    39 
       
    40 (*  (*test problem-name parsing and mangling*)
       
    41   val problem_names =
       
    42     map (Path.base #>
       
    43          Path.implode #>
       
    44          TPTP_Problem_Name.parse_problem_name #>
       
    45          TPTP_Problem_Name.mangle_problem_name)
       
    46         files*)
       
    47 *}
    39 *}
    48 
    40 
    49 
    41 
    50 section "Supporting test functions"
    42 section "Supporting test functions"
    51 ML {*
    43 ML {*
    80 
    72 
    81   fun timed_test ctxt f =
    73   fun timed_test ctxt f =
    82     let
    74     let
    83       fun f' x = (f x; ())
    75       fun f' x = (f x; ())
    84       val time =
    76       val time =
    85         Timing.timing (List.app f') files
    77         Timing.timing (List.app f') (test_files ())
    86         |> fst
    78         |> fst
    87       val duration =
    79       val duration =
    88         #elapsed time
    80         #elapsed time
    89         |> Time.toSeconds
    81         |> Time.toSeconds
    90         |> Real.fromLargeInt
    82         |> Real.fromLargeInt
    91       val average =
    83       val average =
    92         (StringCvt.FIX (SOME 3),
    84         (StringCvt.FIX (SOME 3),
    93          (duration / Real.fromInt (length files)))
    85          (duration / Real.fromInt (length (test_files ()))))
    94         |-> Real.fmt
    86         |-> Real.fmt
    95     in
    87     in
    96       report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    88       report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    97        "s per problem)")
    89        "s per problem)")
    98     end
    90     end