src/HOL/Library/code_test.ML
changeset 58626 6c473ed0ac70
parent 58415 8392d221bd91
child 58832 ec9550bd5fd7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/code_test.ML	Wed Oct 08 09:09:12 2014 +0200
     1.3 @@ -0,0 +1,580 @@
     1.4 +(*  Title:      Code_Test.ML
     1.5 +    Author:     Andreas Lochbihler, ETH Zurich
     1.6 +
     1.7 +Test infrastructure for the code generator
     1.8 +*)
     1.9 +
    1.10 +signature CODE_TEST = sig
    1.11 +  val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory
    1.12 +  val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
    1.13 +  val overlord : bool Config.T
    1.14 +  val successN : string
    1.15 +  val failureN : string
    1.16 +  val start_markerN : string
    1.17 +  val end_markerN : string
    1.18 +  val test_terms : Proof.context -> term list -> string -> unit
    1.19 +  val test_targets : Proof.context -> term list -> string list -> unit list
    1.20 +  val test_code_cmd : string list -> string list -> Toplevel.state -> unit
    1.21 +
    1.22 +  val eval_term : string -> Proof.context -> term -> term
    1.23 +
    1.24 +  val gen_driver :
    1.25 +   (theory -> Path.T -> string list -> string ->
    1.26 +    {files : (Path.T * string) list,
    1.27 +     compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T})
    1.28 +   -> string -> string -> string
    1.29 +   -> theory -> (string * string) list * string -> Path.T -> string
    1.30 +
    1.31 +  val ISABELLE_POLYML : string
    1.32 +  val polymlN : string
    1.33 +  val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
    1.34 +
    1.35 +  val mltonN : string
    1.36 +  val ISABELLE_MLTON : string
    1.37 +  val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string
    1.38 +
    1.39 +  val smlnjN : string
    1.40 +  val ISABELLE_SMLNJ : string
    1.41 +  val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string
    1.42 +
    1.43 +  val ocamlN : string
    1.44 +  val ISABELLE_OCAMLC : string
    1.45 +  val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string
    1.46 +
    1.47 +  val ghcN : string
    1.48 +  val ISABELLE_GHC : string
    1.49 +  val ghc_options : string Config.T
    1.50 +  val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string
    1.51 +
    1.52 +  val scalaN : string
    1.53 +  val ISABELLE_SCALA : string
    1.54 +  val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string
    1.55 +end
    1.56 +
    1.57 +structure Code_Test : CODE_TEST = struct
    1.58 +
    1.59 +(* convert a list of terms into nested tuples and back *)
    1.60 +fun mk_tuples [] = @{term "()"}
    1.61 +  | mk_tuples [t] = t
    1.62 +  | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
    1.63 +
    1.64 +fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r
    1.65 +  | dest_tuples t = [t]
    1.66 +
    1.67 +
    1.68 +fun map_option _ NONE = NONE
    1.69 +  | map_option f (SOME x) = SOME (f x)
    1.70 +
    1.71 +fun last_field sep str =
    1.72 +  let
    1.73 +    val n = size sep;
    1.74 +    val len = size str;
    1.75 +    fun find i =
    1.76 +      if i < 0 then NONE
    1.77 +      else if String.substring (str, i, n) = sep then SOME i
    1.78 +      else find (i - 1);
    1.79 +  in
    1.80 +    (case find (len - n) of
    1.81 +      NONE => NONE
    1.82 +    | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
    1.83 +  end;
    1.84 +
    1.85 +fun split_first_last start stop s =
    1.86 +  case first_field start s
    1.87 +   of NONE => NONE
    1.88 +    | SOME (initial, rest) =>
    1.89 +      case last_field stop rest
    1.90 +       of NONE => NONE
    1.91 +        | SOME (middle, tail) => SOME (initial, middle, tail);
    1.92 +
    1.93 +(* Data slot for drivers *)
    1.94 +
    1.95 +structure Drivers = Theory_Data
    1.96 +(
    1.97 +  type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list;
    1.98 +  val empty = [];
    1.99 +  val extend = I;
   1.100 +  fun merge data : T = AList.merge (op =) (K true) data;
   1.101 +)
   1.102 +
   1.103 +val add_driver = Drivers.map o AList.update (op =);
   1.104 +val get_driver = AList.lookup (op =) o Drivers.get;
   1.105 +
   1.106 +(*
   1.107 +  Test drivers must produce output of the following format:
   1.108 +  
   1.109 +  The start of the relevant data is marked with start_markerN,
   1.110 +  its end with end_markerN.
   1.111 +
   1.112 +  Between these two markers, every line corresponds to one test.
   1.113 +  Lines of successful tests start with successN, failures start with failureN.
   1.114 +  The failure failureN may continue with the YXML encoding of the evaluated term.
   1.115 +  There must not be any additional whitespace in between.
   1.116 +*)
   1.117 +
   1.118 +(* Parsing of results *)
   1.119 +
   1.120 +val successN = "True"
   1.121 +val failureN = "False"
   1.122 +val start_markerN = "*@*Isabelle/Code_Test-start*@*"
   1.123 +val end_markerN = "*@*Isabelle/Code_Test-end*@*"
   1.124 +
   1.125 +fun parse_line line =
   1.126 +  if String.isPrefix successN line then (true, NONE)
   1.127 +  else if String.isPrefix failureN line then (false, 
   1.128 +    if size line > size failureN then
   1.129 +      String.extract (line, size failureN, NONE)
   1.130 +      |> YXML.parse_body
   1.131 +      |> Term_XML.Decode.term
   1.132 +      |> dest_tuples
   1.133 +      |> SOME
   1.134 +    else NONE)
   1.135 +  else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
   1.136 +
   1.137 +fun parse_result target out =
   1.138 +  case split_first_last start_markerN end_markerN out
   1.139 +    of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
   1.140 +     | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line
   1.141 +
   1.142 +(* Pretty printing of test results *)
   1.143 +
   1.144 +fun pretty_eval _ NONE _ = []
   1.145 +  | pretty_eval ctxt (SOME evals) ts = 
   1.146 +    [Pretty.fbrk,
   1.147 +     Pretty.big_list "Evaluated terms"
   1.148 +       (map (fn (t, eval) => Pretty.block 
   1.149 +         [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   1.150 +          Syntax.pretty_term ctxt eval])
   1.151 +       (ts ~~ evals))]
   1.152 +
   1.153 +fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   1.154 +  Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
   1.155 +    @ pretty_eval ctxt evals eval_ts)
   1.156 +
   1.157 +fun pretty_failures ctxt target failures =
   1.158 +  Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   1.159 +
   1.160 +(* Driver invocation *)
   1.161 +
   1.162 +val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false);
   1.163 +
   1.164 +fun with_overlord_dir name f =
   1.165 +  let
   1.166 +    val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   1.167 +    val _ = Isabelle_System.mkdirs path;
   1.168 +  in
   1.169 +    Exn.release (Exn.capture f path)
   1.170 +  end;
   1.171 +
   1.172 +fun dynamic_value_strict ctxt t compiler =
   1.173 +  let
   1.174 +    val thy = Proof_Context.theory_of ctxt
   1.175 +    val (driver, target) = case get_driver thy compiler
   1.176 +     of NONE => error ("No driver for target " ^ compiler)
   1.177 +      | SOME f => f;
   1.178 +    val debug = Config.get (Proof_Context.init_global thy) overlord
   1.179 +    val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
   1.180 +    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
   1.181 +    fun evaluator program _ vs_ty deps =
   1.182 +      Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
   1.183 +    fun postproc f = map (apsnd (map_option (map f)))
   1.184 +  in
   1.185 +    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t)
   1.186 +  end;
   1.187 +
   1.188 +(* Term preprocessing *)
   1.189 +
   1.190 +fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
   1.191 +  | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
   1.192 +    acc
   1.193 +    |> add_eval rhs
   1.194 +    |> add_eval lhs
   1.195 +    |> cons rhs
   1.196 +    |> cons lhs)
   1.197 +  | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
   1.198 +  | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
   1.199 +    lhs :: rhs :: acc)
   1.200 +  | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
   1.201 +    lhs :: rhs :: acc)
   1.202 +  | add_eval _ = I
   1.203 +
   1.204 +fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
   1.205 +  | mk_term_of ts =
   1.206 +  let
   1.207 +    val tuple = mk_tuples ts
   1.208 +    val T = fastype_of tuple
   1.209 +  in
   1.210 +    @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
   1.211 +      (absdummy @{typ unit} (@{const yxml_string_of_term} $
   1.212 +        (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
   1.213 +  end
   1.214 +
   1.215 +fun test_terms ctxt ts target =
   1.216 +  let
   1.217 +    val thy = Proof_Context.theory_of ctxt
   1.218 +
   1.219 +    fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
   1.220 +
   1.221 +    fun ensure_bool t = case fastype_of t of @{typ bool} => ()
   1.222 +      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))
   1.223 +
   1.224 +    val _ = map ensure_bool ts
   1.225 +
   1.226 +    val evals = map (fn t => filter term_of (add_eval t [])) ts
   1.227 +    val eval = map mk_term_of evals
   1.228 +
   1.229 +    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   1.230 +    val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
   1.231 +
   1.232 +    val result = dynamic_value_strict ctxt t target;
   1.233 +
   1.234 +    val failed =
   1.235 +      filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
   1.236 +      handle ListPair.UnequalLengths => 
   1.237 +        error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
   1.238 +    val _ = case failed of [] => () 
   1.239 +      | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
   1.240 +  in
   1.241 +    ()
   1.242 +  end
   1.243 +
   1.244 +fun test_targets ctxt = map o test_terms ctxt
   1.245 +
   1.246 +fun test_code_cmd raw_ts targets state =
   1.247 +  let
   1.248 +    val ctxt = Toplevel.context_of state;
   1.249 +    val ts = Syntax.read_terms ctxt raw_ts;
   1.250 +    val frees = fold Term.add_free_names ts []
   1.251 +    val _ = if frees = [] then () else
   1.252 +      error ("Terms contain free variables: " ^
   1.253 +      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
   1.254 +  in
   1.255 +    test_targets ctxt ts targets; ()
   1.256 +  end
   1.257 +
   1.258 +fun eval_term target ctxt t =
   1.259 +  let
   1.260 +    val frees = Term.add_free_names t []
   1.261 +    val _ = if frees = [] then () else
   1.262 +      error ("Term contains free variables: " ^
   1.263 +      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
   1.264 +
   1.265 +    val thy = Proof_Context.theory_of ctxt
   1.266 +
   1.267 +    val T_t = fastype_of t
   1.268 +    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
   1.269 +      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 
   1.270 +       " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
   1.271 +
   1.272 +    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   1.273 +    val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   1.274 +
   1.275 +    val result = dynamic_value_strict ctxt t' target;
   1.276 +  in
   1.277 +    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
   1.278 +  end
   1.279 +
   1.280 +(* Generic driver *)
   1.281 +
   1.282 +fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   1.283 +  let
   1.284 +    val compiler = getenv env_var
   1.285 +    val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para 
   1.286 +         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   1.287 +         compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
   1.288 +
   1.289 +    fun compile NONE = ()
   1.290 +      | compile (SOME cmd) =
   1.291 +        let
   1.292 +          val (out, ret) = Isabelle_System.bash_output cmd
   1.293 +        in
   1.294 +          if ret = 0 then () else error
   1.295 +            ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   1.296 +        end
   1.297 +
   1.298 +    fun run (path : Path.T)= 
   1.299 +      let
   1.300 +        val modules = map fst code_files
   1.301 +        val {files, compile_cmd, run_cmd, mk_code_file}
   1.302 +          =  mk_driver ctxt path modules value_name
   1.303 +
   1.304 +        val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
   1.305 +        val _ = map (fn (name, content) => File.write name content) files
   1.306 +
   1.307 +        val _ = compile compile_cmd
   1.308 +
   1.309 +        val (out, res) = Isabelle_System.bash_output run_cmd
   1.310 +        val _ = if res = 0 then () else error
   1.311 +          ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
   1.312 +           "\nBash output:\n" ^ out)
   1.313 +      in
   1.314 +        out
   1.315 +      end
   1.316 +  in
   1.317 +    run
   1.318 +  end
   1.319 +
   1.320 +(* Driver for PolyML *)
   1.321 +
   1.322 +val ISABELLE_POLYML = "ISABELLE_POLYML"
   1.323 +val polymlN = "PolyML";
   1.324 +
   1.325 +fun mk_driver_polyml _ path _ value_name =
   1.326 +  let
   1.327 +    val generatedN = "generated.sml"
   1.328 +    val driverN = "driver.sml"
   1.329 +
   1.330 +    val code_path = Path.append path (Path.basic generatedN)
   1.331 +    val driver_path = Path.append path (Path.basic driverN)
   1.332 +    val driver = 
   1.333 +      "fun main prog_name = \n" ^
   1.334 +      "  let\n" ^
   1.335 +      "    fun format_term NONE = \"\"\n" ^ 
   1.336 +      "      | format_term (SOME t) = t ();\n" ^
   1.337 +      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.338 +      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.339 +      "    val result = " ^ value_name ^ " ();\n" ^
   1.340 +      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   1.341 +      "    val _ = map (print o format) result;\n" ^
   1.342 +      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   1.343 +      "  in\n" ^
   1.344 +      "    ()\n" ^
   1.345 +      "  end;\n"
   1.346 +    val cmd =
   1.347 +      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
   1.348 +      Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
   1.349 +      Path.implode (Path.variable ISABELLE_POLYML)
   1.350 +  in
   1.351 +    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   1.352 +  end
   1.353 +
   1.354 +val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
   1.355 +
   1.356 +(* Driver for mlton *)
   1.357 +
   1.358 +val mltonN = "MLton"
   1.359 +val ISABELLE_MLTON = "ISABELLE_MLTON"
   1.360 +
   1.361 +fun mk_driver_mlton _ path _ value_name =
   1.362 +  let
   1.363 +    val generatedN = "generated.sml"
   1.364 +    val driverN = "driver.sml"
   1.365 +    val projectN = "test"
   1.366 +    val ml_basisN = projectN ^ ".mlb"
   1.367 +
   1.368 +    val code_path = Path.append path (Path.basic generatedN)
   1.369 +    val driver_path = Path.append path (Path.basic driverN)
   1.370 +    val ml_basis_path = Path.append path (Path.basic ml_basisN)
   1.371 +    val driver = 
   1.372 +      "fun format_term NONE = \"\"\n" ^ 
   1.373 +      "  | format_term (SOME t) = t ();\n" ^
   1.374 +      "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.375 +      "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.376 +      "val result = " ^ value_name ^ " ();\n" ^
   1.377 +      "val _ = print \"" ^ start_markerN ^ "\";\n" ^
   1.378 +      "val _ = map (print o format) result;\n" ^
   1.379 +      "val _ = print \"" ^ end_markerN ^ "\";\n"
   1.380 +    val ml_basis =
   1.381 +      "$(SML_LIB)/basis/basis.mlb\n" ^
   1.382 +      generatedN ^ "\n" ^
   1.383 +      driverN
   1.384 +
   1.385 +    val compile_cmd =
   1.386 +      File.shell_path (Path.variable ISABELLE_MLTON) ^
   1.387 +      " -default-type intinf " ^ File.shell_path ml_basis_path
   1.388 +    val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
   1.389 +  in
   1.390 +    {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
   1.391 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   1.392 +  end
   1.393 +
   1.394 +val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN
   1.395 +
   1.396 +(* Driver for SML/NJ *)
   1.397 +
   1.398 +val smlnjN = "SMLNJ"
   1.399 +val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   1.400 +
   1.401 +fun mk_driver_smlnj _ path _ value_name =
   1.402 +  let
   1.403 +    val generatedN = "generated.sml"
   1.404 +    val driverN = "driver.sml"
   1.405 +
   1.406 +    val code_path = Path.append path (Path.basic generatedN)
   1.407 +    val driver_path = Path.append path (Path.basic driverN)
   1.408 +    val driver = 
   1.409 +      "structure Test = struct\n" ^
   1.410 +      "fun main prog_name =\n" ^
   1.411 +      "  let\n" ^
   1.412 +      "    fun format_term NONE = \"\"\n" ^ 
   1.413 +      "      | format_term (SOME t) = t ();\n" ^
   1.414 +      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.415 +      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.416 +      "    val result = " ^ value_name ^ " ();\n" ^
   1.417 +      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
   1.418 +      "    val _ = map (print o format) result;\n" ^
   1.419 +      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   1.420 +      "  in\n" ^
   1.421 +      "    0\n" ^
   1.422 +      "  end;\n" ^
   1.423 +      "end;"
   1.424 +    val cmd =
   1.425 +      "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   1.426 +      "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
   1.427 +      "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
   1.428 +  in
   1.429 +    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   1.430 +  end
   1.431 +
   1.432 +val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN
   1.433 +
   1.434 +(* Driver for OCaml *)
   1.435 +
   1.436 +val ocamlN = "OCaml"
   1.437 +val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
   1.438 +
   1.439 +fun mk_driver_ocaml _ path _ value_name =
   1.440 +  let
   1.441 +    val generatedN = "generated.ml"
   1.442 +    val driverN = "driver.ml"
   1.443 +
   1.444 +    val code_path = Path.append path (Path.basic generatedN)
   1.445 +    val driver_path = Path.append path (Path.basic driverN)
   1.446 +    val driver = 
   1.447 +      "let format_term = function\n" ^
   1.448 +      "  | None -> \"\"\n" ^ 
   1.449 +      "  | Some t -> t ();;\n" ^
   1.450 +      "let format = function\n" ^
   1.451 +      "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
   1.452 +      "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
   1.453 +      "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
   1.454 +      "let main x =\n" ^
   1.455 +      "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
   1.456 +      "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
   1.457 +      "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   1.458 +      "main ();;"
   1.459 +
   1.460 +    val compiled_path = Path.append path (Path.basic "test")
   1.461 +    val compile_cmd =
   1.462 +      Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
   1.463 +      " -I " ^ Path.implode path ^
   1.464 +      " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
   1.465 +
   1.466 +    val run_cmd = File.shell_path compiled_path
   1.467 +  in
   1.468 +    {files = [(driver_path, driver)],
   1.469 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   1.470 +  end
   1.471 +
   1.472 +val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN
   1.473 +
   1.474 +(* Driver for GHC *)
   1.475 +
   1.476 +val ghcN = "GHC"
   1.477 +val ISABELLE_GHC = "ISABELLE_GHC"
   1.478 +
   1.479 +val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
   1.480 +
   1.481 +fun mk_driver_ghc ctxt path modules value_name =
   1.482 +  let
   1.483 +    val driverN = "Main.hs"
   1.484 +
   1.485 +    fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   1.486 +    val driver_path = Path.append path (Path.basic driverN)
   1.487 +    val driver = 
   1.488 +      "module Main where {\n" ^
   1.489 +      String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   1.490 +      "main = do {\n" ^
   1.491 +      "    let {\n" ^
   1.492 +      "      format_term Nothing = \"\";\n" ^ 
   1.493 +      "      format_term (Just t) = t ();\n" ^
   1.494 +      "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   1.495 +      "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   1.496 +      "      result = " ^ value_name ^ " ();\n" ^
   1.497 +      "    };\n" ^
   1.498 +      "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
   1.499 +      "    Prelude.mapM_ (putStr . format) result;\n" ^
   1.500 +      "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
   1.501 +      "  }\n" ^
   1.502 +      "}\n"
   1.503 +
   1.504 +    val compiled_path = Path.append path (Path.basic "test")
   1.505 +    val compile_cmd =
   1.506 +      Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
   1.507 +      Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
   1.508 +      Path.implode driver_path ^ " -i" ^ Path.implode path
   1.509 +
   1.510 +    val run_cmd = File.shell_path compiled_path
   1.511 +  in
   1.512 +    {files = [(driver_path, driver)],
   1.513 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   1.514 +  end
   1.515 +
   1.516 +val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN
   1.517 +
   1.518 +(* Driver for Scala *)
   1.519 +
   1.520 +val scalaN = "Scala"
   1.521 +val ISABELLE_SCALA = "ISABELLE_SCALA"
   1.522 +
   1.523 +fun mk_driver_scala _ path _ value_name =
   1.524 +  let
   1.525 +    val generatedN = "Generated_Code"
   1.526 +    val driverN = "Driver.scala"
   1.527 +
   1.528 +    val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   1.529 +    val driver_path = Path.append path (Path.basic driverN)
   1.530 +    val driver = 
   1.531 +      "import " ^ generatedN ^ "._\n" ^
   1.532 +      "object Test {\n" ^
   1.533 +      "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   1.534 +      "    case None => \"\"\n" ^
   1.535 +      "    case Some(x) => x(())\n" ^
   1.536 +      "  }\n" ^
   1.537 +      "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
   1.538 +      "      case (true, _) => \"True\\n\"\n" ^
   1.539 +      "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
   1.540 +      "  }\n" ^
   1.541 +      "  def main(args:Array[String]) = {\n" ^
   1.542 +      "    val result = " ^ value_name ^ "(());\n" ^
   1.543 +      "    print(\"" ^ start_markerN ^ "\");\n" ^
   1.544 +      "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
   1.545 +      "    print(\"" ^ end_markerN ^ "\");\n" ^
   1.546 +      "  }\n" ^
   1.547 +      "}\n"
   1.548 +
   1.549 +    val compile_cmd =
   1.550 +      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
   1.551 +      " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
   1.552 +      File.shell_path code_path ^ " " ^ File.shell_path driver_path
   1.553 +
   1.554 +    val run_cmd =
   1.555 +      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
   1.556 +      " -cp " ^ File.shell_path path ^ " Test"
   1.557 +  in
   1.558 +    {files = [(driver_path, driver)],
   1.559 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   1.560 +  end
   1.561 +
   1.562 +val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN
   1.563 +
   1.564 +val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   1.565 +
   1.566 +val _ = 
   1.567 +  Outer_Syntax.command @{command_spec "test_code"}
   1.568 +    "compile test cases to target languages, execute them and report results"
   1.569 +      (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   1.570 +
   1.571 +val _ = Context.>> (Context.map_theory (
   1.572 +  fold add_driver
   1.573 +    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
   1.574 +     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
   1.575 +     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
   1.576 +     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
   1.577 +     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   1.578 +     (scalaN, (evaluate_in_scala, Code_Scala.target))]
   1.579 +    #> fold (fn target => Value.add_evaluator (target, eval_term target))
   1.580 +      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
   1.581 +    ))
   1.582 +end
   1.583 +