--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:44 2010 +0200
@@ -454,7 +454,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 "*"}, map unarize_unbox_etc_type Ts)
+ Type (@{type_name Product_Type.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 _ :: _)) =
@@ -509,7 +509,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 "*"}, _)) = true
+fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
| is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
| is_lfp_iterator_type _ = false
@@ -546,7 +546,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 "*"}, [T1, T2])) =
+fun num_factors_in_type (Type (@{type_name Product_Type.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])) =
@@ -557,7 +557,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 "*"}, [T1, T2])) (t :: ts) =
+ | mk_flat_tuple (Type (@{type_name Product_Type.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]
@@ -595,7 +595,7 @@
(* 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 "*"}, @{type_name bool}, @{type_name unit},
+ member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit},
@{type_name int}, "Code_Numeral.code_numeral"] s orelse
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
@@ -792,7 +792,7 @@
Type (@{type_name fun}, _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
not (is_boolean_type (body_type T))
- | Type (@{type_name "*"}, Ts) =>
+ | Type (@{type_name Product_Type.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)
@@ -812,12 +812,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 "*"}, Ts)) =>
+ | Type (z as (@{type_name Product_Type.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 "*"},
+ Type (@{type_name Product_Type.prod},
map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
@@ -979,7 +979,7 @@
Const (nth_sel_for_constr x n)
else
let
- fun aux m (Type (@{type_name "*"}, [T1, T2])) =
+ fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
let
val (m, t1) = aux m T1
val (m, t2) = aux m T2
@@ -1069,7 +1069,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 "*"} then
+ old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
case constr_expand hol_ctxt old_T t of
Const (old_s, _) $ t1 =>
if new_s = @{type_name fun} then
@@ -1081,7 +1081,7 @@
(Type (@{type_name fun}, old_Ts)) t1]
| Const _ $ t1 $ t2 =>
construct_value ctxt stds
- (if new_s = @{type_name "*"} then @{const_name Pair}
+ (if new_s = @{type_name Product_Type.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])
@@ -1092,7 +1092,7 @@
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 "*"}, [T1, T2])) =
+ | card_of_type assigns (Type (@{type_name Product_Type.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
@@ -1113,7 +1113,7 @@
else Int.min (max, reasonable_power k2 k1)
end
| bounded_card_of_type max default_card assigns
- (Type (@{type_name "*"}, [T1, T2])) =
+ (Type (@{type_name Product_Type.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
@@ -1143,7 +1143,7 @@
else if k1 >= max orelse k2 >= max then max
else Int.min (max, reasonable_power k2 k1)
end
- | Type (@{type_name "*"}, [T1, T2]) =>
+ | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
let
val k1 = aux avoid T1
val k2 = aux avoid T2
@@ -1196,7 +1196,7 @@
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
fun is_funky_typedef_name thy s =
- member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
+ member (op =) [@{type_name unit}, @{type_name Product_Type.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
@@ -2066,7 +2066,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 "*"}, [tuple_T, tuple_T]) --> bool_T
+ val uncurried_T = Type (@{type_name Product_Type.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)
@@ -2185,7 +2185,7 @@
fun aux T accum =
case T of
Type (@{type_name fun}, Ts) => fold aux Ts accum
- | Type (@{type_name "*"}, Ts) => fold aux Ts accum
+ | Type (@{type_name Product_Type.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)