494 |
494 |
495 (* driver for Scala *) |
495 (* driver for Scala *) |
496 |
496 |
497 val scalaN = "Scala" |
497 val scalaN = "Scala" |
498 |
498 |
499 fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir = |
499 fun evaluate_in_scala ctxt (code_files, value_name) dir = |
500 let |
500 let |
501 val compiler = scalaN |
|
502 val generatedN = "Generated_Code" |
501 val generatedN = "Generated_Code" |
503 val driverN = "Driver.scala" |
502 val driverN = "Driver.scala" |
504 |
503 |
|
504 val code = #2 (the_single code_files); |
505 val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) |
505 val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) |
506 val driver_path = Path.append dir (Path.basic driverN) |
506 val driver_path = Path.append dir (Path.basic driverN) |
507 val driver = |
507 val out_path = Path.append dir (Path.basic "out") |
508 "import " ^ generatedN ^ "._\n" ^ |
508 val driver = \<^verbatim>\<open> |
509 "object Test {\n" ^ |
509 { |
510 " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ |
510 val result = \<close> ^ value_name ^ \<^verbatim>\<open>(()) |
511 " case None => \"\"\n" ^ |
511 val result_text = |
512 " case Some(x) => x(())\n" ^ |
512 result.map( |
513 " }\n" ^ |
513 { |
514 " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^ |
514 case (true, _) => "True\n" |
515 " case (true, _) => \"True\\n\"\n" ^ |
515 case (false, None) => "False\n" |
516 " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^ |
516 case (false, Some(t)) => "False" + t(()) + "\n" |
517 " }\n" ^ |
517 }).mkString |
518 " def main(args:Array[String]) = {\n" ^ |
518 isabelle.File.write( |
519 " val result = " ^ value_name ^ "(());\n" ^ |
519 isabelle.Path.explode(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>), |
520 " print(\"" ^ start_markerN ^ "\");\n" ^ |
520 \<close> ^ quote start_markerN ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_markerN ^ \<^verbatim>\<open>) |
521 " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^ |
521 }\<close> |
522 " print(\"" ^ end_markerN ^ "\");\n" ^ |
522 in |
523 " }\n" ^ |
523 if Config.get ctxt debug |
524 "}\n" |
524 then (File.write code_path code; File.write driver_path driver) |
525 val compile_cmd = |
525 else (); |
526 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_platform_path dir ^ |
526 Scala_Compiler.toplevel true (code ^ driver); |
527 " -classpath " ^ File.bash_platform_path dir ^ " " ^ |
527 File.read out_path |
528 File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path |
|
529 val run_cmd = "isabelle_scala scala -cp " ^ File.bash_platform_path dir ^ " Test" |
|
530 in |
|
531 List.app (File.write code_path o snd) code_files; |
|
532 File.write driver_path driver; |
|
533 compile compiler compile_cmd; |
|
534 evaluate compiler run_cmd |
|
535 end |
528 end |
536 |
529 |
537 |
530 |
538 (* command setup *) |
531 (* command setup *) |
539 |
532 |