reorganised tptp testing thys
authorsultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47512b381d428a725
parent 47511 016ce79deb01
child 47513 50a424b89952
reorganised tptp testing thys
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Parser_Test.thy
src/HOL/TPTP/TPTP_Test.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -0,0 +1,128 @@
     1.4 +(*  Title:      HOL/TPTP/TPTP_Interpret_Test.thy
     1.5 +    Author:     Nik Sultana, Cambridge University Computer Laboratory
     1.6 +
     1.7 +Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     1.8 +environment variable TPTP_PROBLEMS_PATH, which should point to the
     1.9 +TPTP-vX.Y.Z/Problems directory.
    1.10 +*)
    1.11 +
    1.12 +theory TPTP_Interpret_Test
    1.13 +imports TPTP_Test TPTP_Interpret
    1.14 +begin
    1.15 +
    1.16 +section "Interpreter tests"
    1.17 +
    1.18 +text "Interpret a problem."
    1.19 +ML {*
    1.20 +  val (time, ((type_map, const_map, fmlas), thy)) =
    1.21 +    Timing.timing
    1.22 +      (TPTP_Interpret.interpret_file
    1.23 +       false
    1.24 +       (Path.dir tptp_probs_dir)
    1.25 +      (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
    1.26 +       []
    1.27 +       [])
    1.28 +      @{theory}
    1.29 +*}
    1.30 +
    1.31 +text "... and display nicely."
    1.32 +ML {*
    1.33 +  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
    1.34 +*}
    1.35 +ML {*
    1.36 +  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    1.37 +  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    1.38 +*}
    1.39 +
    1.40 +
    1.41 +subsection "Multiple tests"
    1.42 +
    1.43 +ML {*
    1.44 +  fun interpretation_test timeout ctxt =
    1.45 +    test_fn ctxt
    1.46 +     (fn file =>
    1.47 +       TimeLimit.timeLimit (Time.fromSeconds timeout)
    1.48 +        (TPTP_Interpret.interpret_file
    1.49 +          false
    1.50 +          (Path.dir tptp_probs_dir)
    1.51 +          file
    1.52 +          []
    1.53 +          [])
    1.54 +          @{theory})
    1.55 +     "interpreter"
    1.56 +     ()
    1.57 +
    1.58 +  fun interpretation_tests timeout ctxt probs =
    1.59 +    List.app
    1.60 +     (interpretation_test timeout ctxt)
    1.61 +     (List.map situate probs)
    1.62 +*}
    1.63 +
    1.64 +ML {*
    1.65 +  val some_probs =
    1.66 +    ["LCL/LCL825-1.p",
    1.67 +     "ALG/ALG001^5.p",
    1.68 +     "COM/COM003+2.p",
    1.69 +     "COM/COM003-1.p",
    1.70 +     "COM/COM024^5.p",
    1.71 +     "DAT/DAT017=1.p",
    1.72 +     "NUM/NUM021^1.p",
    1.73 +     "NUM/NUM858=1.p",
    1.74 +     "SYN/SYN000^2.p"]
    1.75 +
    1.76 +  val take_too_long =
    1.77 +    ["NLP/NLP562+1.p",
    1.78 +     "SWV/SWV546-1.010.p",
    1.79 +     "SWV/SWV567-1.015.p",
    1.80 +     "LCL/LCL680+1.020.p"]
    1.81 +
    1.82 +  val more_probs =
    1.83 +    ["GEG/GEG014^1.p",
    1.84 +     "GEG/GEG009^1.p",
    1.85 +     "GEG/GEG004^1.p",
    1.86 +     "GEG/GEG007^1.p",
    1.87 +     "GEG/GEG016^1.p",
    1.88 +     "GEG/GEG024=1.p",
    1.89 +     "GEG/GEG010^1.p",
    1.90 +     "GEG/GEG003^1.p",
    1.91 +     "GEG/GEG018^1.p",
    1.92 +     "SYN/SYN045^4.p",
    1.93 +     "SYN/SYN001^4.001.p",
    1.94 +     "SYN/SYN000^2.p",
    1.95 +     "SYN/SYN387^4.p",
    1.96 +     "SYN/SYN393^4.002.p",
    1.97 +     "SYN/SYN978^4.p",
    1.98 +     "SYN/SYN044^4.p",
    1.99 +     "SYN/SYN393^4.003.p",
   1.100 +     "SYN/SYN389^4.p"]
   1.101 +*}
   1.102 +
   1.103 +ML {*
   1.104 + interpretation_tests 5 @{context}
   1.105 +   (some_probs @ take_too_long @ more_probs)
   1.106 +*}
   1.107 +
   1.108 +
   1.109 +subsection "Test against whole TPTP"
   1.110 +
   1.111 +text "Run interpretation over all problems. This works only for logics
   1.112 + for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
   1.113 +ML {*
   1.114 +  report @{context} "Interpreting all problems.";
   1.115 +  fun interpretation_test timeout ctxt =
   1.116 +    test_fn ctxt
   1.117 +     (fn file =>
   1.118 +       TimeLimit.timeLimit (Time.fromSeconds timeout)
   1.119 +        (TPTP_Interpret.interpret_file
   1.120 +          false
   1.121 +          (Path.dir tptp_probs_dir)
   1.122 +          file
   1.123 +          []
   1.124 +          [])
   1.125 +          @{theory})
   1.126 +     "interpreter"
   1.127 +     ()
   1.128 +  (*val _ = S timed_test (interpretation_test 5) @{context}*)
   1.129 +*}
   1.130 +
   1.131 +end
   1.132 \ No newline at end of file
     2.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     2.3 @@ -7,21 +7,12 @@
     2.4  *)
     2.5  
     2.6  theory TPTP_Parser_Test
     2.7 -imports TPTP_Parser TPTP_Parser_Example
     2.8 +imports TPTP_Test (*TPTP_Parser_Example*)
     2.9  begin
    2.10  
    2.11 -ML {*
    2.12 -  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
    2.13 -  fun S x y z = x z (y z)
    2.14 -*}
    2.15 -
    2.16  section "Parser tests"
    2.17  
    2.18  ML {*
    2.19 -  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
    2.20 -  val payloads_of = map payload_of
    2.21 -*}
    2.22 -ML {*
    2.23    TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
    2.24    TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
    2.25    TPTP_Parser.parse_expression ""
    2.26 @@ -66,94 +57,6 @@
    2.27  *}
    2.28  
    2.29  
    2.30 -section "Source problems"
    2.31 -ML {*
    2.32 -  (*problem source*)
    2.33 -  val tptp_probs_dir =
    2.34 -    Path.explode "$TPTP_PROBLEMS_PATH"
    2.35 -    |> Path.expand;
    2.36 -
    2.37 -  (*list of files to under test*)
    2.38 -  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
    2.39 -
    2.40 -(*  (*test problem-name parsing and mangling*)
    2.41 -  val problem_names =
    2.42 -    map (Path.base #>
    2.43 -         Path.implode #>
    2.44 -         TPTP_Problem_Name.parse_problem_name #>
    2.45 -         TPTP_Problem_Name.mangle_problem_name)
    2.46 -        files*)
    2.47 -*}
    2.48 -
    2.49 -
    2.50 -section "Supporting test functions"
    2.51 -ML {*
    2.52 -  fun report ctxt str =
    2.53 -    let
    2.54 -      val warning_out = Config.get ctxt warning_out
    2.55 -    in
    2.56 -      if warning_out = "" then warning str
    2.57 -      else
    2.58 -        let
    2.59 -          val out_stream = TextIO.openAppend warning_out
    2.60 -        in (TextIO.output (out_stream, str ^ "\n");
    2.61 -            TextIO.flushOut out_stream;
    2.62 -            TextIO.closeOut out_stream)
    2.63 -        end
    2.64 -    end
    2.65 -
    2.66 -  fun test_fn ctxt f msg default_val file_name =
    2.67 -    let
    2.68 -      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
    2.69 -    in
    2.70 -     (f file_name; ())
    2.71 -     (*otherwise report exceptions as warnings*)
    2.72 -     handle exn =>
    2.73 -       if Exn.is_interrupt exn then
    2.74 -         reraise exn
    2.75 -       else
    2.76 -         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
    2.77 -          " raised exception: " ^ ML_Compiler.exn_message exn);
    2.78 -          default_val)
    2.79 -    end
    2.80 -
    2.81 -  fun timed_test ctxt f =
    2.82 -    let
    2.83 -      fun f' x = (f x; ())
    2.84 -      val time =
    2.85 -        Timing.timing (List.app f') files
    2.86 -        |> fst
    2.87 -      val duration =
    2.88 -        #elapsed time
    2.89 -        |> Time.toSeconds
    2.90 -        |> Real.fromLargeInt
    2.91 -      val average =
    2.92 -        (StringCvt.FIX (SOME 3),
    2.93 -         (duration / Real.fromInt (length files)))
    2.94 -        |-> Real.fmt
    2.95 -    in
    2.96 -      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    2.97 -       "s per problem)")
    2.98 -    end
    2.99 -*}
   2.100 -
   2.101 -
   2.102 -subsection "More parser tests"
   2.103 -ML {*
   2.104 -  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
   2.105 -  fun parser_test ctxt = (*FIXME argument order*)
   2.106 -    test_fn ctxt
   2.107 -     (fn file_name =>
   2.108 -        Path.implode file_name
   2.109 -        |> (fn file =>
   2.110 -             ((*report ctxt file; this is if you want the filename in the log*)
   2.111 -              TPTP_Parser.parse_file file)))
   2.112 -     "parser"
   2.113 -     ()
   2.114 -*}
   2.115 -
   2.116 -declare [[warning_out = ""]]
   2.117 -
   2.118  text "Parse a specific problem."
   2.119  ML {*
   2.120    map TPTP_Parser.parse_file
   2.121 @@ -176,66 +79,4 @@
   2.122  *}
   2.123  
   2.124  
   2.125 -subsection "Interpretation"
   2.126 -
   2.127 -text "Interpret a problem."
   2.128 -ML {*
   2.129 -  val (time, ((type_map, const_map, fmlas), thy)) =
   2.130 -    Timing.timing
   2.131 -    (TPTP_Interpret.interpret_file
   2.132 -     false
   2.133 -     (Path.dir tptp_probs_dir)
   2.134 -    (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
   2.135 -     []
   2.136 -     [])
   2.137 -    @{theory}
   2.138 -
   2.139 -  (*also tried
   2.140 -     "ALG/ALG001^5.p"
   2.141 -     "COM/COM003+2.p"
   2.142 -     "COM/COM003-1.p"
   2.143 -     "COM/COM024^5.p"
   2.144 -     "DAT/DAT017=1.p"
   2.145 -     "NUM/NUM021^1.p"
   2.146 -     "NUM/NUM858=1.p"
   2.147 -     "SYN/SYN000^2.p"*)
   2.148 -
   2.149 - (*These take too long
   2.150 -    "NLP/NLP562+1.p"
   2.151 -    "SWV/SWV546-1.010.p"
   2.152 -    "SWV/SWV567-1.015.p"
   2.153 -    "LCL/LCL680+1.020.p"*)
   2.154 -*}
   2.155 -
   2.156 -text "... and display nicely."
   2.157 -ML {*
   2.158 -  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
   2.159 -*}
   2.160 -ML {*
   2.161 -  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
   2.162 -  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
   2.163 -*}
   2.164 -
   2.165 -
   2.166 -text "Run interpretation over all problems. This works only for logics
   2.167 - for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
   2.168 -ML {*
   2.169 -  report @{context} "Interpreting all problems.";
   2.170 -  fun interpretation_test timeout ctxt =
   2.171 -    test_fn ctxt
   2.172 -     (fn file =>
   2.173 -      (writeln (Path.implode file);
   2.174 -       TimeLimit.timeLimit (Time.fromSeconds timeout)
   2.175 -       (TPTP_Interpret.interpret_file
   2.176 -         false
   2.177 -         (Path.dir tptp_probs_dir)
   2.178 -         file
   2.179 -         []
   2.180 -         [])
   2.181 -         @{theory}))
   2.182 -     "interpreter"
   2.183 -     ()
   2.184 -  val _ = S timed_test (interpretation_test 5) @{context}
   2.185 -*}
   2.186 -
   2.187  end
   2.188 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     3.3 @@ -0,0 +1,113 @@
     3.4 +(*  Title:      HOL/TPTP/TPTP_Test.thy
     3.5 +5A    Author:     Nik Sultana, Cambridge University Computer Laboratory
     3.6 +
     3.7 +Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     3.8 +environment variable TPTP_PROBLEMS_PATH, which should point to the
     3.9 +TPTP-vX.Y.Z/Problems directory.
    3.10 +*)
    3.11 +
    3.12 +theory TPTP_Test
    3.13 +imports TPTP_Parser
    3.14 +begin
    3.15 +
    3.16 +ML {*
    3.17 +  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
    3.18 +  fun S x y z = x z (y z)
    3.19 +*}
    3.20 +
    3.21 +section "Parser tests"
    3.22 +
    3.23 +ML {*
    3.24 +  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
    3.25 +  val payloads_of = map payload_of
    3.26 +*}
    3.27 +
    3.28 +
    3.29 +section "Source problems"
    3.30 +ML {*
    3.31 +  (*problem source*)
    3.32 +  val tptp_probs_dir =
    3.33 +    Path.explode "$TPTP_PROBLEMS_PATH"
    3.34 +    |> Path.expand;
    3.35 +
    3.36 +  (*list of files to under test*)
    3.37 +  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
    3.38 +
    3.39 +(*  (*test problem-name parsing and mangling*)
    3.40 +  val problem_names =
    3.41 +    map (Path.base #>
    3.42 +         Path.implode #>
    3.43 +         TPTP_Problem_Name.parse_problem_name #>
    3.44 +         TPTP_Problem_Name.mangle_problem_name)
    3.45 +        files*)
    3.46 +*}
    3.47 +
    3.48 +
    3.49 +section "Supporting test functions"
    3.50 +ML {*
    3.51 +  fun report ctxt str =
    3.52 +    let
    3.53 +      val warning_out = Config.get ctxt warning_out
    3.54 +    in
    3.55 +      if warning_out = "" then warning str
    3.56 +      else
    3.57 +        let
    3.58 +          val out_stream = TextIO.openAppend warning_out
    3.59 +        in (TextIO.output (out_stream, str ^ "\n");
    3.60 +            TextIO.flushOut out_stream;
    3.61 +            TextIO.closeOut out_stream)
    3.62 +        end
    3.63 +    end
    3.64 +
    3.65 +  fun test_fn ctxt f msg default_val file_name =
    3.66 +    let
    3.67 +      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
    3.68 +    in
    3.69 +     (f file_name; ())
    3.70 +     (*otherwise report exceptions as warnings*)
    3.71 +     handle exn =>
    3.72 +       if Exn.is_interrupt exn then
    3.73 +         reraise exn
    3.74 +       else
    3.75 +         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
    3.76 +          " raised exception: " ^ ML_Compiler.exn_message exn);
    3.77 +          default_val)
    3.78 +    end
    3.79 +
    3.80 +  fun timed_test ctxt f =
    3.81 +    let
    3.82 +      fun f' x = (f x; ())
    3.83 +      val time =
    3.84 +        Timing.timing (List.app f') files
    3.85 +        |> fst
    3.86 +      val duration =
    3.87 +        #elapsed time
    3.88 +        |> Time.toSeconds
    3.89 +        |> Real.fromLargeInt
    3.90 +      val average =
    3.91 +        (StringCvt.FIX (SOME 3),
    3.92 +         (duration / Real.fromInt (length files)))
    3.93 +        |-> Real.fmt
    3.94 +    in
    3.95 +      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    3.96 +       "s per problem)")
    3.97 +    end
    3.98 +*}
    3.99 +
   3.100 +
   3.101 +ML {*
   3.102 +  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
   3.103 +  fun parser_test ctxt = (*FIXME argument order*)
   3.104 +    test_fn ctxt
   3.105 +     (fn file_name =>
   3.106 +        Path.implode file_name
   3.107 +        |> (fn file =>
   3.108 +             ((*report ctxt file; this is if you want the filename in the log*)
   3.109 +              TPTP_Parser.parse_file file)))
   3.110 +     "parser"
   3.111 +     ()
   3.112 +*}
   3.113 +
   3.114 +declare [[warning_out = ""]]
   3.115 +
   3.116 +end
   3.117 \ No newline at end of file