--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:17 2012 +0100
@@ -102,6 +102,8 @@
val is_number_type : Proof.context -> typ -> bool
val is_higher_order_type : typ -> bool
val elem_type : typ -> typ
+ val pseudo_domain_type : typ -> typ
+ val pseudo_range_type : typ -> typ
val const_for_iterator_type : typ -> styp
val strip_n_binders : int -> typ -> typ list * typ
val nth_range_type : int -> typ -> typ
@@ -382,6 +384,8 @@
(@{const_name Pair}, 2),
(@{const_name fst}, 1),
(@{const_name snd}, 1),
+ (@{const_name Set.member}, 2),
+ (@{const_name Collect}, 1),
(@{const_name Id}, 0),
(@{const_name converse}, 1),
(@{const_name trancl}, 1),
@@ -505,8 +509,13 @@
| is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
| is_higher_order_type _ = false
-fun elem_type (Type (@{type_name set}, [T])) = T
+fun elem_type (Type (@{type_name set}, [T'])) = T'
| elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
+fun pseudo_domain_type (Type (@{type_name fun}, [T1, _])) = T1
+ | pseudo_domain_type T = elem_type T
+fun pseudo_range_type (Type (@{type_name fun}, [_, T2])) = T2
+ | pseudo_range_type (Type (@{type_name set}, _)) = bool_T
+ | pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], [])
fun iterator_type_for_const gfp (s, T) =
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
@@ -575,8 +584,8 @@
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
fun is_basic_datatype thy stds s =
- member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int},
- "Code_Numeral.code_numeral"] s orelse
+ member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
+ @{type_name int}, "Code_Numeral.code_numeral"] s orelse
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
fun repair_constr_type ctxt body_T' T =
@@ -959,6 +968,8 @@
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
| card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
card_of_type assigns T1 * card_of_type assigns T2
+ | card_of_type assigns (Type (@{type_name set}, [T'])) =
+ reasonable_power 2 (card_of_type assigns T')
| card_of_type _ (Type (@{type_name itself}, _)) = 1
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
@@ -983,6 +994,9 @@
val k1 = bounded_card_of_type max default_card assigns T1
val k2 = bounded_card_of_type max default_card assigns T2
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
+ | bounded_card_of_type max default_card assigns
+ (Type (@{type_name set}, [T'])) =
+ bounded_card_of_type max default_card assigns (T' --> bool_T)
| bounded_card_of_type max default_card assigns T =
Int.min (max, if default_card = ~1 then
card_of_type assigns T
@@ -1016,6 +1030,7 @@
| (k1, k2) =>
if k1 >= max orelse k2 >= max then max
else Int.min (max, k1 * k2))
+ | Type (@{type_name set}, [T']) => aux avoid (T' --> bool_T)
| Type (@{type_name itself}, _) => 1
| @{typ prop} => 2
| @{typ bool} => 2
@@ -1256,7 +1271,7 @@
(* FIXME: detect "rep_datatype"? *)
fun is_funky_typedef_name ctxt s =
- member (op =) [@{type_name unit}, @{type_name prod},
+ member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
@{type_name Sum_Type.sum}, @{type_name int}] s orelse
is_frac_type ctxt (Type (s, []))
fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
@@ -2311,6 +2326,7 @@
case T of
Type (@{type_name fun}, Ts) => fold aux Ts accum
| Type (@{type_name prod}, Ts) => fold aux Ts accum
+ | Type (@{type_name set}, Ts) => fold aux Ts accum
| Type (@{type_name itself}, [T1]) => aux T1 accum
| Type (_, Ts) =>
if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
@@ -2323,7 +2339,6 @@
| xs => map snd xs)
| _ => insert (op =) T accum
in aux end
-
fun ground_types_in_type hol_ctxt binarize T =
add_ground_types hol_ctxt binarize T []
fun ground_types_in_terms hol_ctxt binarize ts =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
@@ -786,7 +786,7 @@
(to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
| Op2 (Subset, _, _, u1, u2) =>
let
- val dom_T = domain_type (type_of u1)
+ val dom_T = elem_type (type_of u1)
val R1 = rep_of u1
val R2 = rep_of u2
val (dom_R, ran_R) =
@@ -1060,7 +1060,7 @@
| Op1 (Finite, _, Opt (Atom _), _) => KK.None
| Op1 (Converse, T, R, u1) =>
let
- val (b_T, a_T) = HOLogic.dest_prodT (domain_type T)
+ val (b_T, a_T) = HOLogic.dest_prodT (elem_type T)
val (b_R, a_R) =
case R of
Func (Struct [R1, R2], _) => (R1, R2)
@@ -1191,8 +1191,8 @@
end
| Op2 (Composition, _, R, u1, u2) =>
let
- val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))
- val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u2))
+ val (a_T, b_T) = HOLogic.dest_prodT (elem_type (type_of u1))
+ val (_, c_T) = HOLogic.dest_prodT (elem_type (type_of u2))
val ab_k = card_of_domain_from_rep 2 (rep_of u1)
val bc_k = card_of_domain_from_rep 2 (rep_of u2)
val ac_k = card_of_domain_from_rep 2 R
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jan 03 18:33:17 2012 +0100
@@ -228,6 +228,8 @@
((T1, NONE), (T21, SOME T22))
| factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
+(* Term-encoded data structure for holding key-value pairs as well as an "opt"
+ flag indicating whether the function is approximated. *)
fun make_plain_fun maybe_opt T1 T2 =
let
fun aux T1 T2 [] =
@@ -268,55 +270,55 @@
| pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
-fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
- let
- fun do_curry T1 T1a T1b T2 t =
- let
- val (maybe_opt, tsp) = dest_plain_fun t
- val tps =
- tsp |>> map (break_in_two T1 T1a T1b)
- |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
- |> AList.coalesce (op =)
- |> map (apsnd (make_plain_fun maybe_opt T1b T2))
- in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
- and do_uncurry T1 T2 t =
- let
- val (maybe_opt, tsp) = dest_plain_fun t
- val tps =
- tsp |> op ~~
- |> maps (fn (t1, t2) =>
- multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
- in make_plain_fun maybe_opt T1 T2 tps end
- and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
- | do_arrow T1' T2' T1 T2
- (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
- Const (@{const_name fun_upd},
- (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
- $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
- | do_arrow _ _ _ _ t =
- raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
- and do_fun T1' T2' T1 T2 t =
- case factor_out_types T1' T1 of
- ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
- | ((_, NONE), (T1a, SOME T1b)) =>
- t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
- | ((T1a', SOME T1b'), (_, NONE)) =>
- t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
- | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
- and do_term (Type (@{type_name fun}, [T1', T2']))
- (Type (@{type_name fun}, [T1, T2])) t =
- do_fun T1' T2' T1 T2 t
- | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
- (Type (@{type_name prod}, [T1, T2]))
- (Const (@{const_name Pair}, _) $ t1 $ t2) =
- Const (@{const_name Pair}, Ts' ---> T')
- $ do_term T1' T1 t1 $ do_term T2' T2 t2
- | do_term T' T t =
- if T = T' then t
- else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
- in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
- | typecast_fun T' _ _ _ =
- raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
+fun format_fun T' T1 T2 t =
+ let
+ val T1' = pseudo_domain_type T'
+ val T2' = pseudo_range_type T'
+ fun do_curry T1 T1a T1b T2 t =
+ let
+ val (maybe_opt, tsp) = dest_plain_fun t
+ val tps =
+ tsp |>> map (break_in_two T1 T1a T1b)
+ |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
+ |> AList.coalesce (op =)
+ |> map (apsnd (make_plain_fun maybe_opt T1b T2))
+ in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
+ and do_uncurry T1 T2 t =
+ let
+ val (maybe_opt, tsp) = dest_plain_fun t
+ val tps =
+ tsp |> op ~~
+ |> maps (fn (t1, t2) =>
+ multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
+ in make_plain_fun maybe_opt T1 T2 tps end
+ and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
+ | do_arrow T1' T2' T1 T2
+ (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
+ Const (@{const_name fun_upd},
+ (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
+ $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
+ | do_arrow _ _ _ _ t =
+ raise TERM ("Nitpick_Model.format_fun.do_arrow", [t])
+ and do_fun T1' T2' T1 T2 t =
+ case factor_out_types T1' T1 of
+ ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
+ | ((_, NONE), (T1a, SOME T1b)) =>
+ t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
+ | ((T1a', SOME T1b'), (_, NONE)) =>
+ t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
+ | _ => raise TYPE ("Nitpick_Model.format_fun.do_fun", [T1, T1'], [])
+ and do_term (Type (@{type_name fun}, [T1', T2']))
+ (Type (@{type_name fun}, [T1, T2])) t =
+ do_fun T1' T2' T1 T2 t
+ | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
+ (Type (@{type_name prod}, [T1, T2]))
+ (Const (@{const_name Pair}, _) $ t1 $ t2) =
+ Const (@{const_name Pair}, Ts' ---> T')
+ $ do_term T1' T1 t1 $ do_term T2' T2 t2
+ | do_term T' T t =
+ if T = T' then t
+ else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
+ in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
fun truth_const_sort_key @{const True} = "0"
| truth_const_sort_key @{const False} = "2"
@@ -385,14 +387,14 @@
| postprocess_subterms Ts (Abs (s, T, t')) =
Abs (s, T, postprocess_subterms (T :: Ts) t')
| postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
- fun make_set maybe_opt T1 T2 tps =
+ fun make_set maybe_opt T tps =
let
- val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
- val insert_const = Const (@{const_name insert},
- T1 --> (T1 --> T2) --> T1 --> T2)
+ val empty_const = Const (@{const_abbrev Set.empty}, T --> bool_T)
+ val insert_const =
+ Const (@{const_name insert}, T --> (T --> bool_T) --> T --> bool_T)
fun aux [] =
- if maybe_opt andalso not (is_complete_type datatypes false T1) then
- insert_const $ Const (unrep (), T1) $ empty_const
+ if maybe_opt andalso not (is_complete_type datatypes false T) then
+ insert_const $ Const (unrep (), T) $ empty_const
else
empty_const
| aux ((t1, t2) :: zs) =
@@ -402,11 +404,11 @@
(insert_const
$ (t1 |> t2 <> @{const True}
? curry (op $)
- (Const (maybe_name, T1 --> T1))))
+ (Const (maybe_name, T --> T))))
in
if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
tps then
- Const (unknown, T1 --> T2)
+ Const (unknown, T --> bool_T)
else
aux tps
end
@@ -431,15 +433,7 @@
Type (@{type_name fun}, [T1, T2]) =>
if is_plain_fun t then
case T2 of
- @{typ bool} =>
- let
- val (maybe_opt, ts_pair) =
- dest_plain_fun t ||> pairself (map (polish_funs Ts))
- in
- make_set maybe_opt T1 T2
- (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
- end
- | Type (@{type_name option}, [T2']) =>
+ Type (@{type_name option}, [T2']) =>
let
val (maybe_opt, ts_pair) =
dest_plain_fun t ||> pairself (map (polish_funs Ts))
@@ -466,13 +460,19 @@
else
t
| t => t
- fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
- ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
- |> make_plain_fun maybe_opt T1 T2
- |> unarize_unbox_etc_term
- |> typecast_fun (uniterize_unarize_unbox_etc_type T')
- (uniterize_unarize_unbox_etc_type T1)
- (uniterize_unarize_unbox_etc_type T2)
+ fun make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 =
+ ts1 ~~ ts2
+ |> sort (nice_term_ord o pairself fst)
+ |> (case T of
+ Type (@{type_name set}, _) =>
+ sort_wrt (truth_const_sort_key o snd)
+ #> make_set maybe_opt T'
+ | _ =>
+ make_plain_fun maybe_opt T1 T2
+ #> unarize_unbox_etc_term
+ #> format_fun (uniterize_unarize_unbox_etc_type T')
+ (uniterize_unarize_unbox_etc_type T1)
+ (uniterize_unarize_unbox_etc_type T2))
fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
let
val k1 = card_of_type card_assigns T1
@@ -603,11 +603,16 @@
t
end
end
- and term_for_vect seen k R T1 T2 T' js =
- make_fun true T1 T2 T'
- (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
- (map (term_for_rep true seen T2 T2 R o single)
- (batch_list (arity_of_rep R) js))
+ and term_for_vect seen k R T T' js =
+ let
+ val T1 = pseudo_domain_type T
+ val T2 = pseudo_range_type T
+ in
+ make_fun_or_set true T T1 T2 T'
+ (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
+ (map (term_for_rep true seen T2 T2 R o single)
+ (batch_list (arity_of_rep R) js))
+ end
and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
@@ -621,29 +626,30 @@
map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
[[js1], [js2]])
end
- | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
- (Vect (k, R')) [js] =
- term_for_vect seen k R' T1 T2 T' js
- | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
- (Func (R1, Formula Neut)) jss =
+ | term_for_rep _ seen T T' (Vect (k, R')) [js] =
+ term_for_vect seen k R' T T' js
+ | term_for_rep maybe_opt seen T T' (Func (R1, Formula Neut)) jss =
let
+ val T1 = pseudo_domain_type T
+ val T2 = pseudo_range_type T
val jss1 = all_combinations_for_rep R1
val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
val ts2 =
map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
[[int_from_bool (member (op =) jss js)]])
jss1
- in make_fun maybe_opt T1 T2 T' ts1 ts2 end
- | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
- (Func (R1, R2)) jss =
+ in make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 end
+ | term_for_rep maybe_opt seen T T' (Func (R1, R2)) jss =
let
+ val T1 = pseudo_domain_type T
+ val T2 = pseudo_range_type T
val arity1 = arity_of_rep R1
val jss1 = all_combinations_for_rep R1
val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
o AList.lookup (op =) grouped_jss2) jss1
- in make_fun maybe_opt T1 T2 T' ts1 ts2 end
+ in make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 end
| term_for_rep _ seen T T' (Opt R) jss =
if null jss then Const (unknown, T)
else term_for_rep true seen T T' R jss
@@ -1045,11 +1051,13 @@
|> map_types (map_type_tfree
(fn (s, []) => TFree (s, HOLogic.typeS)
| x => TFree x))
- val _ = if debug then
- Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^
- " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
- else
- ()
+ val _ =
+ if debug then
+ (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
+ Syntax.string_of_term ctxt prop ^ "."
+ |> Output.urgent_message
+ else
+ ()
val goal = prop |> cterm_of thy |> Goal.init
in
(goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
@@ -745,7 +745,7 @@
<= length ts
| _ => true
val mtype_for = fresh_mtype_for_type mdata false
- fun mtype_for_set x T = MFun (mtype_for (elem_type T), V x, bool_M)
+ fun mtype_for_set x T = MFun (mtype_for (pseudo_domain_type T), V x, bool_M)
fun do_all T (gamma, cset) =
let
val abs_M = mtype_for (domain_type (domain_type T))
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:17 2012 +0100
@@ -457,7 +457,7 @@
val (ts', t2) = split_last ts
val t1 = list_comb (t0, ts')
val T1 = fastype_of1 (Ts, t1)
- in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
+ in Op2 (Apply, pseudo_range_type T1, Any, sub t1, sub t2) end
fun do_construct (x as (_, T)) ts =
case num_binder_types T - length ts of
0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
@@ -515,6 +515,8 @@
Op1 (First, range_type T, Any, sub t1)
| (Const (@{const_name snd}, T), [t1]) =>
Op1 (Second, range_type T, Any, sub t1)
+ | (Const (@{const_name Set.member}, _), [t1, t2]) => do_apply t2 [t1]
+ | (Const (@{const_name Collect}, _), [t1]) => sub t1
| (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
| (Const (@{const_name converse}, T), [t1]) =>
Op1 (Converse, range_type T, Any, sub t1)
@@ -558,16 +560,13 @@
Op2 (Less, bool_T, Any, sub t1, sub t2)
else
do_apply t0 ts
- | (Const (@{const_name ord_class.less_eq},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])),
- [t1, t2]) =>
- Op2 (Subset, bool_T, Any, sub t1, sub t2)
- (* FIXME: find out if this case is necessary *)
- | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
+ | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
ts as [t1, t2]) =>
if is_built_in_const thy stds x then
+ (* FIXME: find out if this case is necessary *)
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+ else if is_set_like_type (domain_type T) then
+ Op2 (Subset, bool_T, Any, sub t1, sub t2)
else
do_apply t0 ts
| (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Jan 03 18:33:17 2012 +0100
@@ -165,9 +165,13 @@
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, optable_rep ofs T2 R2)
+ | optable_rep ofs (Type (@{type_name set}, [T'])) R =
+ optable_rep ofs (T' --> bool_T) R
| optable_rep ofs T R = one_rep ofs T R
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, opt_rep ofs T2 R2)
+ | opt_rep ofs (Type (@{type_name set}, [T'])) R =
+ opt_rep ofs (T' --> bool_T) R
| opt_rep ofs T R = Opt (optable_rep ofs T R)
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
| unopt_rep (Opt R) = R
@@ -236,6 +240,8 @@
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
(Type (@{type_name fun}, [T1, T2])) =
Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
+ | best_one_rep_for_type scope (Type (@{type_name set}, [T'])) =
+ best_one_rep_for_type scope (T' --> bool_T)
| best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) =
Struct (map (best_one_rep_for_type scope) Ts)
| best_one_rep_for_type {card_assigns, ofs, ...} T =
@@ -243,6 +249,8 @@
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
+ | best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
+ best_opt_set_rep_for_type scope (T' --> bool_T)
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
opt_rep ofs T (best_one_rep_for_type scope T)
fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
@@ -250,6 +258,8 @@
best_non_opt_set_rep_for_type scope T2) of
(R1, Atom (2, _)) => Func (R1, Formula Neut)
| z => Func z)
+ | best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
+ best_non_opt_set_rep_for_type scope (T' --> bool_T)
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
fun best_set_rep_for_type (scope as {datatypes, ...}) T =
(if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
@@ -279,6 +289,8 @@
replicate_list k (type_schema_of_rep T2 R)
| type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
+ | type_schema_of_rep (Type (@{type_name set}, [T'])) R =
+ type_schema_of_rep (T' --> bool_T) R
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R
| type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jan 03 18:33:17 2012 +0100
@@ -114,6 +114,8 @@
is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
| is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
forall (is_complete_type dtypes facto) Ts
+ | is_complete_type dtypes facto (Type (@{type_name set}, [T'])) =
+ is_concrete_type dtypes facto T'
| is_complete_type dtypes facto T =
not (is_integer_like_type T) andalso not (is_bit_type T) andalso
fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
@@ -122,6 +124,8 @@
is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
| is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
forall (is_concrete_type dtypes facto) Ts
+ | is_concrete_type dtypes facto (Type (@{type_name set}, [T'])) =
+ is_complete_type dtypes facto T'
| is_concrete_type dtypes facto T =
fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
handle Option.Option => true