--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 11:57:33 2010 +0100
@@ -7,7 +7,6 @@
signature NITPICK_NUT =
sig
- type special_fun = Nitpick_HOL.special_fun
type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
@@ -467,7 +466,7 @@
| factorize z = [z]
(* hol_context -> op2 -> term -> nut *)
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -518,11 +517,21 @@
val t1 = list_comb (t0, ts')
val T1 = fastype_of1 (Ts, t1)
in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
+ (* styp -> term list -> term *)
+ fun construct (x as (_, T)) ts =
+ case num_binder_types T - length ts of
+ 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
+ o nth_sel_for_constr x)
+ (~1 upto num_sels_for_constr_type T - 1),
+ body_type T, Any,
+ ts |> map (`(curry fastype_of1 Ts))
+ |> maps factorize |> map (sub o snd))
+ | k => sub (eta_expand Ts t k)
in
case strip_comb t of
(Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
do_quantifier All s T t1
- | (t0 as Const (@{const_name all}, T), [t1]) =>
+ | (t0 as Const (@{const_name all}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
| (Const (@{const_name "==>"}, _), [t1, t2]) =>
@@ -538,11 +547,11 @@
| (Const (@{const_name True}, T), []) => Cst (True, T, Any)
| (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
do_quantifier All s T t1
- | (t0 as Const (@{const_name All}, T), [t1]) =>
+ | (t0 as Const (@{const_name All}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
do_quantifier Exist s T t1
- | (t0 as Const (@{const_name Ex}, T), [t1]) =>
+ | (t0 as Const (@{const_name Ex}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (t0 as Const (@{const_name The}, T), [t1]) =>
if fast_descrs then
@@ -568,7 +577,7 @@
| (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
sub t1, sub_abs s T' t2)
- | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
+ | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
sub (t0 $ t1 $ eta_expand Ts t2 1)
| (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
| (Const (@{const_name Pair}, T), [t1, t2]) =>
@@ -595,7 +604,10 @@
Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
| (Const (@{const_name image}, T), [t1, t2]) =>
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
- | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
+ | (Const (x as (s as @{const_name Suc}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Suc, T, Any)
+ else if is_constr thy stds x then construct x []
+ else ConstName (s, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
(if is_finite_type hol_ctxt (domain_type T) then
Cst (True, bool_T, Any)
@@ -604,14 +616,9 @@
| _ => Op1 (Finite, bool_T, Any, sub t1))
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
| (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
- if is_built_in_const thy stds false x then
- Cst (Num 0, T, Any)
- else if is_constr thy stds x then
- let val (s', T') = discr_for_constr x in
- Construct ([ConstName (s', T', Any)], T, Any, [])
- end
- else
- ConstName (s, T, Any)
+ if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
+ else if is_constr thy stds x then construct x []
+ else ConstName (s, T, Any)
| (Const (x as (s as @{const_name one_class.one}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
else ConstName (s, T, Any)
@@ -631,7 +638,7 @@
| (Const (x as (s as @{const_name div_class.div}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Divide, T, Any)
else ConstName (s, T, Any)
- | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
+ | (t0 as Const (x as (@{const_name ord_class.less}, _)),
ts as [t1, t2]) =>
if is_built_in_const thy stds false x then
Op2 (Less, bool_T, Any, sub t1, sub t2)
@@ -642,7 +649,7 @@
[t1, t2]) =>
Op2 (Subset, bool_T, Any, sub t1, sub t2)
(* FIXME: find out if this case is necessary *)
- | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
+ | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
ts as [t1, t2]) =>
if is_built_in_const thy stds false x then
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
@@ -660,7 +667,7 @@
else
ConstName (s, T, Any)
| (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
- | (Const (@{const_name is_unknown}, T), [t1]) =>
+ | (Const (@{const_name is_unknown}, _), [t1]) =>
Op1 (IsUnknown, bool_T, Any, sub t1)
| (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
Op1 (Tha, T2, Any, sub t1)
@@ -681,14 +688,7 @@
Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
if is_constr thy stds x then
- case num_binder_types T - length ts of
- 0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
- o nth_sel_for_constr x)
- (~1 upto num_sels_for_constr_type T - 1),
- body_type T, Any,
- ts |> map (`(curry fastype_of1 Ts))
- |> maps factorize |> map (sub o snd))
- | k => sub (eta_expand Ts t k)
+ construct x ts
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
else
@@ -726,8 +726,8 @@
in (v :: vs, NameTable.update (v, R) table) end
(* scope -> bool -> nut -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
- ofs, ...}) all_exact v (vs, table) =
+fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+ (vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
val R = (if is_abs_fun thy x then
@@ -904,8 +904,7 @@
| untuple f u = if rep_of u = Unit then [] else [f u]
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
-fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
- bits, datatypes, ofs, ...})
+fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
unsound table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
@@ -991,7 +990,7 @@
Cst (cst, T, best_set_rep_for_type scope T)
| Op1 (Not, T, _, u1) =>
(case gsub def (flip_polarity polar) u1 of
- Op2 (Triad, T, R, u11, u12) =>
+ Op2 (Triad, T, _, u11, u12) =>
triad (s_op1 Not T (Formula Pos) u12)
(s_op1 Not T (Formula Neg) u11)
| u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
@@ -1138,7 +1137,7 @@
else
unopt_rep R
in s_op2 Lambda T R u1' u2' end
- | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
+ | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
| Op2 (oper, T, _, u1, u2) =>
if oper = All orelse oper = Exist then
let
@@ -1307,7 +1306,7 @@
end
| shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
- | shape_tuple T R [u] =
+ | shape_tuple T _ [u] =
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
| shape_tuple T Unit [] = Cst (Unity, T, Unit)
| shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
@@ -1390,7 +1389,6 @@
let
val bs = untuple I u1
val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
- val u11 = rename_vars_in_nut pool table' u1
in
Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
rename_vars_in_nut pool table u2,