src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 47512 b381d428a725
child 47516 9c29589c9b31
     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