diff --git a/src/HOL/Library/code_test.ML b/src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML +++ b/src/HOL/Library/code_test.ML @@ -1,595 +1,564 @@ (* Title: HOL/Library/code_test.ML Author: Andreas Lochbihler, ETH Zürich Test infrastructure for the code generator. *) signature CODE_TEST = sig val add_driver: string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory val overlord: bool Config.T val successN: string val failureN: string val start_markerN: string val end_markerN: string val test_terms: Proof.context -> term list -> string -> unit 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 val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string val ghc_options: string Config.T val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string val target_Scala: string val target_Haskell: string end structure Code_Test: CODE_TEST = struct (* convert a list of terms into nested tuples and back *) fun mk_tuples [] = \<^term>\()\ | mk_tuples [t] = t | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) fun dest_tuples (Const (\<^const_name>\Pair\, _) $ l $ r) = l :: dest_tuples r | dest_tuples t = [t] fun last_field sep str = let val n = size sep val len = size str fun find i = if i < 0 then NONE else if String.substring (str, i, n) = sep then SOME i else find (i - 1) in (case find (len - n) of NONE => NONE | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) end fun split_first_last start stop s = (case first_field start s of NONE => NONE | SOME (initial, rest) => (case last_field stop rest of NONE => NONE | SOME (middle, tail) => SOME (initial, middle, tail))) (* data slot for drivers *) structure Drivers = Theory_Data ( type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list val empty = [] val extend = I fun merge data : T = AList.merge (op =) (K true) data ) val add_driver = Drivers.map o AList.update (op =) val get_driver = AList.lookup (op =) o Drivers.get (* Test drivers must produce output of the following format: The start of the relevant data is marked with start_markerN, its end with end_markerN. Between these two markers, every line corresponds to one test. Lines of successful tests start with successN, failures start with failureN. The failure failureN may continue with the YXML encoding of the evaluated term. There must not be any additional whitespace in between. *) (* parsing of results *) val successN = "True" val failureN = "False" val start_markerN = "*@*Isabelle/Code_Test-start*@*" val end_markerN = "*@*Isabelle/Code_Test-end*@*" fun parse_line line = if String.isPrefix successN line then (true, NONE) else if String.isPrefix failureN line then (false, if size line > size failureN then String.extract (line, size failureN, NONE) |> YXML.parse_body |> Term_XML.Decode.term_raw |> dest_tuples |> SOME else NONE) else raise Fail ("Cannot parse result of evaluation:\n" ^ line) fun parse_result target out = (case split_first_last start_markerN end_markerN out of NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out) | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line) (* pretty printing of test results *) fun pretty_eval _ NONE _ = [] | pretty_eval ctxt (SOME evals) ts = [Pretty.fbrk, Pretty.big_list "Evaluated terms" (map (fn (t, eval) => Pretty.block [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, Syntax.pretty_term ctxt eval]) (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)) (* driver invocation *) val overlord = Attrib.setup_config_bool \<^binding>\code_test_overlord\ (K false) fun with_overlord_dir name f = let val dir = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) val _ = Isabelle_System.mkdirs dir in Exn.release (Exn.capture f dir) end fun dynamic_value_strict ctxt t compiler = let val thy = Proof_Context.theory_of ctxt val (driver, target) = (case get_driver thy compiler of NONE => error ("No driver for target " ^ compiler) | SOME drv => drv) val debug = Config.get (Proof_Context.init_global thy) overlord val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir fun eval result = with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result)) |> parse_result compiler fun evaluator program _ vs_ty deps = Exn.interruptible_capture eval (Code_Target.compilation_text ctxt target program deps true vs_ty) fun postproc f = map (apsnd (Option.map (map f))) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (* term preprocessing *) fun add_eval (Const (\<^const_name>\Trueprop\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\HOL.eq\, _) $ lhs $ rhs) = (fn acc => acc |> add_eval rhs |> add_eval lhs |> cons rhs |> cons lhs) | add_eval (Const (\<^const_name>\Not\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\Orderings.ord_class.less_eq\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval (Const (\<^const_name>\Orderings.ord_class.less\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval _ = I fun mk_term_of [] = \<^term>\None :: (unit \ yxml_of_term) option\ | mk_term_of ts = let val tuple = mk_tuples ts val T = fastype_of tuple in \<^term>\Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option\ $ (absdummy \<^typ>\unit\ (\<^const>\yxml_string_of_term\ $ (Const (\<^const_name>\Code_Evaluation.term_of\, T --> \<^typ>\term\) $ tuple))) end fun test_terms ctxt ts target = let val thy = Proof_Context.theory_of ctxt fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\term_of\) fun ensure_bool t = (case fastype_of t of \<^typ>\bool\ => () | _ => error (Pretty.string_of (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1, Syntax.pretty_term ctxt t]))) val _ = List.app ensure_bool ts val evals = map (fn t => filter term_of (add_eval t [])) ts val eval = map mk_term_of evals val t = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ (map HOLogic.mk_prod (ts ~~ eval)) val result = dynamic_value_strict ctxt t target val failed = filter_out (fst o fst o fst) (result ~~ ts ~~ evals) 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 fun test_targets ctxt = List.app o test_terms ctxt fun pretty_free ctxt = Syntax.pretty_term ctxt o Free fun test_code_cmd raw_ts targets ctxt = let val ts = Syntax.read_terms ctxt raw_ts val frees = fold Term.add_frees ts [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_free ctxt) frees)))) in test_targets ctxt ts targets end fun eval_term target ctxt t = let val frees = Term.add_frees t [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_free ctxt) frees)))) val T = fastype_of t val _ = if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\term_of\) then () else error ("Type " ^ Syntax.string_of_typ ctxt T ^ " of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\term_of\) val t' = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ [HOLogic.mk_prod (\<^term>\False\, mk_term_of [t])] val result = dynamic_value_strict ctxt t' target in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end -(* generic driver *) - -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."))) - | _ => ())) +(* check and invoke compiler *) - 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 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 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 +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 - 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 *) 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 *) 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 *) 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 *) val _ = Outer_Syntax.command \<^command_keyword>\test_code\ "compile test cases to target languages, execute them and report results" (Scan.repeat1 Parse.prop -- (\<^keyword>\in\ |-- Scan.repeat1 Parse.name) >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) 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) [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) end