123 Code_Evaluation.App (Code_Evaluation.App |
123 Code_Evaluation.App (Code_Evaluation.App |
124 (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
124 (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
125 (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))" |
125 (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))" |
126 by (subst term_of_anything) rule |
126 by (subst term_of_anything) rule |
127 |
127 |
128 code_type "term" |
128 code_printing |
129 (Eval "Term.term") |
129 type_constructor "term" \<rightharpoonup> (Eval) "Term.term" |
130 |
130 | constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))" |
131 code_const Const and App and Abs and Free |
131 | constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))" |
132 (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))" |
132 | constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))" |
133 and "Term.Free/ ((_), (_))") |
133 | constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))" |
134 |
134 | constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" |
135 code_const "term_of \<Colon> integer \<Rightarrow> term" |
135 | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal" |
136 (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT") |
|
137 |
|
138 code_const "term_of \<Colon> String.literal \<Rightarrow> term" |
|
139 (Eval "HOLogic.mk'_literal") |
|
140 |
136 |
141 code_reserved Eval HOLogic |
137 code_reserved Eval HOLogic |
142 |
138 |
143 |
139 |
144 subsubsection {* Obfuscation *} |
140 subsubsection {* Obfuscation *} |
159 subsection {* Diagnostic *} |
155 subsection {* Diagnostic *} |
160 |
156 |
161 definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
157 definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
162 [code del]: "tracing s x = x" |
158 [code del]: "tracing s x = x" |
163 |
159 |
164 code_const "tracing :: String.literal => 'a => 'a" |
160 code_printing |
165 (Eval "Code'_Evaluation.tracing") |
161 constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing" |
166 |
162 |
167 |
163 |
168 subsection {* Generic reification *} |
164 subsection {* Generic reification *} |
169 |
165 |
170 ML_file "~~/src/HOL/Tools/reification.ML" |
166 ML_file "~~/src/HOL/Tools/reification.ML" |