author | wenzelm |
Mon, 05 Sep 2016 23:11:00 +0200 | |
changeset 63806 | c54a53ef1873 |
parent 63161 | 2660ba498798 |
child 66013 | 03002d10bf1d |
permissions | -rw-r--r-- |
32657 | 1 |
(* Title: HOL/Code_Evaluation.thy |
28228 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
60758 | 5 |
section \<open>Term evaluation using the generic code generator\<close> |
28228 | 6 |
|
32657 | 7 |
theory Code_Evaluation |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
51112
diff
changeset
|
8 |
imports Typerep Limited_Sequence |
56925 | 9 |
keywords "value" :: diag |
28228 | 10 |
begin |
11 |
||
60758 | 12 |
subsection \<open>Term representation\<close> |
28228 | 13 |
|
61799 | 14 |
subsubsection \<open>Terms and class \<open>term_of\<close>\<close> |
28228 | 15 |
|
58350
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
16 |
datatype (plugins only: code extraction) "term" = dummy_term |
28228 | 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 |
|
42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset
|
27 |
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
|
28 |
"Free _ _ = dummy_term" |
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset
|
29 |
|
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset
|
30 |
code_datatype Const App Abs Free |
28228 | 31 |
|
28335 | 32 |
class term_of = typerep + |
31031 | 33 |
fixes term_of :: "'a \<Rightarrow> term" |
28228 | 34 |
|
35 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
36 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
37 |
||
31191 | 38 |
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) |
31178 | 39 |
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where |
31191 | 40 |
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" |
31178 | 41 |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
42 |
lemma valapp_code [code, code_unfold]: |
31191 | 43 |
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" |
44 |
by (simp only: valapp_def fst_conv snd_conv) |
|
31178 | 45 |
|
28228 | 46 |
|
60758 | 47 |
subsubsection \<open>Syntax\<close> |
31178 | 48 |
|
31191 | 49 |
definition termify :: "'a \<Rightarrow> term" where |
50 |
[code del]: "termify x = dummy_term" |
|
51 |
||
52 |
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where |
|
53 |
"valtermify x \<equiv> (x, \<lambda>u. termify x)" |
|
31178 | 54 |
|
55 |
locale term_syntax |
|
56 |
begin |
|
57 |
||
31191 | 58 |
notation App (infixl "<\<cdot>>" 70) |
59 |
and valapp (infixl "{\<cdot>}" 70) |
|
31178 | 60 |
|
61 |
end |
|
62 |
||
63 |
interpretation term_syntax . |
|
64 |
||
31191 | 65 |
no_notation App (infixl "<\<cdot>>" 70) |
66 |
and valapp (infixl "{\<cdot>}" 70) |
|
67 |
||
68 |
||
60758 | 69 |
subsection \<open>Tools setup and evaluation\<close> |
39564 | 70 |
|
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
71 |
context |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
72 |
begin |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
73 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
74 |
qualified definition TERM_OF :: "'a::term_of itself" |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
75 |
where |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
76 |
"TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))" |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
77 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
78 |
qualified definition TERM_OF_EQUAL :: "'a::term_of itself" |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
79 |
where |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
80 |
"TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))" |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
81 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
82 |
end |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
62958
diff
changeset
|
83 |
|
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
84 |
lemma eq_eq_TrueD: |
62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62597
diff
changeset
|
85 |
fixes x y :: "'a::{}" |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
86 |
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
|
87 |
shows "x \<equiv> y" |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
88 |
using assms by simp |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset
|
89 |
|
56928
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
90 |
code_printing |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
91 |
type_constructor "term" \<rightharpoonup> (Eval) "Term.term" |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
92 |
| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))" |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
93 |
| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))" |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
94 |
| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))" |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
95 |
| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))" |
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
96 |
|
48891 | 97 |
ML_file "Tools/code_evaluation.ML" |
39564 | 98 |
|
99 |
code_reserved Eval Code_Evaluation |
|
100 |
||
63806 | 101 |
ML_file "~~/src/HOL/Tools/value_command.ML" |
56928
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
102 |
|
39564 | 103 |
|
61799 | 104 |
subsection \<open>\<open>term_of\<close> instances\<close> |
39564 | 105 |
|
106 |
instantiation "fun" :: (typerep, typerep) term_of |
|
107 |
begin |
|
108 |
||
109 |
definition |
|
61076 | 110 |
"term_of (f :: 'a \<Rightarrow> 'b) = |
56241 | 111 |
Const (STR ''Pure.dummy_pattern'') |
112 |
(Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" |
|
39564 | 113 |
|
114 |
instance .. |
|
115 |
||
116 |
end |
|
117 |
||
58334 | 118 |
declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _" |
56926 | 119 |
"term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _" |
120 |
"term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]] |
|
39564 | 121 |
|
62597 | 122 |
definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a" |
123 |
where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))" |
|
124 |
||
125 |
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]: |
|
126 |
"term_of = |
|
127 |
case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) |
|
128 |
(\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))" |
|
129 |
by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq]) |
|
39564 | 130 |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
131 |
lemma term_of_string [code]: |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
132 |
"term_of s = App (Const (STR ''STR'') |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
133 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
134 |
Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
135 |
by (subst term_of_anything) rule |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
136 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52286
diff
changeset
|
137 |
code_printing |
61076 | 138 |
constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" |
139 |
| constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal" |
|
39564 | 140 |
|
58036
f23045003476
add code equation for term_of on integer
Andreas Lochbihler
parents:
56928
diff
changeset
|
141 |
declare [[code drop: "term_of :: integer \<Rightarrow> _"]] |
f23045003476
add code equation for term_of on integer
Andreas Lochbihler
parents:
56928
diff
changeset
|
142 |
|
f23045003476
add code equation for term_of on integer
Andreas Lochbihler
parents:
56928
diff
changeset
|
143 |
lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]: |
58038
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
144 |
"term_of (i :: integer) = |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
145 |
(if i > 0 then |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
146 |
App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer))) |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
147 |
(term_of (num_of_integer i)) |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
148 |
else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer) |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
149 |
else |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
150 |
App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer)) |
f8e6197668c9
correct code equation for term_of on integer
Andreas Lochbihler
parents:
58036
diff
changeset
|
151 |
(term_of (- i)))" |
62597 | 152 |
by (rule term_of_anything [THEN meta_eq_to_obj_eq]) |
58036
f23045003476
add code equation for term_of on integer
Andreas Lochbihler
parents:
56928
diff
changeset
|
153 |
|
39564 | 154 |
code_reserved Eval HOLogic |
155 |
||
156 |
||
60758 | 157 |
subsection \<open>Generic reification\<close> |
31178 | 158 |
|
56928
1e50fddbe1f5
dropped term_of obfuscation -- not really required;
haftmann
parents:
56927
diff
changeset
|
159 |
ML_file "~~/src/HOL/Tools/reification.ML" |
31178 | 160 |
|
161 |
||
60758 | 162 |
subsection \<open>Diagnostic\<close> |
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
|
163 |
|
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 |
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
|
165 |
[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
|
166 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52286
diff
changeset
|
167 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52286
diff
changeset
|
168 |
constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing" |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
169 |
|
31178 | 170 |
|
40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset
|
171 |
hide_const dummy_term valapp |
51144 | 172 |
hide_const (open) Const App Abs Free termify valtermify term_of tracing |
28228 | 173 |
|
174 |
end |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
175 |