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