src/HOL/Library/Code_Test.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 64578 7b20f9f94f4e
child 67443 3abf6a722518
permissions -rw-r--r--
tuned proofs;
wenzelm@59720
     1
(*  Title:      HOL/Library/Code_Test.thy
wenzelm@64578
     2
    Author:     Andreas Lochbihler, ETH Z├╝rich
Andreas@58039
     3
wenzelm@64578
     4
Test infrastructure for the code generator.
Andreas@58039
     5
*)
Andreas@58039
     6
Andreas@58039
     7
theory Code_Test
Andreas@58039
     8
imports Main
Andreas@58348
     9
keywords "test_code" :: diag
Andreas@58039
    10
begin
Andreas@58039
    11
wenzelm@60500
    12
subsection \<open>YXML encoding for @{typ Code_Evaluation.term}\<close>
Andreas@58039
    13
Andreas@58626
    14
datatype (plugins del: code size "quickcheck") yxml_of_term = YXML
Andreas@58039
    15
Andreas@58039
    16
lemma yot_anything: "x = (y :: yxml_of_term)"
Andreas@58039
    17
by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
Andreas@58039
    18
Andreas@58039
    19
definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
Andreas@58039
    20
definition yot_literal :: "String.literal \<Rightarrow> yxml_of_term"
Andreas@58039
    21
  where [code del]: "yot_literal _ = YXML"
Andreas@58039
    22
definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
Andreas@58039
    23
  where [code del]: "yot_append _ _ = YXML"
Andreas@58039
    24
definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
Andreas@58039
    25
  where [code del]: "yot_concat _ = YXML"
Andreas@58039
    26
wenzelm@60500
    27
text \<open>Serialise @{typ yxml_of_term} to native string of target language\<close>
Andreas@58039
    28
Andreas@58039
    29
code_printing type_constructor yxml_of_term
Andreas@58039
    30
  \<rightharpoonup>  (SML) "string"
Andreas@58039
    31
  and (OCaml) "string"
Andreas@58039
    32
  and (Haskell) "String"
Andreas@58039
    33
  and (Scala) "String"
Andreas@58039
    34
| constant yot_empty
Andreas@58039
    35
  \<rightharpoonup>  (SML) "\"\""
Andreas@58039
    36
  and (OCaml) "\"\""
Andreas@58039
    37
  and (Haskell) "\"\""
Andreas@58039
    38
  and (Scala) "\"\""
Andreas@58039
    39
| constant yot_literal
Andreas@58039
    40
  \<rightharpoonup>  (SML) "_"
Andreas@58039
    41
  and (OCaml) "_"
Andreas@58039
    42
  and (Haskell) "_"
Andreas@58039
    43
  and (Scala) "_"
Andreas@58039
    44
| constant yot_append
Andreas@58039
    45
  \<rightharpoonup> (SML) "String.concat [(_), (_)]"
Andreas@58039
    46
  and (OCaml) "String.concat \"\" [(_); (_)]"
Andreas@58039
    47
  and (Haskell) infixr 5 "++"
Andreas@58039
    48
  and (Scala) infixl 5 "+"
Andreas@58039
    49
| constant yot_concat
Andreas@58039
    50
  \<rightharpoonup> (SML) "String.concat"
Andreas@58039
    51
  and (OCaml) "String.concat \"\""
Andreas@58039
    52
  and (Haskell) "Prelude.concat"
Andreas@58039
    53
  and (Scala) "_.mkString(\"\")"
Andreas@58039
    54
wenzelm@60500
    55
text \<open>
wenzelm@63680
    56
  Stripped-down implementations of Isabelle's XML tree with YXML encoding as
wenzelm@63680
    57
  defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
wenzelm@63680
    58
  sufficient to encode @{typ "Code_Evaluation.term"} as in
wenzelm@63680
    59
  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
wenzelm@60500
    60
\<close>
Andreas@58039
    61
Andreas@58626
    62
datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
Andreas@58039
    63
Andreas@58039
    64
lemma xml_tree_anything: "x = (y :: xml_tree)"
Andreas@58039
    65
by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
Andreas@58039
    66
Andreas@58039
    67
context begin
wenzelm@60500
    68
local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "xml")\<close>
Andreas@58039
    69
Andreas@58039
    70
