move Code_Test to HOL/Library;
add corresponding entries in NEWS and CONTRIBUTORS
--- a/CONTRIBUTORS Wed Oct 08 00:13:39 2014 +0200
+++ b/CONTRIBUTORS Wed Oct 08 09:09:12 2014 +0200
@@ -10,6 +10,9 @@
Lexicographic order on functions and
sum/product over function bodies.
+* August 2014: Andreas Lochbihler, ETH Zurich
+ Test infrastructure for executing generated code in target langauges
+
* August 2014: Manuel Eberl, TUM
Generic euclidean algorithms for gcd et al.
--- a/NEWS Wed Oct 08 00:13:39 2014 +0200
+++ b/NEWS Wed Oct 08 09:09:12 2014 +0200
@@ -122,6 +122,9 @@
* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
+* New infrastructure for compiling, running, evaluating and testing
+ generated code in target languages in HOL/Library/Code_Test. See
+ HOL/Codegenerator_Test/Code_Test* for examples.
*** ML ***
--- a/src/HOL/Codegenerator_Test/Code_Test.thy Wed Oct 08 00:13:39 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-(* Title: Code_Test.thy
- Author: Andreas Lochbihler, ETH Zurich
-
-Test infrastructure for the code generator
-*)
-
-theory Code_Test
-imports Main
-keywords "test_code" :: 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 \<Rightarrow> yxml_of_term"
- where [code del]: "yot_literal _ = YXML"
-definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
- where [code del]: "yot_append _ _ = YXML"
-definition yot_concat :: "yxml_of_term list \<Rightarrow> 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
- \<rightharpoonup> (SML) "string"
- and (OCaml) "string"
- and (Haskell) "String"
- and (Scala) "String"
-| constant yot_empty
- \<rightharpoonup> (SML) "\"\""
- and (OCaml) "\"\""
- and (Haskell) "\"\""
- and (Scala) "\"\""
-| constant yot_literal
- \<rightharpoonup> (SML) "_"
- and (OCaml) "_"
- and (Haskell) "_"
- and (Scala) "_"
-| constant yot_append
- \<rightharpoonup> (SML) "String.concat [(_), (_)]"
- and (OCaml) "String.concat \"\" [(_); (_)]"
- and (Haskell) infixr 5 "++"
- and (Scala) infixl 5 "+"
-| constant yot_concat
- \<rightharpoonup> (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 \<times> String.literal) list"
-type_synonym body = "xml_tree list"
-
-definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
-where [code del]: "Elem _ _ _ = XML_Tree"
-
-definition Text :: "String.literal \<Rightarrow> xml_tree"
-where [code del]: "Text _ = XML_Tree"
-
-definition node :: "xml_tree list \<Rightarrow> xml_tree"
-where "node ts = Elem (STR '':'') [] ts"
-
-definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
-where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
-
-definition list where "list f xs = map (node \<circ> 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 \<Rightarrow> yxml_of_term \<Rightarrow> 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 (\<lambda>(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 \<Rightarrow> 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 \<Rightarrow> xml.body"
-where [code del]: "xml_of_typ _ = [XML_Tree]"
-
-definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> 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 \<Rightarrow> yxml_of_term"
-where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
-
-subsection {* Test engine and drivers *}
-
-ML_file "code_test.ML"
-
-end
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on GHC
*)
-theory Code_Test_GHC imports Code_Test begin
+theory Code_Test_GHC imports "../Library/Code_Test" begin
test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
--- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on MLton
*)
-theory Code_Test_MLton imports Code_Test begin
+theory Code_Test_MLton imports "../Library/Code_Test" begin
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on OCaml
*)
-theory Code_Test_OCaml imports Code_Test begin
+theory Code_Test_OCaml imports "../Library/Code_Test" begin
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on PolyML
*)
-theory Code_Test_PolyML imports Code_Test begin
+theory Code_Test_PolyML imports "../Library/Code_Test" begin
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
--- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on SMLNJ
*)
-theory Code_Test_SMLNJ imports Code_Test begin
+theory Code_Test_SMLNJ imports "../Library/Code_Test" begin
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Wed Oct 08 09:09:12 2014 +0200
@@ -4,7 +4,7 @@
Test case for test_code on Scala
*)
-theory Code_Test_Scala imports Code_Test begin
+theory Code_Test_Scala imports "../Library/Code_Test" begin
declare [[scala_case_insensitive]]
--- a/src/HOL/Codegenerator_Test/code_test.ML Wed Oct 08 00:13:39 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,580 +0,0 @@
-(* 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 : string -> Proof.context -> term -> term
-
- 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 : 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 \<Rightarrow> yxml_of_term) option"}
- | mk_term_of ts =
- let
- val tuple = mk_tuples ts
- val T = fastype_of tuple
- in
- @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> 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 target ctxt t =
- let
- 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))))
-
- 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;
- in
- case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
- 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 = "ISABELLE_POLYML"
-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)
- 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 "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 _ = 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))]
- #> fold (fn target => Value.add_evaluator (target, eval_term target))
- [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
- ))
-end
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Test.thy Wed Oct 08 09:09:12 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" :: diag
+begin
+
+subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
+
+datatype (plugins del: code size "quickcheck") 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 \<Rightarrow> yxml_of_term"
+ where [code del]: "yot_literal _ = YXML"
+definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
+ where [code del]: "yot_append _ _ = YXML"
+definition yot_concat :: "yxml_of_term list \<Rightarrow> 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
+ \<rightharpoonup> (SML) "string"
+ and (OCaml) "string"
+ and (Haskell) "String"
+ and (Scala) "String"
+| constant yot_empty
+ \<rightharpoonup> (SML) "\"\""
+ and (OCaml) "\"\""
+ and (Haskell) "\"\""
+ and (Scala) "\"\""
+| constant yot_literal
+ \<rightharpoonup> (SML) "_"
+ and (OCaml) "_"
+ and (Haskell) "_"
+ and (Scala) "_"
+| constant yot_append
+ \<rightharpoonup> (SML) "String.concat [(_), (_)]"
+ and (OCaml) "String.concat \"\" [(_); (_)]"
+ and (Haskell) infixr 5 "++"
+ and (Scala) infixl 5 "+"
+| constant yot_concat
+ \<rightharpoonup> (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 (plugins del: code size "quickcheck") 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 \<times> String.literal) list"
+type_synonym body = "xml_tree list"
+
+definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
+where [code del]: "Elem _ _ _ = XML_Tree"
+
+definition Text :: "String.literal \<Rightarrow> xml_tree"
+where [code del]: "Text _ = XML_Tree"
+
+definition node :: "xml_tree list \<Rightarrow> xml_tree"
+where "node ts = Elem (STR '':'') [] ts"
+
+definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
+where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
+
+definition list where "list f xs = map (node \<circ> 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 \<Rightarrow> yxml_of_term \<Rightarrow> 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 (\<lambda>(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 \<Rightarrow> 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 \<Rightarrow> xml.body"
+where [code del]: "xml_of_typ _ = [XML_Tree]"
+
+definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> 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 \<Rightarrow> yxml_of_term"
+where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
+
+subsection {* Test engine and drivers *}
+
+ML_file "code_test.ML"
+
+end
--- a/src/HOL/Library/Library.thy Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/Library/Library.thy Wed Oct 08 09:09:12 2014 +0200
@@ -7,6 +7,7 @@
BNF_Axiomatization
Boolean_Algebra
Char_ord
+ Code_Test
ContNotDenum
Convex
Countable
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/code_test.ML Wed Oct 08 09:09:12 2014 +0200
@@ -0,0 +1,580 @@
+(* 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 : string -> Proof.context -> term -> term
+
+ 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 : 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 \<Rightarrow> yxml_of_term) option"}
+ | mk_term_of ts =
+ let
+ val tuple = mk_tuples ts
+ val T = fastype_of tuple
+ in
+ @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> 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 target ctxt t =
+ let
+ 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))))
+
+ 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;
+ in
+ case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
+ 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 = "ISABELLE_POLYML"
+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)
+ 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 "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 _ = 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))]
+ #> fold (fn target => Value.add_evaluator (target, eval_term target))
+ [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
+ ))
+end
+
--- a/src/HOL/ROOT Wed Oct 08 00:13:39 2014 +0200
+++ b/src/HOL/ROOT Wed Oct 08 09:09:12 2014 +0200
@@ -241,7 +241,6 @@
Generate_Target_Nat
Generate_Efficient_Datastructures
Generate_Pretty_Char
- Code_Test
theories [condition = ISABELLE_GHC]
Code_Test_GHC
theories [condition = ISABELLE_MLTON]