1.1 --- a/NEWS Tue Jun 01 17:36:53 2010 +0200
1.2 +++ b/NEWS Tue Jun 01 20:52:01 2010 +0200
1.3 @@ -425,8 +425,10 @@
1.4 - Improved efficiency of "destroy_constrs" optimization.
1.5 - Fixed soundness bugs related to "destroy_constrs" optimization and
1.6 record getters.
1.7 - - Fixed soundness bug related to higher-order constructors
1.8 + - Fixed soundness bug related to higher-order constructors.
1.9 + - Fixed soundness bug when "full_descrs" is enabled.
1.10 - Improved precision of set constructs.
1.11 + - Added "atoms" option.
1.12 - Added cache to speed up repeated Kodkod invocations on the same
1.13 problems.
1.14 - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
1.15 @@ -434,6 +436,7 @@
1.16 "SAT4J_Light". INCOMPATIBILITY.
1.17 - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
1.18 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
1.19 + - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
1.20
1.21 * Moved the SMT binding into the HOL image.
1.22
2.1 --- a/doc-src/Nitpick/nitpick.tex Tue Jun 01 17:36:53 2010 +0200
2.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Jun 01 20:52:01 2010 +0200
2.3 @@ -1897,6 +1897,8 @@
2.4
2.5 \begin{enum}
2.6 \item[$\bullet$] \qtybf{string}: A string.
2.7 +\item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
2.8 +(e.g., ``\textit{ichi ni san}'').
2.9 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
2.10 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
2.11 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
2.12 @@ -2256,6 +2258,19 @@
2.13 counterexamples. This option suffers from an ``observer effect'': Nitpick might
2.14 find different counterexamples for different values of this option.
2.15
2.16 +\oparg{atoms}{type}{string\_list}
2.17 +Specifies the names to use to refer to the atoms of the given type. By default,
2.18 +Nitpick generates names of the form $a_1, \ldots, a_n$, where $a$ is the first
2.19 +letter of the type's name.
2.20 +
2.21 +\opnodefault{atoms}{string\_list}
2.22 +Specifies the default names to use to refer to atoms of any type. For example,
2.23 +to call the three atoms of type ${'}a$ \textit{ichi}, \textit{ni}, and
2.24 +\textit{san} instead of $a_1$, $a_2$, $a_3$, specify the option
2.25 +``\textit{atoms}~${'}a$ = \textit{ichi~ni~san}''. The default names can be
2.26 +overridden on a per-type basis using the \textit{atoms}~\qty{type} option
2.27 +described above.
2.28 +
2.29 \oparg{format}{term}{int\_seq}
2.30 Specifies how to uncurry the value displayed for a variable or constant.
2.31 Uncurrying sometimes increases the readability of the output for high-arity
2.32 @@ -2563,21 +2578,6 @@
2.33
2.34 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
2.35
2.36 -\flushitem{\textit{nitpick\_intro}}
2.37 -
2.38 -\nopagebreak
2.39 -This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
2.40 -For predicates defined using the \textbf{inductive} or \textbf{coinductive}
2.41 -command, this corresponds to the \textit{intros} rules. The introduction rules
2.42 -must be of the form
2.43 -
2.44 -\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
2.45 -\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
2.46 -\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
2.47 -
2.48 -where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
2.49 -optional monotonic operator. The order of the assumptions is irrelevant.
2.50 -
2.51 \flushitem{\textit{nitpick\_choice\_spec}}
2.52
2.53 \nopagebreak
2.54 @@ -2626,9 +2626,8 @@
2.55 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
2.56 \postw
2.57
2.58 -Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
2.59 -the above rules. Nitpick then uses the \textit{lfp}-based definition in
2.60 -conjunction with these rules. To override this, we can specify an alternative
2.61 +By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
2.62 +the introduction rules. To override this, we can specify an alternative
2.63 definition as follows:
2.64
2.65 \prew
3.1 --- a/src/HOL/HOL.thy Tue Jun 01 17:36:53 2010 +0200
3.2 +++ b/src/HOL/HOL.thy Tue Jun 01 20:52:01 2010 +0200
3.3 @@ -2033,11 +2033,6 @@
3.4 val name = "nitpick_psimp"
3.5 val description = "partial equational specification of constants as needed by Nitpick"
3.6 )
3.7 -structure Nitpick_Intros = Named_Thms
3.8 -(
3.9 - val name = "nitpick_intro"
3.10 - val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
3.11 -)
3.12 structure Nitpick_Choice_Specs = Named_Thms
3.13 (
3.14 val name = "nitpick_choice_spec"
3.15 @@ -2049,7 +2044,6 @@
3.16 Nitpick_Defs.setup
3.17 #> Nitpick_Simps.setup
3.18 #> Nitpick_Psimps.setup
3.19 - #> Nitpick_Intros.setup
3.20 #> Nitpick_Choice_Specs.setup
3.21 *}
3.22
4.1 --- a/src/HOL/Library/Multiset.thy Tue Jun 01 17:36:53 2010 +0200
4.2 +++ b/src/HOL/Library/Multiset.thy Tue Jun 01 20:52:01 2010 +0200
4.3 @@ -1711,7 +1711,8 @@
4.4 | NONE => [Const (maybe_name, elem_T --> elem_T) $ t]
4.5 in
4.6 case maps elems_for (all_values elem_T) @
4.7 - (if maybe_opt then [Const (Nitpick_Model.unrep, elem_T)] else []) of
4.8 + (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)]
4.9 + else []) of
4.10 [] => Const (@{const_name zero_class.zero}, T)
4.11 | ts => foldl1 (fn (t1, t2) =>
4.12 Const (@{const_name plus_class.plus}, T --> T --> T)
5.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 01 17:36:53 2010 +0200
5.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 01 20:52:01 2010 +0200
5.3 @@ -1051,6 +1051,52 @@
5.4 nitpick [expect = none]
5.5 sorry
5.6
5.7 +lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
5.8 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.9 +nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *)
5.10 +oops
5.11 +
5.12 +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
5.13 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.14 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
5.15 +sorry
5.16 +
5.17 +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
5.18 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.19 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
5.20 +sorry
5.21 +
5.22 +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
5.23 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
5.24 +oops
5.25 +
5.26 +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
5.27 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
5.28 +oops
5.29 +
5.30 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
5.31 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.32 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
5.33 +oops
5.34 +
5.35 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
5.36 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.37 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
5.38 +oops
5.39 +
5.40 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
5.41 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
5.42 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
5.43 +sorry
5.44 +
5.45 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
5.46 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
5.47 +oops
5.48 +
5.49 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
5.50 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
5.51 +sorry
5.52 +
5.53 subsection {* Destructors and Recursors *}
5.54
5.55 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
6.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Jun 01 17:36:53 2010 +0200
6.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Jun 01 20:52:01 2010 +0200
6.3 @@ -15,7 +15,7 @@
6.4 exception FAIL
6.5
6.6 val subst = []
6.7 -val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1
6.8 +val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1
6.9 val def_table = Nitpick_HOL.const_def_table @{context} subst defs
6.10 val hol_ctxt : Nitpick_HOL.hol_context =
6.11 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
7.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Jun 01 17:36:53 2010 +0200
7.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Jun 01 20:52:01 2010 +0200
7.3 @@ -64,7 +64,7 @@
7.4 oops
7.5
7.6 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
7.7 -nitpick [fast_descrs (* ### FIXME *), expect = none]
7.8 +nitpick [expect = none]
7.9 sorry
7.10
7.11 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
8.1 --- a/src/HOL/Tools/Nitpick/HISTORY Tue Jun 01 17:36:53 2010 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,189 +0,0 @@
8.4 -Version 2010
8.5 -
8.6 - * Added and implemented "binary_ints" and "bits" options
8.7 - * Added "std" option and implemented support for nonstandard models
8.8 - * Added and implemented "finitize" option to improve the precision of infinite
8.9 - datatypes based on a monotonicity analysis
8.10 - * Added support for quotient types
8.11 - * Added support for "specification" and "ax_specification" constructs
8.12 - * Added support for local definitions (for "function" and "termination"
8.13 - proofs)
8.14 - * Added support for term postprocessors
8.15 - * Optimized "Multiset.multiset" and "FinFun.finfun"
8.16 - * Improved efficiency of "destroy_constrs" optimization
8.17 - * Fixed soundness bugs related to "destroy_constrs" optimization and record
8.18 - getters
8.19 - * Fixed soundness bug related to higher-order constructors
8.20 - * Improved precision of set constructs
8.21 - * Added cache to speed up repeated Kodkod invocations on the same problems
8.22 - * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
8.23 - "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
8.24 - * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
8.25 - "sharing_depth", and "show_skolems" options
8.26 -
8.27 -Version 2009-1
8.28 -
8.29 - * Moved into Isabelle/HOL "Main"
8.30 - * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
8.31 - "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
8.32 - "nitpick_ind_intro" to "nitpick_intro"
8.33 - * Replaced "special_depth" and "skolemize_depth" options by "specialize"
8.34 - and "skolemize"
8.35 - * Renamed "coalesce_type_vars" to "merge_type_vars"
8.36 - * Optimized Kodkod encoding of datatypes whose constructors don't appear in
8.37 - the formula to falsify
8.38 - * Added support for codatatype view of datatypes
8.39 - * Fixed soundness bug in the "uncurry" optimization
8.40 - * Fixed soundness bugs related to sets, sets of sets, (co)inductive
8.41 - predicates, typedefs, "finite", "rel_comp", and negative literals
8.42 - * Fixed monotonicity check
8.43 - * Fixed error when processing definitions
8.44 - * Fixed error in "star_linear_preds" optimization
8.45 - * Fixed error in Kodkod encoding of "The" and "Eps"
8.46 - * Fixed error in display of uncurried constants
8.47 - * Speeded up scope enumeration
8.48 -
8.49 -Version 1.2.2 (16 Oct 2009)
8.50 -
8.51 - * Added and implemented "star_linear_preds" option
8.52 - * Added and implemented "format" option
8.53 - * Added and implemented "coalesce_type_vars" option
8.54 - * Added and implemented "max_genuine" option
8.55 - * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
8.56 - "-1::nat", subset, constructors, sort axioms, and partially applied
8.57 - interpreted constants
8.58 - * Fixed error in "show_consts" for boxed specialized constants
8.59 - * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
8.60 - * Fixed display of Skolem constants
8.61 - * Fixed error in "check_potential" and "check_genuine"
8.62 - * Added boxing support for higher-order constructor parameters
8.63 - * Changed notation used for coinductive datatypes
8.64 - * Optimized Kodkod encoding of "If", "card", and "setsum"
8.65 - * Improved the monotonicity check
8.66 -
8.67 -Version 1.2.1 (25 Sep 2009)
8.68 -
8.69 - * Added explicit support for coinductive datatypes
8.70 - * Added and implemented "box" option
8.71 - * Added and implemented "fast_descrs" option
8.72 - * Added and implemented "uncurry" option
8.73 - * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
8.74 - * Fixed soundness issue related to nullary constructors
8.75 - * Fixed soundness issue related to higher-order quantifiers
8.76 - * Fixed soundness issue related to the "destroy_constrs" optimization
8.77 - * Fixed soundness issues related to the "special_depth" optimization
8.78 - * Added support for PicoSAT and incorporated it with the Nitpick package
8.79 - * Added automatic detection of installed SAT solvers based on naming
8.80 - convention
8.81 - * Optimized handling of quantifiers by moving them inward whenever possible
8.82 - * Optimized and improved precision of "wf" and "wfrec"
8.83 - * Improved handling of definitions made in locales
8.84 - * Fixed checked scope count in message shown upon interruption and timeout
8.85 - * Added minimalistic Nitpick-like tool called Minipick
8.86 -
8.87 -Version 1.2.0 (27 Jul 2009)
8.88 -
8.89 - * Optimized Kodkod encoding of datatypes and records
8.90 - * Optimized coinductive definitions
8.91 - * Fixed soundness issues related to pairs of functions
8.92 - * Fixed soundness issue in the peephole optimizer
8.93 - * Improved precision of non-well-founded predicates occurring positively in
8.94 - the formula to falsify
8.95 - * Added and implemented "destroy_constrs" option
8.96 - * Changed semantics of "inductive_mood" option to ensure soundness
8.97 - * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
8.98 - "sync_cards"
8.99 - * Improved precision of "trancl" and "rtrancl"
8.100 - * Optimized Kodkod encoding of "tranclp" and "rtranclp"
8.101 - * Made detection of inconsistent scope specifications more robust
8.102 - * Fixed a few Kodkod generation bugs
8.103 -
8.104 -Version 1.1.1 (24 Jun 2009)
8.105 -
8.106 - * Added "show_all" option
8.107 - * Fixed soundness issues related to type classes
8.108 - * Improved precision of some set constructs
8.109 - * Fiddled with the automatic monotonicity check
8.110 - * Fixed performance issues related to scope enumeration
8.111 - * Fixed a few Kodkod generation bugs
8.112 -
8.113 -Version 1.1.0 (16 Jun 2009)
8.114 -
8.115 - * Redesigned handling of datatypes to provide an interface baded on "card" and
8.116 - "max", obsoleting "mult"
8.117 - * Redesigned handling of typedefs, "rat", and "real"
8.118 - * Made "lockstep" option a three-state option and added an automatic
8.119 - monotonicity check
8.120 - * Made "batch_size" a (n + 1)-state option whose default depends on whether
8.121 - "debug" is enabled
8.122 - * Made "debug" automatically enable "verbose"
8.123 - * Added "destroy_equals" option
8.124 - * Added "no_assms" option
8.125 - * Fixed bug in computation of ground type
8.126 - * Fixed performance issue related to datatype acyclicity constraint generation
8.127 - * Fixed performance issue related to axiom selection
8.128 - * Improved precision of some well-founded inductive predicates
8.129 - * Added more checks to guard against very large cardinalities
8.130 - * Improved hit rate of potential counterexamples
8.131 - * Fixed several soundness issues
8.132 - * Optimized the Kodkod encoding to benefit more from symmetry breaking
8.133 - * Optimized relational composition, cartesian product, and converse
8.134 - * Added support for HaifaSat
8.135 -
8.136 -Version 1.0.3 (17 Mar 2009)
8.137 -
8.138 - * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
8.139 - * Added "overlord" option to assist debugging
8.140 - * Increased default value of "special_depth" option
8.141 - * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
8.142 - * Ensured that no scopes are skipped when multithreading is enabled
8.143 - * Fixed soundness issue in handling of "The", "Eps", and partial functions
8.144 - defined using Isabelle's function package
8.145 - * Fixed soundness issue in handling of non-definitional axioms
8.146 - * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
8.147 - "nat", "int", and "*"
8.148 - * Fixed a few Kodkod generation bugs
8.149 - * Optimized "div", "mod", and "dvd" on "nat" and "int"
8.150 -
8.151 -Version 1.0.2 (12 Mar 2009)
8.152 -
8.153 - * Added support for non-definitional axioms
8.154 - * Improved Isar integration
8.155 - * Added support for multiplicities of 0
8.156 - * Added "max_threads" option and support for multithreaded Kodkodi
8.157 - * Added "blocking" option to control whether Nitpick should be run
8.158 - synchronously or asynchronously
8.159 - * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
8.160 - * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
8.161 - * Introduced "auto_timeout" to specify Auto Nitpick's time limit
8.162 - * Renamed the possible values for the "expect" option
8.163 - * Renamed the "peephole" option to "peephole_optim"
8.164 - * Added negative versions of all Boolean options and made "= true" optional
8.165 - * Altered order of automatic SAT solver selection
8.166 -
8.167 -Version 1.0.1 (6 Mar 2009)
8.168 -
8.169 - * Eliminated the need to import "Nitpick" to use "nitpick"
8.170 - * Added "debug" option
8.171 - * Replaced "specialize_funs" with the more general "special_depth" option
8.172 - * Renamed "watch" option to "eval"
8.173 - * Improved parsing of "card", "mult", and "iter" options
8.174 - * Fixed a soundness bug in the "specialize_funs" optimization
8.175 - * Increased the scope of the "specialize_funs" optimization
8.176 - * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
8.177 - * Fixed a soundness bug in the "subterm property" optimization for types of
8.178 - cardinality 1
8.179 - * Improved the axiom selection for overloaded constants, which led to an
8.180 - infinite loop for "Nominal.perm"
8.181 - * Added support for multiple instantiations of non-well-founded inductive
8.182 - predicates, which previously raised an exception
8.183 - * Fixed a Kodkod generation bug
8.184 - * Altered order of scope enumeration and automatic SAT solver selection
8.185 - * Optimized "Eps", "nat_case", and "list_case"
8.186 - * Improved output formatting
8.187 - * Added checks to prevent infinite loops in axiom selector and constant
8.188 - unfolding
8.189 -
8.190 -Version 1.0.0 (27 Feb 2009)
8.191 -
8.192 - * First release
9.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 17:36:53 2010 +0200
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 20:52:01 2010 +0200
9.3 @@ -42,6 +42,7 @@
9.4 show_consts: bool,
9.5 evals: term list,
9.6 formats: (term option * int list) list,
9.7 + atomss: (typ option * string list) list,
9.8 max_potential: int,
9.9 max_genuine: int,
9.10 check_potential: bool,
9.11 @@ -112,6 +113,7 @@
9.12 show_consts: bool,
9.13 evals: term list,
9.14 formats: (term option * int list) list,
9.15 + atomss: (typ option * string list) list,
9.16 max_potential: int,
9.17 max_genuine: int,
9.18 check_potential: bool,
9.19 @@ -190,7 +192,7 @@
9.20 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
9.21 destroy_constrs, specialize, star_linear_preds, fast_descrs,
9.22 peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
9.23 - evals, formats, max_potential, max_genuine, check_potential,
9.24 + evals, formats, atomss, max_potential, max_genuine, check_potential,
9.25 check_genuine, batch_size, ...} = params
9.26 val state_ref = Unsynchronized.ref state
9.27 val pprint =
9.28 @@ -235,14 +237,9 @@
9.29 |> pairf hd tl
9.30 val original_max_potential = max_potential
9.31 val original_max_genuine = max_genuine
9.32 -(*
9.33 - val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
9.34 - val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
9.35 - orig_assm_ts
9.36 -*)
9.37 val max_bisim_depth = fold Integer.max bisim_depths ~1
9.38 val case_names = case_const_names thy stds
9.39 - val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
9.40 + val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
9.41 val def_table = const_def_table ctxt subst defs
9.42 val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
9.43 val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
9.44 @@ -322,8 +319,8 @@
9.45 ". " ^ extra
9.46 end
9.47 fun is_type_fundamentally_monotonic T =
9.48 - (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
9.49 - (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
9.50 + (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
9.51 + (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
9.52 is_number_type thy T orelse is_bit_type T
9.53 fun is_type_actually_monotonic T =
9.54 formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
9.55 @@ -369,7 +366,8 @@
9.56 else
9.57 ()
9.58 val (deep_dataTs, shallow_dataTs) =
9.59 - all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
9.60 + all_Ts |> filter (is_datatype ctxt stds)
9.61 + |> List.partition is_datatype_deep
9.62 val finitizable_dataTs =
9.63 shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
9.64 |> filter is_shallow_datatype_finitizable
9.65 @@ -579,8 +577,8 @@
9.66 val (reconstructed_model, codatatypes_ok) =
9.67 reconstruct_hol_model {show_datatypes = show_datatypes,
9.68 show_consts = show_consts}
9.69 - scope formats frees free_names sel_names nonsel_names rel_table
9.70 - bounds
9.71 + scope formats atomss frees free_names sel_names nonsel_names
9.72 + rel_table bounds
9.73 val genuine_means_genuine =
9.74 got_all_user_axioms andalso none_true wfs andalso
9.75 sound_finitizes andalso codatatypes_ok
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 17:36:53 2010 +0200
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 20:52:01 2010 +0200
10.3 @@ -109,20 +109,19 @@
10.4 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
10.5 val is_quot_type : theory -> typ -> bool
10.6 val is_codatatype : theory -> typ -> bool
10.7 - val is_pure_typedef : theory -> typ -> bool
10.8 - val is_univ_typedef : theory -> typ -> bool
10.9 - val is_datatype : theory -> (typ option * bool) list -> typ -> bool
10.10 + val is_pure_typedef : Proof.context -> typ -> bool
10.11 + val is_univ_typedef : Proof.context -> typ -> bool
10.12 + val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
10.13 val is_record_constr : styp -> bool
10.14 val is_record_get : theory -> styp -> bool
10.15 val is_record_update : theory -> styp -> bool
10.16 - val is_abs_fun : theory -> styp -> bool
10.17 - val is_rep_fun : theory -> styp -> bool
10.18 + val is_abs_fun : Proof.context -> styp -> bool
10.19 + val is_rep_fun : Proof.context -> styp -> bool
10.20 val is_quot_abs_fun : Proof.context -> styp -> bool
10.21 val is_quot_rep_fun : Proof.context -> styp -> bool
10.22 - val mate_of_rep_fun : theory -> styp -> styp
10.23 - val is_constr_like : theory -> styp -> bool
10.24 - val is_stale_constr : theory -> styp -> bool
10.25 - val is_constr : theory -> (typ option * bool) list -> styp -> bool
10.26 + val mate_of_rep_fun : Proof.context -> styp -> styp
10.27 + val is_constr_like : Proof.context -> styp -> bool
10.28 + val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
10.29 val is_sel : string -> bool
10.30 val is_sel_like_and_no_discr : string -> bool
10.31 val box_type : hol_context -> boxability -> typ -> typ
10.32 @@ -151,9 +150,10 @@
10.33 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
10.34 val discriminate_value : hol_context -> styp -> term -> term
10.35 val select_nth_constr_arg :
10.36 - theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
10.37 + Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
10.38 + -> term
10.39 val construct_value :
10.40 - theory -> (typ option * bool) list -> styp -> term list -> term
10.41 + Proof.context -> (typ option * bool) list -> styp -> term list -> term
10.42 val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
10.43 val card_of_type : (typ * int) list -> typ -> int
10.44 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
10.45 @@ -165,7 +165,7 @@
10.46 val abs_var : indexname * typ -> term -> term
10.47 val is_funky_typedef : theory -> typ -> bool
10.48 val all_axioms_of :
10.49 - theory -> (term * term) list -> term list * term list * term list
10.50 + Proof.context -> (term * term) list -> term list * term list * term list
10.51 val arity_of_built_in_const :
10.52 theory -> (typ option * bool) list -> bool -> styp -> int option
10.53 val is_built_in_const :
10.54 @@ -186,8 +186,8 @@
10.55 val ground_theorem_table : theory -> term list Inttab.table
10.56 val ersatz_table : theory -> (string * string) list
10.57 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
10.58 - val inverse_axioms_for_rep_fun : theory -> styp -> term list
10.59 - val optimized_typedef_axioms : theory -> string * typ list -> term list
10.60 + val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
10.61 + val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
10.62 val optimized_quot_type_axioms :
10.63 Proof.context -> (typ option * bool) list -> string * typ list -> term list
10.64 val def_of_const : theory -> const_table -> styp -> term option
10.65 @@ -196,8 +196,8 @@
10.66 theory -> const_table -> string * typ -> fixpoint_kind
10.67 val is_inductive_pred : hol_context -> styp -> bool
10.68 val is_equational_fun : hol_context -> styp -> bool
10.69 - val is_constr_pattern_lhs : theory -> term -> bool
10.70 - val is_constr_pattern_formula : theory -> term -> bool
10.71 + val is_constr_pattern_lhs : Proof.context -> term -> bool
10.72 + val is_constr_pattern_formula : Proof.context -> term -> bool
10.73 val nondef_props_for_const :
10.74 theory -> bool -> const_table -> styp -> term list
10.75 val is_choice_spec_fun : hol_context -> styp -> bool
10.76 @@ -524,22 +524,25 @@
10.77 set_def: thm option, prop_of_Rep: thm, set_name: string,
10.78 Abs_inverse: thm option, Rep_inverse: thm option}
10.79
10.80 -fun typedef_info thy s =
10.81 - if is_frac_type thy (Type (s, [])) then
10.82 - SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
10.83 - Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
10.84 - set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
10.85 - |> Logic.varify_global,
10.86 - set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
10.87 - else case Typedef.get_info_global thy s of
10.88 - (* FIXME handle multiple typedef interpretations (!??) *)
10.89 - [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
10.90 - Rep_inverse, ...})] =>
10.91 - SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
10.92 - Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
10.93 - set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
10.94 - Rep_inverse = SOME Rep_inverse}
10.95 - | _ => NONE
10.96 +fun typedef_info ctxt s =
10.97 + let val thy = ProofContext.theory_of ctxt in
10.98 + if is_frac_type thy (Type (s, [])) then
10.99 + SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
10.100 + Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
10.101 + set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
10.102 + |> Logic.varify_global,
10.103 + set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
10.104 + else case Typedef.get_info ctxt s of
10.105 + (* When several entries are returned, it shouldn't matter much which one
10.106 + we take (according to Florian Haftmann). *)
10.107 + ({abs_type, rep_type, Abs_name, Rep_name, ...},
10.108 + {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
10.109 + SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
10.110 + Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
10.111 + set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
10.112 + Rep_inverse = SOME Rep_inverse}
10.113 + | _ => NONE
10.114 + end
10.115
10.116 val is_typedef = is_some oo typedef_info
10.117 val is_real_datatype = is_some oo Datatype.get_info
10.118 @@ -594,14 +597,16 @@
10.119 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
10.120 |> Option.map snd |> these))
10.121 | is_codatatype _ _ = false
10.122 -fun is_pure_typedef thy (T as Type (s, _)) =
10.123 - is_typedef thy s andalso
10.124 - not (is_real_datatype thy s orelse is_quot_type thy T orelse
10.125 - is_codatatype thy T orelse is_record_type T orelse
10.126 - is_integer_like_type T)
10.127 +fun is_pure_typedef ctxt (T as Type (s, _)) =
10.128 + let val thy = ProofContext.theory_of ctxt in
10.129 + is_typedef ctxt s andalso
10.130 + not (is_real_datatype thy s orelse is_quot_type thy T orelse
10.131 + is_codatatype thy T orelse is_record_type T orelse
10.132 + is_integer_like_type T)
10.133 + end
10.134 | is_pure_typedef _ _ = false
10.135 -fun is_univ_typedef thy (Type (s, _)) =
10.136 - (case typedef_info thy s of
10.137 +fun is_univ_typedef ctxt (Type (s, _)) =
10.138 + (case typedef_info ctxt s of
10.139 SOME {set_def, prop_of_Rep, ...} =>
10.140 let
10.141 val t_opt =
10.142 @@ -623,9 +628,11 @@
10.143 end
10.144 | NONE => false)
10.145 | is_univ_typedef _ _ = false
10.146 -fun is_datatype thy stds (T as Type (s, _)) =
10.147 - (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
10.148 - is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
10.149 +fun is_datatype ctxt stds (T as Type (s, _)) =
10.150 + let val thy = ProofContext.theory_of ctxt in
10.151 + (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
10.152 + is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
10.153 + end
10.154 | is_datatype _ _ _ = false
10.155
10.156 fun all_record_fields thy T =
10.157 @@ -651,13 +658,13 @@
10.158 exists (curry (op =) (unsuffix Record.updateN s) o fst)
10.159 (all_record_fields thy (body_type T))
10.160 handle TYPE _ => false
10.161 -fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
10.162 - (case typedef_info thy s' of
10.163 +fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
10.164 + (case typedef_info ctxt s' of
10.165 SOME {Abs_name, ...} => s = Abs_name
10.166 | NONE => false)
10.167 | is_abs_fun _ _ = false
10.168 -fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
10.169 - (case typedef_info thy s' of
10.170 +fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
10.171 + (case typedef_info ctxt s' of
10.172 SOME {Rep_name, ...} => s = Rep_name
10.173 | NONE => false)
10.174 | is_rep_fun _ _ = false
10.175 @@ -672,9 +679,9 @@
10.176 = SOME (Const x))
10.177 | is_quot_rep_fun _ _ = false
10.178
10.179 -fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
10.180 - [T1 as Type (s', _), T2]))) =
10.181 - (case typedef_info thy s' of
10.182 +fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
10.183 + [T1 as Type (s', _), T2]))) =
10.184 + (case typedef_info ctxt s' of
10.185 SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
10.186 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
10.187 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
10.188 @@ -700,23 +707,30 @@
10.189 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
10.190 end
10.191 handle TYPE ("dest_Type", _, _) => false
10.192 -fun is_constr_like thy (s, T) =
10.193 +fun is_constr_like ctxt (s, T) =
10.194 member (op =) [@{const_name FinFun}, @{const_name FunBox},
10.195 @{const_name PairBox}, @{const_name Quot},
10.196 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
10.197 - let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
10.198 - Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
10.199 - (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
10.200 + let
10.201 + val thy = ProofContext.theory_of ctxt
10.202 + val (x as (_, T)) = (s, unarize_unbox_etc_type T)
10.203 + in
10.204 + is_real_constr thy x orelse is_record_constr x orelse
10.205 + (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
10.206 is_coconstr thy x
10.207 end
10.208 -fun is_stale_constr thy (x as (_, T)) =
10.209 - is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
10.210 - not (is_coconstr thy x)
10.211 -fun is_constr thy stds (x as (_, T)) =
10.212 - is_constr_like thy x andalso
10.213 - not (is_basic_datatype thy stds
10.214 +fun is_stale_constr ctxt (x as (_, T)) =
10.215 + let val thy = ProofContext.theory_of ctxt in
10.216 + is_codatatype thy (body_type T) andalso is_constr_like ctxt x andalso
10.217 + not (is_coconstr thy x)
10.218 + end
10.219 +fun is_constr ctxt stds (x as (_, T)) =
10.220 + let val thy = ProofContext.theory_of ctxt in
10.221 + is_constr_like ctxt x andalso
10.222 + not (is_basic_datatype thy stds
10.223 (fst (dest_Type (unarize_type (body_type T))))) andalso
10.224 - not (is_stale_constr thy x)
10.225 + not (is_stale_constr ctxt x)
10.226 + end
10.227 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
10.228 val is_sel_like_and_no_discr =
10.229 String.isPrefix sel_prefix orf
10.230 @@ -815,7 +829,7 @@
10.231 | eta_expand Ts (Abs (s, T, t')) n =
10.232 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
10.233 | eta_expand Ts t n =
10.234 - fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
10.235 + fold_rev (curry3 Abs ("x" ^ nat_subscript n))
10.236 (List.take (binder_types (fastype_of1 (Ts, t)), n))
10.237 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
10.238
10.239 @@ -836,20 +850,20 @@
10.240 fun zero_const T = Const (@{const_name zero_class.zero}, T)
10.241 fun suc_const T = Const (@{const_name Suc}, T --> T)
10.242
10.243 -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
10.244 +fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
10.245 (T as Type (s, Ts)) =
10.246 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
10.247 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
10.248 | _ =>
10.249 - if is_datatype thy stds T then
10.250 + if is_datatype ctxt stds T then
10.251 case Datatype.get_info thy s of
10.252 SOME {index, descr, ...} =>
10.253 let
10.254 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
10.255 in
10.256 - map (fn (s', Us) =>
10.257 - (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
10.258 - ---> T)) constrs
10.259 + map (apsnd (fn Us =>
10.260 + map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
10.261 + constrs
10.262 end
10.263 | NONE =>
10.264 if is_record_type T then
10.265 @@ -860,7 +874,7 @@
10.266 in [(s', T')] end
10.267 else if is_quot_type thy T then
10.268 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
10.269 - else case typedef_info thy s of
10.270 + else case typedef_info ctxt s of
10.271 SOME {abs_type, rep_type, Abs_name, ...} =>
10.272 [(Abs_name,
10.273 varify_and_instantiate_type thy abs_type T rep_type --> T)]
10.274 @@ -905,11 +919,11 @@
10.275 else
10.276 Abs (Name.uu, dataT, @{const True})
10.277 end
10.278 -fun discriminate_value (hol_ctxt as {thy, ...}) x t =
10.279 +fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
10.280 case head_of t of
10.281 Const x' =>
10.282 if x = x' then @{const True}
10.283 - else if is_constr_like thy x' then @{const False}
10.284 + else if is_constr_like ctxt x' then @{const False}
10.285 else betapply (discr_term_for_constr hol_ctxt x, t)
10.286 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
10.287
10.288 @@ -933,24 +947,26 @@
10.289 (List.take (arg_Ts, n)) 0
10.290 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
10.291 end
10.292 -fun select_nth_constr_arg thy stds x t n res_T =
10.293 - (case strip_comb t of
10.294 - (Const x', args) =>
10.295 - if x = x' then nth args n
10.296 - else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
10.297 - else raise SAME ()
10.298 - | _ => raise SAME())
10.299 - handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
10.300 +fun select_nth_constr_arg ctxt stds x t n res_T =
10.301 + let val thy = ProofContext.theory_of ctxt in
10.302 + (case strip_comb t of
10.303 + (Const x', args) =>
10.304 + if x = x' then nth args n
10.305 + else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
10.306 + else raise SAME ()
10.307 + | _ => raise SAME())
10.308 + handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
10.309 + end
10.310
10.311 fun construct_value _ _ x [] = Const x
10.312 - | construct_value thy stds (x as (s, _)) args =
10.313 + | construct_value ctxt stds (x as (s, _)) args =
10.314 let val args = map Envir.eta_contract args in
10.315 case hd args of
10.316 Const (s', _) $ t =>
10.317 if is_sel_like_and_no_discr s' andalso
10.318 constr_name_for_sel_like s' = s andalso
10.319 forall (fn (n, t') =>
10.320 - select_nth_constr_arg thy stds x t n dummyT = t')
10.321 + select_nth_constr_arg ctxt stds x t n dummyT = t')
10.322 (index_seq 0 (length args) ~~ args) then
10.323 t
10.324 else
10.325 @@ -958,9 +974,9 @@
10.326 | _ => list_comb (Const x, args)
10.327 end
10.328
10.329 -fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
10.330 +fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
10.331 (case head_of t of
10.332 - Const x => if is_constr_like thy x then t else raise SAME ()
10.333 + Const x => if is_constr_like ctxt x then t else raise SAME ()
10.334 | _ => raise SAME ())
10.335 handle SAME () =>
10.336 let
10.337 @@ -973,7 +989,7 @@
10.338 datatype_constrs hol_ctxt T |> hd
10.339 val arg_Ts = binder_types T'
10.340 in
10.341 - list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
10.342 + list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
10.343 (index_seq 0 (length arg_Ts)) arg_Ts)
10.344 end
10.345
10.346 @@ -985,7 +1001,7 @@
10.347 | _ => t
10.348 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
10.349 old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
10.350 -and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
10.351 +and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
10.352 if old_T = new_T then
10.353 t
10.354 else
10.355 @@ -999,7 +1015,7 @@
10.356 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
10.357 |> Envir.eta_contract
10.358 |> new_s <> @{type_name fun}
10.359 - ? construct_value thy stds
10.360 + ? construct_value ctxt stds
10.361 (if new_s = @{type_name fin_fun} then @{const_name FinFun}
10.362 else @{const_name FunBox},
10.363 Type (@{type_name fun}, new_Ts) --> new_T)
10.364 @@ -1014,12 +1030,12 @@
10.365 if new_s = @{type_name fun} then
10.366 coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
10.367 else
10.368 - construct_value thy stds
10.369 + construct_value ctxt stds
10.370 (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
10.371 [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
10.372 (Type (@{type_name fun}, old_Ts)) t1]
10.373 | Const _ $ t1 $ t2 =>
10.374 - construct_value thy stds
10.375 + construct_value ctxt stds
10.376 (if new_s = @{type_name "*"} then @{const_name Pair}
10.377 else @{const_name PairBox}, new_Ts ---> new_T)
10.378 (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
10.379 @@ -1145,13 +1161,15 @@
10.380 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
10.381 $ Const (@{const_name TYPE}, _)) = true
10.382 | is_arity_type_axiom _ = false
10.383 -fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
10.384 - is_typedef_axiom thy boring t2
10.385 - | is_typedef_axiom thy boring
10.386 +fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
10.387 + is_typedef_axiom ctxt boring t2
10.388 + | is_typedef_axiom ctxt boring
10.389 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
10.390 $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
10.391 $ Const _ $ _)) =
10.392 - boring <> is_funky_typedef_name thy s andalso is_typedef thy s
10.393 + let val thy = ProofContext.theory_of ctxt in
10.394 + boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s
10.395 + end
10.396 | is_typedef_axiom _ _ _ = false
10.397 val is_class_axiom =
10.398 Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
10.399 @@ -1160,13 +1178,13 @@
10.400 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
10.401 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
10.402 using "typedef_info". *)
10.403 -fun partition_axioms_by_definitionality thy axioms def_names =
10.404 +fun partition_axioms_by_definitionality ctxt axioms def_names =
10.405 let
10.406 val axioms = sort (fast_string_ord o pairself fst) axioms
10.407 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
10.408 val nondefs =
10.409 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
10.410 - |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
10.411 + |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
10.412 in pairself (map snd) (defs, nondefs) end
10.413
10.414 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
10.415 @@ -1189,8 +1207,9 @@
10.416 | do_eq _ = false
10.417 in do_eq end
10.418
10.419 -fun all_axioms_of thy subst =
10.420 +fun all_axioms_of ctxt subst =
10.421 let
10.422 + val thy = ProofContext.theory_of ctxt
10.423 val axioms_of_thys =
10.424 maps Thm.axioms_of
10.425 #> map (apsnd (subst_atomic subst o prop_of))
10.426 @@ -1203,12 +1222,12 @@
10.427 val built_in_axioms = axioms_of_thys built_in_thys
10.428 val user_axioms = axioms_of_thys user_thys
10.429 val (built_in_defs, built_in_nondefs) =
10.430 - partition_axioms_by_definitionality thy built_in_axioms def_names
10.431 - ||> filter (is_typedef_axiom thy false)
10.432 + partition_axioms_by_definitionality ctxt built_in_axioms def_names
10.433 + ||> filter (is_typedef_axiom ctxt false)
10.434 val (user_defs, user_nondefs) =
10.435 - partition_axioms_by_definitionality thy user_axioms def_names
10.436 + partition_axioms_by_definitionality ctxt user_axioms def_names
10.437 val (built_in_nondefs, user_nondefs) =
10.438 - List.partition (is_typedef_axiom thy false) user_nondefs
10.439 + List.partition (is_typedef_axiom ctxt false) user_nondefs
10.440 |>> append built_in_nondefs
10.441 val defs =
10.442 (thy |> PureThy.all_thms_of
10.443 @@ -1369,16 +1388,16 @@
10.444 | _ => NONE
10.445 fun is_constr_pattern _ (Bound _) = true
10.446 | is_constr_pattern _ (Var _) = true
10.447 - | is_constr_pattern thy t =
10.448 + | is_constr_pattern ctxt t =
10.449 case strip_comb t of
10.450 (Const x, args) =>
10.451 - is_constr_like thy x andalso forall (is_constr_pattern thy) args
10.452 + is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
10.453 | _ => false
10.454 -fun is_constr_pattern_lhs thy t =
10.455 - forall (is_constr_pattern thy) (snd (strip_comb t))
10.456 -fun is_constr_pattern_formula thy t =
10.457 +fun is_constr_pattern_lhs ctxt t =
10.458 + forall (is_constr_pattern ctxt) (snd (strip_comb t))
10.459 +fun is_constr_pattern_formula ctxt t =
10.460 case lhs_of_equation t of
10.461 - SOME t' => is_constr_pattern_lhs thy t'
10.462 + SOME t' => is_constr_pattern_lhs ctxt t'
10.463 | NONE => false
10.464
10.465 (* Similar to "specialize_type" but returns all matches rather than only the
10.466 @@ -1397,8 +1416,10 @@
10.467 if slack then
10.468 I
10.469 else
10.470 - raise NOT_SUPPORTED ("too much polymorphism in \
10.471 - \axiom involving " ^ quote s))
10.472 + raise NOT_SUPPORTED
10.473 + ("too much polymorphism in axiom \"" ^
10.474 + Syntax.string_of_term_global thy t ^
10.475 + "\" involving " ^ quote s))
10.476 else
10.477 ys
10.478 | aux _ ys = ys
10.479 @@ -1437,26 +1458,26 @@
10.480
10.481 (** Constant unfolding **)
10.482
10.483 -fun constr_case_body thy stds (j, (x as (_, T))) =
10.484 +fun constr_case_body ctxt stds (j, (x as (_, T))) =
10.485 let val arg_Ts = binder_types T in
10.486 - list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
10.487 + list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
10.488 (index_seq 0 (length arg_Ts)) arg_Ts)
10.489 end
10.490 -fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
10.491 +fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
10.492 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
10.493 - $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
10.494 + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
10.495 $ res_t
10.496 -fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
10.497 +fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
10.498 let
10.499 val xs = datatype_constrs hol_ctxt dataT
10.500 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
10.501 val (xs', x) = split_last xs
10.502 in
10.503 - constr_case_body thy stds (1, x)
10.504 + constr_case_body ctxt stds (1, x)
10.505 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
10.506 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
10.507 end
10.508 -fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
10.509 +fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
10.510 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
10.511 case no_of_record_field thy s rec_T of
10.512 ~1 => (case rec_T of
10.513 @@ -1465,14 +1486,15 @@
10.514 val rec_T' = List.last Ts
10.515 val j = num_record_fields thy rec_T - 1
10.516 in
10.517 - select_nth_constr_arg thy stds constr_x t j res_T
10.518 + select_nth_constr_arg ctxt stds constr_x t j res_T
10.519 |> optimized_record_get hol_ctxt s rec_T' res_T
10.520 end
10.521 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
10.522 []))
10.523 - | j => select_nth_constr_arg thy stds constr_x t j res_T
10.524 + | j => select_nth_constr_arg ctxt stds constr_x t j res_T
10.525 end
10.526 -fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
10.527 +fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
10.528 + rec_t =
10.529 let
10.530 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
10.531 val Ts = binder_types constr_T
10.532 @@ -1480,7 +1502,7 @@
10.533 val special_j = no_of_record_field thy s rec_T
10.534 val ts =
10.535 map2 (fn j => fn T =>
10.536 - let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
10.537 + let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
10.538 if j = special_j then
10.539 betapply (fun_t, t)
10.540 else if j = n - 1 andalso special_j = ~1 then
10.541 @@ -1549,9 +1571,9 @@
10.542 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
10.543 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
10.544 (Abs (Name.uu, body_type T,
10.545 - select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
10.546 + select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
10.547 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
10.548 - (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
10.549 + (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
10.550 and do_const depth Ts t (x as (s, T)) ts =
10.551 case AList.lookup (op =) ersatz_table s of
10.552 SOME s' =>
10.553 @@ -1571,9 +1593,9 @@
10.554 |> do_term (depth + 1) Ts, ts)
10.555 end
10.556 | _ =>
10.557 - if is_constr thy stds x then
10.558 + if is_constr ctxt stds x then
10.559 (Const x, ts)
10.560 - else if is_stale_constr thy x then
10.561 + else if is_stale_constr ctxt x then
10.562 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
10.563 \(\"" ^ s ^ "\")")
10.564 else if is_quot_abs_fun ctxt x then
10.565 @@ -1604,9 +1626,9 @@
10.566 (do_term depth Ts (hd ts))
10.567 (do_term depth Ts (nth ts 1)), [])
10.568 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
10.569 - else if is_rep_fun thy x then
10.570 - let val x' = mate_of_rep_fun thy x in
10.571 - if is_constr thy stds x' then
10.572 + else if is_rep_fun ctxt x then
10.573 + let val x' = mate_of_rep_fun ctxt x in
10.574 + if is_constr ctxt stds x' then
10.575 select_nth_constr_arg_with_args depth Ts x' ts 0
10.576 (range_type T)
10.577 else
10.578 @@ -1652,10 +1674,14 @@
10.579 map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
10.580 |> const_nondef_table
10.581 fun inductive_intro_table ctxt subst def_table =
10.582 - def_table_for
10.583 - (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
10.584 - def_table o prop_of)
10.585 - o Nitpick_Intros.get) ctxt subst
10.586 + let val thy = ProofContext.theory_of ctxt in
10.587 + def_table_for
10.588 + (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
10.589 + o snd o snd)
10.590 + o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
10.591 + cat = Spec_Rules.Co_Inductive)
10.592 + o Spec_Rules.get) ctxt subst
10.593 + end
10.594 fun ground_theorem_table thy =
10.595 fold ((fn @{const Trueprop} $ t1 =>
10.596 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
10.597 @@ -1677,18 +1703,24 @@
10.598 Unsynchronized.change simp_table
10.599 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
10.600
10.601 -fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
10.602 - let val abs_T = domain_type T in
10.603 - typedef_info thy (fst (dest_Type abs_T)) |> the
10.604 +fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
10.605 + let
10.606 + val thy = ProofContext.theory_of ctxt
10.607 + val abs_T = domain_type T
10.608 + in
10.609 + typedef_info ctxt (fst (dest_Type abs_T)) |> the
10.610 |> pairf #Abs_inverse #Rep_inverse
10.611 |> pairself (specialize_type thy x o prop_of o the)
10.612 ||> single |> op ::
10.613 end
10.614 -fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
10.615 - let val abs_T = Type abs_z in
10.616 - if is_univ_typedef thy abs_T then
10.617 +fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
10.618 + let
10.619 + val thy = ProofContext.theory_of ctxt
10.620 + val abs_T = Type abs_z
10.621 + in
10.622 + if is_univ_typedef ctxt abs_T then
10.623 []
10.624 - else case typedef_info thy abs_s of
10.625 + else case typedef_info ctxt abs_s of
10.626 SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
10.627 let
10.628 val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
10.629 @@ -1716,7 +1748,7 @@
10.630 val x_var = Var (("x", 0), rep_T)
10.631 val y_var = Var (("y", 0), rep_T)
10.632 val x = (@{const_name Quot}, rep_T --> abs_T)
10.633 - val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
10.634 + val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
10.635 val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
10.636 val normal_x = normal_t $ x_var
10.637 val normal_y = normal_t $ y_var
10.638 @@ -1734,7 +1766,7 @@
10.639 HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
10.640 end
10.641
10.642 -fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
10.643 +fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T =
10.644 let
10.645 val xs = datatype_constrs hol_ctxt T
10.646 val set_T = T --> bool_T
10.647 @@ -1751,8 +1783,8 @@
10.648 fun nth_sub_bisim x n nth_T =
10.649 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
10.650 else HOLogic.eq_const nth_T)
10.651 - $ select_nth_constr_arg thy stds x x_var n nth_T
10.652 - $ select_nth_constr_arg thy stds x y_var n nth_T
10.653 + $ select_nth_constr_arg ctxt stds x x_var n nth_T
10.654 + $ select_nth_constr_arg ctxt stds x y_var n nth_T
10.655 fun case_func (x as (_, T)) =
10.656 let
10.657 val arg_Ts = binder_types T
10.658 @@ -1785,20 +1817,18 @@
10.659 end
10.660
10.661 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
10.662 -
10.663 fun wf_constraint_for rel side concl main =
10.664 let
10.665 - val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
10.666 - tuple_for_args concl), Var rel)
10.667 + val core = HOLogic.mk_mem (HOLogic.mk_prod
10.668 + (pairself tuple_for_args (main, concl)), Var rel)
10.669 val t = List.foldl HOLogic.mk_imp core side
10.670 - val vars = filter (not_equal rel) (Term.add_vars t [])
10.671 + val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
10.672 in
10.673 Library.foldl (fn (t', ((x, j), T)) =>
10.674 HOLogic.all_const T
10.675 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
10.676 (t, vars)
10.677 end
10.678 -
10.679 fun wf_constraint_for_triple rel (side, main, concl) =
10.680 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
10.681
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Jun 01 17:36:53 2010 +0200
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Jun 01 20:52:01 2010 +0200
11.3 @@ -65,6 +65,7 @@
11.4 ("show_datatypes", "false"),
11.5 ("show_consts", "false"),
11.6 ("format", "1"),
11.7 + ("atoms", ""),
11.8 ("max_potential", "1"),
11.9 ("max_genuine", "1"),
11.10 ("check_potential", "false"),
11.11 @@ -98,10 +99,11 @@
11.12 fun is_known_raw_param s =
11.13 AList.defined (op =) default_default_params s orelse
11.14 AList.defined (op =) negated_params s orelse
11.15 - s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
11.16 + member (op =) ["max", "show_all", "eval", "expect"] s orelse
11.17 exists (fn p => String.isPrefix (p ^ " ") s)
11.18 ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
11.19 - "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
11.20 + "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
11.21 + "atoms"]
11.22
11.23 fun check_raw_param (s, _) =
11.24 if is_known_raw_param s then ()
11.25 @@ -149,8 +151,8 @@
11.26 let
11.27 val override_params = maps normalize_raw_param override_params
11.28 val raw_params = rev override_params @ rev default_params
11.29 - val lookup =
11.30 - Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
11.31 + val raw_lookup = AList.lookup (op =) raw_params
11.32 + val lookup = Option.map stringify_raw_param_value o raw_lookup
11.33 val lookup_string = the_default "" o lookup
11.34 fun general_lookup_bool option default_value name =
11.35 case lookup name of
11.36 @@ -191,27 +193,21 @@
11.37 [] => [min_int]
11.38 | value => value)
11.39 | NONE => [min_int]
11.40 - fun lookup_ints_assigns read prefix min_int =
11.41 - (NONE, lookup_int_seq prefix min_int)
11.42 + fun lookup_assigns read prefix default convert =
11.43 + (NONE, convert (the_default default (lookup prefix)))
11.44 :: map (fn (name, value) =>
11.45 (SOME (read (String.extract (name, size prefix + 1, NONE))),
11.46 - value |> stringify_raw_param_value
11.47 - |> int_seq_from_string name min_int))
11.48 + convert (stringify_raw_param_value value)))
11.49 (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
11.50 + fun lookup_ints_assigns read prefix min_int =
11.51 + lookup_assigns read prefix (signed_string_of_int min_int)
11.52 + (int_seq_from_string prefix min_int)
11.53 fun lookup_bool_assigns read prefix =
11.54 - (NONE, lookup_bool prefix)
11.55 - :: map (fn (name, value) =>
11.56 - (SOME (read (String.extract (name, size prefix + 1, NONE))),
11.57 - value |> stringify_raw_param_value
11.58 - |> parse_bool_option false name |> the))
11.59 - (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
11.60 + lookup_assigns read prefix "" (the o parse_bool_option false prefix)
11.61 fun lookup_bool_option_assigns read prefix =
11.62 - (NONE, lookup_bool_option prefix)
11.63 - :: map (fn (name, value) =>
11.64 - (SOME (read (String.extract (name, size prefix + 1, NONE))),
11.65 - value |> stringify_raw_param_value
11.66 - |> parse_bool_option true name))
11.67 - (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
11.68 + lookup_assigns read prefix "" (parse_bool_option true prefix)
11.69 + fun lookup_strings_assigns read prefix =
11.70 + lookup_assigns read prefix "" (space_explode " ")
11.71 fun lookup_time name =
11.72 case lookup name of
11.73 NONE => NONE
11.74 @@ -255,6 +251,7 @@
11.75 val show_datatypes = debug orelse lookup_bool "show_datatypes"
11.76 val show_consts = debug orelse lookup_bool "show_consts"
11.77 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
11.78 + val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
11.79 val evals = lookup_term_list "eval"
11.80 val max_potential =
11.81 if auto then 0 else Int.max (0, lookup_int "max_potential")
11.82 @@ -279,9 +276,10 @@
11.83 peephole_optim = peephole_optim, timeout = timeout,
11.84 tac_timeout = tac_timeout, max_threads = max_threads,
11.85 show_datatypes = show_datatypes, show_consts = show_consts,
11.86 - formats = formats, evals = evals, max_potential = max_potential,
11.87 - max_genuine = max_genuine, check_potential = check_potential,
11.88 - check_genuine = check_genuine, batch_size = batch_size, expect = expect}
11.89 + formats = formats, atomss = atomss, evals = evals,
11.90 + max_potential = max_potential, max_genuine = max_genuine,
11.91 + check_potential = check_potential, check_genuine = check_genuine,
11.92 + batch_size = batch_size, expect = expect}
11.93 end
11.94
11.95 fun default_params thy =
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 17:36:53 2010 +0200
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 20:52:01 2010 +0200
12.3 @@ -23,7 +23,7 @@
12.4
12.5 val irrelevant : string
12.6 val unknown : string
12.7 - val unrep : string
12.8 + val unrep : unit -> string
12.9 val register_term_postprocessor :
12.10 typ -> term_postprocessor -> theory -> theory
12.11 val unregister_term_postprocessor : typ -> theory -> theory
12.12 @@ -31,8 +31,9 @@
12.13 nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
12.14 val dest_plain_fun : term -> bool * (term list * term list)
12.15 val reconstruct_hol_model :
12.16 - params -> scope -> (term option * int list) list -> styp list -> nut list
12.17 - -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
12.18 + params -> scope -> (term option * int list) list
12.19 + -> (typ option * string list) list -> styp list -> nut list -> nut list
12.20 + -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
12.21 -> Pretty.T * bool
12.22 val prove_hol_model :
12.23 scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
12.24 @@ -64,17 +65,19 @@
12.25 val extend = I
12.26 fun merge (x, y) = AList.merge (op =) (K true) (x, y))
12.27
12.28 +fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
12.29 +
12.30 val irrelevant = "_"
12.31 val unknown = "?"
12.32 -val unrep = "\<dots>"
12.33 -val maybe_mixfix = "_\<^sup>?"
12.34 -val base_mixfix = "_\<^bsub>base\<^esub>"
12.35 -val step_mixfix = "_\<^bsub>step\<^esub>"
12.36 -val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
12.37 +val unrep = xsym "\<dots>" "..."
12.38 +val maybe_mixfix = xsym "_\<^sup>?" "_?"
12.39 +val base_mixfix = xsym "_\<^bsub>base\<^esub>" "_.base"
12.40 +val step_mixfix = xsym "_\<^bsub>step\<^esub>" "_.step"
12.41 +val abs_mixfix = xsym "\<guillemotleft>_\<guillemotright>" "\"_\""
12.42 val arg_var_prefix = "x"
12.43 -val cyclic_co_val_name = "\<omega>"
12.44 -val cyclic_const_prefix = "\<xi>"
12.45 -val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
12.46 +val cyclic_co_val_name = xsym "\<omega>" "w"
12.47 +val cyclic_const_prefix = xsym "\<xi>" "X"
12.48 +fun cyclic_type_name () = nitpick_prefix ^ cyclic_const_prefix ()
12.49 val opt_flag = nitpick_prefix ^ "opt"
12.50 val non_opt_flag = nitpick_prefix ^ "non_opt"
12.51
12.52 @@ -86,16 +89,16 @@
12.53 val thy = ProofContext.theory_of ctxt |> Context.reject_draft
12.54 val (maybe_t, thy) =
12.55 Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
12.56 - Mixfix (maybe_mixfix, [1000], 1000)) thy
12.57 + Mixfix (maybe_mixfix (), [1000], 1000)) thy
12.58 val (abs_t, thy) =
12.59 Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
12.60 - Mixfix (abs_mixfix, [40], 40)) thy
12.61 + Mixfix (abs_mixfix (), [40], 40)) thy
12.62 val (base_t, thy) =
12.63 Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
12.64 - Mixfix (base_mixfix, [1000], 1000)) thy
12.65 + Mixfix (base_mixfix (), [1000], 1000)) thy
12.66 val (step_t, thy) =
12.67 Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
12.68 - Mixfix (step_mixfix, [1000], 1000)) thy
12.69 + Mixfix (step_mixfix (), [1000], 1000)) thy
12.70 in
12.71 (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
12.72 ProofContext.transfer_syntax thy ctxt)
12.73 @@ -103,31 +106,41 @@
12.74
12.75 (** Term reconstruction **)
12.76
12.77 -fun nth_atom_suffix pool s j k =
12.78 - (case AList.lookup (op =) (!pool) (s, k) of
12.79 - SOME js =>
12.80 - (case find_index (curry (op =) j) js of
12.81 - ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
12.82 - length js + 1)
12.83 - | n => length js - n)
12.84 - | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
12.85 - |> nat_subscript
12.86 - |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
12.87 +fun nth_atom_number pool T j =
12.88 + case AList.lookup (op =) (!pool) T of
12.89 + SOME js =>
12.90 + (case find_index (curry (op =) j) js of
12.91 + ~1 => (Unsynchronized.change pool (cons (T, j :: js));
12.92 + length js + 1)
12.93 + | n => length js - n)
12.94 + | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
12.95 +fun atom_suffix s =
12.96 + nat_subscript
12.97 + #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
12.98 ? prefix "\<^isub>,"
12.99 -fun nth_atom_name pool prefix (Type (s, _)) j k =
12.100 - let val s' = shortest_name s in
12.101 - prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
12.102 - nth_atom_suffix pool s j k
12.103 - end
12.104 - | nth_atom_name pool prefix (TFree (s, _)) j k =
12.105 - prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
12.106 - | nth_atom_name _ _ T _ _ =
12.107 - raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
12.108 -fun nth_atom pool for_auto T j k =
12.109 +fun nth_atom_name thy atomss pool prefix T j =
12.110 + let
12.111 + val ss = these (triple_lookup (type_match thy) atomss T)
12.112 + val m = nth_atom_number pool T j
12.113 + in
12.114 + if m <= length ss then
12.115 + nth ss (m - 1)
12.116 + else case T of
12.117 + Type (s, _) =>
12.118 + let val s' = shortest_name s in
12.119 + prefix ^
12.120 + (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
12.121 + atom_suffix s m
12.122 + end
12.123 + | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
12.124 + | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
12.125 + end
12.126 +fun nth_atom thy atomss pool for_auto T j =
12.127 if for_auto then
12.128 - Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
12.129 + Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
12.130 + T j, T)
12.131 else
12.132 - Const (nth_atom_name pool "" T j k, T)
12.133 + Const (nth_atom_name thy atomss pool "" T j, T)
12.134
12.135 fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
12.136 real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
12.137 @@ -300,27 +313,29 @@
12.138 strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
12.139
12.140 fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
12.141 - sel_names rel_table bounds card T =
12.142 + atomss sel_names rel_table bounds card T =
12.143 let
12.144 val card = if card = 0 then card_of_type card_assigns T else card
12.145 fun nth_value_of_type n =
12.146 let
12.147 fun term unfold =
12.148 - reconstruct_term unfold pool wacky_names scope sel_names rel_table
12.149 - bounds T T (Atom (card, 0)) [[n]]
12.150 + reconstruct_term true unfold pool wacky_names scope atomss sel_names
12.151 + rel_table bounds T T (Atom (card, 0)) [[n]]
12.152 in
12.153 case term false of
12.154 t as Const (s, _) =>
12.155 - if String.isPrefix cyclic_const_prefix s then
12.156 + if String.isPrefix (cyclic_const_prefix ()) s then
12.157 HOLogic.mk_eq (t, term true)
12.158 else
12.159 t
12.160 | t => t
12.161 end
12.162 in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
12.163 -and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
12.164 - (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
12.165 - bits, datatypes, ofs, ...}) sel_names rel_table bounds =
12.166 +and reconstruct_term maybe_opt unfold pool
12.167 + (wacky_names as ((maybe_name, abs_name), _))
12.168 + (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
12.169 + bits, datatypes, ofs, ...})
12.170 + atomss sel_names rel_table bounds =
12.171 let
12.172 val for_auto = (maybe_name = "")
12.173 fun value_of_bits jss =
12.174 @@ -332,7 +347,8 @@
12.175 js 0
12.176 end
12.177 val all_values =
12.178 - all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
12.179 + all_values_of_type pool wacky_names scope atomss sel_names rel_table
12.180 + bounds 0
12.181 fun postprocess_term (Type (@{type_name fun}, _)) = I
12.182 | postprocess_term T =
12.183 if null (Data.get thy) then
12.184 @@ -354,7 +370,7 @@
12.185 T1 --> (T1 --> T2) --> T1 --> T2)
12.186 fun aux [] =
12.187 if maybe_opt andalso not (is_complete_type datatypes false T1) then
12.188 - insert_const $ Const (unrep, T1) $ empty_const
12.189 + insert_const $ Const (unrep (), T1) $ empty_const
12.190 else
12.191 empty_const
12.192 | aux ((t1, t2) :: zs) =
12.193 @@ -383,7 +399,7 @@
12.194 | _ => update_const $ aux' tps $ t1 $ t2)
12.195 fun aux tps =
12.196 if maybe_opt andalso not (is_complete_type datatypes false T1) then
12.197 - update_const $ aux' tps $ Const (unrep, T1)
12.198 + update_const $ aux' tps $ Const (unrep (), T1)
12.199 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
12.200 else
12.201 aux' tps
12.202 @@ -471,16 +487,17 @@
12.203 else if T = @{typ bisim_iterator} then
12.204 HOLogic.mk_number nat_T j
12.205 else case datatype_spec datatypes T of
12.206 - NONE => nth_atom pool for_auto T j k
12.207 - | SOME {deep = false, ...} => nth_atom pool for_auto T j k
12.208 + NONE => nth_atom thy atomss pool for_auto T j
12.209 + | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
12.210 | SOME {co, standard, constrs, ...} =>
12.211 let
12.212 fun tuples_for_const (s, T) =
12.213 tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
12.214 fun cyclic_atom () =
12.215 - nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
12.216 - fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
12.217 -
12.218 + nth_atom thy atomss pool for_auto (Type (cyclic_type_name (), []))
12.219 + j
12.220 + fun cyclic_var () =
12.221 + Var ((nth_atom_name thy atomss pool "" T j, 0), T)
12.222 val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
12.223 constrs
12.224 val real_j = j + offset_of_type ofs T
12.225 @@ -536,7 +553,7 @@
12.226 | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
12.227 \term_for_atom (Abs_Frac)", ts)
12.228 else if not for_auto andalso
12.229 - (is_abs_fun thy constr_x orelse
12.230 + (is_abs_fun ctxt constr_x orelse
12.231 constr_s = @{const_name Quot}) then
12.232 Const (abs_name, constr_T) $ the_single ts
12.233 else
12.234 @@ -546,14 +563,15 @@
12.235 let val var = cyclic_var () in
12.236 if unfold andalso not standard andalso
12.237 length seen = 1 andalso
12.238 - exists_subterm (fn Const (s, _) =>
12.239 - String.isPrefix cyclic_const_prefix s
12.240 - | t' => t' = var) t then
12.241 + exists_subterm
12.242 + (fn Const (s, _) =>
12.243 + String.isPrefix (cyclic_const_prefix ()) s
12.244 + | t' => t' = var) t then
12.245 subst_atomic [(var, cyclic_atom ())] t
12.246 else if exists_subterm (curry (op =) var) t then
12.247 if co then
12.248 Const (@{const_name The}, (T --> bool_T) --> T)
12.249 - $ Abs (cyclic_co_val_name, T,
12.250 + $ Abs (cyclic_co_val_name (), T,
12.251 Const (@{const_name "op ="}, T --> T --> bool_T)
12.252 $ Bound 0 $ abstract_over (var, t))
12.253 else
12.254 @@ -612,11 +630,11 @@
12.255 else term_for_rep true seen T T' R jss
12.256 | term_for_rep _ _ T _ R jss =
12.257 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
12.258 - Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
12.259 + Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
12.260 string_of_int (length jss))
12.261 in
12.262 postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
12.263 - oooo term_for_rep true []
12.264 + oooo term_for_rep maybe_opt []
12.265 end
12.266
12.267 (** Constant postprocessing **)
12.268 @@ -801,9 +819,11 @@
12.269
12.270 fun assign_operator_for_const (s, T) =
12.271 if String.isPrefix ubfp_prefix s then
12.272 - if is_fun_type T then "\<subseteq>" else "\<le>"
12.273 + if is_fun_type T then xsym "\<subseteq>" "<=" ()
12.274 + else xsym "\<le>" "<=" ()
12.275 else if String.isPrefix lbfp_prefix s then
12.276 - if is_fun_type T then "\<supseteq>" else "\<ge>"
12.277 + if is_fun_type T then xsym "\<supseteq>" ">=" ()
12.278 + else xsym "\<ge>" ">=" ()
12.279 else if original_name s <> s then
12.280 assign_operator_for_const (strip_first_name_sep s |> snd, T)
12.281 else
12.282 @@ -811,13 +831,6 @@
12.283
12.284 (** Model reconstruction **)
12.285
12.286 -fun term_for_name pool scope sel_names rel_table bounds name =
12.287 - let val T = type_of name in
12.288 - tuple_list_for_name rel_table bounds name
12.289 - |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
12.290 - rel_table bounds T T (rep_of name)
12.291 - end
12.292 -
12.293 fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
12.294 $ Abs (s, T, Const (@{const_name "op ="}, _)
12.295 $ Bound 0 $ t')) =
12.296 @@ -848,7 +861,8 @@
12.297 ground_thm_table, ersatz_table, skolems, special_funs,
12.298 unrolled_preds, wf_cache, constr_cache},
12.299 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
12.300 - formats all_frees free_names sel_names nonsel_names rel_table bounds =
12.301 + formats atomss all_frees free_names sel_names nonsel_names rel_table
12.302 + bounds =
12.303 let
12.304 val pool = Unsynchronized.ref []
12.305 val (wacky_names as (_, base_step_names), ctxt) =
12.306 @@ -870,22 +884,24 @@
12.307 val scope =
12.308 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
12.309 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
12.310 - fun term_for_rep unfold =
12.311 - reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
12.312 + fun term_for_rep maybe_opt unfold =
12.313 + reconstruct_term maybe_opt unfold pool wacky_names scope atomss
12.314 + sel_names rel_table bounds
12.315 fun nth_value_of_type card T n =
12.316 let
12.317 - fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
12.318 + fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
12.319 in
12.320 case aux false of
12.321 t as Const (s, _) =>
12.322 - if String.isPrefix cyclic_const_prefix s then
12.323 + if String.isPrefix (cyclic_const_prefix ()) s then
12.324 HOLogic.mk_eq (t, aux true)
12.325 else
12.326 t
12.327 | t => t
12.328 end
12.329 val all_values =
12.330 - all_values_of_type pool wacky_names scope sel_names rel_table bounds
12.331 + all_values_of_type pool wacky_names scope atomss sel_names rel_table
12.332 + bounds
12.333 fun is_codatatype_wellformed (cos : dtype_spec list)
12.334 ({typ, card, ...} : dtype_spec) =
12.335 let
12.336 @@ -912,7 +928,8 @@
12.337 Const (@{const_name undefined}, T')
12.338 else
12.339 tuple_list_for_name rel_table bounds name
12.340 - |> term_for_rep false T T' (rep_of name)
12.341 + |> term_for_rep (not (is_fully_representable_set name)) false
12.342 + T T' (rep_of name)
12.343 in
12.344 Pretty.block (Pretty.breaks
12.345 [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
12.346 @@ -930,7 +947,7 @@
12.347 Pretty.enum "," "{" "}"
12.348 (map (Syntax.pretty_term ctxt) (all_values card typ) @
12.349 (if fun_from_pair complete false then []
12.350 - else [Pretty.str unrep]))]))
12.351 + else [Pretty.str (unrep ())]))]))
12.352 fun integer_datatype T =
12.353 [{typ = T, card = card_of_type card_assigns T, co = false,
12.354 standard = true, complete = (false, false), concrete = (true, true),
12.355 @@ -991,14 +1008,23 @@
12.356 forall (is_codatatype_wellformed codatatypes) codatatypes)
12.357 end
12.358
12.359 +fun term_for_name pool scope atomss sel_names rel_table bounds name =
12.360 + let val T = type_of name in
12.361 + tuple_list_for_name rel_table bounds name
12.362 + |> reconstruct_term (not (is_fully_representable_set name)) false pool
12.363 + (("", ""), ("", "")) scope atomss sel_names rel_table
12.364 + bounds T T (rep_of name)
12.365 + end
12.366 +
12.367 fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
12.368 card_assigns, ...})
12.369 auto_timeout free_names sel_names rel_table bounds prop =
12.370 let
12.371 val pool = Unsynchronized.ref []
12.372 + val atomss = [(NONE, [])]
12.373 fun free_type_assm (T, k) =
12.374 let
12.375 - fun atom j = nth_atom pool true T j k
12.376 + fun atom j = nth_atom thy atomss pool true T j
12.377 fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
12.378 val eqs = map equation_for_atom (index_seq 0 k)
12.379 val compreh_assm =
12.380 @@ -1008,7 +1034,8 @@
12.381 in s_conj (compreh_assm, distinct_assm) end
12.382 fun free_name_assm name =
12.383 HOLogic.mk_eq (Free (nickname_of name, type_of name),
12.384 - term_for_name pool scope sel_names rel_table bounds name)
12.385 + term_for_name pool scope atomss sel_names rel_table bounds
12.386 + name)
12.387 val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
12.388 val model_assms = map free_name_assm free_names
12.389 val assm = foldr1 s_conj (freeT_assms @ model_assms)
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 17:36:53 2010 +0200
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 20:52:01 2010 +0200
13.3 @@ -162,8 +162,8 @@
13.4 | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
13.5 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
13.6 could_exist_alpha_subtype alpha_T T
13.7 - | could_exist_alpha_sub_mtype thy alpha_T T =
13.8 - (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
13.9 + | could_exist_alpha_sub_mtype ctxt alpha_T T =
13.10 + (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
13.11
13.12 fun exists_alpha_sub_mtype MAlpha = true
13.13 | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
13.14 @@ -243,7 +243,7 @@
13.15 else
13.16 S Minus
13.17 in (M1, a, M2) end
13.18 -and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
13.19 +and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
13.20 datatype_mcache, constr_mcache, ...})
13.21 all_minus =
13.22 let
13.23 @@ -255,7 +255,7 @@
13.24 MFun (fresh_mfun_for_fun_type mdata false T1 T2)
13.25 | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
13.26 | Type (z as (s, _)) =>
13.27 - if could_exist_alpha_sub_mtype thy alpha_T T then
13.28 + if could_exist_alpha_sub_mtype ctxt alpha_T T then
13.29 case AList.lookup (op =) (!datatype_mcache) z of
13.30 SOME M => M
13.31 | NONE =>
13.32 @@ -290,7 +290,7 @@
13.33 end
13.34 else
13.35 MType (s, [])
13.36 - | _ => MType (Refute.string_of_typ T, [])
13.37 + | _ => MType (simple_string_of_typ T, [])
13.38 in do_type end
13.39
13.40 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
13.41 @@ -304,9 +304,9 @@
13.42 case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
13.43 end
13.44
13.45 -fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
13.46 +fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
13.47 ...}) (x as (_, T)) =
13.48 - if could_exist_alpha_sub_mtype thy alpha_T T then
13.49 + if could_exist_alpha_sub_mtype ctxt alpha_T T then
13.50 case AList.lookup (op =) (!constr_mcache) x of
13.51 SOME M => M
13.52 | NONE => if T = alpha_T then
13.53 @@ -741,7 +741,7 @@
13.54 do_robust_set_operation T accum
13.55 else if is_sel s then
13.56 (mtype_for_sel mdata x, accum)
13.57 - else if is_constr thy stds x then
13.58 + else if is_constr ctxt stds x then
13.59 (mtype_for_constr mdata x, accum)
13.60 else if is_built_in_const thy stds fast_descrs x then
13.61 (fresh_mtype_for_type mdata true T, accum)
13.62 @@ -924,8 +924,8 @@
13.63 if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
13.64 else consider_general_formula mdata Plus t
13.65
13.66 -fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
13.67 - if not (is_constr_pattern_formula thy t) then
13.68 +fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
13.69 + if not (is_constr_pattern_formula ctxt t) then
13.70 consider_nondefinitional_axiom mdata t
13.71 else if is_harmless_axiom mdata t then
13.72 pair (MRaw (t, dummy_M))
13.73 @@ -1027,7 +1027,8 @@
13.74 fun fin_fun_constr T1 T2 =
13.75 (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
13.76
13.77 -fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
13.78 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
13.79 + ...})
13.80 binarize finitizes alpha_T tsp =
13.81 case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
13.82 SOME (lits, msp, constr_mtypes) =>
13.83 @@ -1054,11 +1055,11 @@
13.84 (s, case AList.lookup (op =) constr_mtypes x of
13.85 SOME M => type_from_mtype T M
13.86 | NONE => T)
13.87 - fun term_from_mterm Ts m =
13.88 + fun term_from_mterm new_Ts old_Ts m =
13.89 case m of
13.90 MRaw (t, M) =>
13.91 let
13.92 - val T = fastype_of1 (Ts, t)
13.93 + val T = fastype_of1 (old_Ts, t)
13.94 val T' = type_from_mtype T M
13.95 in
13.96 case t of
13.97 @@ -1072,7 +1073,7 @@
13.98 $ (Const (@{const_name is_unknown},
13.99 elem_T' --> bool_T) $ Bound 1)
13.100 $ (Const (@{const_name unknown}, set_T'))
13.101 - $ (coerce_term hol_ctxt Ts T' T (Const x)
13.102 + $ (coerce_term hol_ctxt new_Ts T' T (Const x)
13.103 $ Bound 1 $ Bound 0)))
13.104 | _ => Const (s, T')
13.105 else if s = @{const_name finite} then
13.106 @@ -1084,8 +1085,8 @@
13.107 s = @{const_name "op ="} then
13.108 Const (s, T')
13.109 else if is_built_in_const thy stds fast_descrs x then
13.110 - coerce_term hol_ctxt Ts T' T t
13.111 - else if is_constr thy stds x then
13.112 + coerce_term hol_ctxt new_Ts T' T t
13.113 + else if is_constr ctxt stds x then
13.114 Const (finitize_constr x)
13.115 else if is_sel s then
13.116 let
13.117 @@ -1106,32 +1107,32 @@
13.118 end
13.119 | MApp (m1, m2) =>
13.120 let
13.121 - val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
13.122 - val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
13.123 + val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
13.124 + val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
13.125 val (t1', T2') =
13.126 case T1 of
13.127 Type (s, [T11, T12]) =>
13.128 (if s = @{type_name fin_fun} then
13.129 - select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
13.130 + select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
13.131 0 (T11 --> T12)
13.132 else
13.133 t1, T11)
13.134 | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
13.135 [T1], [])
13.136 - in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
13.137 - | MAbs (s, T, M, a, m') =>
13.138 + in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
13.139 + | MAbs (s, old_T, M, a, m') =>
13.140 let
13.141 - val T = type_from_mtype T M
13.142 - val t' = term_from_mterm (T :: Ts) m'
13.143 - val T' = fastype_of1 (T :: Ts, t')
13.144 + val new_T = type_from_mtype old_T M
13.145 + val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
13.146 + val T' = fastype_of1 (new_T :: new_Ts, t')
13.147 in
13.148 - Abs (s, T, t')
13.149 - |> should_finitize (T --> T') a
13.150 - ? construct_value thy stds (fin_fun_constr T T') o single
13.151 + Abs (s, new_T, t')
13.152 + |> should_finitize (new_T --> T') a
13.153 + ? construct_value ctxt stds (fin_fun_constr new_T T') o single
13.154 end
13.155 in
13.156 Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
13.157 - pairself (map (term_from_mterm [])) msp
13.158 + pairself (map (term_from_mterm [] [])) msp
13.159 end
13.160 | NONE => tsp
13.161
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 17:36:53 2010 +0200
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 20:52:01 2010 +0200
14.3 @@ -105,6 +105,7 @@
14.4 val the_name : 'a NameTable.table -> nut -> 'a
14.5 val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
14.6 val nut_from_term : hol_context -> op2 -> term -> nut
14.7 + val is_fully_representable_set : nut -> bool
14.8 val choose_reps_for_free_vars :
14.9 scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
14.10 val choose_reps_for_consts :
14.11 @@ -439,7 +440,7 @@
14.12 maps factorize [mk_fst z, mk_snd z]
14.13 | factorize z = [z]
14.14
14.15 -fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
14.16 +fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
14.17 let
14.18 fun aux eq ss Ts t =
14.19 let
14.20 @@ -565,7 +566,7 @@
14.21 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
14.22 | (Const (x as (s as @{const_name Suc}, T)), []) =>
14.23 if is_built_in_const thy stds false x then Cst (Suc, T, Any)
14.24 - else if is_constr thy stds x then do_construct x []
14.25 + else if is_constr ctxt stds x then do_construct x []
14.26 else ConstName (s, T, Any)
14.27 | (Const (@{const_name finite}, T), [t1]) =>
14.28 (if is_finite_type hol_ctxt (domain_type T) then
14.29 @@ -576,7 +577,7 @@
14.30 | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
14.31 | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
14.32 if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
14.33 - else if is_constr thy stds x then do_construct x []
14.34 + else if is_constr ctxt stds x then do_construct x []
14.35 else ConstName (s, T, Any)
14.36 | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
14.37 if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
14.38 @@ -653,7 +654,7 @@
14.39 [t1, t2]) =>
14.40 Op2 (Union, T1, Any, sub t1, sub t2)
14.41 | (t0 as Const (x as (s, T)), ts) =>
14.42 - if is_constr thy stds x then
14.43 + if is_constr ctxt stds x then
14.44 do_construct x ts
14.45 else if String.isPrefix numeral_prefix s then
14.46 Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
14.47 @@ -677,6 +678,24 @@
14.48 end
14.49 in aux eq [] [] end
14.50
14.51 +fun is_fully_representable_set u =
14.52 + not (is_opt_rep (rep_of u)) andalso
14.53 + case u of
14.54 + FreeName _ => true
14.55 + | Op1 (SingletonSet, _, _, _) => true
14.56 + | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
14.57 + | Op2 (oper, _, _, u1, u2) =>
14.58 + if oper = Union orelse oper = SetDifference orelse oper = Intersect then
14.59 + forall is_fully_representable_set [u1, u2]
14.60 + else if oper = Apply then
14.61 + case u1 of
14.62 + ConstName (s, _, _) =>
14.63 + is_sel_like_and_no_discr s orelse s = @{const_name set}
14.64 + | _ => false
14.65 + else
14.66 + false
14.67 + | _ => false
14.68 +
14.69 fun rep_for_abs_fun scope T =
14.70 let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
14.71 Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
14.72 @@ -687,13 +706,13 @@
14.73 val R = best_non_opt_set_rep_for_type scope (type_of v)
14.74 val v = modify_name_rep v R
14.75 in (v :: vs, NameTable.update (v, R) table) end
14.76 -fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
14.77 +fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
14.78 (vs, table) =
14.79 let
14.80 val x as (s, T) = (nickname_of v, type_of v)
14.81 - val R = (if is_abs_fun thy x then
14.82 + val R = (if is_abs_fun ctxt x then
14.83 rep_for_abs_fun
14.84 - else if is_rep_fun thy x then
14.85 + else if is_rep_fun ctxt x then
14.86 Func oo best_non_opt_symmetric_reps_for_fun_type
14.87 else if all_exact orelse is_skolem_name v orelse
14.88 member (op =) [@{const_name undefined_fast_The},
14.89 @@ -766,22 +785,6 @@
14.90 fun unknown_boolean T R =
14.91 Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
14.92 T, R)
14.93 -fun is_fully_representable_set u =
14.94 - not (is_opt_rep (rep_of u)) andalso
14.95 - case u of
14.96 - FreeName _ => true
14.97 - | Op1 (SingletonSet, _, _, _) => true
14.98 - | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
14.99 - | Op2 (oper, _, _, u1, u2) =>
14.100 - if oper = Union orelse oper = SetDifference orelse oper = Intersect then
14.101 - forall is_fully_representable_set [u1, u2]
14.102 - else if oper = Apply then
14.103 - case u1 of
14.104 - ConstName (s, _, _) => is_sel_like_and_no_discr s
14.105 - | _ => false
14.106 - else
14.107 - false
14.108 - | _ => false
14.109
14.110 fun s_op1 oper T R u1 =
14.111 ((if oper = Not then
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 17:36:53 2010 +0200
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 20:52:01 2010 +0200
15.3 @@ -25,6 +25,10 @@
15.4 (polar = Pos andalso quant_s = @{const_name Ex}) orelse
15.5 (polar = Neg andalso quant_s <> @{const_name Ex})
15.6
15.7 +val is_descr =
15.8 + member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
15.9 + @{const_name safe_Eps}]
15.10 +
15.11 (** Binary coding of integers **)
15.12
15.13 (* If a formula contains a numeral whose absolute value is more than this
15.14 @@ -65,14 +69,15 @@
15.15
15.16 (** Uncurrying **)
15.17
15.18 -fun add_to_uncurry_table thy t =
15.19 +fun add_to_uncurry_table ctxt t =
15.20 let
15.21 + val thy = ProofContext.theory_of ctxt
15.22 fun aux (t1 $ t2) args table =
15.23 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
15.24 | aux (Abs (_, _, t')) _ table = aux t' [] table
15.25 | aux (t as Const (x as (s, _))) args table =
15.26 if is_built_in_const thy [(NONE, true)] true x orelse
15.27 - is_constr_like thy x orelse
15.28 + is_constr_like ctxt x orelse
15.29 is_sel s orelse s = @{const_name Sigma} then
15.30 table
15.31 else
15.32 @@ -121,8 +126,8 @@
15.33
15.34 (** Boxing **)
15.35
15.36 -fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
15.37 - orig_t =
15.38 +fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
15.39 + def orig_t =
15.40 let
15.41 fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
15.42 Type (@{type_name fun}, map box_relational_operator_type Ts)
15.43 @@ -178,7 +183,7 @@
15.44 list_comb (Const (s0, T --> T --> body_type T0),
15.45 map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
15.46 end
15.47 - and do_description_operator s T =
15.48 + and do_descr s T =
15.49 let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
15.50 Const (s, (T1 --> bool_T) --> T1)
15.51 end
15.52 @@ -213,28 +218,26 @@
15.53 | @{const "op -->"} $ t1 $ t2 =>
15.54 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
15.55 $ do_term new_Ts old_Ts polar t2
15.56 - | Const (s as @{const_name The}, T) => do_description_operator s T
15.57 - | Const (s as @{const_name Eps}, T) => do_description_operator s T
15.58 - | Const (s as @{const_name safe_The}, T) => do_description_operator s T
15.59 - | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T
15.60 | Const (x as (s, T)) =>
15.61 - Const (s, if s = @{const_name converse} orelse
15.62 - s = @{const_name trancl} then
15.63 - box_relational_operator_type T
15.64 - else if String.isPrefix quot_normal_prefix s then
15.65 - let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
15.66 - T' --> T'
15.67 - end
15.68 - else if is_built_in_const thy stds fast_descrs x orelse
15.69 - s = @{const_name Sigma} then
15.70 - T
15.71 - else if is_constr_like thy x then
15.72 - box_type hol_ctxt InConstr T
15.73 - else if is_sel s
15.74 - orelse is_rep_fun thy x then
15.75 - box_type hol_ctxt InSel T
15.76 - else
15.77 - box_type hol_ctxt InExpr T)
15.78 + if is_descr s then
15.79 + do_descr s T
15.80 + else
15.81 + Const (s, if s = @{const_name converse} orelse
15.82 + s = @{const_name trancl} then
15.83 + box_relational_operator_type T
15.84 + else if String.isPrefix quot_normal_prefix s then
15.85 + let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
15.86 + T' --> T'
15.87 + end
15.88 + else if is_built_in_const thy stds fast_descrs x orelse
15.89 + s = @{const_name Sigma} then
15.90 + T
15.91 + else if is_constr_like ctxt x then
15.92 + box_type hol_ctxt InConstr T
15.93 + else if is_sel s orelse is_rep_fun ctxt x then
15.94 + box_type hol_ctxt InSel T
15.95 + else
15.96 + box_type hol_ctxt InExpr T)
15.97 | t1 $ Abs (s, T, t2') =>
15.98 let
15.99 val t1 = do_term new_Ts old_Ts Neut t1
15.100 @@ -248,7 +251,7 @@
15.101 betapply (if s1 = @{type_name fun} then
15.102 t1
15.103 else
15.104 - select_nth_constr_arg thy stds
15.105 + select_nth_constr_arg ctxt stds
15.106 (@{const_name FunBox},
15.107 Type (@{type_name fun}, Ts1) --> T1) t1 0
15.108 (Type (@{type_name fun}, Ts1)), t2)
15.109 @@ -265,7 +268,7 @@
15.110 betapply (if s1 = @{type_name fun} then
15.111 t1
15.112 else
15.113 - select_nth_constr_arg thy stds
15.114 + select_nth_constr_arg ctxt stds
15.115 (@{const_name FunBox},
15.116 Type (@{type_name fun}, Ts1) --> T1) t1 0
15.117 (Type (@{type_name fun}, Ts1)), t2)
15.118 @@ -293,12 +296,12 @@
15.119 | aux _ = true
15.120 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
15.121
15.122 -fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
15.123 +fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
15.124 args seen =
15.125 let val t_comb = list_comb (t, args) in
15.126 case t of
15.127 Const x =>
15.128 - if not relax andalso is_constr thy stds x andalso
15.129 + if not relax andalso is_constr ctxt stds x andalso
15.130 not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
15.131 has_heavy_bounds_or_vars Ts t_comb andalso
15.132 not (loose_bvar (t_comb, level)) then
15.133 @@ -397,7 +400,7 @@
15.134 $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
15.135 end
15.136
15.137 -fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
15.138 +fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
15.139 let
15.140 val num_occs_of_var =
15.141 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
15.142 @@ -432,7 +435,7 @@
15.143 val n = length arg_Ts
15.144 in
15.145 if length args = n andalso
15.146 - (is_constr thy stds x orelse s = @{const_name Pair} orelse
15.147 + (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
15.148 x = (@{const_name Suc}, nat_T --> nat_T)) andalso
15.149 (not careful orelse not (is_Var t1) orelse
15.150 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
15.151 @@ -449,7 +452,7 @@
15.152 else t0 $ aux false t2 $ aux false t1
15.153 and sel_eq x t n nth_T nth_t =
15.154 HOLogic.eq_const nth_T $ nth_t
15.155 - $ select_nth_constr_arg thy stds x t n nth_T
15.156 + $ select_nth_constr_arg ctxt stds x t n nth_T
15.157 |> aux false
15.158 in aux axiom t end
15.159
15.160 @@ -484,7 +487,7 @@
15.161 aux (t1 :: prems) (Term.add_vars t1 zs) t2
15.162 in aux [] [] end
15.163
15.164 -fun find_bound_assign thy stds j =
15.165 +fun find_bound_assign ctxt stds j =
15.166 let
15.167 fun do_term _ [] = NONE
15.168 | do_term seen (t :: ts) =
15.169 @@ -497,8 +500,9 @@
15.170 | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
15.171 if j' = j andalso
15.172 s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
15.173 - SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
15.174 - [t2], ts @ seen)
15.175 + SOME (construct_value ctxt stds
15.176 + (@{const_name FunBox}, T2 --> T1) [t2],
15.177 + ts @ seen)
15.178 else
15.179 raise SAME ()
15.180 | _ => raise SAME ())
15.181 @@ -523,11 +527,11 @@
15.182 | aux _ = raise SAME ()
15.183 in aux (t, j) handle SAME () => t end
15.184
15.185 -fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
15.186 +fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
15.187 let
15.188 fun kill [] [] ts = foldr1 s_conj ts
15.189 | kill (s :: ss) (T :: Ts) ts =
15.190 - (case find_bound_assign thy stds (length ss) [] ts of
15.191 + (case find_bound_assign ctxt stds (length ss) [] ts of
15.192 SOME (_, []) => @{const True}
15.193 | SOME (arg_t, ts) =>
15.194 kill ss Ts (map (subst_one_bound (length ss)
15.195 @@ -893,7 +897,7 @@
15.196 (if head_of t <> @{const "==>"} then add_def_axiom
15.197 else add_nondef_axiom) depth t
15.198 and add_eq_axiom depth t =
15.199 - (if is_constr_pattern_formula thy t then add_def_axiom
15.200 + (if is_constr_pattern_formula ctxt t then add_def_axiom
15.201 else add_nondef_axiom) depth t
15.202 and add_axioms_for_term depth t (accum as (xs, axs)) =
15.203 case t of
15.204 @@ -909,27 +913,30 @@
15.205 \add_axioms_for_term",
15.206 "too many nested axioms (" ^
15.207 string_of_int depth ^ ")")
15.208 - else if Refute.is_const_of_class thy x then
15.209 + else if is_of_class_const thy x then
15.210 let
15.211 val class = Logic.class_of_const s
15.212 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
15.213 class)
15.214 val ax1 = try (specialize_type thy x) of_class
15.215 val ax2 = Option.map (specialize_type thy x o snd)
15.216 - (Refute.get_classdef thy class)
15.217 + (get_class_def thy class)
15.218 in
15.219 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
15.220 accum
15.221 end
15.222 - else if is_constr thy stds x then
15.223 + else if is_constr ctxt stds x then
15.224 accum
15.225 + else if is_descr (original_name s) then
15.226 + fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
15.227 + accum
15.228 else if is_equational_fun hol_ctxt x then
15.229 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
15.230 accum
15.231 else if is_choice_spec_fun hol_ctxt x then
15.232 fold (add_nondef_axiom depth)
15.233 (nondef_props_for_const thy true choice_spec_table x) accum
15.234 - else if is_abs_fun thy x then
15.235 + else if is_abs_fun ctxt x then
15.236 if is_quot_type thy (range_type T) then
15.237 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
15.238 else
15.239 @@ -940,7 +947,7 @@
15.240 ? fold (add_maybe_def_axiom depth)
15.241 (nondef_props_for_const thy true
15.242 (extra_table def_table s) x)
15.243 - else if is_rep_fun thy x then
15.244 + else if is_rep_fun ctxt x then
15.245 if is_quot_type thy (domain_type T) then
15.246 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
15.247 else
15.248 @@ -952,9 +959,11 @@
15.249 (nondef_props_for_const thy true
15.250 (extra_table def_table s) x)
15.251 |> add_axioms_for_term depth
15.252 - (Const (mate_of_rep_fun thy x))
15.253 + (Const (mate_of_rep_fun ctxt x))
15.254 |> fold (add_def_axiom depth)
15.255 - (inverse_axioms_for_rep_fun thy x)
15.256 + (inverse_axioms_for_rep_fun ctxt x)
15.257 + else if s = @{const_name TYPE} then
15.258 + accum
15.259 else
15.260 accum |> user_axioms <> SOME false
15.261 ? fold (add_nondef_axiom depth)
15.262 @@ -977,8 +986,8 @@
15.263 | TVar (_, S) => add_axioms_for_sort depth T S
15.264 | Type (z as (_, Ts)) =>
15.265 fold (add_axioms_for_type depth) Ts
15.266 - #> (if is_pure_typedef thy T then
15.267 - fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
15.268 + #> (if is_pure_typedef ctxt T then
15.269 + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
15.270 else if is_quot_type thy T then
15.271 fold (add_def_axiom depth)
15.272 (optimized_quot_type_axioms ctxt stds z)
15.273 @@ -1018,7 +1027,7 @@
15.274
15.275 (** Simplification of constructor/selector terms **)
15.276
15.277 -fun simplify_constrs_and_sels thy t =
15.278 +fun simplify_constrs_and_sels ctxt t =
15.279 let
15.280 fun is_nth_sel_on t' n (Const (s, _) $ t) =
15.281 (t = t' andalso is_sel_like_and_no_discr s andalso
15.282 @@ -1030,7 +1039,7 @@
15.283 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
15.284 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
15.285 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
15.286 - ((if is_constr_like thy x then
15.287 + ((if is_constr_like ctxt x then
15.288 if length args = num_binder_types T then
15.289 case hd args of
15.290 Const (_, T') $ t' =>
15.291 @@ -1046,7 +1055,7 @@
15.292 else if is_sel_like_and_no_discr s then
15.293 case strip_comb (hd args) of
15.294 (Const (x' as (s', T')), ts') =>
15.295 - if is_constr_like thy x' andalso
15.296 + if is_constr_like ctxt x' andalso
15.297 constr_name_for_sel_like s = s' andalso
15.298 not (exists is_pair_type (binder_types T')) then
15.299 list_comb (nth ts' (sel_no_from_name s), tl args)
15.300 @@ -1228,7 +1237,7 @@
15.301
15.302 val max_skolem_depth = 4
15.303
15.304 -fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
15.305 +fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
15.306 boxes, ...}) finitizes monos t =
15.307 let
15.308 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
15.309 @@ -1248,7 +1257,7 @@
15.310 val box = exists (not_equal (SOME false) o snd) boxes
15.311 val table =
15.312 Termtab.empty
15.313 - |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
15.314 + |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
15.315 fun do_rest def =
15.316 binarize ? binarize_nat_and_int_in_term
15.317 #> box ? uncurry_term table
15.318 @@ -1259,7 +1268,7 @@
15.319 #> curry_assms
15.320 #> destroy_universal_equalities
15.321 #> destroy_existential_equalities hol_ctxt
15.322 - #> simplify_constrs_and_sels thy
15.323 + #> simplify_constrs_and_sels ctxt
15.324 #> distribute_quantifiers
15.325 #> push_quantifiers_inward
15.326 #> close_form
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jun 01 17:36:53 2010 +0200
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jun 01 20:52:01 2010 +0200
16.3 @@ -135,7 +135,7 @@
16.4 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
16.5
16.6 fun quintuple_for_scope quote
16.7 - ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
16.8 + ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
16.9 datatypes, ...} : scope) =
16.10 let
16.11 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
16.12 @@ -144,8 +144,8 @@
16.13 card_assigns |> filter_out (member (op =) boring_Ts o fst)
16.14 |> List.partition (is_fp_iterator_type o fst)
16.15 val (secondary_card_assigns, primary_card_assigns) =
16.16 - card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
16.17 - o fst)
16.18 + card_assigns
16.19 + |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
16.20 val cards =
16.21 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
16.22 string_of_int k)
16.23 @@ -458,13 +458,13 @@
16.24 concrete = concrete, deep = deep, constrs = constrs}
16.25 end
16.26
16.27 -fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
16.28 +fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
16.29 finitizable_dataTs (desc as (card_assigns, _)) =
16.30 let
16.31 val datatypes =
16.32 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
16.33 finitizable_dataTs desc)
16.34 - (filter (is_datatype thy stds o fst) card_assigns)
16.35 + (filter (is_datatype ctxt stds o fst) card_assigns)
16.36 val bits = card_of_type card_assigns @{typ signed_bit} - 1
16.37 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
16.38 card_of_type card_assigns @{typ unsigned_bit}
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 17:36:53 2010 +0200
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 20:52:01 2010 +0200
17.3 @@ -57,8 +57,15 @@
17.4 val bool_T : typ
17.5 val nat_T : typ
17.6 val int_T : typ
17.7 + val simple_string_of_typ : typ -> string
17.8 + val is_real_constr : theory -> string * typ -> bool
17.9 + val typ_of_dtyp :
17.10 + Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
17.11 + -> typ
17.12 + val is_of_class_const : theory -> string * typ -> bool
17.13 + val get_class_def : theory -> string -> (string * term) option
17.14 val monomorphic_term : Type.tyenv -> term -> term
17.15 - val specialize_type : theory -> (string * typ) -> term -> term
17.16 + val specialize_type : theory -> string * typ -> term -> term
17.17 val nat_subscript : int -> string
17.18 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
17.19 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
17.20 @@ -229,15 +236,25 @@
17.21 val nat_T = @{typ nat}
17.22 val int_T = @{typ int}
17.23
17.24 +val simple_string_of_typ = Refute.string_of_typ
17.25 +val is_real_constr = Refute.is_IDT_constructor
17.26 +val typ_of_dtyp = Refute.typ_of_dtyp
17.27 +val is_of_class_const = Refute.is_const_of_class
17.28 +val get_class_def = Refute.get_classdef
17.29 val monomorphic_term = Sledgehammer_Util.monomorphic_term
17.30 val specialize_type = Sledgehammer_Util.specialize_type
17.31
17.32 -val subscript = implode o map (prefix "\<^isub>") o explode
17.33 +val i_subscript = implode o map (prefix "\<^isub>") o explode
17.34 +fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
17.35 fun nat_subscript n =
17.36 - (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
17.37 - numbers *)
17.38 - if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
17.39 - else subscript (string_of_int n)
17.40 + let val s = signed_string_of_int n in
17.41 + if print_mode_active Symbol.xsymbolsN then
17.42 + (* cheap trick to ensure proper alphanumeric ordering for one- and
17.43 + two-digit numbers *)
17.44 + (if n <= 9 then be_subscript else i_subscript) s
17.45 + else
17.46 + s
17.47 + end
17.48
17.49 fun time_limit NONE = I
17.50 | time_limit (SOME delay) = TimeLimit.timeLimit delay
18.1 --- a/src/HOL/Tools/inductive.ML Tue Jun 01 17:36:53 2010 +0200
18.2 +++ b/src/HOL/Tools/inductive.ML Tue Jun 01 20:52:01 2010 +0200
18.3 @@ -719,8 +719,7 @@
18.4 Local_Theory.notes
18.5 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
18.6 map (fn th => [([th],
18.7 - [Attrib.internal (K (Context_Rules.intro_query NONE)),
18.8 - Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
18.9 + [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
18.10 map (hd o snd);
18.11 val (((_, elims'), (_, [induct'])), lthy2) =
18.12 lthy1 |>
19.1 --- a/src/HOL/Tools/refute.ML Tue Jun 01 17:36:53 2010 +0200
19.2 +++ b/src/HOL/Tools/refute.ML Tue Jun 01 20:52:01 2010 +0200
19.3 @@ -1165,6 +1165,13 @@
19.4 val fm_u = (if negate then toFalse else toTrue) (hd intrs)
19.5 val fm_ax = PropLogic.all (map toTrue (tl intrs))
19.6 val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
19.7 + val _ =
19.8 + (if satsolver = "dpll" orelse satsolver = "enumerate" then
19.9 + warning ("Using SAT solver " ^ quote satsolver ^
19.10 + "; for better performance, consider installing an \
19.11 + \external solver.")
19.12 + else
19.13 + ());
19.14 val solver =
19.15 SatSolver.invoke_solver satsolver
19.16 handle Option.Option =>
20.1 --- a/src/HOL/Tools/sat_solver.ML Tue Jun 01 17:36:53 2010 +0200
20.2 +++ b/src/HOL/Tools/sat_solver.ML Tue Jun 01 20:52:01 2010 +0200
20.3 @@ -543,10 +543,6 @@
20.4 (* do not call solver "auto" from within "auto" *)
20.5 loop solvers
20.6 else (
20.7 - (if name="dpll" orelse name="enumerate" then
20.8 - warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
20.9 - else
20.10 - ());
20.11 (* apply 'solver' to 'fm' *)
20.12 solver fm
20.13 handle SatSolver.NOT_CONFIGURED => loop solvers