# HG changeset patch # User blanchet # Date 1266405261 -3600 # Node ID bb64d089c643ab621162bc0b1326de2c428cbc3d # Parent 58b9503a7f9adc5ee9536c9582adcd16b5f5536f# Parent 9b8f351cced6dcc2eab5e458124f8b8c0d6be0bf merged diff -r 58b9503a7f9a -r bb64d089c643 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Feb 17 11:21:59 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Feb 17 12:14:21 2010 +0100 @@ -472,7 +472,9 @@ \prew \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] -\slshape Nitpick found a potential counterexample: \\[2\smallskipamount] +\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported +fragment. Only potential counterexamples may be found. \\[2\smallskipamount] +Nitpick found a potential counterexample: \\[2\smallskipamount] \hbox{}\qquad Free variable: \nopagebreak \\ \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] Confirmation by ``\textit{auto}'': The above counterexample is genuine. @@ -1331,7 +1333,7 @@ and this time \textit{arith} can finish off the subgoals. A similar technique can be employed for structural induction. The -following mini-formalization of full binary trees will serve as illustration: +following mini formalization of full binary trees will serve as illustration: \prew \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount] @@ -1350,8 +1352,7 @@ obtained by swapping $a$ and $b$: \prew -\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\ -\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$'' +\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$'' \postw Nitpick can't find any counterexample, so we proceed with induction @@ -1369,48 +1370,47 @@ \prew \slshape -Hint: To check that the induction hypothesis is general enough, try the following command: -\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}]. +Hint: To check that the induction hypothesis is general enough, try this command: +\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}]. \postw If we follow the hint, we get a ``nonstandard'' counterexample for the step: \prew -\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount] +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount] \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $a = a_1$ \\ \hbox{}\qquad\qquad $b = a_2$ \\ \hbox{}\qquad\qquad $t = \xi_1$ \\ \hbox{}\qquad\qquad $u = \xi_2$ \\ +\hbox{}\qquad Datatype: \nopagebreak \\ +\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\ \hbox{}\qquad {\slshape Constants:} \nopagebreak \\ \hbox{}\qquad\qquad $\textit{labels} = \undef (\!\begin{aligned}[t]% - & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING - & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt] - & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\ + & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt] + & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\ \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef (\!\begin{aligned}[t]% & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt] - & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt] - & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount] + & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount] The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}''). \postw Reading the Nitpick manual is a most excellent idea. -But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'' -option told the tool to look for nonstandard models of binary trees, which -means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in -addition to the standard trees generated by the \textit{Leaf} and -\textit{Branch} constructors.% +But what's going on? The \textit{non\_std} option told the tool to look for +nonstandard models of binary trees, which means that new ``nonstandard'' trees +$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees +generated by the \textit{Leaf} and \textit{Branch} constructors.% \footnote{Notice the similarity between allowing nonstandard trees here and allowing unreachable states in the preceding example (by removing the ``$n \in \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the set of objects over which the induction is performed while doing the step in order to test the induction hypothesis's strength.} -The new trees are so nonstandard that we know nothing about them, except what -the induction hypothesis states and what can be proved about all trees without -relying on induction or case distinction. The key observation is, +Unlike standard trees, these new trees contain cycles. We will see later that +every property of acyclic trees that can be proved without using induction also +holds for cyclic trees. Hence, % \begin{quote} \textsl{If the induction @@ -1418,9 +1418,9 @@ objects, and Nitpick won't find any nonstandard counterexample.} \end{quote} % -But here, Nitpick did find some nonstandard trees $t = \xi_1$ -and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin -\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$. +But here the tool find some nonstandard trees $t = \xi_1$ +and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in +\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$. Because neither tree contains both $a$ and $b$, the induction hypothesis tells us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$, and as a result we know nothing about the labels of the tree diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Nitpick.thy Wed Feb 17 12:14:21 2010 +0100 @@ -37,7 +37,6 @@ and bisim_iterator_max :: bisim_iterator and Quot :: "'a \ 'b" and quot_normal :: "'a \ 'a" - and NonStd :: "'a \ 'b" and Tha :: "('a \ bool) \ 'a" datatype ('a, 'b) pair_box = PairBox 'a 'b @@ -45,7 +44,6 @@ typedecl unsigned_bit typedecl signed_bit -typedecl \ datatype 'a word = Word "('a set)" @@ -254,12 +252,12 @@ setup {* Nitpick_Isar.setup *} hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf' + bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \ word +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 12:14:21 2010 +0100 @@ -259,14 +259,14 @@ (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" -lemma "\a \ labels t; b \ labels t; a \ b\ \ labels (swap t a b) = labels t" +lemma "{a, b} \ labels t \ labels (swap t a b) = labels t" nitpick proof (induct t) case Leaf thus ?case by simp next case (Branch t u) thus ?case nitpick - nitpick [non_std "'a bin_tree", show_consts] + nitpick [non_std, show_all] oops lemma "labels (swap t a b) = diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 12:14:21 2010 +0100 @@ -167,6 +167,7 @@ val max_arity : int -> int val arity_of_rel_expr : rel_expr -> int + val is_problem_trivially_false : problem -> bool val problems_equivalent : problem -> problem -> bool val solve_any_problem : bool -> Time.time option -> int -> int -> problem list -> outcome @@ -491,6 +492,10 @@ | arity_of_decl (DeclSome ((n, _), _)) = n | arity_of_decl (DeclSet ((n, _), _)) = n +(* problem -> bool *) +fun is_problem_trivially_false ({formula = False, ...} : problem) = true + | is_problem_trivially_false _ = false + (* string -> bool *) val is_relevant_setting = not o member (op =) ["solver", "delay"] @@ -1014,7 +1019,7 @@ val indexed_problems = if j >= 0 then [(j, nth problems j)] else - filter (not_equal False o #formula o snd) + filter (is_problem_trivially_false o snd) (0 upto length problems - 1 ~~ problems) val triv_js = filter_out (AList.defined (op =) indexed_problems) (0 upto length problems - 1) diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 17 12:14:21 2010 +0100 @@ -9,7 +9,7 @@ sig val configured_sat_solvers : bool -> string list val smart_sat_solver_name : bool -> string - val sat_solver_spec : bool -> string -> string * string list + val sat_solver_spec : string -> string * string list end; structure Kodkod_SAT : KODKOD_SAT = @@ -51,15 +51,15 @@ ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"], "s SATISFIABLE", "v ", "s UNSATISFIABLE"))] -(* bool -> string -> sink -> string -> string -> string list -> string list +(* string -> sink -> string -> string -> string list -> string list -> (string * (unit -> string list)) option *) -fun dynamic_entry_for_external overlord name dev home exec args markers = +fun dynamic_entry_for_external name dev home exec args markers = case getenv home of "" => NONE | dir => SOME (name, fn () => let - val serial_str = if overlord then "" else serial_string () + val serial_str = serial_string () val base = name ^ serial_str val out_file = base ^ ".out" val dir_sep = @@ -76,9 +76,9 @@ end) (* bool -> bool -> string * sat_solver_info -> (string * (unit -> string list)) option *) -fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) = +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 (name, Internal (JNI, mode, ss)) = + | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) = if incremental andalso mode = Batch then NONE else @@ -92,26 +92,25 @@ else NONE end - | dynamic_entry_for_info overlord false - (name, External (dev, home, exec, args)) = - dynamic_entry_for_external overlord name dev home exec args [] - | dynamic_entry_for_info overlord false + | dynamic_entry_for_info false (name, External (dev, home, exec, args)) = + dynamic_entry_for_external name dev home exec args [] + | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) = - dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3] - | dynamic_entry_for_info _ true _ = NONE -(* bool -> bool -> (string * (unit -> string list)) list *) -fun dynamic_list overlord incremental = - map_filter (dynamic_entry_for_info overlord incremental) static_list + dynamic_entry_for_external name dev home exec args [m1, m2, m3] + | dynamic_entry_for_info true _ = NONE +(* bool -> (string * (unit -> string list)) list *) +fun dynamic_list incremental = + map_filter (dynamic_entry_for_info incremental) static_list (* bool -> string list *) -val configured_sat_solvers = map fst o dynamic_list false +val configured_sat_solvers = map fst o dynamic_list (* bool -> string *) -val smart_sat_solver_name = fst o hd o dynamic_list false +val smart_sat_solver_name = fst o hd o dynamic_list -(* bool -> string -> string * string list *) -fun sat_solver_spec overlord name = +(* string -> string * string list *) +fun sat_solver_spec name = let - val dyn_list = dynamic_list overlord false + val dyn_list = dynamic_list false (* (string * 'a) list -> string *) fun enum_solvers solvers = commas (distinct (op =) (map (quote o fst) solvers)) diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 12:14:21 2010 +0100 @@ -84,7 +84,7 @@ fun atom_from_formula f = RelIf (f, true_atom, false_atom) (* Proof.context -> (typ -> int) -> styp list -> term -> formula *) -fun kodkod_formula_for_term ctxt card frees = +fun kodkod_formula_from_term ctxt card frees = let (* typ -> rel_expr -> rel_expr *) fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r = @@ -145,7 +145,7 @@ | Term.Var _ => raise SAME () | Bound _ => raise SAME () | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s) - | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t])) + | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t])) handle SAME () => formula_from_atom (to_R_rep Ts t) (* typ list -> term -> rel_expr *) and to_S_rep Ts t = @@ -306,7 +306,7 @@ val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees val declarative_axioms = map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees - val formula = kodkod_formula_for_term ctxt card frees neg_t + val formula = kodkod_formula_from_term ctxt card frees neg_t |> fold_rev (curry And) declarative_axioms val univ_card = univ_card 0 0 0 bounds formula val problem = diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 12:14:21 2010 +0100 @@ -130,7 +130,7 @@ sel_names: nut list, nonsel_names: nut list, rel_table: nut NameTable.table, - liberal: bool, + unsound: bool, scope: scope, core: KK.formula, defs: KK.formula list} @@ -157,15 +157,15 @@ (Path.variable "ISABELLE_HOME_USER" :: map Path.basic ["etc", "components"]))) ^ "\"." -val max_liberal_delay_ms = 200 -val max_liberal_delay_percent = 2 +val max_unsound_delay_ms = 200 +val max_unsound_delay_percent = 2 (* Time.time option -> int *) -fun liberal_delay_for_timeout NONE = max_liberal_delay_ms - | liberal_delay_for_timeout (SOME timeout) = - Int.max (0, Int.min (max_liberal_delay_ms, +fun unsound_delay_for_timeout NONE = max_unsound_delay_ms + | unsound_delay_for_timeout (SOME timeout) = + Int.max (0, Int.min (max_unsound_delay_ms, Time.toMilliseconds timeout - * max_liberal_delay_percent div 100)) + * max_unsound_delay_percent div 100)) (* Time.time option -> bool *) fun passed_deadline NONE = false @@ -247,7 +247,7 @@ (if i <> 1 orelse n <> 1 then "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n else - "goal")) [orig_t])) + "goal")) [Logic.list_implies (orig_assm_ts, orig_t)])) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t val assms_t = if assms orelse auto then @@ -382,29 +382,22 @@ else () val deep_dataTs = filter is_deep_datatype all_Ts - (* FIXME: Implement proper detection of induction datatypes. *) + (* This detection code is an ugly hack. Fortunately, it is used only to + provide a hint to the user. *) (* string * (Rule_Cases.T * bool) -> bool *) - fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) = - false -(* - not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes -*) - (* unit -> typ list *) - val induct_dataTs = - if exists is_inductive_case (ProofContext.cases_of ctxt) then - filter (is_datatype thy) all_Ts - else - [] - val _ = if standard andalso not (null induct_dataTs) then + fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) = + not (null fixes) andalso + exists (String.isSuffix ".hyps" o fst) assumes andalso + exists (exists (curry (op =) name o shortest_name o fst) + o datatype_constrs hol_ctxt) deep_dataTs + val likely_in_struct_induct_step = + exists is_struct_induct_step (ProofContext.cases_of ctxt) + val _ = if standard andalso likely_in_struct_induct_step then pprint_m (fn () => Pretty.blk (0, pstrs "Hint: To check that the induction hypothesis is \ - \general enough, try the following command: " @ + \general enough, try this command: " @ [Pretty.mark Markup.sendback (Pretty.blk (0, - pstrs ("nitpick [" ^ - commas (map (prefix "non_std " o maybe_quote - o unyxml o string_for_type ctxt) - induct_dataTs) ^ - ", show_consts]")))] @ pstrs ".")) + pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) else () (* @@ -441,7 +434,7 @@ val too_big_scopes = Unsynchronized.ref [] (* bool -> scope -> rich_problem option *) - fun problem_for_scope liberal + fun problem_for_scope unsound (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = let val _ = not (exists (fn other => scope_less_eq other scope) @@ -476,10 +469,10 @@ (univ_card nat_card int_card main_j0 [] KK.True) val _ = check_arity min_univ_card min_highest_arity - val core_u = choose_reps_in_nut scope liberal rep_table false core_u - val def_us = map (choose_reps_in_nut scope liberal rep_table true) + val core_u = choose_reps_in_nut scope unsound rep_table false core_u + val def_us = map (choose_reps_in_nut scope unsound rep_table true) def_us - val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) + val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) nondef_us (* val _ = List.app (priority o string_for_nut ctxt) @@ -495,21 +488,19 @@ val core_u = rename_vars_in_nut pool rel_table core_u val def_us = map (rename_vars_in_nut pool rel_table) def_us val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us - (* nut -> KK.formula *) - val to_f = kodkod_formula_from_nut bits ofs liberal kk - val core_f = to_f core_u - val def_fs = map to_f def_us - val nondef_fs = map to_f nondef_us + val core_f = kodkod_formula_from_nut bits ofs kk core_u + val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us + val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us val formula = fold (fold s_and) [def_fs, nondef_fs] core_f - val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ + val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ PrintMode.setmp [] multiline_string_for_scope scope val kodkod_sat_solver = - Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd + Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd val bit_width = if bits = 0 then 16 else bits + 1 - val delay = if liberal then + val delay = if unsound then Option.map (fn time => Time.- (time, Time.now ())) deadline - |> liberal_delay_for_timeout + |> unsound_delay_for_timeout else 0 val settings = [("solver", commas (map quote kodkod_sat_solver)), @@ -547,13 +538,13 @@ expr_assigns = [], formula = formula}, {free_names = free_names, sel_names = sel_names, nonsel_names = nonsel_names, rel_table = rel_table, - liberal = liberal, scope = scope, core = core_f, + unsound = unsound, scope = scope, core = core_f, defs = nondef_fs @ def_fs @ declarative_axioms}) end handle TOO_LARGE (loc, msg) => if loc = "Nitpick_Kodkod.check_arity" andalso not (Typtab.is_empty ofs) then - problem_for_scope liberal + problem_for_scope unsound {hol_ctxt = hol_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = Typtab.empty} @@ -563,13 +554,13 @@ else (Unsynchronized.change too_big_scopes (cons scope); print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if liberal then "potential" + ". Skipping " ^ (if unsound then "potential" else "genuine") ^ " component of scope.")); NONE) | TOO_SMALL (loc, msg) => (print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if liberal then "potential" + ". Skipping " ^ (if unsound then "potential" else "genuine") ^ " component of scope.")); NONE) @@ -584,7 +575,7 @@ val scopes = Unsynchronized.ref [] val generated_scopes = Unsynchronized.ref [] - val generated_problems = Unsynchronized.ref [] + val generated_problems = Unsynchronized.ref ([] : rich_problem list) val checked_problems = Unsynchronized.ref (SOME []) val met_potential = Unsynchronized.ref 0 @@ -635,7 +626,7 @@ | NONE => print "No confirmation by \"auto\".") else (); - if not standard andalso not (null induct_dataTs) then + if not standard andalso likely_in_struct_induct_step then print "The existence of a nonstandard model suggests that the \ \induction hypothesis is not general enough or perhaps even \ \wrong. See the \"Inductive Properties\" section of the \ @@ -718,7 +709,7 @@ | KK.Normal (sat_ps, unsat_js) => let val (lib_ps, con_ps) = - List.partition (#liberal o snd o nth problems o fst) sat_ps + List.partition (#unsound o snd o nth problems o fst) sat_ps in update_checked_problems problems (unsat_js @ map fst lib_ps); if null con_ps then @@ -735,9 +726,9 @@ (0, 0, donno) else let - (* "co_js" is the list of conservative problems whose - liberal pendants couldn't be satisfied and hence that - most probably can't be satisfied themselves. *) + (* "co_js" is the list of sound problems whose unsound + pendants couldn't be satisfied and hence that most + probably can't be satisfied themselves. *) val co_js = map (fn j => j - 1) unsat_js |> filter (fn j => @@ -750,7 +741,7 @@ val problems = problems |> filter_out_indices bye_js |> max_potential <= 0 - ? filter_out (#liberal o snd) + ? filter_out (#unsound o snd) in solve_any_problem max_potential max_genuine donno false problems @@ -770,7 +761,7 @@ (map fst sat_ps @ unsat_js) val problems = problems |> filter_out_indices bye_js - |> filter_out (#liberal o snd) + |> filter_out (#unsound o snd) in solve_any_problem 0 max_genuine donno false problems end end end @@ -814,10 +805,10 @@ () (* scope * bool -> rich_problem list * bool -> rich_problem list * bool *) - fun add_problem_for_scope (scope as {datatypes, ...}, liberal) + fun add_problem_for_scope (scope as {datatypes, ...}, unsound) (problems, donno) = (check_deadline (); - case problem_for_scope liberal scope of + case problem_for_scope unsound scope of SOME problem => (problems |> (null problems orelse @@ -833,6 +824,28 @@ ([], donno) val _ = Unsynchronized.change generated_problems (append problems) val _ = Unsynchronized.change generated_scopes (append scopes) + val _ = + if j + 1 = n then + let + val (unsound_problems, sound_problems) = + List.partition (#unsound o snd) (!generated_problems) + in + if not (null sound_problems) andalso + forall (KK.is_problem_trivially_false o fst) + sound_problems then + print_m (fn () => + "Warning: The conjecture either trivially holds or (more \ + \likely) lies outside Nitpick's supported fragment." ^ + (if exists (not o KK.is_problem_trivially_false o fst) + unsound_problems then + " Only potential counterexamples may be found." + else + "")) + else + () + end + else + () in solve_any_problem max_potential max_genuine donno true (rev problems) end @@ -845,7 +858,7 @@ let (* rich_problem list -> rich_problem list *) val do_filter = - if !met_potential = max_potential then filter_out (#liberal o snd) + if !met_potential = max_potential then filter_out (#unsound o snd) else I val total = length (!scopes) val unsat = @@ -874,7 +887,7 @@ if max_potential = original_max_potential then (print_m (fn () => "Nitpick found no " ^ das_wort_model ^ "." ^ - (if not standard andalso not (null induct_dataTs) then + (if not standard andalso likely_in_struct_induct_step then " This suggests that the induction hypothesis might be \ \general enough to prove this subgoal." else diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 12:14:21 2010 +0100 @@ -97,6 +97,7 @@ val dest_n_tuple : int -> term -> term list val instantiate_type : theory -> typ -> typ -> typ -> typ val is_real_datatype : theory -> string -> bool + val is_standard_datatype : hol_context -> typ -> bool val is_quot_type : theory -> typ -> bool val is_codatatype : theory -> typ -> bool val is_pure_typedef : theory -> typ -> bool @@ -574,6 +575,10 @@ (* theory -> string -> bool *) val is_typedef = is_some oo typedef_info val is_real_datatype = is_some oo Datatype.get_info +(* hol_context -> typ -> bool *) +fun is_standard_datatype ({thy, stds, ...} : hol_context) = + the o triple_lookup (type_match thy) stds + (* theory -> typ -> bool *) fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *) | is_quot_type _ (Type ("FSet.fset", _)) = true @@ -828,9 +833,8 @@ fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T) fun suc_const T = Const (@{const_name Suc}, T --> T) -(* hol_context -> typ -> styp list *) -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context) - (T as Type (s, Ts)) = +(* theory -> typ -> styp list *) +fun uncached_datatype_constrs thy (T as Type (s, Ts)) = (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' | _ => @@ -843,8 +847,6 @@ map (fn (s', Us) => (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) constrs - |> (triple_lookup (type_match thy) stds T |> the |> not) ? - cons (@{const_name NonStd}, @{typ \} --> T) end | NONE => if is_record_type T then @@ -867,11 +869,11 @@ []) | uncached_datatype_constrs _ _ = [] (* hol_context -> typ -> styp list *) -fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T = +fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T = case AList.lookup (op =) (!constr_cache) T of SOME xs => xs | NONE => - let val xs = uncached_datatype_constrs hol_ctxt T in + let val xs = uncached_datatype_constrs thy T in (Unsynchronized.change constr_cache (cons (T, xs)); xs) end fun boxed_datatype_constrs hol_ctxt = @@ -957,10 +959,6 @@ | _ => list_comb (Const x, args) end -(* The higher this number is, the more nonstandard models can be generated. It's - not important enough to be a user option, though. *) -val xi_card = 8 - (* (typ * int) list -> typ -> int *) fun card_of_type assigns (Type ("fun", [T1, T2])) = reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) @@ -970,7 +968,6 @@ | card_of_type _ @{typ prop} = 2 | card_of_type _ @{typ bool} = 2 | card_of_type _ @{typ unit} = 1 - | card_of_type _ @{typ \} = xi_card | card_of_type assigns T = case AList.lookup (op =) assigns T of SOME k => k @@ -1027,7 +1024,6 @@ | @{typ prop} => 2 | @{typ bool} => 2 | @{typ unit} => 1 - | @{typ \} => xi_card | Type _ => (case datatype_constrs hol_ctxt T of [] => if is_integer_type T orelse is_bit_type T then 0 @@ -1393,21 +1389,11 @@ fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T = let val xs = datatype_constrs hol_ctxt dataT - val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs - val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs' + val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs + val (xs', x) = split_last xs in - (if length xs = length xs' then - let - val (xs'', x) = split_last xs' - in - constr_case_body thy (1, x) - |> fold_rev (add_constr_case hol_ctxt res_T) - (length xs' downto 2 ~~ xs'') - end - else - Const (@{const_name undefined}, dataT --> res_T) $ Bound 0 - |> fold_rev (add_constr_case hol_ctxt res_T) - (length xs' downto 1 ~~ xs')) + constr_case_body thy (1, x) + |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs') |> fold_rev (curry absdummy) (func_Ts @ [dataT]) end @@ -1738,10 +1724,11 @@ (tac ctxt (auto_tac (clasimpset_of ctxt)))) #> the #> Goal.finish ctxt) goal -val max_cached_wfs = 100 -val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime) -val cached_wf_props : (term * bool) list Unsynchronized.ref = - Unsynchronized.ref [] +val max_cached_wfs = 50 +val cached_timeout = + Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime) +val cached_wf_props = + Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac] @@ -1772,19 +1759,20 @@ else () in - if tac_timeout = (!cached_timeout) andalso - length (!cached_wf_props) < max_cached_wfs then + if tac_timeout = Synchronized.value cached_timeout andalso + length (Synchronized.value cached_wf_props) < max_cached_wfs then () else - (cached_wf_props := []; cached_timeout := tac_timeout); - case AList.lookup (op =) (!cached_wf_props) prop of + (Synchronized.change cached_wf_props (K []); + Synchronized.change cached_timeout (K tac_timeout)); + case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of SOME wf => wf | NONE => let val goal = prop |> cterm_of thy |> Goal.init val wf = exists (terminates_by ctxt tac_timeout goal) termination_tacs - in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end + in Synchronized.change cached_wf_props (cons (prop, wf)); wf end end) handle List.Empty => false | NO_TRIPLE () => false @@ -1799,14 +1787,14 @@ SOME (SOME b) => b | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse case AList.lookup (op =) (!wf_cache) x of - SOME (_, wf) => wf - | NONE => - let - val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) - val wf = uncached_is_well_founded_inductive_pred hol_ctxt x - in - Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf - end + SOME (_, wf) => wf + | NONE => + let + val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) + val wf = uncached_is_well_founded_inductive_pred hol_ctxt x + in + Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf + end (* typ list -> typ -> typ -> term -> term *) fun ap_curry [_] _ _ t = t @@ -2032,8 +2020,7 @@ | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum | Type (_, Ts) => - if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: - @{typ \} :: accum) T then + if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then accum else T :: accum diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 12:14:21 2010 +0100 @@ -36,7 +36,7 @@ hol_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list val kodkod_formula_from_nut : - int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula + int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula end; structure Nitpick_Kodkod : NITPICK_KODKOD = @@ -317,7 +317,9 @@ [ts] |> not exclusive ? cons (KK.TupleSet []) else [KK.TupleSet [], - if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then + if T1 = T2 andalso epsilon > delta andalso + (datatype_spec dtypes T1 |> the |> pairf #co #standard) + = (false, true) then index_seq delta (epsilon - delta) |> map (fn j => KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]], @@ -762,6 +764,7 @@ (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> dtype_spec -> nfa_entry option *) fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE + | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} = SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes @@ -770,45 +773,47 @@ val empty_rel = KK.Product (KK.None, KK.None) (* nfa_table -> typ -> typ -> KK.rel_expr list *) -fun direct_path_rel_exprs nfa start final = - case AList.lookup (op =) nfa final of - SOME trans => map fst (filter (curry (op =) start o snd) trans) +fun direct_path_rel_exprs nfa start_T final_T = + case AList.lookup (op =) nfa final_T of + SOME trans => map fst (filter (curry (op =) start_T o snd) trans) | NONE => [] (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *) -and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = - fold kk_union (direct_path_rel_exprs nfa start final) - (if start = final then KK.Iden else empty_rel) - | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = - kk_union (any_path_rel_expr kk nfa qs start final) - (knot_path_rel_expr kk nfa qs start q final) +and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T + final_T = + fold kk_union (direct_path_rel_exprs nfa start_T final_T) + (if start_T = final_T then KK.Iden else empty_rel) + | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T = + kk_union (any_path_rel_expr kk nfa Ts start_T final_T) + (knot_path_rel_expr kk nfa Ts start_T T final_T) (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ -> KK.rel_expr *) -and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start - knot final = - kk_join (kk_join (any_path_rel_expr kk nfa qs knot final) - (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot))) - (any_path_rel_expr kk nfa qs start knot) +and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts + start_T knot_T final_T = + kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T) + (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T))) + (any_path_rel_expr kk nfa Ts start_T knot_T) (* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *) -and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = - fold kk_union (direct_path_rel_exprs nfa start start) empty_rel - | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start = - if start = q then - kk_closure (loop_path_rel_expr kk nfa qs start) +and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T = + fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel + | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts) + start_T = + if start_T = T then + kk_closure (loop_path_rel_expr kk nfa Ts start_T) else - kk_union (loop_path_rel_expr kk nfa qs start) - (knot_path_rel_expr kk nfa qs start q start) + kk_union (loop_path_rel_expr kk nfa Ts start_T) + (knot_path_rel_expr kk nfa Ts start_T T start_T) (* nfa_table -> unit NfaGraph.T *) fun graph_for_nfa nfa = let (* typ -> unit NfaGraph.T -> unit NfaGraph.T *) - fun new_node q = perhaps (try (NfaGraph.new_node (q, ()))) + fun new_node T = perhaps (try (NfaGraph.new_node (T, ()))) (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *) fun add_nfa [] = I | add_nfa ((_, []) :: nfa) = add_nfa nfa - | add_nfa ((q, ((_, q') :: transitions)) :: nfa) = - add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o - new_node q' o new_node q + | add_nfa ((T, ((_, T') :: transitions)) :: nfa) = + add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o + new_node T' o new_node T in add_nfa nfa NfaGraph.empty end (* nfa_table -> nfa_table list *) @@ -816,22 +821,22 @@ nfa |> graph_for_nfa |> NfaGraph.strong_conn |> map (fn keys => filter (member (op =) keys o fst) nfa) -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *) -fun acyclicity_axiom_for_datatype dtypes kk nfa start = +(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *) +fun acyclicity_axiom_for_datatype kk dtypes nfa start_T = #kk_no kk (#kk_intersect kk - (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) + (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden) (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> KK.formula list *) fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes = map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes |> strongly_connected_sub_nfas - |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst) - nfa) + |> maps (fn nfa => + map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa) (* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr -> constr_spec -> int -> KK.formula *) fun sel_axiom_for_sel hol_ctxt j0 - (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, + (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no, kk_join, ...}) rel_table dom_r ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec) n = @@ -862,19 +867,19 @@ [formula_for_bool honors_explicit_max] else let - val ran_r = discr_rel_expr rel_table const + val dom_r = discr_rel_expr rel_table const val max_axiom = if honors_explicit_max then KK.True else if is_twos_complement_representable bits (epsilon - delta) then - KK.LE (KK.Cardinality ran_r, KK.Num explicit_max) + KK.LE (KK.Cardinality dom_r, KK.Num explicit_max) else raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr", "\"bits\" value " ^ string_of_int bits ^ " too small for \"max\"") in max_axiom :: - map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr) + map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr) (index_seq 0 (num_sels_for_constr_type (snd const))) end end @@ -949,8 +954,8 @@ acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @ maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *) -fun kodkod_formula_from_nut bits ofs liberal +(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *) +fun kodkod_formula_from_nut bits ofs (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union, diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 12:14:21 2010 +0100 @@ -53,6 +53,8 @@ val base_mixfix = "_\<^bsub>base\<^esub>" val step_mixfix = "_\<^bsub>step\<^esub>" val abs_mixfix = "\_\" +val cyclic_co_val_name = "\" +val cyclic_type_name = "\" val opt_flag = nitpick_prefix ^ "opt" val non_opt_flag = nitpick_prefix ^ "non_opt" @@ -88,7 +90,7 @@ Const (nth_atom_name pool "" T j k, T) (* term -> real *) -fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) = +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)) (* term * term -> order *) @@ -257,14 +259,13 @@ | mk_tuple _ (t :: _) = t | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) -(* string * string * string * string -> scope -> nut list -> nut list - -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep - -> int list list -> term *) -fun reconstruct_term (maybe_name, base_name, step_name, abs_name) +(* bool -> atom_pool -> string * string * string * string -> scope -> nut list + -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ + -> typ -> rep -> int list list -> term *) +fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name) ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} : scope) sel_names rel_table bounds = let - val pool = Unsynchronized.ref [] val for_auto = (maybe_name = "") (* int list list -> int *) fun value_of_bits jss = @@ -397,13 +398,16 @@ else case datatype_spec datatypes T of NONE => nth_atom pool for_auto T j k | SOME {deep = false, ...} => nth_atom pool for_auto T j k - | SOME {co, constrs, ...} => + | SOME {co, standard, constrs, ...} => let (* styp -> int list *) fun tuples_for_const (s, T) = tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) - (* unit -> indexname * typ *) - fun var () = ((nth_atom_name pool "" T j k, 0), T) + (* unit -> term *) + fun cyclic_atom () = + nth_atom pool for_auto (Type (cyclic_type_name, [])) j k + fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T) + val discr_jsss = map (tuples_for_const o discr_for_constr o #const) constrs val real_j = j + offset_of_type ofs T @@ -428,16 +432,18 @@ map (map_filter (fn js => if hd js = real_j then SOME (tl js) else NONE)) sel_jsss val uncur_arg_Ts = binder_types constr_T + val maybe_cyclic = co orelse not standard in - if co andalso member (op =) seen (T, j) then - Var (var ()) + if maybe_cyclic andalso not (null seen) andalso + member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then + cyclic_var () else if constr_s = @{const_name Word} then HOLogic.mk_number (if T = @{typ "unsigned_bit word"} then nat_T else int_T) (value_of_bits (the_single arg_jsss)) else let - val seen = seen |> co ? cons (T, j) + val seen = seen |> maybe_cyclic ? cons (T, j) val ts = if length arg_Ts = 0 then [] @@ -459,7 +465,7 @@ 0 => mk_num 0 | n1 => case HOLogic.dest_number t2 |> snd of 1 => mk_num n1 - | n2 => Const (@{const_name Rings.divide}, + | n2 => Const (@{const_name divide}, num_T --> num_T --> num_T) $ mk_num n1 $ mk_num n2) | _ => raise TERM ("Nitpick_Model.reconstruct_term.\ @@ -469,19 +475,27 @@ (is_abs_fun thy constr_x orelse constr_s = @{const_name Quot}) then Const (abs_name, constr_T) $ the_single ts - else if not for_auto andalso - constr_s = @{const_name NonStd} then - Const (fst (dest_Const (the_single ts)), T) else list_comb (Const constr_x, ts) in - if co then - let val var = var () in - if exists_subterm (curry (op =) (Var var)) t then - Const (@{const_name The}, (T --> bool_T) --> T) - $ Abs ("\", T, - Const (@{const_name "op ="}, T --> T --> bool_T) - $ Bound 0 $ abstract_over (Var var, t)) + if maybe_cyclic then + let val var = cyclic_var () in + if elaborate andalso not standard andalso + length seen = 1 andalso + exists_subterm (fn Const (s, _) => + String.isPrefix cyclic_type_name s + | t' => t' = var) t then + let val atom = cyclic_atom () in + HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t) + end + else if exists_subterm (curry (op =) var) t then + if co then + Const (@{const_name The}, (T --> bool_T) --> T) + $ Abs (cyclic_co_val_name, T, + Const (@{const_name "op ="}, T --> T --> bool_T) + $ Bound 0 $ abstract_over (var, t)) + else + cyclic_atom () else t end @@ -537,17 +551,15 @@ raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ string_of_int (length jss)) - in - polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] - end + in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end -(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut - -> term *) -fun term_for_name scope sel_names rel_table bounds name = +(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list + -> nut -> term *) +fun term_for_name pool scope sel_names rel_table bounds name = let val T = type_of name in tuple_list_for_name rel_table bounds name - |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T - (rep_of name) + |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table + bounds T T (rep_of name) end (* Proof.context -> (string * string * string * string) * Proof.context *) @@ -610,6 +622,7 @@ card_assigns, bits, bisim_depth, datatypes, ofs} : scope) formats all_frees free_names sel_names nonsel_names rel_table bounds = let + val pool = Unsynchronized.ref [] val (wacky_names as (_, base_name, step_name, _), ctxt) = add_wacky_syntax ctxt val hol_ctxt = @@ -629,11 +642,13 @@ val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} - (* typ -> typ -> rep -> int list list -> term *) - val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table - bounds + (* bool -> typ -> typ -> rep -> int list list -> term *) + fun term_for_rep elaborate = + reconstruct_term elaborate pool wacky_names scope sel_names rel_table + bounds (* nat -> typ -> nat -> typ *) - fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]] + fun nth_value_of_type card T n = + term_for_rep true T T (Atom (card, 0)) [[n]] (* nat -> typ -> typ list *) fun all_values_of_type card T = index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord @@ -666,7 +681,7 @@ Const (@{const_name undefined}, T') else tuple_list_for_name rel_table bounds name - |> term_for_rep T T' (rep_of name) + |> term_for_rep false T T' (rep_of name) in Pretty.block (Pretty.breaks [setmp_show_all_types (Syntax.pretty_term ctxt) t1, @@ -682,7 +697,8 @@ (* typ -> dtype_spec list *) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, - complete = false, concrete = true, deep = true, constrs = []}] + standard = true, complete = false, concrete = true, deep = true, + constrs = []}] handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = datatypes |> filter #deep |> List.partition #co @@ -758,7 +774,7 @@ (* nut -> term *) fun free_name_assm name = HOLogic.mk_eq (Free (nickname_of name, type_of name), - term_for_name scope sel_names rel_table bounds name) + term_for_name pool scope sel_names rel_table bounds name) val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) val model_assms = map free_name_assm free_names val assm = foldr1 s_conj (freeT_assms @ model_assms) diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 12:14:21 2010 +0100 @@ -892,7 +892,7 @@ (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *) fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}) - liberal table def = + unsound table def = let val bool_atom_R = Atom (2, offset_of_type ofs bool_T) (* polarity -> bool -> rep *) @@ -1036,7 +1036,7 @@ if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2' else opt_opt_case () in - if liberal orelse polar = Neg orelse + if unsound orelse polar = Neg orelse is_concrete_type datatypes (type_of u1) then case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of (true, true) => opt_opt_case () @@ -1138,7 +1138,7 @@ else let val quant_u = s_op2 oper T (Formula polar) u1' u2' in if def orelse - (liberal andalso (polar = Pos) = (oper = All)) orelse + (unsound andalso (polar = Pos) = (oper = All)) orelse is_complete_type datatypes (type_of u1) then quant_u else diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 12:14:21 2010 +0100 @@ -22,6 +22,7 @@ typ: typ, card: int, co: bool, + standard: bool, complete: bool, concrete: bool, deep: bool, @@ -71,6 +72,7 @@ typ: typ, card: int, co: bool, + standard: bool, complete: bool, concrete: bool, deep: bool, @@ -162,7 +164,7 @@ fun miscs () = (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @ (if bisim_depth < 0 andalso forall (not o #co) datatypes then [] - else ["bisim_depth = " ^ string_of_int bisim_depth]) + else ["bisim_depth = " ^ signed_string_of_int bisim_depth]) in setmp_show_all_types (fn () => (cards primary_card_assigns, cards secondary_card_assigns, @@ -466,6 +468,7 @@ let val deep = member (op =) deep_dataTs T val co = is_codatatype thy T + val standard = is_standard_datatype hol_ctxt T val xs = boxed_datatype_constrs hol_ctxt T val self_recs = map (is_self_recursive_constr_type o snd) xs val (num_self_recs, num_non_self_recs) = @@ -481,8 +484,8 @@ num_non_self_recs) (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) [] in - {typ = T, card = card, co = co, complete = complete, concrete = concrete, - deep = deep, constrs = constrs} + {typ = T, card = card, co = co, standard = standard, complete = complete, + concrete = concrete, deep = deep, constrs = constrs} end (* int -> int *) diff -r 58b9503a7f9a -r bb64d089c643 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 11:21:59 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 12:14:21 2010 +0100 @@ -308,7 +308,7 @@ NameTable.empty val u = Op1 (Not, type_of u, rep_of u, u) |> rename_vars_in_nut pool table - val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u + val formula = kodkod_formula_from_nut bits Typtab.empty constrs u val bounds = map (bound_for_plain_rel ctxt debug) free_rels val univ_card = univ_card nat_card int_card j0 bounds formula val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)