1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 22 10:28:49 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 22 11:57:33 2010 +0100
1.3 @@ -465,7 +465,7 @@
1.4 | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
1.5 | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
1.6 | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
1.7 - | arity_of_rel_expr (Project (r, is)) = length is
1.8 + | arity_of_rel_expr (Project (_, is)) = length is
1.9 | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
1.10 | arity_of_rel_expr (Closure _) = 2
1.11 | arity_of_rel_expr (ReflexiveClosure _) = 2
1.12 @@ -590,8 +590,8 @@
1.13 (case tuple_set of
1.14 TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
1.15 | TupleDifference (ts1, ts2) =>
1.16 - sub ts1 prec ^ " - " ^ sub ts1 (prec + 1)
1.17 - | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec
1.18 + sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
1.19 + | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
1.20 | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
1.21 | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
1.22 | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
2.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 10:28:49 2010 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 11:57:33 2010 +0100
2.3 @@ -128,7 +128,7 @@
2.4 All (decls_for SRep card Ts T, to_F (T :: Ts) t')
2.5 | (t0 as Const (@{const_name All}, _)) $ t1 =>
2.6 to_F Ts (t0 $ eta_expand Ts t1 1)
2.7 - | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
2.8 + | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
2.9 Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
2.10 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
2.11 to_F Ts (t0 $ eta_expand Ts t1 1)
2.12 @@ -234,7 +234,7 @@
2.13 | Free (x as (_, T)) =>
2.14 Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
2.15 | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
2.16 - | Bound j => raise SAME ()
2.17 + | Bound _ => raise SAME ()
2.18 | Abs (_, T, t') =>
2.19 (case fastype_of1 (T :: Ts, t') of
2.20 @{typ bool} => Comprehension (decls_for SRep card Ts T,
2.21 @@ -251,11 +251,8 @@
2.22 let val T2 = fastype_of1 (Ts, t2) in
2.23 case arity_of SRep card T2 of
2.24 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
2.25 - | n =>
2.26 - let
2.27 - val arity2 = arity_of SRep card T2
2.28 - val res_arity = arity_of RRep card T
2.29 - in
2.30 + | arity2 =>
2.31 + let val res_arity = arity_of RRep card T in
2.32 Project (Intersect
2.33 (Product (to_S_rep Ts t2,
2.34 atom_schema_of RRep card T
3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 22 10:28:49 2010 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 22 11:57:33 2010 +0100
3.3 @@ -201,13 +201,13 @@
3.4 error "You must import the theory \"Nitpick\" to use Nitpick"
3.5 *)
3.6 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
3.7 - boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose,
3.8 - overlord, user_axioms, assms, merge_type_vars, binary_ints,
3.9 - destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
3.10 - fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
3.11 - flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
3.12 - evals, formats, max_potential, max_genuine, check_potential,
3.13 - check_genuine, batch_size, ...} =
3.14 + boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
3.15 + user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
3.16 + specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
3.17 + peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
3.18 + max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
3.19 + max_potential, max_genuine, check_potential, check_genuine, batch_size,
3.20 + ...} =
3.21 params
3.22 val state_ref = Unsynchronized.ref state
3.23 (* Pretty.T -> unit *)
3.24 @@ -227,7 +227,6 @@
3.25 (* (unit -> string) -> unit *)
3.26 val print_m = pprint_m o K o plazy
3.27 val print_v = pprint_v o K o plazy
3.28 - val print_d = pprint_d o K o plazy
3.29
3.30 (* unit -> unit *)
3.31 fun check_deadline () =
3.32 @@ -489,9 +488,9 @@
3.33 val core_u = rename_vars_in_nut pool rel_table core_u
3.34 val def_us = map (rename_vars_in_nut pool rel_table) def_us
3.35 val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
3.36 - val core_f = kodkod_formula_from_nut bits ofs kk core_u
3.37 - val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
3.38 - val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
3.39 + val core_f = kodkod_formula_from_nut ofs kk core_u
3.40 + val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
3.41 + val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
3.42 val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
3.43 val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
3.44 PrintMode.setmp [] multiline_string_for_scope scope
3.45 @@ -535,9 +534,8 @@
3.46 in
3.47 SOME ({comment = comment, settings = settings, univ_card = univ_card,
3.48 tuple_assigns = [], bounds = bounds,
3.49 - int_bounds =
3.50 - if bits = 0 then sequential_int_bounds univ_card
3.51 - else pow_of_two_int_bounds bits main_j0 univ_card,
3.52 + int_bounds = if bits = 0 then sequential_int_bounds univ_card
3.53 + else pow_of_two_int_bounds bits main_j0,
3.54 expr_assigns = [], formula = formula},
3.55 {free_names = free_names, sel_names = sel_names,
3.56 nonsel_names = nonsel_names, rel_table = rel_table,
3.57 @@ -562,17 +560,13 @@
3.58 else "genuine") ^
3.59 " component of scope."));
3.60 NONE)
3.61 - | TOO_SMALL (loc, msg) =>
3.62 + | TOO_SMALL (_, msg) =>
3.63 (print_v (fn () => ("Limit reached: " ^ msg ^
3.64 ". Skipping " ^ (if unsound then "potential"
3.65 else "genuine") ^
3.66 " component of scope."));
3.67 NONE)
3.68
3.69 - (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
3.70 - fun tuple_set_for_rel univ_card =
3.71 - KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
3.72 -
3.73 val das_wort_model =
3.74 (if falsify then "counterexample" else "model")
3.75 |> not standard ? prefix "nonstandard "
3.76 @@ -809,8 +803,7 @@
3.77 ()
3.78 (* scope * bool -> rich_problem list * bool
3.79 -> rich_problem list * bool *)
3.80 - fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
3.81 - (problems, donno) =
3.82 + fun add_problem_for_scope (scope, unsound) (problems, donno) =
3.83 (check_deadline ();
3.84 case problem_for_scope unsound scope of
3.85 SOME problem =>
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 10:28:49 2010 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 11:57:33 2010 +0100
4.3 @@ -65,6 +65,7 @@
4.4 val conjuncts_of : term -> term list
4.5 val disjuncts_of : term -> term list
4.6 val unarize_and_unbox_type : typ -> typ
4.7 + val unarize_unbox_and_uniterize_type : typ -> typ
4.8 val string_for_type : Proof.context -> typ -> string
4.9 val prefix_name : string -> string -> string
4.10 val shortest_name : string -> string
4.11 @@ -81,6 +82,7 @@
4.12 val is_lfp_iterator_type : typ -> bool
4.13 val is_gfp_iterator_type : typ -> bool
4.14 val is_fp_iterator_type : typ -> bool
4.15 + val is_iterator_type : typ -> bool
4.16 val is_boolean_type : typ -> bool
4.17 val is_integer_type : typ -> bool
4.18 val is_bit_type : typ -> bool
4.19 @@ -261,7 +263,6 @@
4.20 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
4.21 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
4.22 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
4.23 -val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
4.24 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
4.25 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
4.26 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
4.27 @@ -306,7 +307,7 @@
4.28 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
4.29 | strip_connective _ t = [t]
4.30 (* term -> term list * term *)
4.31 -fun strip_any_connective (t as (t0 $ t1 $ t2)) =
4.32 +fun strip_any_connective (t as (t0 $ _ $ _)) =
4.33 if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
4.34 (strip_connective t0 t, t0)
4.35 else
4.36 @@ -389,7 +390,6 @@
4.37 (* typ -> typ *)
4.38 fun unarize_type @{typ "unsigned_bit word"} = nat_T
4.39 | unarize_type @{typ "signed_bit word"} = int_T
4.40 - | unarize_type @{typ bisim_iterator} = nat_T
4.41 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
4.42 | unarize_type T = T
4.43 fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
4.44 @@ -398,10 +398,14 @@
4.45 Type ("*", map unarize_and_unbox_type Ts)
4.46 | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
4.47 | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
4.48 - | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
4.49 | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
4.50 Type (s, map unarize_and_unbox_type Ts)
4.51 | unarize_and_unbox_type T = T
4.52 +fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
4.53 + | uniterize_type @{typ bisim_iterator} = nat_T
4.54 + | uniterize_type T = T
4.55 +val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
4.56 +
4.57 (* Proof.context -> typ -> string *)
4.58 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
4.59
4.60 @@ -436,7 +440,7 @@
4.61 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
4.62 | term_match thy (Free (s1, T1), Free (s2, T2)) =
4.63 const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
4.64 - | term_match thy (t1, t2) = t1 aconv t2
4.65 + | term_match _ (t1, t2) = t1 aconv t2
4.66
4.67 (* typ -> bool *)
4.68 fun is_TFree (TFree _) = true
4.69 @@ -455,14 +459,14 @@
4.70 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
4.71 | is_gfp_iterator_type _ = false
4.72 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
4.73 +fun is_iterator_type T =
4.74 + (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
4.75 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
4.76 fun is_integer_type T = (T = nat_T orelse T = int_T)
4.77 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
4.78 fun is_word_type (Type (@{type_name word}, _)) = true
4.79 | is_word_type _ = false
4.80 -fun is_integer_like_type T =
4.81 - is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
4.82 - T = @{typ bisim_iterator}
4.83 +val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
4.84 val is_record_type = not o null o Record.dest_recTs
4.85 (* theory -> typ -> bool *)
4.86 fun is_frac_type thy (Type (s, [])) =
4.87 @@ -596,7 +600,7 @@
4.88 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
4.89 | is_quot_type _ (Type ("FSet.fset", _)) = true
4.90 | is_quot_type _ _ = false
4.91 -fun is_codatatype thy (T as Type (s, _)) =
4.92 +fun is_codatatype thy (Type (s, _)) =
4.93 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
4.94 |> Option.map snd |> these))
4.95 | is_codatatype _ _ = false
4.96 @@ -630,7 +634,7 @@
4.97 end
4.98 handle TYPE _ => []
4.99 (* styp -> bool *)
4.100 -fun is_record_constr (x as (s, T)) =
4.101 +fun is_record_constr (s, T) =
4.102 String.isSuffix Record.extN s andalso
4.103 let val dataT = body_type T in
4.104 is_record_type dataT andalso
4.105 @@ -706,7 +710,7 @@
4.106 member (op =) [@{const_name FunBox}, @{const_name PairBox},
4.107 @{const_name Quot}, @{const_name Zero_Rep},
4.108 @{const_name Suc_Rep}] s orelse
4.109 - let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
4.110 + let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
4.111 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
4.112 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
4.113 is_coconstr thy x
4.114 @@ -747,7 +751,7 @@
4.115 (map (box_type hol_ctxt InPair) Ts))
4.116 | _ => false
4.117 (* hol_context -> boxability -> string * typ list -> string *)
4.118 -and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
4.119 +and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
4.120 case triple_lookup (type_match thy) boxes (Type z) of
4.121 SOME (SOME box_me) => box_me
4.122 | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
4.123 @@ -934,9 +938,9 @@
4.124 Abs (Name.uu, dataT, @{const True})
4.125 end
4.126 (* hol_context -> styp -> term -> term *)
4.127 -fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
4.128 - case strip_comb t of
4.129 - (Const x', args) =>
4.130 +fun discriminate_value (hol_ctxt as {thy, ...}) x t =
4.131 + case head_of t of
4.132 + Const x' =>
4.133 if x = x' then @{const True}
4.134 else if is_constr_like thy x' then @{const False}
4.135 else betapply (discr_term_for_constr hol_ctxt x, t)
4.136 @@ -979,7 +983,7 @@
4.137 | construct_value thy stds (x as (s, _)) args =
4.138 let val args = map Envir.eta_contract args in
4.139 case hd args of
4.140 - Const (x' as (s', _)) $ t =>
4.141 + Const (s', _) $ t =>
4.142 if is_sel_like_and_no_discr s' andalso
4.143 constr_name_for_sel_like s' = s andalso
4.144 forall (fn (n, t') =>
4.145 @@ -1063,9 +1067,8 @@
4.146 | constrs =>
4.147 let
4.148 val constr_cards =
4.149 - datatype_constrs hol_ctxt T
4.150 - |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
4.151 - o snd)
4.152 + map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
4.153 + constrs
4.154 in
4.155 if exists (curry (op =) 0) constr_cards then 0
4.156 else Integer.sum constr_cards
4.157 @@ -1199,10 +1202,15 @@
4.158 (s, unarize_type T) of
4.159 SOME n => SOME n
4.160 | NONE =>
4.161 - if is_fun_type T andalso is_set_type (domain_type T) then
4.162 - AList.lookup (op =) built_in_set_consts s
4.163 - else
4.164 - NONE
4.165 + case s of
4.166 + @{const_name zero_class.zero} =>
4.167 + if is_iterator_type T then SOME 0 else NONE
4.168 + | @{const_name Suc} =>
4.169 + if is_iterator_type (domain_type T) then SOME 0 else NONE
4.170 + | _ => if is_fun_type T andalso is_set_type (domain_type T) then
4.171 + AList.lookup (op =) built_in_set_consts s
4.172 + else
4.173 + NONE
4.174 end
4.175 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
4.176 val is_built_in_const = is_some oooo arity_of_built_in_const
4.177 @@ -1233,12 +1241,12 @@
4.178 |> map_filter (try (Refute.specialize_type thy x))
4.179 |> filter (curry (op =) (Const x) o term_under_def)
4.180
4.181 -(* theory -> term -> term option *)
4.182 -fun normalized_rhs_of thy t =
4.183 +(* term -> term option *)
4.184 +fun normalized_rhs_of t =
4.185 let
4.186 (* term option -> term option *)
4.187 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
4.188 - | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
4.189 + | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
4.190 | aux _ _ = NONE
4.191 val (lhs, rhs) =
4.192 case t of
4.193 @@ -1256,7 +1264,7 @@
4.194 NONE
4.195 else
4.196 x |> def_props_for_const thy [(NONE, false)] false table |> List.last
4.197 - |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
4.198 + |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
4.199 handle List.Empty => NONE
4.200
4.201 (* term -> fixpoint_kind *)
4.202 @@ -1366,13 +1374,12 @@
4.203 ||> single |> op ::
4.204 end
4.205 (* theory -> string * typ list -> term list *)
4.206 -fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
4.207 +fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
4.208 let val abs_T = Type abs_z in
4.209 if is_univ_typedef thy abs_T then
4.210 []
4.211 else case typedef_info thy abs_s of
4.212 - SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
4.213 - ...} =>
4.214 + SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
4.215 let
4.216 val rep_T = instantiate_type thy abs_type abs_T rep_type
4.217 val rep_t = Const (Rep_name, abs_T --> rep_T)
4.218 @@ -1495,7 +1502,7 @@
4.219 [!simp_table, psimp_table]
4.220 fun is_inductive_pred hol_ctxt =
4.221 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
4.222 -fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
4.223 +fun is_equational_fun hol_ctxt =
4.224 (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
4.225 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
4.226
4.227 @@ -1522,7 +1529,7 @@
4.228 | is_constr_pattern _ (Var _) = true
4.229 | is_constr_pattern thy t =
4.230 case strip_comb t of
4.231 - (Const (x as (s, _)), args) =>
4.232 + (Const x, args) =>
4.233 is_constr_like thy x andalso forall (is_constr_pattern thy) args
4.234 | _ => false
4.235 fun is_constr_pattern_lhs thy t =
4.236 @@ -1536,9 +1543,9 @@
4.237 val unfold_max_depth = 255
4.238
4.239 (* hol_context -> term -> term *)
4.240 -fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
4.241 - case_names, def_table, ground_thm_table,
4.242 - ersatz_table, ...}) =
4.243 +fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
4.244 + def_table, ground_thm_table, ersatz_table,
4.245 + ...}) =
4.246 let
4.247 (* int -> typ list -> term -> term *)
4.248 fun do_term depth Ts t =
4.249 @@ -1566,8 +1573,7 @@
4.250 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
4.251 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
4.252 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
4.253 - | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
4.254 - $ (t2 as Abs (_, _, t2')) =>
4.255 + | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
4.256 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
4.257 map (do_term depth Ts) [t1, t2])
4.258 | Const (x as (@{const_name distinct},
4.259 @@ -1575,7 +1581,7 @@
4.260 $ (t1 as _ $ _) =>
4.261 (t1 |> HOLogic.dest_list |> distinctness_formula T'
4.262 handle TERM _ => do_const depth Ts t x [t1])
4.263 - | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
4.264 + | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
4.265 if is_ground_term t1 andalso
4.266 exists (Pattern.matches thy o rpair t1)
4.267 (Inttab.lookup_list ground_thm_table (hash_term t1)) then
4.268 @@ -1831,9 +1837,9 @@
4.269 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
4.270 end
4.271
4.272 -(* typ list -> typ -> typ -> term -> term *)
4.273 -fun ap_curry [_] _ _ t = t
4.274 - | ap_curry arg_Ts tuple_T body_T t =
4.275 +(* typ list -> typ -> term -> term *)
4.276 +fun ap_curry [_] _ t = t
4.277 + | ap_curry arg_Ts tuple_T t =
4.278 let val n = length arg_Ts in
4.279 list_abs (map (pair "c") arg_Ts,
4.280 incr_boundvars n t
4.281 @@ -1843,7 +1849,7 @@
4.282 (* int -> term -> int *)
4.283 fun num_occs_of_bound_in_term j (t1 $ t2) =
4.284 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
4.285 - | num_occs_of_bound_in_term j (Abs (s, T, t')) =
4.286 + | num_occs_of_bound_in_term j (Abs (_, _, t')) =
4.287 num_occs_of_bound_in_term (j + 1) t'
4.288 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
4.289 | num_occs_of_bound_in_term _ _ = 0
4.290 @@ -1917,8 +1923,7 @@
4.291 in aux end
4.292
4.293 (* hol_context -> styp -> term -> term *)
4.294 -fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
4.295 - def =
4.296 +fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
4.297 let
4.298 val j = maxidx_of_term def + 1
4.299 val (outer, fp_app) = strip_abs def
4.300 @@ -1947,7 +1952,7 @@
4.301 $ (Const (@{const_name split}, curried_T --> uncurried_T)
4.302 $ list_comb (Const step_x, outer_bounds)))
4.303 $ list_comb (Const base_x, outer_bounds)
4.304 - |> ap_curry tuple_arg_Ts tuple_T bool_T)
4.305 + |> ap_curry tuple_arg_Ts tuple_T)
4.306 |> unfold_defs_in_term hol_ctxt
4.307 end
4.308
4.309 @@ -2017,7 +2022,7 @@
4.310
4.311 (* hol_context -> styp -> term list *)
4.312 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
4.313 - psimp_table, ...}) (x as (s, _)) =
4.314 + psimp_table, ...}) x =
4.315 case def_props_for_const thy stds fast_descrs (!simp_table) x of
4.316 [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
4.317 [] => [inductive_pred_axiom hol_ctxt x]
4.318 @@ -2044,7 +2049,7 @@
4.319 | add_type _ table = table
4.320 val table = fold (fold_types (fold_atyps add_type)) ts []
4.321 (* typ -> typ *)
4.322 - fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
4.323 + fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
4.324 | coalesce T = T
4.325 in map (map_types (map_atyps coalesce)) ts end
4.326
4.327 @@ -2122,7 +2127,7 @@
4.328 (* int list -> int list -> typ -> typ *)
4.329 fun format_type default_format format T =
4.330 let
4.331 - val T = unarize_and_unbox_type T
4.332 + val T = unarize_unbox_and_uniterize_type T
4.333 val format = format |> filter (curry (op <) 0)
4.334 in
4.335 if forall (curry (op =) 1) format then
4.336 @@ -2172,14 +2177,14 @@
4.337 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
4.338 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
4.339 val vars = special_bounds ts @ missing_vars
4.340 - val ts' = map2 (fn T => fn j =>
4.341 - case AList.lookup (op =) (js ~~ ts) j of
4.342 - SOME t => do_term t
4.343 - | NONE =>
4.344 - Var (nth missing_vars
4.345 - (find_index (curry (op =) j)
4.346 - missing_js)))
4.347 - Ts (0 upto max_j)
4.348 + val ts' =
4.349 + map (fn j =>
4.350 + case AList.lookup (op =) (js ~~ ts) j of
4.351 + SOME t => do_term t
4.352 + | NONE =>
4.353 + Var (nth missing_vars
4.354 + (find_index (curry (op =) j) missing_js)))
4.355 + (0 upto max_j)
4.356 val t = do_const x' |> fst
4.357 val format =
4.358 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
4.359 @@ -2251,7 +2256,7 @@
4.360 let val t = Const (original_name s, T) in
4.361 (t, format_term_type thy def_table formats t)
4.362 end)
4.363 - |>> map_types unarize_and_unbox_type
4.364 + |>> map_types unarize_unbox_and_uniterize_type
4.365 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
4.366 in do_const end
4.367
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 22 10:28:49 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 22 11:57:33 2010 +0100
5.3 @@ -169,7 +169,7 @@
5.4 | "false" => SOME false
5.5 | "true" => SOME true
5.6 | "" => SOME true
5.7 - | s => raise Option)
5.8 + | _ => raise Option)
5.9 handle Option.Option =>
5.10 let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
5.11 error ("Parameter " ^ quote name ^ " must be assigned " ^
5.12 @@ -433,7 +433,6 @@
5.13 let
5.14 val thy = Proof.theory_of state
5.15 val ctxt = Proof.context_of state
5.16 - val thm = #goal (Proof.raw_goal state)
5.17 val _ = List.app check_raw_param override_params
5.18 val params as {blocking, debug, ...} =
5.19 extract_params ctxt auto (default_raw_params thy) override_params
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 22 10:28:49 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 22 11:57:33 2010 +0100
6.3 @@ -24,7 +24,7 @@
6.4 val kk_tuple : bool -> int -> int list -> Kodkod.tuple
6.5 val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
6.6 val sequential_int_bounds : int -> Kodkod.int_bound list
6.7 - val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
6.8 + val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
6.9 val bounds_for_built_in_rels_in_formula :
6.10 bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
6.11 val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
6.12 @@ -36,7 +36,7 @@
6.13 hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
6.14 -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
6.15 val kodkod_formula_from_nut :
6.16 - int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
6.17 + int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
6.18 end;
6.19
6.20 structure Nitpick_Kodkod : NITPICK_KODKOD =
6.21 @@ -127,7 +127,7 @@
6.22 (* int -> KK.int_bound list *)
6.23 fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
6.24 (* int -> int -> KK.int_bound list *)
6.25 -fun pow_of_two_int_bounds bits j0 univ_card =
6.26 +fun pow_of_two_int_bounds bits j0 =
6.27 let
6.28 (* int -> int -> int -> KK.int_bound list *)
6.29 fun aux 0 _ _ = []
6.30 @@ -141,7 +141,7 @@
6.31 fun built_in_rels_in_formula formula =
6.32 let
6.33 (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
6.34 - fun rel_expr_func (r as KK.Rel (x as (n, j))) =
6.35 + fun rel_expr_func (KK.Rel (x as (n, j))) =
6.36 if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
6.37 I
6.38 else
6.39 @@ -304,7 +304,7 @@
6.40 (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
6.41 nick)) =
6.42 let
6.43 - val constr as {delta, epsilon, exclusive, explicit_max, ...} =
6.44 + val {delta, epsilon, exclusive, explicit_max, ...} =
6.45 constr_spec dtypes (original_name nick, T1)
6.46 in
6.47 ([(x, bound_comment ctxt debug nick T R)],
6.48 @@ -511,7 +511,7 @@
6.49 raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
6.50 end
6.51 (* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
6.52 -and atom_from_rel_expr kk (x as (k, j0)) old_R r =
6.53 +and atom_from_rel_expr kk x old_R r =
6.54 case old_R of
6.55 Func (R1, R2) =>
6.56 let
6.57 @@ -581,7 +581,7 @@
6.58 end
6.59 | func_from_no_opt_rel_expr kk Unit R2 old_R r =
6.60 (case old_R of
6.61 - Vect (k, R') => rel_expr_from_rel_expr kk R2 R' r
6.62 + Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r
6.63 | Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r
6.64 | Func (Atom (1, _), Formula Neut) =>
6.65 (case unopt_rep R2 of
6.66 @@ -824,8 +824,8 @@
6.67 nfa |> graph_for_nfa |> NfaGraph.strong_conn
6.68 |> map (fn keys => filter (member (op =) keys o fst) nfa)
6.69
6.70 -(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
6.71 -fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
6.72 +(* kodkod_constrs -> nfa_table -> typ -> KK.formula *)
6.73 +fun acyclicity_axiom_for_datatype kk nfa start_T =
6.74 #kk_no kk (#kk_intersect kk
6.75 (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
6.76 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
6.77 @@ -834,20 +834,17 @@
6.78 map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
6.79 dtypes
6.80 |> strongly_connected_sub_nfas
6.81 - |> maps (fn nfa =>
6.82 - map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
6.83 + |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)
6.84
6.85 (* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
6.86 -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
6.87 fun sel_axiom_for_sel hol_ctxt binarize j0
6.88 - (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
6.89 - kk_join, ...}) rel_table dom_r
6.90 - ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
6.91 + (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
6.92 + rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
6.93 n =
6.94 let
6.95 - val x as (_, T) =
6.96 - binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
6.97 - val (r, R, arity) = const_triple rel_table x
6.98 + val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
6.99 + val (r, R, _) = const_triple rel_table x
6.100 val R2 = dest_Func R |> snd
6.101 val z = (epsilon - delta, delta + j0)
6.102 in
6.103 @@ -908,10 +905,6 @@
6.104 map (const_triple rel_table
6.105 o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
6.106 (~1 upto num_sels - 1)
6.107 - val j0 = case triples |> hd |> #2 of
6.108 - Func (Atom (_, j0), _) => j0
6.109 - | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
6.110 - [R])
6.111 val set_r = triples |> hd |> #1
6.112 in
6.113 if num_sels = 0 then
6.114 @@ -962,8 +955,8 @@
6.115 maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
6.116 dtypes
6.117
6.118 -(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
6.119 -fun kodkod_formula_from_nut bits ofs
6.120 +(* int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
6.121 +fun kodkod_formula_from_nut ofs
6.122 (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
6.123 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
6.124 kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
6.125 @@ -1098,7 +1091,7 @@
6.126 else
6.127 kk_subset (to_rep min_R u1) (to_rep min_R u2)
6.128 end)
6.129 - | Op2 (Eq, T, R, u1, u2) =>
6.130 + | Op2 (Eq, _, _, u1, u2) =>
6.131 (case min_rep (rep_of u1) (rep_of u2) of
6.132 Unit => KK.True
6.133 | Formula polar =>
6.134 @@ -1196,7 +1189,7 @@
6.135 case u of
6.136 Cst (False, _, Atom _) => false_atom
6.137 | Cst (True, _, Atom _) => true_atom
6.138 - | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) =>
6.139 + | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>
6.140 if R1 = R2 andalso arity_of_rep R1 = 1 then
6.141 kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
6.142 else
6.143 @@ -1214,7 +1207,7 @@
6.144 (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
6.145 (rel_expr_from_rel_expr kk min_R R2 r2))
6.146 end
6.147 - | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
6.148 + | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
6.149 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
6.150 to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
6.151 | Cst (Num j, T, R) =>
6.152 @@ -1235,7 +1228,7 @@
6.153 to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
6.154 | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
6.155 kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
6.156 - | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel
6.157 + | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
6.158 | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
6.159 | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
6.160 | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
6.161 @@ -1303,7 +1296,7 @@
6.162 | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
6.163 KK.Iden
6.164 | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
6.165 - Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
6.166 + Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
6.167 if nat_j0 = int_j0 then
6.168 kk_intersect KK.Iden
6.169 (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
6.170 @@ -1388,14 +1381,14 @@
6.171 (case R of
6.172 Func (R1, Formula Neut) => to_rep R1 u1
6.173 | Func (Unit, Opt R) => to_guard [u1] R true_atom
6.174 - | Func (R1, R2 as Opt _) =>
6.175 + | Func (R1, Opt _) =>
6.176 single_rel_rel_let kk
6.177 (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
6.178 (rel_expr_to_func kk R1 bool_atom_R
6.179 (Func (R1, Formula Neut)) r))
6.180 (to_opt R1 u1)
6.181 | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
6.182 - | Op1 (Tha, T, R, u1) =>
6.183 + | Op1 (Tha, _, R, u1) =>
6.184 if is_opt_rep R then
6.185 kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
6.186 else
6.187 @@ -1413,7 +1406,7 @@
6.188 | Op2 (All, T, R as Opt _, u1, u2) =>
6.189 to_r (Op1 (Not, T, R,
6.190 Op2 (Exist, T, R, u1, Op1 (Not, T, rep_of u2, u2))))
6.191 - | Op2 (Exist, T, Opt _, u1, u2) =>
6.192 + | Op2 (Exist, _, Opt _, u1, u2) =>
6.193 let val rs1 = untuple to_decl u1 in
6.194 if not (is_opt_rep (rep_of u2)) then
6.195 kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
6.196 @@ -1448,7 +1441,7 @@
6.197 (int_expr_from_atom kk (type_of u1)) (r1, r2))))
6.198 KK.None)
6.199 (to_r u1) (to_r u2))
6.200 - | Op2 (The, T, R, u1, u2) =>
6.201 + | Op2 (The, _, R, u1, u2) =>
6.202 if is_opt_rep R then
6.203 let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
6.204 kk_rel_if (kk_one (kk_join r1 true_atom)) (kk_join r1 true_atom)
6.205 @@ -1461,7 +1454,7 @@
6.206 let val r1 = to_rep (Func (R, Formula Neut)) u1 in
6.207 kk_rel_if (kk_one r1) r1 (to_rep R u2)
6.208 end
6.209 - | Op2 (Eps, T, R, u1, u2) =>
6.210 + | Op2 (Eps, _, R, u1, u2) =>
6.211 if is_opt_rep (rep_of u1) then
6.212 let
6.213 val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1
6.214 @@ -1483,7 +1476,7 @@
6.215 (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
6.216 r2 (empty_rel_for_rep R))
6.217 end
6.218 - | Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>
6.219 + | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
6.220 let
6.221 val f1 = to_f u1
6.222 val f2 = to_f u2
6.223 @@ -1608,11 +1601,11 @@
6.224 false_atom
6.225 else
6.226 to_apply R u1 u2
6.227 - | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) =>
6.228 + | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
6.229 to_guard [u1, u2] R (KK.Atom j0)
6.230 - | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) =>
6.231 + | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
6.232 kk_comprehension (untuple to_decl u1) (to_f u2)
6.233 - | Op2 (Lambda, T, Func (_, R2), u1, u2) =>
6.234 + | Op2 (Lambda, _, Func (_, R2), u1, u2) =>
6.235 let
6.236 val dom_decls = untuple to_decl u1
6.237 val ran_schema = atom_schema_of_rep R2
6.238 @@ -1650,7 +1643,7 @@
6.239 (KK.Atom j0) KK.None)
6.240 | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
6.241 | Construct ([u'], _, _, []) => to_r u'
6.242 - | Construct (discr_u :: sel_us, T, R, arg_us) =>
6.243 + | Construct (discr_u :: sel_us, _, _, arg_us) =>
6.244 let
6.245 val set_rs =
6.246 map2 (fn sel_u => fn arg_u =>
6.247 @@ -1676,7 +1669,7 @@
6.248 KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
6.249 | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
6.250 (* nut -> KK.expr_assign *)
6.251 - and to_expr_assign (FormulaReg (j, _, R)) u =
6.252 + and to_expr_assign (FormulaReg (j, _, _)) u =
6.253 KK.AssignFormulaReg (j, to_f u)
6.254 | to_expr_assign (RelReg (j, _, R)) u =
6.255 KK.AssignRelReg ((arity_of_rep R, j), to_r u)
6.256 @@ -1775,7 +1768,7 @@
6.257 case arity_of_rep nth_R of
6.258 0 => to_guard [u] res_R
6.259 (to_rep res_R (Cst (Unity, res_T, Unit)))
6.260 - | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
6.261 + | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
6.262 end
6.263 (* (KK.formula -> KK.formula -> KK.formula)
6.264 -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
6.265 @@ -1788,11 +1781,11 @@
6.266 in
6.267 case min_R of
6.268 Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
6.269 - | Func (R1, Formula Neut) => set_oper r1 r2
6.270 + | Func (_, Formula Neut) => set_oper r1 r2
6.271 | Func (Unit, Atom (2, j0)) =>
6.272 connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
6.273 - | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
6.274 - (kk_join r2 true_atom)
6.275 + | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
6.276 + (kk_join r2 true_atom)
6.277 | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
6.278 end
6.279 (* (KK.formula -> KK.formula -> KK.formula)
6.280 @@ -1815,7 +1808,7 @@
6.281 | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2
6.282 | Func (_, Formula Neut) => set_oper r1 r2
6.283 | Func (Unit, _) => connective3 r1 r2
6.284 - | Func (R1, _) =>
6.285 + | Func _ =>
6.286 double_rel_rel_let kk
6.287 (fn r1 => fn r2 =>
6.288 kk_union
6.289 @@ -1877,7 +1870,7 @@
6.290 | Atom (1, j0) =>
6.291 to_guard [arg_u] res_R
6.292 (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
6.293 - | Atom (k, j0) =>
6.294 + | Atom (k, _) =>
6.295 let
6.296 val dom_card = card_of_rep (rep_of arg_u)
6.297 val ran_R = Atom (exact_root dom_card k,
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 22 10:28:49 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 22 11:57:33 2010 +0100
7.3 @@ -74,12 +74,12 @@
7.4 |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
7.5 ? prefix "\<^isub>,"
7.6 (* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
7.7 -fun nth_atom_name pool prefix (T as Type (s, _)) j k =
7.8 +fun nth_atom_name pool prefix (Type (s, _)) j k =
7.9 let val s' = shortest_name s in
7.10 prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
7.11 nth_atom_suffix pool s j k
7.12 end
7.13 - | nth_atom_name pool prefix (T as TFree (s, _)) j k =
7.14 + | nth_atom_name pool prefix (TFree (s, _)) j k =
7.15 prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
7.16 | nth_atom_name _ _ T _ _ =
7.17 raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
7.18 @@ -113,20 +113,23 @@
7.19 fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
7.20 unarize_and_unbox_term t1
7.21 | unarize_and_unbox_term (Const (@{const_name PairBox},
7.22 - Type ("fun", [T1, Type ("fun", [T2, T3])]))
7.23 + Type ("fun", [T1, Type ("fun", [T2, _])]))
7.24 $ t1 $ t2) =
7.25 - let val Ts = map unarize_and_unbox_type [T1, T2] in
7.26 + let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
7.27 Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
7.28 $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
7.29 end
7.30 - | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
7.31 + | unarize_and_unbox_term (Const (s, T)) =
7.32 + Const (s, unarize_unbox_and_uniterize_type T)
7.33 | unarize_and_unbox_term (t1 $ t2) =
7.34 unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
7.35 - | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
7.36 - | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
7.37 + | unarize_and_unbox_term (Free (s, T)) =
7.38 + Free (s, unarize_unbox_and_uniterize_type T)
7.39 + | unarize_and_unbox_term (Var (x, T)) =
7.40 + Var (x, unarize_unbox_and_uniterize_type T)
7.41 | unarize_and_unbox_term (Bound j) = Bound j
7.42 | unarize_and_unbox_term (Abs (s, T, t')) =
7.43 - Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
7.44 + Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
7.45
7.46 (* typ -> typ -> (typ * typ) * (typ * typ) *)
7.47 fun factor_out_types (T1 as Type ("*", [T11, T12]))
7.48 @@ -260,12 +263,12 @@
7.49 | mk_tuple _ (t :: _) = t
7.50 | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
7.51
7.52 -(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
7.53 - -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
7.54 - -> typ -> rep -> int list list -> term *)
7.55 -fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
7.56 - ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
7.57 - datatypes, ofs, ...} : scope) sel_names rel_table bounds =
7.58 +(* bool -> atom_pool -> (string * string) * (string * string) -> scope
7.59 + -> nut list -> nut list -> nut list -> nut NameTable.table
7.60 + -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
7.61 +fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
7.62 + ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
7.63 + ofs, ...} : scope) sel_names rel_table bounds =
7.64 let
7.65 val for_auto = (maybe_name = "")
7.66 (* int list list -> int *)
7.67 @@ -357,11 +360,11 @@
7.68 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
7.69 |> make_plain_fun maybe_opt T1 T2
7.70 |> unarize_and_unbox_term
7.71 - |> typecast_fun (unarize_and_unbox_type T')
7.72 - (unarize_and_unbox_type T1)
7.73 - (unarize_and_unbox_type T2)
7.74 + |> typecast_fun (unarize_unbox_and_uniterize_type T')
7.75 + (unarize_unbox_and_uniterize_type T1)
7.76 + (unarize_unbox_and_uniterize_type T2)
7.77 (* (typ * int) list -> typ -> typ -> int -> term *)
7.78 - fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
7.79 + fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
7.80 let
7.81 val k1 = card_of_type card_assigns T1
7.82 val k2 = card_of_type card_assigns T2
7.83 @@ -525,7 +528,7 @@
7.84 map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
7.85 [[js1], [js2]])
7.86 end
7.87 - | term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] =
7.88 + | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
7.89 term_for_vect seen k R' T1 T2 T' js
7.90 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
7.91 jss =
7.92 @@ -548,7 +551,7 @@
7.93 in make_fun true T1 T2 T' ts1 ts2 end
7.94 | term_for_rep seen T T' (Opt R) jss =
7.95 if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
7.96 - | term_for_rep seen T _ R jss =
7.97 + | term_for_rep _ T _ R jss =
7.98 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
7.99 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
7.100 string_of_int (length jss))
7.101 @@ -559,11 +562,11 @@
7.102 fun term_for_name pool scope sel_names rel_table bounds name =
7.103 let val T = type_of name in
7.104 tuple_list_for_name rel_table bounds name
7.105 - |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
7.106 - bounds T T (rep_of name)
7.107 + |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
7.108 + rel_table bounds T T (rep_of name)
7.109 end
7.110
7.111 -(* Proof.context -> (string * string * string * string) * Proof.context *)
7.112 +(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
7.113 fun add_wacky_syntax ctxt =
7.114 let
7.115 (* term -> string *)
7.116 @@ -572,17 +575,17 @@
7.117 val (maybe_t, thy) =
7.118 Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
7.119 Mixfix (maybe_mixfix, [1000], 1000)) thy
7.120 + val (abs_t, thy) =
7.121 + Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
7.122 + Mixfix (abs_mixfix, [40], 40)) thy
7.123 val (base_t, thy) =
7.124 Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
7.125 Mixfix (base_mixfix, [1000], 1000)) thy
7.126 val (step_t, thy) =
7.127 Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
7.128 Mixfix (step_mixfix, [1000], 1000)) thy
7.129 - val (abs_t, thy) =
7.130 - Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
7.131 - Mixfix (abs_mixfix, [40], 40)) thy
7.132 in
7.133 - ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
7.134 + (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
7.135 ProofContext.transfer_syntax thy ctxt)
7.136 end
7.137
7.138 @@ -613,18 +616,18 @@
7.139 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
7.140 -> Pretty.T * bool *)
7.141 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
7.142 - ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
7.143 - user_axioms, debug, binary_ints, destroy_constrs,
7.144 - specialize, skolemize, star_linear_preds, uncurry,
7.145 - fast_descrs, tac_timeout, evals, case_names, def_table,
7.146 - nondef_table, user_nondefs, simp_table, psimp_table,
7.147 - intro_table, ground_thm_table, ersatz_table, skolems,
7.148 - special_funs, unrolled_preds, wf_cache, constr_cache},
7.149 + ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
7.150 + debug, binary_ints, destroy_constrs, specialize,
7.151 + skolemize, star_linear_preds, uncurry, fast_descrs,
7.152 + tac_timeout, evals, case_names, def_table, nondef_table,
7.153 + user_nondefs, simp_table, psimp_table, intro_table,
7.154 + ground_thm_table, ersatz_table, skolems, special_funs,
7.155 + unrolled_preds, wf_cache, constr_cache},
7.156 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
7.157 formats all_frees free_names sel_names nonsel_names rel_table bounds =
7.158 let
7.159 val pool = Unsynchronized.ref []
7.160 - val (wacky_names as (_, base_name, step_name, _), ctxt) =
7.161 + val (wacky_names as (_, base_step_names), ctxt) =
7.162 add_wacky_syntax ctxt
7.163 val hol_ctxt =
7.164 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
7.165 @@ -679,13 +682,12 @@
7.166 val (oper, (t1, T'), T) =
7.167 case name of
7.168 FreeName (s, T, _) =>
7.169 - let val t = Free (s, unarize_and_unbox_type T) in
7.170 + let val t = Free (s, unarize_unbox_and_uniterize_type T) in
7.171 ("=", (t, format_term_type thy def_table formats t), T)
7.172 end
7.173 | ConstName (s, T, _) =>
7.174 (assign_operator_for_const (s, T),
7.175 - user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
7.176 - T)
7.177 + user_friendly_const hol_ctxt base_step_names formats (s, T), T)
7.178 | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
7.179 \pretty_for_assign", [name])
7.180 val t2 = if rep_of name = Any then
7.181 @@ -701,7 +703,8 @@
7.182 (* dtype_spec -> Pretty.T *)
7.183 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
7.184 Pretty.block (Pretty.breaks
7.185 - [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
7.186 + [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
7.187 + Pretty.str "=",
7.188 Pretty.enum "," "{" "}"
7.189 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
7.190 (if complete then [] else [Pretty.str unrep]))])
7.191 @@ -746,7 +749,8 @@
7.192 val free_names =
7.193 map (fn x as (s, T) =>
7.194 case filter (curry (op =) x
7.195 - o pairf nickname_of (unarize_and_unbox_type o type_of))
7.196 + o pairf nickname_of
7.197 + (unarize_unbox_and_uniterize_type o type_of))
7.198 free_names of
7.199 [name] => name
7.200 | [] => FreeName (s, T, Any)
7.201 @@ -767,7 +771,7 @@
7.202
7.203 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
7.204 -> KK.raw_bound list -> term -> bool option *)
7.205 -fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
7.206 +fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
7.207 card_assigns, ...})
7.208 auto_timeout free_names sel_names rel_table bounds prop =
7.209 let
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 22 10:28:49 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 22 11:57:33 2010 +0100
8.3 @@ -45,7 +45,7 @@
8.4 exception CTYPE of string * ctype list
8.5
8.6 (* string -> unit *)
8.7 -fun print_g (s : string) = ()
8.8 +fun print_g (_ : string) = ()
8.9
8.10 (* var -> string *)
8.11 val string_for_var = signed_string_of_int
8.12 @@ -265,7 +265,7 @@
8.13 end
8.14
8.15 (* cdata -> styp -> ctype *)
8.16 -fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
8.17 +fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
8.18 ...}) (x as (_, T)) =
8.19 if could_exist_alpha_sub_ctype thy alpha_T T then
8.20 case AList.lookup (op =) (!constr_cache) x of
8.21 @@ -339,7 +339,7 @@
8.22 | (S Minus, S Plus) => NONE
8.23 | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
8.24 | _ => do_sign_atom_comp Eq [] a1 a2 accum)
8.25 - | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
8.26 + | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
8.27 SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
8.28
8.29 (* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
8.30 @@ -367,7 +367,7 @@
8.31 (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
8.32 handle Library.UnequalLengths =>
8.33 raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
8.34 - | do_ctype_comp cmp xs (CType _) (CType _) accum =
8.35 + | do_ctype_comp _ _ (CType _) (CType _) accum =
8.36 accum (* no need to compare them thanks to the cache *)
8.37 | do_ctype_comp _ _ C1 C2 _ =
8.38 raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
8.39 @@ -435,13 +435,6 @@
8.40 val add_ctype_is_right_unique = add_notin_ctype_fv Minus
8.41 val add_ctype_is_right_total = add_notin_ctype_fv Plus
8.42
8.43 -(* constraint_set -> constraint_set -> constraint_set *)
8.44 -fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
8.45 - (case SOME lits1 |> fold do_literal lits2 of
8.46 - NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
8.47 - | SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2))
8.48 - | unite _ _ = UnsolvableCSet
8.49 -
8.50 (* sign -> bool *)
8.51 fun bool_from_sign Plus = false
8.52 | bool_from_sign Minus = true
8.53 @@ -480,10 +473,6 @@
8.54 SOME b => (x, sign_from_bool b) :: accum
8.55 | NONE => accum) (max_var downto 1) lits
8.56
8.57 -(* literal list -> sign_atom -> sign option *)
8.58 -fun lookup_sign_atom _ (S sn) = SOME sn
8.59 - | lookup_sign_atom lit (V x) = AList.lookup (op =) lit x
8.60 -
8.61 (* comp -> string *)
8.62 fun string_for_comp (a1, a2, cmp, xs) =
8.63 string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
8.64 @@ -522,9 +511,6 @@
8.65 | _ => NONE
8.66 end
8.67
8.68 -(* var -> constraint_set -> bool *)
8.69 -val is_solvable = is_some oo solve
8.70 -
8.71 type ctype_schema = ctype * constraint_set
8.72 type ctype_context =
8.73 {bounds: ctype list,
8.74 @@ -545,8 +531,8 @@
8.75 handle List.Empty => initial_gamma
8.76
8.77 (* cdata -> term -> accumulator -> ctype * accumulator *)
8.78 -fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
8.79 - def_table, ...},
8.80 +fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
8.81 + def_table, ...},
8.82 alpha_T, max_fresh, ...}) =
8.83 let
8.84 (* typ -> ctype *)
8.85 @@ -765,7 +751,7 @@
8.86 | Var _ => (print_g "*** Var"; unsolvable)
8.87 | Bound j => (nth bounds j, accum)
8.88 | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
8.89 - | Abs (s, T, t') =>
8.90 + | Abs (_, T, t') =>
8.91 ((case t' of
8.92 t1' $ Bound 0 =>
8.93 if not (loose_bvar1 (t1', 0)) then
8.94 @@ -806,7 +792,7 @@
8.95 in do_term end
8.96
8.97 (* cdata -> sign -> term -> accumulator -> accumulator *)
8.98 -fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
8.99 +fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
8.100 let
8.101 (* typ -> ctype *)
8.102 val ctype_for = fresh_ctype_for_type cdata
8.103 @@ -814,7 +800,7 @@
8.104 val do_term = consider_term cdata
8.105 (* sign -> term -> accumulator -> accumulator *)
8.106 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
8.107 - | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
8.108 + | do_formula sn t (accum as (gamma, cset)) =
8.109 let
8.110 (* term -> accumulator -> accumulator *)
8.111 val do_co_formula = do_formula sn
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 10:28:49 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 11:57:33 2010 +0100
9.3 @@ -7,7 +7,6 @@
9.4
9.5 signature NITPICK_NUT =
9.6 sig
9.7 - type special_fun = Nitpick_HOL.special_fun
9.8 type hol_context = Nitpick_HOL.hol_context
9.9 type scope = Nitpick_Scope.scope
9.10 type name_pool = Nitpick_Peephole.name_pool
9.11 @@ -467,7 +466,7 @@
9.12 | factorize z = [z]
9.13
9.14 (* hol_context -> op2 -> term -> nut *)
9.15 -fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
9.16 +fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
9.17 let
9.18 (* string list -> typ list -> term -> nut *)
9.19 fun aux eq ss Ts t =
9.20 @@ -518,11 +517,21 @@
9.21 val t1 = list_comb (t0, ts')
9.22 val T1 = fastype_of1 (Ts, t1)
9.23 in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
9.24 + (* styp -> term list -> term *)
9.25 + fun construct (x as (_, T)) ts =
9.26 + case num_binder_types T - length ts of
9.27 + 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
9.28 + o nth_sel_for_constr x)
9.29 + (~1 upto num_sels_for_constr_type T - 1),
9.30 + body_type T, Any,
9.31 + ts |> map (`(curry fastype_of1 Ts))
9.32 + |> maps factorize |> map (sub o snd))
9.33 + | k => sub (eta_expand Ts t k)
9.34 in
9.35 case strip_comb t of
9.36 (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
9.37 do_quantifier All s T t1
9.38 - | (t0 as Const (@{const_name all}, T), [t1]) =>
9.39 + | (t0 as Const (@{const_name all}, _), [t1]) =>
9.40 sub' (t0 $ eta_expand Ts t1 1)
9.41 | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
9.42 | (Const (@{const_name "==>"}, _), [t1, t2]) =>
9.43 @@ -538,11 +547,11 @@
9.44 | (Const (@{const_name True}, T), []) => Cst (True, T, Any)
9.45 | (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
9.46 do_quantifier All s T t1
9.47 - | (t0 as Const (@{const_name All}, T), [t1]) =>
9.48 + | (t0 as Const (@{const_name All}, _), [t1]) =>
9.49 sub' (t0 $ eta_expand Ts t1 1)
9.50 | (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
9.51 do_quantifier Exist s T t1
9.52 - | (t0 as Const (@{const_name Ex}, T), [t1]) =>
9.53 + | (t0 as Const (@{const_name Ex}, _), [t1]) =>
9.54 sub' (t0 $ eta_expand Ts t1 1)
9.55 | (t0 as Const (@{const_name The}, T), [t1]) =>
9.56 if fast_descrs then
9.57 @@ -568,7 +577,7 @@
9.58 | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
9.59 Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
9.60 sub t1, sub_abs s T' t2)
9.61 - | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
9.62 + | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
9.63 sub (t0 $ t1 $ eta_expand Ts t2 1)
9.64 | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
9.65 | (Const (@{const_name Pair}, T), [t1, t2]) =>
9.66 @@ -595,7 +604,10 @@
9.67 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
9.68 | (Const (@{const_name image}, T), [t1, t2]) =>
9.69 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
9.70 - | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
9.71 + | (Const (x as (s as @{const_name Suc}, T)), []) =>
9.72 + if is_built_in_const thy stds false x then Cst (Suc, T, Any)
9.73 + else if is_constr thy stds x then construct x []
9.74 + else ConstName (s, T, Any)
9.75 | (Const (@{const_name finite}, T), [t1]) =>
9.76 (if is_finite_type hol_ctxt (domain_type T) then
9.77 Cst (True, bool_T, Any)
9.78 @@ -604,14 +616,9 @@
9.79 | _ => Op1 (Finite, bool_T, Any, sub t1))
9.80 | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
9.81 | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
9.82 - if is_built_in_const thy stds false x then
9.83 - Cst (Num 0, T, Any)
9.84 - else if is_constr thy stds x then
9.85 - let val (s', T') = discr_for_constr x in
9.86 - Construct ([ConstName (s', T', Any)], T, Any, [])
9.87 - end
9.88 - else
9.89 - ConstName (s, T, Any)
9.90 + if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
9.91 + else if is_constr thy stds x then construct x []
9.92 + else ConstName (s, T, Any)
9.93 | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
9.94 if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
9.95 else ConstName (s, T, Any)
9.96 @@ -631,7 +638,7 @@
9.97 | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
9.98 if is_built_in_const thy stds false x then Cst (Divide, T, Any)
9.99 else ConstName (s, T, Any)
9.100 - | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
9.101 + | (t0 as Const (x as (@{const_name ord_class.less}, _)),
9.102 ts as [t1, t2]) =>
9.103 if is_built_in_const thy stds false x then
9.104 Op2 (Less, bool_T, Any, sub t1, sub t2)
9.105 @@ -642,7 +649,7 @@
9.106 [t1, t2]) =>
9.107 Op2 (Subset, bool_T, Any, sub t1, sub t2)
9.108 (* FIXME: find out if this case is necessary *)
9.109 - | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
9.110 + | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
9.111 ts as [t1, t2]) =>
9.112 if is_built_in_const thy stds false x then
9.113 Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
9.114 @@ -660,7 +667,7 @@
9.115 else
9.116 ConstName (s, T, Any)
9.117 | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
9.118 - | (Const (@{const_name is_unknown}, T), [t1]) =>
9.119 + | (Const (@{const_name is_unknown}, _), [t1]) =>
9.120 Op1 (IsUnknown, bool_T, Any, sub t1)
9.121 | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
9.122 Op1 (Tha, T2, Any, sub t1)
9.123 @@ -681,14 +688,7 @@
9.124 Op2 (Union, T1, Any, sub t1, sub t2)
9.125 | (t0 as Const (x as (s, T)), ts) =>
9.126 if is_constr thy stds x then
9.127 - case num_binder_types T - length ts of
9.128 - 0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
9.129 - o nth_sel_for_constr x)
9.130 - (~1 upto num_sels_for_constr_type T - 1),
9.131 - body_type T, Any,
9.132 - ts |> map (`(curry fastype_of1 Ts))
9.133 - |> maps factorize |> map (sub o snd))
9.134 - | k => sub (eta_expand Ts t k)
9.135 + construct x ts
9.136 else if String.isPrefix numeral_prefix s then
9.137 Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
9.138 else
9.139 @@ -726,8 +726,8 @@
9.140 in (v :: vs, NameTable.update (v, R) table) end
9.141 (* scope -> bool -> nut -> nut list * rep NameTable.table
9.142 -> nut list * rep NameTable.table *)
9.143 -fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
9.144 - ofs, ...}) all_exact v (vs, table) =
9.145 +fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
9.146 + (vs, table) =
9.147 let
9.148 val x as (s, T) = (nickname_of v, type_of v)
9.149 val R = (if is_abs_fun thy x then
9.150 @@ -904,8 +904,7 @@
9.151 | untuple f u = if rep_of u = Unit then [] else [f u]
9.152
9.153 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
9.154 -fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
9.155 - bits, datatypes, ofs, ...})
9.156 +fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
9.157 unsound table def =
9.158 let
9.159 val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
9.160 @@ -991,7 +990,7 @@
9.161 Cst (cst, T, best_set_rep_for_type scope T)
9.162 | Op1 (Not, T, _, u1) =>
9.163 (case gsub def (flip_polarity polar) u1 of
9.164 - Op2 (Triad, T, R, u11, u12) =>
9.165 + Op2 (Triad, T, _, u11, u12) =>
9.166 triad (s_op1 Not T (Formula Pos) u12)
9.167 (s_op1 Not T (Formula Neg) u11)
9.168 | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
9.169 @@ -1138,7 +1137,7 @@
9.170 else
9.171 unopt_rep R
9.172 in s_op2 Lambda T R u1' u2' end
9.173 - | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
9.174 + | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
9.175 | Op2 (oper, T, _, u1, u2) =>
9.176 if oper = All orelse oper = Exist then
9.177 let
9.178 @@ -1307,7 +1306,7 @@
9.179 end
9.180 | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
9.181 Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
9.182 - | shape_tuple T R [u] =
9.183 + | shape_tuple T _ [u] =
9.184 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
9.185 | shape_tuple T Unit [] = Cst (Unity, T, Unit)
9.186 | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
9.187 @@ -1390,7 +1389,6 @@
9.188 let
9.189 val bs = untuple I u1
9.190 val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
9.191 - val u11 = rename_vars_in_nut pool table' u1
9.192 in
9.193 Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
9.194 rename_vars_in_nut pool table u2,
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 10:28:49 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 11:57:33 2010 +0100
10.3 @@ -261,14 +261,10 @@
10.4 (* bool -> int -> int -> int -> kodkod_constrs *)
10.5 fun kodkod_constrs optim nat_card int_card main_j0 =
10.6 let
10.7 - val false_atom = Atom main_j0
10.8 - val true_atom = Atom (main_j0 + 1)
10.9 -
10.10 (* bool -> int *)
10.11 val from_bool = atom_for_bool main_j0
10.12 (* int -> rel_expr *)
10.13 fun from_nat n = Atom (n + main_j0)
10.14 - val from_int = Atom o atom_for_int (int_card, main_j0)
10.15 (* int -> int *)
10.16 fun to_nat j = j - main_j0
10.17 val to_int = int_for_atom (int_card, main_j0)
10.18 @@ -415,7 +411,7 @@
10.19 fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
10.20 | s_subset (Atom j) (AtomSeq (k, j0)) =
10.21 formula_for_bool (j >= j0 andalso j < j0 + k)
10.22 - | s_subset (r1 as Union (r11, r12)) r2 =
10.23 + | s_subset (Union (r11, r12)) r2 =
10.24 s_and (s_subset r11 r2) (s_subset r12 r2)
10.25 | s_subset r1 (r2 as Union (r21, r22)) =
10.26 if is_one_rel_expr r1 then
10.27 @@ -516,7 +512,7 @@
10.28 | s_join (r1 as RelIf (f, r11, r12)) r2 =
10.29 if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
10.30 else Join (r1, r2)
10.31 - | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
10.32 + | s_join (r1 as Atom j1) (r2 as Rel (x as (2, _))) =
10.33 if x = suc_rel then
10.34 let val n = to_nat j1 + 1 in
10.35 if n < nat_card then from_nat n else None
10.36 @@ -528,7 +524,7 @@
10.37 s_project (s_join r21 r1) is
10.38 else
10.39 Join (r1, r2)
10.40 - | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
10.41 + | s_join r1 (Join (r21, r22 as Rel (x as (3, _)))) =
10.42 ((if x = nat_add_rel then
10.43 case (r21, r1) of
10.44 (Atom j1, Atom j2) =>
10.45 @@ -613,7 +609,6 @@
10.46 in aux (arity_of_rel_expr r) r end
10.47
10.48 (* rel_expr -> rel_expr -> rel_expr *)
10.49 - fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
10.50 fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
10.51 | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
10.52 fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
10.53 @@ -624,7 +619,6 @@
10.54 (* rel_expr -> rel_expr *)
10.55 fun d_not3 r = Join (r, Rel not3_rel)
10.56 (* rel_expr -> rel_expr -> rel_expr *)
10.57 - fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
10.58 fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
10.59 fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
10.60 in
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 10:28:49 2010 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 11:57:33 2010 +0100
11.3 @@ -87,10 +87,9 @@
11.4 SOME n =>
11.5 if n >= 2 then
11.6 let
11.7 - val (arg_Ts, rest_T) = strip_n_binders n T
11.8 + val arg_Ts = strip_n_binders n T |> fst
11.9 val j =
11.10 - if hd arg_Ts = @{typ bisim_iterator} orelse
11.11 - is_fp_iterator_type (hd arg_Ts) then
11.12 + if is_iterator_type (hd arg_Ts) then
11.13 1
11.14 else case find_index (not_equal bool_T) arg_Ts of
11.15 ~1 => n
11.16 @@ -363,8 +362,8 @@
11.17 fun fresh_value_var Ts k n j t =
11.18 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
11.19
11.20 -(* typ list -> int -> term -> bool *)
11.21 -fun has_heavy_bounds_or_vars Ts level t =
11.22 +(* typ list -> term -> bool *)
11.23 +fun has_heavy_bounds_or_vars Ts t =
11.24 let
11.25 (* typ list -> bool *)
11.26 fun aux [] = false
11.27 @@ -381,7 +380,7 @@
11.28 Const x =>
11.29 if not relax andalso is_constr thy stds x andalso
11.30 not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
11.31 - has_heavy_bounds_or_vars Ts level t_comb andalso
11.32 + has_heavy_bounds_or_vars Ts t_comb andalso
11.33 not (loose_bvar (t_comb, level)) then
11.34 let
11.35 val (j, seen) = case find_index (curry (op =) t_comb) seen of
11.36 @@ -629,7 +628,7 @@
11.37 $ Abs (s, T, kill ss Ts ts))
11.38 | kill _ _ _ = raise UnequalLengths
11.39 (* string list -> typ list -> term -> term *)
11.40 - fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
11.41 + fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
11.42 gather (ss @ [s1]) (Ts @ [T1]) t1
11.43 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
11.44 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
11.45 @@ -704,7 +703,7 @@
11.46 | @{const "op -->"} $ t1 $ t2 =>
11.47 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
11.48 $ aux ss Ts js depth polar t2
11.49 - | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
11.50 + | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
11.51 t0 $ t1 $ aux ss Ts js depth polar t2
11.52 | Const (x as (s, T)) =>
11.53 if is_inductive_pred hol_ctxt x andalso
11.54 @@ -843,7 +842,7 @@
11.55 val bound_var_prefix = "b"
11.56
11.57 (* hol_context -> int -> term -> term *)
11.58 -fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
11.59 +fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
11.60 special_funs, ...}) depth t =
11.61 if not specialize orelse depth > special_max_depth then
11.62 t
11.63 @@ -919,8 +918,8 @@
11.64
11.65 val cong_var_prefix = "c"
11.66
11.67 -(* styp -> special_triple -> special_triple -> term *)
11.68 -fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
11.69 +(* typ -> special_triple -> special_triple -> term *)
11.70 +fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
11.71 let
11.72 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
11.73 val Ts = binder_types T
11.74 @@ -959,28 +958,28 @@
11.75 fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
11.76 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
11.77 (j2 ~~ t2, j1 ~~ t1)
11.78 - (* styp -> special_triple list -> special_triple list -> special_triple list
11.79 + (* typ -> special_triple list -> special_triple list -> special_triple list
11.80 -> term list -> term list *)
11.81 fun do_pass_1 _ [] [_] [_] = I
11.82 - | do_pass_1 x skipped _ [] = do_pass_2 x skipped
11.83 - | do_pass_1 x skipped all (z :: zs) =
11.84 + | do_pass_1 T skipped _ [] = do_pass_2 T skipped
11.85 + | do_pass_1 T skipped all (z :: zs) =
11.86 case filter (is_more_specific z) all
11.87 |> sort (int_ord o pairself generality) of
11.88 - [] => do_pass_1 x (z :: skipped) all zs
11.89 - | (z' :: _) => cons (special_congruence_axiom x z z')
11.90 - #> do_pass_1 x skipped all zs
11.91 - (* styp -> special_triple list -> term list -> term list *)
11.92 + [] => do_pass_1 T (z :: skipped) all zs
11.93 + | (z' :: _) => cons (special_congruence_axiom T z z')
11.94 + #> do_pass_1 T skipped all zs
11.95 + (* typ -> special_triple list -> term list -> term list *)
11.96 and do_pass_2 _ [] = I
11.97 - | do_pass_2 x (z :: zs) =
11.98 - fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
11.99 - in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
11.100 + | do_pass_2 T (z :: zs) =
11.101 + fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
11.102 + in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end
11.103
11.104 (** Axiom selection **)
11.105
11.106 (* Similar to "Refute.specialize_type" but returns all matches rather than only
11.107 the first (preorder) match. *)
11.108 (* theory -> styp -> term -> term list *)
11.109 -fun multi_specialize_type thy slack (x as (s, T)) t =
11.110 +fun multi_specialize_type thy slack (s, T) t =
11.111 let
11.112 (* term -> (typ * term) list -> (typ * term) list *)
11.113 fun aux (Const (s', T')) ys =
11.114 @@ -1062,7 +1061,7 @@
11.115 is_built_in_const thy stds fast_descrs x then
11.116 accum
11.117 else
11.118 - let val accum as (xs, _) = (x :: xs, axs) in
11.119 + let val accum = (x :: xs, axs) in
11.120 if depth > axioms_max_depth then
11.121 raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
11.122 \add_axioms_for_term",
11.123 @@ -1130,7 +1129,7 @@
11.124 | @{typ unit} => I
11.125 | TFree (_, S) => add_axioms_for_sort depth T S
11.126 | TVar (_, S) => add_axioms_for_sort depth T S
11.127 - | Type (z as (s, Ts)) =>
11.128 + | Type (z as (_, Ts)) =>
11.129 fold (add_axioms_for_type depth) Ts
11.130 #> (if is_pure_typedef thy T then
11.131 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
11.132 @@ -1192,7 +1191,7 @@
11.133 ((if is_constr_like thy x then
11.134 if length args = num_binder_types T then
11.135 case hd args of
11.136 - Const (x' as (_, T')) $ t' =>
11.137 + Const (_, T') $ t' =>
11.138 if domain_type T' = body_type T andalso
11.139 forall (uncurry (is_nth_sel_on t'))
11.140 (index_seq 0 (length args) ~~ args) then
11.141 @@ -1276,13 +1275,13 @@
11.142 paper). *)
11.143 val quantifier_cluster_threshold = 7
11.144
11.145 -(* theory -> term -> term *)
11.146 -fun push_quantifiers_inward thy =
11.147 +(* term -> term *)
11.148 +val push_quantifiers_inward =
11.149 let
11.150 (* string -> string list -> typ list -> term -> term *)
11.151 fun aux quant_s ss Ts t =
11.152 (case t of
11.153 - (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
11.154 + Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
11.155 if s0 = quant_s then
11.156 aux s0 (s1 :: ss) (T1 :: Ts) t1
11.157 else if quant_s = "" andalso
11.158 @@ -1406,8 +1405,8 @@
11.159 val table =
11.160 Termtab.empty |> uncurry
11.161 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
11.162 - (* bool -> bool -> term -> term *)
11.163 - fun do_rest def core =
11.164 + (* bool -> term -> term *)
11.165 + fun do_rest def =
11.166 binarize ? binarize_nat_and_int_in_term
11.167 #> uncurry ? uncurry_term table
11.168 #> box ? box_fun_and_pair_in_term hol_ctxt def
11.169 @@ -1419,13 +1418,13 @@
11.170 #> destroy_existential_equalities hol_ctxt
11.171 #> simplify_constrs_and_sels thy
11.172 #> distribute_quantifiers
11.173 - #> push_quantifiers_inward thy
11.174 + #> push_quantifiers_inward
11.175 #> close_form
11.176 #> Term.map_abs_vars shortest_name
11.177 in
11.178 - (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
11.179 + (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
11.180 (got_all_mono_user_axioms, no_poly_user_axioms)),
11.181 - do_rest false true core_t, binarize)
11.182 + do_rest false core_t, binarize)
11.183 end
11.184
11.185 end;
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 22 10:28:49 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 22 11:57:33 2010 +0100
12.3 @@ -166,7 +166,7 @@
12.4
12.5 (* rep -> rep list *)
12.6 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
12.7 - | binder_reps R = []
12.8 + | binder_reps _ = []
12.9 (* rep -> rep *)
12.10 fun body_rep (Func (_, R2)) = body_rep R2
12.11 | body_rep R = R
12.12 @@ -272,10 +272,10 @@
12.13 (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
12.14 (Unit, Unit) => Unit
12.15 | (R1, R2) => Struct [R1, R2])
12.16 - | best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
12.17 + | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
12.18 (case card_of_type card_assigns T of
12.19 1 => if is_some (datatype_spec datatypes T) orelse
12.20 - is_fp_iterator_type T then
12.21 + is_iterator_type T then
12.22 Atom (1, offset_of_type ofs T)
12.23 else
12.24 Unit
12.25 @@ -332,7 +332,7 @@
12.26 | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
12.27 type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
12.28 | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
12.29 - | type_schema_of_rep T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
12.30 + | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
12.31 (* typ list -> rep list -> typ list *)
12.32 and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
12.33
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 22 10:28:49 2010 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 22 11:57:33 2010 +0100
13.3 @@ -136,7 +136,7 @@
13.4 (* (string -> string) -> scope
13.5 -> string list * string list * string list * string list * string list *)
13.6 fun quintuple_for_scope quote
13.7 - ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
13.8 + ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
13.9 datatypes, ...} : scope) =
13.10 let
13.11 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
13.12 @@ -346,7 +346,7 @@
13.13 let
13.14 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
13.15 fun aux seen [] = SOME seen
13.16 - | aux seen ((T, 0) :: _) = NONE
13.17 + | aux _ ((_, 0) :: _) = NONE
13.18 | aux seen ((T, k) :: rest) =
13.19 (if is_surely_inconsistent_scope_description hol_ctxt binarize
13.20 ((T, k) :: seen) rest max_assigns then
13.21 @@ -359,7 +359,7 @@
13.22 in aux [] (rev card_assigns) end
13.23
13.24 (* theory -> (typ * int) list -> typ * int -> typ * int *)
13.25 -fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
13.26 +fun repair_iterator_assign thy assigns (T as Type (_, Ts), k) =
13.27 (T, if T = @{typ bisim_iterator} then
13.28 let
13.29 val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
13.30 @@ -394,15 +394,15 @@
13.31 end
13.32 handle Option.Option => NONE
13.33
13.34 -(* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
13.35 -fun offset_table_for_card_assigns thy assigns dtypes =
13.36 +(* (typ * int) list -> dtype_spec list -> int Typtab.table *)
13.37 +fun offset_table_for_card_assigns assigns dtypes =
13.38 let
13.39 (* int -> (int * int) list -> (typ * int) list -> int Typtab.table
13.40 -> int Typtab.table *)
13.41 fun aux next _ [] = Typtab.update_new (dummyT, next)
13.42 | aux next reusable ((T, k) :: assigns) =
13.43 - if k = 1 orelse is_fp_iterator_type T orelse is_integer_type T
13.44 - orelse T = @{typ bisim_iterator} orelse is_bit_type T then
13.45 + if k = 1 orelse is_iterator_type T orelse is_integer_type T
13.46 + orelse is_bit_type T then
13.47 aux next reusable assigns
13.48 else if length (these (Option.map #constrs (datatype_spec dtypes T)))
13.49 > 1 then
13.50 @@ -421,12 +421,10 @@
13.51 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
13.52 -> constr_spec list -> constr_spec list *)
13.53 fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
13.54 - num_self_recs num_non_self_recs (self_rec, x as (s, T))
13.55 + num_self_recs num_non_self_recs (self_rec, x as (_, T))
13.56 constrs =
13.57 let
13.58 val max = constr_max max_assigns x
13.59 - (* int -> int *)
13.60 - fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
13.61 (* unit -> int *)
13.62 fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
13.63 val {delta, epsilon, exclusive, total} =
13.64 @@ -496,14 +494,6 @@
13.65 concrete = concrete, deep = deep, constrs = constrs}
13.66 end
13.67
13.68 -(* int -> int *)
13.69 -fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
13.70 -(* scope_desc -> int *)
13.71 -fun min_bits_for_max_assigns (_, []) = 0
13.72 - | min_bits_for_max_assigns (card_assigns, max_assigns) =
13.73 - min_bits_for_nat_value (fold Integer.max
13.74 - (map snd card_assigns @ map snd max_assigns) 0)
13.75 -
13.76 (* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
13.77 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
13.78 deep_dataTs (desc as (card_assigns, _)) =
13.79 @@ -520,7 +510,7 @@
13.80 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
13.81 datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
13.82 ofs = if sym_break <= 0 then Typtab.empty
13.83 - else offset_table_for_card_assigns thy card_assigns datatypes}
13.84 + else offset_table_for_card_assigns card_assigns datatypes}
13.85 end
13.86
13.87 (* theory -> typ list -> (typ option * int list) list
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 10:28:49 2010 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 11:57:33 2010 +0100
14.3 @@ -308,7 +308,7 @@
14.4 NameTable.empty
14.5 val u = Op1 (Not, type_of u, rep_of u, u)
14.6 |> rename_vars_in_nut pool table
14.7 - val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
14.8 + val formula = kodkod_formula_from_nut Typtab.empty constrs u
14.9 val bounds = map (bound_for_plain_rel ctxt debug) free_rels
14.10 val univ_card = univ_card nat_card int_card j0 bounds formula
14.11 val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 22 10:28:49 2010 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 22 11:57:33 2010 +0100
15.3 @@ -92,7 +92,7 @@
15.4 val max_exponent = 16384
15.5
15.6 (* int -> int -> int *)
15.7 -fun reasonable_power a 0 = 1
15.8 +fun reasonable_power _ 0 = 1
15.9 | reasonable_power a 1 = a
15.10 | reasonable_power 0 _ = 0
15.11 | reasonable_power 1 _ = 1