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