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