type_synonym attributes = "(String.literal \<times> String.literal) list"
Andreas@58039
    71
type_synonym body = "xml_tree list"
Andreas@58039
    72
Andreas@58039
    73
definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
Andreas@58039
    74
where [code del]: "Elem _ _ _ = XML_Tree"
Andreas@58039
    75
Andreas@58039
    76
definition Text :: "String.literal \<Rightarrow> xml_tree"
Andreas@58039
    77
where [code del]: "Text _ = XML_Tree"
Andreas@58039
    78
Andreas@58039
    79
definition node :: "xml_tree list \<Rightarrow> xml_tree"
Andreas@58039
    80
where "node ts = Elem (STR '':'') [] ts"
Andreas@58039
    81
Andreas@58039
    82
definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
Andreas@58039
    83
where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
Andreas@58039
    84
Andreas@58039
    85
definition list where "list f xs = map (node \<circ> f) xs"
Andreas@58039
    86
haftmann@62597
    87
definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
haftmann@62597
    88
definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
Andreas@58039
    89
definition XY :: yxml_of_term where "XY = yot_append X Y"
Andreas@58039
    90
definition XYX :: yxml_of_term where "XYX = yot_append XY X"
Andreas@58039
    91
Andreas@58039
    92
end
Andreas@58039
    93
Andreas@58039
    94
code_datatype xml.Elem xml.Text
Andreas@58039
    95
Andreas@58039
    96
definition yxml_string_of_xml_tree :: "xml_tree \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
Andreas@58039
    97
where [code del]: "yxml_string_of_xml_tree _ _ = YXML"
Andreas@58039
    98
Andreas@58039
    99
lemma yxml_string_of_xml_tree_code [code]:
Andreas@58039
   100
  "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
Andreas@58039
   101
   yot_append xml.XY (
Andreas@58039
   102
   yot_append (yot_literal name) (
wenzelm@64578
   103
   foldr (\<lambda>(a, x) rest.
Andreas@58039
   104
     yot_append xml.Y (
Andreas@58039
   105
     yot_append (yot_literal a) (
Andreas@58039
   106
     yot_append (yot_literal (STR ''='')) (
Andreas@58039
   107
     yot_append (yot_literal x) rest)))) atts (
Andreas@58039
   108
   foldr yxml_string_of_xml_tree ts (
Andreas@58039
   109
   yot_append xml.XYX rest))))"
Andreas@58039
   110
  "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
Andreas@58039
   111
by(rule yot_anything)+
Andreas@58039
   112
Andreas@58039
   113
definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term"
Andreas@58039
   114
where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
Andreas@58039
   115
wenzelm@60500
   116
text \<open>
wenzelm@63680
   117
  Encoding @{typ Code_Evaluation.term} into XML trees as defined in
wenzelm@63680
   118
  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
wenzelm@60500
   119
\<close>
Andreas@58039
   120
Andreas@58039
   121
definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
Andreas@58039
   122
where [code del]: "xml_of_typ _ = [XML_Tree]"
Andreas@58039
   123
Andreas@58039
   124
definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body"
Andreas@58039
   125
where [code del]: "xml_of_term _ = [XML_Tree]"
Andreas@58039
   126
Andreas@58039
   127
lemma xml_of_typ_code [code]:
Andreas@58039
   128
  "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
Andreas@58039
   129
by(simp add: xml_of_typ_def xml_tree_anything)
Andreas@58039
   130
Andreas@58039
   131
lemma xml_of_term_code [code]:
Andreas@58039
   132
  "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
Andreas@58039
   133
  "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)]]"
Andreas@58039
   134
  "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)]]"
wenzelm@61585
   135
  \<comment> \<open>
hoelzl@58637
   136
    FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
Andreas@58039
   137
    uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
wenzelm@60500
   138
\<close>
Andreas@58039
   139
  "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
Andreas@58039
   140
by(simp_all add: xml_of_term_def xml_tree_anything)
Andreas@58039
   141
Andreas@58039
   142
definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term"
Andreas@58039
   143
where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
Andreas@58039
   144
wenzelm@60500
   145
subsection \<open>Test engine and drivers\<close>
Andreas@58039
   146
Andreas@58039
   147
ML_file "code_test.ML"
Andreas@58039
   148
Andreas@58039
   149
end