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