src/HOL/Library/code_test.ML
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 64957 3faa9b31ff78
child 65531 24544e3f183d
permissions -rw-r--r--
tuned proofs;
     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_line |> 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       "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
   345       Path.implode driver_path ^ "\\\"; main ();\" | \"$ML_HOME/poly\""
   346   in
   347     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   348   end
   349 
   350 fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
   351 
   352 
   353 (* driver for mlton *)
   354 
   355 val mltonN = "MLton"
   356 val ISABELLE_MLTON = "ISABELLE_MLTON"
   357 
   358 fun mk_driver_mlton _ path _ value_name =
   359   let
   360     val generatedN = "generated.sml"
   361     val driverN = "driver.sml"
   362     val projectN = "test"
   363     val ml_basisN = projectN ^ ".mlb"
   364 
   365     val code_path = Path.append path (Path.basic generatedN)
   366     val driver_path = Path.append path (Path.basic driverN)
   367     val ml_basis_path = Path.append path (Path.basic ml_basisN)
   368     val driver =
   369       "fun format_term NONE = \"\"\n" ^
   370       "  | format_term (SOME t) = t ();\n" ^
   371       "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   372       "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   373       "val result = " ^ value_name ^ " ();\n" ^
   374       "val _ = print \"" ^ start_markerN ^ "\";\n" ^
   375       "val _ = map (print o format) result;\n" ^
   376       "val _ = print \"" ^ end_markerN ^ "\";\n"
   377     val ml_basis =
   378       "$(SML_LIB)/basis/basis.mlb\n" ^
   379       generatedN ^ "\n" ^
   380       driverN
   381 
   382     val compile_cmd =
   383       File.bash_path (Path.variable ISABELLE_MLTON) ^
   384       " -default-type intinf " ^ File.bash_path ml_basis_path
   385     val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
   386   in
   387     {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
   388      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   389   end
   390 
   391 fun evaluate_in_mlton ctxt =
   392   evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
   393 
   394 
   395 (* driver for SML/NJ *)
   396 
   397 val smlnjN = "SMLNJ"
   398 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   399 
   400 fun mk_driver_smlnj _ path _ value_name =
   401   let
   402     val generatedN = "generated.sml"
   403     val driverN = "driver.sml"
   404 
   405     val code_path = Path.append path (Path.basic generatedN)
   406     val driver_path = Path.append path (Path.basic driverN)
   407     val driver =
   408       "structure Test = struct\n" ^
   409       "fun main prog_name =\n" ^
   410       "  let\n" ^
   411       "    fun format_term NONE = \"\"\n" ^
   412       "      | format_term (SOME t) = t ();\n" ^
   413       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   414       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   415       "    val result = " ^ value_name ^ " ();\n" ^
   416       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   417       "    val _ = map (print o format) result;\n" ^
   418       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   419       "  in\n" ^
   420       "    0\n" ^
   421       "  end;\n" ^
   422       "end;"
   423     val cmd =
   424       "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   425       "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
   426       "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
   427   in
   428     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   429   end
   430 
   431 fun evaluate_in_smlnj ctxt =
   432   evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
   433 
   434 
   435 (* driver for OCaml *)
   436 
   437 val ocamlN = "OCaml"
   438 val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
   439 
   440 fun mk_driver_ocaml _ path _ value_name =
   441   let
   442     val generatedN = "generated.ml"
   443     val driverN = "driver.ml"
   444 
   445     val code_path = Path.append path (Path.basic generatedN)
   446     val driver_path = Path.append path (Path.basic driverN)
   447     val driver =
   448       "let format_term = function\n" ^
   449       "  | None -> \"\"\n" ^
   450       "  | Some t -> t ();;\n" ^
   451       "let format = function\n" ^
   452       "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
   453       "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
   454       "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
   455       "let main x =\n" ^
   456       "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
   457       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
   458       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   459       "main ();;"
   460 
   461     val compiled_path = Path.append path (Path.basic "test")
   462     val compile_cmd =
   463       Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
   464       " -I " ^ Path.implode path ^
   465       " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
   466 
   467     val run_cmd = File.bash_path compiled_path
   468   in
   469     {files = [(driver_path, driver)],
   470      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   471   end
   472 
   473 fun evaluate_in_ocaml ctxt =
   474   evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
   475 
   476 
   477 (* driver for GHC *)
   478 
   479 val ghcN = "GHC"
   480 val ISABELLE_GHC = "ISABELLE_GHC"
   481 
   482 val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
   483 
   484 fun mk_driver_ghc ctxt path modules value_name =
   485   let
   486     val driverN = "Main.hs"
   487 
   488     fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   489     val driver_path = Path.append path (Path.basic driverN)
   490     val driver =
   491       "module Main where {\n" ^
   492       String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   493       "main = do {\n" ^
   494       "    let {\n" ^
   495       "      format_term Nothing = \"\";\n" ^
   496       "      format_term (Just t) = t ();\n" ^
   497       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   498       "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   499       "      result = " ^ value_name ^ " ();\n" ^
   500       "    };\n" ^
   501       "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
   502       "    Prelude.mapM_ (putStr . format) result;\n" ^
   503       "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
   504       "  }\n" ^
   505       "}\n"
   506 
   507     val compiled_path = Path.append path (Path.basic "test")
   508     val compile_cmd =
   509       Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
   510       Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
   511       Path.implode driver_path ^ " -i" ^ Path.implode path
   512 
   513     val run_cmd = File.bash_path compiled_path
   514   in
   515     {files = [(driver_path, driver)],
   516      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   517   end
   518 
   519 fun evaluate_in_ghc ctxt =
   520   evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
   521 
   522 
   523 (* driver for Scala *)
   524 
   525 val scalaN = "Scala"
   526 
   527 fun mk_driver_scala _ path _ value_name =
   528   let
   529     val generatedN = "Generated_Code"
   530     val driverN = "Driver.scala"
   531 
   532     val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   533     val driver_path = Path.append path (Path.basic driverN)
   534     val driver =
   535       "import " ^ generatedN ^ "._\n" ^
   536       "object Test {\n" ^
   537       "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   538       "    case None => \"\"\n" ^
   539       "    case Some(x) => x(())\n" ^
   540       "  }\n" ^
   541       "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
   542       "      case (true, _) => \"True\\n\"\n" ^
   543       "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
   544       "  }\n" ^
   545       "  def main(args:Array[String]) = {\n" ^
   546       "    val result = " ^ value_name ^ "(());\n" ^
   547       "    print(\"" ^ start_markerN ^ "\");\n" ^
   548       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
   549       "    print(\"" ^ end_markerN ^ "\");\n" ^
   550       "  }\n" ^
   551       "}\n"
   552 
   553     val compile_cmd =
   554       "\"$SCALA_HOME/bin/scalac\" $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_path path ^
   555       " -classpath " ^ File.bash_path path ^ " " ^
   556       File.bash_path code_path ^ " " ^ File.bash_path driver_path
   557 
   558     val run_cmd = "\"$SCALA_HOME/bin/scala\" -cp " ^ File.bash_path path ^ " Test"
   559   in
   560     {files = [(driver_path, driver)],
   561      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   562   end
   563 
   564 fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt
   565 
   566 
   567 (* command setup *)
   568 
   569 val _ =
   570   Outer_Syntax.command @{command_keyword test_code}
   571     "compile test cases to target languages, execute them and report results"
   572       (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   573         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
   574 
   575 val _ =
   576   Theory.setup (fold add_driver
   577     [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
   578      (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
   579      (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
   580      (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
   581      (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   582      (scalaN, (evaluate_in_scala, Code_Scala.target))]
   583   #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
   584       [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
   585 
   586 end