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