# HG changeset patch # User haftmann # Date 1242232898 -7200 # Node ID e2d777dcf1613d0f250ae00464dc0b4be41d4bfc # Parent 1a5591ecb764b1d2a75f5e27c5925f514d9ecf88 added abstract operations for typerep/term_of diff -r 1a5591ecb764 -r e2d777dcf161 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Wed May 13 18:41:36 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Wed May 13 18:41:38 2009 +0200 @@ -119,6 +119,9 @@ val message_stringT: typ val mk_message_string: string -> term val dest_message_string: term -> string + val mk_typerep: typ -> term + val mk_term_of: typ -> term -> term + val reflect_term: term -> term end; structure HOLogic: HOLOGIC = @@ -591,4 +594,26 @@ dest_string t | dest_message_string t = raise TERM ("dest_message_string", [t]); + +(* typerep and term *) + +val typerepT = Type ("Typerep.typerep", []); + +fun mk_typerep T = Const ("Typerep.typerep_class.typerep", + Term.itselfT T --> typerepT) $ Logic.mk_type T; + +val termT = Type ("Code_Eval.term", []); + +fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t; + +fun reflect_term (Const (c, T)) = + Const ("Code_Eval.Const", message_stringT --> typerepT --> termT) + $ mk_message_string c $ mk_typerep T + | reflect_term (t1 $ t2) = + Const ("Code_Eval.App", termT --> termT --> termT) + $ reflect_term t1 $ reflect_term t2 + | reflect_term (t as Free _) = t + | reflect_term (t as Bound _) = t + | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t); + end; diff -r 1a5591ecb764 -r e2d777dcf161 src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Wed May 13 18:41:36 2009 +0200 +++ b/src/HOL/ex/Quickcheck_Generators.thy Wed May 13 18:41:38 2009 +0200 @@ -54,7 +54,7 @@ val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); val c_indices = map (curry ( op + ) 1) t_indices; val c_t = list_comb (c, map Bound c_indices); - val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep + val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); val return = StateMonad.return (term_ty this_ty) @{typ seed}