--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Sep 13 20:21:40 2010 +0200
@@ -224,7 +224,9 @@
fun pprint_v f = () |> verbose ? pprint o f
fun pprint_d f = () |> debug ? pprint o f
val print = pprint o curry Pretty.blk 0 o pstrs
+(*
val print_g = pprint o Pretty.str
+*)
val print_m = pprint_m o K o plazy
val print_v = pprint_v o K o plazy
@@ -552,9 +554,8 @@
(plain_bounds @ sel_bounds) formula,
main_j0 |> bits > 0 ? Integer.add (bits + 1))
val (built_in_bounds, built_in_axioms) =
- bounds_and_axioms_for_built_in_rels_in_formulas debug ofs
- univ_card nat_card int_card main_j0
- (formula :: declarative_axioms)
+ bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card
+ nat_card int_card main_j0 (formula :: declarative_axioms)
val bounds = built_in_bounds @ plain_bounds @ sel_bounds
|> not debug ? merge_bounds
val axioms = built_in_axioms @ declarative_axioms
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 13 20:21:40 2010 +0200
@@ -780,9 +780,11 @@
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
fun rep_type_for_quot_type thy (T as Type (s, _)) =
- let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
- instantiate_type thy qtyp T rtyp
- end
+ let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
+ instantiate_type thy qtyp T rtyp
+ end
+ | rep_type_for_quot_type _ T =
+ raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
val {qtyp, equiv_rel, equiv_thm, ...} =
@@ -1083,7 +1085,7 @@
| _ => t
fun coerce_bound_0_in_term hol_ctxt new_T old_T =
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, stds, ...}) Ts new_T old_T t =
if old_T = new_T then
t
else
@@ -1960,7 +1962,7 @@
|> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
end
-fun codatatype_bisim_axioms (hol_ctxt as {thy, ctxt, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Sep 13 20:21:40 2010 +0200
@@ -23,7 +23,7 @@
val sequential_int_bounds : int -> Kodkod.int_bound list
val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
val bounds_and_axioms_for_built_in_rels_in_formulas :
- bool -> int Typtab.table -> int -> int -> int -> int -> Kodkod.formula list
+ bool -> int -> int -> int -> int -> Kodkod.formula list
-> Kodkod.bound list * Kodkod.formula list
val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
val bound_for_sel_rel :
@@ -130,7 +130,7 @@
fun built_in_rels_in_formulas formulas =
let
- fun rel_expr_func (KK.Rel (x as (n, j))) =
+ fun rel_expr_func (KK.Rel (x as (_, j))) =
(j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
x <> signed_bit_word_sel_rel)
? insert (op =) x
@@ -204,7 +204,7 @@
else if m = 0 orelse n = 0 then (0, 1)
else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
-fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
+fun tabulate_built_in_rel debug univ_card nat_card int_card j0
(x as (n, _)) =
(check_arity "" univ_card n;
if x = not3_rel then
@@ -245,7 +245,7 @@
else
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
-fun bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0
+fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0
(x as (n, j)) =
if n = 2 andalso j <= suc_rels_base then
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
@@ -258,8 +258,8 @@
end
else
let
- val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card
- int_card main_j0 x
+ val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
+ main_j0 x
in ([(x, nick)], [KK.TupleSet ts]) end
fun axiom_for_built_in_rel (x as (n, j)) =
@@ -274,10 +274,10 @@
end
else
NONE
-fun bounds_and_axioms_for_built_in_rels_in_formulas debug ofs univ_card nat_card
+fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
int_card main_j0 formulas =
let val rels = built_in_rels_in_formulas formulas in
- (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
+ (map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0)
rels,
map_filter axiom_for_built_in_rel rels)
end
@@ -741,7 +741,7 @@
KK.Iden)
(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
the first equation. *)
-fun acyclicity_axioms_for_datatypes kk [_] = []
+fun acyclicity_axioms_for_datatypes _ [_] = []
| acyclicity_axioms_for_datatypes kk nfas =
maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
@@ -800,11 +800,11 @@
| NONE => false
fun sym_break_axioms_for_constr_pair hol_ctxt binarize
- (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
- kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
+ (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
+ kk_join, ...}) rel_table nfas dtypes
(constr_ord,
({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
- {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...})
+ {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
: constr_spec * constr_spec) =
let
val dataT = body_type T1
@@ -1418,8 +1418,8 @@
kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
else
to_rep (Func (R, Formula Neut)) u1
- | Op1 (First, T, R, u1) => to_nth_pair_sel 0 T R u1
- | Op1 (Second, T, R, u1) => to_nth_pair_sel 1 T R u1
+ | Op1 (First, _, R, u1) => to_nth_pair_sel 0 R u1
+ | Op1 (Second, _, R, u1) => to_nth_pair_sel 1 R u1
| Op1 (Cast, _, R, u1) =>
((case rep_of u1 of
Formula _ =>
@@ -1685,7 +1685,7 @@
| to_expr_assign (RelReg (j, _, R)) u =
KK.AssignRelReg ((arity_of_rep R, j), to_r u)
| to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
- and to_atom (x as (k, j0)) u =
+ and to_atom (x as (_, j0)) u =
case rep_of u of
Formula _ => atom_from_formula kk j0 (to_f u)
| R => atom_from_rel_expr kk x R (to_r u)
@@ -1727,7 +1727,7 @@
rel_expr_from_rel_expr kk new_R old_R
(kk_project_seq r j0 (arity_of_rep old_R))
and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us))
- and to_nth_pair_sel n res_T res_R u =
+ and to_nth_pair_sel n res_R u =
case u of
Tuple (_, _, us) => to_rep res_R (nth us n)
| _ => let
@@ -1791,7 +1791,7 @@
[KK.IntEq (KK.IntReg 2,
oper (KK.IntReg 0) (KK.IntReg 1))]))))
end
- and to_apply (R as Formula _) func_u arg_u =
+ and to_apply (R as Formula _) _ _ =
raise REP ("Nitpick_Kodkod.to_apply", [R])
| to_apply res_R func_u arg_u =
case unopt_rep (rep_of func_u) of
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Sep 13 20:21:40 2010 +0200
@@ -904,18 +904,6 @@
fun term_for_rep maybe_opt unfold =
reconstruct_term maybe_opt unfold pool wacky_names scope atomss
sel_names rel_table bounds
- fun nth_value_of_type card T n =
- let
- fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
- in
- case aux false of
- t as Const (s, _) =>
- if String.isPrefix (cyclic_const_prefix ()) s then
- HOLogic.mk_eq (t, aux true)
- else
- t
- | t => t
- end
val all_values =
all_values_of_type pool wacky_names scope atomss sel_names rel_table
bounds
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Sep 13 20:21:40 2010 +0200
@@ -549,8 +549,7 @@
consts = consts}
handle List.Empty => initial_gamma (* FIXME: needed? *)
-fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
- def_table, ...},
+fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...},
alpha_T, max_fresh, ...}) =
let
fun is_enough_eta_expanded t =
@@ -617,7 +616,7 @@
accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
|> do_term body_t ||> apfst pop_bound
val bound_M = mtype_of_mterm bound_m
- val (M1, a, M2) = dest_MFun bound_M
+ val (M1, a, _) = dest_MFun bound_M
in
(MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
MAbs (abs_s, abs_T, M1, a,
@@ -626,8 +625,7 @@
MApp (bound_m, MRaw (Bound 0, M1))),
body_m))), accum)
end
- and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
- cset)) =
+ and do_term t (accum as ({bound_Ts, bound_Ms, frees, consts}, cset)) =
(trace_msg (fn () => " \<Gamma> \<turnstile> " ^
Syntax.string_of_term ctxt t ^ " : _?");
case t of
@@ -787,8 +785,6 @@
val (m2, accum) = do_term t2 accum
in
let
- val T11 = domain_type (fastype_of1 (bound_Ts, t1))
- val T2 = fastype_of1 (bound_Ts, t2)
val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
val M2 = mtype_of_mterm m2
in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
@@ -867,7 +863,7 @@
end
| Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
do_quantifier x s1 T1 t1
- | Const (x0 as (s0 as @{const_name Ex}, T0))
+ | Const (x0 as (@{const_name Ex}, T0))
$ (t1 as Abs (s1, T1, t1')) =>
(case sn of
Plus => do_quantifier x0 s1 T1 t1'
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Sep 13 20:21:40 2010 +0200
@@ -982,7 +982,7 @@
else if s = @{const_name TYPE} then
accum
else case def_of_const thy def_table x of
- SOME def =>
+ SOME _ =>
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
accum
| NONE =>
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Sep 13 20:21:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Sep 13 20:21:40 2010 +0200
@@ -238,15 +238,14 @@
Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
| 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, datatypes, ofs, ...} T =
+ | best_one_rep_for_type {card_assigns, ofs, ...} T =
Atom (card_of_type card_assigns T, offset_of_type ofs T)
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 as {ofs, ...}) T =
opt_rep ofs T (best_one_rep_for_type scope T)
-fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
- (Type (@{type_name fun}, [T1, T2])) =
+fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
(case (best_one_rep_for_type scope T1,
best_non_opt_set_rep_for_type scope T2) of
(R1, Atom (2, _)) => Func (R1, Formula Neut)