author | bulwahn |
Mon, 22 Nov 2010 10:41:57 +0100 | |
changeset 40638 | 6b137c96df07 |
parent 39567 | 5ee997fbe5cc |
child 40883 | b37dca06477f |
permissions | -rw-r--r-- |
32657 | 1 |
(* Title: HOL/Code_Evaluation.thy |
28228 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Term evaluation using the generic code generator *} |
|
6 |
||
32657 | 7 |
theory Code_Evaluation |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
8 |
imports Plain Typerep Code_Numeral |
39564 | 9 |
uses ("Tools/code_evaluation.ML") |
28228 | 10 |
begin |
11 |
||
12 |
subsection {* Term representation *} |
|
13 |
||
14 |
subsubsection {* Terms and class @{text term_of} *} |
|
15 |
||
16 |
datatype "term" = dummy_term |
|
17 |
||
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
18 |
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where |
28228 | 19 |
"Const _ _ = dummy_term" |
20 |
||
28661 | 21 |
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where |
28228 | 22 |
"App _ _ = dummy_term" |
23 |
||
40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
24 |
definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where |
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
25 |
"Abs _ _ _ = dummy_term" |
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
26 |
|
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
27 |
code_datatype Const App Abs |
28228 | 28 |
|
28335 | 29 |
class term_of = typerep + |
31031 | 30 |
fixes term_of :: "'a \<Rightarrow> term" |
28228 | 31 |
|
32 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
33 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
34 |
||
31191 | 35 |
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) |
31178 | 36 |
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where |
31191 | 37 |
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" |
31178 | 38 |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
39 |
lemma valapp_code [code, code_unfold]: |
31191 | 40 |
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" |
41 |
by (simp only: valapp_def fst_conv snd_conv) |
|
31178 | 42 |
|
28228 | 43 |
|
31178 | 44 |
subsubsection {* Syntax *} |
45 |
||
31191 | 46 |
definition termify :: "'a \<Rightarrow> term" where |
47 |
[code del]: "termify x = dummy_term" |
|
48 |
||
49 |
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where |
|
50 |
"valtermify x \<equiv> (x, \<lambda>u. termify x)" |
|
31178 | 51 |
|
52 |
locale term_syntax |
|
53 |
begin |
|
54 |
||
31191 | 55 |
notation App (infixl "<\<cdot>>" 70) |
56 |
and valapp (infixl "{\<cdot>}" 70) |
|
31178 | 57 |
|
58 |
end |
|
59 |
||
60 |
interpretation term_syntax . |
|
61 |
||
31191 | 62 |
no_notation App (infixl "<\<cdot>>" 70) |
63 |
and valapp (infixl "{\<cdot>}" 70) |
|
64 |
||
65 |
||
39564 | 66 |
subsection {* Tools setup and evaluation *} |
67 |
||
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
68 |
lemma eq_eq_TrueD: |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
69 |
assumes "(x \<equiv> y) \<equiv> Trueprop True" |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
70 |
shows "x \<equiv> y" |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
71 |
using assms by simp |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
72 |
|
39564 | 73 |
use "Tools/code_evaluation.ML" |
74 |
||
75 |
code_reserved Eval Code_Evaluation |
|
76 |
||
77 |
setup {* Code_Evaluation.setup *} |
|
78 |
||
79 |
||
80 |
subsection {* @{text term_of} instances *} |
|
81 |
||
82 |
instantiation "fun" :: (typerep, typerep) term_of |
|
83 |
begin |
|
84 |
||
85 |
definition |
|
86 |
"term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') |
|
87 |
[Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" |
|
88 |
||
89 |
instance .. |
|
90 |
||
91 |
end |
|
92 |
||
93 |
instantiation String.literal :: term_of |
|
94 |
begin |
|
95 |
||
96 |
definition |
|
97 |
"term_of s = App (Const (STR ''STR'') |
|
98 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], |
|
99 |
Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" |
|
100 |
||
101 |
instance .. |
|
102 |
||
103 |
end |
|
104 |
||
105 |
||
106 |
subsubsection {* Code generator setup *} |
|
107 |
||
108 |
lemmas [code del] = term.recs term.cases term.size |
|
109 |
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" .. |
|
110 |
||
111 |
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
|
112 |
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
|
113 |
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" .. |
|
114 |
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) |
|
115 |
= Code_Evaluation.term_of" .. |
|
116 |
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) |
|
117 |
= Code_Evaluation.term_of" .. |
|
118 |
||
119 |
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: |
|
120 |
"Code_Evaluation.term_of c = |
|
121 |
(let (n, m) = nibble_pair_of_char c |
|
122 |
in Code_Evaluation.App (Code_Evaluation.App |
|
123 |
(Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
|
124 |
(Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" |
|
125 |
by (subst term_of_anything) rule |
|
126 |
||
127 |
code_type "term" |
|
128 |
(Eval "Term.term") |
|
129 |
||
40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
130 |
code_const Const and App and Abs |
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
131 |
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))") |
39564 | 132 |
|
133 |
code_const "term_of \<Colon> String.literal \<Rightarrow> term" |
|
134 |
(Eval "HOLogic.mk'_literal") |
|
135 |
||
136 |
code_reserved Eval HOLogic |
|
137 |
||
138 |
||
139 |
subsubsection {* Numeric types *} |
|
31191 | 140 |
|
141 |
definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where |
|
142 |
"term_of_num two = (\<lambda>_. dummy_term)" |
|
143 |
||
144 |
lemma (in term_syntax) term_of_num_code [code]: |
|
145 |
"term_of_num two k = (if k = 0 then termify Int.Pls |
|
146 |
else (if k mod two = 0 |
|
147 |
then termify Int.Bit0 <\<cdot>> term_of_num two (k div two) |
|
148 |
else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))" |
|
149 |
by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) |
|
150 |
||
151 |
lemma (in term_syntax) term_of_nat_code [code]: |
|
152 |
"term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n" |
|
153 |
by (simp only: term_of_anything) |
|
154 |
||
155 |
lemma (in term_syntax) term_of_int_code [code]: |
|
156 |
"term_of (k::int) = (if k = 0 then termify (0 :: int) |
|
157 |
else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k |
|
158 |
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))" |
|
159 |
by (simp only: term_of_anything) |
|
160 |
||
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
161 |
lemma (in term_syntax) term_of_code_numeral_code [code]: |
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
162 |
"term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k" |
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31191
diff
changeset
|
163 |
by (simp only: term_of_anything) |
31191 | 164 |
|
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
165 |
|
39564 | 166 |
subsubsection {* Obfuscation *} |
31178 | 167 |
|
168 |
print_translation {* |
|
169 |
let |
|
170 |
val term = Const ("<TERM>", dummyT); |
|
171 |
fun tr1' [_, _] = term; |
|
172 |
fun tr2' [] = term; |
|
173 |
in |
|
174 |
[(@{const_syntax Const}, tr1'), |
|
175 |
(@{const_syntax App}, tr1'), |
|
176 |
(@{const_syntax dummy_term}, tr2')] |
|
177 |
end |
|
178 |
*} |
|
179 |
||
180 |
||
39564 | 181 |
subsection {* Diagnostic *} |
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
182 |
|
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
183 |
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
184 |
[code del]: "tracing s x = x" |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
185 |
|
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
186 |
code_const "tracing :: String.literal => 'a => 'a" |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
187 |
(Eval "Code'_Evaluation.tracing") |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
188 |
|
31178 | 189 |
|
40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
190 |
hide_const dummy_term valapp |
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
191 |
hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing |
28228 | 192 |
|
193 |
end |