# HG changeset patch # User wenzelm # Date 1600623405 -7200 # Node ID dfe150a246e6ebac168427beeec689e81c7a2e84 # Parent f7189b7f5567fb59d682c47dad325d6d31b19107 misc tuning and clarification: prefer functions over data; diff -r f7189b7f5567 -r dfe150a246e6 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Sun Sep 20 12:21:54 2020 +0200 +++ b/src/HOL/Library/code_test.ML Sun Sep 20 19:36:45 2020 +0200 @@ -18,13 +18,9 @@ val test_targets: Proof.context -> term list -> string list -> unit val test_code_cmd: string list -> string list -> Proof.context -> unit val eval_term: string -> Proof.context -> term -> term - val evaluate: (string * string) option -> string -> - (Proof.context -> Path.T -> string list -> string -> - {files: (Path.T * string) list, - compile_cmd: string, - run_cmd: string, - mk_code_file: string -> Path.T}) -> Proof.context -> - (string * string) list * string -> Path.T -> string + val check_settings: string -> string -> string -> unit + val compile: string -> string -> unit + val evaluate: string -> string -> string val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string @@ -136,9 +132,9 @@ (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = - Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") - @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] - @ pretty_eval ctxt evals eval_ts) + Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ + [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @ + pretty_eval ctxt evals eval_ts) fun pretty_failures ctxt target failures = Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) @@ -231,8 +227,8 @@ handle ListPair.UnequalLengths => error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result)) in - (case failed of [] => - () + (case failed of + [] => () | _ => error (Pretty.string_of (pretty_failures ctxt target failed))) end @@ -275,86 +271,62 @@ in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end -(* generic driver *) +(* check and invoke compiler *) -fun evaluate opt_env_var compilerN mk_driver (ctxt: Proof.context) (code_files, value_name) = - let - val _ = - (case opt_env_var of - NONE => () - | SOME (env_var, env_var_dest) => - (case getenv env_var of - "" => - error (Pretty.string_of (Pretty.para - ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^ - compilerN ^ ", set this variable to your " ^ env_var_dest ^ - " in the $ISABELLE_HOME_USER/etc/settings file."))) - | _ => ())) +fun check_settings compiler var descr = + if getenv var = "" then + error (Pretty.string_of (Pretty.para + ("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 (); - fun compile "" = () - | compile cmd = - let - val (out, ret) = Isabelle_System.bash_output cmd - in - if ret = 0 then () - else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out) - end +fun compile compiler cmd = + let val (out, ret) = Isabelle_System.bash_output cmd in + if ret = 0 then () + else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out) + end - fun run dir = - let - val modules = map fst code_files - val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt dir modules value_name - - val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files - val _ = List.app (fn (name, content) => File.write name content) files - - val _ = compile compile_cmd - - val (out, res) = Isabelle_System.bash_output run_cmd - val _ = - if res = 0 then () - else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ - string_of_int res ^ "\nCompiler output:\n" ^ out) - in out end - in run end +fun evaluate compiler cmd = + let val (out, res) = Isabelle_System.bash_output cmd in + if res = 0 then out + else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^ + string_of_int res ^ "\nCompiler output:\n" ^ out) + end (* driver for PolyML *) val polymlN = "PolyML" -val evaluate_in_polyml = - evaluate NONE polymlN - (fn _ => fn dir => fn _ => fn value_name => - let - val generatedN = "generated.sml" - val driverN = "driver.sml" - - val code_path = Path.append dir (Path.basic generatedN) - val driver_path = Path.append dir (Path.basic driverN) - val driver = - "fun main prog_name = \n" ^ - " let\n" ^ - " fun format_term NONE = \"\"\n" ^ - " | format_term (SOME t) = t ();\n" ^ - " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ - " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ - " val result = " ^ value_name ^ " ();\n" ^ - " val _ = print \"" ^ start_markerN ^ "\";\n" ^ - " val _ = map (print o format) result;\n" ^ - " val _ = print \"" ^ end_markerN ^ "\";\n" ^ - " in\n" ^ - " ()\n" ^ - " end;\n" - in - {files = [(driver_path, driver)], - compile_cmd = "", - run_cmd = - "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^ - " --use " ^ Bash.string (File.platform_path driver_path) ^ - " --eval " ^ Bash.string "main ()", - mk_code_file = K code_path} - end) +fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir = + let + val compiler = polymlN + val code_path = Path.append dir (Path.basic "generated.sml") + val driver_path = Path.append dir (Path.basic "driver.sml") + val driver = + "fun main prog_name = \n" ^ + " let\n" ^ + " fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + " val result = " ^ value_name ^ " ();\n" ^ + " val _ = print \"" ^ start_markerN ^ "\";\n" ^ + " val _ = map (print o format) result;\n" ^ + " val _ = print \"" ^ end_markerN ^ "\";\n" ^ + " in\n" ^ + " ()\n" ^ + " end;\n"; + val cmd = + "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^ + " --use " ^ Bash.string (File.platform_path driver_path) ^ + " --eval " ^ Bash.string "main ()" + in + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + evaluate compiler cmd + end (* driver for mlton *) @@ -362,36 +334,34 @@ val mltonN = "MLton" val ISABELLE_MLTON = "ISABELLE_MLTON" -val evaluate_in_mlton = - evaluate (SOME (ISABELLE_MLTON, "MLton executable")) mltonN - (fn _ => fn dir => fn _ => fn value_name => - let - val generatedN = "generated.sml" - val driverN = "driver.sml" - val projectN = "test" - val ml_basisN = projectN ^ ".mlb" +fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir = + let + val compiler = mltonN + val generatedN = "generated.sml" + val driverN = "driver.sml" + val projectN = "test" - val code_path = Path.append dir (Path.basic generatedN) - val driver_path = Path.append dir (Path.basic driverN) - val ml_basis_path = Path.append dir (Path.basic ml_basisN) - val driver = - "fun format_term NONE = \"\"\n" ^ - " | format_term (SOME t) = t ();\n" ^ - "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ - " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ - "val result = " ^ value_name ^ " ();\n" ^ - "val _ = print \"" ^ start_markerN ^ "\";\n" ^ - "val _ = map (print o format) result;\n" ^ - "val _ = print \"" ^ end_markerN ^ "\";\n" - val ml_basis = "$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN - in - {files = [(driver_path, driver), (ml_basis_path, ml_basis)], - compile_cmd = - File.bash_path (Path.variable ISABELLE_MLTON) ^ - " -default-type intinf " ^ File.bash_path ml_basis_path, - run_cmd = File.bash_path (Path.append dir (Path.basic projectN)), - mk_code_file = K code_path} - end) + val code_path = Path.append dir (Path.basic generatedN) + val driver_path = Path.append dir (Path.basic driverN) + val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb")) + val driver = + "fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + "val result = " ^ value_name ^ " ();\n" ^ + "val _ = print \"" ^ start_markerN ^ "\";\n" ^ + "val _ = map (print o format) result;\n" ^ + "val _ = print \"" ^ end_markerN ^ "\";\n" + val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path + 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; + evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN))) + end (* driver for SML/NJ *) @@ -399,43 +369,41 @@ val smlnjN = "SMLNJ" val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" -val evaluate_in_smlnj = - evaluate (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN - (fn _ => fn dir => fn _ => fn value_name => - let - val generatedN = "generated.sml" - val driverN = "driver.sml" +fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir = + let + val compiler = smlnjN + val generatedN = "generated.sml" + val driverN = "driver.sml" - val code_path = Path.append dir (Path.basic generatedN) - val driver_path = Path.append dir (Path.basic driverN) - val driver = - "structure Test = struct\n" ^ - "fun main prog_name =\n" ^ - " let\n" ^ - " fun format_term NONE = \"\"\n" ^ - " | format_term (SOME t) = t ();\n" ^ - " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ - " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ - " val result = " ^ value_name ^ " ();\n" ^ - " val _ = print \"" ^ start_markerN ^ "\";\n" ^ - " val _ = map (print o format) result;\n" ^ - " val _ = print \"" ^ end_markerN ^ "\";\n" ^ - " in\n" ^ - " 0\n" ^ - " end;\n" ^ - "end;" - val ml_source = - "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ - "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^ - "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^ - "; Test.main ();" - val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"" - in - {files = [(driver_path, driver)], - compile_cmd = "", - run_cmd = cmd, - mk_code_file = K code_path} - end) + val code_path = Path.append dir (Path.basic generatedN) + val driver_path = Path.append dir (Path.basic driverN) + val driver = + "structure Test = struct\n" ^ + "fun main prog_name =\n" ^ + " let\n" ^ + " fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + " val result = " ^ value_name ^ " ();\n" ^ + " val _ = print \"" ^ start_markerN ^ "\";\n" ^ + " val _ = map (print o format) result;\n" ^ + " val _ = print \"" ^ end_markerN ^ "\";\n" ^ + " in\n" ^ + " 0\n" ^ + " end;\n" ^ + "end;" + val ml_source = + "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ + "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^ + "; use " ^ ML_Syntax.print_string (Bash.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 (* driver for OCaml *) @@ -443,39 +411,37 @@ val ocamlN = "OCaml" val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND" -val evaluate_in_ocaml = - evaluate (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN - (fn _ => fn dir => fn _ => fn value_name => - let - val generatedN = "generated.ml" - val driverN = "driver.ml" +fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir = + let + val compiler = ocamlN - val code_path = Path.append dir (Path.basic generatedN) - val driver_path = Path.append dir (Path.basic driverN) - val driver = - "let format_term = function\n" ^ - " | None -> \"\"\n" ^ - " | Some t -> t ();;\n" ^ - "let format = function\n" ^ - " | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^ - " | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^ - "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^ - "let main x =\n" ^ - " let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^ - " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ - " print_string \"" ^ end_markerN ^ "\";;\n" ^ - "main ();;" - - val compiled_path = Path.append dir (Path.basic "test") - in - {files = [(driver_path, driver)], - compile_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 ^ " \"\"\n" ^ + " | Some t -> t ();;\n" ^ + "let format = function\n" ^ + " | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^ + " | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^ + "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^ + "let main x =\n" ^ + " let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^ + " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ + " print_string \"" ^ end_markerN ^ "\";;\n" ^ + "main ();;" + val compiled_path = Path.append dir (Path.basic "test") + 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 ^ " \code_test_ghc\ (K "") -val evaluate_in_ghc = - evaluate (SOME (ISABELLE_GHC, "GHC executable")) ghcN - (fn ctxt => fn dir => fn modules => fn value_name => - let - val driverN = "Main.hs" +fun evaluate_in_ghc ctxt (code_files, value_name) dir = + let + val compiler = ghcN + val modules = map fst code_files - fun mk_code_file name = Path.append dir (Path.basic name) - val driver_path = Path.append dir (Path.basic driverN) - val driver = - "module Main where {\n" ^ - implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ - "main = do {\n" ^ - " let {\n" ^ - " format_term Nothing = \"\";\n" ^ - " format_term (Just t) = t ();\n" ^ - " format (True, _) = \"" ^ successN ^ "\\n\";\n" ^ - " format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^ - " result = " ^ value_name ^ " ();\n" ^ - " };\n" ^ - " Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^ - " Prelude.mapM_ (putStr . format) result;\n" ^ - " Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^ - " }\n" ^ - "}\n" + val driver_path = Path.append dir (Path.basic "Main.hs") + val driver = + "module Main where {\n" ^ + implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ + "main = do {\n" ^ + " let {\n" ^ + " format_term Nothing = \"\";\n" ^ + " format_term (Just t) = t ();\n" ^ + " format (True, _) = \"" ^ successN ^ "\\n\";\n" ^ + " format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^ + " result = " ^ value_name ^ " ();\n" ^ + " };\n" ^ + " Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^ + " Prelude.mapM_ (putStr . format) result;\n" ^ + " Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^ + " }\n" ^ + "}\n" - val compiled_path = Path.append dir (Path.basic "test") - in - {files = [(driver_path, driver)], - compile_cmd = - "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ - Config.get ctxt ghc_options ^ " -o " ^ - Bash.string (File.platform_path compiled_path) ^ " " ^ - Bash.string (File.platform_path driver_path) ^ " -i" ^ - Bash.string (File.platform_path dir), - run_cmd = File.bash_path compiled_path, - mk_code_file = mk_code_file} - end) + val compiled_path = Path.append dir (Path.basic "test") + val cmd = + "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ + Config.get ctxt ghc_options ^ " -o " ^ + Bash.string (File.platform_path compiled_path) ^ " " ^ + Bash.string (File.platform_path driver_path) ^ " -i" ^ + Bash.string (File.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 (* driver for Scala *) val scalaN = "Scala" -val evaluate_in_scala = evaluate NONE scalaN - (fn _ => fn dir => fn _ => fn value_name => - let - val generatedN = "Generated_Code" - val driverN = "Driver.scala" +fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir = + let + val compiler = scalaN + val generatedN = "Generated_Code" + val driverN = "Driver.scala" - val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) - val driver_path = Path.append dir (Path.basic driverN) - val driver = - "import " ^ generatedN ^ "._\n" ^ - "object Test {\n" ^ - " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ - " case None => \"\"\n" ^ - " case Some(x) => x(())\n" ^ - " }\n" ^ - " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^ - " case (true, _) => \"True\\n\"\n" ^ - " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^ - " }\n" ^ - " def main(args:Array[String]) = {\n" ^ - " val result = " ^ value_name ^ "(());\n" ^ - " print(\"" ^ start_markerN ^ "\");\n" ^ - " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^ - " print(\"" ^ end_markerN ^ "\");\n" ^ - " }\n" ^ - "}\n" - in - {files = [(driver_path, driver)], - compile_cmd = - "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path dir) ^ - " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^ - Bash.string (File.platform_path code_path) ^ " " ^ - Bash.string (File.platform_path driver_path), - run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path dir) ^ " Test", - mk_code_file = K code_path} - end) + val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) + val driver_path = Path.append dir (Path.basic driverN) + val driver = + "import " ^ generatedN ^ "._\n" ^ + "object Test {\n" ^ + " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ + " case None => \"\"\n" ^ + " case Some(x) => x(())\n" ^ + " }\n" ^ + " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^ + " case (true, _) => \"True\\n\"\n" ^ + " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^ + " }\n" ^ + " def main(args:Array[String]) = {\n" ^ + " val result = " ^ value_name ^ "(());\n" ^ + " print(\"" ^ start_markerN ^ "\");\n" ^ + " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^ + " print(\"" ^ end_markerN ^ "\");\n" ^ + " }\n" ^ + "}\n" + val compile_cmd = + "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path dir) ^ + " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^ + Bash.string (File.platform_path code_path) ^ " " ^ + Bash.string (File.platform_path driver_path) + val run_cmd = + "isabelle_scala scala -cp " ^ Bash.string (File.platform_path dir) ^ " Test" + in + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + compile compiler compile_cmd; + evaluate compiler run_cmd + end (* command setup *)