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