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