move Code_Test to HOL/Library;
authorAndreas Lochbihler
Wed Oct 08 09:09:12 2014 +0200 (2014-10-08)
changeset 586266c473ed0ac70
parent 58625 c78b2223f001
child 58627 1329679abb2d
child 58628 fd3c96a8ca60
move Code_Test to HOL/Library;
add corresponding entries in NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
src/HOL/Codegenerator_Test/Code_Test.thy
src/HOL/Codegenerator_Test/Code_Test_GHC.thy
src/HOL/Codegenerator_Test/Code_Test_MLton.thy
src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/HOL/Codegenerator_Test/code_test.ML
src/HOL/Library/Code_Test.thy
src/HOL/Library/Library.thy
src/HOL/Library/code_test.ML
src/HOL/ROOT
     1.1 --- a/CONTRIBUTORS	Wed Oct 08 00:13:39 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Oct 08 09:09:12 2014 +0200
     1.3 @@ -10,6 +10,9 @@
     1.4    Lexicographic order on functions and
     1.5    sum/product over function bodies.
     1.6  
     1.7 +* August 2014: Andreas Lochbihler, ETH Zurich
     1.8 +  Test infrastructure for executing generated code in target langauges
     1.9 +
    1.10  * August 2014: Manuel Eberl, TUM
    1.11    Generic euclidean algorithms for gcd et al.
    1.12  
     2.1 --- a/NEWS	Wed Oct 08 00:13:39 2014 +0200
     2.2 +++ b/NEWS	Wed Oct 08 09:09:12 2014 +0200
     2.3 @@ -122,6 +122,9 @@
     2.4  
     2.5  * List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
     2.6  
     2.7 +* New infrastructure for compiling, running, evaluating and testing
     2.8 +  generated code in target languages in HOL/Library/Code_Test. See
     2.9 +  HOL/Codegenerator_Test/Code_Test* for examples.
    2.10  
    2.11  *** ML ***
    2.12  
     3.1 --- a/src/HOL/Codegenerator_Test/Code_Test.thy	Wed Oct 08 00:13:39 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,148 +0,0 @@
     3.4 -(*  Title:      Code_Test.thy
     3.5 -    Author:     Andreas Lochbihler, ETH Zurich
     3.6 -
     3.7 -Test infrastructure for the code generator
     3.8 -*)
     3.9 -
    3.10 -theory Code_Test
    3.11 -imports Main
    3.12 -keywords "test_code" :: diag
    3.13 -begin
    3.14 -
    3.15 -subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
    3.16 -
    3.17 -datatype yxml_of_term = YXML
    3.18 -
    3.19 -lemma yot_anything: "x = (y :: yxml_of_term)"
    3.20 -by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
    3.21 -
    3.22 -definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
    3.23 -definition yot_literal :: "String.literal \<Rightarrow> yxml_of_term"
    3.24 -  where [code del]: "yot_literal _ = YXML"
    3.25 -definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    3.26 -  where [code del]: "yot_append _ _ = YXML"
    3.27 -definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
    3.28 -  where [code del]: "yot_concat _ = YXML"
    3.29 -
    3.30 -text {* Serialise @{typ yxml_of_term} to native string of target language *}
    3.31 -
    3.32 -code_printing type_constructor yxml_of_term
    3.33 -  \<rightharpoonup>  (SML) "string"
    3.34 -  and (OCaml) "string"
    3.35 -  and (Haskell) "String"
    3.36 -  and (Scala) "String"
    3.37 -| constant yot_empty
    3.38 -  \<rightharpoonup>  (SML) "\"\""
    3.39 -  and (OCaml) "\"\""
    3.40 -  and (Haskell) "\"\""
    3.41 -  and (Scala) "\"\""
    3.42 -| constant yot_literal
    3.43 -  \<rightharpoonup>  (SML) "_"
    3.44 -  and (OCaml) "_"
    3.45 -  and (Haskell) "_"
    3.46 -  and (Scala) "_"
    3.47 -| constant yot_append
    3.48 -  \<rightharpoonup> (SML) "String.concat [(_), (_)]"
    3.49 -  and (OCaml) "String.concat \"\" [(_); (_)]"
    3.50 -  and (Haskell) infixr 5 "++"
    3.51 -  and (Scala) infixl 5 "+"
    3.52 -| constant yot_concat
    3.53 -  \<rightharpoonup> (SML) "String.concat"
    3.54 -  and (OCaml) "String.concat \"\""
    3.55 -  and (Haskell) "Prelude.concat"
    3.56 -  and (Scala) "_.mkString(\"\")"
    3.57 -
    3.58 -text {*
    3.59 -  Stripped-down implementations of Isabelle's XML tree with YXML encoding
    3.60 -  as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
    3.61 -  sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
    3.62 -*}
    3.63 -
    3.64 -datatype xml_tree = XML_Tree
    3.65 -
    3.66 -lemma xml_tree_anything: "x = (y :: xml_tree)"
    3.67 -by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    3.68 -
    3.69 -context begin
    3.70 -local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
    3.71 -
    3.72 -type_synonym attributes = "(String.literal \<times> String.literal) list"
    3.73 -type_synonym body = "xml_tree list"
    3.74 -
    3.75 -definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    3.76 -where [code del]: "Elem _ _ _ = XML_Tree"
    3.77 -
    3.78 -definition Text :: "String.literal \<Rightarrow> xml_tree"
    3.79 -where [code del]: "Text _ = XML_Tree"
    3.80 -
    3.81 -definition node :: "xml_tree list \<Rightarrow> xml_tree"
    3.82 -where "node ts = Elem (STR '':'') [] ts"
    3.83 -
    3.84 -definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    3.85 -where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
    3.86 -
    3.87 -definition list where "list f xs = map (node \<circ> f) xs"
    3.88 -
    3.89 -definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
    3.90 -definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
    3.91 -definition XY :: yxml_of_term where "XY = yot_append X Y"
    3.92 -definition XYX :: yxml_of_term where "XYX = yot_append XY X"
    3.93 -
    3.94 -end
    3.95 -
    3.96 -code_datatype xml.Elem xml.Text
    3.97 -
    3.98 -definition yxml_string_of_xml_tree :: "xml_tree \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    3.99 -where [code del]: "yxml_string_of_xml_tree _ _ = YXML"
   3.100 -
   3.101 -lemma yxml_string_of_xml_tree_code [code]:
   3.102 -  "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
   3.103 -   yot_append xml.XY (
   3.104 -   yot_append (yot_literal name) (
   3.105 -   foldr (\<lambda>(a, x) rest. 
   3.106 -     yot_append xml.Y (
   3.107 -     yot_append (yot_literal a) (
   3.108 -     yot_append (yot_literal (STR ''='')) (
   3.109 -     yot_append (yot_literal x) rest)))) atts (
   3.110 -   foldr yxml_string_of_xml_tree ts (
   3.111 -   yot_append xml.XYX rest))))"
   3.112 -  "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
   3.113 -by(rule yot_anything)+
   3.114 -
   3.115 -definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term"
   3.116 -where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
   3.117 -
   3.118 -text {*
   3.119 -  Encoding @{typ Code_Evaluation.term} into XML trees
   3.120 -  as defined in @{file "~~/src/Pure/term_xml.ML"}
   3.121 -*}
   3.122 -
   3.123 -definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
   3.124 -where [code del]: "xml_of_typ _ = [XML_Tree]"
   3.125 -
   3.126 -definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body"
   3.127 -where [code del]: "xml_of_term _ = [XML_Tree]"
   3.128 -
   3.129 -lemma xml_of_typ_code [code]:
   3.130 -  "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
   3.131 -by(simp add: xml_of_typ_def xml_tree_anything)
   3.132 -
   3.133 -lemma xml_of_term_code [code]:
   3.134 -  "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
   3.135 -  "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)]]"
   3.136 -  "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)]]"
   3.137 -  -- {*
   3.138 -    FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
   3.139 -    uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
   3.140 -  *}
   3.141 -  "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
   3.142 -by(simp_all add: xml_of_term_def xml_tree_anything)
   3.143 -
   3.144 -definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term"
   3.145 -where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
   3.146 -
   3.147 -subsection {* Test engine and drivers *}
   3.148 -
   3.149 -ML_file "code_test.ML"
   3.150 -
   3.151 -end
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Wed Oct 08 00:13:39 2014 +0200
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Wed Oct 08 09:09:12 2014 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  Test case for test_code on GHC
     4.5  *)
     4.6  
     4.7 -theory Code_Test_GHC imports Code_Test begin
     4.8 +theory Code_Test_GHC imports "../Library/Code_Test" begin
     4.9  
    4.10  test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
    4.11  
     5.1 --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Wed Oct 08 00:13:39 2014 +0200
     5.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Wed Oct 08 09:09:12 2014 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  Test case for test_code on MLton
     5.5  *)
     5.6  
     5.7 -theory Code_Test_MLton imports Code_Test begin
     5.8 +theory Code_Test_MLton imports  "../Library/Code_Test" begin
     5.9  
    5.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
    5.11  
     6.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Wed Oct 08 00:13:39 2014 +0200
     6.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Wed Oct 08 09:09:12 2014 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  Test case for test_code on OCaml
     6.5  *)
     6.6  
     6.7 -theory Code_Test_OCaml imports Code_Test begin
     6.8 +theory Code_Test_OCaml imports  "../Library/Code_Test" begin
     6.9  
    6.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
    6.11  
     7.1 --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Wed Oct 08 00:13:39 2014 +0200
     7.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Wed Oct 08 09:09:12 2014 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  Test case for test_code on PolyML
     7.5  *)
     7.6  
     7.7 -theory Code_Test_PolyML imports Code_Test begin
     7.8 +theory Code_Test_PolyML imports  "../Library/Code_Test" begin
     7.9  
    7.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
    7.11  
     8.1 --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Wed Oct 08 00:13:39 2014 +0200
     8.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Wed Oct 08 09:09:12 2014 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  Test case for test_code on SMLNJ
     8.5  *)
     8.6  
     8.7 -theory Code_Test_SMLNJ imports Code_Test begin
     8.8 +theory Code_Test_SMLNJ imports  "../Library/Code_Test" begin
     8.9  
    8.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
    8.11  
     9.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Wed Oct 08 00:13:39 2014 +0200
     9.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Wed Oct 08 09:09:12 2014 +0200
     9.3 @@ -4,7 +4,7 @@
     9.4  Test case for test_code on Scala
     9.5  *)
     9.6  
     9.7 -theory Code_Test_Scala imports Code_Test begin 
     9.8 +theory Code_Test_Scala imports  "../Library/Code_Test" begin 
     9.9  
    9.10  declare [[scala_case_insensitive]]
    9.11  
    10.1 --- a/src/HOL/Codegenerator_Test/code_test.ML	Wed Oct 08 00:13:39 2014 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,580 +0,0 @@
    10.4 -(*  Title:      Code_Test.ML
    10.5 -    Author:     Andreas Lochbihler, ETH Zurich
    10.6 -
    10.7 -Test infrastructure for the code generator
    10.8 -*)
    10.9 -
   10.10 -signature CODE_TEST = sig
   10.11 -  val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory
   10.12 -  val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
   10.13 -  val overlord : bool Config.T
   10.14 -  val successN : string
   10.15 -  val failureN : string
   10.16 -  val start_markerN : string
   10.17 -  val end_markerN : string
   10.18 -  val test_terms : Proof.context -> term list -> string -> unit
   10.19 -  val test_targets : Proof.context -> term list -> string list -> unit list
   10.20 -  val test_code_cmd : string list -> string list -> Toplevel.state -> unit
   10.21 -
   10.22 -  val eval_term : string -> Proof.context -> term -> term
   10.23 -
   10.24 -  val gen_driver :
   10.25 -   (theory -> Path.T -> string list -> string ->
   10.26 -    {files : (Path.T * string) list,
   10.27 -     compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T})
   10.28 -   -> string -> string -> string
   10.29 -   -> theory -> (string * string) list * string -> Path.T -> string
   10.30 -
   10.31 -  val ISABELLE_POLYML : string
   10.32 -  val polymlN : string
   10.33 -  val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
   10.34 -
   10.35 -  val mltonN : string
   10.36 -  val ISABELLE_MLTON : string
   10.37 -  val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string
   10.38 -
   10.39 -  val smlnjN : string
   10.40 -  val ISABELLE_SMLNJ : string
   10.41 -  val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string
   10.42 -
   10.43 -  val ocamlN : string
   10.44 -  val ISABELLE_OCAMLC : string
   10.45 -  val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string
   10.46 -
   10.47 -  val ghcN : string
   10.48 -  val ISABELLE_GHC : string
   10.49 -  val ghc_options : string Config.T
   10.50 -  val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string
   10.51 -
   10.52 -  val scalaN : string
   10.53 -  val ISABELLE_SCALA : string
   10.54 -  val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string
   10.55 -end
   10.56 -
   10.57 -structure Code_Test : CODE_TEST = struct
   10.58 -
   10.59 -(* convert a list of terms into nested tuples and back *)
   10.60 -fun mk_tuples [] = @{term "()"}
   10.61 -  | mk_tuples [t] = t
   10.62 -  | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
   10.63 -
   10.64 -fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r
   10.65 -  | dest_tuples t = [t]
   10.66 -
   10.67 -
   10.68 -fun map_option _ NONE = NONE
   10.69 -  | map_option f (SOME x) = SOME (f x)
   10.70 -
   10.71 -fun last_field sep str =
   10.72 -  let
   10.73 -    val n = size sep;
   10.74 -    val len = size str;
   10.75 -    fun find i =
   10.76 -      if i < 0 then NONE
   10.77 -      else if String.substring (str, i, n) = sep then SOME i
   10.78 -      else find (i - 1);
   10.79 -  in
   10.80 -    (case find (len - n) of
   10.81 -      NONE => NONE
   10.82 -    | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   10.83 -  end;
   10.84 -
   10.85 -fun split_first_last start stop s =
   10.86 -  case first_field start s
   10.87 -   of NONE => NONE
   10.88 -    | SOME (initial, rest) =>
   10.89 -      case last_field stop rest
   10.90 -       of NONE => NONE
   10.91 -        | SOME (middle, tail) => SOME (initial, middle, tail);
   10.92 -
   10.93 -(* Data slot for drivers *)
   10.94 -
   10.95 -structure Drivers = Theory_Data
   10.96 -(
   10.97 -  type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list;
   10.98 -  val empty = [];
   10.99 -  val extend = I;
  10.100 -  fun merge data : T = AList.merge (op =) (K true) data;
  10.101 -)
  10.102 -
  10.103 -val add_driver = Drivers.map o AList.update (op =);
  10.104 -val get_driver = AList.lookup (op =) o Drivers.get;
  10.105 -
  10.106 -(*
  10.107 -  Test drivers must produce output of the following format:
  10.108 -  
  10.109 -  The start of the relevant data is marked with start_markerN,
  10.110 -  its end with end_markerN.
  10.111 -
  10.112 -  Between these two markers, every line corresponds to one test.
  10.113 -  Lines of successful tests start with successN, failures start with failureN.
  10.114 -  The failure failureN may continue with the YXML encoding of the evaluated term.
  10.115 -  There must not be any additional whitespace in between.
  10.116 -*)
  10.117 -
  10.118 -(* Parsing of results *)
  10.119 -
  10.120 -val successN = "True"
  10.121 -val failureN = "False"
  10.122 -val start_markerN = "*@*Isabelle/Code_Test-start*@*"
  10.123 -val end_markerN = "*@*Isabelle/Code_Test-end*@*"
  10.124 -
  10.125 -fun parse_line line =
  10.126 -  if String.isPrefix successN line then (true, NONE)
  10.127 -  else if String.isPrefix failureN line then (false, 
  10.128 -    if size line > size failureN then
  10.129 -      String.extract (line, size failureN, NONE)
  10.130 -      |> YXML.parse_body
  10.131 -      |> Term_XML.Decode.term
  10.132 -      |> dest_tuples
  10.133 -      |> SOME
  10.134 -    else NONE)
  10.135 -  else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
  10.136 -
  10.137 -fun parse_result target out =
  10.138 -  case split_first_last start_markerN end_markerN out
  10.139 -    of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
  10.140 -     | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line
  10.141 -
  10.142 -(* Pretty printing of test results *)
  10.143 -
  10.144 -fun pretty_eval _ NONE _ = []
  10.145 -  | pretty_eval ctxt (SOME evals) ts = 
  10.146 -    [Pretty.fbrk,
  10.147 -     Pretty.big_list "Evaluated terms"
  10.148 -       (map (fn (t, eval) => Pretty.block 
  10.149 -         [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
  10.150 -          Syntax.pretty_term ctxt eval])
  10.151 -       (ts ~~ evals))]
  10.152 -
  10.153 -fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
  10.154 -  Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
  10.155 -    @ pretty_eval ctxt evals eval_ts)
  10.156 -
  10.157 -fun pretty_failures ctxt target failures =
  10.158 -  Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
  10.159 -
  10.160 -(* Driver invocation *)
  10.161 -
  10.162 -val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false);
  10.163 -
  10.164 -fun with_overlord_dir name f =
  10.165 -  let
  10.166 -    val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
  10.167 -    val _ = Isabelle_System.mkdirs path;
  10.168 -  in
  10.169 -    Exn.release (Exn.capture f path)
  10.170 -  end;
  10.171 -
  10.172 -fun dynamic_value_strict ctxt t compiler =
  10.173 -  let
  10.174 -    val thy = Proof_Context.theory_of ctxt
  10.175 -    val (driver, target) = case get_driver thy compiler
  10.176 -     of NONE => error ("No driver for target " ^ compiler)
  10.177 -      | SOME f => f;
  10.178 -    val debug = Config.get (Proof_Context.init_global thy) overlord
  10.179 -    val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
  10.180 -    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
  10.181 -    fun evaluator program _ vs_ty deps =
  10.182 -      Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
  10.183 -    fun postproc f = map (apsnd (map_option (map f)))
  10.184 -  in
  10.185 -    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t)
  10.186 -  end;
  10.187 -
  10.188 -(* Term preprocessing *)
  10.189 -
  10.190 -fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
  10.191 -  | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
  10.192 -    acc
  10.193 -    |> add_eval rhs
  10.194 -    |> add_eval lhs
  10.195 -    |> cons rhs
  10.196 -    |> cons lhs)
  10.197 -  | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
  10.198 -  | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
  10.199 -    lhs :: rhs :: acc)
  10.200 -  | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
  10.201 -    lhs :: rhs :: acc)
  10.202 -  | add_eval _ = I
  10.203 -
  10.204 -fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
  10.205 -  | mk_term_of ts =
  10.206 -  let
  10.207 -    val tuple = mk_tuples ts
  10.208 -    val T = fastype_of tuple
  10.209 -  in
  10.210 -    @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
  10.211 -      (absdummy @{typ unit} (@{const yxml_string_of_term} $
  10.212 -        (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
  10.213 -  end
  10.214 -
  10.215 -fun test_terms ctxt ts target =
  10.216 -  let
  10.217 -    val thy = Proof_Context.theory_of ctxt
  10.218 -
  10.219 -    fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
  10.220 -
  10.221 -    fun ensure_bool t = case fastype_of t of @{typ bool} => ()
  10.222 -      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))
  10.223 -
  10.224 -    val _ = map ensure_bool ts
  10.225 -
  10.226 -    val evals = map (fn t => filter term_of (add_eval t [])) ts
  10.227 -    val eval = map mk_term_of evals
  10.228 -
  10.229 -    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
  10.230 -    val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
  10.231 -
  10.232 -    val result = dynamic_value_strict ctxt t target;
  10.233 -
  10.234 -    val failed =
  10.235 -      filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
  10.236 -      handle ListPair.UnequalLengths => 
  10.237 -        error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
  10.238 -    val _ = case failed of [] => () 
  10.239 -      | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
  10.240 -  in
  10.241 -    ()
  10.242 -  end
  10.243 -
  10.244 -fun test_targets ctxt = map o test_terms ctxt
  10.245 -
  10.246 -fun test_code_cmd raw_ts targets state =
  10.247 -  let
  10.248 -    val ctxt = Toplevel.context_of state;
  10.249 -    val ts = Syntax.read_terms ctxt raw_ts;
  10.250 -    val frees = fold Term.add_free_names ts []
  10.251 -    val _ = if frees = [] then () else
  10.252 -      error ("Terms contain free variables: " ^
  10.253 -      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
  10.254 -  in
  10.255 -    test_targets ctxt ts targets; ()
  10.256 -  end
  10.257 -
  10.258 -fun eval_term target ctxt t =
  10.259 -  let
  10.260 -    val frees = Term.add_free_names t []
  10.261 -    val _ = if frees = [] then () else
  10.262 -      error ("Term contains free variables: " ^
  10.263 -      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
  10.264 -
  10.265 -    val thy = Proof_Context.theory_of ctxt
  10.266 -
  10.267 -    val T_t = fastype_of t
  10.268 -    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
  10.269 -      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 
  10.270 -       " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
  10.271 -
  10.272 -    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
  10.273 -    val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
  10.274 -
  10.275 -    val result = dynamic_value_strict ctxt t' target;
  10.276 -  in
  10.277 -    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
  10.278 -  end
  10.279 -
  10.280 -(* Generic driver *)
  10.281 -
  10.282 -fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
  10.283 -  let
  10.284 -    val compiler = getenv env_var
  10.285 -    val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para 
  10.286 -         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
  10.287 -         compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
  10.288 -
  10.289 -    fun compile NONE = ()
  10.290 -      | compile (SOME cmd) =
  10.291 -        let
  10.292 -          val (out, ret) = Isabelle_System.bash_output cmd
  10.293 -        in
  10.294 -          if ret = 0 then () else error
  10.295 -            ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
  10.296 -        end
  10.297 -
  10.298 -    fun run (path : Path.T)= 
  10.299 -      let
  10.300 -        val modules = map fst code_files
  10.301 -        val {files, compile_cmd, run_cmd, mk_code_file}
  10.302 -          =  mk_driver ctxt path modules value_name
  10.303 -
  10.304 -        val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
  10.305 -        val _ = map (fn (name, content) => File.write name content) files
  10.306 -
  10.307 -        val _ = compile compile_cmd
  10.308 -
  10.309 -        val (out, res) = Isabelle_System.bash_output run_cmd
  10.310 -        val _ = if res = 0 then () else error
  10.311 -          ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
  10.312 -           "\nBash output:\n" ^ out)
  10.313 -      in
  10.314 -        out
  10.315 -      end
  10.316 -  in
  10.317 -    run
  10.318 -  end
  10.319 -
  10.320 -(* Driver for PolyML *)
  10.321 -
  10.322 -val ISABELLE_POLYML = "ISABELLE_POLYML"
  10.323 -val polymlN = "PolyML";
  10.324 -
  10.325 -fun mk_driver_polyml _ path _ value_name =
  10.326 -  let
  10.327 -    val generatedN = "generated.sml"
  10.328 -    val driverN = "driver.sml"
  10.329 -
  10.330 -    val code_path = Path.append path (Path.basic generatedN)
  10.331 -    val driver_path = Path.append path (Path.basic driverN)
  10.332 -    val driver = 
  10.333 -      "fun main prog_name = \n" ^
  10.334 -      "  let\n" ^
  10.335 -      "    fun format_term NONE = \"\"\n" ^ 
  10.336 -      "      | format_term (SOME t) = t ();\n" ^
  10.337 -      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  10.338 -      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  10.339 -      "    val result = " ^ value_name ^ " ();\n" ^
  10.340 -      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
  10.341 -      "    val _ = map (print o format) result;\n" ^
  10.342 -      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
  10.343 -      "  in\n" ^
  10.344 -      "    ()\n" ^
  10.345 -      "  end;\n"
  10.346 -    val cmd =
  10.347 -      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
  10.348 -      Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
  10.349 -      Path.implode (Path.variable ISABELLE_POLYML)
  10.350 -  in
  10.351 -    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
  10.352 -  end
  10.353 -
  10.354 -val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
  10.355 -
  10.356 -(* Driver for mlton *)
  10.357 -
  10.358 -val mltonN = "MLton"
  10.359 -val ISABELLE_MLTON = "ISABELLE_MLTON"
  10.360 -
  10.361 -fun mk_driver_mlton _ path _ value_name =
  10.362 -  let
  10.363 -    val generatedN = "generated.sml"
  10.364 -    val driverN = "driver.sml"
  10.365 -    val projectN = "test"
  10.366 -    val ml_basisN = projectN ^ ".mlb"
  10.367 -
  10.368 -    val code_path = Path.append path (Path.basic generatedN)
  10.369 -    val driver_path = Path.append path (Path.basic driverN)
  10.370 -    val ml_basis_path = Path.append path (Path.basic ml_basisN)
  10.371 -    val driver = 
  10.372 -      "fun format_term NONE = \"\"\n" ^ 
  10.373 -      "  | format_term (SOME t) = t ();\n" ^
  10.374 -      "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  10.375 -      "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  10.376 -      "val result = " ^ value_name ^ " ();\n" ^
  10.377 -      "val _ = print \"" ^ start_markerN ^ "\";\n" ^
  10.378 -      "val _ = map (print o format) result;\n" ^
  10.379 -      "val _ = print \"" ^ end_markerN ^ "\";\n"
  10.380 -    val ml_basis =
  10.381 -      "$(SML_LIB)/basis/basis.mlb\n" ^
  10.382 -      generatedN ^ "\n" ^
  10.383 -      driverN
  10.384 -
  10.385 -    val compile_cmd =
  10.386 -      File.shell_path (Path.variable ISABELLE_MLTON) ^
  10.387 -      " -default-type intinf " ^ File.shell_path ml_basis_path
  10.388 -    val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
  10.389 -  in
  10.390 -    {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
  10.391 -     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  10.392 -  end
  10.393 -
  10.394 -val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN
  10.395 -
  10.396 -(* Driver for SML/NJ *)
  10.397 -
  10.398 -val smlnjN = "SMLNJ"
  10.399 -val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
  10.400 -
  10.401 -fun mk_driver_smlnj _ path _ value_name =
  10.402 -  let
  10.403 -    val generatedN = "generated.sml"
  10.404 -    val driverN = "driver.sml"
  10.405 -
  10.406 -    val code_path = Path.append path (Path.basic generatedN)
  10.407 -    val driver_path = Path.append path (Path.basic driverN)
  10.408 -    val driver = 
  10.409 -      "structure Test = struct\n" ^
  10.410 -      "fun main prog_name =\n" ^
  10.411 -      "  let\n" ^
  10.412 -      "    fun format_term NONE = \"\"\n" ^ 
  10.413 -      "      | format_term (SOME t) = t ();\n" ^
  10.414 -      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  10.415 -      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  10.416 -      "    val result = " ^ value_name ^ " ();\n" ^
  10.417 -      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
  10.418 -      "    val _ = map (print o format) result;\n" ^
  10.419 -      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
  10.420 -      "  in\n" ^
  10.421 -      "    0\n" ^
  10.422 -      "  end;\n" ^
  10.423 -      "end;"
  10.424 -    val cmd =
  10.425 -      "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
  10.426 -      "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
  10.427 -      "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
  10.428 -  in
  10.429 -    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
  10.430 -  end
  10.431 -
  10.432 -val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN
  10.433 -
  10.434 -(* Driver for OCaml *)
  10.435 -
  10.436 -val ocamlN = "OCaml"
  10.437 -val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
  10.438 -
  10.439 -fun mk_driver_ocaml _ path _ value_name =
  10.440 -  let
  10.441 -    val generatedN = "generated.ml"
  10.442 -    val driverN = "driver.ml"
  10.443 -
  10.444 -    val code_path = Path.append path (Path.basic generatedN)
  10.445 -    val driver_path = Path.append path (Path.basic driverN)
  10.446 -    val driver = 
  10.447 -      "let format_term = function\n" ^
  10.448 -      "  | None -> \"\"\n" ^ 
  10.449 -      "  | Some t -> t ();;\n" ^
  10.450 -      "let format = function\n" ^
  10.451 -      "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
  10.452 -      "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
  10.453 -      "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
  10.454 -      "let main x =\n" ^
  10.455 -      "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
  10.456 -      "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
  10.457 -      "  print_string \"" ^ end_markerN ^ "\";;\n" ^
  10.458 -      "main ();;"
  10.459 -
  10.460 -    val compiled_path = Path.append path (Path.basic "test")
  10.461 -    val compile_cmd =
  10.462 -      Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
  10.463 -      " -I " ^ Path.implode path ^
  10.464 -      " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
  10.465 -
  10.466 -    val run_cmd = File.shell_path compiled_path
  10.467 -  in
  10.468 -    {files = [(driver_path, driver)],
  10.469 -     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  10.470 -  end
  10.471 -
  10.472 -val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN
  10.473 -
  10.474 -(* Driver for GHC *)
  10.475 -
  10.476 -val ghcN = "GHC"
  10.477 -val ISABELLE_GHC = "ISABELLE_GHC"
  10.478 -
  10.479 -val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
  10.480 -
  10.481 -fun mk_driver_ghc ctxt path modules value_name =
  10.482 -  let
  10.483 -    val driverN = "Main.hs"
  10.484 -
  10.485 -    fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
  10.486 -    val driver_path = Path.append path (Path.basic driverN)
  10.487 -    val driver = 
  10.488 -      "module Main where {\n" ^
  10.489 -      String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
  10.490 -      "main = do {\n" ^
  10.491 -      "    let {\n" ^
  10.492 -      "      format_term Nothing = \"\";\n" ^ 
  10.493 -      "      format_term (Just t) = t ();\n" ^
  10.494 -      "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
  10.495 -      "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
  10.496 -      "      result = " ^ value_name ^ " ();\n" ^
  10.497 -      "    };\n" ^
  10.498 -      "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
  10.499 -      "    Prelude.mapM_ (putStr . format) result;\n" ^
  10.500 -      "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
  10.501 -      "  }\n" ^
  10.502 -      "}\n"
  10.503 -
  10.504 -    val compiled_path = Path.append path (Path.basic "test")
  10.505 -    val compile_cmd =
  10.506 -      Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
  10.507 -      Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
  10.508 -      Path.implode driver_path ^ " -i" ^ Path.implode path
  10.509 -
  10.510 -    val run_cmd = File.shell_path compiled_path
  10.511 -  in
  10.512 -    {files = [(driver_path, driver)],
  10.513 -     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
  10.514 -  end
  10.515 -
  10.516 -val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN
  10.517 -
  10.518 -(* Driver for Scala *)
  10.519 -
  10.520 -val scalaN = "Scala"
  10.521 -val ISABELLE_SCALA = "ISABELLE_SCALA"
  10.522 -
  10.523 -fun mk_driver_scala _ path _ value_name =
  10.524 -  let
  10.525 -    val generatedN = "Generated_Code"
  10.526 -    val driverN = "Driver.scala"
  10.527 -
  10.528 -    val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
  10.529 -    val driver_path = Path.append path (Path.basic driverN)
  10.530 -    val driver = 
  10.531 -      "import " ^ generatedN ^ "._\n" ^
  10.532 -      "object Test {\n" ^
  10.533 -      "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
  10.534 -      "    case None => \"\"\n" ^
  10.535 -      "    case Some(x) => x(())\n" ^
  10.536 -      "  }\n" ^
  10.537 -      "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
  10.538 -      "      case (true, _) => \"True\\n\"\n" ^
  10.539 -      "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
  10.540 -      "  }\n" ^
  10.541 -      "  def main(args:Array[String]) = {\n" ^
  10.542 -      "    val result = " ^ value_name ^ "(());\n" ^
  10.543 -      "    print(\"" ^ start_markerN ^ "\");\n" ^
  10.544 -      "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
  10.545 -      "    print(\"" ^ end_markerN ^ "\");\n" ^
  10.546 -      "  }\n" ^
  10.547 -      "}\n"
  10.548 -
  10.549 -    val compile_cmd =
  10.550 -      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
  10.551 -      " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
  10.552 -      File.shell_path code_path ^ " " ^ File.shell_path driver_path
  10.553 -
  10.554 -    val run_cmd =
  10.555 -      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
  10.556 -      " -cp " ^ File.shell_path path ^ " Test"
  10.557 -  in
  10.558 -    {files = [(driver_path, driver)],
  10.559 -     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  10.560 -  end
  10.561 -
  10.562 -val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN
  10.563 -
  10.564 -val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
  10.565 -
  10.566 -val _ = 
  10.567 -  Outer_Syntax.command @{command_spec "test_code"}
  10.568 -    "compile test cases to target languages, execute them and report results"
  10.569 -      (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
  10.570 -
  10.571 -val _ = Context.>> (Context.map_theory (
  10.572 -  fold add_driver
  10.573 -    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
  10.574 -     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
  10.575 -     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
  10.576 -     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
  10.577 -     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
  10.578 -     (scalaN, (evaluate_in_scala, Code_Scala.target))]
  10.579 -    #> fold (fn target => Value.add_evaluator (target, eval_term target))
  10.580 -      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
  10.581 -    ))
  10.582 -end
  10.583 -
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/Code_Test.thy	Wed Oct 08 09:09:12 2014 +0200
    11.3 @@ -0,0 +1,148 @@
    11.4 +(*  Title:      Code_Test.thy
    11.5 +    Author:     Andreas Lochbihler, ETH Zurich
    11.6 +
    11.7 +Test infrastructure for the code generator
    11.8 +*)
    11.9 +
   11.10 +theory Code_Test
   11.11 +imports Main
   11.12 +keywords "test_code" :: diag
   11.13 +begin
   11.14 +
   11.15 +subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
   11.16 +
   11.17 +datatype (plugins del: code size "quickcheck") yxml_of_term = YXML
   11.18 +
   11.19 +lemma yot_anything: "x = (y :: yxml_of_term)"
   11.20 +by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
   11.21 +
   11.22 +definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
   11.23 +definition yot_literal :: "String.literal \<Rightarrow> yxml_of_term"
   11.24 +  where [code del]: "yot_literal _ = YXML"
   11.25 +definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
   11.26 +  where [code del]: "yot_append _ _ = YXML"
   11.27 +definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
   11.28 +  where [code del]: "yot_concat _ = YXML"
   11.29 +
   11.30 +text {* Serialise @{typ yxml_of_term} to native string of target language *}
   11.31 +
   11.32 +code_printing type_constructor yxml_of_term
   11.33 +  \<rightharpoonup>  (SML) "string"
   11.34 +  and (OCaml) "string"
   11.35 +  and (Haskell) "String"
   11.36 +  and (Scala) "String"
   11.37 +| constant yot_empty
   11.38 +  \<rightharpoonup>  (SML) "\"\""
   11.39 +  and (OCaml) "\"\""
   11.40 +  and (Haskell) "\"\""
   11.41 +  and (Scala) "\"\""
   11.42 +| constant yot_literal
   11.43 +  \<rightharpoonup>  (SML) "_"
   11.44 +  and (OCaml) "_"
   11.45 +  and (Haskell) "_"
   11.46 +  and (Scala) "_"
   11.47 +| constant yot_append
   11.48 +  \<rightharpoonup> (SML) "String.concat [(_), (_)]"
   11.49 +  and (OCaml) "String.concat \"\" [(_); (_)]"
   11.50 +  and (Haskell) infixr 5 "++"
   11.51 +  and (Scala) infixl 5 "+"
   11.52 +| constant yot_concat
   11.53 +  \<rightharpoonup> (SML) "String.concat"
   11.54 +  and (OCaml) "String.concat \"\""
   11.55 +  and (Haskell) "Prelude.concat"
   11.56 +  and (Scala) "_.mkString(\"\")"
   11.57 +
   11.58 +text {*
   11.59 +  Stripped-down implementations of Isabelle's XML tree with YXML encoding
   11.60 +  as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
   11.61 +  sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
   11.62 +*}
   11.63 +
   11.64 +datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
   11.65 +
   11.66 +lemma xml_tree_anything: "x = (y :: xml_tree)"
   11.67 +by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
   11.68 +
   11.69 +context begin
   11.70 +local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
   11.71 +
   11.72 +type_synonym attributes = "(String.literal \<times> String.literal) list"
   11.73 +type_synonym body = "xml_tree list"
   11.74 +
   11.75 +definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
   11.76 +where [code del]: "Elem _ _ _ = XML_Tree"
   11.77 +
   11.78 +definition Text :: "String.literal \<Rightarrow> xml_tree"
   11.79 +where [code del]: "Text _ = XML_Tree"
   11.80 +
   11.81 +definition node :: "xml_tree list \<Rightarrow> xml_tree"
   11.82 +where "node ts = Elem (STR '':'') [] ts"
   11.83 +
   11.84 +definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
   11.85 +where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
   11.86 +
   11.87 +definition list where "list f xs = map (node \<circ> f) xs"
   11.88 +
   11.89 +definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
   11.90 +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
   11.91 +definition XY :: yxml_of_term where "XY = yot_append X Y"
   11.92 +definition XYX :: yxml_of_term where "XYX = yot_append XY X"
   11.93 +
   11.94 +end
   11.95 +
   11.96 +code_datatype xml.Elem xml.Text
   11.97 +
   11.98 +definition yxml_string_of_xml_tree :: "xml_tree \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
   11.99 +where [code del]: "yxml_string_of_xml_tree _ _ = YXML"
  11.100 +
  11.101 +lemma yxml_string_of_xml_tree_code [code]:
  11.102 +  "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
  11.103 +   yot_append xml.XY (
  11.104 +   yot_append (yot_literal name) (
  11.105 +   foldr (\<lambda>(a, x) rest. 
  11.106 +     yot_append xml.Y (
  11.107 +     yot_append (yot_literal a) (
  11.108 +     yot_append (yot_literal (STR ''='')) (
  11.109 +     yot_append (yot_literal x) rest)))) atts (
  11.110 +   foldr yxml_string_of_xml_tree ts (
  11.111 +   yot_append xml.XYX rest))))"
  11.112 +  "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
  11.113 +by(rule yot_anything)+
  11.114 +
  11.115 +definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term"
  11.116 +where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
  11.117 +
  11.118 +text {*
  11.119 +  Encoding @{typ Code_Evaluation.term} into XML trees
  11.120 +  as defined in @{file "~~/src/Pure/term_xml.ML"}
  11.121 +*}
  11.122 +
  11.123 +definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
  11.124 +where [code del]: "xml_of_typ _ = [XML_Tree]"
  11.125 +
  11.126 +definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body"
  11.127 +where [code del]: "xml_of_term _ = [XML_Tree]"
  11.128 +
  11.129 +lemma xml_of_typ_code [code]:
  11.130 +  "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
  11.131 +by(simp add: xml_of_typ_def xml_tree_anything)
  11.132 +
  11.133 +lemma xml_of_term_code [code]:
  11.134 +  "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
  11.135 +  "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)]]"
  11.136 +  "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)]]"
  11.137 +  -- {*
  11.138 +    FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
  11.139 +    uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
  11.140 +  *}
  11.141 +  "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
  11.142 +by(simp_all add: xml_of_term_def xml_tree_anything)
  11.143 +
  11.144 +definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term"
  11.145 +where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
  11.146 +
  11.147 +subsection {* Test engine and drivers *}
  11.148 +
  11.149 +ML_file "code_test.ML"
  11.150 +
  11.151 +end
    12.1 --- a/src/HOL/Library/Library.thy	Wed Oct 08 00:13:39 2014 +0200
    12.2 +++ b/src/HOL/Library/Library.thy	Wed Oct 08 09:09:12 2014 +0200
    12.3 @@ -7,6 +7,7 @@
    12.4    BNF_Axiomatization
    12.5    Boolean_Algebra
    12.6    Char_ord
    12.7 +  Code_Test
    12.8    ContNotDenum
    12.9    Convex
   12.10    Countable
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Library/code_test.ML	Wed Oct 08 09:09:12 2014 +0200
    13.3 @@ -0,0 +1,580 @@
    13.4 +(*  Title:      Code_Test.ML
    13.5 +    Author:     Andreas Lochbihler, ETH Zurich
    13.6 +
    13.7 +Test infrastructure for the code generator
    13.8 +*)
    13.9 +
   13.10 +signature CODE_TEST = sig
   13.11 +  val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory
   13.12 +  val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
   13.13 +  val overlord : bool Config.T
   13.14 +  val successN : string
   13.15 +  val failureN : string
   13.16 +  val start_markerN : string
   13.17 +  val end_markerN : string
   13.18 +  val test_terms : Proof.context -> term list -> string -> unit
   13.19 +  val test_targets : Proof.context -> term list -> string list -> unit list
   13.20 +  val test_code_cmd : string list -> string list -> Toplevel.state -> unit
   13.21 +
   13.22 +  val eval_term : string -> Proof.context -> term -> term
   13.23 +
   13.24 +  val gen_driver :
   13.25 +   (theory -> Path.T -> string list -> string ->
   13.26 +    {files : (Path.T * string) list,
   13.27 +     compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T})
   13.28 +   -> string -> string -> string
   13.29 +   -> theory -> (string * string) list * string -> Path.T -> string
   13.30 +
   13.31 +  val ISABELLE_POLYML : string
   13.32 +  val polymlN : string
   13.33 +  val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
   13.34 +
   13.35 +  val mltonN : string
   13.36 +  val ISABELLE_MLTON : string
   13.37 +  val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string
   13.38 +
   13.39 +  val smlnjN : string
   13.40 +  val ISABELLE_SMLNJ : string
   13.41 +  val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string
   13.42 +
   13.43 +  val ocamlN : string
   13.44 +  val ISABELLE_OCAMLC : string
   13.45 +  val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string
   13.46 +
   13.47 +  val ghcN : string
   13.48 +  val ISABELLE_GHC : string
   13.49 +  val ghc_options : string Config.T
   13.50 +  val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string
   13.51 +
   13.52 +  val scalaN : string
   13.53 +  val ISABELLE_SCALA : string
   13.54 +  val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string
   13.55 +end
   13.56 +
   13.57 +structure Code_Test : CODE_TEST = struct
   13.58 +
   13.59 +(* convert a list of terms into nested tuples and back *)
   13.60 +fun mk_tuples [] = @{term "()"}
   13.61 +  | mk_tuples [t] = t
   13.62 +  | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
   13.63 +
   13.64 +fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r
   13.65 +  | dest_tuples t = [t]
   13.66 +
   13.67 +
   13.68 +fun map_option _ NONE = NONE
   13.69 +  | map_option f (SOME x) = SOME (f x)
   13.70 +
   13.71 +fun last_field sep str =
   13.72 +  let
   13.73 +    val n = size sep;
   13.74 +    val len = size str;
   13.75 +    fun find i =
   13.76 +      if i < 0 then NONE
   13.77 +      else if String.substring (str, i, n) = sep then SOME i
   13.78 +      else find (i - 1);
   13.79 +  in
   13.80 +    (case find (len - n) of
   13.81 +      NONE => NONE
   13.82 +    | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   13.83 +  end;
   13.84 +
   13.85 +fun split_first_last start stop s =
   13.86 +  case first_field start s
   13.87 +   of NONE => NONE
   13.88 +    | SOME (initial, rest) =>
   13.89 +      case last_field stop rest
   13.90 +       of NONE => NONE
   13.91 +        | SOME (middle, tail) => SOME (initial, middle, tail);
   13.92 +
   13.93 +(* Data slot for drivers *)
   13.94 +
   13.95 +structure Drivers = Theory_Data
   13.96 +(
   13.97 +  type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list;
   13.98 +  val empty = [];
   13.99 +  val extend = I;
  13.100 +  fun merge data : T = AList.merge (op =) (K true) data;
  13.101 +)
  13.102 +
  13.103 +val add_driver = Drivers.map o AList.update (op =);
  13.104 +val get_driver = AList.lookup (op =) o Drivers.get;
  13.105 +
  13.106 +(*
  13.107 +  Test drivers must produce output of the following format:
  13.108 +  
  13.109 +  The start of the relevant data is marked with start_markerN,
  13.110 +  its end with end_markerN.
  13.111 +
  13.112 +  Between these two markers, every line corresponds to one test.
  13.113 +  Lines of successful tests start with successN, failures start with failureN.
  13.114 +  The failure failureN may continue with the YXML encoding of the evaluated term.
  13.115 +  There must not be any additional whitespace in between.
  13.116 +*)
  13.117 +
  13.118 +(* Parsing of results *)
  13.119 +
  13.120 +val successN = "True"
  13.121 +val failureN = "False"
  13.122 +val start_markerN = "*@*Isabelle/Code_Test-start*@*"
  13.123 +val end_markerN = "*@*Isabelle/Code_Test-end*@*"
  13.124 +
  13.125 +fun parse_line line =
  13.126 +  if String.isPrefix successN line then (true, NONE)
  13.127 +  else if String.isPrefix failureN line then (false, 
  13.128 +    if size line > size failureN then
  13.129 +      String.extract (line, size failureN, NONE)
  13.130 +      |> YXML.parse_body
  13.131 +      |> Term_XML.Decode.term
  13.132 +      |> dest_tuples
  13.133 +      |> SOME
  13.134 +    else NONE)
  13.135 +  else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
  13.136 +
  13.137 +fun parse_result target out =
  13.138 +  case split_first_last start_markerN end_markerN out
  13.139 +    of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
  13.140 +     | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line
  13.141 +
  13.142 +(* Pretty printing of test results *)
  13.143 +
  13.144 +fun pretty_eval _ NONE _ = []
  13.145 +  | pretty_eval ctxt (SOME evals) ts = 
  13.146 +    [Pretty.fbrk,
  13.147 +     Pretty.big_list "Evaluated terms"
  13.148 +       (map (fn (t, eval) => Pretty.block 
  13.149 +         [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
  13.150 +          Syntax.pretty_term ctxt eval])
  13.151 +       (ts ~~ evals))]
  13.152 +
  13.153 +fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
  13.154 +  Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
  13.155 +    @ pretty_eval ctxt evals eval_ts)
  13.156 +
  13.157 +fun pretty_failures ctxt target failures =
  13.158 +  Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
  13.159 +
  13.160 +(* Driver invocation *)
  13.161 +
  13.162 +val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false);
  13.163 +
  13.164 +fun with_overlord_dir name f =
  13.165 +  let
  13.166 +    val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
  13.167 +    val _ = Isabelle_System.mkdirs path;
  13.168 +  in
  13.169 +    Exn.release (Exn.capture f path)
  13.170 +  end;
  13.171 +
  13.172 +fun dynamic_value_strict ctxt t compiler =
  13.173 +  let
  13.174 +    val thy = Proof_Context.theory_of ctxt
  13.175 +    val (driver, target) = case get_driver thy compiler
  13.176 +     of NONE => error ("No driver for target " ^ compiler)
  13.177 +      | SOME f => f;
  13.178 +    val debug = Config.get (Proof_Context.init_global thy) overlord
  13.179 +    val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
  13.180 +    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
  13.181 +    fun evaluator program _ vs_ty deps =
  13.182 +      Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
  13.183 +    fun postproc f = map (apsnd (map_option (map f)))
  13.184 +  in
  13.185 +    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t)
  13.186 +  end;
  13.187 +
  13.188 +(* Term preprocessing *)
  13.189 +
  13.190 +fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
  13.191 +  | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
  13.192 +    acc
  13.193 +    |> add_eval rhs
  13.194 +    |> add_eval lhs
  13.195 +    |> cons rhs
  13.196 +    |> cons lhs)
  13.197 +  | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
  13.198 +  | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
  13.199 +    lhs :: rhs :: acc)
  13.200 +  | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
  13.201 +    lhs :: rhs :: acc)
  13.202 +  | add_eval _ = I
  13.203 +
  13.204 +fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
  13.205 +  | mk_term_of ts =
  13.206 +  let
  13.207 +    val tuple = mk_tuples ts
  13.208 +    val T = fastype_of tuple
  13.209 +  in
  13.210 +    @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
  13.211 +      (absdummy @{typ unit} (@{const yxml_string_of_term} $
  13.212 +        (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
  13.213 +  end
  13.214 +
  13.215 +fun test_terms ctxt ts target =
  13.216 +  let
  13.217 +    val thy = Proof_Context.theory_of ctxt
  13.218 +
  13.219 +    fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
  13.220 +
  13.221 +    fun ensure_bool t = case fastype_of t of @{typ bool} => ()
  13.222 +      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))
  13.223 +
  13.224 +    val _ = map ensure_bool ts
  13.225 +
  13.226 +    val evals = map (fn t => filter term_of (add_eval t [])) ts
  13.227 +    val eval = map mk_term_of evals
  13.228 +
  13.229 +    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
  13.230 +    val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
  13.231 +
  13.232 +    val result = dynamic_value_strict ctxt t target;
  13.233 +
  13.234 +    val failed =
  13.235 +      filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
  13.236 +      handle ListPair.UnequalLengths => 
  13.237 +        error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
  13.238 +    val _ = case failed of [] => () 
  13.239 +      | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
  13.240 +  in
  13.241 +    ()
  13.242 +  end
  13.243 +
  13.244 +fun test_targets ctxt = map o test_terms ctxt
  13.245 +
  13.246 +fun test_code_cmd raw_ts targets state =
  13.247 +  let
  13.248 +    val ctxt = Toplevel.context_of state;
  13.249 +    val ts = Syntax.read_terms ctxt raw_ts;
  13.250 +    val frees = fold Term.add_free_names ts []
  13.251 +    val _ = if frees = [] then () else
  13.252 +      error ("Terms contain free variables: " ^
  13.253 +      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
  13.254 +  in
  13.255 +    test_targets ctxt ts targets; ()
  13.256 +  end
  13.257 +
  13.258 +fun eval_term target ctxt t =
  13.259 +  let
  13.260 +    val frees = Term.add_free_names t []
  13.261 +    val _ = if frees = [] then () else
  13.262 +      error ("Term contains free variables: " ^
  13.263 +      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
  13.264 +
  13.265 +    val thy = Proof_Context.theory_of ctxt
  13.266 +
  13.267 +    val T_t = fastype_of t
  13.268 +    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
  13.269 +      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 
  13.270 +       " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
  13.271 +
  13.272 +    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
  13.273 +    val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
  13.274 +
  13.275 +    val result = dynamic_value_strict ctxt t' target;
  13.276 +  in
  13.277 +    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
  13.278 +  end
  13.279 +
  13.280 +(* Generic driver *)
  13.281 +
  13.282 +fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
  13.283 +  let
  13.284 +    val compiler = getenv env_var
  13.285 +    val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para 
  13.286 +         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
  13.287 +         compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
  13.288 +
  13.289 +    fun compile NONE = ()
  13.290 +      | compile (SOME cmd) =
  13.291 +        let
  13.292 +          val (out, ret) = Isabelle_System.bash_output cmd
  13.293 +        in
  13.294 +          if ret = 0 then () else error
  13.295 +            ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
  13.296 +        end
  13.297 +
  13.298 +    fun run (path : Path.T)= 
  13.299 +      let
  13.300 +        val modules = map fst code_files
  13.301 +        val {files, compile_cmd, run_cmd, mk_code_file}
  13.302 +          =  mk_driver ctxt path modules value_name
  13.303 +
  13.304 +        val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
  13.305 +        val _ = map (fn (name, content) => File.write name content) files
  13.306 +
  13.307 +        val _ = compile compile_cmd
  13.308 +
  13.309 +        val (out, res) = Isabelle_System.bash_output run_cmd
  13.310 +        val _ = if res = 0 then () else error
  13.311 +          ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
  13.312 +           "\nBash output:\n" ^ out)
  13.313 +      in
  13.314 +        out
  13.315 +      end
  13.316 +  in
  13.317 +    run
  13.318 +  end
  13.319 +
  13.320 +(* Driver for PolyML *)
  13.321 +
  13.322 +val ISABELLE_POLYML = "ISABELLE_POLYML"
  13.323 +val polymlN = "PolyML";
  13.324 +
  13.325 +fun mk_driver_polyml _ path _ value_name =
  13.326 +  let
  13.327 +    val generatedN = "generated.sml"
  13.328 +    val driverN = "driver.sml"
  13.329 +
  13.330 +    val code_path = Path.append path (Path.basic generatedN)
  13.331 +    val driver_path = Path.append path (Path.basic driverN)
  13.332 +    val driver = 
  13.333 +      "fun main prog_name = \n" ^
  13.334 +      "  let\n" ^
  13.335 +      "    fun format_term NONE = \"\"\n" ^ 
  13.336 +      "      | format_term (SOME t) = t ();\n" ^
  13.337 +      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  13.338 +      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  13.339 +      "    val result = " ^ value_name ^ " ();\n" ^
  13.340 +      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
  13.341 +      "    val _ = map (print o format) result;\n" ^
  13.342 +      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
  13.343 +      "  in\n" ^
  13.344 +      "    ()\n" ^
  13.345 +      "  end;\n"
  13.346 +    val cmd =
  13.347 +      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
  13.348 +      Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
  13.349 +      Path.implode (Path.variable ISABELLE_POLYML)
  13.350 +  in
  13.351 +    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
  13.352 +  end
  13.353 +
  13.354 +val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
  13.355 +
  13.356 +(* Driver for mlton *)
  13.357 +
  13.358 +val mltonN = "MLton"
  13.359 +val ISABELLE_MLTON = "ISABELLE_MLTON"
  13.360 +
  13.361 +fun mk_driver_mlton _ path _ value_name =
  13.362 +  let
  13.363 +    val generatedN = "generated.sml"
  13.364 +    val driverN = "driver.sml"
  13.365 +    val projectN = "test"
  13.366 +    val ml_basisN = projectN ^ ".mlb"
  13.367 +
  13.368 +    val code_path = Path.append path (Path.basic generatedN)
  13.369 +    val driver_path = Path.append path (Path.basic driverN)
  13.370 +    val ml_basis_path = Path.append path (Path.basic ml_basisN)
  13.371 +    val driver = 
  13.372 +      "fun format_term NONE = \"\"\n" ^ 
  13.373 +      "  | format_term (SOME t) = t ();\n" ^
  13.374 +      "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  13.375 +      "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  13.376 +      "val result = " ^ value_name ^ " ();\n" ^
  13.377 +      "val _ = print \"" ^ start_markerN ^ "\";\n" ^
  13.378 +      "val _ = map (print o format) result;\n" ^
  13.379 +      "val _ = print \"" ^ end_markerN ^ "\";\n"
  13.380 +    val ml_basis =
  13.381 +      "$(SML_LIB)/basis/basis.mlb\n" ^
  13.382 +      generatedN ^ "\n" ^
  13.383 +      driverN
  13.384 +
  13.385 +    val compile_cmd =
  13.386 +      File.shell_path (Path.variable ISABELLE_MLTON) ^
  13.387 +      " -default-type intinf " ^ File.shell_path ml_basis_path
  13.388 +    val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
  13.389 +  in
  13.390 +    {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
  13.391 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  13.392 +  end
  13.393 +
  13.394 +val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN
  13.395 +
  13.396 +(* Driver for SML/NJ *)
  13.397 +
  13.398 +val smlnjN = "SMLNJ"
  13.399 +val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
  13.400 +
  13.401 +fun mk_driver_smlnj _ path _ value_name =
  13.402 +  let
  13.403 +    val generatedN = "generated.sml"
  13.404 +    val driverN = "driver.sml"
  13.405 +
  13.406 +    val code_path = Path.append path (Path.basic generatedN)
  13.407 +    val driver_path = Path.append path (Path.basic driverN)
  13.408 +    val driver = 
  13.409 +      "structure Test = struct\n" ^
  13.410 +      "fun main prog_name =\n" ^
  13.411 +      "  let\n" ^
  13.412 +      "    fun format_term NONE = \"\"\n" ^ 
  13.413 +      "      | format_term (SOME t) = t ();\n" ^
  13.414 +      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
  13.415 +      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
  13.416 +      "    val result = " ^ value_name ^ " ();\n" ^
  13.417 +      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
  13.418 +      "    val _ = map (print o format) result;\n" ^
  13.419 +      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
  13.420 +      "  in\n" ^
  13.421 +      "    0\n" ^
  13.422 +      "  end;\n" ^
  13.423 +      "end;"
  13.424 +    val cmd =
  13.425 +      "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
  13.426 +      "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
  13.427 +      "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
  13.428 +  in
  13.429 +    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
  13.430 +  end
  13.431 +
  13.432 +val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN
  13.433 +
  13.434 +(* Driver for OCaml *)
  13.435 +
  13.436 +val ocamlN = "OCaml"
  13.437 +val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
  13.438 +
  13.439 +fun mk_driver_ocaml _ path _ value_name =
  13.440 +  let
  13.441 +    val generatedN = "generated.ml"
  13.442 +    val driverN = "driver.ml"
  13.443 +
  13.444 +    val code_path = Path.append path (Path.basic generatedN)
  13.445 +    val driver_path = Path.append path (Path.basic driverN)
  13.446 +    val driver = 
  13.447 +      "let format_term = function\n" ^
  13.448 +      "  | None -> \"\"\n" ^ 
  13.449 +      "  | Some t -> t ();;\n" ^
  13.450 +      "let format = function\n" ^
  13.451 +      "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
  13.452 +      "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
  13.453 +      "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
  13.454 +      "let main x =\n" ^
  13.455 +      "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
  13.456 +      "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
  13.457 +      "  print_string \"" ^ end_markerN ^ "\";;\n" ^
  13.458 +      "main ();;"
  13.459 +
  13.460 +    val compiled_path = Path.append path (Path.basic "test")
  13.461 +    val compile_cmd =
  13.462 +      Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
  13.463 +      " -I " ^ Path.implode path ^
  13.464 +      " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
  13.465 +
  13.466 +    val run_cmd = File.shell_path compiled_path
  13.467 +  in
  13.468 +    {files = [(driver_path, driver)],
  13.469 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  13.470 +  end
  13.471 +
  13.472 +val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN
  13.473 +
  13.474 +(* Driver for GHC *)
  13.475 +
  13.476 +val ghcN = "GHC"
  13.477 +val ISABELLE_GHC = "ISABELLE_GHC"
  13.478 +
  13.479 +val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "")
  13.480 +
  13.481 +fun mk_driver_ghc ctxt path modules value_name =
  13.482 +  let
  13.483 +    val driverN = "Main.hs"
  13.484 +
  13.485 +    fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
  13.486 +    val driver_path = Path.append path (Path.basic driverN)
  13.487 +    val driver = 
  13.488 +      "module Main where {\n" ^
  13.489 +      String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
  13.490 +      "main = do {\n" ^
  13.491 +      "    let {\n" ^
  13.492 +      "      format_term Nothing = \"\";\n" ^ 
  13.493 +      "      format_term (Just t) = t ();\n" ^
  13.494 +      "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
  13.495 +      "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
  13.496 +      "      result = " ^ value_name ^ " ();\n" ^
  13.497 +      "    };\n" ^
  13.498 +      "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
  13.499 +      "    Prelude.mapM_ (putStr . format) result;\n" ^
  13.500 +      "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
  13.501 +      "  }\n" ^
  13.502 +      "}\n"
  13.503 +
  13.504 +    val compiled_path = Path.append path (Path.basic "test")
  13.505 +    val compile_cmd =
  13.506 +      Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
  13.507 +      Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
  13.508 +      Path.implode driver_path ^ " -i" ^ Path.implode path
  13.509 +
  13.510 +    val run_cmd = File.shell_path compiled_path
  13.511 +  in
  13.512 +    {files = [(driver_path, driver)],
  13.513 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
  13.514 +  end
  13.515 +
  13.516 +val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN
  13.517 +
  13.518 +(* Driver for Scala *)
  13.519 +
  13.520 +val scalaN = "Scala"
  13.521 +val ISABELLE_SCALA = "ISABELLE_SCALA"
  13.522 +
  13.523 +fun mk_driver_scala _ path _ value_name =
  13.524 +  let
  13.525 +    val generatedN = "Generated_Code"
  13.526 +    val driverN = "Driver.scala"
  13.527 +
  13.528 +    val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
  13.529 +    val driver_path = Path.append path (Path.basic driverN)
  13.530 +    val driver = 
  13.531 +      "import " ^ generatedN ^ "._\n" ^
  13.532 +      "object Test {\n" ^
  13.533 +      "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
  13.534 +      "    case None => \"\"\n" ^
  13.535 +      "    case Some(x) => x(())\n" ^
  13.536 +      "  }\n" ^
  13.537 +      "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
  13.538 +      "      case (true, _) => \"True\\n\"\n" ^
  13.539 +      "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
  13.540 +      "  }\n" ^
  13.541 +      "  def main(args:Array[String]) = {\n" ^
  13.542 +      "    val result = " ^ value_name ^ "(());\n" ^
  13.543 +      "    print(\"" ^ start_markerN ^ "\");\n" ^
  13.544 +      "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
  13.545 +      "    print(\"" ^ end_markerN ^ "\");\n" ^
  13.546 +      "  }\n" ^
  13.547 +      "}\n"
  13.548 +
  13.549 +    val compile_cmd =
  13.550 +      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
  13.551 +      " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
  13.552 +      File.shell_path code_path ^ " " ^ File.shell_path driver_path
  13.553 +
  13.554 +    val run_cmd =
  13.555 +      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
  13.556 +      " -cp " ^ File.shell_path path ^ " Test"
  13.557 +  in
  13.558 +    {files = [(driver_path, driver)],
  13.559 +     compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
  13.560 +  end
  13.561 +
  13.562 +val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN
  13.563 +
  13.564 +val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
  13.565 +
  13.566 +val _ = 
  13.567 +  Outer_Syntax.command @{command_spec "test_code"}
  13.568 +    "compile test cases to target languages, execute them and report results"
  13.569 +      (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
  13.570 +
  13.571 +val _ = Context.>> (Context.map_theory (
  13.572 +  fold add_driver
  13.573 +    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
  13.574 +     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
  13.575 +     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
  13.576 +     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
  13.577 +     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
  13.578 +     (scalaN, (evaluate_in_scala, Code_Scala.target))]
  13.579 +    #> fold (fn target => Value.add_evaluator (target, eval_term target))
  13.580 +      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
  13.581 +    ))
  13.582 +end
  13.583 +
    14.1 --- a/src/HOL/ROOT	Wed Oct 08 00:13:39 2014 +0200
    14.2 +++ b/src/HOL/ROOT	Wed Oct 08 09:09:12 2014 +0200
    14.3 @@ -241,7 +241,6 @@
    14.4      Generate_Target_Nat
    14.5      Generate_Efficient_Datastructures
    14.6      Generate_Pretty_Char
    14.7 -    Code_Test
    14.8    theories [condition = ISABELLE_GHC]
    14.9      Code_Test_GHC
   14.10    theories [condition = ISABELLE_MLTON]