# HG changeset patch # User blanchet # Date 1393882402 -3600 # Node ID 6bfbec3dff62ddd8a4b9a6bc2a93a879b560aa10 # Parent cac1add157e8cb82b36612bcbceb8c7af81dd37c tuned code diff -r cac1add157e8 -r 6bfbec3dff62 NEWS --- 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). diff -r cac1add157e8 -r 6bfbec3dff62 src/Doc/Nitpick/document/root.tex --- 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} diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 "\length xs = 1; length ys = 1\ \ xs = ys" -nitpick [show_datatypes, expect = genuine] +nitpick [show_types, expect = genuine] oops @@ -111,7 +111,7 @@ definition C :: three where "C \ Abs_three 2" lemma "\A \ X; B \ X\ \ c \ 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\point) = Xcoord (q\point)" -nitpick [show_datatypes, expect = genuine] +nitpick [show_types, expect = genuine] oops lemma "4 * x + 3 * (y\real) \ 1 / 2" -nitpick [show_datatypes, expect = genuine] +nitpick [show_types, expect = genuine] oops @@ -217,7 +217,7 @@ oops lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" -nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] +nitpick [bisim_depth = -1, show_types, expect = quasi_genuine] nitpick [card = 1\5, expect = none] sorry diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/kodkod.ML --- 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" diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/kodkod_sat.ML --- 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 diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick.ML --- 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) = diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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, diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 [] diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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}) diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- 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)) = diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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) diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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), diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 diff -r cac1add157e8 -r 6bfbec3dff62 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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]