author  haftmann 
Fri, 15 Feb 2013 08:31:31 +0100  
changeset 51144  0ede9e2266a8 
parent 51143  0a2371e7ced3 
child 51160  599ff65b85e2 
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 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
51112
diff
changeset

8 
imports Typerep Limited_Sequence 
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 

51144  136 
code_const "term_of \<Colon> integer \<Rightarrow> term" 
137 
(Eval "HOLogic.mk'_number/ HOLogic.code'_integerT") 

138 

39564  139 
code_const "term_of \<Colon> String.literal \<Rightarrow> term" 
140 
(Eval "HOLogic.mk'_literal") 

141 

142 
code_reserved Eval HOLogic 

143 

144 

145 
subsubsection {* Obfuscation *} 

31178  146 

147 
print_translation {* 

148 
let 

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

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

151 
fun tr2' [] = term; 

152 
in 

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

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

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

156 
end 

157 
*} 

158 

159 

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

161 

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

162 
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

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

164 

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

165 
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

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

167 

31178  168 

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

169 
hide_const dummy_term valapp 
51144  170 
hide_const (open) Const App Abs Free termify valtermify term_of tracing 
28228  171 

172 
end 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

173 