# 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;