# HG changeset patch # User wenzelm # Date 1601111869 -7200 # Node ID d144038fa88aa4a96e3ac1769940a15e47e0d460 # Parent 6f0e85e16d8498dc9c2ddf211d37d783cd176b1e tuned; diff -r 6f0e85e16d84 -r d144038fa88a src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Fri Sep 25 17:13:12 2020 +0100 +++ b/src/HOL/Library/code_test.ML Sat Sep 26 11:17:49 2020 +0200 @@ -273,7 +273,7 @@ ("Environment variable " ^ var ^ " is not set. To test code generation with " ^ compiler ^ ", set this variable to your " ^ descr ^ " in the $ISABELLE_HOME_USER/etc/settings file."))) - else (); + else () fun compile compiler cmd = let val (out, ret) = Isabelle_System.bash_output cmd in @@ -299,7 +299,7 @@ val driver_path = Path.append dir (Path.basic "driver.sml") val out_path = Path.append dir (Path.basic "out") - val code = #2 (the_single code_files); + val code = #2 (the_single code_files) val driver = \<^verbatim>\ fun main () = let @@ -316,18 +316,17 @@ val _ = BinIO.closeOut out in () end; \ - in - File.write code_path code; - File.write driver_path driver; - ML_Context.eval - {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE, - writeln = writeln, warning = warning} - Position.none - (ML_Lex.read_text (code, Path.position code_path) @ - ML_Lex.read_text (driver, Path.position driver_path) @ - ML_Lex.read "main ()"); - File.read out_path - end + val _ = File.write code_path code + val _ = File.write driver_path driver + val _ = + ML_Context.eval + {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE, + writeln = writeln, warning = warning} + Position.none + (ML_Lex.read_text (code, Path.position code_path) @ + ML_Lex.read_text (driver, Path.position driver_path) @ + ML_Lex.read "main ()") + in File.read out_path end (* driver for mlton *) @@ -354,13 +353,12 @@ val _ = List.app (print o format) result val _ = print \ ^ ML_Syntax.print_string end_markerN ^ \<^verbatim>\ \ - val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path + val _ = check_settings compiler ISABELLE_MLTON "MLton executable" + val _ = List.app (File.write code_path o snd) code_files + val _ = File.write driver_path driver + val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN) in - check_settings compiler ISABELLE_MLTON "MLton executable"; - List.app (File.write code_path o snd) code_files; - File.write driver_path driver; - File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN); - compile compiler cmd; + compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path); evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN))) end @@ -393,17 +391,15 @@ in 0 end end \ + val _ = check_settings compiler ISABELLE_SMLNJ "SMLNJ executable" + val _ = List.app (File.write code_path o snd) code_files + val _ = File.write driver_path driver val ml_source = "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^ "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^ "; Test.main ();" - in - check_settings compiler ISABELLE_SMLNJ "SMLNJ executable"; - List.app (File.write code_path o snd) code_files; - File.write driver_path driver; - evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") - end + in evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") end (* driver for OCaml *) @@ -431,17 +427,15 @@ " print_string \"" ^ end_markerN ^ "\";;\n" ^ "main ();;" val compiled_path = Path.append dir (Path.basic "test") + + val _ = check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable" + val _ = List.app (File.write code_path o snd) code_files + val _ = File.write driver_path driver val cmd = "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " File.write (Path.append dir (Path.basic name)) code) code_files + val _ = File.write driver_path driver + val compiled_path = Path.append dir (Path.basic "test") val cmd = "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ @@ -481,13 +479,7 @@ File.bash_platform_path compiled_path ^ " " ^ File.bash_platform_path driver_path ^ " -i" ^ File.bash_platform_path dir - in - check_settings compiler ISABELLE_GHC "GHC executable"; - List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files; - File.write driver_path driver; - compile compiler cmd; - evaluate compiler (File.bash_path compiled_path) - end + in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end (* driver for Scala *) @@ -503,7 +495,7 @@ val driver_path = Path.append dir (Path.basic driverN) val out_path = Path.append dir (Path.basic "out") - val code = #2 (the_single code_files); + val code = #2 (the_single code_files) val driver = \<^verbatim>\ { val result = \ ^ value_name ^ \<^verbatim>\(()) @@ -518,12 +510,10 @@ isabelle.Path.explode(\ ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\), \ ^ quote start_markerN ^ \<^verbatim>\ + result_text + \ ^ quote end_markerN ^ \<^verbatim>\) }\ - in - File.write code_path code; - File.write driver_path driver; - Scala_Compiler.toplevel true (code ^ driver); - File.read out_path - end + val _ = File.write code_path code + val _ = File.write driver_path driver + val _ = Scala_Compiler.toplevel true (code ^ driver) + in File.read out_path end (* command setup *) @@ -537,19 +527,18 @@ val target_Scala = "Scala_eval" val target_Haskell = "Haskell_eval" -val _ = Theory.setup - (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) - #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)])) - val _ = - Theory.setup (fold add_driver - [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), - (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), - (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), - (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), - (ghcN, (evaluate_in_ghc, target_Haskell)), - (scalaN, (evaluate_in_scala, target_Scala))] - #> fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> snd) + Theory.setup + (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) #> + Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]) #> + fold add_driver + [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), + (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), + (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), + (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), + (ghcN, (evaluate_in_ghc, target_Haskell)), + (scalaN, (evaluate_in_scala, target_Scala))] #> + fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> #2) [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) end