# HG changeset patch
# User haftmann
# Date 1244186621 -7200
# Node ID c5681ed50eab9c4a154f4bb2a39acf94b1a4ddad
# Parent  4fcbf17b5a98cd529843abbf0d86211c4b6fec4e
added mk_valtermify_app and mk_random

diff -r 4fcbf17b5a98 -r c5681ed50eab src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Jun 05 08:28:24 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri Jun 05 09:23:41 2009 +0200
@@ -122,8 +122,10 @@
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
+  val mk_valtermify_app: string -> (string * typ) list -> typ -> term
   val mk_return: typ -> typ -> term -> term
   val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
+  val mk_random: typ -> term -> term
 end;
 
 structure HOLogic: HOLOGIC =
@@ -617,6 +619,19 @@
   | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   | reflect_term t = t;
 
+fun mk_valtermify_app c vs T =
+  let
+    fun termifyT T = mk_prodT (T, unitT --> termT);
+    fun valapp T T' = Const ("Code_Eval.valapp",
+      termifyT (T --> T') --> termifyT T --> termifyT T');
+    fun mk_fTs [] _ = []
+      | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
+    val Ts = map snd vs;
+    val t = Const (c, Ts ---> T);
+    val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
+    fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
+  in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
+
 
 (* open state monads *)
 
@@ -633,4 +648,10 @@
             $ t $ t', U)
   in fold_rev mk_clause clauses (t, U) |> fst end;
 
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
+val random_seedT = mk_prodT (code_numeralT, code_numeralT);
+
+fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
+  --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
+
 end;