author  wenzelm 
Thu, 24 Sep 2020 15:27:24 +0200  
changeset 72285  989bd067ae30 
parent 72284  38497ecb4892 
child 72286  e4a317d00489 
permissions  rwrr 
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 successN: string 
14 
val failureN: string 

15 
val start_markerN: string 

16 
val end_markerN: string 

17 
val test_terms: Proof.context > term list > string > unit 

64580  18 
val test_code_cmd: string list > string list > Proof.context > unit 
64577  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  23 
val evaluate_in_polyml: Proof.context > (string * string) list * string > Path.T > string 
24 
val evaluate_in_mlton: Proof.context > (string * string) list * string > Path.T > string 

25 
val evaluate_in_smlnj: Proof.context > (string * string) list * string > Path.T > string 

26 
val evaluate_in_ocaml: Proof.context > (string * string) list * string > Path.T > string 

27 
val ghc_options: string Config.T 

28 
val evaluate_in_ghc: Proof.context > (string * string) list * string > Path.T > string 

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  32 
end 
33 

64577  34 
structure Code_Test: CODE_TEST = 
35 
struct 

58039  36 

37 
(* convert a list of terms into nested tuples and back *) 

64577  38 

69593  39 
fun mk_tuples [] = \<^term>\<open>()\<close> 
58039  40 
 mk_tuples [t] = t 
41 
 mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) 

42 

69593  43 
fun dest_tuples (Const (\<^const_name>\<open>Pair\<close>, _) $ l $ r) = l :: dest_tuples r 
58039  44 
 dest_tuples t = [t] 
45 

46 

47 
fun last_field sep str = 

48 
let 

64577  49 
val n = size sep 
50 
val len = size str 

58039  51 
fun find i = 
52 
if i < 0 then NONE 

53 
else if String.substring (str, i, n) = sep then SOME i 

64577  54 
else find (i  1) 
58039  55 
in 
56 
(case find (len  n) of 

57 
NONE => NONE 

58 
 SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) 

64577  59 
end 
58039  60 

61 
fun split_first_last start stop s = 

64577  62 
(case first_field start s of 
63 
NONE => NONE 

64 
 SOME (initial, rest) => 

65 
(case last_field stop rest of 

66 
NONE => NONE 

67 
 SOME (middle, tail) => SOME (initial, middle, tail))) 

58039  68 

64577  69 

70 
(* data slot for drivers *) 

58039  71 

72 
structure Drivers = Theory_Data 

73 
( 

64577  74 
type T = 
75 
(string * ((Proof.context > (string * string) list * string > Path.T > string) * string)) list 

76 
val empty = [] 

77 
val extend = I 

78 
fun merge data : T = AList.merge (op =) (K true) data 

58039  79 
) 
80 

64577  81 
val add_driver = Drivers.map o AList.update (op =) 
82 
val get_driver = AList.lookup (op =) o Drivers.get 

58039  83 

84 
(* 

85 
Test drivers must produce output of the following format: 

64577  86 

58039  87 
The start of the relevant data is marked with start_markerN, 
88 
its end with end_markerN. 

89 

90 
Between these two markers, every line corresponds to one test. 

91 
Lines of successful tests start with successN, failures start with failureN. 

92 
The failure failureN may continue with the YXML encoding of the evaluated term. 

93 
There must not be any additional whitespace in between. 

94 
*) 

95 

64577  96 

97 
(* parsing of results *) 

58039  98 

99 
val successN = "True" 

100 
val failureN = "False" 

101 
val start_markerN = "*@*Isabelle/Code_Teststart*@*" 

102 
val end_markerN = "*@*Isabelle/Code_Testend*@*" 

103 

104 
fun parse_line line = 

105 
if String.isPrefix successN line then (true, NONE) 

64577  106 
else if String.isPrefix failureN line then (false, 
58039  107 
if size line > size failureN then 
108 
String.extract (line, size failureN, NONE) 

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  111 
> dest_tuples 
112 
> SOME 

113 
else NONE) 

114 
else raise Fail ("Cannot parse result of evaluation:\n" ^ line) 

115 

116 
fun parse_result target out = 

