Factored out ML into separate file
authorhaftmann
Mon Sep 20 15:10:21 2010 +0200 (2010-09-20)
changeset 39564acfd10e38e80
parent 39559 e7d4923b9b1c
child 39565 f4f87c6e2fad
Factored out ML into separate file
src/HOL/Code_Evaluation.thy
src/HOL/IsaMakefile
src/HOL/Tools/code_evaluation.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Sep 20 14:50:45 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Sep 20 15:10:21 2010 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory Code_Evaluation
     1.6  imports Plain Typerep Code_Numeral
     1.7 +uses ("Tools/code_evaluation.ML")
     1.8  begin
     1.9  
    1.10  subsection {* Term representation *}
    1.11 @@ -37,171 +38,6 @@
    1.12    by (simp only: valapp_def fst_conv snd_conv)
    1.13  
    1.14  
    1.15 -subsubsection {* @{text term_of} instances *}
    1.16 -
    1.17 -instantiation "fun" :: (typerep, typerep) term_of
    1.18 -begin
    1.19 -
    1.20 -definition
    1.21 -  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    1.22 -     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    1.23 -
    1.24 -instance ..
    1.25 -
    1.26 -end
    1.27 -
    1.28 -setup {*
    1.29 -let
    1.30 -  fun add_term_of tyco raw_vs thy =
    1.31 -    let
    1.32 -      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    1.33 -      val ty = Type (tyco, map TFree vs);
    1.34 -      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    1.35 -        $ Free ("x", ty);
    1.36 -      val rhs = @{term "undefined \<Colon> term"};
    1.37 -      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.38 -      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    1.39 -        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    1.40 -    in
    1.41 -      thy
    1.42 -      |> Class.instantiation ([tyco], vs, @{sort term_of})
    1.43 -      |> `(fn lthy => Syntax.check_term lthy eq)
    1.44 -      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    1.45 -      |> snd
    1.46 -      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.47 -    end;
    1.48 -  fun ensure_term_of (tyco, (raw_vs, _)) thy =
    1.49 -    let
    1.50 -      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    1.51 -        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    1.52 -    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    1.53 -in
    1.54 -  Code.datatype_interpretation ensure_term_of
    1.55 -  #> Code.abstype_interpretation ensure_term_of
    1.56 -end
    1.57 -*}
    1.58 -
    1.59 -setup {*
    1.60 -let
    1.61 -  fun mk_term_of_eq thy ty vs tyco (c, tys) =
    1.62 -    let
    1.63 -      val t = list_comb (Const (c, tys ---> ty),
    1.64 -        map Free (Name.names Name.context "a" tys));
    1.65 -      val (arg, rhs) =
    1.66 -        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    1.67 -          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    1.68 -      val cty = Thm.ctyp_of thy ty;
    1.69 -    in
    1.70 -      @{thm term_of_anything}
    1.71 -      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    1.72 -      |> Thm.varifyT_global
    1.73 -    end;
    1.74 -  fun add_term_of_code tyco raw_vs raw_cs thy =
    1.75 -    let
    1.76 -      val algebra = Sign.classes_of thy;
    1.77 -      val vs = map (fn (v, sort) =>
    1.78 -        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    1.79 -      val ty = Type (tyco, map TFree vs);
    1.80 -      val cs = (map o apsnd o map o map_atyps)
    1.81 -        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.82 -      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.83 -      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
    1.84 -   in
    1.85 -      thy
    1.86 -      |> Code.del_eqns const
    1.87 -      |> fold Code.add_eqn eqs
    1.88 -    end;
    1.89 -  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    1.90 -    let
    1.91 -      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.92 -    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    1.93 -in
    1.94 -  Code.datatype_interpretation ensure_term_of_code
    1.95 -end
    1.96 -*}
    1.97 -
    1.98 -setup {*
    1.99 -let
   1.100 -  fun mk_term_of_eq thy ty vs tyco abs ty_rep proj =
   1.101 -    let
   1.102 -      val arg = Var (("x", 0), ty);
   1.103 -      val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
   1.104 -        (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
   1.105 -        |> Thm.cterm_of thy;
   1.106 -      val cty = Thm.ctyp_of thy ty;
   1.107 -    in
   1.108 -      @{thm term_of_anything}
   1.109 -      |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
   1.110 -      |> Thm.varifyT_global
   1.111 -    end;
   1.112 -  fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
   1.113 -    let
   1.114 -      val algebra = Sign.classes_of thy;
   1.115 -      val vs = map (fn (v, sort) =>
   1.116 -        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   1.117 -      val ty = Type (tyco, map TFree vs);
   1.118 -      val ty_rep = map_atyps
   1.119 -        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   1.120 -      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   1.121 -      val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj;
   1.122 -   in
   1.123 -      thy
   1.124 -      |> Code.del_eqns const
   1.125 -      |> Code.add_eqn eq
   1.126 -    end;
   1.127 -  fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
   1.128 -    let
   1.129 -      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   1.130 -    in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end;
   1.131 -in
   1.132 -  Code.abstype_interpretation ensure_term_of_code
   1.133 -end
   1.134 -*}
   1.135 -
   1.136 -
   1.137 -instantiation String.literal :: term_of
   1.138 -begin
   1.139 -
   1.140 -definition
   1.141 -  "term_of s = App (Const (STR ''STR'')
   1.142 -    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
   1.143 -      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
   1.144 -
   1.145 -instance ..
   1.146 -
   1.147 -end
   1.148 -
   1.149 -subsubsection {* Code generator setup *}
   1.150 -
   1.151 -lemmas [code del] = term.recs term.cases term.size
   1.152 -lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
   1.153 -
   1.154 -lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   1.155 -lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   1.156 -lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   1.157 -lemma [code, code del]:
   1.158 -  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   1.159 -lemma [code, code del]:
   1.160 -  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   1.161 -
   1.162 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
   1.163 -    (let (n, m) = nibble_pair_of_char c
   1.164 -  in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   1.165 -    (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
   1.166 -  by (subst term_of_anything) rule 
   1.167 -
   1.168 -code_type "term"
   1.169 -  (Eval "Term.term")
   1.170 -
   1.171 -code_const Const and App
   1.172 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   1.173 -
   1.174 -code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   1.175 -  (Eval "HOLogic.mk'_literal")
   1.176 -
   1.177 -code_reserved Eval HOLogic
   1.178 -
   1.179 -
   1.180  subsubsection {* Syntax *}
   1.181  
   1.182  definition termify :: "'a \<Rightarrow> term" where
   1.183 @@ -210,34 +46,6 @@
   1.184  abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   1.185    "valtermify x \<equiv> (x, \<lambda>u. termify x)"
   1.186  
   1.187 -setup {*
   1.188 -let
   1.189 -  fun map_default f xs =
   1.190 -    let val ys = map f xs
   1.191 -    in if exists is_some ys
   1.192 -      then SOME (map2 the_default xs ys)
   1.193 -      else NONE
   1.194 -    end;
   1.195 -  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   1.196 -        if not (Term.has_abs t)
   1.197 -        then if fold_aterms (fn Const _ => I | _ => K false) t true
   1.198 -          then SOME (HOLogic.reflect_term t)
   1.199 -          else error "Cannot termify expression containing variables"
   1.200 -        else error "Cannot termify expression containing abstraction"
   1.201 -    | subst_termify_app (t, ts) = case map_default subst_termify ts
   1.202 -       of SOME ts' => SOME (list_comb (t, ts'))
   1.203 -        | NONE => NONE
   1.204 -  and subst_termify (Abs (v, T, t)) = (case subst_termify t
   1.205 -       of SOME t' => SOME (Abs (v, T, t'))
   1.206 -        | NONE => NONE)
   1.207 -    | subst_termify t = subst_termify_app (strip_comb t) 
   1.208 -  fun check_termify ts ctxt = map_default subst_termify ts
   1.209 -    |> Option.map (rpair ctxt)
   1.210 -in
   1.211 -  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   1.212 -end;
   1.213 -*}
   1.214 -
   1.215  locale term_syntax
   1.216  begin
   1.217  
   1.218 @@ -252,7 +60,75 @@
   1.219    and valapp (infixl "{\<cdot>}" 70)
   1.220  
   1.221  
   1.222 -subsection {* Numeric types *}
   1.223 +subsection {* Tools setup and evaluation *}
   1.224 +
   1.225 +use "Tools/code_evaluation.ML"
   1.226 +
   1.227 +code_reserved Eval Code_Evaluation
   1.228 +
   1.229 +setup {* Code_Evaluation.setup *}
   1.230 +
   1.231 +
   1.232 +subsection {* @{text term_of} instances *}
   1.233 +
   1.234 +instantiation "fun" :: (typerep, typerep) term_of
   1.235 +begin
   1.236 +
   1.237 +definition
   1.238 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
   1.239 +     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
   1.240 +
   1.241 +instance ..
   1.242 +
   1.243 +end
   1.244 +
   1.245 +instantiation String.literal :: term_of
   1.246 +begin
   1.247 +
   1.248 +definition
   1.249 +  "term_of s = App (Const (STR ''STR'')
   1.250 +    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
   1.251 +      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
   1.252 +
   1.253 +instance ..
   1.254 +
   1.255 +end
   1.256 +
   1.257 +
   1.258 +subsubsection {* Code generator setup *}
   1.259 +
   1.260 +lemmas [code del] = term.recs term.cases term.size
   1.261 +lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
   1.262 +
   1.263 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   1.264 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   1.265 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   1.266 +lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
   1.267 +  = Code_Evaluation.term_of" ..
   1.268 +lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
   1.269 +  = Code_Evaluation.term_of" ..
   1.270 +
   1.271 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
   1.272 +  "Code_Evaluation.term_of c =
   1.273 +    (let (n, m) = nibble_pair_of_char c
   1.274 +  in Code_Evaluation.App (Code_Evaluation.App
   1.275 +    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   1.276 +      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
   1.277 +  by (subst term_of_anything) rule 
   1.278 +
   1.279 +code_type "term"
   1.280 +  (Eval "Term.term")
   1.281 +
   1.282 +code_const Const and App
   1.283 +  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   1.284 +
   1.285 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   1.286 +  (Eval "HOLogic.mk'_literal")
   1.287 +
   1.288 +code_reserved Eval HOLogic
   1.289 +
   1.290 +
   1.291 +subsubsection {* Numeric types *}
   1.292  
   1.293  definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   1.294    "term_of_num two = (\<lambda>_. dummy_term)"
   1.295 @@ -279,7 +155,7 @@
   1.296    by (simp only: term_of_anything)
   1.297  
   1.298  
   1.299 -subsection {* Obfuscate *}
   1.300 +subsubsection {* Obfuscation *}
   1.301  
   1.302  print_translation {*
   1.303  let
   1.304 @@ -294,36 +170,7 @@
   1.305  *}
   1.306  
   1.307  
   1.308 -subsection {* Evaluation setup *}
   1.309 -
   1.310 -ML {*
   1.311 -signature CODE_EVALUATION =
   1.312 -sig
   1.313 -  val eval_term: theory -> term -> term
   1.314 -  val put_term: (unit -> term) -> Proof.context -> Proof.context
   1.315 -  val tracing: string -> 'a -> 'a
   1.316 -end;
   1.317 -
   1.318 -structure Code_Evaluation : CODE_EVALUATION =
   1.319 -struct
   1.320 -
   1.321 -structure Evaluation = Proof_Data (
   1.322 -  type T = unit -> term
   1.323 -  fun init _ () = error "Evaluation"
   1.324 -);
   1.325 -val put_term = Evaluation.put;
   1.326 -
   1.327 -fun tracing s x = (Output.tracing s; x);
   1.328 -
   1.329 -fun eval_term thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
   1.330 -  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
   1.331 -
   1.332 -end
   1.333 -*}
   1.334 -
   1.335 -setup {*
   1.336 -  Value.add_evaluator ("code", Code_Evaluation.eval_term o ProofContext.theory_of)
   1.337 -*}
   1.338 +subsection {* Diagnostic *}
   1.339  
   1.340  definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.341    [code del]: "tracing s x = x"
   1.342 @@ -331,7 +178,6 @@
   1.343  code_const "tracing :: String.literal => 'a => 'a"
   1.344    (Eval "Code'_Evaluation.tracing")
   1.345  
   1.346 -code_reserved Eval Code_Evaluation
   1.347  
   1.348  hide_const dummy_term App valapp
   1.349  hide_const (open) Const termify valtermify term_of term_of_num tracing
     2.1 --- a/src/HOL/IsaMakefile	Mon Sep 20 14:50:45 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Sep 20 15:10:21 2010 +0200
     2.3 @@ -271,6 +271,7 @@
     2.4    Tools/ATP/atp_proof.ML \
     2.5    Tools/ATP/atp_systems.ML \
     2.6    Tools/choice_specification.ML \
     2.7 +  Tools/code_evaluation.ML \
     2.8    Tools/Datatype/datatype_selectors.ML \
     2.9    Tools/int_arith.ML \
    2.10    Tools/groebner.ML \
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 15:10:21 2010 +0200
     3.3 @@ -0,0 +1,174 @@
     3.4 +(*  Title:      HOL/Tools/code_evaluation.ML
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +
     3.7 +Evaluation and reconstruction of terms in ML.
     3.8 +*)
     3.9 +
    3.10 +signature CODE_EVALUATION =
    3.11 +sig
    3.12 +  val dynamic_value_strict: theory -> term -> term
    3.13 +  val put_term: (unit -> term) -> Proof.context -> Proof.context
    3.14 +  val tracing: string -> 'a -> 'a
    3.15 +  val setup: theory -> theory
    3.16 +end;
    3.17 +
    3.18 +structure Code_Evaluation : CODE_EVALUATION =
    3.19 +struct
    3.20 +
    3.21 +(** term_of instances **)
    3.22 +
    3.23 +(* formal definition *)
    3.24 +
    3.25 +fun add_term_of tyco raw_vs thy =
    3.26 +  let
    3.27 +    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    3.28 +    val ty = Type (tyco, map TFree vs);
    3.29 +    val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    3.30 +      $ Free ("x", ty);
    3.31 +    val rhs = @{term "undefined :: term"};
    3.32 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    3.33 +    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    3.34 +      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    3.35 +  in
    3.36 +    thy
    3.37 +    |> Class.instantiation ([tyco], vs, @{sort term_of})
    3.38 +    |> `(fn lthy => Syntax.check_term lthy eq)
    3.39 +    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    3.40 +    |> snd
    3.41 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    3.42 +  end;
    3.43 +
    3.44 +fun ensure_term_of (tyco, (raw_vs, _)) thy =
    3.45 +  let
    3.46 +    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    3.47 +      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    3.48 +  in if need_inst then add_term_of tyco raw_vs thy else thy end;
    3.49 +
    3.50 +
    3.51 +(* code equations for datatypes *)
    3.52 +
    3.53 +fun mk_term_of_eq thy ty vs tyco (c, tys) =
    3.54 +  let
    3.55 +    val t = list_comb (Const (c, tys ---> ty),
    3.56 +      map Free (Name.names Name.context "a" tys));
    3.57 +    val (arg, rhs) =
    3.58 +      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    3.59 +        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    3.60 +    val cty = Thm.ctyp_of thy ty;
    3.61 +  in
    3.62 +    @{thm term_of_anything}
    3.63 +    |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    3.64 +    |> Thm.varifyT_global
    3.65 +  end;
    3.66 +
    3.67 +fun add_term_of_code tyco raw_vs raw_cs thy =
    3.68 +  let
    3.69 +    val algebra = Sign.classes_of thy;
    3.70 +    val vs = map (fn (v, sort) =>
    3.71 +      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    3.72 +    val ty = Type (tyco, map TFree vs);
    3.73 +    val cs = (map o apsnd o map o map_atyps)
    3.74 +      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    3.75 +    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    3.76 +    val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
    3.77 + in
    3.78 +    thy
    3.79 +    |> Code.del_eqns const
    3.80 +    |> fold Code.add_eqn eqs
    3.81 +  end;
    3.82 +
    3.83 +fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    3.84 +  let
    3.85 +    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    3.86 +  in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    3.87 +
    3.88 +
    3.89 +(* code equations for abstypes *)
    3.90 +
    3.91 +fun mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj =
    3.92 +  let
    3.93 +    val arg = Var (("x", 0), ty);
    3.94 +    val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
    3.95 +      (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
    3.96 +      |> Thm.cterm_of thy;
    3.97 +    val cty = Thm.ctyp_of thy ty;
    3.98 +  in
    3.99 +    @{thm term_of_anything}
   3.100 +    |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
   3.101 +    |> Thm.varifyT_global
   3.102 +  end;
   3.103 +
   3.104 +fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
   3.105 +  let
   3.106 +    val algebra = Sign.classes_of thy;
   3.107 +    val vs = map (fn (v, sort) =>
   3.108 +      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   3.109 +    val ty = Type (tyco, map TFree vs);
   3.110 +    val ty_rep = map_atyps
   3.111 +      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   3.112 +    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   3.113 +    val eq = mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj;
   3.114 + in
   3.115 +    thy
   3.116 +    |> Code.del_eqns const
   3.117 +    |> Code.add_eqn eq
   3.118 +  end;
   3.119 +
   3.120 +fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
   3.121 +  let
   3.122 +    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   3.123 +  in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
   3.124 +
   3.125 +
   3.126 +(** termifying syntax **)
   3.127 +
   3.128 +fun map_default f xs =
   3.129 +  let val ys = map f xs
   3.130 +  in if exists is_some ys
   3.131 +    then SOME (map2 the_default xs ys)
   3.132 +    else NONE
   3.133 +  end;
   3.134 +
   3.135 +fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   3.136 +      if not (Term.has_abs t)
   3.137 +      then if fold_aterms (fn Const _ => I | _ => K false) t true
   3.138 +        then SOME (HOLogic.reflect_term t)
   3.139 +        else error "Cannot termify expression containing variables"
   3.140 +      else error "Cannot termify expression containing abstraction"
   3.141 +  | subst_termify_app (t, ts) = case map_default subst_termify ts
   3.142 +     of SOME ts' => SOME (list_comb (t, ts'))
   3.143 +      | NONE => NONE
   3.144 +and subst_termify (Abs (v, T, t)) = (case subst_termify t
   3.145 +     of SOME t' => SOME (Abs (v, T, t'))
   3.146 +      | NONE => NONE)
   3.147 +  | subst_termify t = subst_termify_app (strip_comb t) 
   3.148 +
   3.149 +fun check_termify ts ctxt = map_default subst_termify ts
   3.150 +  |> Option.map (rpair ctxt)
   3.151 +
   3.152 +
   3.153 +(** evaluation **)
   3.154 +
   3.155 +structure Evaluation = Proof_Data (
   3.156 +  type T = unit -> term
   3.157 +  fun init _ () = error "Evaluation"
   3.158 +);
   3.159 +val put_term = Evaluation.put;
   3.160 +
   3.161 +fun tracing s x = (Output.tracing s; x);
   3.162 +
   3.163 +fun dynamic_value_strict thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
   3.164 +  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
   3.165 +
   3.166 +
   3.167 +(** setup **)
   3.168 +
   3.169 +val setup =
   3.170 +  Code.datatype_interpretation ensure_term_of
   3.171 +  #> Code.abstype_interpretation ensure_term_of
   3.172 +  #> Code.datatype_interpretation ensure_term_of_code
   3.173 +  #> Code.abstype_interpretation ensure_abs_term_of_code
   3.174 +  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   3.175 +  #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
   3.176 +
   3.177 +end;