improved evaluation mechanism
authorhaftmann
Wed Jan 02 15:14:15 2008 +0100 (2008-01-02)
changeset 25763474f8ba9dfa9
parent 25762 c03e9d04b3e4
child 25764 878c37886eed
improved evaluation mechanism
src/HOL/IsaMakefile
src/HOL/Library/Eval.thy
src/HOL/Library/Pure_term.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Jan 02 15:14:02 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jan 02 15:14:15 2008 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4    Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
     1.5    Library/Coinductive_List.thy Library/AssocList.thy \
     1.6    Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
     1.7 -  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
     1.8 +  Library/Eval.thy Library/Eval_Witness.thy \
     1.9    Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
    1.10    Library/Code_Integer.thy Library/Code_Message.thy \
    1.11    Library/Abstract_Rat.thy \
     2.1 --- a/src/HOL/Library/Eval.thy	Wed Jan 02 15:14:02 2008 +0100
     2.2 +++ b/src/HOL/Library/Eval.thy	Wed Jan 02 15:14:15 2008 +0100
     2.3 @@ -6,19 +6,80 @@
     2.4  header {* A simple term evaluation mechanism *}
     2.5  
     2.6  theory Eval
     2.7 -imports ATP_Linkup Pure_term
     2.8 +imports ATP_Linkup Code_Message
     2.9  begin
    2.10  
    2.11 -subsection {* @{text typ_of} class *}
    2.12 +subsection {* Type reflection *}
    2.13 +
    2.14 +subsubsection {* Definition *}
    2.15 +
    2.16 +types vname = message_string;
    2.17 +types "class" = message_string;
    2.18 +types sort = "class list"
    2.19 +
    2.20 +datatype "typ" =
    2.21 +    Type message_string "typ list"
    2.22 +  | TFree vname sort  
    2.23 +
    2.24 +abbreviation
    2.25 +  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
    2.26 +  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
    2.27 +
    2.28 +locale (open) pure_term_syntax = -- {* FIXME drop this *}
    2.29 +  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
    2.30 +    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
    2.31 +    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
    2.32 +
    2.33 +parse_translation {*
    2.34 +let
    2.35 +  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
    2.36 +    | Type_tr ts = raise TERM ("Type_tr", ts);
    2.37 +  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
    2.38 +    | TFree_tr ts = raise TERM ("TFree_tr", ts);
    2.39 +  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
    2.40 +    | Fun_tr ts = raise TERM("Fun_tr", ts);
    2.41 +in [
    2.42 +  ("\\<^fixed>pure_term_Type", Type_tr),
    2.43 +  ("\\<^fixed>pure_term_TFree", TFree_tr),
    2.44 +  ("\\<^fixed>pure_term_Fun", Fun_tr)
    2.45 +] end
    2.46 +*}
    2.47 +
    2.48 +notation (output)
    2.49 +  Type (infixl "{\<struct>}" 120)
    2.50 +and
    2.51 +  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
    2.52 +and
    2.53 +  Fun (infixr "\<rightarrow>" 114)
    2.54 +
    2.55 +ML {*
    2.56 +structure Eval_Aux =
    2.57 +struct
    2.58 +
    2.59 +val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
    2.60 +
    2.61 +fun mk_typ f (Type (tyco, tys)) =
    2.62 +      @{term Type} $ Message_String.mk tyco
    2.63 +        $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
    2.64 +  | mk_typ f (TFree v) =
    2.65 +      f v;
    2.66 +
    2.67 +end;
    2.68 +*}
    2.69 +
    2.70 +
    2.71 +subsubsection {* Class @{text typ_of} *}
    2.72  
    2.73  class typ_of =
    2.74    fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
    2.75  
    2.76  ML {*
    2.77 -structure TypOf =
    2.78 +structure Eval_Aux =
    2.79  struct
    2.80  
    2.81 -fun mk ty =
    2.82 +open Eval_Aux;
    2.83 +
    2.84 +fun mk_typ_of ty =
    2.85    Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    2.86      $ Logic.mk_type ty;
    2.87  
    2.88 @@ -27,11 +88,12 @@
    2.89  
    2.90  setup {*
    2.91  let
    2.92 +  open Eval_Aux;
    2.93    fun define_typ_of ty lthy =
    2.94      let
    2.95        val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    2.96          $ Free ("T", Term.itselfT ty);
    2.97 -      val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
    2.98 +      val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty;
    2.99        val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   2.100      in lthy |> Specification.definition (NONE, (("", []), eq)) end;
   2.101    fun interpretator tyco thy =
   2.102 @@ -81,16 +143,72 @@
   2.103  end
   2.104  
   2.105  
   2.106 -subsection {* @{text term_of} class *}
   2.107 +subsubsection {* Code generator setup *}
   2.108 +
   2.109 +lemma [code func]:
   2.110 +  includes pure_term_syntax
   2.111 +  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
   2.112 +     \<and> list_all2 (op =) tys1 tys2"
   2.113 +  by (auto simp add: list_all2_eq [symmetric])
   2.114 +
   2.115 +code_type "typ"
   2.116 +  (SML "Term.typ")
   2.117 +
   2.118 +code_const Type and TFree
   2.119 +  (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
   2.120 +
   2.121 +code_reserved SML Term
   2.122 +
   2.123 +
   2.124 +
   2.125 +subsection {* Term representation *}
   2.126 +
   2.127 +subsubsection {* Definition *}
   2.128 +
   2.129 +datatype "term" =
   2.130 +    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
   2.131 +  | Fix   vname "typ" (infix ":\<epsilon>" 112)
   2.132 +  | App   "term" "term" (infixl "\<bullet>" 110)
   2.133 +  | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
   2.134 +  | Bnd   nat
   2.135 +
   2.136 +code_datatype Const App Fix
   2.137 +
   2.138 +abbreviation
   2.139 +  Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
   2.140 +  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
   2.141 +abbreviation
   2.142 +  Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
   2.143 +  "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
   2.144 +
   2.145 +ML {*
   2.146 +structure Eval_Aux =
   2.147 +struct
   2.148 +
   2.149 +open Eval_Aux;
   2.150 +
   2.151 +fun mk_term f g (Const (c, ty)) =
   2.152 +      @{term Const} $ Message_String.mk c $ g ty
   2.153 +  | mk_term f g (t1 $ t2) =
   2.154 +      @{term App} $ mk_term f g t1 $ mk_term f g t2
   2.155 +  | mk_term f g (Free v) = f v;
   2.156 +
   2.157 +end;
   2.158 +*}
   2.159 +
   2.160 +
   2.161 +subsubsection {* Class @{text term_of} *}
   2.162  
   2.163  class term_of = typ_of +
   2.164    constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
   2.165    fixes term_of :: "'a \<Rightarrow> term"
   2.166  
   2.167  ML {*
   2.168 -structure TermOf =
   2.169 +structure Eval_Aux =
   2.170  struct
   2.171  
   2.172 +open Eval_Aux;
   2.173 +
   2.174  local
   2.175    fun term_term_of ty =
   2.176      Const (@{const_name term_of}, ty --> @{typ term});
   2.177 @@ -102,9 +220,9 @@
   2.178        fun mk_eq c =
   2.179          let
   2.180            val lhs : term = term_term_of dty $ c;
   2.181 -          val rhs : term = Pure_term.mk_term
   2.182 +          val rhs : term = mk_term
   2.183              (fn (v, ty) => term_term_of ty $ Free (v, ty))
   2.184 -            (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
   2.185 +            (mk_typ (fn (v, sort) => mk_typ_of (TFree (v, sort)))) c
   2.186          in
   2.187            HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   2.188          end;
   2.189 @@ -118,6 +236,7 @@
   2.190  
   2.191  setup {*
   2.192  let
   2.193 +  open Eval_Aux;
   2.194    fun thy_note ((name, atts), thms) =
   2.195      PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   2.196    fun thy_def ((name, atts), t) =
   2.197 @@ -143,7 +262,7 @@
   2.198        val sorts = map (inter_sort o snd) vs_proto;
   2.199        val vs = map fst vs_proto ~~ sorts;
   2.200        val css = map (prep_dtyp thy vs) tycos;
   2.201 -      val defs = map (TermOf.mk_terms_of_defs vs) css;
   2.202 +      val defs = map (mk_terms_of_defs vs) css;
   2.203      in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
   2.204          andalso not (tycos = [@{type_name typ}])
   2.205        then SOME (sorts, defs)
   2.206 @@ -212,12 +331,20 @@
   2.207  end
   2.208  
   2.209  
   2.210 -text {* Adaption for @{typ message_string}s *}
   2.211 +subsubsection {* Code generator setup *}
   2.212 +
   2.213 +lemmas [code func del] = term.recs term.cases term.size
   2.214 +lemmas [code func del] = term_of_message_string.simps
   2.215 +lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   2.216  
   2.217 -lemmas [code func del] = term_of_message_string.simps
   2.218 +code_type "term"
   2.219 +  (SML "Term.term")
   2.220 +
   2.221 +code_const Const and App and Fix
   2.222 +  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
   2.223  
   2.224  
   2.225 -subsection {* Evaluation infrastructure *}
   2.226 +subsection {* Evaluation setup *}
   2.227  
   2.228  ML {*
   2.229  signature EVAL =
   2.230 @@ -238,7 +365,7 @@
   2.231    CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
   2.232  
   2.233  fun eval_term thy =
   2.234 -  TermOf.mk_term_of
   2.235 +  Eval_Aux.mk_term_of
   2.236    #> CodePackage.eval_term thy (eval_invoke thy)
   2.237    #> Code.postprocess_term thy;
   2.238  
     3.1 --- a/src/HOL/Library/Pure_term.thy	Wed Jan 02 15:14:02 2008 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,116 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Pure_term.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Florian Haftmann, TU Muenchen
     3.7 -*)
     3.8 -
     3.9 -header {* Partial reflection of the Pure term algebra in HOL *}
    3.10 -
    3.11 -theory Pure_term
    3.12 -imports Code_Message
    3.13 -begin
    3.14 -
    3.15 -subsection {* Definitions and syntax *}
    3.16 -
    3.17 -types vname = message_string;
    3.18 -types "class" = message_string;
    3.19 -types sort = "class list"
    3.20 -
    3.21 -datatype "typ" =
    3.22 -    Type message_string "typ list"
    3.23 -  | TFree vname sort  
    3.24 -
    3.25 -abbreviation
    3.26 -  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
    3.27 -  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
    3.28 -
    3.29 -locale (open) pure_term_syntax =
    3.30 -  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
    3.31 -    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
    3.32 -    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
    3.33 -
    3.34 -parse_translation {*
    3.35 -let
    3.36 -  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
    3.37 -    | Type_tr ts = raise TERM ("Type_tr", ts);
    3.38 -  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
    3.39 -    | TFree_tr ts = raise TERM ("TFree_tr", ts);
    3.40 -  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
    3.41 -    | Fun_tr ts = raise TERM("Fun_tr", ts);
    3.42 -in [
    3.43 -  ("\\<^fixed>pure_term_Type", Type_tr),
    3.44 -  ("\\<^fixed>pure_term_TFree", TFree_tr),
    3.45 -  ("\\<^fixed>pure_term_Fun", Fun_tr)
    3.46 -] end
    3.47 -*}
    3.48 -
    3.49 -notation (output)
    3.50 -  Type (infixl "{\<struct>}" 120)
    3.51 -and
    3.52 -  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
    3.53 -and
    3.54 -  Fun (infixr "\<rightarrow>" 114)
    3.55 -
    3.56 -datatype "term" =
    3.57 -    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
    3.58 -  | Fix   vname "typ" (infix ":\<epsilon>" 112)
    3.59 -  | App   "term" "term" (infixl "\<bullet>" 110)
    3.60 -  | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
    3.61 -  | Bnd   nat
    3.62 -
    3.63 -abbreviation
    3.64 -  Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
    3.65 -  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
    3.66 -abbreviation
    3.67 -  Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
    3.68 -  "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
    3.69 -
    3.70 -
    3.71 -subsection {* ML interface *}
    3.72 -
    3.73 -ML {*
    3.74 -structure Pure_term =
    3.75 -struct
    3.76 -
    3.77 -val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
    3.78 -
    3.79 -fun mk_typ f (Type (tyco, tys)) =
    3.80 -      @{term Type} $ Message_String.mk tyco
    3.81 -        $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
    3.82 -  | mk_typ f (TFree v) =
    3.83 -      f v;
    3.84 -
    3.85 -fun mk_term f g (Const (c, ty)) =
    3.86 -      @{term Const} $ Message_String.mk c $ g ty
    3.87 -  | mk_term f g (t1 $ t2) =
    3.88 -      @{term App} $ mk_term f g t1 $ mk_term f g t2
    3.89 -  | mk_term f g (Free v) = f v;
    3.90 -
    3.91 -end;
    3.92 -*}
    3.93 -
    3.94 -
    3.95 -subsection {* Code generator setup *}
    3.96 -
    3.97 -lemma [code func]:
    3.98 -  includes pure_term_syntax
    3.99 -  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
   3.100 -     \<and> list_all2 (op =) tys1 tys2"
   3.101 -  by (auto simp add: list_all2_eq [symmetric])
   3.102 -
   3.103 -code_datatype Const App Fix
   3.104 -
   3.105 -lemmas [code func del] = term.recs term.cases term.size
   3.106 -lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   3.107 -
   3.108 -code_type "typ" and "term"
   3.109 -  (SML "Term.typ" and "Term.term")
   3.110 -
   3.111 -code_const Type and TFree
   3.112 -  (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
   3.113 -
   3.114 -code_const Const and App and Fix
   3.115 -  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
   3.116 - 
   3.117 -code_reserved SML Term
   3.118 -
   3.119 -end