remove "fast_descs" option from Nitpick;
the option has been unsound for over a year and is too imprecise to be of any use when made sound
--- a/doc-src/Nitpick/nitpick.tex Tue Sep 14 12:52:50 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Tue Sep 14 13:24:18 2010 +0200
@@ -296,40 +296,18 @@
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\
\hbox{}\qquad Constant: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
+\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
\postw
-We can see more clearly now. Since the predicate $P$ isn't true for a unique
-value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
-$a_1$. Since $P~a_1$ is false, the entire formula is falsified.
-
-As an optimization, Nitpick's preprocessor introduced the special constant
-``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
-$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
-satisfying $P~y$. We disable this optimization by passing the
-\textit{full\_descrs} option:
+As the result of an optimization, Nitpick directly assigned a value to the
+subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
+disable this optimization by using the command
\prew
-\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
-\slshape
-Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
-\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
-\hbox{}\qquad\qquad $x = a_3$ \\
-\hbox{}\qquad Constant: \nopagebreak \\
-\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
+\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
\postw
-As the result of another optimization, Nitpick directly assigned a value to the
-subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
-disable this second optimization by using the command
-
-\prew
-\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
-\textit{show\_consts}]
-\postw
-
-we finally get \textit{The}:
+we get \textit{The}:
\prew
\slshape Constant: \nopagebreak \\
@@ -2490,13 +2468,6 @@
{\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
(\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
-\optrue{fast\_descrs}{full\_descrs}
-Specifies whether Nitpick should optimize the definite and indefinite
-description operators (THE and SOME). The optimized versions usually help
-Nitpick generate more counterexamples or at least find them faster, but only the
-unoptimized versions are complete when all types occurring in the formula are
-finite.
-
{\small See also \textit{debug} (\S\ref{output-format}).}
\opnodefault{whack}{term\_list}
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Sep 14 13:24:18 2010 +0200
@@ -892,7 +892,7 @@
nitpick [expect = none]
sorry
-nitpick_params [full_descrs, max_potential = 1]
+nitpick_params [max_potential = 1]
lemma "(THE j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
nitpick [card nat = 2, expect = potential]
@@ -940,7 +940,7 @@
nitpick [card nat = 6, expect = none]
sorry
-nitpick_params [fast_descrs, max_potential = 0]
+nitpick_params [max_potential = 0]
subsection {* Destructors and Recursors *}
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Sep 14 13:24:18 2010 +0200
@@ -21,8 +21,8 @@
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
whacks = [], binary_ints = SOME false, destroy_constrs = false,
- specialize = false, star_linear_preds = false, fast_descrs = false,
- tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
+ specialize = false, star_linear_preds = false, tac_timeout = NONE,
+ evals = [], case_names = [], def_table = def_table,
nondef_table = Symtab.empty, user_nondefs = [],
simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
choice_spec_table = Symtab.empty, intro_table = Symtab.empty,
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 13:24:18 2010 +0200
@@ -34,7 +34,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -108,7 +107,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -207,10 +205,10 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
- fast_descrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
- tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
- atomss, max_potential, max_genuine, check_potential, check_genuine,
- batch_size, ...} = params
+ peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
+ max_threads, show_datatypes, show_consts, evals, formats, atomss,
+ max_potential, max_genuine, check_potential, check_genuine, batch_size,
+ ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
if auto then
@@ -280,14 +278,13 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
- tac_timeout = tac_timeout, evals = evals, case_names = case_names,
- def_table = def_table, nondef_table = nondef_table,
- user_nondefs = user_nondefs, simp_table = simp_table,
- psimp_table = psimp_table, choice_spec_table = choice_spec_table,
- intro_table = intro_table, ground_thm_table = ground_thm_table,
- ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
- special_funs = Unsynchronized.ref [],
+ star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
+ evals = evals, case_names = case_names, def_table = def_table,
+ nondef_table = nondef_table, user_nondefs = user_nondefs,
+ simp_table = simp_table, psimp_table = psimp_table,
+ choice_spec_table = choice_spec_table, intro_table = intro_table,
+ ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+ skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = fold Term.add_frees assm_ts []
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:24:18 2010 +0200
@@ -27,7 +27,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
@@ -181,9 +180,9 @@
val all_axioms_of :
Proof.context -> (term * term) list -> term list * term list * term list
val arity_of_built_in_const :
- theory -> (typ option * bool) list -> bool -> styp -> int option
+ theory -> (typ option * bool) list -> styp -> int option
val is_built_in_const :
- theory -> (typ option * bool) list -> bool -> styp -> bool
+ theory -> (typ option * bool) list -> styp -> bool
val term_under_def : term -> term
val case_const_names :
Proof.context -> (typ option * bool) list -> (string * int) list
@@ -254,7 +253,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
@@ -434,9 +432,6 @@
(@{const_name nat}, 0),
(@{const_name nat_gcd}, 0),
(@{const_name nat_lcm}, 0)]
-val built_in_descr_consts =
- [(@{const_name The}, 1),
- (@{const_name Eps}, 1)]
val built_in_typed_consts =
[((@{const_name zero_class.zero}, int_T), 0),
((@{const_name one_class.one}, int_T), 0),
@@ -1317,15 +1312,14 @@
user_defs @ built_in_defs
in (defs, built_in_nondefs, user_nondefs) end
-fun arity_of_built_in_const thy stds fast_descrs (s, T) =
+fun arity_of_built_in_const thy stds (s, T) =
if s = @{const_name If} then
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
else
let val std_nats = is_standard_datatype thy stds nat_T in
case AList.lookup (op =)
(built_in_consts
- |> std_nats ? append built_in_nat_consts
- |> fast_descrs ? append built_in_descr_consts) s of
+ |> std_nats ? append built_in_nat_consts) s of
SOME n => SOME n
| NONE =>
case AList.lookup (op =)
@@ -1344,7 +1338,7 @@
else
NONE
end
-val is_built_in_const = is_some oooo arity_of_built_in_const
+val is_built_in_const = is_some ooo arity_of_built_in_const
(* This function is designed to work for both real definition axioms and
simplification rules (equational specifications). *)
@@ -1361,8 +1355,8 @@
(* Here we crucially rely on "specialize_type" performing a preorder traversal
of the term, without which the wrong occurrence of a constant could be
matched in the face of overloading. *)
-fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
- if is_built_in_const thy stds fast_descrs x then
+fun def_props_for_const thy stds table (x as (s, _)) =
+ if is_built_in_const thy stds x then
[]
else
these (Symtab.lookup table s)
@@ -1384,12 +1378,11 @@
in fold_rev aux args (SOME rhs) end
fun def_of_const thy table (x as (s, _)) =
- if is_built_in_const thy [(NONE, false)] false x orelse
+ if is_built_in_const thy [(NONE, false)] x orelse
original_name s <> s then
NONE
else
- x |> def_props_for_const thy [(NONE, false)] false table
- |> List.last
+ x |> def_props_for_const thy [(NONE, false)] table |> List.last
|> normalized_rhs_of |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
@@ -1438,16 +1431,14 @@
end
fun fixpoint_kind_of_const thy table x =
- if is_built_in_const thy [(NONE, false)] false x then
- NoFp
- else
- fixpoint_kind_of_rhs (the (def_of_const thy table x))
- handle Option.Option => NoFp
+ if is_built_in_const thy [(NONE, false)] x then NoFp
+ else fixpoint_kind_of_rhs (the (def_of_const thy table x))
+ handle Option.Option => NoFp
-fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
- ...} : hol_context) x =
+fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...}
+ : hol_context) x =
fixpoint_kind_of_const thy def_table x <> NoFp andalso
- not (null (def_props_for_const thy stds fast_descrs intro_table x))
+ not (null (def_props_for_const thy stds intro_table x))
fun is_inductive_pred hol_ctxt (x as (s, _)) =
is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
String.isPrefix lbfp_prefix s
@@ -1532,10 +1523,9 @@
exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
choice_spec_table
-fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
- ...} : hol_context) x =
- exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
- x)))
+fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...}
+ : hol_context) x =
+ exists (fn table => not (null (def_props_for_const thy stds table x)))
[!simp_table, psimp_table]
fun is_equational_fun_but_no_plain_def hol_ctxt =
is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
@@ -1625,8 +1615,8 @@
val def_inline_threshold_for_non_booleans = 20
fun unfold_defs_in_term
- (hol_ctxt as {thy, ctxt, stds, whacks, fast_descrs, case_names,
- def_table, ground_thm_table, ersatz_table, ...}) =
+ (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table,
+ ground_thm_table, ersatz_table, ...}) =
let
fun do_term depth Ts t =
case t of
@@ -1702,7 +1692,7 @@
else
def_inline_threshold_for_non_booleans
val (const, ts) =
- if is_built_in_const thy stds fast_descrs x then
+ if is_built_in_const thy stds x then
(Const x, ts)
else case AList.lookup (op =) case_names s of
SOME n =>
@@ -2046,9 +2036,9 @@
ScnpReconstruct.sizechange_tac]
fun uncached_is_well_founded_inductive_pred
- ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
- : hol_context) (x as (_, T)) =
- case def_props_for_const thy stds fast_descrs intro_table x of
+ ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context)
+ (x as (_, T)) =
+ case def_props_for_const thy stds intro_table x of
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
| intro_ts =>
@@ -2281,10 +2271,10 @@
else
raw_inductive_pred_axiom hol_ctxt x
-fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, fast_descrs, def_table,
- simp_table, 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
+fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, simp_table,
+ psimp_table, ...}) x =
+ case def_props_for_const thy stds (!simp_table) x of
+ [] => (case def_props_for_const thy stds psimp_table x of
[] => (if is_inductive_pred hol_ctxt x then
[inductive_pred_axiom hol_ctxt x]
else case def_of_const thy def_table x of
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Sep 14 13:24:18 2010 +0200
@@ -58,7 +58,6 @@
("destroy_constrs", "true"),
("specialize", "true"),
("star_linear_preds", "true"),
- ("fast_descrs", "true"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
("kodkod_sym_break", "15"),
@@ -91,7 +90,6 @@
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
- ("full_descrs", "fast_descrs"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
("quiet", "verbose"),
@@ -251,7 +249,6 @@
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val star_linear_preds = lookup_bool "star_linear_preds"
- val fast_descrs = lookup_bool "fast_descrs"
val peephole_optim = lookup_bool "peephole_optim"
val datatype_sym_break = lookup_int "datatype_sym_break"
val kodkod_sym_break = lookup_int "kodkod_sym_break"
@@ -282,8 +279,8 @@
user_axioms = user_axioms, assms = assms, whacks = whacks,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
- peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
+ star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
+ datatype_sym_break = datatype_sym_break,
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
show_datatypes = show_datatypes, show_consts = show_consts,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:24:18 2010 +0200
@@ -872,9 +872,9 @@
fun reconstruct_hol_model {show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
- star_linear_preds, fast_descrs, tac_timeout, evals,
- case_names, def_table, nondef_table, user_nondefs,
- simp_table, psimp_table, choice_spec_table, intro_table,
+ star_linear_preds, tac_timeout, evals, case_names,
+ def_table, nondef_table, user_nondefs, simp_table,
+ psimp_table, choice_spec_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)
@@ -889,15 +889,15 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
- tac_timeout = tac_timeout, evals = evals, case_names = case_names,
- def_table = def_table, nondef_table = nondef_table,
- user_nondefs = user_nondefs, simp_table = simp_table,
- psimp_table = psimp_table, choice_spec_table = choice_spec_table,
- intro_table = intro_table, ground_thm_table = ground_thm_table,
- ersatz_table = ersatz_table, skolems = skolems,
- special_funs = special_funs, unrolled_preds = unrolled_preds,
- wf_cache = wf_cache, constr_cache = constr_cache}
+ star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
+ evals = evals, case_names = case_names, def_table = def_table,
+ nondef_table = nondef_table, user_nondefs = user_nondefs,
+ simp_table = simp_table, psimp_table = psimp_table,
+ choice_spec_table = choice_spec_table, intro_table = intro_table,
+ ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+ skolems = skolems, special_funs = special_funs,
+ unrolled_preds = unrolled_preds, wf_cache = wf_cache,
+ constr_cache = constr_cache}
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:24:18 2010 +0200
@@ -549,13 +549,12 @@
consts = consts}
handle List.Empty => initial_gamma (* FIXME: needed? *)
-fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...},
- alpha_T, max_fresh, ...}) =
+fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
+ max_fresh, ...}) =
let
fun is_enough_eta_expanded t =
case strip_comb t of
- (Const x, ts) =>
- the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
+ (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
<= length ts
| _ => true
val mtype_for = fresh_mtype_for_type mdata false
@@ -725,7 +724,7 @@
(mtype_for_sel mdata x, accum)
else if is_constr ctxt stds x then
(mtype_for_constr mdata x, accum)
- else if is_built_in_const thy stds fast_descrs x then
+ else if is_built_in_const thy stds x then
(fresh_mtype_for_type mdata true T, accum)
else
let val M = mtype_for T in
@@ -908,9 +907,9 @@
val bounteous_consts = [@{const_name bisim}]
fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
- | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
+ | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
Term.add_consts t []
- |> filter_out (is_built_in_const thy stds fast_descrs)
+ |> filter_out (is_built_in_const thy stds)
|> (forall (member (op =) harmless_consts o original_name o fst) orf
exists (member (op =) bounteous_consts o fst))
@@ -1022,8 +1021,7 @@
fun fin_fun_constr T1 T2 =
(@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
- ...})
+fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
binarize finitizes alpha_T tsp =
case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
SOME (lits, msp, constr_mtypes) =>
@@ -1074,7 +1072,7 @@
| _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
\term_from_mterm", [T, T'], [])
in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
- else if is_built_in_const thy stds fast_descrs x then
+ else if is_built_in_const thy stds x then
coerce_term hol_ctxt new_Ts T' T t
else if is_constr ctxt stds x then
Const (finitize_constr x)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:24:18 2010 +0200
@@ -430,7 +430,7 @@
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq =
let
fun aux eq ss Ts t =
let
@@ -470,12 +470,6 @@
val t1 = list_comb (t0, ts')
val T1 = fastype_of1 (Ts, t1)
in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
- fun do_description_operator oper undef_s (x as (_, T)) t1 =
- if fast_descrs then
- Op2 (oper, range_type T, Any, sub t1,
- sub (Const (undef_s, range_type T)))
- else
- do_apply (Const x) [t1]
fun do_construct (x as (_, T)) ts =
case num_binder_types T - length ts of
0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
@@ -511,10 +505,6 @@
do_quantifier Exist s T t1
| (t0 as Const (@{const_name Ex}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
- | (Const (x as (@{const_name The}, _)), [t1]) =>
- do_description_operator The @{const_name undefined_fast_The} x t1
- | (Const (x as (@{const_name Eps}, _)), [t1]) =>
- do_description_operator Eps @{const_name undefined_fast_Eps} x t1
| (Const (@{const_name HOL.eq}, T), [t1]) =>
Op1 (SingletonSet, range_type T, Any, sub t1)
| (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
@@ -549,7 +539,7 @@
| (Const (@{const_name image}, T), [t1, t2]) =>
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (x as (s as @{const_name Suc}, T)), []) =>
- if is_built_in_const thy stds false x then Cst (Suc, T, Any)
+ if is_built_in_const thy stds x then Cst (Suc, T, Any)
else if is_constr ctxt stds x then do_construct x []
else ConstName (s, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
@@ -560,27 +550,27 @@
| _ => 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)
+ if is_built_in_const thy stds x then Cst (Num 0, T, Any)
else if is_constr ctxt stds x then do_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)
+ if is_built_in_const thy stds x then Cst (Num 1, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
- if is_built_in_const thy stds false x then Cst (Add, T, Any)
+ if is_built_in_const thy stds x then Cst (Add, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
- if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
+ if is_built_in_const thy stds x then Cst (Subtract, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name times_class.times}, T)), []) =>
- if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
+ if is_built_in_const thy stds x then Cst (Multiply, T, Any)
else ConstName (s, T, Any)
| (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)
+ if is_built_in_const thy stds x then Cst (Divide, T, Any)
else ConstName (s, T, Any)
| (t0 as Const (x as (@{const_name ord_class.less}, _)),
ts as [t1, t2]) =>
- if is_built_in_const thy stds false x then
+ if is_built_in_const thy stds x then
Op2 (Less, bool_T, Any, sub t1, sub t2)
else
do_apply t0 ts
@@ -592,14 +582,14 @@
(* FIXME: find out if this case is necessary *)
| (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
+ if is_built_in_const thy stds x then
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
else
do_apply t0 ts
| (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
| (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
| (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
- if is_built_in_const thy stds false x then
+ if is_built_in_const thy stds x then
let val num_T = domain_type T in
Op2 (Apply, num_T --> num_T, Any,
Cst (Subtract, num_T --> num_T --> num_T, Any),
@@ -613,8 +603,6 @@
| (Const (@{const_name safe_The},
Type (@{type_name fun}, [_, T2])), [t1]) =>
Op1 (SafeThe, T2, Any, sub t1)
- | (Const (x as (@{const_name safe_Eps}, _)), [t1]) =>
- do_description_operator Eps @{const_name undefined_fast_Eps} x t1
| (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
| (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
| (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
@@ -628,7 +616,7 @@
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
else
- (case arity_of_built_in_const thy stds fast_descrs x of
+ (case arity_of_built_in_const thy stds x of
SOME n =>
(case n - length ts of
0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:24:18 2010 +0200
@@ -76,7 +76,7 @@
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
| aux (t as Const (x as (s, _))) args table =
- if is_built_in_const thy [(NONE, true)] true x orelse
+ if is_built_in_const thy [(NONE, true)] x orelse
is_constr_like ctxt x orelse
is_sel s orelse s = @{const_name Sigma} then
table
@@ -127,8 +127,7 @@
(** Boxing **)
-fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
- def orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t =
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
@@ -231,7 +230,7 @@
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
T' --> T'
end
- else if is_built_in_const thy stds fast_descrs x orelse
+ else if is_built_in_const thy stds x orelse
s = @{const_name Sigma} then
T
else if is_constr_like ctxt x then
@@ -732,8 +731,8 @@
forall (op aconv) (ts1 ~~ ts2)
fun specialize_consts_in_term
- (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table,
- simp_table, special_funs, ...}) def depth t =
+ (hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table,
+ special_funs, ...}) def depth t =
if not specialize orelse depth > special_max_depth then
t
else
@@ -743,7 +742,7 @@
fun aux args Ts (Const (x as (s, T))) =
((if not (member (op =) blacklist x) andalso not (null args) andalso
not (String.isPrefix special_prefix s) andalso
- not (is_built_in_const thy stds fast_descrs x) andalso
+ not (is_built_in_const thy stds x) andalso
(is_equational_fun_but_no_plain_def hol_ctxt x orelse
(is_some (def_of_const thy def_table x) andalso
not (is_of_class_const thy x) andalso
@@ -894,8 +893,8 @@
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
- fast_descrs, evals, def_table, nondef_table,
- choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
+ evals, def_table, nondef_table, choice_spec_table,
+ user_nondefs, ...}) assm_ts neg_t =
let
val (def_assm_ts, nondef_assm_ts) =
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
@@ -926,8 +925,7 @@
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if member (op aconv) seen t orelse
- is_built_in_const thy stds fast_descrs x then
+ (if member (op aconv) seen t orelse is_built_in_const thy stds x then
accum
else
let val accum = (t :: seen, axs) in