# HG changeset patch # User Andreas Lochbihler # Date 1408952450 -7200 # Node ID 469a375212c17691ddd1df0c40d52e1f0a138a60 # Parent f8e6197668c96c533173333c4cabde234b448e7a add testing framework for generated code diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,148 @@ +(* Title: Code_Test.thy + Author: Andreas Lochbihler, ETH Zurich + +Test infrastructure for the code generator +*) + +theory Code_Test +imports Main +keywords "test_code" "eval_term" :: diag +begin + +subsection {* YXML encoding for @{typ Code_Evaluation.term} *} + +datatype yxml_of_term = YXML + +lemma yot_anything: "x = (y :: yxml_of_term)" +by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp) + +definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML" +definition yot_literal :: "String.literal \ yxml_of_term" + where [code del]: "yot_literal _ = YXML" +definition yot_append :: "yxml_of_term \ yxml_of_term \ yxml_of_term" + where [code del]: "yot_append _ _ = YXML" +definition yot_concat :: "yxml_of_term list \ yxml_of_term" + where [code del]: "yot_concat _ = YXML" + +text {* Serialise @{typ yxml_of_term} to native string of target language *} + +code_printing type_constructor yxml_of_term + \ (SML) "string" + and (OCaml) "string" + and (Haskell) "String" + and (Scala) "String" +| constant yot_empty + \ (SML) "\"\"" + and (OCaml) "\"\"" + and (Haskell) "\"\"" + and (Scala) "\"\"" +| constant yot_literal + \ (SML) "_" + and (OCaml) "_" + and (Haskell) "_" + and (Scala) "_" +| constant yot_append + \ (SML) "String.concat [(_), (_)]" + and (OCaml) "String.concat \"\" [(_); (_)]" + and (Haskell) infixr 5 "++" + and (Scala) infixl 5 "+" +| constant yot_concat + \ (SML) "String.concat" + and (OCaml) "String.concat \"\"" + and (Haskell) "Prelude.concat" + and (Scala) "_.mkString(\"\")" + +text {* + Stripped-down implementations of Isabelle's XML tree with YXML encoding + as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"} + sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}. +*} + +datatype xml_tree = XML_Tree + +lemma xml_tree_anything: "x = (y :: xml_tree)" +by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp) + +context begin +local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *} + +type_synonym attributes = "(String.literal \ String.literal) list" +type_synonym body = "xml_tree list" + +definition Elem :: "String.literal \ attributes \ xml_tree list \ xml_tree" +where [code del]: "Elem _ _ _ = XML_Tree" + +definition Text :: "String.literal \ xml_tree" +where [code del]: "Text _ = XML_Tree" + +definition node :: "xml_tree list \ xml_tree" +where "node ts = Elem (STR '':'') [] ts" + +definition tagged :: "String.literal \ String.literal option \ xml_tree list \ xml_tree" +where "tagged tag x ts = Elem tag (case x of None \ [] | Some x' \ [(STR ''0'', x')]) ts" + +definition list where "list f xs = map (node \ f) xs" + +definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])" +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])" +definition XY :: yxml_of_term where "XY = yot_append X Y" +definition XYX :: yxml_of_term where "XYX = yot_append XY X" + +end + +code_datatype xml.Elem xml.Text + +definition yxml_string_of_xml_tree :: "xml_tree \ yxml_of_term \ yxml_of_term" +where [code del]: "yxml_string_of_xml_tree _ _ = YXML" + +lemma yxml_string_of_xml_tree_code [code]: + "yxml_string_of_xml_tree (xml.Elem name atts ts) rest = + yot_append xml.XY ( + yot_append (yot_literal name) ( + foldr (\(a, x) rest. + yot_append xml.Y ( + yot_append (yot_literal a) ( + yot_append (yot_literal (STR ''='')) ( + yot_append (yot_literal x) rest)))) atts ( + foldr yxml_string_of_xml_tree ts ( + yot_append xml.XYX rest))))" + "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest" +by(rule yot_anything)+ + +definition yxml_string_of_body :: "xml.body \ yxml_of_term" +where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty" + +text {* + Encoding @{typ Code_Evaluation.term} into XML trees + as defined in @{file "~~/src/Pure/term_xml.ML"} +*} + +definition xml_of_typ :: "Typerep.typerep \ xml.body" +where [code del]: "xml_of_typ _ = [XML_Tree]" + +definition xml_of_term :: "Code_Evaluation.term \ xml.body" +where [code del]: "xml_of_term _ = [XML_Tree]" + +lemma xml_of_typ_code [code]: + "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]" +by(simp add: xml_of_typ_def xml_tree_anything) + +lemma xml_of_term_code [code]: + "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]" + "xml_of_term (Code_Evaluation.App t1 t2) = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]" + "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]" + -- {* + FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent + uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. + *} + "xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]" +by(simp_all add: xml_of_term_def xml_tree_anything) + +definition yxml_string_of_term :: "Code_Evaluation.term \ yxml_of_term" +where "yxml_string_of_term = yxml_string_of_body \ xml_of_term" + +subsection {* Test engine and drivers *} + +ML_file "code_test.ML" + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,15 @@ +(* Title: Code_Test_GHC.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on GHC +*) + +theory Code_Test_GHC imports Code_Test begin + +definition id_integer :: "integer \ integer" where "id_integer = id" + +test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC + +eval_term "14 + 7 * -12 :: integer" in GHC + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_MLton.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_MLtonL.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on MLton +*) + +theory Code_Test_MLton imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton + +eval_term "14 + 7 * -12 :: integer" in MLton + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_OCaml.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on OCaml +*) + +theory Code_Test_OCaml imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml + +eval_term "14 + 7 * -12 :: integer" in OCaml + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_PolyML.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on PolyML +*) + +theory Code_Test_PolyML imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML + +eval_term "14 + 7 * -12 :: integer" in PolyML + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_SMLNJ.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on SMLNJ +*) + +theory Code_Test_SMLNJ imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ + +eval_term "14 + 7 * -12 :: integer" in SMLNJ + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_Scala.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on Scala +*) + +theory Code_Test_Scala imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala + +eval_term "14 + 7 * -12 :: integer" in Scala + +end diff -r f8e6197668c9 -r 469a375212c1 src/HOL/Codegenerator_Test/code_test.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/code_test.ML Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,594 @@ +(* Title: Code_Test.ML + Author: Andreas Lochbihler, ETH Zurich + +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 get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option + 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 list + val test_code_cmd : string list -> string list -> Toplevel.state -> unit + + val eval_term : Proof.context -> term -> string -> unit + + val gen_driver : + (theory -> Path.T -> string list -> string -> + {files : (Path.T * string) list, + compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T}) + -> string -> string -> string + -> theory -> (string * string) list * string -> Path.T -> string + + val ISABELLE_POLYML_PATH : string + val polymlN : string + val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string + + val mltonN : string + val ISABELLE_MLTON : string + val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string + + val smlnjN : string + val ISABELLE_SMLNJ : string + val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string + + val ocamlN : string + val ISABELLE_OCAMLC : string + val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string + + val ghcN : string + val ISABELLE_GHC : string + val ghc_options : string Config.T + val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string + + val scalaN : string + val ISABELLE_SCALA : string + val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> 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 map_option _ NONE = NONE + | map_option f (SOME x) = SOME (f x) + +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 + |> 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 ^ "!\nBash output:\n" ^ out) + | SOME (_, middle, _) => middle |> trim_line |> 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) + +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 path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) + val _ = Isabelle_System.mkdirs path; + in + Exn.release (Exn.capture f path) + 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 f => f; + 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 evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler + fun evaluator program _ vs_ty deps = + Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty); + fun postproc f = map (apsnd (map_option (map f))) + in + Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result 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 ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)) + + val _ = map 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_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) + val t = HOLogic.mk_list T (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: " ^ Int.toString (length result)) + val _ = case failed of [] => () + | _ => error (Pretty.string_of (pretty_failures ctxt target failed)) + in + () + end + +fun test_targets ctxt = map o test_terms ctxt + +fun test_code_cmd raw_ts targets state = + let + val ctxt = Toplevel.context_of state; + val ts = Syntax.read_terms ctxt raw_ts; + val frees = fold Term.add_free_names ts [] + val _ = if frees = [] then () else + error ("Terms contain free variables: " ^ + Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees)))) + in + test_targets ctxt ts targets; () + end + + +fun eval_term ctxt t target = + let + val thy = Proof_Context.theory_of ctxt + + val T_t = fastype_of t + val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error + ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ + " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of})) + + val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) + val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])] + + val result = dynamic_value_strict ctxt t' target; + val t_eval = case result of [(_, SOME [t])] => t | _ => error "Evaluation failed" + in + Pretty.writeln (Syntax.pretty_term ctxt t_eval) + end + +fun eval_term_cmd raw_t target state = + let + val ctxt = Toplevel.context_of state; + val t = Syntax.read_term ctxt raw_t; + val frees = Term.add_free_names t [] + val _ = if frees = [] then () else + error ("Term contains free variables: " ^ + Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees)))) + in + eval_term ctxt t target + end + + +(* Generic driver *) + +fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) = + let + val compiler = getenv env_var + val _ = if compiler <> "" then () else 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 settings file."))) + + fun compile NONE = () + | compile (SOME 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 run (path : Path.T)= + let + val modules = map fst code_files + val {files, compile_cmd, run_cmd, mk_code_file} + = mk_driver ctxt path modules value_name + + val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files + val _ = map (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 " ^ Int.toString res ^ + "\nBash output:\n" ^ out) + in + out + end + in + run + end + +(* Driver for PolyML *) + +val ISABELLE_POLYML_PATH = "ISABELLE_POLYML_PATH" +val polymlN = "PolyML"; + +fun mk_driver_polyml _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (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" + val cmd = + "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ + Path.implode driver_path ^ "\\\"; main ();\" | " ^ + Path.implode (Path.variable ISABELLE_POLYML_PATH) + in + {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + end + +val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML_PATH "PolyML executable" polymlN + +(* Driver for mlton *) + +val mltonN = "MLton" +val ISABELLE_MLTON = "ISABELLE_MLTON" + +fun mk_driver_mlton _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + val projectN = "test" + val ml_basisN = projectN ^ ".mlb" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (Path.basic driverN) + val ml_basis_path = Path.append path (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 + + val compile_cmd = + File.shell_path (Path.variable ISABELLE_MLTON) ^ + " -default-type intinf " ^ File.shell_path ml_basis_path + val run_cmd = File.shell_path (Path.append path (Path.basic projectN)) + in + {files = [(driver_path, driver), (ml_basis_path, ml_basis)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN + +(* Driver for SML/NJ *) + +val smlnjN = "SMLNJ" +val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" + +fun mk_driver_smlnj _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (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 cmd = + "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ + "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^ + "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ) + in + {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + end + +val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN + +(* Driver for OCaml *) + +val ocamlN = "OCaml" +val ISABELLE_OCAMLC = "ISABELLE_OCAMLC" + +fun mk_driver_ocaml _ path _ value_name = + let + val generatedN = "generated.ml" + val driverN = "driver.ml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (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 path (Path.basic "test") + val compile_cmd = + Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^ + " -I " ^ Path.implode path ^ + " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path + + val run_cmd = File.shell_path compiled_path + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN + +(* Driver for GHC *) + +val ghcN = "GHC" +val ISABELLE_GHC = "ISABELLE_GHC" + +val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "") + +fun mk_driver_ghc ctxt path modules value_name = + let + val driverN = "Main.hs" + + fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs")) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "module Main where {\n" ^ + String.concat (map (fn module => "import qualified " ^ 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 path (Path.basic "test") + val compile_cmd = + Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^ + Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^ + Path.implode driver_path ^ " -i" ^ Path.implode path + + val run_cmd = File.shell_path compiled_path + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file} + end + +val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN + +(* Driver for Scala *) + +val scalaN = "Scala" +val ISABELLE_SCALA = "ISABELLE_SCALA" + +fun mk_driver_scala _ path _ value_name = + let + val generatedN = "Generated_Code" + val driverN = "Driver.scala" + + val code_path = Path.append path (Path.basic (generatedN ^ ".scala")) + val driver_path = Path.append path (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 = + Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^ + " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^ + File.shell_path code_path ^ " " ^ File.shell_path driver_path + + val run_cmd = + Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^ + " -cp " ^ File.shell_path path ^ " Test" + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN + +val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) + +val _ = + Outer_Syntax.command @{command_spec "test_code"} + "compile test cases to target languages, execute them and report results" + (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets))) + +val eval_termP = Parse.term -- (@{keyword "in"} |-- Parse.name) + +val _ = + Outer_Syntax.command @{command_spec "eval_term"} + "evaluate term in target language" + (eval_termP >> (fn (raw_t, target) => Toplevel.keep (eval_term_cmd raw_t target))) + +val _ = Context.>> (Context.map_theory ( + 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, Code_Haskell.target)), + (scalaN, (evaluate_in_scala, Code_Scala.target))])) +end + diff -r f8e6197668c9 -r 469a375212c1 src/HOL/ROOT --- a/src/HOL/ROOT Mon Aug 25 09:08:45 2014 +0200 +++ b/src/HOL/ROOT Mon Aug 25 09:40:50 2014 +0200 @@ -237,6 +237,19 @@ Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char + Code_Test + theories[condition = ISABELLE_GHC] + Code_Test_GHC + theories[condition = ISABELLE_MLTON] + Code_Test_MLton + theories[condition = ISABELLE_OCAMLC] + Code_Test_OCaml + theories[condition = ISABELLE_POLYML_PATH] + Code_Test_PolyML + theories[condition = ISABELLE_SCALA] + Code_Test_Scala + theories[condition = ISABELLE_SMLNJ] + Code_Test_SMLNJ session "HOL-Metis_Examples" in Metis_Examples = HOL + description {*