src/HOL/Library/code_test.ML
author wenzelm
Sat Dec 17 14:04:05 2016 +0100 (2016-12-17)
changeset 64579 38a1d8b41189
parent 64578 7b20f9f94f4e
child 64580 43ad19fbe9dc
permissions -rw-r--r--
more standard pretty printing;
tuned messages;
     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       | _ =>
   232         error (Pretty.string_of
   233           (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
   234             Syntax.pretty_term ctxt t])))
   235 
   236     val _ = List.app ensure_bool ts
   237 
   238     val evals = map (fn t => filter term_of (add_eval t [])) ts
   239     val eval = map mk_term_of evals
   240 
   241     val t =
   242       HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
   243         (map HOLogic.mk_prod (ts ~~ eval))
   244 
   245     val result = dynamic_value_strict ctxt t target
   246 
   247     val failed =
   248       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
   249       handle ListPair.UnequalLengths =>
   250         error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
   251   in
   252     (case failed of [] =>
   253       ()
   254     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   255   end
   256 
   257 fun test_targets ctxt = List.app o test_terms ctxt
   258 
   259 fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
   260 
   261 fun test_code_cmd raw_ts targets state =
   262   let
   263     val ctxt = Toplevel.context_of state
   264     val ts = Syntax.read_terms ctxt raw_ts
   265     val frees = fold Term.add_frees ts []
   266     val _ =
   267       if null frees then ()
   268       else error (Pretty.string_of
   269         (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
   270           Pretty.commas (map (pretty_free ctxt) frees))))
   271   in test_targets ctxt ts targets end
   272 
   273 fun eval_term target ctxt t =
   274   let
   275     val frees = Term.add_frees t []
   276     val _ =
   277       if null frees then ()
   278       else
   279         error (Pretty.string_of
   280           (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
   281             Pretty.commas (map (pretty_free ctxt) frees))))
   282 
   283     val T = fastype_of t
   284     val _ =
   285       if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort term_of}) then ()
   286       else error ("Type " ^ Syntax.string_of_typ ctxt T ^
   287        " of term not of sort " ^ Syntax.string_of_sort ctxt @{sort term_of})
   288 
   289     val t' =
   290       HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
   291         [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   292 
   293     val result = dynamic_value_strict ctxt t' target
   294   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
   295 
   296 
   297 (* generic driver *)
   298 
   299 fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   300   let
   301     val compiler = getenv env_var
   302     val _ =
   303       if compiler <> "" then ()
   304       else error (Pretty.string_of (Pretty.para
   305         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   306           compilerN ^ ", set this variable to your " ^ env_var_dest ^
   307           " in the $ISABELLE_HOME_USER/etc/settings file.")))
   308 
   309     fun compile NONE = ()
   310       | compile (SOME cmd) =
   311           let
   312             val (out, ret) = Isabelle_System.bash_output cmd
   313           in
   314             if ret = 0 then ()
   315             else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   316           end
   317 
   318     fun run path =
   319       let
   320         val modules = map fst code_files
   321         val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
   322 
   323         val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
   324         val _ = List.app (fn (name, content) => File.write name content) files
   325 
   326         val _ = compile compile_cmd
   327 
   328         val (out, res) = Isabelle_System.bash_output run_cmd
   329         val _ =
   330           if res = 0 then ()
   331           else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
   332             Int.toString res ^ "\nBash output:\n" ^ out)
   333       in out end
   334   in run end
   335 
   336 
   337 (* driver for PolyML *)
   338 
   339 val ISABELLE_POLYML = "ISABELLE_POLYML"
   340 val polymlN = "PolyML"
   341 
   342 fun mk_driver_polyml _ path _ value_name =
   343   let
   344     val generatedN = "generated.sml"
   345     val driverN = "driver.sml"
   346 
   347     val code_path = Path.append path (Path.basic generatedN)
   348     val driver_path = Path.append path (Path.basic driverN)
   349     val driver =
   350       "fun main prog_name = \n" ^
   351       "  let\n" ^
   352       "    fun format_term NONE = \"\"\n" ^
   353       "      | format_term (SOME t) = t ();\n" ^
   354       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   355       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   356       "    val result = " ^ value_name ^ " ();\n" ^
   357       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   358       "    val _ = map (print o format) result;\n" ^
   359       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   360       "  in\n" ^
   361       "    ()\n" ^
   362       "  end;\n"
   363     val cmd =
   364       "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
   365       Path.implode driver_path ^ "\\\"; main ();\" | " ^
   366       Path.implode (Path.variable ISABELLE_POLYML)
   367   in
   368     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   369   end
   370 
   371 fun evaluate_in_polyml ctxt =
   372   gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
   373 
   374 
   375 (* driver for mlton *)
   376 
   377 val mltonN = "MLton"
   378 val ISABELLE_MLTON = "ISABELLE_MLTON"
   379 
   380 fun mk_driver_mlton _ path _ value_name =
   381   let
   382     val generatedN = "generated.sml"
   383     val driverN = "driver.sml"
   384     val projectN = "test"
   385     val ml_basisN = projectN ^ ".mlb"
   386 
   387     val code_path = Path.append path (Path.basic generatedN)
   388     val driver_path = Path.append path (Path.basic driverN)
   389     val ml_basis_path = Path.append path (Path.basic ml_basisN)
   390     val driver =
   391       "fun format_term NONE = \"\"\n" ^
   392       "  | format_term (SOME t) = t ();\n" ^
   393       "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   394       "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   395       "val result = " ^ value_name ^ " ();\n" ^
   396       "val _ = print \"" ^ start_markerN ^ "\";\n" ^
   397       "val _ = map (print o format) result;\n" ^
   398       "val _ = print \"" ^ end_markerN ^ "\";\n"
   399     val ml_basis =
   400       "$(SML_LIB)/basis/basis.mlb\n" ^
   401       generatedN ^ "\n" ^
   402       driverN
   403 
   404     val compile_cmd =
   405       File.bash_path (Path.variable ISABELLE_MLTON) ^
   406       " -default-type intinf " ^ File.bash_path ml_basis_path
   407     val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
   408   in
   409     {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
   410      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   411   end
   412 
   413 fun evaluate_in_mlton ctxt =
   414   gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
   415 
   416 
   417 (* driver for SML/NJ *)
   418 
   419 val smlnjN = "SMLNJ"
   420 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   421 
   422 fun mk_driver_smlnj _ path _ value_name =
   423   let
   424     val generatedN = "generated.sml"
   425     val driverN = "driver.sml"
   426 
   427     val code_path = Path.append path (Path.basic generatedN)
   428     val driver_path = Path.append path (Path.basic driverN)
   429     val driver =
   430       "structure Test = struct\n" ^
   431       "fun main prog_name =\n" ^
   432       "  let\n" ^
   433       "    fun format_term NONE = \"\"\n" ^
   434       "      | format_term (SOME t) = t ();\n" ^
   435       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   436       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   437       "    val result = " ^ value_name ^ " ();\n" ^
   438       "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   439       "    val _ = map (print o format) result;\n" ^
   440       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   441       "  in\n" ^
   442       "    0\n" ^
   443       "  end;\n" ^
   444       "end;"
   445     val cmd =
   446       "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   447       "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
   448       "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
   449   in
   450     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   451   end
   452 
   453 fun evaluate_in_smlnj ctxt =
   454   gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
   455 
   456 
   457 (* driver for OCaml *)
   458 
   459 val ocamlN = "OCaml"
   460 val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
   461 
   462 fun mk_driver_ocaml _ path _ value_name =
   463   let
   464     val generatedN = "generated.ml"
   465     val driverN = "driver.ml"
   466 
   467     val code_path = Path.append path (Path.basic generatedN)
   468     val driver_path = Path.append path (Path.basic driverN)
   469     val driver =
   470       "let format_term = function\n" ^
   471       "  | None -> \"\"\n" ^
   472       "  | Some t -> t ();;\n" ^
   473       "let format = function\n" ^
   474       "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
   475       "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
   476       "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
   477       "let main x =\n" ^
   478       "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
   479       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
   480       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   481       "main ();;"
   482 
   483     val compiled_path = Path.append path (Path.basic "test")
   484     val compile_cmd =
   485       Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
   486       " -I " ^ Path.implode path ^
   487       " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
   488 
   489     val run_cmd = File.bash_path compiled_path
   490   in
   491     {files = [(driver_path, driver)],
   492      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   493   end
   494 
   495 fun evaluate_in_ocaml ctxt =
   496   gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
   497 
   498 
   499 (* driver for GHC *)
   500 
   501 val ghcN = "GHC"
   502 val ISABELLE_GHC = "ISABELLE_GHC"
   503 
   504 val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
   505 
   506 fun mk_driver_ghc ctxt path modules value_name =
   507   let
   508     val driverN = "Main.hs"
   509 
   510     fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   511     val driver_path = Path.append path (Path.basic driverN)
   512     val driver =
   513       "module Main where {\n" ^
   514       String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   515       "main = do {\n" ^
   516       "    let {\n" ^
   517       "      format_term Nothing = \"\";\n" ^
   518       "      format_term (Just t) = t ();\n" ^
   519       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   520       "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   521       "      result = " ^ value_name ^ " ();\n" ^
   522       "    };\n" ^
   523       "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
   524       "    Prelude.mapM_ (putStr . format) result;\n" ^
   525       "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
   526       "  }\n" ^
   527       "}\n"
   528 
   529     val compiled_path = Path.append path (Path.basic "test")
   530     val compile_cmd =
   531       Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
   532       Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
   533       Path.implode driver_path ^ " -i" ^ Path.implode path
   534 
   535     val run_cmd = File.bash_path compiled_path
   536   in
   537     {files = [(driver_path, driver)],
   538      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   539   end
   540 
   541 fun evaluate_in_ghc ctxt =
   542   gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   543 
   544 
   545 (* driver for Scala *)
   546 
   547 val scalaN = "Scala"
   548 val ISABELLE_SCALA = "ISABELLE_SCALA"
   549 
   550 fun mk_driver_scala _ path _ value_name =
   551   let
   552     val generatedN = "Generated_Code"
   553     val driverN = "Driver.scala"
   554 
   555     val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   556     val driver_path = Path.append path (Path.basic driverN)
   557     val driver =
   558       "import " ^ generatedN ^ "._\n" ^
   559       "object Test {\n" ^
   560       "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   561       "    case None => \"\"\n" ^
   562       "    case Some(x) => x(())\n" ^
   563       "  }\n" ^
   564       "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
   565       "      case (true, _) => \"True\\n\"\n" ^
   566       "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
   567       "  }\n" ^
   568       "  def main(args:Array[String]) = {\n" ^
   569       "    val result = " ^ value_name ^ "(());\n" ^
   570       "    print(\"" ^ start_markerN ^ "\");\n" ^
   571       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
   572       "    print(\"" ^ end_markerN ^ "\");\n" ^
   573       "  }\n" ^
   574       "}\n"
   575 
   576     val compile_cmd =
   577       Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
   578       " -d " ^ File.bash_path path ^ " -classpath " ^ File.bash_path path ^ " " ^
   579       File.bash_path code_path ^ " " ^ File.bash_path driver_path
   580 
   581     val run_cmd =
   582       Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
   583       " -cp " ^ File.bash_path path ^ " Test"
   584   in
   585     {files = [(driver_path, driver)],
   586      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   587   end
   588 
   589 fun evaluate_in_scala ctxt =
   590   gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
   591 
   592 val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   593 
   594 val _ =
   595   Outer_Syntax.command @{command_keyword test_code}
   596     "compile test cases to target languages, execute them and report results"
   597       (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   598 
   599 val _ = Theory.setup (fold add_driver
   600   [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
   601    (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
   602    (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
   603    (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
   604    (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   605    (scalaN, (evaluate_in_scala, Code_Scala.target))]
   606   #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
   607     [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
   608 
   609 end