--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 21:37:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Aug 04 10:39:35 2010 +0200
@@ -400,7 +400,6 @@
(@{const_name "op -->"}, 2),
(@{const_name If}, 3),
(@{const_name Let}, 2),
- (@{const_name Unity}, 0),
(@{const_name Pair}, 2),
(@{const_name fst}, 1),
(@{const_name snd}, 1),
@@ -456,7 +455,7 @@
| unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
| unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
- Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts)
+ Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
| unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
| unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
| unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
@@ -512,7 +511,7 @@
| is_fun_type _ = false
fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
| is_set_type _ = false
-fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
+fun is_pair_type (Type (@{type_name prod}, _)) = true
| is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
| is_lfp_iterator_type _ = false
@@ -549,7 +548,7 @@
| strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
val nth_range_type = snd oo strip_n_binders
-fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
fold (Integer.add o num_factors_in_type) [T1, T2] 0
| num_factors_in_type _ = 1
fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
@@ -560,7 +559,7 @@
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T
fun mk_flat_tuple _ [t] = t
- | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) =
+ | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
| mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
fun dest_n_tuple 1 t = [t]
@@ -598,8 +597,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 Product_Type.prod}, @{type_name bool}, @{type_name unit},
- @{type_name int}, "Code_Numeral.code_numeral"] s orelse
+ member (op =) [@{type_name prod}, @{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 instantiate_type thy T1 T1' T2 =
@@ -795,7 +794,7 @@
Type (@{type_name fun}, _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
not (is_boolean_type (body_type T))
- | Type (@{type_name Product_Type.prod}, Ts) =>
+ | Type (@{type_name prod}, Ts) =>
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
((boxy = InExpr orelse boxy = InFunLHS) andalso
exists (is_boxing_worth_it hol_ctxt InPair)
@@ -815,12 +814,12 @@
else
box_type hol_ctxt (in_fun_lhs_for boxy) T1
--> box_type hol_ctxt (in_fun_rhs_for boxy) T2
- | Type (z as (@{type_name Product_Type.prod}, Ts)) =>
+ | Type (z as (@{type_name prod}, Ts)) =>
if boxy <> InConstr andalso boxy <> InSel
andalso should_box_type hol_ctxt boxy z then
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
else
- Type (@{type_name Product_Type.prod},
+ Type (@{type_name prod},
map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
@@ -982,7 +981,7 @@
Const (nth_sel_for_constr x n)
else
let
- fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ fun aux m (Type (@{type_name prod}, [T1, T2])) =
let
val (m, t1) = aux m T1
val (m, t2) = aux m T2
@@ -1072,7 +1071,7 @@
| (Type (new_s, new_Ts as [new_T1, new_T2]),
Type (old_s, old_Ts as [old_T1, old_T2])) =>
if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
+ old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
case constr_expand hol_ctxt old_T t of
Const (old_s, _) $ t1 =>
if new_s = @{type_name fun} then
@@ -1084,7 +1083,7 @@
(Type (@{type_name fun}, old_Ts)) t1]
| Const _ $ t1 $ t2 =>
construct_value ctxt stds
- (if new_s = @{type_name Product_Type.prod} then @{const_name Pair}
+ (if new_s = @{type_name prod} then @{const_name Pair}
else @{const_name PairBox}, new_Ts ---> new_T)
(map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
[t1, t2])
@@ -1095,12 +1094,11 @@
fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
- | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
card_of_type assigns T1 * card_of_type assigns T2
| card_of_type _ (Type (@{type_name itself}, _)) = 1
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
- | card_of_type _ @{typ unit} = 1
| card_of_type assigns T =
case AList.lookup (op =) assigns T of
SOME k => k
@@ -1116,7 +1114,7 @@
else Int.min (max, reasonable_power k2 k1)
end
| bounded_card_of_type max default_card assigns
- (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ (Type (@{type_name prod}, [T1, T2])) =
let
val k1 = bounded_card_of_type max default_card assigns T1
val k2 = bounded_card_of_type max default_card assigns T2
@@ -1146,7 +1144,7 @@
else if k1 >= max orelse k2 >= max then max
else Int.min (max, reasonable_power k2 k1)
end
- | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
+ | Type (@{type_name prod}, [T1, T2]) =>
let
val k1 = aux avoid T1
val k2 = aux avoid T2
@@ -1158,7 +1156,6 @@
| Type (@{type_name itself}, _) => 1
| @{typ prop} => 2
| @{typ bool} => 2
- | @{typ unit} => 1
| Type _ =>
(case datatype_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
@@ -1198,9 +1195,10 @@
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
+(* FIXME: detect "rep_datatype"? *)
fun is_funky_typedef_name thy s =
- member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum},
- @{type_name int}] s orelse
+ member (op =) [@{type_name unit}, @{type_name prod},
+ @{type_name Sum_Type.sum}, @{type_name int}] s orelse
is_frac_type thy (Type (s, []))
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
@@ -2088,7 +2086,7 @@
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
val set_T = tuple_T --> bool_T
val curried_T = tuple_T --> set_T
- val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T
+ val uncurried_T = Type (@{type_name prod}, [tuple_T, tuple_T]) --> bool_T
val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
@@ -2215,11 +2213,10 @@
fun aux T accum =
case T of
Type (@{type_name fun}, Ts) => fold aux Ts accum
- | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum
+ | Type (@{type_name prod}, Ts) => fold aux Ts accum
| Type (@{type_name itself}, [T1]) => aux T1 accum
| Type (_, Ts) =>
- if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
- T then
+ if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
accum
else
T :: accum