added abstract operations for typerep/term_of
authorhaftmann
Wed May 13 18:41:38 2009 +0200 (2009-05-13)
changeset 31135e2d777dcf161
parent 31134 1a5591ecb764
child 31136 85d04515abb3
added abstract operations for typerep/term_of
src/HOL/Tools/hologic.ML
src/HOL/ex/Quickcheck_Generators.thy
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed May 13 18:41:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed May 13 18:41:38 2009 +0200
     1.3 @@ -119,6 +119,9 @@
     1.4    val message_stringT: typ
     1.5    val mk_message_string: string -> term
     1.6    val dest_message_string: term -> string
     1.7 +  val mk_typerep: typ -> term
     1.8 +  val mk_term_of: typ -> term -> term
     1.9 +  val reflect_term: term -> term
    1.10  end;
    1.11  
    1.12  structure HOLogic: HOLOGIC =
    1.13 @@ -591,4 +594,26 @@
    1.14        dest_string t
    1.15    | dest_message_string t = raise TERM ("dest_message_string", [t]);
    1.16  
    1.17 +
    1.18 +(* typerep and term *)
    1.19 +
    1.20 +val typerepT = Type ("Typerep.typerep", []);
    1.21 +
    1.22 +fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
    1.23 +  Term.itselfT T --> typerepT) $ Logic.mk_type T;
    1.24 +
    1.25 +val termT = Type ("Code_Eval.term", []);
    1.26 +
    1.27 +fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
    1.28 +
    1.29 +fun reflect_term (Const (c, T)) =
    1.30 +      Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
    1.31 +        $ mk_message_string c $ mk_typerep T
    1.32 +  | reflect_term (t1 $ t2) =
    1.33 +      Const ("Code_Eval.App", termT --> termT --> termT)
    1.34 +        $ reflect_term t1 $ reflect_term t2
    1.35 +  | reflect_term (t as Free _) = t
    1.36 +  | reflect_term (t as Bound _) = t
    1.37 +  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
    1.38 +
    1.39  end;
     2.1 --- a/src/HOL/ex/Quickcheck_Generators.thy	Wed May 13 18:41:36 2009 +0200
     2.2 +++ b/src/HOL/ex/Quickcheck_Generators.thy	Wed May 13 18:41:38 2009 +0200
     2.3 @@ -54,7 +54,7 @@
     2.4        val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
     2.5        val c_indices = map (curry ( op + ) 1) t_indices;
     2.6        val c_t = list_comb (c, map Bound c_indices);
     2.7 -      val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
     2.8 +      val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term
     2.9          (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    2.10          |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    2.11        val return = StateMonad.return (term_ty this_ty) @{typ seed}