64577  117 
(case split_first_last start_markerN end_markerN out of 
72273  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  120 

64577  121 

122 
(* pretty printing of test results *) 

58039  123 

124 
fun pretty_eval _ NONE _ = [] 

64577  125 
 pretty_eval ctxt (SOME evals) ts = 
126 
[Pretty.fbrk, 

127 
Pretty.big_list "Evaluated terms" 

128 
(map (fn (t, eval) => Pretty.block 

129 
[Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, 

130 
Syntax.pretty_term ctxt eval]) 

131 
(ts ~~ evals))] 

58039  132 

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  137 

138 
fun pretty_failures ctxt target failures = 

139 
Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) 

140 

141 

64577  142 
(* driver invocation *) 
143 

72284  144 
val debug = Attrib.setup_config_bool \<^binding>\<open>code_test_debug\<close> (K false) 
58039  145 

72284  146 
fun with_debug_dir name f = 
58039  147 
let 
72275  148 
val dir = 
64577  149 
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) 
72275  150 
val _ = Isabelle_System.mkdirs dir 
151 
in Exn.release (Exn.capture f dir) end 

58039  152 

153 
fun dynamic_value_strict ctxt t compiler = 

154 
let 

155 
val thy = Proof_Context.theory_of ctxt 

64577  156 
val (driver, target) = 
157 
(case get_driver thy compiler of 

158 
NONE => error ("No driver for target " ^ compiler) 

72272  159 
 SOME drv => drv) 
72285  160 
val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir 
72274  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  164 
fun evaluator program _ vs_ty deps = 
72274  165 
Exn.interruptible_capture eval 
64957  166 
(Code_Target.compilation_text ctxt target program deps true vs_ty) 
64578  167 
fun postproc f = map (apsnd (Option.map (map f))) 
64577  168 
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end 
58039  169 

64577  170 

171 
(* term preprocessing *) 

58039  172 

69593  173 
fun add_eval (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = add_eval t 
174 
 add_eval (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (fn acc => 

64577  175 
acc 
176 
> add_eval rhs 

177 
> add_eval lhs 

178 
> cons rhs 

179 
> cons lhs) 

69593  180 
 add_eval (Const (\<^const_name>\<open>Not\<close>, _) $ t) = add_eval t 
181 
 add_eval (Const (\<^const_name>\<open>Orderings.ord_class.less_eq\<close>, _) $ lhs $ rhs) = (fn acc => 

64577  182 
lhs :: rhs :: acc) 
69593  183 
 add_eval (Const (\<^const_name>\<open>Orderings.ord_class.less\<close>, _) $ lhs $ rhs) = (fn acc => 
64577  184 
lhs :: rhs :: acc) 
58039  185 
 add_eval _ = I 
186 

69593  187 
fun mk_term_of [] = \<^term>\<open>None :: (unit \<Rightarrow> yxml_of_term) option\<close> 
58039  188 
 mk_term_of ts = 
64577  189 
let 
190 
val tuple = mk_tuples ts 

191 
val T = fastype_of tuple 

192 
in 

69593  193 
\<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $ 
69597  194 
(absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $ 
69593  195 
(Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T > \<^typ>\<open>term\<close>) $ tuple))) 
64577  196 
end 
58039  197 

198 
fun test_terms ctxt ts target = 

199 
let 

200 
val thy = Proof_Context.theory_of ctxt 

201 

69593  202 
fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\<open>term_of\<close>) 
58039  203 

64577  204 
fun ensure_bool t = 
205 
(case fastype_of t of 

69593  206 
\<^typ>\<open>bool\<close> => () 
64579  207 
 _ => 
208 
error (Pretty.string_of 

209 
(Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1, 

210 
Syntax.pretty_term ctxt t]))) 

58039  211 

64578  212 
val _ = List.app ensure_bool ts 
58039  213 

214 
val evals = map (fn t => filter term_of (add_eval t [])) ts 

215 
val eval = map mk_term_of evals 

216 

64578  217 
val t = 
69593  218 
HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close> 
64578  219 
(map HOLogic.mk_prod (ts ~~ eval)) 
58039  220 

64577  221 
val result = dynamic_value_strict ctxt t target 
58039  222 

223 
val failed = 

