1 (* Title: HOL/Code_Eval.thy
2 Author: Florian Haftmann, TU Muenchen
5 header {* Term evaluation using the generic code generator *}
8 imports Plain Typerep Code_Index
11 subsection {* Term representation *}
13 subsubsection {* Terms and class @{text term_of} *}
15 datatype "term" = dummy_term
17 definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
18 "Const _ _ = dummy_term"
20 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
21 "App _ _ = dummy_term"
23 code_datatype Const App
25 class term_of = typerep +
26 fixes term_of :: "'a \<Rightarrow> term"
28 lemma term_of_anything: "term_of x \<equiv> t"
29 by (rule eq_reflection) (cases "term_of x", cases t, simp)
31 definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
32 \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
33 "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
35 lemma valapp_code [code, code inline]:
36 "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
37 by (simp only: valapp_def fst_conv snd_conv)
40 subsubsection {* @{text term_of} instances *}
44 fun add_term_of tyco raw_vs thy =
46 val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
47 val ty = Type (tyco, map TFree vs);
48 val lhs = Const (@{const_name term_of}, ty --> @{typ term})
50 val rhs = @{term "undefined \<Colon> term"};
51 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
52 fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
53 o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
56 |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
57 |> `(fn lthy => Syntax.check_term lthy eq)
58 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
60 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
62 fun ensure_term_of (tyco, (raw_vs, _)) thy =
64 val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
65 andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
68 |> need_inst ? add_term_of tyco raw_vs
71 Code.type_interpretation ensure_term_of
77 fun mk_term_of_eq thy ty vs tyco (c, tys) =
79 val t = list_comb (Const (c, tys ---> ty),
80 map Free (Name.names Name.context "a" tys));
81 val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
82 (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
83 val cty = Thm.ctyp_of thy ty;
85 @{thm term_of_anything}
86 |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
89 fun add_term_of_code tyco raw_vs raw_cs thy =
91 val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
92 val ty = Type (tyco, map TFree vs);
93 val cs = (map o apsnd o map o map_atyps)
94 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
95 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
96 val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
99 |> Code.del_eqns const
100 |> fold Code.add_eqn eqs
102 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
104 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
107 |> has_inst ? add_term_of_code tyco raw_vs cs
110 Code.type_interpretation ensure_term_of_code
115 subsubsection {* Code generator setup *}
117 lemmas [code del] = term.recs term.cases term.size
118 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
120 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
121 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
122 lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
123 lemma [code, code del]:
124 "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
125 lemma [code, code del]:
126 "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
128 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
129 (let (n, m) = nibble_pair_of_char c
130 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
131 (Code_Eval.term_of n)) (Code_Eval.term_of m))"
132 by (subst term_of_anything) rule
137 code_const Const and App
138 (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
140 code_const "term_of \<Colon> message_string \<Rightarrow> term"
141 (Eval "HOLogic.mk'_message'_string")
143 code_reserved Eval HOLogic
146 subsubsection {* Syntax *}
148 definition termify :: "'a \<Rightarrow> term" where
149 [code del]: "termify x = dummy_term"
151 abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
152 "valtermify x \<equiv> (x, \<lambda>u. termify x)"
156 fun map_default f xs =
157 let val ys = map f xs
158 in if exists is_some ys
159 then SOME (map2 the_default xs ys)
162 fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
163 if not (Term.has_abs t)
164 then if fold_aterms (fn Const _ => I | _ => K false) t true
165 then SOME (HOLogic.reflect_term t)
166 else error "Cannot termify expression containing variables"
167 else error "Cannot termify expression containing abstraction"
168 | subst_termify_app (t, ts) = case map_default subst_termify ts
169 of SOME ts' => SOME (list_comb (t, ts'))
171 and subst_termify (Abs (v, T, t)) = (case subst_termify t
172 of SOME t' => SOME (Abs (v, T, t'))
174 | subst_termify t = subst_termify_app (strip_comb t)
175 fun check_termify ts ctxt = map_default subst_termify ts
176 |> Option.map (rpair ctxt)
178 Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
185 notation App (infixl "<\<cdot>>" 70)
186 and valapp (infixl "{\<cdot>}" 70)
190 interpretation term_syntax .
192 no_notation App (infixl "<\<cdot>>" 70)
193 and valapp (infixl "{\<cdot>}" 70)
196 subsection {* Numeric types *}
198 definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
199 "term_of_num two = (\<lambda>_. dummy_term)"
201 lemma (in term_syntax) term_of_num_code [code]:
202 "term_of_num two k = (if k = 0 then termify Int.Pls
203 else (if k mod two = 0
204 then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
205 else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
206 by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
208 lemma (in term_syntax) term_of_nat_code [code]:
209 "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
210 by (simp only: term_of_anything)
212 lemma (in term_syntax) term_of_int_code [code]:
213 "term_of (k::int) = (if k = 0 then termify (0 :: int)
214 else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
215 else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
216 by (simp only: term_of_anything)
218 lemma (in term_syntax) term_of_index_code [code]:
219 "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
220 by (simp only: term_of_anything)
222 subsection {* Obfuscate *}
226 val term = Const ("<TERM>", dummyT);
227 fun tr1' [_, _] = term;
230 [(@{const_syntax Const}, tr1'),
231 (@{const_syntax App}, tr1'),
232 (@{const_syntax dummy_term}, tr2')]
236 hide const dummy_term App valapp
237 hide (open) const Const termify valtermify term_of term_of_num
240 subsection {* Evaluation setup *}
245 val eval_ref: (unit -> term) option ref
246 val eval_term: theory -> term -> term
249 structure Eval : EVAL =
252 val eval_ref = ref (NONE : (unit -> term) option);
254 fun eval_term thy t =
255 Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
261 Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)