equal
deleted
inserted
replaced
22 "App _ _ = dummy_term" |
22 "App _ _ = dummy_term" |
23 |
23 |
24 definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where |
24 definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where |
25 "Abs _ _ _ = dummy_term" |
25 "Abs _ _ _ = dummy_term" |
26 |
26 |
27 code_datatype Const App Abs |
27 definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where |
|
28 "Free _ _ = dummy_term" |
|
29 |
|
30 code_datatype Const App Abs Free |
28 |
31 |
29 class term_of = typerep + |
32 class term_of = typerep + |
30 fixes term_of :: "'a \<Rightarrow> term" |
33 fixes term_of :: "'a \<Rightarrow> term" |
31 |
34 |
32 lemma term_of_anything: "term_of x \<equiv> t" |
35 lemma term_of_anything: "term_of x \<equiv> t" |
125 by (subst term_of_anything) rule |
128 by (subst term_of_anything) rule |
126 |
129 |
127 code_type "term" |
130 code_type "term" |
128 (Eval "Term.term") |
131 (Eval "Term.term") |
129 |
132 |
130 code_const Const and App and Abs |
133 code_const Const and App and Abs and Free |
131 (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))") |
134 (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))" |
|
135 and "Term.Free/ ((_), (_))") |
132 |
136 |
133 code_const "term_of \<Colon> String.literal \<Rightarrow> term" |
137 code_const "term_of \<Colon> String.literal \<Rightarrow> term" |
134 (Eval "HOLogic.mk'_literal") |
138 (Eval "HOLogic.mk'_literal") |
135 |
139 |
136 code_reserved Eval HOLogic |
140 code_reserved Eval HOLogic |
195 code_const "tracing :: String.literal => 'a => 'a" |
199 code_const "tracing :: String.literal => 'a => 'a" |
196 (Eval "Code'_Evaluation.tracing") |
200 (Eval "Code'_Evaluation.tracing") |
197 |
201 |
198 |
202 |
199 hide_const dummy_term valapp |
203 hide_const dummy_term valapp |
200 hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing |
204 hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring term_of_num_ring tracing |
201 |
205 |
202 end |
206 end |