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