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