--- /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 \<Rightarrow> 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 \<Rightarrow> typ"
+ fixes term_of :: "'a \<Rightarrow> 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 \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> 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 \<Colon> ml_string \<Rightarrow> 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
--- /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 "{\<struct>}" 120)
+ | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
+
+abbreviation
+ Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
+ "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+abbreviation
+ Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
+ "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
+
+datatype "term" =
+ Const ml_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 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 \<Rightarrow> 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 \<Rightarrow> typ \<Rightarrow> term \<Rightarrow> term"
+where
+ "Absp v ty t = (v, ty) \<mapsto> t"
+
+lemma Abs_Absp [code inline, code func]:
+ "(op \<mapsto>) (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 (\<lambda>(v, ty). k v ty) (\<lambda>n. l (int n))"
+
+lemma term_case' [code inline, code func]:
+ "term_case = (\<lambda>f g h k l. term_case' f g h (\<lambda>v ty. k (v, ty)) (\<lambda>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 \<Colon> term \<Rightarrow> 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
--- 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 "{\<struct>}" 120)
- | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
-
-abbreviation
- Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
- "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
-abbreviation
- Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
- "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
-
-datatype "term" =
- Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
- | Fix vname "typ" (infix ":\<epsilon>" 112)
- | App "term" "term" (infixl "\<bullet>" 110)
-
-abbreviation
- Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
- "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) 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
--- 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 \<Rightarrow> 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 \<Rightarrow> typ"
- fixes term_of :: "'a \<Rightarrow> 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 \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> 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 \<Colon> ml_string \<Rightarrow> 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\<Colon>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 \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-
-end
\ No newline at end of file
--- /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 \<or> False" by eval
+lemma "\<not> (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\<Colon>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