--- a/NEWS Mon Mar 03 22:33:22 2014 +0100
+++ b/NEWS Mon Mar 03 22:33:22 2014 +0100
@@ -367,6 +367,11 @@
* Nitpick:
- Fixed soundness bug whereby mutually recursive datatypes could take
infinite values.
+ - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
+ "Rep_Integ".
+ - Removed "std" option.
+ - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
+ "hide_types".
* HOL-Multivariate_Analysis:
- type class ordered_real_vector for ordered vector spaces
@@ -812,16 +817,16 @@
INCOMPATIBILITY.
* Nitpick:
- - Added option "spy"
- - Reduce incidence of "too high arity" errors
+ - Added option "spy".
+ - Reduce incidence of "too high arity" errors.
* Sledgehammer:
- Renamed option:
isar_shrink ~> isar_compress
INCOMPATIBILITY.
- - Added options "isar_try0", "spy"
- - Better support for "isar_proofs"
- - MaSh has been fined-tuned and now runs as a local server
+ - Added options "isar_try0", "spy".
+ - Better support for "isar_proofs".
+ - MaSh has been fined-tuned and now runs as a local server.
* Improved support for ad hoc overloading of constants (see also
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).--- a/src/Doc/Nitpick/document/root.tex Mon Mar 03 22:33:22 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex Mon Mar 03 22:33:22 2014 +0100
@@ -609,7 +609,7 @@
\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$''
\\
-\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
@@ -638,7 +638,7 @@
\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
\textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\
-\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\
@@ -667,7 +667,7 @@
\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
%
\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
-\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
@@ -709,7 +709,7 @@
\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
-\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
@@ -726,7 +726,7 @@
\prew
\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
-\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $x = 1/2$ \\
@@ -1048,7 +1048,7 @@
\prew
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
\,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
-\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_1$ \\
@@ -1916,7 +1916,7 @@
\textit{Suc}, \textit{gcd}, or \textit{lcm}.
{\small See also \textit{bits} (\S\ref{scope-of-search}) and
-\textit{show\_datatypes} (\S\ref{output-format}).}
+\textit{show\_types} (\S\ref{output-format}).}
\opdefault{bits}{int\_seq}{\upshape 1--10}
Specifies the number of bits to use to represent natural numbers and integers in
@@ -2079,7 +2079,7 @@
\textit{overlord} (\S\ref{mode-of-operation}), and
\textit{batch\_size} (\S\ref{optimizations}).}
-\opfalse{show\_datatypes}{hide\_datatypes}
+\opfalse{show\_types}{hide\_types}
Specifies whether the subsets used to approximate (co)in\-duc\-tive data\-types should
be displayed as part of counterexamples. Such subsets are sometimes helpful when
investigating whether a potentially spurious counterexample is genuine, but
@@ -2098,7 +2098,7 @@
genuine, but they can clutter the output.
\opnodefault{show\_all}{bool}
-Abbreviation for \textit{show\_datatypes}, \textit{show\_skolems}, and
+Abbreviation for \textit{show\_types}, \textit{show\_skolems}, and
\textit{show\_consts}.
\opdefault{max\_potential}{int}{\upshape 1}--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 22:33:22 2014 +0100
@@ -92,11 +92,11 @@
lemma "hd (xs @ [y, y]) = hd xs"
nitpick [expect = genuine]
-nitpick [show_consts, show_datatypes, expect = genuine]
+nitpick [show_consts, show_types, expect = genuine]
oops
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
-nitpick [show_datatypes, expect = genuine]
+nitpick [show_types, expect = genuine]
oops
@@ -111,7 +111,7 @@
definition C :: three where "C \<equiv> Abs_three 2"
lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
-nitpick [show_datatypes, expect = genuine]
+nitpick [show_types, expect = genuine]
oops
fun my_int_rel where
@@ -127,7 +127,7 @@
unfolding add_raw_def by auto
lemma "add x y = add x x"
-nitpick [show_datatypes, expect = genuine]
+nitpick [show_types, expect = genuine]
oops
ML {*
@@ -142,7 +142,7 @@
*}
lemma "add x y = add x x"
-nitpick [show_datatypes]
+nitpick [show_types]
oops
record point =
@@ -150,11 +150,11 @@
Ycoord :: int
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
-nitpick [show_datatypes, expect = genuine]
+nitpick [show_types, expect = genuine]
oops
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
-nitpick [show_datatypes, expect = genuine]
+nitpick [show_types, expect = genuine]
oops
@@ -217,7 +217,7 @@
oops
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
-nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
+nitpick [bisim_depth = -1, show_types, expect = quasi_genuine]
nitpick [card = 1\<emdash>5, expect = none]
sorry
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 03 22:33:22 2014 +0100
@@ -433,6 +433,7 @@
tuple_set_func: tuple_set -> 'a -> 'a}
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
+
fun fold_tuple_set F tuple_set =
case tuple_set of
TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
@@ -445,18 +446,22 @@
| TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
| TupleAtomSeq _ => #tuple_set_func F tuple_set
| TupleSetReg _ => #tuple_set_func F tuple_set
+
fun fold_tuple_assign F assign =
case assign of
AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
| AssignTupleSet (x, ts) =>
fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
+
fun fold_bound expr_F tuple_F (zs, tss) =
fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
#> fold (fold_tuple_set tuple_F) tss
+
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
fun max_arity univ_card = floor (Math.ln 2147483647.0
/ Math.ln (Real.fromInt univ_card))
+
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
| arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
| arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
@@ -539,6 +544,7 @@
| inline_comment comment =
" /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
" */"
+
fun block_comment "" = ""
| block_comment comment = prefix_lines "// " comment ^ "\n"
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Mar 03 22:33:22 2014 +0100
@@ -74,6 +74,7 @@
else [if dev = ToFile then out_file else ""]) @ markers @
(if dev = ToFile then [out_file] else []) @ args
end)
+
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
| dynamic_entry_for_info incremental
@@ -98,6 +99,7 @@
(name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
dynamic_entry_for_external name dev home exec args [m1, m2, m3]
| dynamic_entry_for_info true _ = NONE
+
fun dynamic_list incremental =
map_filter (dynamic_entry_for_info incremental) static_list
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,21 +7,20 @@
signature NITPICK =
sig
- type styp = Nitpick_Util.styp
type term_postprocessor = Nitpick_Model.term_postprocessor
datatype mode = Auto_Try | Try | Normal | TPTP
type params =
{cards_assigns: (typ option * int list) list,
- maxes_assigns: (styp option * int list) list,
- iters_assigns: (styp option * int list) list,
+ maxes_assigns: ((string * typ) option * int list) list,
+ iters_assigns: ((string * typ) option * int list) list,
bitss: int list,
bisim_depths: int list,
boxes: (typ option * bool option) list,
finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
- wfs: (styp option * bool option) list,
+ wfs: ((string * typ) option * bool option) list,
sat_solver: string,
blocking: bool,
falsify: bool,
@@ -45,7 +44,7 @@
timeout: Time.time,
tac_timeout: Time.time,
max_threads: int,
- show_datatypes: bool,
+ show_types: bool,
show_skolems: bool,
show_consts: bool,
evals: term list,
@@ -65,7 +64,8 @@
val unknownN : string
val register_frac_type : string -> (string * string) list -> theory -> theory
val unregister_frac_type : string -> theory -> theory
- val register_codatatype : typ -> string -> styp list -> theory -> theory
+ val register_codatatype : typ -> string -> (string * typ) list -> theory ->
+ theory
val unregister_codatatype : typ -> theory -> theory
val register_term_postprocessor :
typ -> term_postprocessor -> theory -> theory
@@ -99,14 +99,14 @@
type params =
{cards_assigns: (typ option * int list) list,
- maxes_assigns: (styp option * int list) list,
- iters_assigns: (styp option * int list) list,
+ maxes_assigns: ((string * typ) option * int list) list,
+ iters_assigns: ((string * typ) option * int list) list,
bitss: int list,
bisim_depths: int list,
boxes: (typ option * bool option) list,
finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
- wfs: (styp option * bool option) list,
+ wfs: ((string * typ) option * bool option) list,
sat_solver: string,
blocking: bool,
falsify: bool,
@@ -130,7 +130,7 @@
timeout: Time.time,
tac_timeout: Time.time,
max_threads: int,
- show_datatypes: bool,
+ show_types: bool,
show_skolems: bool,
show_consts: bool,
evals: term list,
@@ -181,13 +181,14 @@
val isabelle_wrong_message =
"Something appears to be wrong with your Isabelle installation."
-fun java_not_found_message () =
+val java_not_found_message =
"Java could not be launched. " ^ isabelle_wrong_message
-fun java_too_old_message () =
+val java_too_old_message =
"The Java version is too old. " ^ isabelle_wrong_message
-fun kodkodi_not_installed_message () =
+val kodkodi_not_installed_message =
"Nitpick requires the external Java program Kodkodi."
-fun kodkodi_too_old_message () = "The installed Kodkodi version is too old."
+val kodkodi_too_old_message = "The installed Kodkodi version is too old."
+
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
@@ -205,6 +206,7 @@
val syntactic_sorts =
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
@{sort numeral}
+
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
subset (op =) (S, syntactic_sorts)
| has_tfree_syntactic_sort _ = false
@@ -229,9 +231,9 @@
overlord, spy, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
total_consts, needs, peephole_optim, datatype_sym_break,
- kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
- show_skolems, show_consts, evals, formats, atomss, max_potential,
- max_genuine, check_potential, check_genuine, batch_size, ...} = params
+ kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
+ show_consts, evals, formats, atomss, max_potential, max_genuine,
+ check_potential, check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
fun pprint print =
if mode = Auto_Try then
@@ -652,7 +654,7 @@
"% SZS output start FiniteModel")
val (reconstructed_model, codatatypes_ok) =
reconstruct_hol_model
- {show_datatypes = show_datatypes, show_skolems = show_skolems,
+ {show_types = show_types, show_skolems = show_skolems,
show_consts = show_consts}
scope formats atomss real_frees pseudo_frees free_names sel_names
nonsel_names rel_table bounds
@@ -771,16 +773,16 @@
case KK.solve_any_problem debug overlord deadline max_threads
max_solutions (map fst problems) of
KK.JavaNotFound =>
- (print_nt java_not_found_message;
+ (print_nt (K java_not_found_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.JavaTooOld =>
- (print_nt java_too_old_message;
+ (print_nt (K java_too_old_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.KodkodiNotInstalled =>
- (print_nt kodkodi_not_installed_message;
+ (print_nt (K kodkodi_not_installed_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.KodkodiTooOld =>
- (print_nt kodkodi_too_old_message;
+ (print_nt (K kodkodi_too_old_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
@@ -1029,7 +1031,7 @@
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
that the "Nitpick_Examples" can be processed on any machine. *)
- (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
+ (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
("no_kodkodi", state))
else
let
@@ -1062,6 +1064,7 @@
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
Variable.is_fixed ctxt s
| is_fixed_equation _ _ = false
+
fun extract_fixed_frees ctxt (assms, t) =
let
val (subst, other_assms) =--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 22:33:22 2014 +0100
@@ -71,7 +71,7 @@
("verbose", "false"),
("overlord", "false"),
("spy", "false"),
- ("show_datatypes", "false"),
+ ("show_types", "false"),
("show_skolems", "true"),
("show_consts", "false"),
("format", "1"),
@@ -100,7 +100,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_spy", "spy"),
- ("hide_datatypes", "show_datatypes"),
+ ("hide_types", "show_types"),
("hide_skolems", "show_skolems"),
("hide_consts", "show_consts"),
("trust_potential", "check_potential"),
@@ -125,6 +125,7 @@
else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
else NONE
| some_name => some_name
+
fun normalize_raw_param (name, value) =
case unnegate_param_name name of
SOME name' => [(name', case value of
@@ -133,7 +134,7 @@
| [] => ["false"]
| _ => value)]
| NONE => if name = "show_all" then
- [("show_datatypes", value), ("show_skolems", value),
+ [("show_types", value), ("show_skolems", value),
("show_consts", value)]
else
[(name, value)]
@@ -267,7 +268,7 @@
val tac_timeout = lookup_time "tac_timeout"
val max_threads =
if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
- val show_datatypes = debug orelse lookup_bool "show_datatypes"
+ val show_types = debug orelse lookup_bool "show_types"
val show_skolems = debug orelse lookup_bool "show_skolems"
val show_consts = debug orelse lookup_bool "show_consts"
val evals = lookup_term_list_option_polymorphic "eval" |> these
@@ -297,7 +298,7 @@
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_skolems = show_skolems,
+ show_types = show_types, show_skolems = show_skolems,
show_consts = show_consts, evals = evals, formats = formats,
atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
check_potential = check_potential, check_genuine = check_genuine,--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,18 +7,17 @@
signature NITPICK_HOL =
sig
- type styp = Nitpick_Util.styp
type const_table = term list Symtab.table
- type special_fun = (styp * int list * term list) * styp
- type unrolled = styp * styp
- type wf_cache = (styp * (bool * bool)) list
+ type special_fun = ((string * typ) * int list * term list) * (string * typ)
+ type unrolled = (string * typ) * (string * typ)
+ type wf_cache = ((string * typ) * (bool * bool)) list
type hol_context =
{thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
- wfs: (styp option * bool option) list,
+ wfs: ((string * typ) option * bool option) list,
user_axioms: bool option,
debug: bool,
whacks: term list,
@@ -44,7 +43,7 @@
special_funs: special_fun list Unsynchronized.ref,
unrolled_preds: unrolled list Unsynchronized.ref,
wf_cache: wf_cache Unsynchronized.ref,
- constr_cache: (typ * styp list) list Unsynchronized.ref}
+ constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}
datatype fixpoint_kind = Lfp | Gfp | NoFp
datatype boxability =
@@ -81,7 +80,7 @@
val shorten_names_in_term : term -> term
val strict_type_match : theory -> typ * typ -> bool
val type_match : theory -> typ * typ -> bool
- val const_match : theory -> styp * styp -> bool
+ val const_match : theory -> (string * typ) * (string * typ) -> bool
val term_match : theory -> term * term -> bool
val frac_from_term_pair : typ -> term -> term -> term
val is_TFree : typ -> bool
@@ -105,41 +104,40 @@
val elem_type : typ -> typ
val pseudo_domain_type : typ -> typ
val pseudo_range_type : typ -> typ
- val const_for_iterator_type : typ -> styp
+ val const_for_iterator_type : typ -> string * typ
val strip_n_binders : int -> typ -> typ list * typ
val nth_range_type : int -> typ -> typ
val num_factors_in_type : typ -> int
val curried_binder_types : typ -> typ list
val mk_flat_tuple : typ -> term list -> term
val dest_n_tuple : int -> term -> term list
- val is_real_datatype : theory -> string -> bool
val is_codatatype : Proof.context -> typ -> bool
val is_quot_type : Proof.context -> typ -> bool
val is_pure_typedef : Proof.context -> typ -> bool
val is_univ_typedef : Proof.context -> typ -> bool
val is_datatype : Proof.context -> typ -> bool
- val is_record_constr : styp -> bool
- val is_record_get : theory -> styp -> bool
- val is_record_update : theory -> styp -> bool
- val is_abs_fun : Proof.context -> styp -> bool
- val is_rep_fun : Proof.context -> styp -> bool
- val is_quot_abs_fun : Proof.context -> styp -> bool
- val is_quot_rep_fun : Proof.context -> styp -> bool
- val mate_of_rep_fun : Proof.context -> styp -> styp
- val is_constr_like : Proof.context -> styp -> bool
- val is_constr_like_injective : Proof.context -> styp -> bool
- val is_constr : Proof.context -> styp -> bool
+ val is_record_constr : string * typ -> bool
+ val is_record_get : theory -> string * typ -> bool
+ val is_record_update : theory -> string * typ -> bool
+ val is_abs_fun : Proof.context -> string * typ -> bool
+ val is_rep_fun : Proof.context -> string * typ -> bool
+ val is_quot_abs_fun : Proof.context -> string * typ -> bool
+ val is_quot_rep_fun : Proof.context -> string * typ -> bool
+ val mate_of_rep_fun : Proof.context -> string * typ -> string * typ
+ val is_nonfree_constr : Proof.context -> string * typ -> bool
+ val is_free_constr : Proof.context -> string * typ -> bool
+ val is_constr : Proof.context -> string * typ -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
val binarize_nat_and_int_in_type : typ -> typ
val binarize_nat_and_int_in_term : term -> term
- val discr_for_constr : styp -> styp
+ val discr_for_constr : string * typ -> string * typ
val num_sels_for_constr_type : typ -> int
val nth_sel_name_for_constr_name : string -> int -> string
- val nth_sel_for_constr : styp -> int -> styp
+ val nth_sel_for_constr : string * typ -> int -> string * typ
val binarized_and_boxed_nth_sel_for_constr :
- hol_context -> bool -> styp -> int -> styp
+ hol_context -> bool -> string * typ -> int -> string * typ
val sel_no_from_name : string -> int
val close_form : term -> term
val distinctness_formula : typ -> term list -> term
@@ -155,18 +153,20 @@
(string * string) list -> morphism -> Context.generic -> Context.generic
val register_ersatz_global : (string * string) list -> theory -> theory
val register_codatatype :
- typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
+ typ -> string -> (string * typ) list -> morphism -> Context.generic ->
+ Context.generic
val register_codatatype_global :
- typ -> string -> styp list -> theory -> theory
+ typ -> string -> (string * typ) list -> theory -> theory
val unregister_codatatype :
typ -> morphism -> Context.generic -> Context.generic
val unregister_codatatype_global : typ -> theory -> theory
- val datatype_constrs : hol_context -> typ -> styp list
+ val datatype_constrs : hol_context -> typ -> (string * typ) list
val binarized_and_boxed_datatype_constrs :
- hol_context -> bool -> typ -> styp list
+ hol_context -> bool -> typ -> (string * typ) list
val num_datatype_constrs : hol_context -> typ -> int
val constr_name_for_sel_like : string -> string
- val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
+ val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
+ string * typ -> string * typ
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_exact_card_of_type :
@@ -178,17 +178,17 @@
typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
val s_betapply : typ list -> term * term -> term
val s_betapplys : typ list -> term * term list -> term
- val discriminate_value : hol_context -> styp -> term -> term
+ val discriminate_value : hol_context -> string * typ -> term -> term
val select_nth_constr_arg :
- Proof.context -> styp -> term -> int -> typ -> term
- val construct_value : Proof.context -> styp -> term list -> term
+ Proof.context -> string * typ -> term -> int -> typ -> term
+ val construct_value : Proof.context -> string * typ -> term list -> term
val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val special_bounds : term list -> (indexname * typ) list
val is_funky_typedef : Proof.context -> typ -> bool
val all_defs_of : theory -> (term * term) list -> term list
val all_nondefs_of : Proof.context -> (term * term) list -> term list
- val arity_of_built_in_const : styp -> int option
- val is_built_in_const : styp -> bool
+ val arity_of_built_in_const : string * typ -> int option
+ val is_built_in_const : string * typ -> bool
val term_under_def : term -> term
val case_const_names : Proof.context -> (string * int) list
val unfold_defs_in_term : hol_context -> term -> term
@@ -206,29 +206,31 @@
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : Proof.context -> (string * string) list
val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
- val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
+ val inverse_axioms_for_rep_fun : Proof.context -> string * typ -> term list
val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
val optimized_quot_type_axioms :
Proof.context -> string * typ list -> term list
- val def_of_const : theory -> const_table * const_table -> styp -> term option
+ val def_of_const : theory -> const_table * const_table -> string * typ ->
+ term option
val fixpoint_kind_of_rhs : term -> fixpoint_kind
val fixpoint_kind_of_const :
theory -> const_table * const_table -> string * typ -> fixpoint_kind
- val is_real_inductive_pred : hol_context -> styp -> bool
+ val is_raw_inductive_pred : hol_context -> string * typ -> bool
val is_constr_pattern : Proof.context -> term -> bool
val is_constr_pattern_lhs : Proof.context -> term -> bool
val is_constr_pattern_formula : Proof.context -> term -> bool
val nondef_props_for_const :
- theory -> bool -> const_table -> styp -> term list
- val is_choice_spec_fun : hol_context -> styp -> bool
+ theory -> bool -> const_table -> string * typ -> term list
+ val is_choice_spec_fun : hol_context -> string * typ -> bool
val is_choice_spec_axiom : theory -> const_table -> term -> bool
- val is_real_equational_fun : hol_context -> styp -> bool
- val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool
+ val is_raw_equational_fun : hol_context -> string * typ -> bool
+ val is_equational_fun : hol_context -> string * typ -> bool
val codatatype_bisim_axioms : hol_context -> typ -> term list
- val is_well_founded_inductive_pred : hol_context -> styp -> bool
- val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
- val equational_fun_axioms : hol_context -> styp -> term list
- val is_equational_fun_surely_complete : hol_context -> styp -> bool
+ val is_well_founded_inductive_pred : hol_context -> string * typ -> bool
+ val unrolled_inductive_pred_const : hol_context -> bool -> string * typ ->
+ term
+ val equational_fun_axioms : hol_context -> string * typ -> term list
+ val is_equational_fun_surely_complete : hol_context -> string * typ -> bool
val merged_type_var_table_for_terms :
theory -> term list -> (sort * string) list
val merge_type_vars_in_term :
@@ -243,16 +245,16 @@
open Nitpick_Util
type const_table = term list Symtab.table
-type special_fun = (styp * int list * term list) * styp
-type unrolled = styp * styp
-type wf_cache = (styp * (bool * bool)) list
+type special_fun = ((string * typ) * int list * term list) * (string * typ)
+type unrolled = (string * typ) * (string * typ)
+type wf_cache = ((string * typ) * (bool * bool)) list
type hol_context =
{thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
- wfs: (styp option * bool option) list,
+ wfs: ((string * typ) option * bool option) list,
user_axioms: bool option,
debug: bool,
whacks: term list,
@@ -278,7 +280,7 @@
special_funs: special_fun list Unsynchronized.ref,
unrolled_preds: unrolled list Unsynchronized.ref,
wf_cache: wf_cache Unsynchronized.ref,
- constr_cache: (typ * styp list) list Unsynchronized.ref}
+ constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}
datatype fixpoint_kind = Lfp | Gfp | NoFp
datatype boxability =
@@ -289,7 +291,7 @@
(
type T = {frac_types: (string * (string * string) list) list,
ersatz_table: (string * string) list,
- codatatypes: (string * (string * styp list)) list}
+ codatatypes: (string * (string * (string * typ) list)) list}
val empty = {frac_types = [], ersatz_table = [], codatatypes = []}
val extend = I
fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1},
@@ -320,12 +322,14 @@
(** Constant/type information and term/type manipulation **)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
+
fun quot_normal_name_for_type ctxt T =
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
val strip_first_name_sep =
Substring.full #> Substring.position name_sep ##> Substring.triml 1
#> pairself Substring.string
+
fun original_name s =
if String.isPrefix nitpick_prefix s then
case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
@@ -337,6 +341,7 @@
| s_conj (t1, t2) =
if t1 = @{const False} orelse t2 = @{const False} then @{const False}
else HOLogic.mk_conj (t1, t2)
+
fun s_disj (t1, @{const False}) = t1
| s_disj (@{const False}, t2) = t2
| s_disj (t1, t2) =
@@ -346,6 +351,7 @@
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
| strip_connective _ t = [t]
+
fun strip_any_connective (t as (t0 $ _ $ _)) =
if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
(strip_connective t0 t, t0)
@@ -420,6 +426,7 @@
| unarize_type @{typ "signed_bit word"} = int_T
| unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
| unarize_type T = T
+
fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
| unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
@@ -429,6 +436,7 @@
| unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
Type (s, map unarize_unbox_etc_type Ts)
| unarize_unbox_etc_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
@@ -440,13 +448,16 @@
val prefix_name = Long_Name.qualify o Long_Name.base_name
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
val prefix_abs_vars = Term.map_abs_vars o prefix_name
+
fun short_name s =
case space_explode name_sep s of
[_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
| ss => map shortest_name ss |> space_implode "_"
+
fun shorten_names_in_type (Type (s, Ts)) =
Type (short_name s, map shorten_names_in_type Ts)
| shorten_names_in_type T = T
+
val shorten_names_in_term =
map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
#> map_types shorten_names_in_type
@@ -454,9 +465,12 @@
fun strict_type_match thy (T1, T2) =
(Sign.typ_match thy (T2, T1) Vartab.empty; true)
handle Type.TYPE_MATCH => false
+
fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
+
fun const_match thy ((s1, T1), (s2, T2)) =
s1 = s2 andalso type_match thy (T1, T2)
+
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))
@@ -472,35 +486,53 @@
fun is_TFree (TFree _) = true
| is_TFree _ = false
+
fun is_fun_type (Type (@{type_name fun}, _)) = true
| is_fun_type _ = false
+
fun is_set_type (Type (@{type_name set}, _)) = true
| is_set_type _ = false
+
val is_fun_or_set_type = is_fun_type orf is_set_type
+
fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
(body_type T' = bool_T)
| is_set_like_type (Type (@{type_name set}, _)) = true
| is_set_like_type _ = false
+
fun is_pair_type (Type (@{type_name prod}, _)) = true
| is_pair_type _ = false
+
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
| is_lfp_iterator_type _ = false
+
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
+
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
+
fun is_frac_type ctxt (Type (s, [])) =
s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt)))
| is_frac_type _ _ = false
+
fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
+
fun is_higher_order_type (Type (@{type_name fun}, _)) = true
| is_higher_order_type (Type (@{type_name set}, _)) = true
| is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
@@ -508,8 +540,10 @@
fun elem_type (Type (@{type_name set}, [T'])) = T'
| elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
+
fun pseudo_domain_type (Type (@{type_name fun}, [T1, _])) = T1
| pseudo_domain_type T = elem_type T
+
fun pseudo_range_type (Type (@{type_name fun}, [_, T2])) = T2
| pseudo_range_type (Type (@{type_name set}, _)) = bool_T
| pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], [])
@@ -517,6 +551,7 @@
fun iterator_type_for_const gfp (s, T) =
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
binder_types T)
+
fun const_for_iterator_type (Type (s, Ts)) =
(strip_first_name_sep s |> snd, Ts ---> bool_T)
| const_for_iterator_type T =
@@ -528,12 +563,15 @@
| strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
strip_n_binders n (Type (@{type_name fun}, Ts))
| strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
+
val nth_range_type = snd oo strip_n_binders
fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
fold (Integer.add o num_factors_in_type) [T1, T2] 0
| num_factors_in_type _ = 1
+
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
+
fun maybe_curried_binder_types T =
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T
@@ -541,6 +579,7 @@
| mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
| mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
+
fun dest_n_tuple 1 t = [t]
| dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
@@ -571,8 +610,8 @@
Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse}
| _ => NONE
-val is_typedef = is_some oo typedef_info
-val is_real_datatype = is_some oo Datatype.get_info
+val is_raw_typedef = is_some oo typedef_info
+val is_raw_old_datatype = is_some oo Datatype.get_info
(* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
@@ -590,15 +629,19 @@
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
codatatypes = codatatypes} generic end
+
(* TODO: Consider morphism. *)
fun register_frac_type frac_s ersaetze (_ : morphism) =
register_frac_type_generic frac_s ersaetze
+
val register_frac_type_global = Context.theory_map oo register_frac_type_generic
fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
(* TODO: Consider morphism. *)
+
fun unregister_frac_type frac_s (_ : morphism) =
unregister_frac_type_generic frac_s
+
val unregister_frac_type_global =
Context.theory_map o unregister_frac_type_generic
@@ -608,9 +651,11 @@
val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz)
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
codatatypes = codatatypes} generic end
+
(* TODO: Consider morphism. *)
fun register_ersatz ersatz (_ : morphism) =
register_ersatz_generic ersatz
+
val register_ersatz_global = Context.theory_map o register_ersatz_generic
fun register_codatatype_generic coT case_name constr_xs generic =
@@ -628,41 +673,56 @@
codatatypes
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
codatatypes = codatatypes} generic end
+
(* TODO: Consider morphism. *)
fun register_codatatype coT case_name constr_xs (_ : morphism) =
register_codatatype_generic coT case_name constr_xs
+
val register_codatatype_global =
Context.theory_map ooo register_codatatype_generic
fun unregister_codatatype_generic coT = register_codatatype_generic coT "" []
(* TODO: Consider morphism. *)
+
fun unregister_codatatype coT (_ : morphism) =
unregister_codatatype_generic coT
val unregister_codatatype_global =
Context.theory_map o unregister_codatatype_generic
+fun is_raw_codatatype ctxt s =
+ not (null (these (Option.map snd (AList.lookup (op =)
+ (#codatatypes (Data.get (Context.Proof ctxt))) s))))
+
+fun is_registered_codatatype ctxt s =
+ Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
+ = SOME BNF_Util.Greatest_FP
+
fun is_codatatype ctxt (Type (s, _)) =
- Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
- = SOME BNF_Util.Greatest_FP orelse
- not (null (these (Option.map snd (AList.lookup (op =)
- (#codatatypes (Data.get (Context.Proof ctxt))) s))))
+ is_raw_codatatype ctxt s orelse is_registered_codatatype ctxt s
| is_codatatype _ _ = false
-fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T
-fun is_real_quot_type ctxt (Type (s, _)) =
+
+fun is_registered_type ctxt (T as Type (s, _)) =
+ is_frac_type ctxt T orelse is_registered_codatatype ctxt s
+ | is_registered_type _ _ = false
+
+fun is_raw_quot_type ctxt (Type (s, _)) =
is_some (Quotient_Info.lookup_quotients ctxt s)
- | is_real_quot_type _ _ = false
+ | is_raw_quot_type _ _ = false
+
fun is_quot_type ctxt T =
- is_real_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
+ is_raw_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
T <> @{typ int}
+
fun is_pure_typedef ctxt (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
is_frac_type ctxt T orelse
- (is_typedef ctxt s andalso
- not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
+ (is_raw_typedef ctxt s andalso
+ not (is_raw_old_datatype thy s orelse is_raw_quot_type ctxt T orelse
is_codatatype ctxt T orelse is_record_type T orelse
is_integer_like_type T))
end
| is_pure_typedef _ _ = false
+
fun is_univ_typedef ctxt (Type (s, _)) =
(case typedef_info ctxt s of
SOME {prop_of_Rep, ...} =>
@@ -683,9 +743,10 @@
end
| NONE => false)
| is_univ_typedef _ _ = false
+
fun is_datatype ctxt (T as Type (s, _)) =
- (is_typedef ctxt s orelse is_registered_type ctxt T orelse
- T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
+ (is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse
+ T = @{typ ind} orelse is_raw_quot_type ctxt T) andalso
not (is_basic_datatype s)
| is_datatype _ _ = false
@@ -694,39 +755,48 @@
recs @ more :: all_record_fields thy (snd more)
end
handle TYPE _ => []
+
fun is_record_constr (s, T) =
String.isSuffix Record.extN s andalso
let val dataT = body_type T in
is_record_type dataT andalso
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
end
+
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
+
fun no_of_record_field thy s T1 =
find_index (curry (op =) s o fst)
(Record.get_extT_fields thy T1 ||> single |> op @)
+
fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
exists (curry (op =) s o fst) (all_record_fields thy T1)
| is_record_get _ _ = false
+
fun is_record_update thy (s, T) =
String.isSuffix Record.updateN s andalso
exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
+
fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
(case typedef_info ctxt s' of
SOME {Abs_name, ...} => s = Abs_name
| NONE => false)
| is_abs_fun _ _ = false
+
fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
(case typedef_info ctxt s' of
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
+
fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
[_, abs_T as Type (s', _)]))) =
try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
= SOME (Const x) andalso not (is_registered_type ctxt abs_T)
| is_quot_abs_fun _ _ = false
+
fun is_quot_rep_fun ctxt (s, Type (@{type_name fun},
[abs_T as Type (abs_s, _), _])) =
(case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
@@ -741,6 +811,7 @@
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
+
fun rep_type_for_quot_type ctxt (T as Type (s, _)) =
let
val thy = Proof_Context.theory_of ctxt
@@ -750,6 +821,7 @@
end
| rep_type_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
+
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
val {qtyp, equiv_rel, equiv_thm, ...} =
@@ -765,6 +837,16 @@
| equiv_relation_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
+fun is_raw_old_datatype_constr thy (s, T) =
+ case body_type T of
+ Type (s', _) =>
+ (case Datatype.get_constrs thy s' of
+ SOME constrs =>
+ List.exists (fn (cname, cty) =>
+ cname = s andalso Sign.typ_instance thy (T, cty)) constrs
+ | NONE => false)
+ | _ => false
+
fun is_coconstr ctxt (s, T) =
case body_type T of
coT as Type (co_s, _) =>
@@ -783,7 +865,8 @@
(ctrs1 @ ctrs2)
end
| _ => false
-fun is_constr_like ctxt (s, T) =
+
+fun is_nonfree_constr ctxt (s, T) =
member (op =) [@{const_name FunBox}, @{const_name PairBox},
@{const_name Quot}, @{const_name Zero_Rep},
@{const_name Suc_Rep}] s orelse
@@ -791,22 +874,26 @@
val thy = Proof_Context.theory_of ctxt
val (x as (_, T)) = (s, unarize_unbox_etc_type T)
in
- is_real_constr thy x orelse is_record_constr x orelse
+ is_raw_old_datatype_constr thy x orelse is_record_constr x orelse
(is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
is_coconstr ctxt x
end
-fun is_constr_like_injective ctxt (s, T) =
- is_constr_like ctxt (s, T) andalso
+
+fun is_free_constr ctxt (s, T) =
+ is_nonfree_constr ctxt (s, T) andalso
let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
not (is_abs_fun ctxt x) orelse is_univ_typedef ctxt (range_type T)
end
+
fun is_stale_constr ctxt (x as (s, T)) =
- is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
+ is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
+
fun is_constr ctxt (x as (_, T)) =
- is_constr_like ctxt x andalso
+ is_nonfree_constr ctxt x andalso
not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
not (is_stale_constr ctxt x)
+
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
String.isPrefix sel_prefix orf
@@ -814,6 +901,7 @@
fun in_fun_lhs_for InConstr = InSel
| in_fun_lhs_for _ = InFunLHS
+
fun in_fun_rhs_for InConstr = InConstr
| in_fun_rhs_for InSel = InSel
| in_fun_rhs_for InFunRHS1 = InFunRHS2
@@ -865,15 +953,18 @@
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
+
fun nth_sel_name_for_constr_name s n =
if s = @{const_name Pair} then
if n = 0 then @{const_name fst} else @{const_name snd}
else
sel_prefix_for n ^ s
+
fun nth_sel_for_constr x ~1 = discr_for_constr x
| nth_sel_for_constr (s, T) n =
(nth_sel_name_for_constr_name s n,
body_type T --> nth (maybe_curried_binder_types T) n)
+
fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
oo nth_sel_for_constr
@@ -943,7 +1034,7 @@
val T' = (Record.get_extT_fields thy T
|> apsnd single |> uncurry append |> map snd) ---> T
in [(s', T')] end
- else if is_real_quot_type ctxt T then
+ else if is_raw_quot_type ctxt T then
[(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
else case typedef_info ctxt s of
SOME {abs_type, rep_type, Abs_name, ...} =>
@@ -957,6 +1048,7 @@
else
[]))
| uncached_datatype_constrs _ _ = []
+
fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
@@ -964,6 +1056,7 @@
let val xs = uncached_datatype_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
+
fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
map (apsnd ((binarize ? binarize_nat_and_int_in_type)
o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
@@ -972,6 +1065,7 @@
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
| constr_name_for_sel_like s' = original_name s'
+
fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
let val s = constr_name_for_sel_like s' in
AList.lookup (op =)
@@ -1127,6 +1221,7 @@
handle TERM _ => betapply (t1, t2)
| General.Subscript => betapply (t1, t2))
| s_betapply _ (t1, t2) = t1 $ t2
+
fun s_betapplys Ts = Library.foldl (s_betapply Ts)
fun s_beta_norm Ts t =
@@ -1153,11 +1248,12 @@
else
Abs (Name.uu, dataT, @{const True})
end
+
fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
case head_of t of
Const x' =>
if x = x' then @{const True}
- else if is_constr_like ctxt x' then @{const False}
+ else if is_nonfree_constr ctxt x' then @{const False}
else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
| _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
@@ -1181,12 +1277,13 @@
(List.take (arg_Ts, n)) 0
in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
end
+
fun select_nth_constr_arg ctxt x t n res_T =
(case strip_comb t of
(Const x', args) =>
if x = x' then
- if is_constr_like_injective ctxt x then nth args n else raise SAME ()
- else if is_constr_like ctxt x' then
+ if is_free_constr ctxt x then nth args n else raise SAME ()
+ else if is_nonfree_constr ctxt x' then
Const (@{const_name unknown}, res_T)
else
raise SAME ()
@@ -1210,7 +1307,7 @@
fun constr_expand (hol_ctxt as {ctxt, ...}) T t =
(case head_of t of
- Const x => if is_constr_like ctxt x then t else raise SAME ()
+ Const x => if is_nonfree_constr ctxt x then t else raise SAME ()
| _ => raise SAME ())
handle SAME () =>
let
@@ -1233,6 +1330,7 @@
| Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
| Bound j' => if j' = j then f t else t
| _ => t
+
fun coerce_bound_0_in_term hol_ctxt new_T old_T =
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t =
@@ -1290,6 +1388,7 @@
member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
@{type_name Sum_Type.sum}, @{type_name int}] s orelse
is_frac_type ctxt (Type (s, []))
+
fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
| is_funky_typedef _ _ = false
@@ -1415,6 +1514,7 @@
| NONE => false)
| _ => false
end
+
fun unfold_mutually_inductive_preds thy table =
map_aterms (fn t as Const x =>
(case def_of_const thy table x of
@@ -1449,13 +1549,14 @@
else fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-fun is_real_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
- x =
+fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
+ x =
fixpoint_kind_of_const thy def_tables x <> NoFp andalso
not (null (def_props_for_const thy 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
+ String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse
+ is_raw_inductive_pred hol_ctxt x
fun lhs_of_equation t =
case t of
@@ -1467,15 +1568,18 @@
| Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
| @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
+
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
| is_constr_pattern ctxt t =
case strip_comb t of
(Const x, args) =>
- is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
+ is_nonfree_constr ctxt x andalso forall (is_constr_pattern ctxt) args
| _ => false
+
fun is_constr_pattern_lhs ctxt t =
forall (is_constr_pattern ctxt) (snd (strip_comb t))
+
fun is_constr_pattern_formula ctxt t =
case lhs_of_equation t of
SOME t' => is_constr_pattern_lhs ctxt t'
@@ -1505,6 +1609,7 @@
ys
| aux _ ys = ys
in map snd (fold_aterms aux t []) end
+
fun nondef_props_for_const thy slack table (x as (s, _)) =
these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
@@ -1512,11 +1617,13 @@
| unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
| unvarify_term t = t
+
fun axiom_for_choice_spec thy =
unvarify_term
#> Object_Logic.atomize_term thy
#> Choice_Specification.close_form
#> HOLogic.mk_Trueprop
+
fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
: hol_context) x =
case nondef_props_for_const thy true choice_spec_table x of
@@ -1533,16 +1640,16 @@
end
fun is_choice_spec_axiom thy choice_spec_table t =
- Symtab.exists (fn (_, ts) =>
- exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
+ Symtab.exists (exists (curry (op aconv) t o axiom_for_choice_spec thy) o snd)
choice_spec_table
-fun is_real_equational_fun ({thy, simp_table, psimp_table, ...}
- : hol_context) x =
+fun is_raw_equational_fun ({thy, simp_table, psimp_table, ...} : hol_context)
+ x =
exists (fn table => not (null (def_props_for_const thy 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
+
+fun is_equational_fun hol_ctxt =
+ is_raw_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
(** Constant unfolding **)
@@ -1551,12 +1658,14 @@
s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
+
fun add_constr_case res_T (body_t, guard_t) res_t =
if res_T = bool_T then
s_conj (HOLogic.mk_imp (guard_t, body_t), res_t)
else
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
$ guard_t $ body_t $ res_t
+
fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
let
val xs = datatype_constrs hol_ctxt dataT
@@ -1601,6 +1710,7 @@
[]))
| j => select_nth_constr_arg ctxt constr_x t j res_T
end
+
fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
rec_t =
let
@@ -1818,7 +1928,7 @@
else
(Const x, ts)
end
- else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
+ else if is_equational_fun hol_ctxt x orelse
is_choice_spec_fun hol_ctxt x then
(Const x, ts)
else case def_of_const_ext thy def_tables x of
@@ -1894,12 +2004,14 @@
(map pair_for_prop ts) Symtab.empty)
fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
+
fun const_nondef_table ts =
fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
fun const_simp_table ctxt =
def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of)
o Nitpick_Simps.get) ctxt
+
fun const_psimp_table ctxt =
def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of)
o Nitpick_Psimps.get) ctxt
@@ -1941,6 +2053,7 @@
|> pairself (specialize_type thy x o prop_of o the)
||> single |> op ::
end
+
fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
let
val thy = Proof_Context.theory_of ctxt
@@ -1964,6 +2077,7 @@
end
| NONE => []
end
+
fun optimized_quot_type_axioms ctxt abs_z =
let
val abs_T = Type abs_z
@@ -2044,6 +2158,7 @@
end
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
+
fun wf_constraint_for rel side concl main =
let
val core = HOLogic.mk_mem (HOLogic.mk_prod
@@ -2056,6 +2171,7 @@
$ Abs (x, T, abstract_over (Var ((x, j), T), t')))
(t, vars)
end
+
fun wf_constraint_for_triple rel (side, main, concl) =
map (wf_constraint_for rel side concl) main |> foldr1 s_conj
@@ -2267,7 +2383,7 @@
val unrolled_const = Const x' $ zero_const iter_T
val def = the (def_of_const thy def_tables x)
in
- if is_equational_fun_but_no_plain_def hol_ctxt x' then
+ if is_equational_fun hol_ctxt x' then
unrolled_const (* already done *)
else if not gfp andalso star_linear_preds andalso
is_linear_inductive_pred_def def andalso
@@ -2314,6 +2430,7 @@
HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
|> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
end
+
fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
let val x' = (strip_first_name_sep s |> snd, T) in
@@ -2335,6 +2452,7 @@
| NONE => [])
| psimps => psimps)
| simps => simps
+
fun is_equational_fun_surely_complete hol_ctxt x =
case equational_fun_axioms hol_ctxt x of
[@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
@@ -2383,8 +2501,10 @@
| xs => map snd xs)
| _ => insert (op =) T accum
in aux end
+
fun ground_types_in_type hol_ctxt binarize T =
add_ground_types hol_ctxt binarize T []
+
fun ground_types_in_terms hol_ctxt binarize ts =
fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 22:33:22 2014 +0100
@@ -126,7 +126,9 @@
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
val single_atom = KK.TupleSet o single o KK.Tuple o single
+
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
+
fun pow_of_two_int_bounds bits j0 =
let
fun aux 0 _ _ = []
@@ -164,6 +166,7 @@
else
NONE
end) (index_seq 0 k))
+
fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
(check_table_size (k * k);
map_filter (fn j => let
@@ -177,6 +180,7 @@
else
NONE
end) (index_seq 0 (k * k)))
+
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
(check_table_size (k * k);
map_filter (fn j => let
@@ -191,11 +195,14 @@
else
NONE
end) (index_seq 0 (k * k)))
+
fun tabulate_nat_op2 debug univ_card (k, j0) f =
tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
+
fun tabulate_int_op2 debug univ_card (k, j0) f =
tabulate_op2 debug univ_card (k, j0) j0
(atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
+
fun tabulate_int_op2_2 debug univ_card (k, j0) f =
tabulate_op2_2 debug univ_card (k, j0) j0
(pairself (atom_for_int (k, 0)) o f
@@ -203,10 +210,13 @@
fun isa_div (m, n) = m div n handle General.Div => 0
fun isa_mod (m, n) = m mod n handle General.Div => m
+
fun isa_gcd (m, 0) = m
| isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
+
fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
val isa_zgcd = isa_gcd o pairself abs
+
fun isa_norm_frac (m, n) =
if n < 0 then isa_norm_frac (~m, ~n)
else if m = 0 orelse n = 0 then (0, 1)
@@ -282,6 +292,7 @@
end
else
NONE
+
fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
int_card main_j0 formulas =
let val rels = built_in_rels_in_formulas formulas in
@@ -424,6 +435,7 @@
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
val singleton_from_combination = foldl1 KK.Product o map KK.Atom
+
fun all_singletons_for_rep R =
if is_lone_rep R then
all_combinations_for_rep R |> map singleton_from_combination
@@ -433,10 +445,12 @@
fun unpack_products (KK.Product (r1, r2)) =
unpack_products r1 @ unpack_products r2
| unpack_products r = [r]
+
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
| unpack_joins r = [r]
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
+
fun full_rel_for_rep R =
case atom_schema_of_rep R of
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
@@ -471,6 +485,7 @@
else
KK.True
end
+
fun kk_n_ary_function kk R (r as KK.Rel x) =
if not (is_opt_rep R) then
if x = suc_rel then
@@ -499,15 +514,19 @@
let val x = (KK.arity_of_rel_expr r, j) in
kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
end
+
val single_rel_rel_let = basic_rel_rel_let 0
+
fun double_rel_rel_let kk f r1 r2 =
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
+
fun triple_rel_rel_let kk f r1 r2 r3 =
double_rel_rel_let kk
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
+
fun rel_expr_from_formula kk R f =
case unopt_rep R of
Atom (2, j0) => atom_from_formula kk j0 f
@@ -723,7 +742,9 @@
unsigned_bit_word_sel_rel
else
signed_bit_word_sel_rel))
+
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
+
fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
: kodkod_constrs) T R i =
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
@@ -1493,10 +1514,12 @@
else SOME ((x, kk_project r (map KK.Num [0, j])), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
+
fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
(x as (_, T)) =
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
+
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
| nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
| nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
@@ -1551,6 +1574,7 @@
[kk_no (kk_intersect
(loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
KK.Iden)]
+
fun acyclicity_axioms_for_datatypes kk =
maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
@@ -1603,6 +1627,7 @@
fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
+
fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
@@ -1794,6 +1819,7 @@
(kk_n_ary_function kk R2 r') (kk_no r'))]
end
end
+
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table
dtype (constr as {const, delta, epsilon, explicit_max, ...}) =
let
@@ -1822,6 +1848,7 @@
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
+
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
(dtype as {constrs, ...}) =
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
@@ -1851,12 +1878,14 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
end
+
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
(dtype as {constrs, ...}) =
maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
dtype) constrs
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
+
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
need_vals rel_table (dtype as {card, constrs, ...}) =
if forall #exclusive constrs then--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,13 +7,12 @@
signature NITPICK_MODEL =
sig
- type styp = Nitpick_Util.styp
type scope = Nitpick_Scope.scope
type rep = Nitpick_Rep.rep
type nut = Nitpick_Nut.nut
type params =
- {show_datatypes: bool,
+ {show_types: bool,
show_skolems: bool,
show_consts: bool}
@@ -37,9 +36,9 @@
val dest_plain_fun : term -> bool * (term list * term list)
val reconstruct_hol_model :
params -> scope -> (term option * int list) list
- -> (typ option * string list) list -> styp list -> styp list -> nut list
- -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
- -> Pretty.T * bool
+ -> (typ option * string list) list -> (string * typ) list ->
+ (string * typ) list -> nut list -> nut list -> nut list ->
+ nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool
val prove_hol_model :
scope -> Time.time -> nut list -> nut list -> nut NameTable.table
-> Kodkod.raw_bound list -> term -> bool option
@@ -58,7 +57,7 @@
structure KK = Kodkod
type params =
- {show_datatypes: bool,
+ {show_types: bool,
show_skolems: bool,
show_consts: bool}
@@ -122,10 +121,12 @@
length js + 1)
| n => length js - n)
| NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
+
fun atom_suffix s =
nat_subscript
#> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s))) (* FIXME Symbol.explode (?) *)
? prefix "\<^sub>,"
+
fun nth_atom_name thy atomss pool prefix T j =
let
val ss = these (triple_lookup (type_match thy) atomss T)
@@ -144,6 +145,7 @@
| TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
| _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
end
+
fun nth_atom thy atomss pool for_auto T j =
if for_auto then
Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
@@ -154,6 +156,7 @@
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
+
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
| nice_term_ord tp = Real.compare (pairself extract_real_number tp)
handle TERM ("dest_number", _) =>
@@ -166,16 +169,20 @@
fun register_term_postprocessor_generic T postproc =
Data.map (cons (T, postproc))
+
(* TODO: Consider morphism. *)
fun register_term_postprocessor T postproc (_ : morphism) =
register_term_postprocessor_generic T postproc
+
val register_term_postprocessor_global =
Context.theory_map oo register_term_postprocessor_generic
fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
(* TODO: Consider morphism. *)
+
fun unregister_term_postprocessor T (_ : morphism) =
unregister_term_postprocessor_generic T
+
val unregister_term_postprocessor_global =
Context.theory_map o unregister_term_postprocessor_generic
@@ -238,6 +245,7 @@
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
$ aux T1 T2 tps $ t1 $ t2
in aux T1 T2 o rev end
+
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
| is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
is_plain_fun t0
@@ -260,6 +268,7 @@
val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
+
fun pair_up (Type (@{type_name prod}, [T1', T2']))
(t1 as Const (@{const_name Pair},
Type (@{type_name fun},
@@ -268,6 +277,7 @@
if T1 = T1' then HOLogic.mk_prod (t1, t2)
else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
| pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
+
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
fun format_fun T' T1 T2 t =
@@ -689,6 +699,7 @@
else
[num_binder_types T]
| NONE => [num_binder_types T]
+
fun intersect_formats _ [] = []
| intersect_formats [] _ = []
| intersect_formats ks1 ks2 =
@@ -727,6 +738,7 @@
|> map (HOLogic.mk_tupleT o rev)
in List.foldl (op -->) body_T batched end
end
+
fun format_term_type thy def_tables formats t =
format_type (the (AList.lookup (op =) formats NONE))
(lookup_format thy def_tables formats t) (fastype_of t)
@@ -851,6 +863,7 @@
$ Bound 0 $ t')) =
betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
| unfold_outer_the_binders t = t
+
fun bisimilar_values _ 0 _ = true
| bisimilar_values coTs max_depth (t1, t2) =
let val T = fastype_of t1 in
@@ -867,7 +880,7 @@
t1 = t2
end
-fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
+fun reconstruct_hol_model {show_types, show_skolems, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
star_linear_preds, total_consts, needs, tac_timeout,
@@ -958,13 +971,13 @@
datatypes |> filter #deep |> List.partition #co
||> append (integer_datatype nat_T @ integer_datatype int_T)
val block_of_datatypes =
- if show_datatypes andalso not (null datatypes) then
+ if show_types andalso not (null datatypes) then
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
(map pretty_for_datatype datatypes)]
else
[]
val block_of_codatatypes =
- if show_datatypes andalso not (null codatatypes) then
+ if show_types andalso not (null codatatypes) then
[Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
(map pretty_for_datatype codatatypes)]
else--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 22:33:22 2014 +0100
@@ -42,12 +42,13 @@
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
- constr_mcache: (styp * mtyp) list Unsynchronized.ref}
+ constr_mcache: ((string * typ) * mtyp) list Unsynchronized.ref}
exception UNSOLVABLE of unit
exception MTYPE of string * mtyp list * typ list
val trace = Unsynchronized.ref false
+
fun trace_msg msg = if !trace then tracing (msg ()) else ()
fun string_for_sign Plus = "+"
@@ -57,8 +58,10 @@
| negate_sign Minus = Plus
val string_for_var = signed_string_of_int
+
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
| string_for_vars sep xs = space_implode sep (map string_for_var xs)
+
fun subscript_string_for_vars sep xs =
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
@@ -79,6 +82,7 @@
fun is_MRec (MRec _) = true
| is_MRec _ = false
+
fun dest_MFun (MFun z) = z
| dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
@@ -126,6 +130,7 @@
T = alpha_T orelse (not (is_fp_iterator_type T) andalso
exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
+
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
| could_exist_alpha_sub_mtype ctxt alpha_T T =
@@ -269,9 +274,11 @@
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
| prodM_factors M = [M]
+
fun curried_strip_mtype (MFun (M1, _, M2)) =
curried_strip_mtype M2 |>> append (prodM_factors M1)
| curried_strip_mtype M = ([], M)
+
fun sel_mtype_from_constr_mtype s M =
let
val (arg_Ms, dataM) = curried_strip_mtype M
@@ -299,6 +306,7 @@
AList.lookup (op =) (!constr_mcache) x |> the)
else
fresh_mtype_for_type mdata false T
+
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
|> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
@@ -306,6 +314,7 @@
fun resolve_annotation_atom asgs (V x) =
x |> AList.lookup (op =) asgs |> Option.map A |> the_default (V x)
| resolve_annotation_atom _ aa = aa
+
fun resolve_mtype asgs =
let
fun aux MAlpha = MAlpha
@@ -474,29 +483,37 @@
val annotation_from_bools = AList.find (op =) bool_table #> the_single
fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
+
fun prop_for_bool_var_equality (v1, v2) =
Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1,
Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1),
Prop_Logic.BoolVar v2))
+
fun prop_for_assign (x, a) =
let val (b1, b2) = bools_from_annotation a in
Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
end
+
fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
| prop_for_assign_literal (x, (Minus, a)) =
Prop_Logic.SNot (prop_for_assign (x, a))
+
fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
| prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
+
fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
| prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
| prop_for_atom_equality (V x1, V x2) =
Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
prop_for_bool_var_equality (pairself snd_var (x1, x2)))
+
val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal
+
fun prop_for_exists_var_assign_literal xs a =
Prop_Logic.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
+
fun prop_for_comp (aa1, aa2, Eq, []) =
Prop_Logic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
prop_for_comp (aa2, aa1, Leq, []))
@@ -578,16 +595,18 @@
{bound_Ts: typ list,
bound_Ms: mtyp list,
frame: (int * annotation_atom) list,
- frees: (styp * mtyp) list,
- consts: (styp * mtyp) list}
+ frees: ((string * typ) * mtyp) list,
+ consts: ((string * typ) * mtyp) list}
fun string_for_bound ctxt Ms (j, aa) =
Syntax.string_of_term ctxt (Bound (length Ms - j - 1)) ^ " :\<^bsup>" ^
string_for_annotation_atom aa ^ "\<^esup> " ^
string_for_mtype (nth Ms (length Ms - j - 1))
+
fun string_for_free relevant_frees ((s, _), M) =
if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
else NONE
+
fun string_for_mcontext ctxt t ({bound_Ms, frame, frees, ...} : mcontext) =
(map_filter (string_for_free (Term.add_free_names t [])) frees @
map (string_for_bound ctxt bound_Ms) frame)
@@ -599,6 +618,7 @@
fun push_bound aa T M {bound_Ts, bound_Ms, frame, frees, consts} =
{bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
frame = frame @ [(length bound_Ts, aa)], frees = frees, consts = consts}
+
fun pop_bound {bound_Ts, bound_Ms, frame, frees, consts} =
{bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
frame = frame |> filter_out (fn (j, _) => j = length bound_Ts - 1),
@@ -678,6 +698,7 @@
string_for_annotation_atom aa2);
fold (add_assign_clause o assign_clause_from_quasi_clause)
(mk_quasi_clauses res_aa aa1 aa2))
+
fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
@@ -709,6 +730,7 @@
fun add_arg_order1 ((_, aa), (_, prev_aa)) = I
add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa
+
fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = I
let
val clause = [(arg_aa, (Eq, New)), (res_aa, (Eq, Gen))]
@@ -718,6 +740,7 @@
apsnd (add_assign_clause clause)
#> add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa
end
+
fun add_app _ [] [] = I
| add_app fun_aa res_frame arg_frame =
add_comp_frame (A New) Leq arg_frame
@@ -986,6 +1009,7 @@
| force_gen_funs n (M as MFun (M1, _, M2)) =
add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
| force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
+
fun consider_general_equals mdata def t1 t2 accum =
let
val (M1, accum) = consider_term mdata t1 accum--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,7 +7,6 @@
signature NITPICK_NUT =
sig
- type styp = Nitpick_Util.styp
type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
@@ -100,7 +99,7 @@
val nut_from_term : hol_context -> op2 -> term -> nut
val is_fully_representable_set : nut -> bool
val choose_reps_for_free_vars :
- scope -> styp list -> nut list -> rep NameTable.table
+ scope -> (string * typ) list -> nut list -> rep NameTable.table
-> nut list * rep NameTable.table
val choose_reps_for_consts :
scope -> bool -> nut list -> rep NameTable.table
@@ -333,9 +332,11 @@
space_explode name_sep (nickname_of u)
|> exists (String.isPrefix skolem_prefix)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
+
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
+
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
@@ -347,6 +348,7 @@
| Tuple (_, _, us) => fold (fold_nut f) us
| Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
| _ => f u
+
fun map_nut f u =
case u of
Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
@@ -398,6 +400,7 @@
case NameTable.lookup table name of
SOME u => u
| NONE => raise NUT ("Nitpick_Nut.the_name", [name])
+
fun the_rel table name =
case the_name table name of
FreeRel (x, _, _, _) => x
@@ -408,12 +411,14 @@
let val res_T = fst (HOLogic.dest_prodT T) in
(res_T, Const (@{const_name fst}, T --> res_T) $ t)
end
+
fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) =
(domain_type (range_type T), t2)
| mk_snd (T, t) =
let val res_T = snd (HOLogic.dest_prodT T) in
(res_T, Const (@{const_name snd}, T --> res_T) $ t)
end
+
fun factorize (z as (Type (@{type_name prod}, _), _)) =
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
@@ -649,6 +654,7 @@
best_non_opt_set_rep_for_type) scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
+
fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
(vs, table) =
let
@@ -674,6 +680,7 @@
fun choose_reps_for_free_vars scope pseudo_frees vs table =
fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
+
fun choose_reps_for_consts scope total_consts vs table =
fold (choose_rep_for_const scope total_consts) vs ([], table)
@@ -690,12 +697,15 @@
best_opt_set_rep_for_type scope T' |> unopt_rep
val v = ConstName (s', T', R')
in (v :: vs, NameTable.update (v, R') table) end
+
fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
fold_rev (choose_rep_for_nth_sel_for_constr scope x)
(~1 upto num_sels_for_constr_type T - 1)
+
fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
| choose_rep_for_sels_of_datatype scope {constrs, ...} =
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
+
fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
@@ -744,6 +754,7 @@
else
raise SAME ())
handle SAME () => Op1 (oper, T, R, u1))
+
fun s_op2 oper T R u1 u2 =
((case oper of
All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
@@ -785,6 +796,7 @@
raise SAME ()
| _ => raise SAME ())
handle SAME () => Op2 (oper, T, R, u1, u2))
+
fun s_op3 oper T R u1 u2 u3 =
((case oper of
Let =>
@@ -794,6 +806,7 @@
raise SAME ()
| _ => raise SAME ())
handle SAME () => Op3 (oper, T, R, u1, u2, u3))
+
fun s_tuple T R us =
if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
@@ -1077,19 +1090,23 @@
| fresh_n_ary_index n ((m, j) :: xs) ys =
if m = n then (j, ys @ ((m, j + 1) :: xs))
else fresh_n_ary_index n xs ((m, j) :: ys)
+
fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
let val (j, rels') = fresh_n_ary_index n rels [] in
(j, {rels = rels', vars = vars, formula_reg = formula_reg,
rel_reg = rel_reg})
end
+
fun fresh_var n {rels, vars, formula_reg, rel_reg} =
let val (j, vars') = fresh_n_ary_index n vars [] in
(j, {rels = rels, vars = vars', formula_reg = formula_reg,
rel_reg = rel_reg})
end
+
fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
(formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
rel_reg = rel_reg})
+
fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
(rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
rel_reg = rel_reg + 1})--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Mar 03 22:33:22 2014 +0100
@@ -128,14 +128,18 @@
fun formula_for_bool b = if b then True else False
fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
+
fun min_int_for_card k = ~k div 2 + 1
fun max_int_for_card k = k div 2
+
fun int_for_atom (k, j0) j =
let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
+
fun atom_for_int (k, j0) n =
if n < min_int_for_card k orelse n > max_int_for_card k then ~1
else if n < 0 then n + k + j0
else n + j0
+
fun is_twos_complement_representable bits n =
let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
@@ -147,6 +151,7 @@
"too large cardinality (" ^ string_of_int n ^ ")")
else
(max_squeeze_card + 1) * m + n
+
fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
fun boolify (j, b) = 2 * j + (if b then 0 else 1)
@@ -154,6 +159,7 @@
fun suc_rel_for_atom_seq (x, tabulate) =
(2, suc_rels_base - boolify (squeeze x, tabulate))
+
fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
fun is_none_product (Product (r1, r2)) =
@@ -206,8 +212,10 @@
fun is_Num (Num _) = true
| is_Num _ = false
+
fun dest_Num (Num k) = k
| dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
+
fun num_seq j0 n = map Num (index_seq j0 n)
fun occurs_in_union r (Union (r1, r2)) =--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 03 22:33:22 2014 +0100
@@ -74,7 +74,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 x orelse is_constr_like ctxt x orelse
+ if is_built_in_const x orelse is_nonfree_constr ctxt x orelse
is_sel s orelse s = @{const_name Sigma} then
table
else
@@ -230,7 +230,7 @@
else if is_built_in_const x orelse
s = @{const_name Sigma} then
T
- else if is_constr_like ctxt x then
+ else if is_nonfree_constr ctxt x then
box_type hol_ctxt InConstr T
else if is_sel s orelse is_rep_fun ctxt x then
box_type hol_ctxt InSel T
@@ -617,8 +617,8 @@
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js skolemizable polar t2
| Const (x as (s, T)) =>
- if is_real_inductive_pred hol_ctxt x andalso
- not (is_real_equational_fun hol_ctxt x) andalso
+ if is_raw_inductive_pred hol_ctxt x andalso
+ not (is_raw_equational_fun hol_ctxt x) andalso
not (is_well_founded_inductive_pred hol_ctxt x) then
let
val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
@@ -704,6 +704,7 @@
| [t as Free _] => cons (j, SOME t)
| _ => I) indexed_sets []
end
+
fun static_args_in_terms hol_ctxt x =
map (static_args_in_term hol_ctxt x)
#> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
@@ -740,7 +741,7 @@
((if not (member (op =) blacklist x) andalso not (null args) andalso
not (String.isPrefix special_prefix s) andalso
not (is_built_in_const x) andalso
- (is_equational_fun_but_no_plain_def hol_ctxt x orelse
+ (is_equational_fun hol_ctxt x orelse
(is_some (def_of_const thy def_tables x) andalso
not (is_of_class_const thy x) andalso
not (is_constr ctxt x) andalso
@@ -804,7 +805,7 @@
| aux args _ t = list_comb (t, args)
in aux [] [] t end
-type special_triple = int list * term list * styp
+type special_triple = int list * term list * (string * typ)
val cong_var_prefix = "c"
@@ -880,6 +881,7 @@
| NONE => false
fun all_table_entries table = Symtab.fold (append o snd) table []
+
fun extra_table tables s =
Symtab.make [(s, pairself all_table_entries tables |> op @)]
@@ -899,7 +901,7 @@
val (def_assm_ts, nondef_assm_ts) =
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts
- type accumulator = styp list * (term list * term list)
+ type accumulator = (string * typ) list * (term list * term list)
fun add_axiom get app def depth t (accum as (seen, axs)) =
let
val t = t |> unfold_defs_in_term hol_ctxt
@@ -951,7 +953,7 @@
else if is_descr (original_name s) then
fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
accum
- else if is_equational_fun_but_no_plain_def hol_ctxt x then
+ else if is_equational_fun hol_ctxt x then
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
accum
else if is_choice_spec_fun hol_ctxt x then
@@ -1066,7 +1068,7 @@
do_term t1 []
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
| do_term (t as Const (x as (s, T))) (args as _ :: _) =
- ((if is_constr_like ctxt x then
+ ((if is_nonfree_constr ctxt x then
if length args = num_binder_types T then
case hd args of
Const (_, T') $ t' =>
@@ -1082,7 +1084,7 @@
else if is_sel_like_and_no_discr s then
case strip_comb (hd args) of
(Const (x' as (s', T')), ts') =>
- if is_constr_like_injective ctxt x' andalso
+ if is_free_constr ctxt x' andalso
constr_name_for_sel_like s = s' andalso
not (exists is_pair_type (binder_types T')) then
list_comb (nth ts' (sel_no_from_name s), tl args)--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 03 22:33:22 2014 +0100
@@ -97,8 +97,10 @@
fun is_Func (Func _) = true
| is_Func _ = false
+
fun is_Opt (Opt _) = true
| is_Opt _ = false
+
fun is_opt_rep (Func (_, R2)) = is_opt_rep R2
| is_opt_rep (Opt _) = true
| is_opt_rep _ = false
@@ -111,6 +113,7 @@
| card_of_rep (Func (R1, R2)) =
reasonable_power (card_of_rep R2) (card_of_rep R1)
| card_of_rep (Opt R) = card_of_rep R
+
fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
| arity_of_rep (Formula _) = 0
| arity_of_rep (Atom _) = 1
@@ -118,6 +121,7 @@
| arity_of_rep (Vect (k, R)) = k * arity_of_rep R
| arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
| arity_of_rep (Opt R) = arity_of_rep R
+
fun min_univ_card_of_rep Any =
raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
| min_univ_card_of_rep (Formula _) = 0
@@ -133,11 +137,13 @@
| is_one_rep (Struct _) = true
| is_one_rep (Vect _) = true
| is_one_rep _ = false
+
fun is_lone_rep (Opt R) = is_one_rep R
| is_lone_rep R = is_one_rep R
fun dest_Func (Func z) = z
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
+
fun lazy_range_rep _ _ _ (Vect (_, R)) = R
| lazy_range_rep _ _ _ (Func (_, R2)) = R2
| lazy_range_rep ofs T ran_card (Opt R) =
@@ -150,6 +156,7 @@
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
| binder_reps _ = []
+
fun body_rep (Func (_, R2)) = body_rep R2
| body_rep R = R
@@ -163,16 +170,19 @@
| one_rep _ _ (Vect z) = Vect z
| one_rep ofs T (Opt R) = one_rep ofs T R
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
+
fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, optable_rep ofs T2 R2)
| optable_rep ofs (Type (@{type_name set}, [T'])) R =
optable_rep ofs (T' --> bool_T) R
| optable_rep ofs T R = one_rep ofs T R
+
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, opt_rep ofs T2 R2)
| opt_rep ofs (Type (@{type_name set}, [T'])) R =
opt_rep ofs (T' --> bool_T) R
| opt_rep ofs T R = Opt (optable_rep ofs T R)
+
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
| unopt_rep (Opt R) = R
| unopt_rep R = R
@@ -254,6 +264,7 @@
best_opt_set_rep_for_type scope (T' --> bool_T)
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
opt_rep ofs T (best_one_rep_for_type scope T)
+
fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
(case (best_one_rep_for_type scope T1,
best_non_opt_set_rep_for_type scope T2) of
@@ -262,9 +273,11 @@
| best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
best_non_opt_set_rep_for_type scope (T' --> bool_T)
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
+
fun best_set_rep_for_type (scope as {datatypes, ...}) T =
(if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
else best_opt_set_rep_for_type) scope T
+
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
(Type (@{type_name fun}, [T1, T2])) =
(optable_rep ofs T1 (best_one_rep_for_type scope T1),--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,11 +7,10 @@
signature NITPICK_SCOPE =
sig
- type styp = Nitpick_Util.styp
type hol_context = Nitpick_HOL.hol_context
type constr_spec =
- {const: styp,
+ {const: string * typ,
delta: int,
epsilon: int,
exclusive: bool,
@@ -39,7 +38,7 @@
val is_asymmetric_nondatatype : typ -> bool
val datatype_spec : datatype_spec list -> typ -> datatype_spec option
- val constr_spec : datatype_spec list -> styp -> constr_spec
+ val constr_spec : datatype_spec list -> string * typ -> constr_spec
val is_complete_type : datatype_spec list -> bool -> typ -> bool
val is_concrete_type : datatype_spec list -> bool -> typ -> bool
val is_exact_type : datatype_spec list -> bool -> typ -> bool
@@ -51,10 +50,10 @@
val scope_less_eq : scope -> scope -> bool
val is_self_recursive_constr_type : typ -> bool
val all_scopes :
- hol_context -> bool -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list
- -> int list -> int list -> typ list -> typ list -> typ list -> typ list
- -> int * scope list
+ hol_context -> bool -> (typ option * int list) list ->
+ ((string * typ) option * int list) list ->
+ ((string * typ) option * int list) list -> int list -> int list ->
+ typ list -> typ list -> typ list -> typ list -> int * scope list
end;
structure Nitpick_Scope : NITPICK_SCOPE =
@@ -64,7 +63,7 @@
open Nitpick_HOL
type constr_spec =
- {const: styp,
+ {const: string * typ,
delta: int,
epsilon: int,
exclusive: bool,
@@ -90,7 +89,7 @@
datatypes: datatype_spec list,
ofs: int Typtab.table}
-datatype row_kind = Card of typ | Max of styp
+datatype row_kind = Card of typ | Max of string * typ
type row = row_kind * int list
type block = row list
@@ -212,23 +211,29 @@
fun scopes_equivalent (s1 : scope, s2 : scope) =
#datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
+
fun scope_less_eq (s1 : scope) (s2 : scope) =
(s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
fun rank_of_row (_, ks) = length ks
+
fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
+
fun project_row _ (y, []) = (y, [1]) (* desperate measure *)
| project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
+
fun project_block (column, block) = map (project_row column) block
fun lookup_ints_assign eq assigns key =
case triple_lookup eq assigns key of
SOME ks => ks
| NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
+
fun lookup_type_ints_assign thy assigns T =
map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T)
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
+
fun lookup_const_ints_assign thy assigns x =
lookup_ints_assign (const_match thy) assigns x
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
@@ -295,7 +300,7 @@
fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
-type scope_desc = (typ * int) list * (styp * int) list
+type scope_desc = (typ * int) list * ((string * typ) * int) list
fun is_surely_inconsistent_card_assign hol_ctxt binarize
(card_assigns, max_assigns) (T, k) =
@@ -311,6 +316,7 @@
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
+
fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
max_assigns =
exists (is_surely_inconsistent_card_assign hol_ctxt binarize
@@ -348,8 +354,10 @@
case kind of
Card T => ((T, the_single ks) :: card_assigns, max_assigns)
| Max x => (card_assigns, (x, the_single ks) :: max_assigns)
+
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
+
fun scope_descriptor_from_combination (hol_ctxt as {ctxt, ...}) binarize blocks
columns =
let--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 03 22:33:22 2014 +0100
@@ -7,7 +7,6 @@
signature NITPICK_UTIL =
sig
- type styp = string * typ
datatype polarity = Pos | Neg | Neut
exception ARG of string * string
@@ -61,7 +60,6 @@
val int_T : typ
val simple_string_of_typ : typ -> string
val num_binder_types : typ -> int
- val is_real_constr : theory -> string * typ -> bool
val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
@@ -84,8 +82,6 @@
structure Nitpick_Util : NITPICK_UTIL =
struct
-type styp = string * typ
-
datatype polarity = Pos | Neg | Neut
exception ARG of string * string
@@ -154,6 +150,7 @@
| replicate_list n xs = xs @ replicate_list (n - 1) xs
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
+
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
fun filter_indices js xs =
@@ -164,6 +161,7 @@
| aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
"indices unordered or out of range")
in aux 0 js xs end
+
fun filter_out_indices js xs =
let
fun aux _ [] xs = xs
@@ -212,6 +210,7 @@
(SOME key) of
SOME z => SOME z
| NONE => ps |> find_first (is_none o fst) |> Option.map snd
+
fun triple_lookup _ [(NONE, z)] _ = SOME z
| triple_lookup eq ps key =
case AList.lookup (op =) ps (SOME key) of
@@ -242,6 +241,7 @@
val string_of_time = ATP_Util.string_of_time
val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
+
fun nat_subscript n =
n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
@@ -260,16 +260,6 @@
val num_binder_types = BNF_Util.num_binder_types
-fun is_real_constr thy (s, T) =
- case body_type T of
- Type (s', _) =>
- (case Datatype.get_constrs thy s' of
- SOME constrs =>
- List.exists (fn (cname, cty) =>
- cname = s andalso Sign.typ_instance thy (T, cty)) constrs
- | NONE => false)
- | _ => false
-
fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
| typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
@@ -309,6 +299,7 @@
val unyxml = ATP_Util.unyxml
val maybe_quote = ATP_Util.maybe_quote
+
fun pretty_maybe_quote pretty =
let val s = Pretty.str_of pretty in
if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]