# HG changeset patch # User haftmann # Date 1199283255 -3600 # Node ID 474f8ba9dfa9bd0a2c6a7196ebf95e62e1c329d7 # Parent c03e9d04b3e408b9e32f077a94f6fe1d63f80eb0 improved evaluation mechanism diff -r c03e9d04b3e4 -r 474f8ba9dfa9 src/HOL/IsaMakefile --- 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 \ diff -r c03e9d04b3e4 -r 474f8ba9dfa9 src/HOL/Library/Eval.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 \ typ \ typ" where + "Fun ty1 ty2 \ Type (STR ''fun'') [ty1, ty2]" + +locale (open) pure_term_syntax = -- {* FIXME drop this *} + fixes pure_term_Type :: "message_string \ typ list \ typ" (infixl "{\}" 120) + and pure_term_TFree :: "vname \ sort \ typ" ("\_\_\" [118, 118] 117) + and pure_term_Fun :: "typ \ typ \ typ" (infixr "\" 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 "{\}" 120) +and + TFree ("\_\_\" [118, 118] 117) +and + Fun (infixr "\" 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\{} itself \ 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 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 + \ 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 "\\" 112) + | Fix vname "typ" (infix ":\" 112) + | App "term" "term" (infixl "\" 110) + | Abs "vname \ typ" "term" (infixr "\" 111) + | Bnd nat + +code_datatype Const App Fix + +abbreviation + Apps :: "term \ term list \ term" (infixl "{\}" 110) where + "t {\} ts \ foldl (op \) t ts" +abbreviation + Abss :: "(vname \ typ) list \ term \ term" (infixr "{\}" 111) where + "vs {\} t \ foldr (op \) 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\{} itself \ typ" fixes term_of :: "'a \ 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\term) = t2 \ 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; diff -r c03e9d04b3e4 -r 474f8ba9dfa9 src/HOL/Library/Pure_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 \ typ \ typ" where - "Fun ty1 ty2 \ Type (STR ''fun'') [ty1, ty2]" - -locale (open) pure_term_syntax = - fixes pure_term_Type :: "message_string \ typ list \ typ" (infixl "{\}" 120) - and pure_term_TFree :: "vname \ sort \ typ" ("\_\_\" [118, 118] 117) - and pure_term_Fun :: "typ \ typ \ typ" (infixr "\" 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 "{\}" 120) -and - TFree ("\_\_\" [118, 118] 117) -and - Fun (infixr "\" 114) - -datatype "term" = - Const message_string "typ" (infix "\\" 112) - | Fix vname "typ" (infix ":\" 112) - | App "term" "term" (infixl "\" 110) - | Abs "vname \ typ" "term" (infixr "\" 111) - | Bnd nat - -abbreviation - Apps :: "term \ term list \ term" (infixl "{\}" 110) where - "t {\} ts \ foldl (op \) t ts" -abbreviation - Abss :: "(vname \ typ) list \ term \ term" (infixr "{\}" 111) where - "vs {\} t \ foldr (op \) 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 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 - \ 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\term) = t2 \ 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