improved evaluation mechanism

--- a/src/HOL/IsaMakefile	Wed Jan 02 15:14:02 2008 +0100
+++ b/src/HOL/IsaMakefile	Wed Jan 02 15:14:15 2008 +0100
@@ -228,7 +228,7 @@
   Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
   Library/Coinductive_List.thy Library/AssocList.thy \
   Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
-  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
+  Library/Eval.thy Library/Eval_Witness.thy \
   Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
   Library/Code_Integer.thy Library/Code_Message.thy \
   Library/Abstract_Rat.thy \

--- a/src/HOL/Library/Eval.thy	Wed Jan 02 15:14:02 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Wed Jan 02 15:14:15 2008 +0100
@@ -6,19 +6,80 @@
 header {* A simple term evaluation mechanism *}
 
 theory Eval
-imports ATP_Linkup Pure_term
+imports ATP_Linkup Code_Message
 begin
 
-subsection {* @{text typ_of} class *}
+subsection {* Type reflection *}
+
+subsubsection {* Definition *}
+
+types vname = message_string;
+types "class" = message_string;
+types sort = "class list"
+
+datatype "typ" =
+    Type message_string "typ list"
+  | TFree vname sort  
+
+abbreviation
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
+  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+
+locale (open) pure_term_syntax = -- {* FIXME drop this *}
+  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
+    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
+    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
+
+parse_translation {*
+let
+  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
+    | Type_tr ts = raise TERM ("Type_tr", ts);
+  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
+    | TFree_tr ts = raise TERM ("TFree_tr", ts);
+  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
+    | Fun_tr ts = raise TERM("Fun_tr", ts);
+in [
+  ("\\<^fixed>pure_term_Type", Type_tr),
+  ("\\<^fixed>pure_term_TFree", TFree_tr),
+  ("\\<^fixed>pure_term_Fun", Fun_tr)
+] end
+*}
+
+notation (output)
+  Type (infixl "{\<struct>}" 120)
+and
+  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
+and
+  Fun (infixr "\<rightarrow>" 114)
+
+ML {*
+structure Eval_Aux =
+struct
+
+val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
+
+fun mk_typ f (Type (tyco, tys)) =
+      @{term Type} $ Message_String.mk tyco
+        $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
+  | mk_typ f (TFree v) =
+      f v;
+
+end;
+*}
+
+
+subsubsection {* Class @{text typ_of} *}
 
 class typ_of =
   fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
 
 ML {*
-structure TypOf =
+structure Eval_Aux =
 struct
 
-fun mk ty =
+open Eval_Aux;
+
+fun mk_typ_of ty =
   Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
     $ Logic.mk_type ty;
 
@@ -27,11 +88,12 @@
 
 setup {*
 let
+  open Eval_Aux;
   fun define_typ_of ty lthy =
     let
       val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
         $ Free ("T", Term.itselfT ty);
-      val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
+      val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty;
       val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
     in lthy |> Specification.definition (NONE, (("", []), eq)) end;
   fun interpretator tyco thy =
@@ -81,16 +143,72 @@
 end
 
 
-subsection {* @{text term_of} class *}
+subsubsection {* Code generator setup *}
+
+lemma [code func]:
+  includes pure_term_syntax
+  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
+     \<and> list_all2 (op =) tys1 tys2"
+  by (auto simp add: list_all2_eq [symmetric])
+
+code_type "typ"
+  (SML "Term.typ")
+
+code_const Type and TFree
+  (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
+
+code_reserved SML Term
+
+
+
+subsection {* Term representation *}
+
+subsubsection {* Definition *}
+
+datatype "term" =
+    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
+  | Fix   vname "typ" (infix ":\<epsilon>" 112)
+  | App   "term" "term" (infixl "\<bullet>" 110)
+  | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
+  | Bnd   nat
+
+code_datatype Const App Fix
+
+abbreviation
+  Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
+  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
+abbreviation
+  Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
+  "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
+
+ML {*
+structure Eval_Aux =
+struct
+
+open Eval_Aux;
+
+fun mk_term f g (Const (c, ty)) =
+      @{term Const} $ Message_String.mk c $ g ty
+  | mk_term f g (t1 $ t2) =
+      @{term App} $ mk_term f g t1 $ mk_term f g t2
+  | mk_term f g (Free v) = f v;
+
+end;
+*}
+
+
+subsubsection {* Class @{text term_of} *}
 
 class term_of = typ_of +
   constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
   fixes term_of :: "'a \<Rightarrow> term"
 
 ML {*
-structure TermOf =
+structure Eval_Aux =
 struct
 
+open Eval_Aux;
+
 local
   fun term_term_of ty =
     Const (@{const_name term_of}, ty --> @{typ term});
@@ -102,9 +220,9 @@
       fun mk_eq c =
         let
           val lhs : term = term_term_of dty $ c;
-          val rhs : term = Pure_term.mk_term
+          val rhs : term = mk_term
             (fn (v, ty) => term_term_of ty $ Free (v, ty))
-            (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
+            (mk_typ (fn (v, sort) => mk_typ_of (TFree (v, sort)))) c
         in
           HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
         end;
@@ -118,6 +236,7 @@
 
 setup {*
 let
+  open Eval_Aux;
   fun thy_note ((name, atts), thms) =
     PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   fun thy_def ((name, atts), t) =
@@ -143,7 +262,7 @@
       val sorts = map (inter_sort o snd) vs_proto;
       val vs = map fst vs_proto ~~ sorts;
       val css = map (prep_dtyp thy vs) tycos;
-      val defs = map (TermOf.mk_terms_of_defs vs) css;
+      val defs = map (mk_terms_of_defs vs) css;
     in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
         andalso not (tycos = [@{type_name typ}])
       then SOME (sorts, defs)
@@ -212,12 +331,20 @@
 end
 
 
-text {* Adaption for @{typ message_string}s *}
+subsubsection {* Code generator setup *}
+
+lemmas [code func del] = term.recs term.cases term.size
+lemmas [code func del] = term_of_message_string.simps
+lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
 
-lemmas [code func del] = term_of_message_string.simps
+code_type "term"
+  (SML "Term.term")
+
+code_const Const and App and Fix
+  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
 
 
-subsection {* Evaluation infrastructure *}
+subsection {* Evaluation setup *}
 
 ML {*
 signature EVAL =
@@ -238,7 +365,7 @@
   CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
 
 fun eval_term thy =
-  TermOf.mk_term_of
+  Eval_Aux.mk_term_of
   #> CodePackage.eval_term thy (eval_invoke thy)
   #> Code.postprocess_term thy;
 

--- a/src/HOL/Library/Pure_term.thy	Wed Jan 02 15:14:02 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(*  Title:      HOL/Library/Pure_term.thy
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Partial reflection of the Pure term algebra in HOL *}
-
-theory Pure_term
-imports Code_Message
-begin
-
-subsection {* Definitions and syntax *}
-
-types vname = message_string;
-types "class" = message_string;
-types sort = "class list"
-
-datatype "typ" =
-    Type message_string "typ list"
-  | TFree vname sort  
-
-abbreviation
-  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
-  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
-
-locale (open) pure_term_syntax =
-  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
-    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
-    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
-
-parse_translation {*
-let
-  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
-    | Type_tr ts = raise TERM ("Type_tr", ts);
-  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
-    | TFree_tr ts = raise TERM ("TFree_tr", ts);
-  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
-    | Fun_tr ts = raise TERM("Fun_tr", ts);
-in [
-  ("\\<^fixed>pure_term_Type", Type_tr),
-  ("\\<^fixed>pure_term_TFree", TFree_tr),
-  ("\\<^fixed>pure_term_Fun", Fun_tr)
-] end
-*}
-
-notation (output)
-  Type (infixl "{\<struct>}" 120)
-and
-  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
-and
-  Fun (infixr "\<rightarrow>" 114)
-
-datatype "term" =
-    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
-  | Fix   vname "typ" (infix ":\<epsilon>" 112)
-  | App   "term" "term" (infixl "\<bullet>" 110)
-  | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
-  | Bnd   nat
-
-abbreviation
-  Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
-  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
-abbreviation
-  Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
-  "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
-
-
-subsection {* ML interface *}
-
-ML {*
-structure Pure_term =
-struct
-
-val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
-
-fun mk_typ f (Type (tyco, tys)) =
-      @{term Type} $ Message_String.mk tyco
-        $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
-  | mk_typ f (TFree v) =
-      f v;
-
-fun mk_term f g (Const (c, ty)) =
-      @{term Const} $ Message_String.mk c $ g ty
-  | mk_term f g (t1 $ t2) =
-      @{term App} $ mk_term f g t1 $ mk_term f g t2
-  | mk_term f g (Free v) = f v;
-
-end;
-*}
-
-
-subsection {* Code generator setup *}
-
-lemma [code func]:
-  includes pure_term_syntax
-  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
-     \<and> list_all2 (op =) tys1 tys2"
-  by (auto simp add: list_all2_eq [symmetric])
-
-code_datatype Const App Fix
-
-lemmas [code func del] = term.recs term.cases term.size
-lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
-
-code_type "typ" and "term"
-  (SML "Term.typ" and "Term.term")
-
-code_const Type and TFree
-  (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
-
-code_const Const and App and Fix
-  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
- 
-code_reserved SML Term
-
-end