src/HOL/Tools/hologic.ML
changeset 31463 c5681ed50eab
parent 31456 55edadbd43d5
child 31736 926ebca5a145
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri Jun 05 08:28:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Fri Jun 05 09:23:41 2009 +0200
     1.3 @@ -122,8 +122,10 @@
     1.4    val mk_typerep: typ -> term
     1.5    val mk_term_of: typ -> term -> term
     1.6    val reflect_term: term -> term
     1.7 +  val mk_valtermify_app: string -> (string * typ) list -> typ -> term
     1.8    val mk_return: typ -> typ -> term -> term
     1.9    val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
    1.10 +  val mk_random: typ -> term -> term
    1.11  end;
    1.12  
    1.13  structure HOLogic: HOLOGIC =
    1.14 @@ -617,6 +619,19 @@
    1.15    | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
    1.16    | reflect_term t = t;
    1.17  
    1.18 +fun mk_valtermify_app c vs T =
    1.19 +  let
    1.20 +    fun termifyT T = mk_prodT (T, unitT --> termT);
    1.21 +    fun valapp T T' = Const ("Code_Eval.valapp",
    1.22 +      termifyT (T --> T') --> termifyT T --> termifyT T');
    1.23 +    fun mk_fTs [] _ = []
    1.24 +      | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
    1.25 +    val Ts = map snd vs;
    1.26 +    val t = Const (c, Ts ---> T);
    1.27 +    val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
    1.28 +    fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
    1.29 +  in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
    1.30 +
    1.31  
    1.32  (* open state monads *)
    1.33  
    1.34 @@ -633,4 +648,10 @@
    1.35              $ t $ t', U)
    1.36    in fold_rev mk_clause clauses (t, U) |> fst end;
    1.37  
    1.38 +val code_numeralT = Type ("Code_Numeral.code_numeral", []);
    1.39 +val random_seedT = mk_prodT (code_numeralT, code_numeralT);
    1.40 +
    1.41 +fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
    1.42 +  --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
    1.43 +
    1.44  end;