# HG changeset patch # User haftmann # Date 1174913685 -7200 # Node ID d929a900584cfd99bffe71a05db8b889c3adf863 # Parent f9bf5c08b446c3583b46075d16536bd8c9d467ca cleaned up Library/ and ex/ diff -r f9bf5c08b446 -r d929a900584c src/HOL/Library/Eval.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Eval.thy Mon Mar 26 14:54:45 2007 +0200 @@ -0,0 +1,154 @@ +(* Title: HOL/Library/Eval.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* A simple term evaluation mechanism *} + +theory Eval +imports Pure_term +begin + +subsection {* The typ_of class *} + +class typ_of = type + + fixes typ_of :: "'a itself \ typ" + +ML {* +structure TypOf = +struct + +val class_typ_of = Sign.intern_class @{theory} "typ_of"; + +fun term_typ_of_type ty = + Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) + $ Logic.mk_type ty; + +fun mk_typ_of_def ty = + let + val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) + $ Free ("x", Term.itselfT ty) + val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty + in Logic.mk_equals (lhs, rhs) end; + +end; +*} + +setup {* +let + fun mk arities _ thy = + (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def + (Type (tyco, + map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); + fun hook specs = + DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) + (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) + [TypOf.class_typ_of] mk ((K o K) I) +in DatatypeCodegen.add_codetypes_hook_bootstrap hook end +*} + + +subsection {* term_of class *} + +class term_of = typ_of + + constrains typ_of :: "'a itself \ typ" + fixes term_of :: "'a \ term" + +ML {* +structure TermOf = +struct + +local + fun term_term_of ty = + Const (@{const_name term_of}, ty --> @{typ term}); +in + val class_term_of = Sign.intern_class @{theory} "term_of"; + fun mk_terms_of_defs vs (tyco, cs) = + let + val dty = Type (tyco, map TFree vs); + fun mk_eq c = + let + val lhs : term = term_term_of dty $ c; + val rhs : term = Pure_term.mk_term + (fn (v, ty) => term_term_of ty $ Free (v, ty)) + (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c + in + HOLogic.mk_eq (lhs, rhs) + end; + in map mk_eq cs end; + fun mk_term_of t = + term_term_of (Term.fastype_of t) $ t; +end; + +end; +*} + +setup {* +let + fun thy_note ((name, atts), thms) = + PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); + fun thy_def ((name, atts), t) = + PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); + fun mk arities css thy = + let + val (_, asorts, _) :: _ = arities; + val vs = Name.names Name.context "'a" asorts; + val defs = map (TermOf.mk_terms_of_defs vs) css; + val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs; + in + thy + |> PrimrecPackage.gen_primrec thy_note thy_def "" defs' + |> snd + end; + fun hook specs = + if (fst o hd) specs = (fst o dest_Type) @{typ typ} then I + else + DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) + (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) + [TermOf.class_term_of] ((K o K o pair) []) mk +in DatatypeCodegen.add_codetypes_hook_bootstrap hook end +*} + +text {* Disable for characters and ml_strings *} + +code_const "typ_of \ char itself \ typ" and "term_of \ char \ term" + (SML "!((_); raise Fail \"typ'_of'_char\")" + and "!((_); raise Fail \"term'_of'_char\")") + (OCaml "!((_); failwith \"typ'_of'_char\")" + and "!((_); failwith \"term'_of'_char\")") + (Haskell "error/ \"typ'_of'_char\"" + and "error/ \"term'_of'_char\"") + +code_const "term_of \ ml_string \ term" + (SML "!((_); raise Fail \"term'_of'_ml'_string\")") + (OCaml "!((_); failwith \"term'_of'_ml'_string\")") + +subsection {* Evaluation infrastructure *} + +ML {* +signature EVAL = +sig + val eval_term: theory -> term -> term + val term: string -> unit + val eval_ref: term option ref +end; + +structure Eval : EVAL = +struct + +val eval_ref = ref (NONE : term option); + +fun eval_term thy t = + CodegenPackage.eval_term + thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t); + +fun term t = + let + val thy = the_context (); + val t = eval_term thy (Sign.read_term thy t); + in (writeln o Sign.string_of_term thy) t end; + +end; +*} + +end \ No newline at end of file diff -r f9bf5c08b446 -r d929a900584c src/HOL/Library/Pure_term.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Pure_term.thy Mon Mar 26 14:54:45 2007 +0200 @@ -0,0 +1,116 @@ +(* Title: HOL/Library/Pure_term.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Embedding (a subset of) the Pure term algebra in HOL *} + +theory Pure_term +imports MLString +begin + +subsection {* Definitions *} + +types vname = ml_string; +types "class" = ml_string; +types sort = "class list" + +datatype "typ" = + Type ml_string "typ list" (infix "{\}" 120) + | TFix vname sort (infix "\\" 117) + +abbreviation + Fun :: "typ \ typ \ typ" (infixr "\" 115) where + "ty1 \ ty2 \ Type (STR ''fun'') [ty1, ty2]" +abbreviation + Funs :: "typ list \ typ \ typ" (infixr "{\}" 115) where + "tys {\} ty \ foldr (op \) tys ty" + +datatype "term" = + Const ml_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 MLString.mk; + +fun mk_typ f (Type (tyco, tys)) = + @{term Type} $ MLString.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} $ MLString.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 *} + +definition + Bound :: "int \ term" +where + "Bound k = Bnd (nat k)" + +lemma Bnd_Bound [code inline, code func]: + "Bnd n = Bound (int n)" + unfolding Bound_def by auto + +definition + Absp :: "vname \ typ \ term \ term" +where + "Absp v ty t = (v, ty) \ t" + +lemma Abs_Absp [code inline, code func]: + "(op \) (v, ty) = Absp v ty" + by rule (auto simp add: Absp_def) + +definition + "term_case' f g h k l = term_case f g h (\(v, ty). k v ty) (\n. l (int n))" + +lemma term_case' [code inline, code func]: + "term_case = (\f g h k l. term_case' f g h (\v ty. k (v, ty)) (\v. l (nat v)))" + unfolding term_case'_def by auto + +code_datatype Const App Fix Absp Bound +lemmas [code func] = Bnd_Bound Abs_Absp + +code_type "typ" and "term" + (SML "Term.typ" and "Term.term") + +code_const Type and TFix + (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)") + +code_const Const and App and Fix + and Absp and Bound + (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)" + and "Term.Abs/ (_, _, _)" and "Term.Bound/ (IntInf.toInt/ _)") + +code_const term_rec and term_case and "size \ term \ nat" + (SML "!(_; _; _; _; _; raise Fail \"term'_rec\")" + and "!(_; _; _; _; _; raise Fail \"term'_case\")" + and "!(_; raise Fail \"size'_term\")") + +code_reserved SML Term + +end \ No newline at end of file diff -r f9bf5c08b446 -r d929a900584c src/HOL/ex/CodeEmbed.thy --- a/src/HOL/ex/CodeEmbed.thy Mon Mar 26 14:53:07 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,88 +0,0 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) - -header {* Embedding (a subset of) the Pure term algebra in HOL *} - -theory CodeEmbed -imports Main MLString -begin - -subsection {* Definitions *} - -types vname = ml_string; -types "class" = ml_string; -types sort = "class list" - -datatype "typ" = - Type ml_string "typ list" (infix "{\}" 120) - | TFix vname sort (infix "\\" 117) - -abbreviation - Fun :: "typ \ typ \ typ" (infixr "\" 115) where - "ty1 \ ty2 \ Type (STR ''fun'') [ty1, ty2]" -abbreviation - Funs :: "typ list \ typ \ typ" (infixr "{\}" 115) where - "tys {\} ty \ foldr (op \) tys ty" - -datatype "term" = - Const ml_string "typ" (infix "\\" 112) - | Fix vname "typ" (infix ":\" 112) - | App "term" "term" (infixl "\" 110) - -abbreviation - Apps :: "term \ term list \ term" (infixl "{\}" 110) where - "t {\} ts \ foldl (op \) t ts" - - -subsection {* ML interface *} - -ML {* -structure Embed = -struct - -local - val thy = the_context (); - val const_Type = Sign.intern_const thy "Type"; - val const_TFix = Sign.intern_const thy "TFix"; - val const_Const = Sign.intern_const thy "Const"; - val const_App = Sign.intern_const thy "App"; - val const_Fix = Sign.intern_const thy "Fix"; -in - val typ_vname = Type (Sign.intern_type thy "vname", []); - val typ_class = Type (Sign.intern_type thy "class", []); - val typ_sort = Type (Sign.intern_type thy "sort", []); - val typ_typ = Type (Sign.intern_type thy "typ", []); - val typ_term = Type (Sign.intern_type thy "term", []); - val term_sort = HOLogic.mk_list typ_class o map MLString.term_ml_string; - fun term_typ f (Type (tyco, tys)) = - Const (const_Type, MLString.typ_ml_string --> HOLogic.listT typ_typ --> typ_typ) - $ MLString.term_ml_string tyco $ HOLogic.mk_list typ_typ (map (term_typ f) tys) - | term_typ f (TFree v) = - f v; - fun term_term f g (Const (c, ty)) = - Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term) - $ MLString.term_ml_string c $ g ty - | term_term f g (t1 $ t2) = - Const (const_App, typ_term --> typ_term --> typ_term) - $ term_term f g t1 $ term_term f g t2 - | term_term f g (Free v) = f v; -end; - -end; -*} - - -subsection {* Code serialization setup *} - -code_type "typ" and "term" - (SML "Term.typ" and "Term.term") - -code_const Type and TFix - and Const and App and Fix - (SML "Term.Type (_, _)" and "Term.TFree (_, _)" - and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)") - -code_reserved SML Term - -end \ No newline at end of file diff -r f9bf5c08b446 -r d929a900584c src/HOL/ex/CodeEval.thy --- a/src/HOL/ex/CodeEval.thy Mon Mar 26 14:53:07 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) - -header {* A simple embedded term evaluation mechanism *} - -theory CodeEval -imports CodeEmbed -begin - -subsection {* The typ_of class *} - -class typ_of = type + - fixes typ_of :: "'a itself \ typ" - -ML {* -structure TypOf = -struct - -local - val thy = the_context (); - val const_typ_of = Sign.intern_const thy "typ_of"; - fun term_typ_of ty = Const (const_typ_of, Term.itselfT ty --> Embed.typ_typ); -in - val class_typ_of = Sign.intern_class thy "typ_of"; - fun term_typ_of_type ty = - term_typ_of ty $ Logic.mk_type ty; - fun mk_typ_of_def ty = - let - val lhs = term_typ_of ty $ Free ("x", Term.itselfT ty) - val rhs = Embed.term_typ (fn v => term_typ_of_type (TFree v)) ty - in Logic.mk_equals (lhs, rhs) end; -end; - -end; -*} - -setup {* -let - fun mk arities _ thy = - (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def - (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); - fun hook specs = - DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) - (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TypOf.class_typ_of] mk ((K o K) I) -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end -*} - - -subsection {* term_of class *} - -class term_of = typ_of + - constrains typ_of :: "'a itself \ typ" - fixes term_of :: "'a \ term" - -ML {* -structure TermOf = -struct - -local - val thy = the_context (); - val const_term_of = Sign.intern_const thy "term_of"; - fun term_term_of ty = Const (const_term_of, ty --> Embed.typ_term); -in - val class_term_of = Sign.intern_class thy "term_of"; - fun mk_terms_of_defs vs (tyco, cs) = - let - val dty = Type (tyco, map TFree vs); - fun mk_eq c = - let - val lhs : term = term_term_of dty $ c; - val rhs : term = Embed.term_term - (fn (v, ty) => term_term_of ty $ Free (v, ty)) - (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c - in - HOLogic.mk_eq (lhs, rhs) - end; - in map mk_eq cs end; - fun mk_term_of t = - term_term_of (Term.fastype_of t) $ t; -end; - -end; -*} - -setup {* -let - fun thy_note ((name, atts), thms) = - PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); - fun thy_def ((name, atts), t) = - PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); - fun mk arities css thy = - let - val (_, asorts, _) :: _ = arities; - val vs = Name.names Name.context "'a" asorts; - val defs = map (TermOf.mk_terms_of_defs vs) css; - val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs; - in - thy - |> PrimrecPackage.gen_primrec thy_note thy_def "" defs' - |> snd - end; - fun hook specs = - if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I - else - DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) - (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TermOf.class_term_of] ((K o K o pair) []) mk -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end -*} - -text {* Disable for characters and ml_strings *} - -code_const "typ_of \ char itself \ typ" and "term_of \ char \ term" - (SML "!((_); raise Fail \"typ'_of'_char\")" - and "!((_); raise Fail \"term'_of'_char\")") - (OCaml "!((_); failwith \"typ'_of'_char\")" - and "!((_); failwith \"term'_of'_char\")") - (Haskell "error/ \"typ'_of'_char\"" - and "error/ \"term'_of'_char\"") - -code_const "term_of \ ml_string \ term" - (SML "!((_); raise Fail \"term'_of'_ml'_string\")") - (OCaml "!((_); failwith \"term'_of'_ml'_string\")") - -subsection {* Evaluation infrastructure *} - -ML {* -signature EVAL = -sig - val eval_term: theory -> term -> term - val term: string -> unit - val eval_ref: term option ref -end; - -structure Eval : EVAL = -struct - -val eval_ref = ref (NONE : term option); - -fun eval_term thy t = - CodegenPackage.eval_term - thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t); - -fun term t = - let - val thy = the_context (); - val t = eval_term thy (Sign.read_term thy t); - in (writeln o Sign.string_of_term thy) t end; - -end; -*} - - -subsection {* Small examples *} - -ML {* Eval.term "(Suc 2 + 1) * 4" *} -ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} -ML {* Eval.term "[]::nat list" *} -ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *} - -text {* a fancy datatype *} - -datatype ('a, 'b) bair = - Bair "'a\order" 'b - | Shift "('a, 'b) cair" - | Dummy unit -and ('a, 'b) cair = - Cair 'a 'b - -ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *} - -text {* also test evaluation oracle *} - -lemma "True \ False" by eval -lemma "\ (Suc 0 = Suc 1)" by eval - -end \ No newline at end of file diff -r f9bf5c08b446 -r d929a900584c src/HOL/ex/Eval_examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Eval_examples.thy Mon Mar 26 14:54:45 2007 +0200 @@ -0,0 +1,34 @@ +(* ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Small examples for evaluation mechanisms *} + +theory Eval_examples +imports Eval +begin + +text {* evaluation oracle *} + +lemma "True \ False" by eval +lemma "\ (Suc 0 = Suc 1)" by eval + +text {* term evaluation *} + +ML {* Eval.term "(Suc 2 + 1) * 4" *} +ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} +ML {* Eval.term "[]::nat list" *} +ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *} + +text {* a fancy datatype *} + +datatype ('a, 'b) bair = + Bair "'a\order" 'b + | Shift "('a, 'b) cair" + | Dummy unit +and ('a, 'b) cair = + Cair 'a 'b + +ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *} + +end \ No newline at end of file