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