--- a/src/HOL/Tools/smallvalue_generators.ML Wed Dec 15 17:46:45 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Wed Dec 15 17:46:46 2010 +0100
@@ -282,24 +282,33 @@
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
| make_set T1 ((t1, @{const False}) :: tps) = make_set T1 tps
- | make_set T1 ((t1, @{const True}) :: tps) = insert_const t1 (make_set T1 tps)
- | make_set T1 ((t1, _) :: tps) = raise TERM ("make_set", [t])
+ | make_set T1 ((t1, @{const True}) :: tps) =
+ Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
+ $ t1 $ (make_set T1 tps)
+ | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
| dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
+fun mk_fun_upd T1 T2 (t1, t2) t =
+ Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
+
fun dest_plain_fun t =
- case try (dest_fun_upd t) of
+ case try dest_fun_upd t of
NONE =>
- case t of
+ (case t of
(Abs (_, _, Const (@{const_name HOL.undefined}, _))) => []
- | _ => raise TERM ("dest_plain_fun", [t])
+ | _ => raise TERM ("dest_plain_fun", [t]))
| SOME (t0, (t1, t2)) => (t1, t2) :: dest_plain_fun t0
+fun make_plain_fun T1 T2 tps =
+ fold_rev (mk_fun_upd T1 T2) tps (absdummy (T1, Const ("_", T2)))
+
fun post_process_term t =
case fastype_of t of
- Type (@{type_name fun}, [T1, @{typ bool}]) =>
- dest_plain_fun t |> map (pairself post_process_term) |> make_set
+ Type (@{type_name fun}, [T1, T2]) =>
+ dest_plain_fun t |> map (pairself post_process_term) |>
+ (if T2 = @{typ bool} then rev #> make_set T1 else make_plain_fun T1 T2)
| _ => t
fun compile_generator_expr ctxt t =
@@ -312,7 +321,7 @@
(Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
in
- fn size => rpair NONE (compile size |> Option.map post_process_term)
+ fn size => rpair NONE (compile size |> Option.map (map post_process_term))
end;
(** setup **)