author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 50055  94041d602ecb 
permissions  rwrr 
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 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

8 
imports Plain Typerep Code_Numeral Predicate 
28228  9 
begin 
10 

11 
subsection {* Term representation *} 

12 

13 
subsubsection {* Terms and class @{text term_of} *} 

14 

15 
datatype "term" = dummy_term 

16 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

17 
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 
28228  18 
"Const _ _ = dummy_term" 
19 

28661  20 
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where 
28228  21 
"App _ _ = dummy_term" 
22 

40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

23 
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

24 
"Abs _ _ _ = dummy_term" 
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

25 

42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

26 
definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

27 
"Free _ _ = dummy_term" 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

28 

5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

29 
code_datatype Const App Abs Free 
28228  30 

28335  31 
class term_of = typerep + 
31031  32 
fixes term_of :: "'a \<Rightarrow> term" 
28228  33 

34 
lemma term_of_anything: "term_of x \<equiv> t" 

35 
by (rule eq_reflection) (cases "term_of x", cases t, simp) 

36 

31191  37 
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) 
31178  38 
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where 
31191  39 
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" 
31178  40 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

41 
lemma valapp_code [code, code_unfold]: 
31191  42 
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" 
43 
by (simp only: valapp_def fst_conv snd_conv) 

31178  44 

28228  45 

31178  46 
subsubsection {* Syntax *} 
47 

31191  48 
definition termify :: "'a \<Rightarrow> term" where 
49 
[code del]: "termify x = dummy_term" 

50 

51 
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where 

52 
"valtermify x \<equiv> (x, \<lambda>u. termify x)" 

31178  53 

54 
locale term_syntax 

55 
begin 

56 

31191  57 
notation App (infixl "<\<cdot>>" 70) 
58 
and valapp (infixl "{\<cdot>}" 70) 

31178  59 

60 
end 

61 

62 
interpretation term_syntax . 

63 

31191  64 
no_notation App (infixl "<\<cdot>>" 70) 
65 
and valapp (infixl "{\<cdot>}" 70) 

66 

67 

39564  68 
subsection {* Tools setup and evaluation *} 
69 

39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

70 
lemma eq_eq_TrueD: 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

71 
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

72 
shows "x \<equiv> y" 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

73 
using assms by simp 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

74 

48891  75 
ML_file "Tools/code_evaluation.ML" 
39564  76 

77 
code_reserved Eval Code_Evaluation 

78 

79 
setup {* Code_Evaluation.setup *} 

80 

81 

82 
subsection {* @{text term_of} instances *} 

83 

84 
instantiation "fun" :: (typerep, typerep) term_of 

85 
begin 

86 

87 
definition 

88 
"term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') 

89 
[Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" 

90 

91 
instance .. 

92 

93 
end 

94 

95 
instantiation String.literal :: term_of 

96 
begin 

97 

98 
definition 

99 
"term_of s = App (Const (STR ''STR'') 

100 
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], 

101 
Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" 

102 

103 
instance .. 

104 

105 
end 

106 

107 

108 
subsubsection {* Code generator setup *} 

109 

110 
lemmas [code del] = term.recs term.cases term.size 

111 
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" .. 

112 

113 
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. 

114 
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. 

115 
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" .. 

116 
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) 

117 
= Code_Evaluation.term_of" .. 

118 
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) 

119 
= Code_Evaluation.term_of" .. 

120 

121 
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: 

122 
"Code_Evaluation.term_of c = 

123 
(let (n, m) = nibble_pair_of_char c 

124 
in Code_Evaluation.App (Code_Evaluation.App 

125 
(Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) 

126 
(Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" 

127 
by (subst term_of_anything) rule 

128 

129 
code_type "term" 

130 
(Eval "Term.term") 

131 

42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

132 
code_const Const and App and Abs and Free 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

133 
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))" 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

134 
and "Term.Free/ ((_), (_))") 
39564  135 

136 
code_const "term_of \<Colon> String.literal \<Rightarrow> term" 

137 
(Eval "HOLogic.mk'_literal") 

138 

139 
code_reserved Eval HOLogic 

140 

141 

142 
subsubsection {* Numeric types *} 

31191  143 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

144 
definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

145 
"term_of_num_semiring two = (\<lambda>_. dummy_term)" 
31191  146 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

147 
lemma (in term_syntax) term_of_num_semiring_code [code]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

148 
"term_of_num_semiring two k = ( 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

149 
if k = 1 then termify Num.One 
31191  150 
else (if k mod two = 0 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

151 
then termify Num.Bit0 <\<cdot>> term_of_num_semiring two (k div two) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

152 
else termify Num.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

153 
by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def) 
31191  154 

155 
lemma (in term_syntax) term_of_nat_code [code]: 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

156 
"term_of (n::nat) = ( 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

157 
if n = 0 then termify (0 :: nat) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

158 
else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)" 
31191  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]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

162 
"term_of (k::code_numeral) = ( 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

163 
if k = 0 then termify (0 :: code_numeral) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

164 
else termify (numeral :: num \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k)" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31191
diff
changeset

165 
by (simp only: term_of_anything) 
31191  166 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

167 
lemma (in term_syntax) term_of_int_code [code]: 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

168 
"term_of (k::int) = (if k = 0 then termify (0 :: int) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

169 
else if k < 0 then termify (neg_numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) ( k) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

170 
else termify (numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) k)" 
40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

171 
by (simp only: term_of_anything) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

172 

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

173 

39564  174 
subsubsection {* Obfuscation *} 
31178  175 

176 
print_translation {* 

177 
let 

178 
val term = Const ("<TERM>", dummyT); 

179 
fun tr1' [_, _] = term; 

180 
fun tr2' [] = term; 

181 
in 

182 
[(@{const_syntax Const}, tr1'), 

183 
(@{const_syntax App}, tr1'), 

184 
(@{const_syntax dummy_term}, tr2')] 

185 
end 

186 
*} 

187 

188 

39564  189 
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

190 

6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

191 
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

192 
[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

193 

33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

194 
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

195 
(Eval "Code'_Evaluation.tracing") 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

196 

31178  197 

40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

198 
hide_const dummy_term valapp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

199 
hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing 
28228  200 

201 
end 