remove unreferenced identifiers
authorblanchet
Mon Sep 13 20:21:40 2010 +0200 (2010-09-13)
changeset 39345062c10ff848c
parent 39344 9de74cdcd833
child 39346 d837998f1e60
remove unreferenced identifiers
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Sep 13 20:21:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Sep 13 20:21:40 2010 +0200
     1.3 @@ -224,7 +224,9 @@
     1.4      fun pprint_v f = () |> verbose ? pprint o f
     1.5      fun pprint_d f = () |> debug ? pprint o f
     1.6      val print = pprint o curry Pretty.blk 0 o pstrs
     1.7 +(*
     1.8      val print_g = pprint o Pretty.str
     1.9 +*)
    1.10      val print_m = pprint_m o K o plazy
    1.11      val print_v = pprint_v o K o plazy
    1.12  
    1.13 @@ -552,9 +554,8 @@
    1.14                                       (plain_bounds @ sel_bounds) formula,
    1.15                                   main_j0 |> bits > 0 ? Integer.add (bits + 1))
    1.16          val (built_in_bounds, built_in_axioms) =
    1.17 -          bounds_and_axioms_for_built_in_rels_in_formulas debug ofs
    1.18 -              univ_card nat_card int_card main_j0
    1.19 -              (formula :: declarative_axioms)
    1.20 +          bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card
    1.21 +              nat_card int_card main_j0 (formula :: declarative_axioms)
    1.22          val bounds = built_in_bounds @ plain_bounds @ sel_bounds
    1.23                       |> not debug ? merge_bounds
    1.24          val axioms = built_in_axioms @ declarative_axioms
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 13 20:21:24 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 13 20:21:40 2010 +0200
     2.3 @@ -780,9 +780,11 @@
     2.4       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
     2.5    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
     2.6  fun rep_type_for_quot_type thy (T as Type (s, _)) =
     2.7 -  let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
     2.8 -    instantiate_type thy qtyp T rtyp
     2.9 -  end
    2.10 +    let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
    2.11 +      instantiate_type thy qtyp T rtyp
    2.12 +    end
    2.13 +  | rep_type_for_quot_type _ T =
    2.14 +    raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
    2.15  fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
    2.16      let
    2.17        val {qtyp, equiv_rel, equiv_thm, ...} =
    2.18 @@ -1083,7 +1085,7 @@
    2.19    | _ => t
    2.20  fun coerce_bound_0_in_term hol_ctxt new_T old_T =
    2.21    old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
    2.22 -and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
    2.23 +and coerce_term (hol_ctxt as {ctxt, stds, ...}) Ts new_T old_T t =
    2.24    if old_T = new_T then
    2.25      t
    2.26    else
    2.27 @@ -1960,7 +1962,7 @@
    2.28      |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
    2.29    end
    2.30  
    2.31 -fun codatatype_bisim_axioms (hol_ctxt as {thy, ctxt, stds, ...}) T =
    2.32 +fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
    2.33    let
    2.34      val xs = datatype_constrs hol_ctxt T
    2.35      val set_T = T --> bool_T
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Sep 13 20:21:24 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Sep 13 20:21:40 2010 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4    val sequential_int_bounds : int -> Kodkod.int_bound list
     3.5    val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
     3.6    val bounds_and_axioms_for_built_in_rels_in_formulas :
     3.7 -    bool -> int Typtab.table -> int -> int -> int -> int -> Kodkod.formula list
     3.8 +    bool -> int -> int -> int -> int -> Kodkod.formula list
     3.9      -> Kodkod.bound list * Kodkod.formula list
    3.10    val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
    3.11    val bound_for_sel_rel :
    3.12 @@ -130,7 +130,7 @@
    3.13  
    3.14  fun built_in_rels_in_formulas formulas =
    3.15    let
    3.16 -    fun rel_expr_func (KK.Rel (x as (n, j))) =
    3.17 +    fun rel_expr_func (KK.Rel (x as (_, j))) =
    3.18          (j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
    3.19           x <> signed_bit_word_sel_rel)
    3.20          ? insert (op =) x
    3.21 @@ -204,7 +204,7 @@
    3.22    else if m = 0 orelse n = 0 then (0, 1)
    3.23    else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
    3.24  
    3.25 -fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
    3.26 +fun tabulate_built_in_rel debug univ_card nat_card int_card j0
    3.27                            (x as (n, _)) =
    3.28    (check_arity "" univ_card n;
    3.29     if x = not3_rel then
    3.30 @@ -245,7 +245,7 @@
    3.31     else
    3.32       raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
    3.33  
    3.34 -fun bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0
    3.35 +fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0
    3.36                             (x as (n, j)) =
    3.37    if n = 2 andalso j <= suc_rels_base then
    3.38      let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
    3.39 @@ -258,8 +258,8 @@
    3.40      end
    3.41    else
    3.42      let
    3.43 -      val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card
    3.44 -                                             int_card main_j0 x
    3.45 +      val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
    3.46 +                                             main_j0 x
    3.47      in ([(x, nick)], [KK.TupleSet ts]) end
    3.48  
    3.49  fun axiom_for_built_in_rel (x as (n, j)) =
    3.50 @@ -274,10 +274,10 @@
    3.51      end
    3.52    else
    3.53      NONE
    3.54 -fun bounds_and_axioms_for_built_in_rels_in_formulas debug ofs univ_card nat_card
    3.55 +fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
    3.56                                                      int_card main_j0 formulas =
    3.57    let val rels = built_in_rels_in_formulas formulas in
    3.58 -    (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
    3.59 +    (map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0)
    3.60           rels,
    3.61       map_filter axiom_for_built_in_rel rels)
    3.62    end
    3.63 @@ -741,7 +741,7 @@
    3.64               KK.Iden)
    3.65  (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
    3.66     the first equation. *)
    3.67 -fun acyclicity_axioms_for_datatypes kk [_] = []
    3.68 +fun acyclicity_axioms_for_datatypes _ [_] = []
    3.69    | acyclicity_axioms_for_datatypes kk nfas =
    3.70      maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
    3.71  
    3.72 @@ -800,11 +800,11 @@
    3.73    | NONE => false
    3.74  
    3.75  fun sym_break_axioms_for_constr_pair hol_ctxt binarize
    3.76 -       (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
    3.77 -               kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
    3.78 +       (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
    3.79 +               kk_join, ...}) rel_table nfas dtypes
    3.80         (constr_ord,
    3.81          ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
    3.82 -         {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...})
    3.83 +         {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
    3.84          : constr_spec * constr_spec) =
    3.85    let
    3.86      val dataT = body_type T1
    3.87 @@ -1418,8 +1418,8 @@
    3.88            kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
    3.89          else
    3.90            to_rep (Func (R, Formula Neut)) u1
    3.91 -      | Op1 (First, T, R, u1) => to_nth_pair_sel 0 T R u1
    3.92 -      | Op1 (Second, T, R, u1) => to_nth_pair_sel 1 T R u1
    3.93 +      | Op1 (First, _, R, u1) => to_nth_pair_sel 0 R u1
    3.94 +      | Op1 (Second, _, R, u1) => to_nth_pair_sel 1 R u1
    3.95        | Op1 (Cast, _, R, u1) =>
    3.96          ((case rep_of u1 of
    3.97              Formula _ =>
    3.98 @@ -1685,7 +1685,7 @@
    3.99        | to_expr_assign (RelReg (j, _, R)) u =
   3.100          KK.AssignRelReg ((arity_of_rep R, j), to_r u)
   3.101        | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
   3.102 -    and to_atom (x as (k, j0)) u =
   3.103 +    and to_atom (x as (_, j0)) u =
   3.104        case rep_of u of
   3.105          Formula _ => atom_from_formula kk j0 (to_f u)
   3.106        | R => atom_from_rel_expr kk x R (to_r u)
   3.107 @@ -1727,7 +1727,7 @@
   3.108        rel_expr_from_rel_expr kk new_R old_R
   3.109                               (kk_project_seq r j0 (arity_of_rep old_R))
   3.110      and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us))
   3.111 -    and to_nth_pair_sel n res_T res_R u =
   3.112 +    and to_nth_pair_sel n res_R u =
   3.113        case u of
   3.114          Tuple (_, _, us) => to_rep res_R (nth us n)
   3.115        | _ => let
   3.116 @@ -1791,7 +1791,7 @@
   3.117                              [KK.IntEq (KK.IntReg 2,
   3.118                                         oper (KK.IntReg 0) (KK.IntReg 1))]))))
   3.119        end
   3.120 -    and to_apply (R as Formula _) func_u arg_u =
   3.121 +    and to_apply (R as Formula _) _ _ =
   3.122          raise REP ("Nitpick_Kodkod.to_apply", [R])
   3.123        | to_apply res_R func_u arg_u =
   3.124          case unopt_rep (rep_of func_u) of
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Sep 13 20:21:24 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Sep 13 20:21:40 2010 +0200
     4.3 @@ -904,18 +904,6 @@
     4.4      fun term_for_rep maybe_opt unfold =
     4.5        reconstruct_term maybe_opt unfold pool wacky_names scope atomss
     4.6                         sel_names rel_table bounds
     4.7 -    fun nth_value_of_type card T n =
     4.8 -      let
     4.9 -        fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
    4.10 -      in
    4.11 -        case aux false of
    4.12 -          t as Const (s, _) =>
    4.13 -          if String.isPrefix (cyclic_const_prefix ()) s then
    4.14 -            HOLogic.mk_eq (t, aux true)
    4.15 -          else
    4.16 -            t
    4.17 -        | t => t
    4.18 -      end
    4.19      val all_values =
    4.20        all_values_of_type pool wacky_names scope atomss sel_names rel_table
    4.21                           bounds
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Sep 13 20:21:24 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Sep 13 20:21:40 2010 +0200
     5.3 @@ -549,8 +549,7 @@
     5.4     consts = consts}
     5.5    handle List.Empty => initial_gamma (* FIXME: needed? *)
     5.6  
     5.7 -fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
     5.8 -                                          def_table, ...},
     5.9 +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...},
    5.10                               alpha_T, max_fresh, ...}) =
    5.11    let
    5.12      fun is_enough_eta_expanded t =
    5.13 @@ -617,7 +616,7 @@
    5.14            accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
    5.15                  |> do_term body_t ||> apfst pop_bound
    5.16          val bound_M = mtype_of_mterm bound_m
    5.17 -        val (M1, a, M2) = dest_MFun bound_M
    5.18 +        val (M1, a, _) = dest_MFun bound_M
    5.19        in
    5.20          (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
    5.21                 MAbs (abs_s, abs_T, M1, a,
    5.22 @@ -626,8 +625,7 @@
    5.23                                   MApp (bound_m, MRaw (Bound 0, M1))),
    5.24                             body_m))), accum)
    5.25        end
    5.26 -    and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
    5.27 -                             cset)) =
    5.28 +    and do_term t (accum as ({bound_Ts, bound_Ms, frees, consts}, cset)) =
    5.29          (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
    5.30                               Syntax.string_of_term ctxt t ^ " : _?");
    5.31           case t of
    5.32 @@ -787,8 +785,6 @@
    5.33               val (m2, accum) = do_term t2 accum
    5.34             in
    5.35               let
    5.36 -               val T11 = domain_type (fastype_of1 (bound_Ts, t1))
    5.37 -               val T2 = fastype_of1 (bound_Ts, t2)
    5.38                 val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
    5.39                 val M2 = mtype_of_mterm m2
    5.40               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
    5.41 @@ -867,7 +863,7 @@
    5.42               end
    5.43             | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    5.44               do_quantifier x s1 T1 t1
    5.45 -           | Const (x0 as (s0 as @{const_name Ex}, T0))
    5.46 +           | Const (x0 as (@{const_name Ex}, T0))
    5.47               $ (t1 as Abs (s1, T1, t1')) =>
    5.48               (case sn of
    5.49                  Plus => do_quantifier x0 s1 T1 t1'
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Sep 13 20:21:24 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Sep 13 20:21:40 2010 +0200
     6.3 @@ -982,7 +982,7 @@
     6.4               else if s = @{const_name TYPE} then
     6.5                 accum
     6.6               else case def_of_const thy def_table x of
     6.7 -               SOME def =>
     6.8 +               SOME _ =>
     6.9                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
    6.10                      accum
    6.11               | NONE =>
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Sep 13 20:21:24 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Sep 13 20:21:40 2010 +0200
     7.3 @@ -238,15 +238,14 @@
     7.4      Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
     7.5    | best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) =
     7.6      Struct (map (best_one_rep_for_type scope) Ts)
     7.7 -  | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
     7.8 +  | best_one_rep_for_type {card_assigns, ofs, ...} T =
     7.9      Atom (card_of_type card_assigns T, offset_of_type ofs T)
    7.10  
    7.11  fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
    7.12      Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
    7.13    | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
    7.14      opt_rep ofs T (best_one_rep_for_type scope T)
    7.15 -fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
    7.16 -                                  (Type (@{type_name fun}, [T1, T2])) =
    7.17 +fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
    7.18      (case (best_one_rep_for_type scope T1,
    7.19             best_non_opt_set_rep_for_type scope T2) of
    7.20         (R1, Atom (2, _)) => Func (R1, Formula Neut)