src/HOL/Library/code_test.ML
author wenzelm
Tue Sep 01 23:10:23 2015 +0200 (2015-09-01)
changeset 61077 06cca32aa519
parent 60022 ea987317a785
child 62549 9498623b27f0
permissions -rw-r--r--
thread context for exceptions from forks, e.g. relevant when printing errors;
tuned signature;
     1 (*  Title:      HOL/Library/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")
   152     @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
   153     @ pretty_eval ctxt evals eval_ts)
   154 
   155 fun pretty_failures ctxt target failures =
   156   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   157 
   158 (* Driver invocation *)
   159 
   160 val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false);
   161 
   162 fun with_overlord_dir name f =
   163   let
   164     val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   165     val _ = Isabelle_System.mkdirs path;
   166   in
   167     Exn.release (Exn.capture f path)
   168   end;
   169 
   170 fun dynamic_value_strict ctxt t compiler =
   171   let
   172     val thy = Proof_Context.theory_of ctxt
   173     val (driver, target) = case get_driver thy compiler
   174      of NONE => error ("No driver for target " ^ compiler)
   175       | SOME f => f;
   176     val debug = Config.get (Proof_Context.init_global thy) overlord
   177     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
   178     fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
   179     fun evaluator program _ vs_ty deps =
   180       Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
   181     fun postproc f = map (apsnd (map_option (map f)))
   182   in
   183     Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
   184   end;
   185 
   186 (* Term preprocessing *)
   187 
   188 fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
   189   | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
   190     acc
   191     |> add_eval rhs
   192     |> add_eval lhs
   193     |> cons rhs
   194     |> cons lhs)
   195   | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
   196   | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
   197     lhs :: rhs :: acc)
   198   | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
   199     lhs :: rhs :: acc)
   200   | add_eval _ = I
   201 
   202 fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
   203   | mk_term_of ts =
   204   let
   205     val tuple = mk_tuples ts
   206     val T = fastype_of tuple
   207   in
   208     @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
   209       (absdummy @{typ unit} (@{const yxml_string_of_term} $
   210         (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
   211   end
   212 
   213 fun test_terms ctxt ts target =
   214   let
   215     val thy = Proof_Context.theory_of ctxt
   216 
   217     fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
   218 
   219     fun ensure_bool t = case fastype_of t of @{typ bool} => ()
   220       | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))
   221 
   222     val _ = map ensure_bool ts
   223 
   224     val evals = map (fn t => filter term_of (add_eval t [])) ts
   225     val eval = map mk_term_of evals
   226 
   227     val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   228     val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
   229 
   230     val result = dynamic_value_strict ctxt t target;
   231 
   232     val failed =
   233       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
   234       handle ListPair.UnequalLengths => 
   235         error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
   236     val _ = case failed of [] => () 
   237       | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
   238   in
   239     ()
   240   end
   241 
   242 fun test_targets ctxt = map o test_terms ctxt
   243 
   244 fun test_code_cmd raw_ts targets state =
   245   let
   246     val ctxt = Toplevel.context_of state;
   247     val ts = Syntax.read_terms ctxt raw_ts;
   248     val frees = fold Term.add_free_names ts []
   249     val _ = if frees = [] then () else
   250       error ("Terms contain free variables: " ^
   251       Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
   252   in
   253     test_targets ctxt ts targets; ()
   254   end
   255 
   256 fun eval_term target ctxt t =
   257   let
   258     val frees = Term.add_free_names t []
   259     val _ = if frees = [] then () else
   260       error ("Term contains free variables: " ^
   261       Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
   262 
   263     val thy = Proof_Context.theory_of ctxt
   264 
   265     val T_t = fastype_of t
   266     val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
   267       ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 
   268        " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
   269 
   270     val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   271     val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   272 
   273     val result = dynamic_value_strict ctxt t' target;
   274   in
   275     case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
   276   end
   277 
   278 (* Generic driver *)
   279 
   280 fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   281   let
   282     val compiler = getenv env_var
   283     val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para 
   284          ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   285          compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
   286 
   287     fun compile NONE = ()
   288       | compile (SOME cmd) =
   289         let
   290           val (out, ret) = Isabelle_System.bash_output cmd
   291         in
   292           if ret = 0 then () else error
   293             ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   294         end
   295 
   296     fun run (path : Path.T)= 
   297       let
   298         val modules = map fst code_files
   299         val {files, compile_cmd, run_cmd, mk_code_file}
   300           =  mk_driver ctxt path modules value_name
   301 
   302         val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
   303         val _ = map (fn (name, content) => File.write name content) files
   304 
   305         val _ = compile compile_cmd
   306 
   307         val (out, res) = Isabelle_System.bash_output run_cmd
   308         val _ = if res = 0 then () else error
   309           ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
   310            "\nBash output:\n" ^ out)
   311       in
   312         out
   313       end
   314   in
   315     run
   316   end
   317 
   318 (* Driver for PolyML *)
   319 
   320 val ISABELLE_POLYML = "ISABELLE_POLYML"
   321 val polymlN = "PolyML";
   322 
   323 fun mk_driver_polyml _ path _ value_name =
   324   let
   325     val generatedN = "generated.sml"
   326     val driverN = "driver.sml"
   327 
   328     val code_path = Path.append path (Path.basic generatedN)
   329     val driver_path = Path.append path (Path.basic driverN)
   330     val driver = 
   331       "fun main prog_name = \n" ^
   332       "  let\n" ^
   333       "    fun format_term NONE = \"\"\n" ^ 
   334       "      | format_term (SOME t) = t ();\n" ^
   335       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   336       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   337       "    val result = " ^ value_name ^ " ();\n" ^
   338       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   339       "    val _ = map (print o format) result;\n" ^
   340       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   341       "  in\n" ^
   342       "    ()\n" ^
   343       "  end;\n"
   344     val cmd =
   345       "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
   346       Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
   347       Path.implode (Path.variable ISABELLE_POLYML)
   348   in
   349     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   350   end
   351 
   352 fun evaluate_in_polyml ctxt =
   353   gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
   354 
   355 (* Driver for mlton *)
   356 
   357 val mltonN = "MLton"
   358 val ISABELLE_MLTON = "ISABELLE_MLTON"
   359 
   360 fun mk_driver_mlton _ path _ value_name =
   361   let
   362     val generatedN = "generated.sml"
   363     val driverN = "driver.sml"
   364     val projectN = "test"
   365     val ml_basisN = projectN ^ ".mlb"
   366 
   367     val code_path = Path.append path (Path.basic generatedN)
   368     val driver_path = Path.append path (Path.basic driverN)
   369     val ml_basis_path = Path.append path (Path.basic ml_basisN)
   370     val driver = 
   371       "fun format_term NONE = \"\"\n" ^ 
   372       "  | format_term (SOME t) = t ();\n" ^
   373       "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   374       "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   375       "val result = " ^ value_name ^ " ();\n" ^
   376       "val _ = print \"" ^ start_markerN ^ "\";\n" ^
   377       "val _ = map (print o format) result;\n" ^
   378       "val _ = print \"" ^ end_markerN ^ "\";\n"
   379     val ml_basis =
   380       "$(SML_LIB)/basis/basis.mlb\n" ^
   381       generatedN ^ "\n" ^
   382       driverN
   383 
   384     val compile_cmd =
   385       File.shell_path (Path.variable ISABELLE_MLTON) ^
   386       " -default-type intinf " ^ File.shell_path ml_basis_path
   387     val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
   388   in
   389     {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
   390      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   391   end
   392 
   393 fun evaluate_in_mlton ctxt =
   394   gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
   395 
   396 (* Driver for SML/NJ *)
   397 
   398 val smlnjN = "SMLNJ"
   399 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   400 
   401 fun mk_driver_smlnj _ path _ value_name =
   402   let
   403     val generatedN = "generated.sml"
   404     val driverN = "driver.sml"
   405 
   406     val code_path = Path.append path (Path.basic generatedN)
   407     val driver_path = Path.append path (Path.basic driverN)
   408     val driver = 
   409       "structure Test = struct\n" ^
   410       "fun main prog_name =\n" ^
   411       "  let\n" ^
   412       "    fun format_term NONE = \"\"\n" ^ 
   413       "      | format_term (SOME t) = t ();\n" ^
   414       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   415       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   416       "    val result = " ^ value_name ^ " ();\n" ^
   417       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   418       "    val _ = map (print o format) result;\n" ^
   419       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   420       "  in\n" ^
   421       "    0\n" ^
   422       "  end;\n" ^
   423       "end;"
   424     val cmd =
   425       "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   426       "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
   427       "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
   428   in
   429     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   430   end
   431 
   432 fun evaluate_in_smlnj ctxt =
   433   gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
   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.shell_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   gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
   475 
   476 (* Driver for GHC *)
   477 
   478 val ghcN = "GHC"
   479 val ISABELLE_GHC = "ISABELLE_GHC"
   480 
   481 val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
   482 
   483 fun mk_driver_ghc ctxt path modules value_name =
   484   let
   485     val driverN = "Main.hs"
   486 
   487     fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   488     val driver_path = Path.append path (Path.basic driverN)
   489     val driver = 
   490       "module Main where {\n" ^
   491       String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   492       "main = do {\n" ^
   493       "    let {\n" ^
   494       "      format_term Nothing = \"\";\n" ^ 
   495       "      format_term (Just t) = t ();\n" ^
   496       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   497       "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   498       "      result = " ^ value_name ^ " ();\n" ^
   499       "    };\n" ^
   500       "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
   501       "    Prelude.mapM_ (putStr . format) result;\n" ^
   502       "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
   503       "  }\n" ^
   504       "}\n"
   505 
   506     val compiled_path = Path.append path (Path.basic "test")
   507     val compile_cmd =
   508       Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
   509       Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
   510       Path.implode driver_path ^ " -i" ^ Path.implode path
   511 
   512     val run_cmd = File.shell_path compiled_path
   513   in
   514     {files = [(driver_path, driver)],
   515      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   516   end
   517 
   518 fun evaluate_in_ghc ctxt =
   519   gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   520 
   521 (* Driver for Scala *)
   522 
   523 val scalaN = "Scala"
   524 val ISABELLE_SCALA = "ISABELLE_SCALA"
   525 
   526 fun mk_driver_scala _ path _ value_name =
   527   let
   528     val generatedN = "Generated_Code"
   529     val driverN = "Driver.scala"
   530 
   531     val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   532     val driver_path = Path.append path (Path.basic driverN)
   533     val driver = 
   534       "import " ^ generatedN ^ "._\n" ^
   535       "object Test {\n" ^
   536       "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   537       "    case None => \"\"\n" ^
   538       "    case Some(x) => x(())\n" ^
   539       "  }\n" ^
   540       "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
   541       "      case (true, _) => \"True\\n\"\n" ^
   542       "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
   543       "  }\n" ^
   544       "  def main(args:Array[String]) = {\n" ^
   545       "    val result = " ^ value_name ^ "(());\n" ^
   546       "    print(\"" ^ start_markerN ^ "\");\n" ^
   547       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
   548       "    print(\"" ^ end_markerN ^ "\");\n" ^
   549       "  }\n" ^
   550       "}\n"
   551 
   552     val compile_cmd =
   553       Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
   554       " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
   555       File.shell_path code_path ^ " " ^ File.shell_path driver_path
   556 
   557     val run_cmd =
   558       Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
   559       " -cp " ^ File.shell_path path ^ " Test"
   560   in
   561     {files = [(driver_path, driver)],
   562      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   563   end
   564 
   565 fun evaluate_in_scala ctxt =
   566   gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
   567 
   568 val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   569 
   570 val _ = 
   571   Outer_Syntax.command @{command_keyword test_code}
   572     "compile test cases to target languages, execute them and report results"
   573       (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   574 
   575 val _ = Theory.setup (fold add_driver
   576   [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
   577    (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
   578    (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
   579    (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
   580    (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   581    (scalaN, (evaluate_in_scala, Code_Scala.target))]
   582   #> fold (fn target => Value.add_evaluator (target, eval_term target))
   583     [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
   584 
   585 end
   586