1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Code_Evaluation.thy Wed Sep 23 14:00:12 2009 +0200
1.3 @@ -0,0 +1,271 @@
1.4 +(* Title: HOL/Code_Evaluation.thy
1.5 + Author: Florian Haftmann, TU Muenchen
1.6 +*)
1.7 +
1.8 +header {* Term evaluation using the generic code generator *}
1.9 +
1.10 +theory Code_Evaluation
1.11 +imports Plain Typerep Code_Numeral
1.12 +begin
1.13 +
1.14 +subsection {* Term representation *}
1.15 +
1.16 +subsubsection {* Terms and class @{text term_of} *}
1.17 +
1.18 +datatype "term" = dummy_term
1.19 +
1.20 +definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
1.21 + "Const _ _ = dummy_term"
1.22 +
1.23 +definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
1.24 + "App _ _ = dummy_term"
1.25 +
1.26 +code_datatype Const App
1.27 +
1.28 +class term_of = typerep +
1.29 + fixes term_of :: "'a \<Rightarrow> term"
1.30 +
1.31 +lemma term_of_anything: "term_of x \<equiv> t"
1.32 + by (rule eq_reflection) (cases "term_of x", cases t, simp)
1.33 +
1.34 +definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
1.35 + \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
1.36 + "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
1.37 +
1.38 +lemma valapp_code [code, code_unfold]:
1.39 + "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
1.40 + by (simp only: valapp_def fst_conv snd_conv)
1.41 +
1.42 +
1.43 +subsubsection {* @{text term_of} instances *}
1.44 +
1.45 +instantiation "fun" :: (typerep, typerep) term_of
1.46 +begin
1.47 +
1.48 +definition
1.49 + "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
1.50 + [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
1.51 +
1.52 +instance ..
1.53 +
1.54 +end
1.55 +
1.56 +setup {*
1.57 +let
1.58 + fun add_term_of tyco raw_vs thy =
1.59 + let
1.60 + val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
1.61 + val ty = Type (tyco, map TFree vs);
1.62 + val lhs = Const (@{const_name term_of}, ty --> @{typ term})
1.63 + $ Free ("x", ty);
1.64 + val rhs = @{term "undefined \<Colon> term"};
1.65 + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
1.66 + fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
1.67 + o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
1.68 + in
1.69 + thy
1.70 + |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
1.71 + |> `(fn lthy => Syntax.check_term lthy eq)
1.72 + |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
1.73 + |> snd
1.74 + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.75 + end;
1.76 + fun ensure_term_of (tyco, (raw_vs, _)) thy =
1.77 + let
1.78 + val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
1.79 + andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
1.80 + in if need_inst then add_term_of tyco raw_vs thy else thy end;
1.81 +in
1.82 + Code.type_interpretation ensure_term_of
1.83 +end
1.84 +*}
1.85 +
1.86 +setup {*
1.87 +let
1.88 + fun mk_term_of_eq thy ty vs tyco (c, tys) =
1.89 + let
1.90 + val t = list_comb (Const (c, tys ---> ty),
1.91 + map Free (Name.names Name.context "a" tys));
1.92 + val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
1.93 + (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
1.94 + val cty = Thm.ctyp_of thy ty;
1.95 + in
1.96 + @{thm term_of_anything}
1.97 + |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
1.98 + |> Thm.varifyT
1.99 + end;
1.100 + fun add_term_of_code tyco raw_vs raw_cs thy =
1.101 + let
1.102 + val algebra = Sign.classes_of thy;
1.103 + val vs = map (fn (v, sort) =>
1.104 + (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
1.105 + val ty = Type (tyco, map TFree vs);
1.106 + val cs = (map o apsnd o map o map_atyps)
1.107 + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
1.108 + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
1.109 + val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
1.110 + in
1.111 + thy
1.112 + |> Code.del_eqns const
1.113 + |> fold Code.add_eqn eqs
1.114 + end;
1.115 + fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
1.116 + let
1.117 + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
1.118 + in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
1.119 +in
1.120 + Code.type_interpretation ensure_term_of_code
1.121 +end
1.122 +*}
1.123 +
1.124 +
1.125 +subsubsection {* Code generator setup *}
1.126 +
1.127 +lemmas [code del] = term.recs term.cases term.size
1.128 +lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
1.129 +
1.130 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
1.131 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
1.132 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
1.133 +lemma [code, code del]:
1.134 + "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
1.135 +lemma [code, code del]:
1.136 + "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
1.137 +
1.138 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
1.139 + (let (n, m) = nibble_pair_of_char c
1.140 + in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
1.141 + (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
1.142 + by (subst term_of_anything) rule
1.143 +
1.144 +code_type "term"
1.145 + (Eval "Term.term")
1.146 +
1.147 +code_const Const and App
1.148 + (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
1.149 +
1.150 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
1.151 + (Eval "HOLogic.mk'_message'_string")
1.152 +
1.153 +code_reserved Eval HOLogic
1.154 +
1.155 +
1.156 +subsubsection {* Syntax *}
1.157 +
1.158 +definition termify :: "'a \<Rightarrow> term" where
1.159 + [code del]: "termify x = dummy_term"
1.160 +
1.161 +abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
1.162 + "valtermify x \<equiv> (x, \<lambda>u. termify x)"
1.163 +
1.164 +setup {*
1.165 +let
1.166 + fun map_default f xs =
1.167 + let val ys = map f xs
1.168 + in if exists is_some ys
1.169 + then SOME (map2 the_default xs ys)
1.170 + else NONE
1.171 + end;
1.172 + fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
1.173 + if not (Term.has_abs t)
1.174 + then if fold_aterms (fn Const _ => I | _ => K false) t true
1.175 + then SOME (HOLogic.reflect_term t)
1.176 + else error "Cannot termify expression containing variables"
1.177 + else error "Cannot termify expression containing abstraction"
1.178 + | subst_termify_app (t, ts) = case map_default subst_termify ts
1.179 + of SOME ts' => SOME (list_comb (t, ts'))
1.180 + | NONE => NONE
1.181 + and subst_termify (Abs (v, T, t)) = (case subst_termify t
1.182 + of SOME t' => SOME (Abs (v, T, t'))
1.183 + | NONE => NONE)
1.184 + | subst_termify t = subst_termify_app (strip_comb t)
1.185 + fun check_termify ts ctxt = map_default subst_termify ts
1.186 + |> Option.map (rpair ctxt)
1.187 +in
1.188 + Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
1.189 +end;
1.190 +*}
1.191 +
1.192 +locale term_syntax
1.193 +begin
1.194 +
1.195 +notation App (infixl "<\<cdot>>" 70)
1.196 + and valapp (infixl "{\<cdot>}" 70)
1.197 +
1.198 +end
1.199 +
1.200 +interpretation term_syntax .
1.201 +
1.202 +no_notation App (infixl "<\<cdot>>" 70)
1.203 + and valapp (infixl "{\<cdot>}" 70)
1.204 +
1.205 +
1.206 +subsection {* Numeric types *}
1.207 +
1.208 +definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
1.209 + "term_of_num two = (\<lambda>_. dummy_term)"
1.210 +
1.211 +lemma (in term_syntax) term_of_num_code [code]:
1.212 + "term_of_num two k = (if k = 0 then termify Int.Pls
1.213 + else (if k mod two = 0
1.214 + then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
1.215 + else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
1.216 + by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
1.217 +
1.218 +lemma (in term_syntax) term_of_nat_code [code]:
1.219 + "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
1.220 + by (simp only: term_of_anything)
1.221 +
1.222 +lemma (in term_syntax) term_of_int_code [code]:
1.223 + "term_of (k::int) = (if k = 0 then termify (0 :: int)
1.224 + else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
1.225 + else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
1.226 + by (simp only: term_of_anything)
1.227 +
1.228 +lemma (in term_syntax) term_of_code_numeral_code [code]:
1.229 + "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
1.230 + by (simp only: term_of_anything)
1.231 +
1.232 +subsection {* Obfuscate *}
1.233 +
1.234 +print_translation {*
1.235 +let
1.236 + val term = Const ("<TERM>", dummyT);
1.237 + fun tr1' [_, _] = term;
1.238 + fun tr2' [] = term;
1.239 +in
1.240 + [(@{const_syntax Const}, tr1'),
1.241 + (@{const_syntax App}, tr1'),
1.242 + (@{const_syntax dummy_term}, tr2')]
1.243 +end
1.244 +*}
1.245 +
1.246 +hide const dummy_term App valapp
1.247 +hide (open) const Const termify valtermify term_of term_of_num
1.248 +
1.249 +
1.250 +subsection {* Evaluation setup *}
1.251 +
1.252 +ML {*
1.253 +signature EVAL =
1.254 +sig
1.255 + val eval_ref: (unit -> term) option ref
1.256 + val eval_term: theory -> term -> term
1.257 +end;
1.258 +
1.259 +structure Eval : EVAL =
1.260 +struct
1.261 +
1.262 +val eval_ref = ref (NONE : (unit -> term) option);
1.263 +
1.264 +fun eval_term thy t =
1.265 + Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
1.266 +
1.267 +end;
1.268 +*}
1.269 +
1.270 +setup {*
1.271 + Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
1.272 +*}
1.273 +
1.274 +end