# HG changeset patch # User haftmann # Date 1221549684 -7200 # Node ID 7ebe8dc06cbb297c142de663df3ae671128189a5 # Parent 77221ee0f7b97ca253225e9b53a810904ae9945a evaluation using code generator diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Code_Eval.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Code_Eval.thy Tue Sep 16 09:21:24 2008 +0200 @@ -0,0 +1,248 @@ +(* Title: HOL/Code_Eval.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Term evaluation using the generic code generator *} + +theory Code_Eval +imports Plain RType +begin + +subsection {* Term representation *} + +subsubsection {* Terms and class @{text term_of} *} + +datatype "term" = dummy_term + +definition + Const :: "message_string \ rtype \ term" +where + "Const _ _ = dummy_term" + +definition + App :: "term \ term \ term" +where + "App _ _ = dummy_term" + +code_datatype Const App + +class term_of = rtype + + fixes term_of :: "'a \ term" + +lemma term_of_anything: "term_of x \ t" + by (rule eq_reflection) (cases "term_of x", cases t, simp) + +ML {* +structure Eval = +struct + +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 + | mk_term f g (Bound i) = Bound i + | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t); + +fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; + +end; +*} + + +subsubsection {* @{text term_of} instances *} + +setup {* +let + fun add_term_of_def ty vs tyco thy = + let + val lhs = Const (@{const_name term_of}, ty --> @{typ term}) + $ Free ("x", ty); + val rhs = @{term "undefined \ term"}; + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) + |> snd + |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) + |> LocalTheory.exit + |> ProofContext.theory_of + end; + fun interpretator (tyco, (raw_vs, _)) thy = + let + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; + val constrain_sort = + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; + val vs = (map o apsnd) constrain_sort raw_vs; + val ty = Type (tyco, map TFree vs); + in + thy + |> RType.perhaps_add_def tyco + |> not has_inst ? add_term_of_def ty vs tyco + end; +in + Code.type_interpretation interpretator +end +*} + +setup {* +let + fun mk_term_of_eq ty vs tyco (c, tys) = + let + val t = list_comb (Const (c, tys ---> ty), + map Free (Name.names Name.context "a" tys)); + in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term + (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) + (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) + end; + fun prove_term_of_eq ty eq thy = + let + val cty = Thm.ctyp_of thy ty; + val (arg, rhs) = pairself (Thm.cterm_of thy) eq; + val thm = @{thm term_of_anything} + |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] + |> Thm.varifyT; + in + thy + |> Code.add_func thm + end; + fun interpretator (tyco, (raw_vs, raw_cs)) thy = + let + val constrain_sort = + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; + val vs = (map o apsnd) constrain_sort raw_vs; + val cs = (map o apsnd o map o map_atyps) + (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; + val ty = Type (tyco, map TFree vs); + val eqs = map (mk_term_of_eq ty vs tyco) cs; + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + in + thy + |> Code.del_funcs const + |> fold (prove_term_of_eq ty) eqs + end; +in + Code.type_interpretation interpretator +end +*} + + +subsubsection {* Code generator setup *} + +lemmas [code func del] = term.recs term.cases term.size +lemma [code func, code func del]: "(t1\term) = t2 \ t1 = t2" .. + +lemma [code func, code func del]: "(term_of \ rtype \ term) = term_of" .. +lemma [code func, code func del]: "(term_of \ term \ term) = term_of" .. +lemma [code func, code func del]: "(term_of \ message_string \ term) = term_of" .. + +code_type "term" + (SML "Term.term") + +code_const Const and App + (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") + +code_const "term_of \ message_string \ term" + (SML "Message'_String.mk") + + +subsubsection {* Syntax *} + +print_translation {* +let + val term = Const ("", dummyT); + fun tr1' [_, _] = term; + fun tr2' [] = term; +in + [(@{const_syntax Const}, tr1'), + (@{const_syntax App}, tr1'), + (@{const_syntax dummy_term}, tr2')] +end +*} +setup {* + Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \ 'b"}), NoSyn) + #> snd +*} + +notation (output) + rterm_of ("\_\") + +locale rterm_syntax = + fixes rterm_of_syntax :: "'a \ 'b" ("\_\") + +parse_translation {* +let + fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t + | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts); +in + [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)] +end +*} + +setup {* +let + val subst_rterm_of = Eval.mk_term + (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) + (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); + fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t + | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = + error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) + | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); + fun subst_rterm_of'' t = + let + val t' = subst_rterm_of' (strip_comb t); + in if t aconv t' + then NONE + else SOME t' + end; + fun check_rterm_of ts ctxt = + let + val ts' = map subst_rterm_of'' ts; + in if exists is_some ts' + then SOME (map2 the_default ts ts', ctxt) + else NONE + end; +in + Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of) +end; +*} + +hide const dummy_term +hide (open) const Const App +hide (open) const term_of + + +subsection {* Evaluation setup *} + +ML {* +signature EVAL = +sig + val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term + val eval_ref: (unit -> term) option ref + val eval_term: theory -> term -> term +end; + +structure Eval : EVAL = +struct + +open Eval; + +val eval_ref = ref (NONE : (unit -> term) option); + +fun eval_term thy t = + t + |> Eval.mk_term_of (fastype_of t) + |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t []) + |> Code.postprocess_term thy; + +end; +*} + +setup {* + Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of) +*} + +end diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:24 2008 +0200 @@ -6,19 +6,11 @@ header {* Code generation of pretty characters (and strings) *} theory Code_Char -imports Plain "~~/src/HOL/List" +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" begin declare char.recs [code func del] char.cases [code func del] -lemma [code func]: - "size (c\char) = 0" - by (cases c) simp - -lemma [code func]: - "char_size (c\char) = 0" - by (cases c) simp - code_type char (SML "char") (OCaml "char") @@ -43,4 +35,10 @@ (OCaml "!((_ : char) = _)") (Haskell infixl 4 "==") +lemma [code func, code func del]: + "(Code_Eval.term_of :: char \ term) = Code_Eval.term_of" .. + +code_const "Code_Eval.term_of \ char \ term" + (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") + end diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Code_Index.thy --- a/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:24 2008 +0200 @@ -5,7 +5,7 @@ header {* Type of indices *} theory Code_Index -imports Plain "~~/src/HOL/Presburger" +imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" begin text {* @@ -234,7 +234,8 @@ text {* Measure function (for termination proofs) *} -lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial) +lemma [measure_function]: + "is_measure nat_of_index" by (rule is_measure_trivial) subsection {* ML interface *} @@ -278,7 +279,7 @@ unfolding div_mod_index_def by simp -subsection {* Code serialization *} +subsection {* Code generator setup *} text {* Implementation of indices by bounded integers *} @@ -333,4 +334,12 @@ (OCaml "!((_ : int) < _)") (Haskell infix 4 "<") +text {* Evaluation *} + +lemma [code func, code func del]: + "(Code_Eval.term_of \ index \ term) = Code_Eval.term_of" .. + +code_const "Code_Eval.term_of \ index \ term" + (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)") + end diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Code_Integer.thy Tue Sep 16 09:21:24 2008 +0200 @@ -6,7 +6,7 @@ header {* Pretty integer literals for code generation *} theory Code_Integer -imports Plain "~~/src/HOL/Presburger" +imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" begin text {* @@ -90,4 +90,12 @@ code_reserved SML IntInf code_reserved OCaml Big_int +text {* Evaluation *} + +lemma [code func, code func del]: + "(Code_Eval.term_of \ int \ term) = Code_Eval.term_of" .. + +code_const "Code_Eval.term_of \ int \ term" + (SML "HOLogic.mk'_number/ HOLogic.intT") + end \ No newline at end of file diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 16 09:21:24 2008 +0200 @@ -6,7 +6,7 @@ header {* Implementation of natural numbers by target-language integers *} theory Efficient_Nat -imports Plain Code_Integer Code_Index +imports Plain Code_Index Code_Integer begin text {* @@ -424,6 +424,15 @@ "op < \ nat \ nat \ bool" ("(_ nat \ term) = Code_Eval.term_of" .. + +code_const "Code_Eval.term_of \ nat \ term" + (SML "HOLogic.mk'_number/ HOLogic.natT") + + text {* Module names *} code_modulename SML diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Library.thy Tue Sep 16 09:21:24 2008 +0200 @@ -19,7 +19,6 @@ Dense_Linear_Order Efficient_Nat Enum - Eval Eval_Witness Executable_Set "../Real/Float" diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/Nested_Environment.thy --- a/src/HOL/Library/Nested_Environment.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/Nested_Environment.thy Tue Sep 16 09:21:24 2008 +0200 @@ -6,7 +6,7 @@ header {* Nested environments *} theory Nested_Environment -imports Plain "~~/src/HOL/List" +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" begin text {* @@ -523,7 +523,7 @@ qed qed -text {* Equality of environments for code generation *} +text {* Environments and code generation *} lemma [code func, code func del]: fixes e1 e2 :: "('b\eq, 'a\eq, 'c\eq) env" @@ -567,4 +567,7 @@ of None \ False | Some b \ a = b))" by simp qed simp_all +lemma [code func, code func del]: + "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \ term) = Code_Eval.term_of" .. + end diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Library/RType.thy --- a/src/HOL/Library/RType.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Library/RType.thy Tue Sep 16 09:21:24 2008 +0200 @@ -6,7 +6,7 @@ header {* Reflecting Pure types into HOL *} theory RType -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Message" "~~/src/HOL/Code_Index" (* import all 'special code' types *) +imports Plain "~~/src/HOL/List" "~~/src/HOL/Library/Code_Message" begin datatype "rtype" = RType message_string "rtype list" diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/Main.thy Tue Sep 16 09:21:24 2008 +0200 @@ -5,7 +5,7 @@ header {* Main HOL *} theory Main -imports Plain Map Nat_Int_Bij Recdef +imports Plain Code_Eval Map Nat_Int_Bij Recdef begin ML {* val HOL_proofs = ! Proofterm.proofs *} diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/ex/Codegenerator_Pretty.thy --- a/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 16 09:21:24 2008 +0200 @@ -9,22 +9,13 @@ imports ExecutableContent Code_Char Efficient_Nat begin -setup {* - Code.del_funcs - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"})) - #> Code.del_funcs - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"})) - #> Code.del_funcs - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"})) - #> Code.del_funcs - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"})) -*} +declare isnorm.simps [code func del] + +lemma [code func, code func del]: + "(Code_Eval.term_of :: char \ term) = Code_Eval.term_of" .. declare char.recs [code func del] char.cases [code func del] - char.size [code func del] - -declare isnorm.simps [code func del] ML {* (*FIXME get rid of this*) nonfix union; diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/ex/Quickcheck.thy Tue Sep 16 09:21:24 2008 +0200 @@ -5,7 +5,7 @@ header {* A simple counterexample generator *} theory Quickcheck -imports Random Eval +imports Random Code_Eval begin subsection {* The @{text random} class *} @@ -19,7 +19,7 @@ begin definition - "random _ = return (TYPE('a), \u. Eval.Const (STR ''TYPE'') RTYPE('a))" + "random _ = return (TYPE('a), \u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))" instance .. @@ -173,9 +173,9 @@ "random n = (do (b, _) \ random n; (m, t) \ random n; - return (if b then (int m, \u. Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())) - else (- int m, \u. Eval.App (Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \ int)) - (Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())))) + return (if b then (int m, \u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())) + else (- int m, \u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \ int)) + (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())))) done)" instance .. @@ -229,7 +229,7 @@ begin definition random_fun :: "index \ seed \ (('a \ 'b) \ (unit \ term)) \ seed" where - "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Eval.term_of (random n) split_seed" + "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed" instance .. diff -r 77221ee0f7b9 -r 7ebe8dc06cbb src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Sep 16 09:21:22 2008 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Sep 16 09:21:24 2008 +0200 @@ -6,7 +6,7 @@ no_document use_thys [ "Parity", - "Eval", + "Code_Eval", "State_Monad", "Efficient_Nat_examples", "ExecutableContent",