7 theory Code_Test |
7 theory Code_Test |
8 imports Main |
8 imports Main |
9 keywords "test_code" :: diag |
9 keywords "test_code" :: diag |
10 begin |
10 begin |
11 |
11 |
12 subsection {* YXML encoding for @{typ Code_Evaluation.term} *} |
12 subsection \<open>YXML encoding for @{typ Code_Evaluation.term}\<close> |
13 |
13 |
14 datatype (plugins del: code size "quickcheck") yxml_of_term = YXML |
14 datatype (plugins del: code size "quickcheck") yxml_of_term = YXML |
15 |
15 |
16 lemma yot_anything: "x = (y :: yxml_of_term)" |
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) |
17 by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp) |
22 definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term" |
22 definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term" |
23 where [code del]: "yot_append _ _ = YXML" |
23 where [code del]: "yot_append _ _ = YXML" |
24 definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term" |
24 definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term" |
25 where [code del]: "yot_concat _ = YXML" |
25 where [code del]: "yot_concat _ = YXML" |
26 |
26 |
27 text {* Serialise @{typ yxml_of_term} to native string of target language *} |
27 text \<open>Serialise @{typ yxml_of_term} to native string of target language\<close> |
28 |
28 |
29 code_printing type_constructor yxml_of_term |
29 code_printing type_constructor yxml_of_term |
30 \<rightharpoonup> (SML) "string" |
30 \<rightharpoonup> (SML) "string" |
31 and (OCaml) "string" |
31 and (OCaml) "string" |
32 and (Haskell) "String" |
32 and (Haskell) "String" |
50 \<rightharpoonup> (SML) "String.concat" |
50 \<rightharpoonup> (SML) "String.concat" |
51 and (OCaml) "String.concat \"\"" |
51 and (OCaml) "String.concat \"\"" |
52 and (Haskell) "Prelude.concat" |
52 and (Haskell) "Prelude.concat" |
53 and (Scala) "_.mkString(\"\")" |
53 and (Scala) "_.mkString(\"\")" |
54 |
54 |
55 text {* |
55 text \<open> |
56 Stripped-down implementations of Isabelle's XML tree with YXML encoding |
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"} |
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"}. |
58 sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}. |
59 *} |
59 \<close> |
60 |
60 |
61 datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree |
61 datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree |
62 |
62 |
63 lemma xml_tree_anything: "x = (y :: xml_tree)" |
63 lemma xml_tree_anything: "x = (y :: xml_tree)" |
64 by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp) |
64 by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp) |
65 |
65 |
66 context begin |
66 context begin |
67 local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "xml") *} |
67 local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "xml")\<close> |
68 |
68 |
69 type_synonym attributes = "(String.literal \<times> String.literal) list" |
69 type_synonym attributes = "(String.literal \<times> String.literal) list" |
70 type_synonym body = "xml_tree list" |
70 type_synonym body = "xml_tree list" |
71 |
71 |
72 definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree" |
72 definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree" |
110 by(rule yot_anything)+ |
110 by(rule yot_anything)+ |
111 |
111 |
112 definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term" |
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" |
113 where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty" |
114 |
114 |
115 text {* |
115 text \<open> |
116 Encoding @{typ Code_Evaluation.term} into XML trees |
116 Encoding @{typ Code_Evaluation.term} into XML trees |
117 as defined in @{file "~~/src/Pure/term_xml.ML"} |
117 as defined in @{file "~~/src/Pure/term_xml.ML"} |
118 *} |
118 \<close> |
119 |
119 |
120 definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body" |
120 definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body" |
121 where [code del]: "xml_of_typ _ = [XML_Tree]" |
121 where [code del]: "xml_of_typ _ = [XML_Tree]" |
122 |
122 |
123 definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body" |
123 definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body" |
129 |
129 |
130 lemma xml_of_term_code [code]: |
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)]" |
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)]]" |
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)]]" |
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 -- {* |
134 -- \<open> |
135 FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent |
135 FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent |
136 uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. |
136 uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. |
137 *} |
137 \<close> |
138 "xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]" |
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) |
139 by(simp_all add: xml_of_term_def xml_tree_anything) |
140 |
140 |
141 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term" |
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" |
142 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term" |
143 |
143 |
144 subsection {* Test engine and drivers *} |
144 subsection \<open>Test engine and drivers\<close> |
145 |
145 |
146 ML_file "code_test.ML" |
146 ML_file "code_test.ML" |
147 |
147 |
148 end |
148 end |