224 
filter_out (fst o fst o fst) (result ~~ ts ~~ evals) 

64577  225 
handle ListPair.UnequalLengths => 
72272  226 
error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result)) 
58039  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  230 
 _ => error (Pretty.string_of (pretty_failures ctxt target failed))) 
58039  231 
end 
232 

64580  233 
fun test_code_cmd raw_ts targets ctxt = 
58039  234 
let 
64577  235 
val ts = Syntax.read_terms ctxt raw_ts 
64579  236 
val frees = fold Term.add_frees ts [] 
64578  237 
val _ = 
238 
if null frees then () 

64579  239 
else error (Pretty.string_of 
240 
(Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 :: 

72283  241 
Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees)))) 
242 
in List.app (test_terms ctxt ts) targets end 

58039  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  246 
val frees = Term.add_frees t [] 
64578  247 
val _ = 
248 
if null frees then () 

64579  249 
else 
250 
error (Pretty.string_of 

251 
(Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 :: 

72283  252 
Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees)))) 
58039  253 

64579  254 
val T = fastype_of t 
64578  255 
val _ = 
69593  256 
if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>term_of\<close>) then () 
64579  257 
else error ("Type " ^ Syntax.string_of_typ ctxt T ^ 
69593  258 
" of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\<open>term_of\<close>) 
58039  259 

64578  260 
val t' = 
69593  261 
HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close> 
262 
[HOLogic.mk_prod (\<^term>\<open>False\<close>, mk_term_of [t])] 

58039  263 

64577  264 
val result = dynamic_value_strict ctxt t' target 
265 
in (case result of [(_, SOME [t])] => t  _ => error "Evaluation failed") end 

58039  266 

64577  267 

72276
dfe150a246e6
misc tuning and clarification: prefer functions over data;
wenzelm
parents:
72275
diff
changeset

268 
(* check and invoke compiler *) 
58039  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  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  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  290 

64577  291 

292 
(* driver for PolyML *) 

58039  293 

64577  294 
val polymlN = "PolyML" 
58039  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  316 
"\"$POLYML_EXE\" use " ^ File.bash_platform_path code_path ^ 
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  324 

64577  325 

326 
(* driver for mlton *) 

58039  327 

328 
val mltonN = "MLton" 

329 
val ISABELLE_MLTON = "ISABELLE_MLTON" 

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  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\" defaulttype 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  359 

64577  360 

361 
(* driver for SML/NJ *) 

58039  362 

363 
val smlnjN = "SMLNJ" 

364 
val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" 

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  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  392 
"use " ^ ML_Syntax.print_string (File.platform_path code_path) ^ 
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  401 

64577  402 

403 
(* driver for OCaml *) 

58039  404 

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  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  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  439 

64577  440 

441 
(* driver for GHC *) 

58039  442 

443 
val ghcN = "GHC" 

444 
val ISABELLE_GHC = "ISABELLE_GHC" 

445 

69593  446 
val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "") 
58039  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  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  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  475 
File.bash_platform_path compiled_path ^ " " ^ 
476 
File.bash_platform_path driver_path ^ " i" ^ 

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  485 

64577  486 

487 
(* driver for Scala *) 

58039  488 

489 
val scalaN = "Scala" 

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  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  518 
"isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS d " ^ File.bash_platform_path dir ^ 
519 
" classpath " ^ File.bash_platform_path dir ^ " " ^ 

520 
File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path 

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  528 

64580  529 

530 
(* command setup *) 

58039  531 

64577  532 
val _ = 
69593  533 
Outer_Syntax.command \<^command_keyword>\<open>test_code\<close> 
58039  534 
"compile test cases to target languages, execute them and report results" 
69593  535 
(Scan.repeat1 Parse.prop  (\<^keyword>\<open>in\<close>  Scan.repeat1 Parse.name) 
64580  536 
>> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) 
58039  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  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  545 
val _ = 
546 
Theory.setup (fold add_driver 

547 
[(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), 

548 
(mltonN, (evaluate_in_mlton, Code_ML.target_SML)), 

549 
(smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), 

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  553 
#> fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> snd) 
64580  554 
[polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) 
59323  555 

58039  556 
end 