src/HOL/Code_Eval.thy
changeset 32657 5f13912245ff
parent 32653 7feb35deb6f6
child 32658 82956a3f0e0b
child 32701 5059a733a4b8
     1.1 --- a/src/HOL/Code_Eval.thy	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,271 +0,0 @@
     1.4 -(*  Title:      HOL/Code_Eval.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_Eval
    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_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   1.135 -lemma [code, code del]:
   1.136 -  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   1.137 -
   1.138 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
   1.139 -    (let (n, m) = nibble_pair_of_char c
   1.140 -  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   1.141 -    (Code_Eval.term_of n)) (Code_Eval.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