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