# HG changeset patch # User haftmann # Date 1253712325 -7200 # Node ID 82956a3f0e0b1b521c65b76bf213d35448eef483 # Parent 3bd9296b16acd57103b694d1c8736aa7e167493b# Parent 5f13912245fff387aa49ffd43bdcfe6f08758d24 merged diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Wed Sep 23 13:48:16 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,271 +0,0 @@ -(* Title: HOL/Code_Eval.thy - Author: Florian Haftmann, TU Muenchen -*) - -header {* Term evaluation using the generic code generator *} - -theory Code_Eval -imports Plain Typerep Code_Numeral -begin - -subsection {* Term representation *} - -subsubsection {* Terms and class @{text term_of} *} - -datatype "term" = dummy_term - -definition Const :: "String.literal \ typerep \ term" where - "Const _ _ = dummy_term" - -definition App :: "term \ term \ term" where - "App _ _ = dummy_term" - -code_datatype Const App - -class term_of = typerep + - fixes term_of :: "'a \ term" - -lemma term_of_anything: "term_of x \ t" - by (rule eq_reflection) (cases "term_of x", cases t, simp) - -definition valapp :: "('a \ 'b) \ (unit \ term) - \ 'a \ (unit \ term) \ 'b \ (unit \ term)" where - "valapp f x = (fst f (fst x), \u. App (snd f ()) (snd x ()))" - -lemma valapp_code [code, code_unfold]: - "valapp (f, tf) (x, tx) = (f x, \u. App (tf ()) (tx ()))" - by (simp only: valapp_def fst_conv snd_conv) - - -subsubsection {* @{text term_of} instances *} - -instantiation "fun" :: (typerep, typerep) term_of -begin - -definition - "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') - [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" - -instance .. - -end - -setup {* -let - fun add_term_of tyco raw_vs thy = - let - val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; - val ty = Type (tyco, map TFree vs); - 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)); - fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst - o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; - in - thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) - |> `(fn lthy => Syntax.check_term lthy eq) - |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) - |> snd - |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) - end; - fun ensure_term_of (tyco, (raw_vs, _)) thy = - let - val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) - andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; - in if need_inst then add_term_of tyco raw_vs thy else thy end; -in - Code.type_interpretation ensure_term_of -end -*} - -setup {* -let - fun mk_term_of_eq thy ty vs tyco (c, tys) = - let - val t = list_comb (Const (c, tys ---> ty), - map Free (Name.names Name.context "a" tys)); - val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify) - (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) - val cty = Thm.ctyp_of thy ty; - in - @{thm term_of_anything} - |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] - |> Thm.varifyT - end; - fun add_term_of_code tyco raw_vs raw_cs thy = - let - val algebra = Sign.classes_of thy; - val vs = map (fn (v, sort) => - (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; - val ty = Type (tyco, map TFree vs); - val cs = (map o apsnd o map o map_atyps) - (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); - val eqs = map (mk_term_of_eq thy ty vs tyco) cs; - in - thy - |> Code.del_eqns const - |> fold Code.add_eqn eqs - end; - fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = - let - val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; - in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; -in - Code.type_interpretation ensure_term_of_code -end -*} - - -subsubsection {* Code generator setup *} - -lemmas [code del] = term.recs term.cases term.size -lemma [code, code del]: "eq_class.eq (t1\term) t2 \ eq_class.eq t1 t2" .. - -lemma [code, code del]: "(term_of \ typerep \ term) = term_of" .. -lemma [code, code del]: "(term_of \ term \ term) = term_of" .. -lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. -lemma [code, code del]: - "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Eval.term) = Code_Eval.term_of" .. -lemma [code, code del]: - "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.seq \ Code_Eval.term) = Code_Eval.term_of" .. - -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c = - (let (n, m) = nibble_pair_of_char c - in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \ nibble \ char))) - (Code_Eval.term_of n)) (Code_Eval.term_of m))" - by (subst term_of_anything) rule - -code_type "term" - (Eval "Term.term") - -code_const Const and App - (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") - -code_const "term_of \ String.literal \ term" - (Eval "HOLogic.mk'_message'_string") - -code_reserved Eval HOLogic - - -subsubsection {* Syntax *} - -definition termify :: "'a \ term" where - [code del]: "termify x = dummy_term" - -abbreviation valtermify :: "'a \ 'a \ (unit \ term)" where - "valtermify x \ (x, \u. termify x)" - -setup {* -let - fun map_default f xs = - let val ys = map f xs - in if exists is_some ys - then SOME (map2 the_default xs ys) - else NONE - end; - fun subst_termify_app (Const (@{const_name termify}, T), [t]) = - if not (Term.has_abs t) - then if fold_aterms (fn Const _ => I | _ => K false) t true - then SOME (HOLogic.reflect_term t) - else error "Cannot termify expression containing variables" - else error "Cannot termify expression containing abstraction" - | subst_termify_app (t, ts) = case map_default subst_termify ts - of SOME ts' => SOME (list_comb (t, ts')) - | NONE => NONE - and subst_termify (Abs (v, T, t)) = (case subst_termify t - of SOME t' => SOME (Abs (v, T, t')) - | NONE => NONE) - | subst_termify t = subst_termify_app (strip_comb t) - fun check_termify ts ctxt = map_default subst_termify ts - |> Option.map (rpair ctxt) -in - Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) -end; -*} - -locale term_syntax -begin - -notation App (infixl "<\>" 70) - and valapp (infixl "{\}" 70) - -end - -interpretation term_syntax . - -no_notation App (infixl "<\>" 70) - and valapp (infixl "{\}" 70) - - -subsection {* Numeric types *} - -definition term_of_num :: "'a\{semiring_div} \ 'a\{semiring_div} \ term" where - "term_of_num two = (\_. dummy_term)" - -lemma (in term_syntax) term_of_num_code [code]: - "term_of_num two k = (if k = 0 then termify Int.Pls - else (if k mod two = 0 - then termify Int.Bit0 <\> term_of_num two (k div two) - else termify Int.Bit1 <\> term_of_num two (k div two)))" - by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) - -lemma (in term_syntax) term_of_nat_code [code]: - "term_of (n::nat) = termify (number_of :: int \ nat) <\> term_of_num (2::nat) n" - by (simp only: term_of_anything) - -lemma (in term_syntax) term_of_int_code [code]: - "term_of (k::int) = (if k = 0 then termify (0 :: int) - else if k > 0 then termify (number_of :: int \ int) <\> term_of_num (2::int) k - else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> term_of_num (2::int) (- k)))" - by (simp only: term_of_anything) - -lemma (in term_syntax) term_of_code_numeral_code [code]: - "term_of (k::code_numeral) = termify (number_of :: int \ code_numeral) <\> term_of_num (2::code_numeral) k" - by (simp only: term_of_anything) - -subsection {* Obfuscate *} - -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 -*} - -hide const dummy_term App valapp -hide (open) const Const termify valtermify term_of term_of_num - - -subsection {* Evaluation setup *} - -ML {* -signature EVAL = -sig - val eval_ref: (unit -> term) option ref - val eval_term: theory -> term -> term -end; - -structure Eval : EVAL = -struct - -val eval_ref = ref (NONE : (unit -> term) option); - -fun eval_term thy t = - Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) []; - -end; -*} - -setup {* - Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of) -*} - -end diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Code_Evaluation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Code_Evaluation.thy Wed Sep 23 15:25:25 2009 +0200 @@ -0,0 +1,271 @@ +(* Title: HOL/Code_Evaluation.thy + Author: Florian Haftmann, TU Muenchen +*) + +header {* Term evaluation using the generic code generator *} + +theory Code_Evaluation +imports Plain Typerep Code_Numeral +begin + +subsection {* Term representation *} + +subsubsection {* Terms and class @{text term_of} *} + +datatype "term" = dummy_term + +definition Const :: "String.literal \ typerep \ term" where + "Const _ _ = dummy_term" + +definition App :: "term \ term \ term" where + "App _ _ = dummy_term" + +code_datatype Const App + +class term_of = typerep + + fixes term_of :: "'a \ term" + +lemma term_of_anything: "term_of x \ t" + by (rule eq_reflection) (cases "term_of x", cases t, simp) + +definition valapp :: "('a \ 'b) \ (unit \ term) + \ 'a \ (unit \ term) \ 'b \ (unit \ term)" where + "valapp f x = (fst f (fst x), \u. App (snd f ()) (snd x ()))" + +lemma valapp_code [code, code_unfold]: + "valapp (f, tf) (x, tx) = (f x, \u. App (tf ()) (tx ()))" + by (simp only: valapp_def fst_conv snd_conv) + + +subsubsection {* @{text term_of} instances *} + +instantiation "fun" :: (typerep, typerep) term_of +begin + +definition + "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') + [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" + +instance .. + +end + +setup {* +let + fun add_term_of tyco raw_vs thy = + let + val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; + val ty = Type (tyco, map TFree vs); + 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)); + fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst + o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) + |> snd + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) + end; + fun ensure_term_of (tyco, (raw_vs, _)) thy = + let + val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) + andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; + in if need_inst then add_term_of tyco raw_vs thy else thy end; +in + Code.type_interpretation ensure_term_of +end +*} + +setup {* +let + fun mk_term_of_eq thy ty vs tyco (c, tys) = + let + val t = list_comb (Const (c, tys ---> ty), + map Free (Name.names Name.context "a" tys)); + val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify) + (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) + val cty = Thm.ctyp_of thy ty; + in + @{thm term_of_anything} + |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] + |> Thm.varifyT + end; + fun add_term_of_code tyco raw_vs raw_cs thy = + let + val algebra = Sign.classes_of thy; + val vs = map (fn (v, sort) => + (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; + val ty = Type (tyco, map TFree vs); + val cs = (map o apsnd o map o map_atyps) + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + val eqs = map (mk_term_of_eq thy ty vs tyco) cs; + in + thy + |> Code.del_eqns const + |> fold Code.add_eqn eqs + end; + fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = + let + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; + in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; +in + Code.type_interpretation ensure_term_of_code +end +*} + + +subsubsection {* Code generator setup *} + +lemmas [code del] = term.recs term.cases term.size +lemma [code, code del]: "eq_class.eq (t1\term) t2 \ eq_class.eq t1 t2" .. + +lemma [code, code del]: "(term_of \ typerep \ term) = term_of" .. +lemma [code, code del]: "(term_of \ term \ term) = term_of" .. +lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. +lemma [code, code del]: + "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Evaluation.term) = Code_Evaluation.term_of" .. +lemma [code, code del]: + "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.seq \ Code_Evaluation.term) = Code_Evaluation.term_of" .. + +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c = + (let (n, m) = nibble_pair_of_char c + in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \ nibble \ char))) + (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" + by (subst term_of_anything) rule + +code_type "term" + (Eval "Term.term") + +code_const Const and App + (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") + +code_const "term_of \ String.literal \ term" + (Eval "HOLogic.mk'_message'_string") + +code_reserved Eval HOLogic + + +subsubsection {* Syntax *} + +definition termify :: "'a \ term" where + [code del]: "termify x = dummy_term" + +abbreviation valtermify :: "'a \ 'a \ (unit \ term)" where + "valtermify x \ (x, \u. termify x)" + +setup {* +let + fun map_default f xs = + let val ys = map f xs + in if exists is_some ys + then SOME (map2 the_default xs ys) + else NONE + end; + fun subst_termify_app (Const (@{const_name termify}, T), [t]) = + if not (Term.has_abs t) + then if fold_aterms (fn Const _ => I | _ => K false) t true + then SOME (HOLogic.reflect_term t) + else error "Cannot termify expression containing variables" + else error "Cannot termify expression containing abstraction" + | subst_termify_app (t, ts) = case map_default subst_termify ts + of SOME ts' => SOME (list_comb (t, ts')) + | NONE => NONE + and subst_termify (Abs (v, T, t)) = (case subst_termify t + of SOME t' => SOME (Abs (v, T, t')) + | NONE => NONE) + | subst_termify t = subst_termify_app (strip_comb t) + fun check_termify ts ctxt = map_default subst_termify ts + |> Option.map (rpair ctxt) +in + Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) +end; +*} + +locale term_syntax +begin + +notation App (infixl "<\>" 70) + and valapp (infixl "{\}" 70) + +end + +interpretation term_syntax . + +no_notation App (infixl "<\>" 70) + and valapp (infixl "{\}" 70) + + +subsection {* Numeric types *} + +definition term_of_num :: "'a\{semiring_div} \ 'a\{semiring_div} \ term" where + "term_of_num two = (\_. dummy_term)" + +lemma (in term_syntax) term_of_num_code [code]: + "term_of_num two k = (if k = 0 then termify Int.Pls + else (if k mod two = 0 + then termify Int.Bit0 <\> term_of_num two (k div two) + else termify Int.Bit1 <\> term_of_num two (k div two)))" + by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) + +lemma (in term_syntax) term_of_nat_code [code]: + "term_of (n::nat) = termify (number_of :: int \ nat) <\> term_of_num (2::nat) n" + by (simp only: term_of_anything) + +lemma (in term_syntax) term_of_int_code [code]: + "term_of (k::int) = (if k = 0 then termify (0 :: int) + else if k > 0 then termify (number_of :: int \ int) <\> term_of_num (2::int) k + else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> term_of_num (2::int) (- k)))" + by (simp only: term_of_anything) + +lemma (in term_syntax) term_of_code_numeral_code [code]: + "term_of (k::code_numeral) = termify (number_of :: int \ code_numeral) <\> term_of_num (2::code_numeral) k" + by (simp only: term_of_anything) + +subsection {* Obfuscate *} + +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 +*} + +hide const dummy_term App valapp +hide (open) const Const termify valtermify term_of term_of_num + + +subsection {* Evaluation setup *} + +ML {* +signature EVAL = +sig + val eval_ref: (unit -> term) option ref + val eval_term: theory -> term -> term +end; + +structure Eval : EVAL = +struct + +val eval_ref = ref (NONE : (unit -> term) option); + +fun eval_term thy t = + Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) []; + +end; +*} + +setup {* + Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of) +*} + +end diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/IsaMakefile Wed Sep 23 15:25:25 2009 +0200 @@ -210,7 +210,7 @@ MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ ATP_Linkup.thy \ - Code_Eval.thy \ + Code_Evaluation.thy \ Code_Numeral.thy \ Equiv_Relations.thy \ Groebner_Basis.thy \ diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Library/Code_Char.thy Wed Sep 23 15:25:25 2009 +0200 @@ -5,7 +5,7 @@ header {* Code generation of pretty characters (and strings) *} theory Code_Char -imports List Code_Eval Main +imports List Code_Evaluation Main begin code_type char @@ -32,7 +32,7 @@ (OCaml "!((_ : char) = _)") (Haskell infixl 4 "==") -code_const "Code_Eval.term_of \ char \ term" +code_const "Code_Evaluation.term_of \ char \ term" (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") end diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Library/Code_Integer.thy Wed Sep 23 15:25:25 2009 +0200 @@ -100,7 +100,7 @@ text {* Evaluation *} -code_const "Code_Eval.term_of \ int \ term" +code_const "Code_Evaluation.term_of \ int \ term" (Eval "HOLogic.mk'_number/ HOLogic.intT") end \ No newline at end of file diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Sep 23 15:25:25 2009 +0200 @@ -415,9 +415,9 @@ text {* Evaluation *} lemma [code, code del]: - "(Code_Eval.term_of \ nat \ term) = Code_Eval.term_of" .. + "(Code_Evaluation.term_of \ nat \ term) = Code_Evaluation.term_of" .. -code_const "Code_Eval.term_of \ nat \ term" +code_const "Code_Evaluation.term_of \ nat \ term" (SML "HOLogic.mk'_number/ HOLogic.natT") diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Library/Fin_Fun.thy --- a/src/HOL/Library/Fin_Fun.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Library/Fin_Fun.thy Wed Sep 23 15:25:25 2009 +0200 @@ -311,17 +311,17 @@ notation scomp (infixl "o\" 60) definition (in term_syntax) valtermify_finfun_const :: - "'b\typerep \ (unit \ Code_Eval.term) \ ('a\typerep \\<^isub>f 'b) \ (unit \ Code_Eval.term)" where - "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\} y" + "'b\typerep \ (unit \ Code_Evaluation.term) \ ('a\typerep \\<^isub>f 'b) \ (unit \ Code_Evaluation.term)" where + "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\} y" definition (in term_syntax) valtermify_finfun_update_code :: - "'a\typerep \ (unit \ Code_Eval.term) \ 'b\typerep \ (unit \ Code_Eval.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Eval.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Eval.term)" where - "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\} f {\} x {\} y" + "'a\typerep \ (unit \ Code_Evaluation.term) \ 'b\typerep \ (unit \ Code_Evaluation.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Evaluation.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Evaluation.term)" where + "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\} f {\} x {\} y" instantiation finfun :: (random, random) random begin -primrec random_finfun_aux :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where +primrec random_finfun_aux :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Evaluation.term)) \ Random.seed" where "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight [(1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Library/Nested_Environment.thy --- a/src/HOL/Library/Nested_Environment.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Library/Nested_Environment.thy Wed Sep 23 15:25:25 2009 +0200 @@ -567,6 +567,6 @@ qed simp_all lemma [code, code del]: - "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \ term) = Code_Eval.term_of" .. + "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \ term) = Code_Evaluation.term_of" .. end diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Quickcheck.thy Wed Sep 23 15:25:25 2009 +0200 @@ -3,7 +3,7 @@ header {* A simple counterexample generator *} theory Quickcheck -imports Random Code_Eval +imports Random Code_Evaluation uses ("Tools/quickcheck_generators.ML") begin @@ -24,7 +24,7 @@ definition "random i = Random.range 2 o\ - (\k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))" + (\k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" instance .. @@ -34,7 +34,7 @@ begin definition random_itself :: "code_numeral \ Random.seed \ ('a itself \ (unit \ term)) \ Random.seed" where - "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))" + "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" instance .. @@ -44,7 +44,7 @@ begin definition - "random _ = Random.select chars o\ (\c. Pair (c, \u. Code_Eval.term_of c))" + "random _ = Random.select chars o\ (\c. Pair (c, \u. Code_Evaluation.term_of c))" instance .. @@ -54,7 +54,7 @@ begin definition - "random _ = Pair (STR '''', \u. Code_Eval.term_of (STR ''''))" + "random _ = Pair (STR '''', \u. Code_Evaluation.term_of (STR ''''))" instance .. @@ -63,10 +63,10 @@ instantiation nat :: random begin -definition random_nat :: "code_numeral \ Random.seed \ (nat \ (unit \ Code_Eval.term)) \ Random.seed" where +definition random_nat :: "code_numeral \ Random.seed \ (nat \ (unit \ Code_Evaluation.term)) \ Random.seed" where "random_nat i = Random.range (i + 1) o\ (\k. Pair ( let n = Code_Numeral.nat_of k - in (n, \_. Code_Eval.term_of n)))" + in (n, \_. Code_Evaluation.term_of n)))" instance .. @@ -78,7 +78,7 @@ definition "random i = Random.range (2 * i + 1) o\ (\k. Pair ( let j = (if k \ i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k)) - in (j, \_. Code_Eval.term_of j)))" + in (j, \_. Code_Evaluation.term_of j)))" instance .. @@ -95,7 +95,7 @@ definition random_fun_lift :: "(Random.seed \ ('b \ (unit \ term)) \ Random.seed) \ Random.seed \ (('a\term_of \ 'b\typerep) \ (unit \ term)) \ Random.seed" where - "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed" + "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed" instantiation "fun" :: ("{eq, term_of}", random) random begin diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Rational.thy --- a/src/HOL/Rational.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Rational.thy Wed Sep 23 15:25:25 2009 +0200 @@ -1002,8 +1002,8 @@ by simp definition (in term_syntax) - valterm_fract :: "int \ (unit \ Code_Eval.term) \ int \ (unit \ Code_Eval.term) \ rat \ (unit \ Code_Eval.term)" where - [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\} k {\} l" + valterm_fract :: "int \ (unit \ Code_Evaluation.term) \ int \ (unit \ Code_Evaluation.term) \ rat \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\} k {\} l" notation fcomp (infixl "o>" 60) notation scomp (infixl "o\" 60) @@ -1014,7 +1014,7 @@ definition "Quickcheck.random i = Quickcheck.random i o\ (\num. Random.range i o\ (\denom. Pair ( let j = Code_Numeral.int_of (denom + 1) - in valterm_fract num (j, \u. Code_Eval.term_of j))))" + in valterm_fract num (j, \u. Code_Evaluation.term_of j))))" instance .. diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/RealDef.thy Wed Sep 23 15:25:25 2009 +0200 @@ -1128,8 +1128,8 @@ by (simp add: of_rat_divide) definition (in term_syntax) - valterm_ratreal :: "rat \ (unit \ Code_Eval.term) \ real \ (unit \ Code_Eval.term)" where - [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\} k" + valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" notation fcomp (infixl "o>" 60) notation scomp (infixl "o\" 60) diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Wed Sep 23 15:25:25 2009 +0200 @@ -613,17 +613,17 @@ | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep", Term.itselfT T --> typerepT) $ Logic.mk_type T; -val termT = Type ("Code_Eval.term", []); +val termT = Type ("Code_Evaluation.term", []); -fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT); +fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT); fun mk_term_of T t = term_of_const T $ t; fun reflect_term (Const (c, T)) = - Const ("Code_Eval.Const", literalT --> typerepT --> termT) + Const ("Code_Evaluation.Const", literalT --> typerepT --> termT) $ mk_literal c $ mk_typerep T | reflect_term (t1 $ t2) = - Const ("Code_Eval.App", termT --> termT --> termT) + Const ("Code_Evaluation.App", termT --> termT --> termT) $ reflect_term t1 $ reflect_term t2 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) | reflect_term t = t; @@ -631,7 +631,7 @@ fun mk_valtermify_app c vs T = let fun termifyT T = mk_prodT (T, unitT --> termT); - fun valapp T T' = Const ("Code_Eval.valapp", + fun valapp T T' = Const ("Code_Evaluation.valapp", termifyT (T --> T') --> termifyT T --> termifyT T'); fun mk_fTs [] _ = [] | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T; diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 23 15:25:25 2009 +0200 @@ -76,7 +76,7 @@ val lhs = HOLogic.mk_random T size; val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))] (HOLogic.mk_return Tm @{typ Random.seed} - (mk_const "Code_Eval.valapp" [T', T] + (mk_const "Code_Evaluation.valapp" [T', T] $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) @{typ Random.seed} (SOME Tm, @{typ Random.seed}); val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); diff -r 3bd9296b16ac -r 82956a3f0e0b src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Wed Sep 23 13:48:16 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Wed Sep 23 15:25:25 2009 +0200 @@ -169,7 +169,7 @@ end; fun dest_randomT (Type ("fun", [@{typ Random.seed}, - Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T + Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T | dest_randomT T = raise TYPE ("dest_randomT", [T], []) (* destruction of intro rules *) @@ -707,7 +707,7 @@ end; (* termify_code: -val termT = Type ("Code_Eval.term", []); +val termT = Type ("Code_Evaluation.term", []); fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT) *) (* @@ -1198,7 +1198,7 @@ val t1' = mk_valtermify_term t1 val t2' = mk_valtermify_term t2 in - Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2' + Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2' end | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term" *)