# HG changeset patch
# User haftmann
# Date 1284988221 -7200
# Node ID acfd10e38e801eccf25a4fccc522b6ed66dd7d18
# Parent  e7d4923b9b1c9f47558eb3e25d34d4bde6c5a363
Factored out ML into separate file

diff -r e7d4923b9b1c -r acfd10e38e80 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Sep 20 14:50:45 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Sep 20 15:10:21 2010 +0200
@@ -6,6 +6,7 @@
 
 theory Code_Evaluation
 imports Plain Typerep Code_Numeral
+uses ("Tools/code_evaluation.ML")
 begin
 
 subsection {* Term representation *}
@@ -37,171 +38,6 @@
   by (simp only: valapp_def fst_conv snd_conv)
 
 
-subsubsection {* @{text term_of} instances *}
-
-instantiation "fun" :: (typerep, typerep) term_of
-begin
-
-definition
-  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
-     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
-
-instance ..
-
-end
-
-setup {*
-let
-  fun add_term_of tyco raw_vs thy =
-    let
-      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
-        $ Free ("x", ty);
-      val rhs = @{term "undefined \<Colon> term"};
-      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
-      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
-        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
-    in
-      thy
-      |> Class.instantiation ([tyco], vs, @{sort term_of})
-      |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
-      |> snd
-      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-    end;
-  fun ensure_term_of (tyco, (raw_vs, _)) thy =
-    let
-      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
-        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
-    in if need_inst then add_term_of tyco raw_vs thy else thy end;
-in
-  Code.datatype_interpretation ensure_term_of
-  #> Code.abstype_interpretation ensure_term_of
-end
-*}
-
-setup {*
-let
-  fun mk_term_of_eq thy ty vs tyco (c, tys) =
-    let
-      val t = list_comb (Const (c, tys ---> ty),
-        map Free (Name.names Name.context "a" tys));
-      val (arg, rhs) =
-        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
-          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
-      val cty = Thm.ctyp_of thy ty;
-    in
-      @{thm term_of_anything}
-      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
-      |> Thm.varifyT_global
-    end;
-  fun add_term_of_code tyco raw_vs raw_cs thy =
-    let
-      val algebra = Sign.classes_of thy;
-      val vs = map (fn (v, sort) =>
-        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val cs = (map o apsnd o map o map_atyps)
-        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
-      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
-      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
-   in
-      thy
-      |> Code.del_eqns const
-      |> fold Code.add_eqn eqs
-    end;
-  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
-    let
-      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
-in
-  Code.datatype_interpretation ensure_term_of_code
-end
-*}
-
-setup {*
-let
-  fun mk_term_of_eq thy ty vs tyco abs ty_rep proj =
-    let
-      val arg = Var (("x", 0), ty);
-      val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
-        (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
-        |> Thm.cterm_of thy;
-      val cty = Thm.ctyp_of thy ty;
-    in
-      @{thm term_of_anything}
-      |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
-      |> Thm.varifyT_global
-    end;
-  fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
-    let
-      val algebra = Sign.classes_of thy;
-      val vs = map (fn (v, sort) =>
-        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
-      val ty = Type (tyco, map TFree vs);
-      val ty_rep = map_atyps
-        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
-      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
-      val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj;
-   in
-      thy
-      |> Code.del_eqns const
-      |> Code.add_eqn eq
-    end;
-  fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
-    let
-      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-    in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end;
-in
-  Code.abstype_interpretation ensure_term_of_code
-end
-*}
-
-
-instantiation String.literal :: term_of
-begin
-
-definition
-  "term_of s = App (Const (STR ''STR'')
-    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
-      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
-
-instance ..
-
-end
-
-subsubsection {* Code generator setup *}
-
-lemmas [code del] = term.recs term.cases term.size
-lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
-
-lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
-lemma [code, code del]:
-  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
-lemma [code, code del]:
-  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
-
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
-    (let (n, m) = nibble_pair_of_char c
-  in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
-    (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
-  by (subst term_of_anything) rule 
-
-code_type "term"
-  (Eval "Term.term")
-
-code_const Const and App
-  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
-
-code_const "term_of \<Colon> String.literal \<Rightarrow> term"
-  (Eval "HOLogic.mk'_literal")
-
-code_reserved Eval HOLogic
-
-
 subsubsection {* Syntax *}
 
 definition termify :: "'a \<Rightarrow> term" where
@@ -210,34 +46,6 @@
 abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   "valtermify x \<equiv> (x, \<lambda>u. termify x)"
 
-setup {*
-let
-  fun map_default f xs =
-    let val ys = map f xs
-    in if exists is_some ys
-      then SOME (map2 the_default xs ys)
-      else NONE
-    end;
-  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
-        if not (Term.has_abs t)
-        then if fold_aterms (fn Const _ => I | _ => K false) t true
-          then SOME (HOLogic.reflect_term t)
-          else error "Cannot termify expression containing variables"
-        else error "Cannot termify expression containing abstraction"
-    | subst_termify_app (t, ts) = case map_default subst_termify ts
-       of SOME ts' => SOME (list_comb (t, ts'))
-        | NONE => NONE
-  and subst_termify (Abs (v, T, t)) = (case subst_termify t
-       of SOME t' => SOME (Abs (v, T, t'))
-        | NONE => NONE)
-    | subst_termify t = subst_termify_app (strip_comb t) 
-  fun check_termify ts ctxt = map_default subst_termify ts
-    |> Option.map (rpair ctxt)
-in
-  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
-end;
-*}
-
 locale term_syntax
 begin
 
@@ -252,7 +60,75 @@
   and valapp (infixl "{\<cdot>}" 70)
 
 
-subsection {* Numeric types *}
+subsection {* Tools setup and evaluation *}
+
+use "Tools/code_evaluation.ML"
+
+code_reserved Eval Code_Evaluation
+
+setup {* Code_Evaluation.setup *}
+
+
+subsection {* @{text term_of} instances *}
+
+instantiation "fun" :: (typerep, typerep) term_of
+begin
+
+definition
+  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
+     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
+
+instance ..
+
+end
+
+instantiation String.literal :: term_of
+begin
+
+definition
+  "term_of s = App (Const (STR ''STR'')
+    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
+      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
+
+instance ..
+
+end
+
+
+subsubsection {* Code generator setup *}
+
+lemmas [code del] = term.recs term.cases term.size
+lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
+
+lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
+  = Code_Evaluation.term_of" ..
+lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
+  = Code_Evaluation.term_of" ..
+
+lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
+  "Code_Evaluation.term_of c =
+    (let (n, m) = nibble_pair_of_char c
+  in Code_Evaluation.App (Code_Evaluation.App
+    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
+  by (subst term_of_anything) rule 
+
+code_type "term"
+  (Eval "Term.term")
+
+code_const Const and App
+  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
+
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
+  (Eval "HOLogic.mk'_literal")
+
+code_reserved Eval HOLogic
+
+
+subsubsection {* Numeric types *}
 
 definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   "term_of_num two = (\<lambda>_. dummy_term)"
@@ -279,7 +155,7 @@
   by (simp only: term_of_anything)
 
 
-subsection {* Obfuscate *}
+subsubsection {* Obfuscation *}
 
 print_translation {*
 let
@@ -294,36 +170,7 @@
 *}
 
 
-subsection {* Evaluation setup *}
-
-ML {*
-signature CODE_EVALUATION =
-sig
-  val eval_term: theory -> term -> term
-  val put_term: (unit -> term) -> Proof.context -> Proof.context
-  val tracing: string -> 'a -> 'a
-end;
-
-structure Code_Evaluation : CODE_EVALUATION =
-struct
-
-structure Evaluation = Proof_Data (
-  type T = unit -> term
-  fun init _ () = error "Evaluation"
-);
-val put_term = Evaluation.put;
-
-fun tracing s x = (Output.tracing s; x);
-
-fun eval_term thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
-  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
-
-end
-*}
-
-setup {*
-  Value.add_evaluator ("code", Code_Evaluation.eval_term o ProofContext.theory_of)
-*}
+subsection {* Diagnostic *}
 
 definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
   [code del]: "tracing s x = x"
@@ -331,7 +178,6 @@
 code_const "tracing :: String.literal => 'a => 'a"
   (Eval "Code'_Evaluation.tracing")
 
-code_reserved Eval Code_Evaluation
 
 hide_const dummy_term App valapp
 hide_const (open) Const termify valtermify term_of term_of_num tracing
diff -r e7d4923b9b1c -r acfd10e38e80 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 20 14:50:45 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 20 15:10:21 2010 +0200
@@ -271,6 +271,7 @@
   Tools/ATP/atp_proof.ML \
   Tools/ATP/atp_systems.ML \
   Tools/choice_specification.ML \
+  Tools/code_evaluation.ML \
   Tools/Datatype/datatype_selectors.ML \
   Tools/int_arith.ML \
   Tools/groebner.ML \
diff -r e7d4923b9b1c -r acfd10e38e80 src/HOL/Tools/code_evaluation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 15:10:21 2010 +0200
@@ -0,0 +1,174 @@
+(*  Title:      HOL/Tools/code_evaluation.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Evaluation and reconstruction of terms in ML.
+*)
+
+signature CODE_EVALUATION =
+sig
+  val dynamic_value_strict: theory -> term -> term
+  val put_term: (unit -> term) -> Proof.context -> Proof.context
+  val tracing: string -> 'a -> 'a
+  val setup: theory -> theory
+end;
+
+structure Code_Evaluation : CODE_EVALUATION =
+struct
+
+(** term_of instances **)
+
+(* formal definition *)
+
+fun add_term_of tyco raw_vs thy =
+  let
+    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+    val ty = Type (tyco, map TFree vs);
+    val lhs = Const (@{const_name term_of}, ty --> @{typ term})
+      $ Free ("x", ty);
+    val rhs = @{term "undefined :: term"};
+    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
+      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
+  in
+    thy
+    |> Class.instantiation ([tyco], vs, @{sort term_of})
+    |> `(fn lthy => Syntax.check_term lthy eq)
+    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
+    |> snd
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end;
+
+fun ensure_term_of (tyco, (raw_vs, _)) thy =
+  let
+    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
+      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+  in if need_inst then add_term_of tyco raw_vs thy else thy end;
+
+
+(* code equations for datatypes *)
+
+fun mk_term_of_eq thy ty vs tyco (c, tys) =
+  let
+    val t = list_comb (Const (c, tys ---> ty),
+      map Free (Name.names Name.context "a" tys));
+    val (arg, rhs) =
+      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+    val cty = Thm.ctyp_of thy ty;
+  in
+    @{thm term_of_anything}
+    |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
+    |> Thm.varifyT_global
+  end;
+
+fun add_term_of_code tyco raw_vs raw_cs thy =
+  let
+    val algebra = Sign.classes_of thy;
+    val vs = map (fn (v, sort) =>
+      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+    val ty = Type (tyco, map TFree vs);
+    val cs = (map o apsnd o map o map_atyps)
+      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
+    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+    val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
+ in
+    thy
+    |> Code.del_eqns const
+    |> fold Code.add_eqn eqs
+  end;
+
+fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
+  let
+    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+  in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
+
+
+(* code equations for abstypes *)
+
+fun mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj =
+  let
+    val arg = Var (("x", 0), ty);
+    val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
+      (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
+      |> Thm.cterm_of thy;
+    val cty = Thm.ctyp_of thy ty;
+  in
+    @{thm term_of_anything}
+    |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
+    |> Thm.varifyT_global
+  end;
+
+fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
+  let
+    val algebra = Sign.classes_of thy;
+    val vs = map (fn (v, sort) =>
+      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+    val ty = Type (tyco, map TFree vs);
+    val ty_rep = map_atyps
+      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
+    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+    val eq = mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj;
+ in
+    thy
+    |> Code.del_eqns const
+    |> Code.add_eqn eq
+  end;
+
+fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
+  let
+    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+  in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
+
+
+(** termifying syntax **)
+
+fun map_default f xs =
+  let val ys = map f xs
+  in if exists is_some ys
+    then SOME (map2 the_default xs ys)
+    else NONE
+  end;
+
+fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
+      if not (Term.has_abs t)
+      then if fold_aterms (fn Const _ => I | _ => K false) t true
+        then SOME (HOLogic.reflect_term t)
+        else error "Cannot termify expression containing variables"
+      else error "Cannot termify expression containing abstraction"
+  | subst_termify_app (t, ts) = case map_default subst_termify ts
+     of SOME ts' => SOME (list_comb (t, ts'))
+      | NONE => NONE
+and subst_termify (Abs (v, T, t)) = (case subst_termify t
+     of SOME t' => SOME (Abs (v, T, t'))
+      | NONE => NONE)
+  | subst_termify t = subst_termify_app (strip_comb t) 
+
+fun check_termify ts ctxt = map_default subst_termify ts
+  |> Option.map (rpair ctxt)
+
+
+(** evaluation **)
+
+structure Evaluation = Proof_Data (
+  type T = unit -> term
+  fun init _ () = error "Evaluation"
+);
+val put_term = Evaluation.put;
+
+fun tracing s x = (Output.tracing s; x);
+
+fun dynamic_value_strict thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
+  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
+
+
+(** setup **)
+
+val setup =
+  Code.datatype_interpretation ensure_term_of
+  #> Code.abstype_interpretation ensure_term_of
+  #> Code.datatype_interpretation ensure_term_of_code
+  #> Code.abstype_interpretation ensure_abs_term_of_code
+  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+  #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
+
+end;