src/HOL/Library/code_test.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65905 6181ccb4ec8c
child 66284 378895354604
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Library/code_test.ML
     2     Author:     Andreas Lochbihler, ETH Z├╝rich
     3 
     4 Test infrastructure for the code generator.
     5 *)
     6 
     7 signature CODE_TEST =
     8 sig
     9   val add_driver:
    10     string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
    11     theory -> theory
    12   val overlord: bool Config.T
    13   val successN: string
    14   val failureN: string
    15   val start_markerN: string
    16   val end_markerN: string
    17   val test_terms: Proof.context -> term list -> string -> unit
    18   val test_targets: Proof.context -> term list -> string list -> unit
    19   val test_code_cmd: string list -> string list -> Proof.context -> unit
    20   val eval_term: string -> Proof.context -> term -> term
    21   val evaluate:
    22    (theory -> Path.T -> string list -> string ->
    23      {files: (Path.T * string) list,
    24        compile_cmd: string option,
    25        run_cmd: string,
    26        mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory ->
    27      (string * string) list * string -> Path.T -> string
    28   val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
    29   val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
    30   val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
    31   val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
    32   val ghc_options: string Config.T
    33   val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
    34   val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
    35 end
    36 
    37 structure Code_Test: CODE_TEST =
    38 struct
    39 
    40 (* convert a list of terms into nested tuples and back *)
    41 
    42 fun mk_tuples [] = @{term "()"}
    43   | mk_tuples [t] = t
    44   | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
    45 
    46 fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r
    47   | dest_tuples t = [t]
    48 
    49 
    50 fun last_field sep str =
    51   let
    52     val n = size sep
    53     val len = size str
    54     fun find i =
    55       if i < 0 then NONE
    56       else if String.substring (str, i, n) = sep then SOME i
    57       else find (i - 1)
    58   in
    59     (case find (len - n) of
    60       NONE => NONE
    61     | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
    62   end
    63 
    64 fun split_first_last start stop s =
    65   (case first_field start s of
    66     NONE => NONE
    67   | SOME (initial, rest) =>
    68       (case last_field stop rest of
    69         NONE => NONE
    70       | SOME (middle, tail) => SOME (initial, middle, tail)))
    71 
    72 
    73 (* data slot for drivers *)
    74 
    75 structure Drivers = Theory_Data
    76 (
    77   type T =
    78     (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list
    79   val empty = []
    80   val extend = I
    81   fun merge data : T = AList.merge (op =) (K true) data
    82 )
    83 
    84 val add_driver = Drivers.map o AList.update (op =)
    85 val get_driver = AList.lookup (op =) o Drivers.get
    86 
    87 (*
    88   Test drivers must produce output of the following format:
    89 
    90   The start of the relevant data is marked with start_markerN,
    91   its end with end_markerN.
    92 
    93   Between these two markers, every line corresponds to one test.
    94   Lines of successful tests start with successN, failures start with failureN.
    95   The failure failureN may continue with the YXML encoding of the evaluated term.
    96   There must not be any additional whitespace in between.
    97 *)
    98 
    99 
   100 (* parsing of results *)
   101 
   102 val successN = "True"
   103 val failureN = "False"
   104 val start_markerN = "*@*Isabelle/Code_Test-start*@*"
   105 val end_markerN = "*@*Isabelle/Code_Test-end*@*"
   106 
   107 fun parse_line line =
   108   if String.isPrefix successN line then (true, NONE)
   109   else if String.isPrefix failureN line then (false,
   110     if size line > size failureN then
   111       String.extract (line, size failureN, NONE)
   112       |> YXML.parse_body
   113       |> Term_XML.Decode.term
   114       |> dest_tuples
   115       |> SOME
   116     else NONE)
   117   else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
   118 
   119 fun parse_result target out =
   120   (case split_first_last start_markerN end_markerN out of
   121     NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
   122   | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line)
   123 
   124 
   125 (* pretty printing of test results *)
   126 
   127 fun pretty_eval _ NONE _ = []
   128   | pretty_eval ctxt (SOME evals) ts =
   129       [Pretty.fbrk,
   130        Pretty.big_list "Evaluated terms"
   131          (map (fn (t, eval) => Pretty.block
   132            [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   133             Syntax.pretty_term ctxt eval])
   134          (ts ~~ evals))]
   135 
   136 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   137   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
   138     @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
   139     @ pretty_eval ctxt evals eval_ts)
   140 
   141 fun pretty_failures ctxt target failures =
   142   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   143 
   144 
   145 (* driver invocation *)
   146 
   147 val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false)
   148 
   149 fun with_overlord_dir name f =
   150   let
   151     val path =
   152       Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   153     val _ = Isabelle_System.mkdirs path
   154   in Exn.release (Exn.capture f path) end
   155 
   156 fun dynamic_value_strict ctxt t compiler =
   157   let
   158     val thy = Proof_Context.theory_of ctxt
   159     val (driver, target) =
   160       (case get_driver thy compiler of
   161         NONE => error ("No driver for target " ^ compiler)
   162       | SOME f => f)
   163     val debug = Config.get (Proof_Context.init_global thy) overlord
   164     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
   165     fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
   166     fun evaluator program _ vs_ty deps =
   167       Exn.interruptible_capture evaluate
   168         (Code_Target.compilation_text ctxt target program deps true vs_ty)
   169     fun postproc f = map (apsnd (Option.map (map f)))
   170   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
   171 
   172 
   173 (* term preprocessing *)
   174 
   175 fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
   176   | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
   177       acc
   178       |> add_eval rhs
   179       |> add_eval lhs
   180       |> cons rhs
   181       |> cons lhs)
   182   | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
   183   | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
   184       lhs :: rhs :: acc)
   185   | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
   186       lhs :: rhs :: acc)
   187   | add_eval _ = I
   188 
   189 fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
   190   | mk_term_of ts =
   191       let
   192         val tuple = mk_tuples ts
   193         val T = fastype_of tuple
   194       in
   195         @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
   196           (absdummy @{typ unit} (@{const yxml_string_of_term} $
   197             (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
   198       end
   199 
   200 fun test_terms ctxt ts target =
   201   let
   202     val thy = Proof_Context.theory_of ctxt
   203 
   204     fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
   205 
   206     fun ensure_bool t =
   207       (case fastype_of t of
   208         @{typ bool} => ()
   209       | _ =>
   210         error (Pretty.string_of
   211           (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
   212             Syntax.pretty_term ctxt t])))
   213 
   214     val _ = List.app ensure_bool ts
   215 
   216     val evals = map (fn t => filter term_of (add_eval t [])) ts
   217     val eval = map mk_term_of evals
   218 
   219     val t =
   220       HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
   221         (map HOLogic.mk_prod (ts ~~ eval))
   222 
   223     val result = dynamic_value_strict ctxt t target
   224 
   225     val failed =
   226       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
   227       handle ListPair.UnequalLengths =>
   228         error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
   229   in
   230     (case failed of [] =>
   231       ()
   232     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   233   end
   234 
   235 fun test_targets ctxt = List.app o test_terms ctxt
   236 
   237 fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
   238 
   239 fun test_code_cmd raw_ts targets ctxt =
   240   let
   241     val ts = Syntax.read_terms ctxt raw_ts
   242     val frees = fold Term.add_frees ts []
   243     val _ =
   244       if null frees then ()
   245       else error (Pretty.string_of
   246         (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
   247           Pretty.commas (map (pretty_free ctxt) frees))))
   248   in test_targets ctxt ts targets end
   249 
   250 fun eval_term target ctxt t =
   251   let
   252     val frees = Term.add_frees t []
   253     val _ =
   254       if null frees then ()
   255       else
   256         error (Pretty.string_of
   257           (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
   258             Pretty.commas (map (pretty_free ctxt) frees))))
   259 
   260     val T = fastype_of t
   261     val _ =
   262       if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort term_of}) then ()
   263       else error ("Type " ^ Syntax.string_of_typ ctxt T ^
   264        " of term not of sort " ^ Syntax.string_of_sort ctxt @{sort term_of})
   265 
   266     val t' =
   267       HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
   268         [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   269 
   270     val result = dynamic_value_strict ctxt t' target
   271   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
   272 
   273 
   274 (* generic driver *)
   275 
   276 fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) =
   277   let
   278     val _ =
   279       (case opt_env_var of
   280         NONE => ()
   281       | SOME (env_var, env_var_dest) =>
   282           (case getenv env_var of
   283             "" =>
   284               error (Pretty.string_of (Pretty.para
   285                 ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   286                   compilerN ^ ", set this variable to your " ^ env_var_dest ^
   287                   " in the $ISABELLE_HOME_USER/etc/settings file.")))
   288           | _ => ()))
   289 
   290     fun compile NONE = ()
   291       | compile (SOME cmd) =
   292           let
   293             val (out, ret) = Isabelle_System.bash_output cmd
   294           in
   295             if ret = 0 then ()
   296             else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   297           end
   298 
   299     fun run path =
   300       let
   301         val modules = map fst code_files
   302         val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
   303 
   304         val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
   305         val _ = List.app (fn (name, content) => File.write name content) files
   306 
   307         val _ = compile compile_cmd
   308 
   309         val (out, res) = Isabelle_System.bash_output run_cmd
   310         val _ =
   311           if res = 0 then ()
   312           else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
   313             Int.toString res ^ "\nBash output:\n" ^ out)
   314       in out end
   315   in run end
   316 
   317 
   318 (* driver for PolyML *)
   319 
   320 val polymlN = "PolyML"
   321 
   322 fun mk_driver_polyml _ path _ value_name =
   323   let
   324     val generatedN = "generated.sml"
   325     val driverN = "driver.sml"
   326 
   327     val code_path = Path.append path (Path.basic generatedN)
   328     val driver_path = Path.append path (Path.basic driverN)
   329     val driver =
   330       "fun main prog_name = \n" ^
   331       "  let\n" ^
   332       "    fun format_term NONE = \"\"\n" ^
   333       "      | format_term (SOME t) = t ();\n" ^
   334       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   335       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   336       "    val result = " ^ value_name ^ " ();\n" ^
   337       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   338       "    val _ = map (print o format) result;\n" ^
   339       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   340       "  in\n" ^
   341       "    ()\n" ^
   342       "  end;\n"
   343     val cmd =
   344       "\"$ML_HOME/poly\" --use " ^ Bash.string (File.platform_path code_path) ^
   345       " --use " ^ Bash.string (File.platform_path driver_path) ^
   346       " --eval " ^ Bash.string "main ()"
   347   in
   348     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   349   end
   350 
   351 fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
   352 
   353 
   354 (* driver for mlton *)
   355 
   356 val mltonN = "MLton"
   357 val ISABELLE_MLTON = "ISABELLE_MLTON"
   358 
   359 fun mk_driver_mlton _ path _ value_name =
   360   let
   361     val generatedN = "generated.sml"
   362     val driverN = "driver.sml"
   363     val projectN = "test"
   364     val ml_basisN = projectN ^ ".mlb"
   365 
   366     val code_path = Path.append path (Path.basic generatedN)
   367     val driver_path = Path.append path (Path.basic driverN)
   368     val ml_basis_path = Path.append path (Path.basic ml_basisN)
   369     val driver =
   370       "fun format_term NONE = \"\"\n" ^
   371       "  | format_term (SOME t) = t ();\n" ^
   372       "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   373       "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   374       "val result = " ^ value_name ^ " ();\n" ^
   375       "val _ = print \"" ^ start_markerN ^ "\";\n" ^
   376       "val _ = map (print o format) result;\n" ^
   377       "val _ = print \"" ^ end_markerN ^ "\";\n"
   378     val ml_basis =
   379       "$(SML_LIB)/basis/basis.mlb\n" ^
   380       generatedN ^ "\n" ^
   381       driverN
   382 
   383     val compile_cmd =
   384       File.bash_path (Path.variable ISABELLE_MLTON) ^
   385       " -default-type intinf " ^ File.bash_path ml_basis_path
   386     val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
   387   in
   388     {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
   389      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   390   end
   391 
   392 fun evaluate_in_mlton ctxt =
   393   evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
   394 
   395 
   396 (* driver for SML/NJ *)
   397 
   398 val smlnjN = "SMLNJ"
   399 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   400 
   401 fun mk_driver_smlnj _ path _ value_name =
   402   let
   403     val generatedN = "generated.sml"
   404     val driverN = "driver.sml"
   405 
   406     val code_path = Path.append path (Path.basic generatedN)
   407     val driver_path = Path.append path (Path.basic driverN)
   408     val driver =
   409       "structure Test = struct\n" ^
   410       "fun main prog_name =\n" ^
   411       "  let\n" ^
   412       "    fun format_term NONE = \"\"\n" ^
   413       "      | format_term (SOME t) = t ();\n" ^
   414       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   415       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   416       "    val result = " ^ value_name ^ " ();\n" ^
   417       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   418       "    val _ = map (print o format) result;\n" ^
   419       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   420       "  in\n" ^
   421       "    0\n" ^
   422       "  end;\n" ^
   423       "end;"
   424     val ml_source =
   425       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   426       "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
   427       "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand driver_path)) ^
   428       "; Test.main ();"
   429     val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
   430   in
   431     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   432   end
   433 
   434 fun evaluate_in_smlnj ctxt =
   435   evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
   436 
   437 
   438 (* driver for OCaml *)
   439 
   440 val ocamlN = "OCaml"
   441 val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
   442 
   443 fun mk_driver_ocaml _ path _ value_name =
   444   let
   445     val generatedN = "generated.ml"
   446     val driverN = "driver.ml"
   447 
   448     val code_path = Path.append path (Path.basic generatedN)
   449     val driver_path = Path.append path (Path.basic driverN)
   450     val driver =
   451       "let format_term = function\n" ^
   452       "  | None -> \"\"\n" ^
   453       "  | Some t -> t ();;\n" ^
   454       "let format = function\n" ^
   455       "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
   456       "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
   457       "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
   458       "let main x =\n" ^
   459       "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
   460       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
   461       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   462       "main ();;"
   463 
   464     val compiled_path = Path.append path (Path.basic "test")
   465     val compile_cmd =
   466       "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
   467       " -I " ^ File.bash_path path ^
   468       " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
   469 
   470     val run_cmd = File.bash_path compiled_path
   471   in
   472     {files = [(driver_path, driver)],
   473      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   474   end
   475 
   476 fun evaluate_in_ocaml ctxt =
   477   evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
   478 
   479 
   480 (* driver for GHC *)
   481 
   482 val ghcN = "GHC"
   483 val ISABELLE_GHC = "ISABELLE_GHC"
   484 
   485 val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
   486 
   487 fun mk_driver_ghc ctxt path modules value_name =
   488   let
   489     val driverN = "Main.hs"
   490 
   491     fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   492     val driver_path = Path.append path (Path.basic driverN)
   493     val driver =
   494       "module Main where {\n" ^
   495       String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   496       "main = do {\n" ^
   497       "    let {\n" ^
   498       "      format_term Nothing = \"\";\n" ^
   499       "      format_term (Just t) = t ();\n" ^
   500       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   501       "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   502       "      result = " ^ value_name ^ " ();\n" ^
   503       "    };\n" ^
   504       "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
   505       "    Prelude.mapM_ (putStr . format) result;\n" ^
   506       "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
   507       "  }\n" ^
   508       "}\n"
   509 
   510     val compiled_path = Path.append path (Path.basic "test")
   511     val compile_cmd =
   512       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
   513       Config.get ctxt ghc_options ^ " -o " ^ Bash.string (File.platform_path compiled_path) ^ " " ^
   514       Bash.string (File.platform_path driver_path) ^ " -i" ^ Bash.string (File.platform_path path)
   515 
   516     val run_cmd = File.bash_path compiled_path
   517   in
   518     {files = [(driver_path, driver)],
   519      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   520   end
   521 
   522 fun evaluate_in_ghc ctxt =
   523   evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
   524 
   525 
   526 (* driver for Scala *)
   527 
   528 val scalaN = "Scala"
   529 
   530 fun mk_driver_scala _ path _ value_name =
   531   let
   532     val generatedN = "Generated_Code"
   533     val driverN = "Driver.scala"
   534 
   535     val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   536     val driver_path = Path.append path (Path.basic driverN)
   537     val driver =
   538       "import " ^ generatedN ^ "._\n" ^
   539       "object Test {\n" ^
   540       "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   541       "    case None => \"\"\n" ^
   542       "    case Some(x) => x(())\n" ^
   543       "  }\n" ^
   544       "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
   545       "      case (true, _) => \"True\\n\"\n" ^
   546       "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
   547       "  }\n" ^
   548       "  def main(args:Array[String]) = {\n" ^
   549       "    val result = " ^ value_name ^ "(());\n" ^
   550       "    print(\"" ^ start_markerN ^ "\");\n" ^
   551       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
   552       "    print(\"" ^ end_markerN ^ "\");\n" ^
   553       "  }\n" ^
   554       "}\n"
   555 
   556     val compile_cmd =
   557       "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path path) ^
   558       " -classpath " ^ Bash.string (File.platform_path path) ^ " " ^
   559       Bash.string (File.platform_path code_path) ^ " " ^
   560       Bash.string (File.platform_path driver_path)
   561 
   562     val run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path path) ^ " Test"
   563   in
   564     {files = [(driver_path, driver)],
   565      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   566   end
   567 
   568 fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt
   569 
   570 
   571 (* command setup *)
   572 
   573 val _ =
   574   Outer_Syntax.command @{command_keyword test_code}
   575     "compile test cases to target languages, execute them and report results"
   576       (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   577         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
   578 
   579 val _ =
   580   Theory.setup (fold add_driver
   581     [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
   582      (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
   583      (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
   584      (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
   585      (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   586      (scalaN, (evaluate_in_scala, Code_Scala.target))]
   587   #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
   588       [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
   589 
   590 end