# HG changeset patch # User blanchet # Date 1325611997 -3600 # Node ID efeaa79f021b31a885b7a26a0b00f59989520f76 # Parent 1c436a920730b3b34c906ab9d27db40d4bbc0636 port part of Nitpick to "set" type constructor diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 = diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_model.ML --- 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)) diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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)) diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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) diff -r 1c436a920730 -r efeaa79f021b src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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