# HG changeset patch # User blanchet # Date 1284402100 -7200 # Node ID 062c10ff848cd31dcadf7c7d63c316318555b422 # Parent 9de74cdcd833c7e3d00f5f2a01657d55d89369be remove unreferenced identifiers diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 () => " \ \ " ^ 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' diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 => diff -r 9de74cdcd833 -r 062c10ff848c src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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)