--- a/src/HOL/Tools/smallvalue_generators.ML Fri Mar 11 08:12:55 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Fri Mar 11 08:12:58 2011 +0100
@@ -306,12 +306,11 @@
case try dest_fun_upd t of
NONE =>
(case t of
- (Abs (_, _, Const (@{const_name HOL.undefined}, _))) => []
+ Abs (_, _, _) => ([], t)
| _ => raise TERM ("dest_plain_fun", [t]))
- | SOME (t0, (t1, t2)) => (t1, t2) :: dest_plain_fun t0
+ | SOME (t0, (t1, t2)) => apfst (cons (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 make_plain_fun T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
| make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
@@ -320,23 +319,48 @@
$ t1 $ (make_set T1 tps)
| make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
+fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
+ | make_coset T tps =
+ let
+ val U = T --> @{typ bool}
+ fun invert @{const False} = @{const True}
+ | invert @{const True} = @{const False}
+ in
+ Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
+ $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
+ end
+
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
| make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
| make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
fun post_process_term t =
- case fastype_of t of
- Type (@{type_name fun}, [T1, T2]) =>
- (case try dest_plain_fun t of
- SOME tps =>
- tps
- |> map (pairself post_process_term)
- |> (case T2 of
- @{typ bool} => rev #> make_set T1
- | Type (@{type_name option}, _) => make_map T1 T2
- | _ => make_plain_fun T1 T2)
- | NONE => t)
- | _ => t
+ let
+ (*val _ = tracing ("post_process:" ^ Syntax.string_of_term ctxt t)*)
+ fun map_Abs f t =
+ case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t])
+ fun process_args t = case strip_comb t of
+ (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
+ in
+ case fastype_of t of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case try dest_plain_fun t of
+ SOME (tps, t) =>
+ (map (pairself post_process_term) tps, map_Abs post_process_term t)
+ |> (case T2 of
+ @{typ bool} =>
+ (case t of
+ Abs(_, _, @{const True}) => fst #> rev #> make_set T1
+ | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
+ | _ => raise TERM ("post_process_term", [t]))
+ | Type (@{type_name option}, _) =>
+ (case t of
+ Abs(_, _, Const(@{const_name None}, _)) => fst #> (make_map T1 T2)
+ | _ => make_plain_fun T1 T2)
+ | _ => make_plain_fun T1 T2)
+ | NONE => raise TERM ("post_process_term", [t]))
+ | _ => process_args t
+ end
(** generator compiliation **)