--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 22 11:57:33 2010 +0100
@@ -465,7 +465,7 @@
| arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
| arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
| arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
- | arity_of_rel_expr (Project (r, is)) = length is
+ | arity_of_rel_expr (Project (_, is)) = length is
| arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
| arity_of_rel_expr (Closure _) = 2
| arity_of_rel_expr (ReflexiveClosure _) = 2
@@ -590,8 +590,8 @@
(case tuple_set of
TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
| TupleDifference (ts1, ts2) =>
- sub ts1 prec ^ " - " ^ sub ts1 (prec + 1)
- | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec
+ sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
+ | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
| TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
| TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
| TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 11:57:33 2010 +0100
@@ -128,7 +128,7 @@
All (decls_for SRep card Ts T, to_F (T :: Ts) t')
| (t0 as Const (@{const_name All}, _)) $ t1 =>
to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+ | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
to_F Ts (t0 $ eta_expand Ts t1 1)
@@ -234,7 +234,7 @@
| Free (x as (_, T)) =>
Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
| Term.Var _ => raise NOT_SUPPORTED "schematic variables"
- | Bound j => raise SAME ()
+ | Bound _ => raise SAME ()
| Abs (_, T, t') =>
(case fastype_of1 (T :: Ts, t') of
@{typ bool} => Comprehension (decls_for SRep card Ts T,
@@ -251,11 +251,8 @@
let val T2 = fastype_of1 (Ts, t2) in
case arity_of SRep card T2 of
1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
- | n =>
- let
- val arity2 = arity_of SRep card T2
- val res_arity = arity_of RRep card T
- in
+ | arity2 =>
+ let val res_arity = arity_of RRep card T in
Project (Intersect
(Product (to_S_rep Ts t2,
atom_schema_of RRep card T
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 22 11:57:33 2010 +0100
@@ -201,13 +201,13 @@
error "You must import the theory \"Nitpick\" to use Nitpick"
*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
- boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose,
- overlord, user_axioms, assms, merge_type_vars, binary_ints,
- destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
- fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
- flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
- evals, formats, max_potential, max_genuine, check_potential,
- check_genuine, batch_size, ...} =
+ boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
+ user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
+ specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
+ peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
+ max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
+ max_potential, max_genuine, check_potential, check_genuine, batch_size,
+ ...} =
params
val state_ref = Unsynchronized.ref state
(* Pretty.T -> unit *)
@@ -227,7 +227,6 @@
(* (unit -> string) -> unit *)
val print_m = pprint_m o K o plazy
val print_v = pprint_v o K o plazy
- val print_d = pprint_d o K o plazy
(* unit -> unit *)
fun check_deadline () =
@@ -489,9 +488,9 @@
val core_u = rename_vars_in_nut pool rel_table core_u
val def_us = map (rename_vars_in_nut pool rel_table) def_us
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
- val core_f = kodkod_formula_from_nut bits ofs kk core_u
- val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
- val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
+ val core_f = kodkod_formula_from_nut ofs kk core_u
+ val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
+ val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
PrintMode.setmp [] multiline_string_for_scope scope
@@ -535,9 +534,8 @@
in
SOME ({comment = comment, settings = settings, univ_card = univ_card,
tuple_assigns = [], bounds = bounds,
- int_bounds =
- if bits = 0 then sequential_int_bounds univ_card
- else pow_of_two_int_bounds bits main_j0 univ_card,
+ int_bounds = if bits = 0 then sequential_int_bounds univ_card
+ else pow_of_two_int_bounds bits main_j0,
expr_assigns = [], formula = formula},
{free_names = free_names, sel_names = sel_names,
nonsel_names = nonsel_names, rel_table = rel_table,
@@ -562,17 +560,13 @@
else "genuine") ^
" component of scope."));
NONE)
- | TOO_SMALL (loc, msg) =>
+ | TOO_SMALL (_, msg) =>
(print_v (fn () => ("Limit reached: " ^ msg ^
". Skipping " ^ (if unsound then "potential"
else "genuine") ^
" component of scope."));
NONE)
- (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
- fun tuple_set_for_rel univ_card =
- KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
-
val das_wort_model =
(if falsify then "counterexample" else "model")
|> not standard ? prefix "nonstandard "
@@ -809,8 +803,7 @@
()
(* scope * bool -> rich_problem list * bool
-> rich_problem list * bool *)
- fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
- (problems, donno) =
+ fun add_problem_for_scope (scope, unsound) (problems, donno) =
(check_deadline ();
case problem_for_scope unsound scope of
SOME problem =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 11:57:33 2010 +0100
@@ -65,6 +65,7 @@
val conjuncts_of : term -> term list
val disjuncts_of : term -> term list
val unarize_and_unbox_type : typ -> typ
+ val unarize_unbox_and_uniterize_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
val shortest_name : string -> string
@@ -81,6 +82,7 @@
val is_lfp_iterator_type : typ -> bool
val is_gfp_iterator_type : typ -> bool
val is_fp_iterator_type : typ -> bool
+ val is_iterator_type : typ -> bool
val is_boolean_type : typ -> bool
val is_integer_type : typ -> bool
val is_bit_type : typ -> bool
@@ -261,7 +263,6 @@
val set_prefix = nitpick_prefix ^ "set" ^ name_sep
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
-val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
val base_prefix = nitpick_prefix ^ "base" ^ name_sep
val step_prefix = nitpick_prefix ^ "step" ^ name_sep
@@ -306,7 +307,7 @@
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
| strip_connective _ t = [t]
(* term -> term list * term *)
-fun strip_any_connective (t as (t0 $ t1 $ t2)) =
+fun strip_any_connective (t as (t0 $ _ $ _)) =
if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
(strip_connective t0 t, t0)
else
@@ -389,7 +390,6 @@
(* typ -> typ *)
fun unarize_type @{typ "unsigned_bit word"} = nat_T
| unarize_type @{typ "signed_bit word"} = int_T
- | unarize_type @{typ bisim_iterator} = nat_T
| unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
| unarize_type T = T
fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
@@ -398,10 +398,14 @@
Type ("*", map unarize_and_unbox_type Ts)
| unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
| unarize_and_unbox_type @{typ "signed_bit word"} = int_T
- | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
| unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
Type (s, map unarize_and_unbox_type Ts)
| unarize_and_unbox_type T = T
+fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
+ | uniterize_type @{typ bisim_iterator} = nat_T
+ | uniterize_type T = T
+val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
+
(* Proof.context -> typ -> string *)
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
@@ -436,7 +440,7 @@
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
| term_match thy (Free (s1, T1), Free (s2, T2)) =
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
- | term_match thy (t1, t2) = t1 aconv t2
+ | term_match _ (t1, t2) = t1 aconv t2
(* typ -> bool *)
fun is_TFree (TFree _) = true
@@ -455,14 +459,14 @@
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
| is_gfp_iterator_type _ = false
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
+fun is_iterator_type T =
+ (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
fun is_boolean_type T = (T = prop_T orelse T = bool_T)
fun is_integer_type T = (T = nat_T orelse T = int_T)
fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
fun is_word_type (Type (@{type_name word}, _)) = true
| is_word_type _ = false
-fun is_integer_like_type T =
- is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
- T = @{typ bisim_iterator}
+val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
val is_record_type = not o null o Record.dest_recTs
(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
@@ -596,7 +600,7 @@
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
| is_quot_type _ (Type ("FSet.fset", _)) = true
| is_quot_type _ _ = false
-fun is_codatatype thy (T as Type (s, _)) =
+fun is_codatatype thy (Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
|> Option.map snd |> these))
| is_codatatype _ _ = false
@@ -630,7 +634,7 @@
end
handle TYPE _ => []
(* styp -> bool *)
-fun is_record_constr (x as (s, T)) =
+fun is_record_constr (s, T) =
String.isSuffix Record.extN s andalso
let val dataT = body_type T in
is_record_type dataT andalso
@@ -706,7 +710,7 @@
member (op =) [@{const_name FunBox}, @{const_name PairBox},
@{const_name Quot}, @{const_name Zero_Rep},
@{const_name Suc_Rep}] s orelse
- let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
+ let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
is_coconstr thy x
@@ -747,7 +751,7 @@
(map (box_type hol_ctxt InPair) Ts))
| _ => false
(* hol_context -> boxability -> string * typ list -> string *)
-and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
+and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
case triple_lookup (type_match thy) boxes (Type z) of
SOME (SOME box_me) => box_me
| _ => is_boxing_worth_it hol_ctxt boxy (Type z)
@@ -934,9 +938,9 @@
Abs (Name.uu, dataT, @{const True})
end
(* hol_context -> styp -> term -> term *)
-fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
- case strip_comb t of
- (Const x', args) =>
+fun discriminate_value (hol_ctxt as {thy, ...}) x t =
+ case head_of t of
+ Const x' =>
if x = x' then @{const True}
else if is_constr_like thy x' then @{const False}
else betapply (discr_term_for_constr hol_ctxt x, t)
@@ -979,7 +983,7 @@
| construct_value thy stds (x as (s, _)) args =
let val args = map Envir.eta_contract args in
case hd args of
- Const (x' as (s', _)) $ t =>
+ Const (s', _) $ t =>
if is_sel_like_and_no_discr s' andalso
constr_name_for_sel_like s' = s andalso
forall (fn (n, t') =>
@@ -1063,9 +1067,8 @@
| constrs =>
let
val constr_cards =
- datatype_constrs hol_ctxt T
- |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
- o snd)
+ map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
+ constrs
in
if exists (curry (op =) 0) constr_cards then 0
else Integer.sum constr_cards
@@ -1199,10 +1202,15 @@
(s, unarize_type T) of
SOME n => SOME n
| NONE =>
- if is_fun_type T andalso is_set_type (domain_type T) then
- AList.lookup (op =) built_in_set_consts s
- else
- NONE
+ case s of
+ @{const_name zero_class.zero} =>
+ if is_iterator_type T then SOME 0 else NONE
+ | @{const_name Suc} =>
+ if is_iterator_type (domain_type T) then SOME 0 else NONE
+ | _ => if is_fun_type T andalso is_set_type (domain_type T) then
+ AList.lookup (op =) built_in_set_consts s
+ else
+ NONE
end
(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
val is_built_in_const = is_some oooo arity_of_built_in_const
@@ -1233,12 +1241,12 @@
|> map_filter (try (Refute.specialize_type thy x))
|> filter (curry (op =) (Const x) o term_under_def)
-(* theory -> term -> term option *)
-fun normalized_rhs_of thy t =
+(* term -> term option *)
+fun normalized_rhs_of t =
let
(* term option -> term option *)
fun aux (v as Var _) (SOME t) = SOME (lambda v t)
- | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
+ | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
| aux _ _ = NONE
val (lhs, rhs) =
case t of
@@ -1256,7 +1264,7 @@
NONE
else
x |> def_props_for_const thy [(NONE, false)] false table |> List.last
- |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
+ |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
(* term -> fixpoint_kind *)
@@ -1366,13 +1374,12 @@
||> single |> op ::
end
(* theory -> string * typ list -> term list *)
-fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
+fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
let val abs_T = Type abs_z in
if is_univ_typedef thy abs_T then
[]
else case typedef_info thy abs_s of
- SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
- ...} =>
+ SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
let
val rep_T = instantiate_type thy abs_type abs_T rep_type
val rep_t = Const (Rep_name, abs_T --> rep_T)
@@ -1495,7 +1502,7 @@
[!simp_table, psimp_table]
fun is_inductive_pred hol_ctxt =
is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
-fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
+fun is_equational_fun hol_ctxt =
(is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
@@ -1522,7 +1529,7 @@
| is_constr_pattern _ (Var _) = true
| is_constr_pattern thy t =
case strip_comb t of
- (Const (x as (s, _)), args) =>
+ (Const x, args) =>
is_constr_like thy x andalso forall (is_constr_pattern thy) args
| _ => false
fun is_constr_pattern_lhs thy t =
@@ -1536,9 +1543,9 @@
val unfold_max_depth = 255
(* hol_context -> term -> term *)
-fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
- case_names, def_table, ground_thm_table,
- ersatz_table, ...}) =
+fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
+ def_table, ground_thm_table, ersatz_table,
+ ...}) =
let
(* int -> typ list -> term -> term *)
fun do_term depth Ts t =
@@ -1566,8 +1573,7 @@
handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
| Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
- | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
- $ (t2 as Abs (_, _, t2')) =>
+ | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
map (do_term depth Ts) [t1, t2])
| Const (x as (@{const_name distinct},
@@ -1575,7 +1581,7 @@
$ (t1 as _ $ _) =>
(t1 |> HOLogic.dest_list |> distinctness_formula T'
handle TERM _ => do_const depth Ts t x [t1])
- | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
+ | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
if is_ground_term t1 andalso
exists (Pattern.matches thy o rpair t1)
(Inttab.lookup_list ground_thm_table (hash_term t1)) then
@@ -1831,9 +1837,9 @@
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
end
-(* typ list -> typ -> typ -> term -> term *)
-fun ap_curry [_] _ _ t = t
- | ap_curry arg_Ts tuple_T body_T t =
+(* typ list -> typ -> term -> term *)
+fun ap_curry [_] _ t = t
+ | ap_curry arg_Ts tuple_T t =
let val n = length arg_Ts in
list_abs (map (pair "c") arg_Ts,
incr_boundvars n t
@@ -1843,7 +1849,7 @@
(* int -> term -> int *)
fun num_occs_of_bound_in_term j (t1 $ t2) =
op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
- | num_occs_of_bound_in_term j (Abs (s, T, t')) =
+ | num_occs_of_bound_in_term j (Abs (_, _, t')) =
num_occs_of_bound_in_term (j + 1) t'
| num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
| num_occs_of_bound_in_term _ _ = 0
@@ -1917,8 +1923,7 @@
in aux end
(* hol_context -> styp -> term -> term *)
-fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
- def =
+fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
let
val j = maxidx_of_term def + 1
val (outer, fp_app) = strip_abs def
@@ -1947,7 +1952,7 @@
$ (Const (@{const_name split}, curried_T --> uncurried_T)
$ list_comb (Const step_x, outer_bounds)))
$ list_comb (Const base_x, outer_bounds)
- |> ap_curry tuple_arg_Ts tuple_T bool_T)
+ |> ap_curry tuple_arg_Ts tuple_T)
|> unfold_defs_in_term hol_ctxt
end
@@ -2017,7 +2022,7 @@
(* hol_context -> styp -> term list *)
fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
- psimp_table, ...}) (x as (s, _)) =
+ psimp_table, ...}) x =
case def_props_for_const thy stds fast_descrs (!simp_table) x of
[] => (case def_props_for_const thy stds fast_descrs psimp_table x of
[] => [inductive_pred_axiom hol_ctxt x]
@@ -2044,7 +2049,7 @@
| add_type _ table = table
val table = fold (fold_types (fold_atyps add_type)) ts []
(* typ -> typ *)
- fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
+ fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
| coalesce T = T
in map (map_types (map_atyps coalesce)) ts end
@@ -2122,7 +2127,7 @@
(* int list -> int list -> typ -> typ *)
fun format_type default_format format T =
let
- val T = unarize_and_unbox_type T
+ val T = unarize_unbox_and_uniterize_type T
val format = format |> filter (curry (op <) 0)
in
if forall (curry (op =) 1) format then
@@ -2172,14 +2177,14 @@
((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
val vars = special_bounds ts @ missing_vars
- val ts' = map2 (fn T => fn j =>
- case AList.lookup (op =) (js ~~ ts) j of
- SOME t => do_term t
- | NONE =>
- Var (nth missing_vars
- (find_index (curry (op =) j)
- missing_js)))
- Ts (0 upto max_j)
+ val ts' =
+ map (fn j =>
+ case AList.lookup (op =) (js ~~ ts) j of
+ SOME t => do_term t
+ | NONE =>
+ Var (nth missing_vars
+ (find_index (curry (op =) j) missing_js)))
+ (0 upto max_j)
val t = do_const x' |> fst
val format =
case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
@@ -2251,7 +2256,7 @@
let val t = Const (original_name s, T) in
(t, format_term_type thy def_table formats t)
end)
- |>> map_types unarize_and_unbox_type
+ |>> map_types unarize_unbox_and_uniterize_type
|>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 22 11:57:33 2010 +0100
@@ -169,7 +169,7 @@
| "false" => SOME false
| "true" => SOME true
| "" => SOME true
- | s => raise Option)
+ | _ => raise Option)
handle Option.Option =>
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
error ("Parameter " ^ quote name ^ " must be assigned " ^
@@ -433,7 +433,6 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val thm = #goal (Proof.raw_goal state)
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 22 11:57:33 2010 +0100
@@ -24,7 +24,7 @@
val kk_tuple : bool -> int -> int list -> Kodkod.tuple
val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
val sequential_int_bounds : int -> Kodkod.int_bound list
- val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
+ val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
val bounds_for_built_in_rels_in_formula :
bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
@@ -36,7 +36,7 @@
hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
- int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
+ int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -127,7 +127,7 @@
(* int -> KK.int_bound list *)
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
(* int -> int -> KK.int_bound list *)
-fun pow_of_two_int_bounds bits j0 univ_card =
+fun pow_of_two_int_bounds bits j0 =
let
(* int -> int -> int -> KK.int_bound list *)
fun aux 0 _ _ = []
@@ -141,7 +141,7 @@
fun built_in_rels_in_formula formula =
let
(* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
- fun rel_expr_func (r as KK.Rel (x as (n, j))) =
+ fun rel_expr_func (KK.Rel (x as (n, j))) =
if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
I
else
@@ -304,7 +304,7 @@
(FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
nick)) =
let
- val constr as {delta, epsilon, exclusive, explicit_max, ...} =
+ val {delta, epsilon, exclusive, explicit_max, ...} =
constr_spec dtypes (original_name nick, T1)
in
([(x, bound_comment ctxt debug nick T R)],
@@ -511,7 +511,7 @@
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
end
(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
-and atom_from_rel_expr kk (x as (k, j0)) old_R r =
+and atom_from_rel_expr kk x old_R r =
case old_R of
Func (R1, R2) =>
let
@@ -581,7 +581,7 @@
end
| func_from_no_opt_rel_expr kk Unit R2 old_R r =
(case old_R of
- Vect (k, R') => rel_expr_from_rel_expr kk R2 R' r
+ Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r
| Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r
| Func (Atom (1, _), Formula Neut) =>
(case unopt_rep R2 of
@@ -824,8 +824,8 @@
nfa |> graph_for_nfa |> NfaGraph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
-fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
+(* kodkod_constrs -> nfa_table -> typ -> KK.formula *)
+fun acyclicity_axiom_for_datatype kk nfa start_T =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
@@ -834,20 +834,17 @@
map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
dtypes
|> strongly_connected_sub_nfas
- |> maps (fn nfa =>
- map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
+ |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)
(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
-> KK.rel_expr -> constr_spec -> int -> KK.formula *)
fun sel_axiom_for_sel hol_ctxt binarize j0
- (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
- kk_join, ...}) rel_table dom_r
- ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
+ (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
+ rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
n =
let
- val x as (_, T) =
- binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
- val (r, R, arity) = const_triple rel_table x
+ val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
+ val (r, R, _) = const_triple rel_table x
val R2 = dest_Func R |> snd
val z = (epsilon - delta, delta + j0)
in
@@ -908,10 +905,6 @@
map (const_triple rel_table
o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
(~1 upto num_sels - 1)
- val j0 = case triples |> hd |> #2 of
- Func (Atom (_, j0), _) => j0
- | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
- [R])
val set_r = triples |> hd |> #1
in
if num_sels = 0 then
@@ -962,8 +955,8 @@
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
dtypes
-(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
-fun kodkod_formula_from_nut bits ofs
+(* int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
+fun kodkod_formula_from_nut ofs
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
@@ -1098,7 +1091,7 @@
else
kk_subset (to_rep min_R u1) (to_rep min_R u2)
end)
- | Op2 (Eq, T, R, u1, u2) =>
+ | Op2 (Eq, _, _, u1, u2) =>
(case min_rep (rep_of u1) (rep_of u2) of
Unit => KK.True
| Formula polar =>
@@ -1196,7 +1189,7 @@
case u of
Cst (False, _, Atom _) => false_atom
| Cst (True, _, Atom _) => true_atom
- | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) =>
+ | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>
if R1 = R2 andalso arity_of_rep R1 = 1 then
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
else
@@ -1214,7 +1207,7 @@
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
(rel_expr_from_rel_expr kk min_R R2 r2))
end
- | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
+ | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
| Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
| Cst (Num j, T, R) =>
@@ -1235,7 +1228,7 @@
to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
| Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
- | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel
+ | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
| Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
| Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
| Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
@@ -1303,7 +1296,7 @@
| Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
KK.Iden
| Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
- Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
+ Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
if nat_j0 = int_j0 then
kk_intersect KK.Iden
(kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
@@ -1388,14 +1381,14 @@
(case R of
Func (R1, Formula Neut) => to_rep R1 u1
| Func (Unit, Opt R) => to_guard [u1] R true_atom
- | Func (R1, R2 as Opt _) =>
+ | Func (R1, Opt _) =>
single_rel_rel_let kk
(fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
(rel_expr_to_func kk R1 bool_atom_R
(Func (R1, Formula Neut)) r))
(to_opt R1 u1)
| _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
- | Op1 (Tha, T, R, u1) =>
+ | Op1 (Tha, _, R, u1) =>
if is_opt_rep R then
kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
else
@@ -1413,7 +1406,7 @@
| Op2 (All, T, R as Opt _, u1, u2) =>
to_r (Op1 (Not, T, R,
Op2 (Exist, T, R, u1, Op1 (Not, T, rep_of u2, u2))))
- | Op2 (Exist, T, Opt _, u1, u2) =>
+ | Op2 (Exist, _, Opt _, u1, u2) =>
let val rs1 = untuple to_decl u1 in
if not (is_opt_rep (rep_of u2)) then
kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
@@ -1448,7 +1441,7 @@
(int_expr_from_atom kk (type_of u1)) (r1, r2))))
KK.None)
(to_r u1) (to_r u2))
- | Op2 (The, T, R, u1, u2) =>
+ | Op2 (The, _, R, u1, u2) =>
if is_opt_rep R then
let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
kk_rel_if (kk_one (kk_join r1 true_atom)) (kk_join r1 true_atom)
@@ -1461,7 +1454,7 @@
let val r1 = to_rep (Func (R, Formula Neut)) u1 in
kk_rel_if (kk_one r1) r1 (to_rep R u2)
end
- | Op2 (Eps, T, R, u1, u2) =>
+ | Op2 (Eps, _, R, u1, u2) =>
if is_opt_rep (rep_of u1) then
let
val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1
@@ -1483,7 +1476,7 @@
(kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
r2 (empty_rel_for_rep R))
end
- | Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>
+ | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
let
val f1 = to_f u1
val f2 = to_f u2
@@ -1608,11 +1601,11 @@
false_atom
else
to_apply R u1 u2
- | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) =>
+ | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
to_guard [u1, u2] R (KK.Atom j0)
- | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) =>
+ | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
kk_comprehension (untuple to_decl u1) (to_f u2)
- | Op2 (Lambda, T, Func (_, R2), u1, u2) =>
+ | Op2 (Lambda, _, Func (_, R2), u1, u2) =>
let
val dom_decls = untuple to_decl u1
val ran_schema = atom_schema_of_rep R2
@@ -1650,7 +1643,7 @@
(KK.Atom j0) KK.None)
| _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
| Construct ([u'], _, _, []) => to_r u'
- | Construct (discr_u :: sel_us, T, R, arg_us) =>
+ | Construct (discr_u :: sel_us, _, _, arg_us) =>
let
val set_rs =
map2 (fn sel_u => fn arg_u =>
@@ -1676,7 +1669,7 @@
KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
| to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
(* nut -> KK.expr_assign *)
- and to_expr_assign (FormulaReg (j, _, R)) u =
+ and to_expr_assign (FormulaReg (j, _, _)) u =
KK.AssignFormulaReg (j, to_f u)
| to_expr_assign (RelReg (j, _, R)) u =
KK.AssignRelReg ((arity_of_rep R, j), to_r u)
@@ -1775,7 +1768,7 @@
case arity_of_rep nth_R of
0 => to_guard [u] res_R
(to_rep res_R (Cst (Unity, res_T, Unit)))
- | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
+ | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
end
(* (KK.formula -> KK.formula -> KK.formula)
-> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
@@ -1788,11 +1781,11 @@
in
case min_R of
Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
- | Func (R1, Formula Neut) => set_oper r1 r2
+ | Func (_, Formula Neut) => set_oper r1 r2
| Func (Unit, Atom (2, j0)) =>
connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
- | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
- (kk_join r2 true_atom)
+ | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
+ (kk_join r2 true_atom)
| _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
end
(* (KK.formula -> KK.formula -> KK.formula)
@@ -1815,7 +1808,7 @@
| Vect (k, Atom _) => kk_vect_set_op connective k r1 r2
| Func (_, Formula Neut) => set_oper r1 r2
| Func (Unit, _) => connective3 r1 r2
- | Func (R1, _) =>
+ | Func _ =>
double_rel_rel_let kk
(fn r1 => fn r2 =>
kk_union
@@ -1877,7 +1870,7 @@
| Atom (1, j0) =>
to_guard [arg_u] res_R
(rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
- | Atom (k, j0) =>
+ | Atom (k, _) =>
let
val dom_card = card_of_rep (rep_of arg_u)
val ran_R = Atom (exact_root dom_card k,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 22 11:57:33 2010 +0100
@@ -74,12 +74,12 @@
|> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
? prefix "\<^isub>,"
(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
-fun nth_atom_name pool prefix (T as Type (s, _)) j k =
+fun nth_atom_name pool prefix (Type (s, _)) j k =
let val s' = shortest_name s in
prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
nth_atom_suffix pool s j k
end
- | nth_atom_name pool prefix (T as TFree (s, _)) j k =
+ | nth_atom_name pool prefix (TFree (s, _)) j k =
prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
| nth_atom_name _ _ T _ _ =
raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
@@ -113,20 +113,23 @@
fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
unarize_and_unbox_term t1
| unarize_and_unbox_term (Const (@{const_name PairBox},
- Type ("fun", [T1, Type ("fun", [T2, T3])]))
+ Type ("fun", [T1, Type ("fun", [T2, _])]))
$ t1 $ t2) =
- let val Ts = map unarize_and_unbox_type [T1, T2] in
+ let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
$ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
end
- | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
+ | unarize_and_unbox_term (Const (s, T)) =
+ Const (s, unarize_unbox_and_uniterize_type T)
| unarize_and_unbox_term (t1 $ t2) =
unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
- | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
- | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
+ | unarize_and_unbox_term (Free (s, T)) =
+ Free (s, unarize_unbox_and_uniterize_type T)
+ | unarize_and_unbox_term (Var (x, T)) =
+ Var (x, unarize_unbox_and_uniterize_type T)
| unarize_and_unbox_term (Bound j) = Bound j
| unarize_and_unbox_term (Abs (s, T, t')) =
- Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
+ Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
(* typ -> typ -> (typ * typ) * (typ * typ) *)
fun factor_out_types (T1 as Type ("*", [T11, T12]))
@@ -260,12 +263,12 @@
| mk_tuple _ (t :: _) = t
| mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
-(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
- -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
- -> typ -> rep -> int list list -> term *)
-fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
- ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
- datatypes, ofs, ...} : scope) sel_names rel_table bounds =
+(* bool -> atom_pool -> (string * string) * (string * string) -> scope
+ -> nut list -> nut list -> nut list -> nut NameTable.table
+ -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
+fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
+ ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
+ ofs, ...} : scope) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
(* int list list -> int *)
@@ -357,11 +360,11 @@
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
|> make_plain_fun maybe_opt T1 T2
|> unarize_and_unbox_term
- |> typecast_fun (unarize_and_unbox_type T')
- (unarize_and_unbox_type T1)
- (unarize_and_unbox_type T2)
+ |> typecast_fun (unarize_unbox_and_uniterize_type T')
+ (unarize_unbox_and_uniterize_type T1)
+ (unarize_unbox_and_uniterize_type T2)
(* (typ * int) list -> typ -> typ -> int -> term *)
- fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
+ fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
let
val k1 = card_of_type card_assigns T1
val k2 = card_of_type card_assigns T2
@@ -525,7 +528,7 @@
map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
[[js1], [js2]])
end
- | term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] =
+ | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
term_for_vect seen k R' T1 T2 T' js
| term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
jss =
@@ -548,7 +551,7 @@
in make_fun true T1 T2 T' ts1 ts2 end
| term_for_rep seen T T' (Opt R) jss =
if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
- | term_for_rep seen T _ R jss =
+ | term_for_rep _ T _ R jss =
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
@@ -559,11 +562,11 @@
fun term_for_name pool scope sel_names rel_table bounds name =
let val T = type_of name in
tuple_list_for_name rel_table bounds name
- |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
- bounds T T (rep_of name)
+ |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
+ rel_table bounds T T (rep_of name)
end
-(* Proof.context -> (string * string * string * string) * Proof.context *)
+(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
fun add_wacky_syntax ctxt =
let
(* term -> string *)
@@ -572,17 +575,17 @@
val (maybe_t, thy) =
Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
Mixfix (maybe_mixfix, [1000], 1000)) thy
+ val (abs_t, thy) =
+ Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
+ Mixfix (abs_mixfix, [40], 40)) thy
val (base_t, thy) =
Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
Mixfix (base_mixfix, [1000], 1000)) thy
val (step_t, thy) =
Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
Mixfix (step_mixfix, [1000], 1000)) thy
- val (abs_t, thy) =
- Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
- Mixfix (abs_mixfix, [40], 40)) thy
in
- ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
+ (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
ProofContext.transfer_syntax thy ctxt)
end
@@ -613,18 +616,18 @@
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
-> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
- ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
- user_axioms, debug, binary_ints, destroy_constrs,
- specialize, skolemize, star_linear_preds, uncurry,
- fast_descrs, tac_timeout, evals, case_names, def_table,
- nondef_table, user_nondefs, simp_table, psimp_table,
- intro_table, ground_thm_table, ersatz_table, skolems,
- special_funs, unrolled_preds, wf_cache, constr_cache},
+ ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
+ debug, binary_ints, destroy_constrs, specialize,
+ skolemize, star_linear_preds, uncurry, fast_descrs,
+ tac_timeout, evals, case_names, def_table, nondef_table,
+ user_nondefs, simp_table, psimp_table, intro_table,
+ ground_thm_table, ersatz_table, skolems, special_funs,
+ unrolled_preds, wf_cache, constr_cache},
binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
val pool = Unsynchronized.ref []
- val (wacky_names as (_, base_name, step_name, _), ctxt) =
+ val (wacky_names as (_, base_step_names), ctxt) =
add_wacky_syntax ctxt
val hol_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
@@ -679,13 +682,12 @@
val (oper, (t1, T'), T) =
case name of
FreeName (s, T, _) =>
- let val t = Free (s, unarize_and_unbox_type T) in
+ let val t = Free (s, unarize_unbox_and_uniterize_type T) in
("=", (t, format_term_type thy def_table formats t), T)
end
| ConstName (s, T, _) =>
(assign_operator_for_const (s, T),
- user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
- T)
+ user_friendly_const hol_ctxt base_step_names formats (s, T), T)
| _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
\pretty_for_assign", [name])
val t2 = if rep_of name = Any then
@@ -701,7 +703,8 @@
(* dtype_spec -> Pretty.T *)
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
Pretty.block (Pretty.breaks
- [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
+ [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
+ Pretty.str "=",
Pretty.enum "," "{" "}"
(map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
(if complete then [] else [Pretty.str unrep]))])
@@ -746,7 +749,8 @@
val free_names =
map (fn x as (s, T) =>
case filter (curry (op =) x
- o pairf nickname_of (unarize_and_unbox_type o type_of))
+ o pairf nickname_of
+ (unarize_unbox_and_uniterize_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
@@ -767,7 +771,7 @@
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
-> KK.raw_bound list -> term -> bool option *)
-fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
+fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 22 11:57:33 2010 +0100
@@ -45,7 +45,7 @@
exception CTYPE of string * ctype list
(* string -> unit *)
-fun print_g (s : string) = ()
+fun print_g (_ : string) = ()
(* var -> string *)
val string_for_var = signed_string_of_int
@@ -265,7 +265,7 @@
end
(* cdata -> styp -> ctype *)
-fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
+fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
...}) (x as (_, T)) =
if could_exist_alpha_sub_ctype thy alpha_T T then
case AList.lookup (op =) (!constr_cache) x of
@@ -339,7 +339,7 @@
| (S Minus, S Plus) => NONE
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
| _ => do_sign_atom_comp Eq [] a1 a2 accum)
- | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
+ | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
@@ -367,7 +367,7 @@
(accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
handle Library.UnequalLengths =>
raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
- | do_ctype_comp cmp xs (CType _) (CType _) accum =
+ | do_ctype_comp _ _ (CType _) (CType _) accum =
accum (* no need to compare them thanks to the cache *)
| do_ctype_comp _ _ C1 C2 _ =
raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
@@ -435,13 +435,6 @@
val add_ctype_is_right_unique = add_notin_ctype_fv Minus
val add_ctype_is_right_total = add_notin_ctype_fv Plus
-(* constraint_set -> constraint_set -> constraint_set *)
-fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
- (case SOME lits1 |> fold do_literal lits2 of
- NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
- | SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2))
- | unite _ _ = UnsolvableCSet
-
(* sign -> bool *)
fun bool_from_sign Plus = false
| bool_from_sign Minus = true
@@ -480,10 +473,6 @@
SOME b => (x, sign_from_bool b) :: accum
| NONE => accum) (max_var downto 1) lits
-(* literal list -> sign_atom -> sign option *)
-fun lookup_sign_atom _ (S sn) = SOME sn
- | lookup_sign_atom lit (V x) = AList.lookup (op =) lit x
-
(* comp -> string *)
fun string_for_comp (a1, a2, cmp, xs) =
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
@@ -522,9 +511,6 @@
| _ => NONE
end
-(* var -> constraint_set -> bool *)
-val is_solvable = is_some oo solve
-
type ctype_schema = ctype * constraint_set
type ctype_context =
{bounds: ctype list,
@@ -545,8 +531,8 @@
handle List.Empty => initial_gamma
(* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
- def_table, ...},
+fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
+ def_table, ...},
alpha_T, max_fresh, ...}) =
let
(* typ -> ctype *)
@@ -765,7 +751,7 @@
| Var _ => (print_g "*** Var"; unsolvable)
| Bound j => (nth bounds j, accum)
| Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
- | Abs (s, T, t') =>
+ | Abs (_, T, t') =>
((case t' of
t1' $ Bound 0 =>
if not (loose_bvar1 (t1', 0)) then
@@ -806,7 +792,7 @@
in do_term end
(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
+fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
@@ -814,7 +800,7 @@
val do_term = consider_term cdata
(* sign -> term -> accumulator -> accumulator *)
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
- | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
+ | do_formula sn t (accum as (gamma, cset)) =
let
(* term -> accumulator -> accumulator *)
val do_co_formula = do_formula sn
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 22 11:57:33 2010 +0100
@@ -7,7 +7,6 @@
signature NITPICK_NUT =
sig
- type special_fun = Nitpick_HOL.special_fun
type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
@@ -467,7 +466,7 @@
| factorize z = [z]
(* hol_context -> op2 -> term -> nut *)
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -518,11 +517,21 @@
val t1 = list_comb (t0, ts')
val T1 = fastype_of1 (Ts, t1)
in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
+ (* styp -> term list -> term *)
+ fun construct (x as (_, T)) ts =
+ case num_binder_types T - length ts of
+ 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
+ o nth_sel_for_constr x)
+ (~1 upto num_sels_for_constr_type T - 1),
+ body_type T, Any,
+ ts |> map (`(curry fastype_of1 Ts))
+ |> maps factorize |> map (sub o snd))
+ | k => sub (eta_expand Ts t k)
in
case strip_comb t of
(Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
do_quantifier All s T t1
- | (t0 as Const (@{const_name all}, T), [t1]) =>
+ | (t0 as Const (@{const_name all}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
| (Const (@{const_name "==>"}, _), [t1, t2]) =>
@@ -538,11 +547,11 @@
| (Const (@{const_name True}, T), []) => Cst (True, T, Any)
| (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
do_quantifier All s T t1
- | (t0 as Const (@{const_name All}, T), [t1]) =>
+ | (t0 as Const (@{const_name All}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
do_quantifier Exist s T t1
- | (t0 as Const (@{const_name Ex}, T), [t1]) =>
+ | (t0 as Const (@{const_name Ex}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
| (t0 as Const (@{const_name The}, T), [t1]) =>
if fast_descrs then
@@ -568,7 +577,7 @@
| (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
sub t1, sub_abs s T' t2)
- | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
+ | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
sub (t0 $ t1 $ eta_expand Ts t2 1)
| (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
| (Const (@{const_name Pair}, T), [t1, t2]) =>
@@ -595,7 +604,10 @@
Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
| (Const (@{const_name image}, T), [t1, t2]) =>
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
- | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
+ | (Const (x as (s as @{const_name Suc}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Suc, T, Any)
+ else if is_constr thy stds x then construct x []
+ else ConstName (s, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
(if is_finite_type hol_ctxt (domain_type T) then
Cst (True, bool_T, Any)
@@ -604,14 +616,9 @@
| _ => Op1 (Finite, bool_T, Any, sub t1))
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
| (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
- if is_built_in_const thy stds false x then
- Cst (Num 0, T, Any)
- else if is_constr thy stds x then
- let val (s', T') = discr_for_constr x in
- Construct ([ConstName (s', T', Any)], T, Any, [])
- end
- else
- ConstName (s, T, Any)
+ if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
+ else if is_constr thy stds x then construct x []
+ else ConstName (s, T, Any)
| (Const (x as (s as @{const_name one_class.one}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
else ConstName (s, T, Any)
@@ -631,7 +638,7 @@
| (Const (x as (s as @{const_name div_class.div}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Divide, T, Any)
else ConstName (s, T, Any)
- | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
+ | (t0 as Const (x as (@{const_name ord_class.less}, _)),
ts as [t1, t2]) =>
if is_built_in_const thy stds false x then
Op2 (Less, bool_T, Any, sub t1, sub t2)
@@ -642,7 +649,7 @@
[t1, t2]) =>
Op2 (Subset, bool_T, Any, sub t1, sub t2)
(* FIXME: find out if this case is necessary *)
- | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
+ | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
ts as [t1, t2]) =>
if is_built_in_const thy stds false x then
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
@@ -660,7 +667,7 @@
else
ConstName (s, T, Any)
| (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
- | (Const (@{const_name is_unknown}, T), [t1]) =>
+ | (Const (@{const_name is_unknown}, _), [t1]) =>
Op1 (IsUnknown, bool_T, Any, sub t1)
| (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
Op1 (Tha, T2, Any, sub t1)
@@ -681,14 +688,7 @@
Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
if is_constr thy stds x then
- case num_binder_types T - length ts of
- 0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
- o nth_sel_for_constr x)
- (~1 upto num_sels_for_constr_type T - 1),
- body_type T, Any,
- ts |> map (`(curry fastype_of1 Ts))
- |> maps factorize |> map (sub o snd))
- | k => sub (eta_expand Ts t k)
+ construct x ts
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
else
@@ -726,8 +726,8 @@
in (v :: vs, NameTable.update (v, R) table) end
(* scope -> bool -> nut -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
- ofs, ...}) all_exact v (vs, table) =
+fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+ (vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
val R = (if is_abs_fun thy x then
@@ -904,8 +904,7 @@
| untuple f u = if rep_of u = Unit then [] else [f u]
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
-fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
- bits, datatypes, ofs, ...})
+fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
unsound table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
@@ -991,7 +990,7 @@
Cst (cst, T, best_set_rep_for_type scope T)
| Op1 (Not, T, _, u1) =>
(case gsub def (flip_polarity polar) u1 of
- Op2 (Triad, T, R, u11, u12) =>
+ Op2 (Triad, T, _, u11, u12) =>
triad (s_op1 Not T (Formula Pos) u12)
(s_op1 Not T (Formula Neg) u11)
| u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
@@ -1138,7 +1137,7 @@
else
unopt_rep R
in s_op2 Lambda T R u1' u2' end
- | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
+ | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
| Op2 (oper, T, _, u1, u2) =>
if oper = All orelse oper = Exist then
let
@@ -1307,7 +1306,7 @@
end
| shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
- | shape_tuple T R [u] =
+ | shape_tuple T _ [u] =
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
| shape_tuple T Unit [] = Cst (Unity, T, Unit)
| shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
@@ -1390,7 +1389,6 @@
let
val bs = untuple I u1
val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
- val u11 = rename_vars_in_nut pool table' u1
in
Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
rename_vars_in_nut pool table u2,
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 11:57:33 2010 +0100
@@ -261,14 +261,10 @@
(* bool -> int -> int -> int -> kodkod_constrs *)
fun kodkod_constrs optim nat_card int_card main_j0 =
let
- val false_atom = Atom main_j0
- val true_atom = Atom (main_j0 + 1)
-
(* bool -> int *)
val from_bool = atom_for_bool main_j0
(* int -> rel_expr *)
fun from_nat n = Atom (n + main_j0)
- val from_int = Atom o atom_for_int (int_card, main_j0)
(* int -> int *)
fun to_nat j = j - main_j0
val to_int = int_for_atom (int_card, main_j0)
@@ -415,7 +411,7 @@
fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
| s_subset (Atom j) (AtomSeq (k, j0)) =
formula_for_bool (j >= j0 andalso j < j0 + k)
- | s_subset (r1 as Union (r11, r12)) r2 =
+ | s_subset (Union (r11, r12)) r2 =
s_and (s_subset r11 r2) (s_subset r12 r2)
| s_subset r1 (r2 as Union (r21, r22)) =
if is_one_rel_expr r1 then
@@ -516,7 +512,7 @@
| s_join (r1 as RelIf (f, r11, r12)) r2 =
if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
else Join (r1, r2)
- | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
+ | s_join (r1 as Atom j1) (r2 as Rel (x as (2, _))) =
if x = suc_rel then
let val n = to_nat j1 + 1 in
if n < nat_card then from_nat n else None
@@ -528,7 +524,7 @@
s_project (s_join r21 r1) is
else
Join (r1, r2)
- | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
+ | s_join r1 (Join (r21, r22 as Rel (x as (3, _)))) =
((if x = nat_add_rel then
case (r21, r1) of
(Atom j1, Atom j2) =>
@@ -613,7 +609,6 @@
in aux (arity_of_rel_expr r) r end
(* rel_expr -> rel_expr -> rel_expr *)
- fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
| s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
@@ -624,7 +619,6 @@
(* rel_expr -> rel_expr *)
fun d_not3 r = Join (r, Rel not3_rel)
(* rel_expr -> rel_expr -> rel_expr *)
- fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
in
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 11:57:33 2010 +0100
@@ -87,10 +87,9 @@
SOME n =>
if n >= 2 then
let
- val (arg_Ts, rest_T) = strip_n_binders n T
+ val arg_Ts = strip_n_binders n T |> fst
val j =
- if hd arg_Ts = @{typ bisim_iterator} orelse
- is_fp_iterator_type (hd arg_Ts) then
+ if is_iterator_type (hd arg_Ts) then
1
else case find_index (not_equal bool_T) arg_Ts of
~1 => n
@@ -363,8 +362,8 @@
fun fresh_value_var Ts k n j t =
Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
-(* typ list -> int -> term -> bool *)
-fun has_heavy_bounds_or_vars Ts level t =
+(* typ list -> term -> bool *)
+fun has_heavy_bounds_or_vars Ts t =
let
(* typ list -> bool *)
fun aux [] = false
@@ -381,7 +380,7 @@
Const x =>
if not relax andalso is_constr thy stds x andalso
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
- has_heavy_bounds_or_vars Ts level t_comb andalso
+ has_heavy_bounds_or_vars Ts t_comb andalso
not (loose_bvar (t_comb, level)) then
let
val (j, seen) = case find_index (curry (op =) t_comb) seen of
@@ -629,7 +628,7 @@
$ Abs (s, T, kill ss Ts ts))
| kill _ _ _ = raise UnequalLengths
(* string list -> typ list -> term -> term *)
- fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
+ fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
gather (ss @ [s1]) (Ts @ [T1]) t1
| gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
| gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
@@ -704,7 +703,7 @@
| @{const "op -->"} $ t1 $ t2 =>
@{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
$ aux ss Ts js depth polar t2
- | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
+ | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js depth polar t2
| Const (x as (s, T)) =>
if is_inductive_pred hol_ctxt x andalso
@@ -843,7 +842,7 @@
val bound_var_prefix = "b"
(* hol_context -> int -> term -> term *)
-fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
+fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
special_funs, ...}) depth t =
if not specialize orelse depth > special_max_depth then
t
@@ -919,8 +918,8 @@
val cong_var_prefix = "c"
-(* styp -> special_triple -> special_triple -> term *)
-fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
+(* typ -> special_triple -> special_triple -> term *)
+fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
let
val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
val Ts = binder_types T
@@ -959,28 +958,28 @@
fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
(j2 ~~ t2, j1 ~~ t1)
- (* styp -> special_triple list -> special_triple list -> special_triple list
+ (* typ -> special_triple list -> special_triple list -> special_triple list
-> term list -> term list *)
fun do_pass_1 _ [] [_] [_] = I
- | do_pass_1 x skipped _ [] = do_pass_2 x skipped
- | do_pass_1 x skipped all (z :: zs) =
+ | do_pass_1 T skipped _ [] = do_pass_2 T skipped
+ | do_pass_1 T skipped all (z :: zs) =
case filter (is_more_specific z) all
|> sort (int_ord o pairself generality) of
- [] => do_pass_1 x (z :: skipped) all zs
- | (z' :: _) => cons (special_congruence_axiom x z z')
- #> do_pass_1 x skipped all zs
- (* styp -> special_triple list -> term list -> term list *)
+ [] => do_pass_1 T (z :: skipped) all zs
+ | (z' :: _) => cons (special_congruence_axiom T z z')
+ #> do_pass_1 T skipped all zs
+ (* typ -> special_triple list -> term list -> term list *)
and do_pass_2 _ [] = I
- | do_pass_2 x (z :: zs) =
- fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
- in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
+ | do_pass_2 T (z :: zs) =
+ fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
+ in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end
(** Axiom selection **)
(* Similar to "Refute.specialize_type" but returns all matches rather than only
the first (preorder) match. *)
(* theory -> styp -> term -> term list *)
-fun multi_specialize_type thy slack (x as (s, T)) t =
+fun multi_specialize_type thy slack (s, T) t =
let
(* term -> (typ * term) list -> (typ * term) list *)
fun aux (Const (s', T')) ys =
@@ -1062,7 +1061,7 @@
is_built_in_const thy stds fast_descrs x then
accum
else
- let val accum as (xs, _) = (x :: xs, axs) in
+ let val accum = (x :: xs, axs) in
if depth > axioms_max_depth then
raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
\add_axioms_for_term",
@@ -1130,7 +1129,7 @@
| @{typ unit} => I
| TFree (_, S) => add_axioms_for_sort depth T S
| TVar (_, S) => add_axioms_for_sort depth T S
- | Type (z as (s, Ts)) =>
+ | Type (z as (_, Ts)) =>
fold (add_axioms_for_type depth) Ts
#> (if is_pure_typedef thy T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
@@ -1192,7 +1191,7 @@
((if is_constr_like thy x then
if length args = num_binder_types T then
case hd args of
- Const (x' as (_, T')) $ t' =>
+ Const (_, T') $ t' =>
if domain_type T' = body_type T andalso
forall (uncurry (is_nth_sel_on t'))
(index_seq 0 (length args) ~~ args) then
@@ -1276,13 +1275,13 @@
paper). *)
val quantifier_cluster_threshold = 7
-(* theory -> term -> term *)
-fun push_quantifiers_inward thy =
+(* term -> term *)
+val push_quantifiers_inward =
let
(* string -> string list -> typ list -> term -> term *)
fun aux quant_s ss Ts t =
(case t of
- (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
+ Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
if s0 = quant_s then
aux s0 (s1 :: ss) (T1 :: Ts) t1
else if quant_s = "" andalso
@@ -1406,8 +1405,8 @@
val table =
Termtab.empty |> uncurry
? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
- (* bool -> bool -> term -> term *)
- fun do_rest def core =
+ (* bool -> term -> term *)
+ fun do_rest def =
binarize ? binarize_nat_and_int_in_term
#> uncurry ? uncurry_term table
#> box ? box_fun_and_pair_in_term hol_ctxt def
@@ -1419,13 +1418,13 @@
#> destroy_existential_equalities hol_ctxt
#> simplify_constrs_and_sels thy
#> distribute_quantifiers
- #> push_quantifiers_inward thy
+ #> push_quantifiers_inward
#> close_form
#> Term.map_abs_vars shortest_name
in
- (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
+ (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
(got_all_mono_user_axioms, no_poly_user_axioms)),
- do_rest false true core_t, binarize)
+ do_rest false core_t, binarize)
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 22 11:57:33 2010 +0100
@@ -166,7 +166,7 @@
(* rep -> rep list *)
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
- | binder_reps R = []
+ | binder_reps _ = []
(* rep -> rep *)
fun body_rep (Func (_, R2)) = body_rep R2
| body_rep R = R
@@ -272,10 +272,10 @@
(case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
(Unit, Unit) => Unit
| (R1, R2) => Struct [R1, R2])
- | best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
+ | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
(case card_of_type card_assigns T of
1 => if is_some (datatype_spec datatypes T) orelse
- is_fp_iterator_type T then
+ is_iterator_type T then
Atom (1, offset_of_type ofs T)
else
Unit
@@ -332,7 +332,7 @@
| type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R
- | type_schema_of_rep T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
+ | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
(* typ list -> rep list -> typ list *)
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 22 11:57:33 2010 +0100
@@ -136,7 +136,7 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
fun quintuple_for_scope quote
- ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -346,7 +346,7 @@
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
- | aux seen ((T, 0) :: _) = NONE
+ | aux _ ((_, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
(if is_surely_inconsistent_scope_description hol_ctxt binarize
((T, k) :: seen) rest max_assigns then
@@ -359,7 +359,7 @@
in aux [] (rev card_assigns) end
(* theory -> (typ * int) list -> typ * int -> typ * int *)
-fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
+fun repair_iterator_assign thy assigns (T as Type (_, Ts), k) =
(T, if T = @{typ bisim_iterator} then
let
val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
@@ -394,15 +394,15 @@
end
handle Option.Option => NONE
-(* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
-fun offset_table_for_card_assigns thy assigns dtypes =
+(* (typ * int) list -> dtype_spec list -> int Typtab.table *)
+fun offset_table_for_card_assigns assigns dtypes =
let
(* int -> (int * int) list -> (typ * int) list -> int Typtab.table
-> int Typtab.table *)
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
- if k = 1 orelse is_fp_iterator_type T orelse is_integer_type T
- orelse T = @{typ bisim_iterator} orelse is_bit_type T then
+ if k = 1 orelse is_iterator_type T orelse is_integer_type T
+ orelse is_bit_type T then
aux next reusable assigns
else if length (these (Option.map #constrs (datatype_spec dtypes T)))
> 1 then
@@ -421,12 +421,10 @@
(* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
-> constr_spec list -> constr_spec list *)
fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
- num_self_recs num_non_self_recs (self_rec, x as (s, T))
+ num_self_recs num_non_self_recs (self_rec, x as (_, T))
constrs =
let
val max = constr_max max_assigns x
- (* int -> int *)
- fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
(* unit -> int *)
fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
val {delta, epsilon, exclusive, total} =
@@ -496,14 +494,6 @@
concrete = concrete, deep = deep, constrs = constrs}
end
-(* int -> int *)
-fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
-(* scope_desc -> int *)
-fun min_bits_for_max_assigns (_, []) = 0
- | min_bits_for_max_assigns (card_assigns, max_assigns) =
- min_bits_for_nat_value (fold Integer.max
- (map snd card_assigns @ map snd max_assigns) 0)
-
(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
deep_dataTs (desc as (card_assigns, _)) =
@@ -520,7 +510,7 @@
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
- else offset_table_for_card_assigns thy card_assigns datatypes}
+ else offset_table_for_card_assigns card_assigns datatypes}
end
(* theory -> typ list -> (typ option * int list) list
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 11:57:33 2010 +0100
@@ -308,7 +308,7 @@
NameTable.empty
val u = Op1 (Not, type_of u, rep_of u, u)
|> rename_vars_in_nut pool table
- val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
+ val formula = kodkod_formula_from_nut Typtab.empty constrs u
val bounds = map (bound_for_plain_rel ctxt debug) free_rels
val univ_card = univ_card nat_card int_card j0 bounds formula
val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 22 11:57:33 2010 +0100
@@ -92,7 +92,7 @@
val max_exponent = 16384
(* int -> int -> int *)
-fun reasonable_power a 0 = 1
+fun reasonable_power _ 0 = 1
| reasonable_power a 1 = a
| reasonable_power 0 _ = 0
| reasonable_power 1 _ = 1