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