58039
|
1 |
(* Title: Code_Test.thy
|
|
2 |
Author: Andreas Lochbihler, ETH Zurich
|
|
3 |
|
|
4 |
Test infrastructure for the code generator
|
|
5 |
*)
|
|
6 |
|
|
7 |
theory Code_Test
|
|
8 |
imports Main
|
|
9 |
keywords "test_code" "eval_term" :: diag
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
|
|
13 |
|
58310
|
14 |
datatype 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 |
|
|
27 |
text {* Serialise @{typ yxml_of_term} to native string of target language *}
|
|
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 |
|
|
55 |
text {*
|
|
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"}.
|
|
59 |
*}
|
|
60 |
|
58310
|
61 |
datatype 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
|
|
67 |
local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
|
|
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 |
|
|
115 |
text {*
|
|
116 |
Encoding @{typ Code_Evaluation.term} into XML trees
|
|
117 |
as defined in @{file "~~/src/Pure/term_xml.ML"}
|
|
118 |
*}
|
|
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)]]"
|
|
134 |
-- {*
|
|
135 |
FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
|
|
136 |
uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
|
|
137 |
*}
|
|
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 |
|
|
144 |
subsection {* Test engine and drivers *}
|
|
145 |
|
|
146 |
ML_file "code_test.ML"
|
|
147 |
|
|
148 |
end
|