1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Mar 08 15:20:40 2010 -0800
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Mar 09 09:25:23 2010 +0100
1.3 @@ -136,8 +136,8 @@
1.4 suggesting several textual improvements.
1.5 % and Perry James for reporting a typo.
1.6
1.7 -\section{First Steps}
1.8 -\label{first-steps}
1.9 +\section{Overview}
1.10 +\label{overview}
1.11
1.12 This section introduces Nitpick by presenting small examples. If possible, you
1.13 should try out the examples on your workstation. Your theory file should start
1.14 @@ -145,7 +145,7 @@
1.15
1.16 \prew
1.17 \textbf{theory}~\textit{Scratch} \\
1.18 -\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
1.19 +\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
1.20 \textbf{begin}
1.21 \postw
1.22
1.23 @@ -677,7 +677,7 @@
1.24 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
1.25 \hbox{}\qquad Datatypes: \\
1.26 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
1.27 -\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.28 +\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.29 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
1.30 \postw
1.31
1.32 @@ -704,8 +704,6 @@
1.33 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
1.34 \postw
1.35
1.36 -
1.37 -
1.38 Finally, Nitpick provides rudimentary support for rationals and reals using a
1.39 similar approach:
1.40
1.41 @@ -940,9 +938,10 @@
1.42 \label{coinductive-datatypes}
1.43
1.44 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
1.45 -datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
1.46 -list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
1.47 -these lazy lists seamlessly and provides a hook, described in
1.48 +datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
1.49 +\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
1.50 +``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
1.51 +supports these lazy lists seamlessly and provides a hook, described in
1.52 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
1.53 datatypes.
1.54
1.55 @@ -1165,10 +1164,11 @@
1.56
1.57 {\looseness=-1
1.58 Boxing can be enabled or disabled globally or on a per-type basis using the
1.59 -\textit{box} option. Moreover, setting the cardinality of a function or
1.60 -product type implicitly enables boxing for that type. Nitpick usually performs
1.61 -reasonable choices about which types should be boxed, but option tweaking
1.62 -sometimes helps.
1.63 +\textit{box} option. Nitpick usually performs reasonable choices about which
1.64 +types should be boxed, but option tweaking sometimes helps. A related optimization,
1.65 +``finalization,'' attempts to wrap functions that constant at all but finitely
1.66 +many points (e.g., finite sets); see the documentation for the \textit{finalize}
1.67 +option in \S\ref{scope-of-search} for details.
1.68
1.69 }
1.70
1.71 @@ -1850,7 +1850,7 @@
1.72 The number of options can be overwhelming at first glance. Do not let that worry
1.73 you: Nitpick's defaults have been chosen so that it almost always does the right
1.74 thing, and the most important options have been covered in context in
1.75 -\S\ref{first-steps}.
1.76 +\S\ref{overview}.
1.77
1.78 The descriptions below refer to the following syntactic quantities:
1.79
1.80 @@ -1936,14 +1936,10 @@
1.81 Specifies the sequence of cardinalities to use for a given type.
1.82 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.83 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.84 -Although function and product types are normally mapped directly to the
1.85 -corresponding Kodkod concepts, setting
1.86 -the cardinality of such types is also allowed and implicitly enables ``boxing''
1.87 -for them, as explained in the description of the \textit{box}~\qty{type}
1.88 -and \textit{box} (\S\ref{scope-of-search}) options.
1.89
1.90 \nopagebreak
1.91 -{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.92 +{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1.93 +(\S\ref{scope-of-search}).}
1.94
1.95 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.96 Specifies the default sequence of cardinalities to use. This can be overridden
1.97 @@ -2062,8 +2058,8 @@
1.98 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1.99 product type in an isomorphic datatype internally. Boxing is an effective mean
1.100 to reduce the search space and speed up Nitpick, because the isomorphic datatype
1.101 -is approximated by a subset of the possible function or pair values;
1.102 -like other drastic optimizations, it can also prevent the discovery of
1.103 +is approximated by a subset of the possible function or pair values.
1.104 +Like other drastic optimizations, it can also prevent the discovery of
1.105 counterexamples. The option can take the following values:
1.106
1.107 \begin{enum}
1.108 @@ -2075,30 +2071,68 @@
1.109 higher-order functions are good candidates for boxing.
1.110 \end{enum}
1.111
1.112 -Setting the \textit{card}~\qty{type} option for a function or product type
1.113 -implicitly enables boxing for that type.
1.114 -
1.115 \nopagebreak
1.116 -{\small See also \textit{verbose} (\S\ref{output-format})
1.117 -and \textit{debug} (\S\ref{output-format}).}
1.118 +{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
1.119 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
1.120
1.121 \opsmart{box}{dont\_box}
1.122 Specifies the default boxing setting to use. This can be overridden on a
1.123 per-type basis using the \textit{box}~\qty{type} option described above.
1.124
1.125 +\opargboolorsmart{finitize}{type}{dont\_finitize}
1.126 +Specifies whether Nitpick should attempt to finitize a given type, which can be
1.127 +a function type or an infinite ``shallow datatype'' (an infinite datatype whose
1.128 +constructors don't appear in the problem).
1.129 +
1.130 +For function types, Nitpick performs a monotonicity analysis to detect functions
1.131 +that are constant at all but finitely many points (e.g., finite sets) and treats
1.132 +such occurrences specially, thereby increasing the precision. The option can
1.133 +then take the following values:
1.134 +
1.135 +\begin{enum}
1.136 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
1.137 +\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
1.138 +type wherever possible.
1.139 +\end{enum}
1.140 +
1.141 +The semantics of the option is somewhat different for infinite shallow
1.142 +datatypes:
1.143 +
1.144 +\begin{enum}
1.145 +\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
1.146 +unsound, counterexamples generated under these conditions are tagged as ``likely
1.147 +genuine.''
1.148 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
1.149 +\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
1.150 +detect whether the datatype can be safely finitized before finitizing it.
1.151 +\end{enum}
1.152 +
1.153 +Like other drastic optimizations, finitization can sometimes prevent the
1.154 +discovery of counterexamples.
1.155 +
1.156 +\nopagebreak
1.157 +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
1.158 +(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
1.159 +\textit{debug} (\S\ref{output-format}).}
1.160 +
1.161 +\opsmart{finitize}{dont\_finitize}
1.162 +Specifies the default finitization setting to use. This can be overridden on a
1.163 +per-type basis using the \textit{finitize}~\qty{type} option described above.
1.164 +
1.165 \opargboolorsmart{mono}{type}{non\_mono}
1.166 -Specifies whether the given type should be considered monotonic when
1.167 -enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1.168 -monotonicity check on the type. Setting this option to \textit{true} can reduce
1.169 -the number of scopes tried, but it also diminishes the theoretical chance of
1.170 +Specifies whether the given type should be considered monotonic when enumerating
1.171 +scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
1.172 +performs a monotonicity check on the type. Setting this option to \textit{true}
1.173 +can reduce the number of scopes tried, but it can also diminish the chance of
1.174 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
1.175
1.176 \nopagebreak
1.177 {\small See also \textit{card} (\S\ref{scope-of-search}),
1.178 +\textit{finitize} (\S\ref{scope-of-search}),
1.179 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1.180 (\S\ref{output-format}).}
1.181
1.182 -\opsmart{mono}{non\_box}
1.183 +\opsmart{mono}{non\_mono}
1.184 Specifies the default monotonicity setting to use. This can be overridden on a
1.185 per-type basis using the \textit{mono}~\qty{type} option described above.
1.186
2.1 --- a/doc-src/manual.bib Mon Mar 08 15:20:40 2010 -0800
2.2 +++ b/doc-src/manual.bib Tue Mar 09 09:25:23 2010 +0100
2.3 @@ -1759,3 +1759,12 @@
2.4 key = "Wikipedia",
2.5 title = "Wikipedia: {AA} Tree",
2.6 note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
2.7 +
2.8 +@incollection{lochbihler-2010,
2.9 + title = "Coinduction",
2.10 + author = "Andreas Lochbihler",
2.11 + booktitle = "The Archive of Formal Proofs",
2.12 + editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
2.13 + publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
2.14 + month = "Feb.",
2.15 + year = 2010}
3.1 --- a/src/HOL/Nitpick.thy Mon Mar 08 15:20:40 2010 -0800
3.2 +++ b/src/HOL/Nitpick.thy Tue Mar 09 09:25:23 2010 +0100
3.3 @@ -38,8 +38,9 @@
3.4 and Quot :: "'a \<Rightarrow> 'b"
3.5 and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
3.6
3.7 +datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
3.8 +datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
3.9 datatype ('a, 'b) pair_box = PairBox 'a 'b
3.10 -datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
3.11
3.12 typedecl unsigned_bit
3.13 typedecl signed_bit
3.14 @@ -220,8 +221,8 @@
3.15 use "Tools/Nitpick/kodkod_sat.ML"
3.16 use "Tools/Nitpick/nitpick_util.ML"
3.17 use "Tools/Nitpick/nitpick_hol.ML"
3.18 +use "Tools/Nitpick/nitpick_mono.ML"
3.19 use "Tools/Nitpick/nitpick_preproc.ML"
3.20 -use "Tools/Nitpick/nitpick_mono.ML"
3.21 use "Tools/Nitpick/nitpick_scope.ML"
3.22 use "Tools/Nitpick/nitpick_peephole.ML"
3.23 use "Tools/Nitpick/nitpick_rep.ML"
3.24 @@ -236,11 +237,12 @@
3.25 setup {* Nitpick_Isar.setup *}
3.26
3.27 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
3.28 - bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
3.29 - wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
3.30 - Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
3.31 + bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
3.32 + wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
3.33 + Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
3.34 times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
3.35 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
3.36 +hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
3.37 + word
3.38 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
3.39 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
3.40 The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
4.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 08 15:20:40 2010 -0800
4.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 09:25:23 2010 +0100
4.3 @@ -8,7 +8,7 @@
4.4 header {* Examples from the Nitpick Manual *}
4.5
4.6 theory Manual_Nits
4.7 -imports Main Coinductive_List Quotient_Product RealDef
4.8 +imports Main Quotient_Product RealDef
4.9 begin
4.10
4.11 chapter {* 3. First Steps *}
4.12 @@ -173,13 +173,35 @@
4.13
4.14 subsection {* 3.9. Coinductive Datatypes *}
4.15
4.16 +(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
4.17 +we cannot rely on its presence, we expediently provide our own axiomatization.
4.18 +The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
4.19 +
4.20 +typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
4.21 +
4.22 +definition LNil where "LNil = Abs_llist (Inl [])"
4.23 +definition LCons where
4.24 +"LCons y ys = Abs_llist (case Rep_llist ys of
4.25 + Inl ys' \<Rightarrow> Inl (y # ys')
4.26 + | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
4.27 +
4.28 +axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
4.29 +
4.30 +lemma iterates_def [nitpick_simp]:
4.31 +"iterates f a = LCons a (iterates f (f a))"
4.32 +sorry
4.33 +
4.34 +setup {*
4.35 +Nitpick.register_codatatype @{typ "'a llist"} ""
4.36 + (map dest_Const [@{term LNil}, @{term LCons}])
4.37 +*}
4.38 +
4.39 lemma "xs \<noteq> LCons a xs"
4.40 nitpick
4.41 oops
4.42
4.43 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
4.44 nitpick [verbose]
4.45 -nitpick [bisim_depth = -1, verbose]
4.46 oops
4.47
4.48 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
5.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Mar 08 15:20:40 2010 -0800
5.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Mar 09 09:25:23 2010 +0100
5.3 @@ -36,8 +36,10 @@
5.4 datatype rep = SRep | RRep
5.5
5.6 (* Proof.context -> typ -> unit *)
5.7 -fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
5.8 - | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts
5.9 +fun check_type ctxt (Type (@{type_name fun}, Ts)) =
5.10 + List.app (check_type ctxt) Ts
5.11 + | check_type ctxt (Type (@{type_name "*"}, Ts)) =
5.12 + List.app (check_type ctxt) Ts
5.13 | check_type _ @{typ bool} = ()
5.14 | check_type _ (TFree (_, @{sort "{}"})) = ()
5.15 | check_type _ (TFree (_, @{sort HOL.type})) = ()
5.16 @@ -45,13 +47,14 @@
5.17 raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
5.18
5.19 (* rep -> (typ -> int) -> typ -> int list *)
5.20 -fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =
5.21 +fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
5.22 replicate_list (card T1) (atom_schema_of SRep card T2)
5.23 - | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =
5.24 + | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
5.25 atom_schema_of SRep card T1
5.26 - | atom_schema_of RRep card (Type ("fun", [T1, T2])) =
5.27 + | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
5.28 atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
5.29 - | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts
5.30 + | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
5.31 + maps (atom_schema_of SRep card) Ts
5.32 | atom_schema_of _ card T = [card T]
5.33 (* rep -> (typ -> int) -> typ -> int *)
5.34 val arity_of = length ooo atom_schema_of
5.35 @@ -89,7 +92,7 @@
5.36 fun kodkod_formula_from_term ctxt card frees =
5.37 let
5.38 (* typ -> rel_expr -> rel_expr *)
5.39 - fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
5.40 + fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
5.41 let
5.42 val jss = atom_schema_of SRep card T1 |> map (rpair 0)
5.43 |> all_combinations
5.44 @@ -100,7 +103,7 @@
5.45 (index_seq 0 (length jss)) jss
5.46 |> foldl1 Union
5.47 end
5.48 - | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =
5.49 + | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
5.50 let
5.51 val jss = atom_schema_of SRep card T1 |> map (rpair 0)
5.52 |> all_combinations
5.53 @@ -115,7 +118,7 @@
5.54 end
5.55 | R_rep_from_S_rep _ r = r
5.56 (* typ list -> typ -> rel_expr -> rel_expr *)
5.57 - fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =
5.58 + fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
5.59 Comprehension (decls_for SRep card Ts T,
5.60 RelEq (R_rep_from_S_rep T
5.61 (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
5.62 @@ -137,7 +140,9 @@
5.63 | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
5.64 RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
5.65 | Const (@{const_name ord_class.less_eq},
5.66 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
5.67 + Type (@{type_name fun},
5.68 + [Type (@{type_name fun}, [_, @{typ bool}]), _]))
5.69 + $ t1 $ t2 =>
5.70 Subset (to_R_rep Ts t1, to_R_rep Ts t2)
5.71 | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
5.72 | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
5.73 @@ -179,7 +184,8 @@
5.74 | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
5.75 | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
5.76 | Const (@{const_name ord_class.less_eq},
5.77 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
5.78 + Type (@{type_name fun},
5.79 + [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
5.80 to_R_rep Ts (eta_expand Ts t 1)
5.81 | Const (@{const_name ord_class.less_eq}, _) =>
5.82 to_R_rep Ts (eta_expand Ts t 2)
5.83 @@ -190,7 +196,7 @@
5.84 | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
5.85 | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
5.86 | Const (@{const_name bot_class.bot},
5.87 - T as Type ("fun", [_, @{typ bool}])) =>
5.88 + T as Type (@{type_name fun}, [_, @{typ bool}])) =>
5.89 empty_n_ary_rel (arity_of RRep card T)
5.90 | Const (@{const_name insert}, _) $ t1 $ t2 =>
5.91 Union (to_S_rep Ts t1, to_R_rep Ts t2)
5.92 @@ -203,27 +209,35 @@
5.93 raise NOT_SUPPORTED "transitive closure for function or pair type"
5.94 | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
5.95 | Const (@{const_name semilattice_inf_class.inf},
5.96 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
5.97 + Type (@{type_name fun},
5.98 + [Type (@{type_name fun}, [_, @{typ bool}]), _]))
5.99 + $ t1 $ t2 =>
5.100 Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
5.101 | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
5.102 to_R_rep Ts (eta_expand Ts t 1)
5.103 | Const (@{const_name semilattice_inf_class.inf}, _) =>
5.104 to_R_rep Ts (eta_expand Ts t 2)
5.105 | Const (@{const_name semilattice_sup_class.sup},
5.106 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
5.107 + Type (@{type_name fun},
5.108 + [Type (@{type_name fun}, [_, @{typ bool}]), _]))
5.109 + $ t1 $ t2 =>
5.110 Union (to_R_rep Ts t1, to_R_rep Ts t2)
5.111 | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
5.112 to_R_rep Ts (eta_expand Ts t 1)
5.113 | Const (@{const_name semilattice_sup_class.sup}, _) =>
5.114 to_R_rep Ts (eta_expand Ts t 2)
5.115 | Const (@{const_name minus_class.minus},
5.116 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
5.117 + Type (@{type_name fun},
5.118 + [Type (@{type_name fun}, [_, @{typ bool}]), _]))
5.119 + $ t1 $ t2 =>
5.120 Difference (to_R_rep Ts t1, to_R_rep Ts t2)
5.121 | Const (@{const_name minus_class.minus},
5.122 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
5.123 + Type (@{type_name fun},
5.124 + [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
5.125 to_R_rep Ts (eta_expand Ts t 1)
5.126 | Const (@{const_name minus_class.minus},
5.127 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>
5.128 + Type (@{type_name fun},
5.129 + [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
5.130 to_R_rep Ts (eta_expand Ts t 2)
5.131 | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
5.132 | Const (@{const_name Pair}, _) $ _ => raise SAME ()
5.133 @@ -277,7 +291,8 @@
5.134 end
5.135
5.136 (* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
5.137 -fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =
5.138 +fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
5.139 + r =
5.140 if body_type T2 = bool_T then
5.141 True
5.142 else
5.143 @@ -294,8 +309,9 @@
5.144 let
5.145 val thy = ProofContext.theory_of ctxt
5.146 (* typ -> int *)
5.147 - fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
5.148 - | card (Type ("*", [T1, T2])) = card T1 * card T2
5.149 + fun card (Type (@{type_name fun}, [T1, T2])) =
5.150 + reasonable_power (card T2) (card T1)
5.151 + | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
5.152 | card @{typ bool} = 2
5.153 | card T = Int.max (1, raw_card T)
5.154 val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
6.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 08 15:20:40 2010 -0800
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 09:25:23 2010 +0100
6.3 @@ -15,6 +15,7 @@
6.4 bitss: int list,
6.5 bisim_depths: int list,
6.6 boxes: (typ option * bool option) list,
6.7 + finitizes: (typ option * bool option) list,
6.8 monos: (typ option * bool option) list,
6.9 stds: (typ option * bool) list,
6.10 wfs: (styp option * bool option) list,
6.11 @@ -87,6 +88,7 @@
6.12 bitss: int list,
6.13 bisim_depths: int list,
6.14 boxes: (typ option * bool option) list,
6.15 + finitizes: (typ option * bool option) list,
6.16 monos: (typ option * bool option) list,
6.17 stds: (typ option * bool) list,
6.18 wfs: (styp option * bool option) list,
6.19 @@ -200,13 +202,13 @@
6.20 error "You must import the theory \"Nitpick\" to use Nitpick"
6.21 *)
6.22 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
6.23 - boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
6.24 - user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
6.25 - specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
6.26 - peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
6.27 - max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
6.28 - max_potential, max_genuine, check_potential, check_genuine, batch_size,
6.29 - ...} =
6.30 + boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
6.31 + verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
6.32 + destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
6.33 + fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
6.34 + flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
6.35 + evals, formats, max_potential, max_genuine, check_potential,
6.36 + check_genuine, batch_size, ...} =
6.37 params
6.38 val state_ref = Unsynchronized.ref state
6.39 (* Pretty.T -> unit *)
6.40 @@ -289,7 +291,7 @@
6.41 val _ = null (Term.add_tvars assms_t []) orelse
6.42 raise NOT_SUPPORTED "schematic type variables"
6.43 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
6.44 - binarize) = preprocess_term hol_ctxt assms_t
6.45 + binarize) = preprocess_term hol_ctxt finitizes monos assms_t
6.46 val got_all_user_axioms =
6.47 got_all_mono_user_axioms andalso no_poly_user_axioms
6.48
6.49 @@ -321,7 +323,11 @@
6.50 fold add_free_and_const_names (nondef_us @ def_us) ([], [])
6.51 val (sel_names, nonsel_names) =
6.52 List.partition (is_sel o nickname_of) const_names
6.53 - val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
6.54 + val sound_finitizes =
6.55 + none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
6.56 + | _ => false) finitizes)
6.57 + val genuine_means_genuine =
6.58 + got_all_user_axioms andalso none_true wfs andalso sound_finitizes
6.59 val standard = forall snd stds
6.60 (*
6.61 val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
6.62 @@ -340,21 +346,30 @@
6.63 ". " ^ extra
6.64 end
6.65 (* typ -> bool *)
6.66 - fun is_type_always_monotonic T =
6.67 + fun is_type_fundamentally_monotonic T =
6.68 (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
6.69 (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
6.70 is_number_type thy T orelse is_bit_type T
6.71 fun is_type_actually_monotonic T =
6.72 formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
6.73 + fun is_type_kind_of_monotonic T =
6.74 + case triple_lookup (type_match thy) monos T of
6.75 + SOME (SOME false) => false
6.76 + | _ => is_type_actually_monotonic T
6.77 fun is_type_monotonic T =
6.78 unique_scope orelse
6.79 case triple_lookup (type_match thy) monos T of
6.80 SOME (SOME b) => b
6.81 - | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
6.82 - fun is_type_finitizable T =
6.83 - case triple_lookup (type_match thy) monos T of
6.84 - SOME (SOME false) => false
6.85 - | _ => is_type_actually_monotonic T
6.86 + | _ => is_type_fundamentally_monotonic T orelse
6.87 + is_type_actually_monotonic T
6.88 + fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
6.89 + is_type_kind_of_monotonic T
6.90 + | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
6.91 + is_type_kind_of_monotonic T
6.92 + | is_shallow_datatype_finitizable T =
6.93 + case triple_lookup (type_match thy) finitizes T of
6.94 + SOME (SOME b) => b
6.95 + | _ => is_type_kind_of_monotonic T
6.96 fun is_datatype_deep T =
6.97 not standard orelse T = nat_T orelse is_word_type T orelse
6.98 exists (curry (op =) T o domain_type o type_of) sel_names
6.99 @@ -371,7 +386,7 @@
6.100 val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
6.101 val _ =
6.102 if verbose andalso not unique_scope then
6.103 - case filter_out is_type_always_monotonic mono_Ts of
6.104 + case filter_out is_type_fundamentally_monotonic mono_Ts of
6.105 [] => ()
6.106 | interesting_mono_Ts =>
6.107 print_v (K (monotonicity_message interesting_mono_Ts
6.108 @@ -382,7 +397,7 @@
6.109 all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
6.110 val finitizable_dataTs =
6.111 shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
6.112 - |> filter is_type_finitizable
6.113 + |> filter is_shallow_datatype_finitizable
6.114 val _ =
6.115 if verbose andalso not (null finitizable_dataTs) then
6.116 print_v (K (monotonicity_message finitizable_dataTs
6.117 @@ -649,6 +664,8 @@
6.118 ? cons ("user_axioms", "\"true\"")
6.119 |> not (none_true wfs)
6.120 ? cons ("wf", "\"smart\" or \"false\"")
6.121 + |> not sound_finitizes
6.122 + ? cons ("finitize", "\"smart\" or \"false\"")
6.123 |> not codatatypes_ok
6.124 ? cons ("bisim_depth", "a nonnegative value")
6.125 val ss =
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 08 15:20:40 2010 -0800
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 09:25:23 2010 +0100
7.3 @@ -65,8 +65,8 @@
7.4 val strip_any_connective : term -> term list * term
7.5 val conjuncts_of : term -> term list
7.6 val disjuncts_of : term -> term list
7.7 - val unarize_and_unbox_type : typ -> typ
7.8 - val unarize_unbox_and_uniterize_type : typ -> typ
7.9 + val unarize_unbox_etc_type : typ -> typ
7.10 + val uniterize_unarize_unbox_etc_type : typ -> typ
7.11 val string_for_type : Proof.context -> typ -> string
7.12 val prefix_name : string -> string -> string
7.13 val shortest_name : string -> string
7.14 @@ -148,11 +148,13 @@
7.15 theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
7.16 val construct_value :
7.17 theory -> (typ option * bool) list -> styp -> term list -> term
7.18 + val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
7.19 val card_of_type : (typ * int) list -> typ -> int
7.20 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
7.21 val bounded_exact_card_of_type :
7.22 hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
7.23 val is_finite_type : hol_context -> typ -> bool
7.24 + val is_small_finite_type : hol_context -> typ -> bool
7.25 val special_bounds : term list -> (indexname * typ) list
7.26 val abs_var : indexname * typ -> term -> term
7.27 val is_funky_typedef : theory -> typ -> bool
7.28 @@ -401,22 +403,24 @@
7.29 | unarize_type @{typ "signed_bit word"} = int_T
7.30 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
7.31 | unarize_type T = T
7.32 -fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
7.33 - unarize_and_unbox_type (Type ("fun", Ts))
7.34 - | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
7.35 - Type ("*", map unarize_and_unbox_type Ts)
7.36 - | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
7.37 - | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
7.38 - | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
7.39 - Type (s, map unarize_and_unbox_type Ts)
7.40 - | unarize_and_unbox_type T = T
7.41 +fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
7.42 + unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
7.43 + | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
7.44 + unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
7.45 + | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
7.46 + Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
7.47 + | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
7.48 + | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
7.49 + | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
7.50 + Type (s, map unarize_unbox_etc_type Ts)
7.51 + | unarize_unbox_etc_type T = T
7.52 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
7.53 | uniterize_type @{typ bisim_iterator} = nat_T
7.54 | uniterize_type T = T
7.55 -val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
7.56 +val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
7.57
7.58 (* Proof.context -> typ -> string *)
7.59 -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
7.60 +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
7.61
7.62 (* string -> string -> string *)
7.63 val prefix_name = Long_Name.qualify o Long_Name.base_name
7.64 @@ -439,9 +443,10 @@
7.65 #> map_types shorten_names_in_type
7.66
7.67 (* theory -> typ * typ -> bool *)
7.68 -fun type_match thy (T1, T2) =
7.69 +fun strict_type_match thy (T1, T2) =
7.70 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
7.71 handle Type.TYPE_MATCH => false
7.72 +fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
7.73 (* theory -> styp * styp -> bool *)
7.74 fun const_match thy ((s1, T1), (s2, T2)) =
7.75 s1 = s2 andalso type_match thy (T1, T2)
7.76 @@ -454,14 +459,14 @@
7.77 (* typ -> bool *)
7.78 fun is_TFree (TFree _) = true
7.79 | is_TFree _ = false
7.80 -fun is_higher_order_type (Type ("fun", _)) = true
7.81 +fun is_higher_order_type (Type (@{type_name fun}, _)) = true
7.82 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
7.83 | is_higher_order_type _ = false
7.84 -fun is_fun_type (Type ("fun", _)) = true
7.85 +fun is_fun_type (Type (@{type_name fun}, _)) = true
7.86 | is_fun_type _ = false
7.87 -fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
7.88 +fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
7.89 | is_set_type _ = false
7.90 -fun is_pair_type (Type ("*", _)) = true
7.91 +fun is_pair_type (Type (@{type_name "*"}, _)) = true
7.92 | is_pair_type _ = false
7.93 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
7.94 | is_lfp_iterator_type _ = false
7.95 @@ -494,19 +499,20 @@
7.96
7.97 (* int -> typ -> typ list * typ *)
7.98 fun strip_n_binders 0 T = ([], T)
7.99 - | strip_n_binders n (Type ("fun", [T1, T2])) =
7.100 + | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
7.101 strip_n_binders (n - 1) T2 |>> cons T1
7.102 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
7.103 - strip_n_binders n (Type ("fun", Ts))
7.104 + strip_n_binders n (Type (@{type_name fun}, Ts))
7.105 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
7.106 (* typ -> typ *)
7.107 val nth_range_type = snd oo strip_n_binders
7.108
7.109 (* typ -> int *)
7.110 -fun num_factors_in_type (Type ("*", [T1, T2])) =
7.111 +fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
7.112 fold (Integer.add o num_factors_in_type) [T1, T2] 0
7.113 | num_factors_in_type _ = 1
7.114 -fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
7.115 +fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
7.116 + 1 + num_binder_types T2
7.117 | num_binder_types _ = 0
7.118 (* typ -> typ list *)
7.119 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
7.120 @@ -515,7 +521,7 @@
7.121
7.122 (* typ -> term list -> term *)
7.123 fun mk_flat_tuple _ [t] = t
7.124 - | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
7.125 + | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
7.126 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
7.127 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
7.128 (* int -> term -> term list *)
7.129 @@ -595,7 +601,7 @@
7.130 val (co_s, co_Ts) = dest_Type co_T
7.131 val _ =
7.132 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
7.133 - co_s <> "fun" andalso
7.134 + co_s <> @{type_name fun} andalso
7.135 not (is_basic_datatype thy [(NONE, true)] co_s) then
7.136 ()
7.137 else
7.138 @@ -669,7 +675,7 @@
7.139 find_index (curry (op =) s o fst)
7.140 (Record.get_extT_fields thy T1 ||> single |> op @)
7.141 (* theory -> styp -> bool *)
7.142 -fun is_record_get thy (s, Type ("fun", [T1, _])) =
7.143 +fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
7.144 exists (curry (op =) s o fst) (all_record_fields thy T1)
7.145 | is_record_get _ _ = false
7.146 fun is_record_update thy (s, T) =
7.147 @@ -677,30 +683,33 @@
7.148 exists (curry (op =) (unsuffix Record.updateN s) o fst)
7.149 (all_record_fields thy (body_type T))
7.150 handle TYPE _ => false
7.151 -fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
7.152 +fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
7.153 (case typedef_info thy s' of
7.154 SOME {Abs_name, ...} => s = Abs_name
7.155 | NONE => false)
7.156 | is_abs_fun _ _ = false
7.157 -fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
7.158 +fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
7.159 (case typedef_info thy s' of
7.160 SOME {Rep_name, ...} => s = Rep_name
7.161 | NONE => false)
7.162 | is_rep_fun _ _ = false
7.163 (* Proof.context -> styp -> bool *)
7.164 -fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
7.165 +fun is_quot_abs_fun ctxt
7.166 + (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
7.167 (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
7.168 = SOME (Const x))
7.169 | is_quot_abs_fun _ _ = false
7.170 -fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
7.171 +fun is_quot_rep_fun ctxt
7.172 + (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
7.173 (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
7.174 = SOME (Const x))
7.175 | is_quot_rep_fun _ _ = false
7.176
7.177 (* theory -> styp -> styp *)
7.178 -fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
7.179 +fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
7.180 + [T1 as Type (s', _), T2]))) =
7.181 (case typedef_info thy s' of
7.182 - SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
7.183 + SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
7.184 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
7.185 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
7.186 (* theory -> typ -> typ *)
7.187 @@ -729,10 +738,10 @@
7.188 end
7.189 handle TYPE ("dest_Type", _, _) => false
7.190 fun is_constr_like thy (s, T) =
7.191 - member (op =) [@{const_name FunBox}, @{const_name PairBox},
7.192 - @{const_name Quot}, @{const_name Zero_Rep},
7.193 - @{const_name Suc_Rep}] s orelse
7.194 - let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
7.195 + member (op =) [@{const_name FinFun}, @{const_name FunBox},
7.196 + @{const_name PairBox}, @{const_name Quot},
7.197 + @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
7.198 + let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
7.199 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
7.200 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
7.201 is_coconstr thy x
7.202 @@ -749,8 +758,8 @@
7.203 (* string -> bool *)
7.204 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
7.205 val is_sel_like_and_no_discr =
7.206 - String.isPrefix sel_prefix
7.207 - orf (member (op =) [@{const_name fst}, @{const_name snd}])
7.208 + String.isPrefix sel_prefix orf
7.209 + (member (op =) [@{const_name fst}, @{const_name snd}])
7.210
7.211 (* boxability -> boxability *)
7.212 fun in_fun_lhs_for InConstr = InSel
7.213 @@ -763,10 +772,10 @@
7.214 (* hol_context -> boxability -> typ -> bool *)
7.215 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
7.216 case T of
7.217 - Type ("fun", _) =>
7.218 + Type (@{type_name fun}, _) =>
7.219 (boxy = InPair orelse boxy = InFunLHS) andalso
7.220 not (is_boolean_type (body_type T))
7.221 - | Type ("*", Ts) =>
7.222 + | Type (@{type_name "*"}, Ts) =>
7.223 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
7.224 ((boxy = InExpr orelse boxy = InFunLHS) andalso
7.225 exists (is_boxing_worth_it hol_ctxt InPair)
7.226 @@ -780,7 +789,7 @@
7.227 (* hol_context -> boxability -> typ -> typ *)
7.228 and box_type hol_ctxt boxy T =
7.229 case T of
7.230 - Type (z as ("fun", [T1, T2])) =>
7.231 + Type (z as (@{type_name fun}, [T1, T2])) =>
7.232 if boxy <> InConstr andalso boxy <> InSel andalso
7.233 should_box_type hol_ctxt boxy z then
7.234 Type (@{type_name fun_box},
7.235 @@ -788,12 +797,13 @@
7.236 else
7.237 box_type hol_ctxt (in_fun_lhs_for boxy) T1
7.238 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
7.239 - | Type (z as ("*", Ts)) =>
7.240 + | Type (z as (@{type_name "*"}, Ts)) =>
7.241 if boxy <> InConstr andalso boxy <> InSel
7.242 andalso should_box_type hol_ctxt boxy z then
7.243 Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
7.244 else
7.245 - Type ("*", map (box_type hol_ctxt
7.246 + Type (@{type_name "*"},
7.247 + map (box_type hol_ctxt
7.248 (if boxy = InConstr orelse boxy = InSel then boxy
7.249 else InPair)) Ts)
7.250 | _ => T
7.251 @@ -979,7 +989,7 @@
7.252 else
7.253 let
7.254 (* int -> typ -> int * term *)
7.255 - fun aux m (Type ("*", [T1, T2])) =
7.256 + fun aux m (Type (@{type_name "*"}, [T1, T2])) =
7.257 let
7.258 val (m, t1) = aux m T1
7.259 val (m, t2) = aux m T2
7.260 @@ -1018,10 +1028,85 @@
7.261 | _ => list_comb (Const x, args)
7.262 end
7.263
7.264 +(* hol_context -> typ -> term -> term *)
7.265 +fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
7.266 + (case head_of t of
7.267 + Const x => if is_constr_like thy x then t else raise SAME ()
7.268 + | _ => raise SAME ())
7.269 + handle SAME () =>
7.270 + let
7.271 + val x' as (_, T') =
7.272 + if is_pair_type T then
7.273 + let val (T1, T2) = HOLogic.dest_prodT T in
7.274 + (@{const_name Pair}, T1 --> T2 --> T)
7.275 + end
7.276 + else
7.277 + datatype_constrs hol_ctxt T |> hd
7.278 + val arg_Ts = binder_types T'
7.279 + in
7.280 + list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
7.281 + (index_seq 0 (length arg_Ts)) arg_Ts)
7.282 + end
7.283 +
7.284 +(* (term -> term) -> int -> term -> term *)
7.285 +fun coerce_bound_no f j t =
7.286 + case t of
7.287 + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
7.288 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
7.289 + | Bound j' => if j' = j then f t else t
7.290 + | _ => t
7.291 +(* hol_context -> typ -> typ -> term -> term *)
7.292 +fun coerce_bound_0_in_term hol_ctxt new_T old_T =
7.293 + old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
7.294 +(* hol_context -> typ list -> typ -> typ -> term -> term *)
7.295 +and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
7.296 + if old_T = new_T then
7.297 + t
7.298 + else
7.299 + case (new_T, old_T) of
7.300 + (Type (new_s, new_Ts as [new_T1, new_T2]),
7.301 + Type (@{type_name fun}, [old_T1, old_T2])) =>
7.302 + (case eta_expand Ts t 1 of
7.303 + Abs (s, _, t') =>
7.304 + Abs (s, new_T1,
7.305 + t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
7.306 + |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
7.307 + |> Envir.eta_contract
7.308 + |> new_s <> @{type_name fun}
7.309 + ? construct_value thy stds
7.310 + (if new_s = @{type_name fin_fun} then @{const_name FinFun}
7.311 + else @{const_name FunBox},
7.312 + Type (@{type_name fun}, new_Ts) --> new_T)
7.313 + o single
7.314 + | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
7.315 + | (Type (new_s, new_Ts as [new_T1, new_T2]),
7.316 + Type (old_s, old_Ts as [old_T1, old_T2])) =>
7.317 + if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
7.318 + old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
7.319 + case constr_expand hol_ctxt old_T t of
7.320 + Const (old_s, _) $ t1 =>
7.321 + if new_s = @{type_name fun} then
7.322 + coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
7.323 + else
7.324 + construct_value thy stds
7.325 + (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
7.326 + [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
7.327 + (Type (@{type_name fun}, old_Ts)) t1]
7.328 + | Const _ $ t1 $ t2 =>
7.329 + construct_value thy stds
7.330 + (if new_s = @{type_name "*"} then @{const_name Pair}
7.331 + else @{const_name PairBox}, new_Ts ---> new_T)
7.332 + (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
7.333 + [t1, t2])
7.334 + | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
7.335 + else
7.336 + raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
7.337 + | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
7.338 +
7.339 (* (typ * int) list -> typ -> int *)
7.340 -fun card_of_type assigns (Type ("fun", [T1, T2])) =
7.341 +fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
7.342 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
7.343 - | card_of_type assigns (Type ("*", [T1, T2])) =
7.344 + | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
7.345 card_of_type assigns T1 * card_of_type assigns T2
7.346 | card_of_type _ (Type (@{type_name itself}, _)) = 1
7.347 | card_of_type _ @{typ prop} = 2
7.348 @@ -1033,7 +1118,8 @@
7.349 | NONE => if T = @{typ bisim_iterator} then 0
7.350 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
7.351 (* int -> (typ * int) list -> typ -> int *)
7.352 -fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
7.353 +fun bounded_card_of_type max default_card assigns
7.354 + (Type (@{type_name fun}, [T1, T2])) =
7.355 let
7.356 val k1 = bounded_card_of_type max default_card assigns T1
7.357 val k2 = bounded_card_of_type max default_card assigns T2
7.358 @@ -1041,7 +1127,8 @@
7.359 if k1 = max orelse k2 = max then max
7.360 else Int.min (max, reasonable_power k2 k1)
7.361 end
7.362 - | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
7.363 + | bounded_card_of_type max default_card assigns
7.364 + (Type (@{type_name "*"}, [T1, T2])) =
7.365 let
7.366 val k1 = bounded_card_of_type max default_card assigns T1
7.367 val k2 = bounded_card_of_type max default_card assigns T2
7.368 @@ -1064,7 +1151,7 @@
7.369 else if member (op =) finitizable_dataTs T then
7.370 raise SAME ()
7.371 else case T of
7.372 - Type ("fun", [T1, T2]) =>
7.373 + Type (@{type_name fun}, [T1, T2]) =>
7.374 let
7.375 val k1 = aux avoid T1
7.376 val k2 = aux avoid T2
7.377 @@ -1073,7 +1160,7 @@
7.378 else if k1 >= max orelse k2 >= max then max
7.379 else Int.min (max, reasonable_power k2 k1)
7.380 end
7.381 - | Type ("*", [T1, T2]) =>
7.382 + | Type (@{type_name "*"}, [T1, T2]) =>
7.383 let
7.384 val k1 = aux avoid T1
7.385 val k2 = aux avoid T2
7.386 @@ -1104,9 +1191,16 @@
7.387 AList.lookup (op =) assigns T |> the_default default_card
7.388 in Int.min (max, aux [] T) end
7.389
7.390 +val small_type_max_card = 5
7.391 +
7.392 (* hol_context -> typ -> bool *)
7.393 fun is_finite_type hol_ctxt T =
7.394 - bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
7.395 + bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
7.396 +(* hol_context -> typ -> bool *)
7.397 +fun is_small_finite_type hol_ctxt T =
7.398 + let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
7.399 + n > 0 andalso n <= small_type_max_card
7.400 + end
7.401
7.402 (* term -> bool *)
7.403 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
7.404 @@ -1144,7 +1238,8 @@
7.405 is_typedef_axiom thy boring t2
7.406 | is_typedef_axiom thy boring
7.407 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
7.408 - $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
7.409 + $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
7.410 + $ Const _ $ _)) =
7.411 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
7.412 | is_typedef_axiom _ _ _ = false
7.413
7.414 @@ -1538,8 +1633,8 @@
7.415 fun is_inductive_pred hol_ctxt =
7.416 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
7.417 fun is_equational_fun hol_ctxt =
7.418 - (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
7.419 - orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
7.420 + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
7.421 + (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
7.422
7.423 (* term * term -> term *)
7.424 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
7.425 @@ -1586,7 +1681,7 @@
7.426 fun do_term depth Ts t =
7.427 case t of
7.428 (t0 as Const (@{const_name Int.number_class.number_of},
7.429 - Type ("fun", [_, ran_T]))) $ t1 =>
7.430 + Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
7.431 ((if is_number_type thy ran_T then
7.432 let
7.433 val j = t1 |> HOLogic.dest_numeral
7.434 @@ -1612,7 +1707,7 @@
7.435 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
7.436 map (do_term depth Ts) [t1, t2])
7.437 | Const (x as (@{const_name distinct},
7.438 - Type ("fun", [Type (@{type_name list}, [T']), _])))
7.439 + Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
7.440 $ (t1 as _ $ _) =>
7.441 (t1 |> HOLogic.dest_list |> distinctness_formula T'
7.442 handle TERM _ => do_const depth Ts t x [t1])
7.443 @@ -1969,7 +2064,7 @@
7.444 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
7.445 val set_T = tuple_T --> bool_T
7.446 val curried_T = tuple_T --> set_T
7.447 - val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
7.448 + val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
7.449 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
7.450 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
7.451 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
7.452 @@ -2092,8 +2187,8 @@
7.453 let
7.454 fun aux T accum =
7.455 case T of
7.456 - Type ("fun", Ts) => fold aux Ts accum
7.457 - | Type ("*", Ts) => fold aux Ts accum
7.458 + Type (@{type_name fun}, Ts) => fold aux Ts accum
7.459 + | Type (@{type_name "*"}, Ts) => fold aux Ts accum
7.460 | Type (@{type_name itself}, [T1]) => aux T1 accum
7.461 | Type (_, Ts) =>
7.462 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
7.463 @@ -2161,7 +2256,7 @@
7.464 (* int list -> int list -> typ -> typ *)
7.465 fun format_type default_format format T =
7.466 let
7.467 - val T = unarize_unbox_and_uniterize_type T
7.468 + val T = uniterize_unarize_unbox_etc_type T
7.469 val format = format |> filter (curry (op <) 0)
7.470 in
7.471 if forall (curry (op =) 1) format then
7.472 @@ -2200,7 +2295,7 @@
7.473 (* term -> term *)
7.474 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
7.475 val (x' as (_, T'), js, ts) =
7.476 - AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
7.477 + AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
7.478 |> the_single
7.479 val max_j = List.last js
7.480 val Ts = List.take (binder_types T', max_j + 1)
7.481 @@ -2294,7 +2389,7 @@
7.482 let val t = Const (original_name s, T) in
7.483 (t, format_term_type thy def_table formats t)
7.484 end)
7.485 - |>> map_types unarize_unbox_and_uniterize_type
7.486 + |>> map_types uniterize_unarize_unbox_etc_type
7.487 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
7.488 in do_const end
7.489
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 08 15:20:40 2010 -0800
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Mar 09 09:25:23 2010 +0100
8.3 @@ -39,6 +39,7 @@
8.4 ("bits", ["1,2,3,4,6,8,10,12"]),
8.5 ("bisim_depth", ["7"]),
8.6 ("box", ["smart"]),
8.7 + ("finitize", ["smart"]),
8.8 ("mono", ["smart"]),
8.9 ("std", ["true"]),
8.10 ("wf", ["smart"]),
8.11 @@ -78,6 +79,7 @@
8.12
8.13 val negated_params =
8.14 [("dont_box", "box"),
8.15 + ("dont_finitize", "finitize"),
8.16 ("non_mono", "mono"),
8.17 ("non_std", "std"),
8.18 ("non_wf", "wf"),
8.19 @@ -111,8 +113,8 @@
8.20 AList.defined (op =) negated_params s orelse
8.21 s = "max" orelse s = "eval" orelse s = "expect" orelse
8.22 exists (fn p => String.isPrefix (p ^ " ") s)
8.23 - ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
8.24 - "non_std", "wf", "non_wf", "format"]
8.25 + ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
8.26 + "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
8.27
8.28 (* string * 'a -> unit *)
8.29 fun check_raw_param (s, _) =
8.30 @@ -297,14 +299,8 @@
8.31 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
8.32 val bitss = lookup_int_seq "bits" 1
8.33 val bisim_depths = lookup_int_seq "bisim_depth" ~1
8.34 - val boxes =
8.35 - lookup_bool_option_assigns read_type_polymorphic "box" @
8.36 - map_filter (fn (SOME T, _) =>
8.37 - if is_fun_type T orelse is_pair_type T then
8.38 - SOME (SOME T, SOME true)
8.39 - else
8.40 - NONE
8.41 - | (NONE, _) => NONE) cards_assigns
8.42 + val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
8.43 + val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
8.44 val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
8.45 val stds = lookup_bool_assigns read_type_polymorphic "std"
8.46 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
8.47 @@ -349,8 +345,8 @@
8.48 in
8.49 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
8.50 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
8.51 - boxes = boxes, monos = monos, stds = stds, wfs = wfs,
8.52 - sat_solver = sat_solver, blocking = blocking, falsify = falsify,
8.53 + boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
8.54 + wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
8.55 debug = debug, verbose = verbose, overlord = overlord,
8.56 user_axioms = user_axioms, assms = assms,
8.57 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 08 15:20:40 2010 -0800
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 09:25:23 2010 +0100
9.3 @@ -301,8 +301,8 @@
9.4
9.5 (* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
9.6 fun bound_for_sel_rel ctxt debug dtypes
9.7 - (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
9.8 - nick)) =
9.9 + (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
9.10 + R as Func (Atom (_, j0), R2), nick)) =
9.11 let
9.12 val {delta, epsilon, exclusive, explicit_max, ...} =
9.13 constr_spec dtypes (original_name nick, T1)
9.14 @@ -1208,7 +1208,7 @@
9.15 (rel_expr_from_rel_expr kk min_R R2 r2))
9.16 end
9.17 | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
9.18 - | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
9.19 + | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
9.20 to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
9.21 | Cst (Num j, T, R) =>
9.22 if is_word_type T then
9.23 @@ -1229,36 +1229,36 @@
9.24 | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
9.25 kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
9.26 | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
9.27 - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
9.28 - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
9.29 - | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
9.30 + | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
9.31 + | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
9.32 + | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
9.33 to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
9.34 - | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
9.35 + | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
9.36 to_bit_word_binary_op T R
9.37 (SOME (fn i1 => fn i2 => fn i3 =>
9.38 kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
9.39 (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
9.40 (SOME (curry KK.Add))
9.41 - | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
9.42 + | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>
9.43 KK.Rel nat_subtract_rel
9.44 - | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
9.45 + | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>
9.46 KK.Rel int_subtract_rel
9.47 - | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
9.48 + | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
9.49 to_bit_word_binary_op T R NONE
9.50 (SOME (fn i1 => fn i2 =>
9.51 KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
9.52 - | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
9.53 + | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
9.54 to_bit_word_binary_op T R
9.55 (SOME (fn i1 => fn i2 => fn i3 =>
9.56 kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
9.57 (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
9.58 (SOME (curry KK.Sub))
9.59 - | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
9.60 + | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>
9.61 KK.Rel nat_multiply_rel
9.62 - | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
9.63 + | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>
9.64 KK.Rel int_multiply_rel
9.65 | Cst (Multiply,
9.66 - T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
9.67 + T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>
9.68 to_bit_word_binary_op T R
9.69 (SOME (fn i1 => fn i2 => fn i3 =>
9.70 kk_or (KK.IntEq (i2, KK.Num 0))
9.71 @@ -1267,14 +1267,14 @@
9.72 ? kk_and (KK.LE (KK.Num 0,
9.73 foldl1 KK.BitAnd [i1, i2, i3])))))
9.74 (SOME (curry KK.Mult))
9.75 - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
9.76 - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
9.77 - | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
9.78 + | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
9.79 + | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel
9.80 + | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
9.81 to_bit_word_binary_op T R NONE
9.82 (SOME (fn i1 => fn i2 =>
9.83 KK.IntIf (KK.IntEq (i2, KK.Num 0),
9.84 KK.Num 0, KK.Div (i1, i2))))
9.85 - | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
9.86 + | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
9.87 to_bit_word_binary_op T R
9.88 (SOME (fn i1 => fn i2 => fn i3 =>
9.89 KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
9.90 @@ -1293,9 +1293,9 @@
9.91 | Cst (Fracs, _, Func (Struct _, _)) =>
9.92 kk_project_seq (KK.Rel norm_frac_rel) 2 2
9.93 | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
9.94 - | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
9.95 + | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>
9.96 KK.Iden
9.97 - | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
9.98 + | Cst (NatToInt, Type (_, [@{typ nat}, _]),
9.99 Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
9.100 if nat_j0 = int_j0 then
9.101 kk_intersect KK.Iden
9.102 @@ -1303,9 +1303,9 @@
9.103 KK.Univ)
9.104 else
9.105 raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
9.106 - | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
9.107 + | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
9.108 to_bit_word_unary_op T R I
9.109 - | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
9.110 + | Cst (IntToNat, Type (_, [@{typ int}, _]),
9.111 Func (Atom (int_k, int_j0), nat_R)) =>
9.112 let
9.113 val abs_card = max_int_for_card int_k + 1
9.114 @@ -1321,7 +1321,7 @@
9.115 else
9.116 raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
9.117 end
9.118 - | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
9.119 + | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
9.120 to_bit_word_unary_op T R
9.121 (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
9.122 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 08 15:20:40 2010 -0800
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 09 09:25:23 2010 +0100
10.3 @@ -110,48 +110,53 @@
10.4 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
10.5
10.6 (* term -> term *)
10.7 -fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
10.8 - unarize_and_unbox_term t1
10.9 - | unarize_and_unbox_term (Const (@{const_name PairBox},
10.10 - Type ("fun", [T1, Type ("fun", [T2, _])]))
10.11 - $ t1 $ t2) =
10.12 - let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
10.13 - Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
10.14 - $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
10.15 +fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
10.16 + unarize_unbox_etc_term t1
10.17 + | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
10.18 + unarize_unbox_etc_term t1
10.19 + | unarize_unbox_etc_term
10.20 + (Const (@{const_name PairBox},
10.21 + Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
10.22 + $ t1 $ t2) =
10.23 + let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
10.24 + Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
10.25 + $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
10.26 end
10.27 - | unarize_and_unbox_term (Const (s, T)) =
10.28 - Const (s, unarize_unbox_and_uniterize_type T)
10.29 - | unarize_and_unbox_term (t1 $ t2) =
10.30 - unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
10.31 - | unarize_and_unbox_term (Free (s, T)) =
10.32 - Free (s, unarize_unbox_and_uniterize_type T)
10.33 - | unarize_and_unbox_term (Var (x, T)) =
10.34 - Var (x, unarize_unbox_and_uniterize_type T)
10.35 - | unarize_and_unbox_term (Bound j) = Bound j
10.36 - | unarize_and_unbox_term (Abs (s, T, t')) =
10.37 - Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
10.38 + | unarize_unbox_etc_term (Const (s, T)) =
10.39 + Const (s, uniterize_unarize_unbox_etc_type T)
10.40 + | unarize_unbox_etc_term (t1 $ t2) =
10.41 + unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
10.42 + | unarize_unbox_etc_term (Free (s, T)) =
10.43 + Free (s, uniterize_unarize_unbox_etc_type T)
10.44 + | unarize_unbox_etc_term (Var (x, T)) =
10.45 + Var (x, uniterize_unarize_unbox_etc_type T)
10.46 + | unarize_unbox_etc_term (Bound j) = Bound j
10.47 + | unarize_unbox_etc_term (Abs (s, T, t')) =
10.48 + Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
10.49
10.50 (* typ -> typ -> (typ * typ) * (typ * typ) *)
10.51 -fun factor_out_types (T1 as Type ("*", [T11, T12]))
10.52 - (T2 as Type ("*", [T21, T22])) =
10.53 +fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
10.54 + (T2 as Type (@{type_name "*"}, [T21, T22])) =
10.55 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
10.56 if n1 = n2 then
10.57 let
10.58 val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
10.59 in
10.60 - ((Type ("*", [T11, T11']), opt_T12'),
10.61 - (Type ("*", [T21, T21']), opt_T22'))
10.62 + ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
10.63 + (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
10.64 end
10.65 else if n1 < n2 then
10.66 case factor_out_types T1 T21 of
10.67 (p1, (T21', NONE)) => (p1, (T21', SOME T22))
10.68 | (p1, (T21', SOME T22')) =>
10.69 - (p1, (T21', SOME (Type ("*", [T22', T22]))))
10.70 + (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
10.71 else
10.72 swap (factor_out_types T2 T1)
10.73 end
10.74 - | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
10.75 - | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
10.76 + | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
10.77 + ((T11, SOME T12), (T2, NONE))
10.78 + | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
10.79 + ((T1, NONE), (T21, SOME T22))
10.80 | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
10.81
10.82 (* bool -> typ -> typ -> (term * term) list -> term *)
10.83 @@ -188,10 +193,11 @@
10.84 val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
10.85 in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
10.86 (* typ -> term -> term -> term *)
10.87 -fun pair_up (Type ("*", [T1', T2']))
10.88 +fun pair_up (Type (@{type_name "*"}, [T1', T2']))
10.89 (t1 as Const (@{const_name Pair},
10.90 - Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
10.91 - t2 =
10.92 + Type (@{type_name fun},
10.93 + [_, Type (@{type_name fun}, [_, T1])]))
10.94 + $ t11 $ t12) t2 =
10.95 if T1 = T1' then HOLogic.mk_prod (t1, t2)
10.96 else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
10.97 | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
10.98 @@ -199,7 +205,7 @@
10.99 fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
10.100
10.101 (* typ -> typ -> typ -> term -> term *)
10.102 -fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
10.103 +fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
10.104 let
10.105 (* typ -> typ -> typ -> typ -> term -> term *)
10.106 fun do_curry T1 T1a T1b T2 t =
10.107 @@ -238,9 +244,11 @@
10.108 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
10.109 | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
10.110 (* typ -> typ -> term -> term *)
10.111 - and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
10.112 + and do_term (Type (@{type_name fun}, [T1', T2']))
10.113 + (Type (@{type_name fun}, [T1, T2])) t =
10.114 do_fun T1' T2' T1 T2 t
10.115 - | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
10.116 + | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
10.117 + (Type (@{type_name "*"}, [T1, T2]))
10.118 (Const (@{const_name Pair}, _) $ t1 $ t2) =
10.119 Const (@{const_name Pair}, Ts' ---> T')
10.120 $ do_term T1' T1 t1 $ do_term T2' T2 t2
10.121 @@ -257,7 +265,7 @@
10.122 | truth_const_sort_key _ = "1"
10.123
10.124 (* typ -> term list -> term *)
10.125 -fun mk_tuple (Type ("*", [T1, T2])) ts =
10.126 +fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
10.127 HOLogic.mk_prod (mk_tuple T1 ts,
10.128 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
10.129 | mk_tuple _ (t :: _) = t
10.130 @@ -307,8 +315,8 @@
10.131 else
10.132 aux tps
10.133 end
10.134 - (* typ -> typ -> typ -> (term * term) list -> term *)
10.135 - fun make_map T1 T2 T2' =
10.136 + (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
10.137 + fun make_map maybe_opt T1 T2 T2' =
10.138 let
10.139 val update_const = Const (@{const_name fun_upd},
10.140 (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
10.141 @@ -319,7 +327,7 @@
10.142 Const (@{const_name None}, _) => aux' ps
10.143 | _ => update_const $ aux' ps $ t1 $ t2)
10.144 fun aux ps =
10.145 - if not (is_complete_type datatypes false T1) then
10.146 + if maybe_opt andalso not (is_complete_type datatypes false T1) then
10.147 update_const $ aux' ps $ Const (unrep, T1)
10.148 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
10.149 else
10.150 @@ -328,7 +336,7 @@
10.151 (* typ list -> term -> term *)
10.152 fun polish_funs Ts t =
10.153 (case fastype_of1 (Ts, t) of
10.154 - Type ("fun", [T1, T2]) =>
10.155 + Type (@{type_name fun}, [T1, T2]) =>
10.156 if is_plain_fun t then
10.157 case T2 of
10.158 @{typ bool} =>
10.159 @@ -341,9 +349,9 @@
10.160 end
10.161 | Type (@{type_name option}, [T2']) =>
10.162 let
10.163 - val ts_pair = snd (dest_plain_fun t)
10.164 - |> pairself (map (polish_funs Ts))
10.165 - in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
10.166 + val (maybe_opt, ts_pair) =
10.167 + dest_plain_fun t ||> pairself (map (polish_funs Ts))
10.168 + in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
10.169 | _ => raise SAME ()
10.170 else
10.171 raise SAME ()
10.172 @@ -356,7 +364,7 @@
10.173 else polish_funs Ts t1 $ polish_funs Ts t2
10.174 | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
10.175 | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
10.176 - | Const (s, Type ("fun", [T1, T2])) =>
10.177 + | Const (s, Type (@{type_name fun}, [T1, T2])) =>
10.178 if s = opt_flag orelse s = non_opt_flag then
10.179 Abs ("x", T1, Const (unknown, T2))
10.180 else
10.181 @@ -366,24 +374,24 @@
10.182 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
10.183 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
10.184 |> make_plain_fun maybe_opt T1 T2
10.185 - |> unarize_and_unbox_term
10.186 - |> typecast_fun (unarize_unbox_and_uniterize_type T')
10.187 - (unarize_unbox_and_uniterize_type T1)
10.188 - (unarize_unbox_and_uniterize_type T2)
10.189 + |> unarize_unbox_etc_term
10.190 + |> typecast_fun (uniterize_unarize_unbox_etc_type T')
10.191 + (uniterize_unarize_unbox_etc_type T1)
10.192 + (uniterize_unarize_unbox_etc_type T2)
10.193 (* (typ * int) list -> typ -> typ -> int -> term *)
10.194 - fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
10.195 + fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
10.196 let
10.197 val k1 = card_of_type card_assigns T1
10.198 val k2 = card_of_type card_assigns T2
10.199 in
10.200 - term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
10.201 + term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
10.202 [nth_combination (replicate k1 (k2, 0)) j]
10.203 handle General.Subscript =>
10.204 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
10.205 signed_string_of_int j ^ " for " ^
10.206 string_for_rep (Vect (k1, Atom (k2, 0))))
10.207 end
10.208 - | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
10.209 + | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
10.210 let
10.211 val k1 = card_of_type card_assigns T1
10.212 val k2 = k div k1
10.213 @@ -461,8 +469,9 @@
10.214 if length arg_Ts = 0 then
10.215 []
10.216 else
10.217 - map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
10.218 - arg_jsss
10.219 + map3 (fn Ts =>
10.220 + term_for_rep (constr_s <> @{const_name FinFun})
10.221 + seen Ts Ts) arg_Ts arg_Rs arg_jsss
10.222 |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
10.223 |> dest_n_tuple (length uncur_arg_Ts)
10.224 val t =
10.225 @@ -519,50 +528,54 @@
10.226 and term_for_vect seen k R T1 T2 T' js =
10.227 make_fun true T1 T2 T'
10.228 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
10.229 - (map (term_for_rep seen T2 T2 R o single)
10.230 + (map (term_for_rep true seen T2 T2 R o single)
10.231 (batch_list (arity_of_rep R) js))
10.232 - (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
10.233 - and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
10.234 - | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
10.235 + (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
10.236 + and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
10.237 + | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
10.238 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
10.239 else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
10.240 - | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
10.241 + | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
10.242 + (Struct [R1, R2]) [js] =
10.243 let
10.244 val arity1 = arity_of_rep R1
10.245 val (js1, js2) = chop arity1 js
10.246 in
10.247 list_comb (HOLogic.pair_const T1 T2,
10.248 - map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
10.249 + map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
10.250 [[js1], [js2]])
10.251 end
10.252 - | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
10.253 + | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
10.254 + (Vect (k, R')) [js] =
10.255 term_for_vect seen k R' T1 T2 T' js
10.256 - | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
10.257 - jss =
10.258 + | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
10.259 + (Func (R1, Formula Neut)) jss =
10.260 let
10.261 val jss1 = all_combinations_for_rep R1
10.262 - val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
10.263 + val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
10.264 val ts2 =
10.265 - map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
10.266 + map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
10.267 [[int_from_bool (member (op =) jss js)]])
10.268 jss1
10.269 in make_fun false T1 T2 T' ts1 ts2 end
10.270 - | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
10.271 + | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
10.272 + (Func (R1, R2)) jss =
10.273 let
10.274 val arity1 = arity_of_rep R1
10.275 val jss1 = all_combinations_for_rep R1
10.276 - val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
10.277 + val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
10.278 val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
10.279 - val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
10.280 + val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
10.281 o AList.lookup (op =) grouped_jss2) jss1
10.282 - in make_fun true T1 T2 T' ts1 ts2 end
10.283 - | term_for_rep seen T T' (Opt R) jss =
10.284 - if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
10.285 - | term_for_rep _ T _ R jss =
10.286 + in make_fun maybe_opt T1 T2 T' ts1 ts2 end
10.287 + | term_for_rep _ seen T T' (Opt R) jss =
10.288 + if null jss then Const (unknown, T)
10.289 + else term_for_rep true seen T T' R jss
10.290 + | term_for_rep _ _ T _ R jss =
10.291 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
10.292 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
10.293 string_of_int (length jss))
10.294 - in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
10.295 + in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
10.296
10.297 (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
10.298 -> nut -> term *)
10.299 @@ -689,7 +702,7 @@
10.300 val (oper, (t1, T'), T) =
10.301 case name of
10.302 FreeName (s, T, _) =>
10.303 - let val t = Free (s, unarize_unbox_and_uniterize_type T) in
10.304 + let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
10.305 ("=", (t, format_term_type thy def_table formats t), T)
10.306 end
10.307 | ConstName (s, T, _) =>
10.308 @@ -710,12 +723,17 @@
10.309 (* dtype_spec -> Pretty.T *)
10.310 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
10.311 Pretty.block (Pretty.breaks
10.312 - [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
10.313 - Pretty.str "=",
10.314 - Pretty.enum "," "{" "}"
10.315 - (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
10.316 - (if fun_from_pair complete false then []
10.317 - else [Pretty.str unrep]))])
10.318 + (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
10.319 + (case typ of
10.320 + Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
10.321 + | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
10.322 + | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
10.323 + | _ => []) @
10.324 + [Pretty.str "=",
10.325 + Pretty.enum "," "{" "}"
10.326 + (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
10.327 + (if fun_from_pair complete false then []
10.328 + else [Pretty.str unrep]))]))
10.329 (* typ -> dtype_spec list *)
10.330 fun integer_datatype T =
10.331 [{typ = T, card = card_of_type card_assigns T, co = false,
10.332 @@ -752,13 +770,14 @@
10.333 val (eval_names, noneval_nonskolem_nonsel_names) =
10.334 List.partition (String.isPrefix eval_prefix o nickname_of)
10.335 nonskolem_nonsel_names
10.336 - ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
10.337 + ||> filter_out (member (op =) [@{const_name bisim},
10.338 + @{const_name bisim_iterator_max}]
10.339 o nickname_of)
10.340 val free_names =
10.341 map (fn x as (s, T) =>
10.342 case filter (curry (op =) x
10.343 o pairf nickname_of
10.344 - (unarize_unbox_and_uniterize_type o type_of))
10.345 + (uniterize_unarize_unbox_etc_type o type_of))
10.346 free_names of
10.347 [name] => name
10.348 | [] => FreeName (s, T, Any)
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 08 15:20:40 2010 -0800
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 09:25:23 2010 +0100
11.3 @@ -11,6 +11,9 @@
11.4
11.5 val formulas_monotonic :
11.6 hol_context -> bool -> typ -> term list * term list -> bool
11.7 + val finitize_funs :
11.8 + hol_context -> bool -> (typ option * bool option) list -> typ
11.9 + -> term list * term list -> term list * term list
11.10 end;
11.11
11.12 structure Nitpick_Mono : NITPICK_MONO =
11.13 @@ -42,14 +45,17 @@
11.14 {hol_ctxt: hol_context,
11.15 binarize: bool,
11.16 alpha_T: typ,
11.17 + no_harmless: bool,
11.18 max_fresh: int Unsynchronized.ref,
11.19 - datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
11.20 - constr_cache: (styp * mtyp) list Unsynchronized.ref}
11.21 + datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
11.22 + constr_mcache: (styp * mtyp) list Unsynchronized.ref}
11.23
11.24 -exception MTYPE of string * mtyp list
11.25 +exception MTYPE of string * mtyp list * typ list
11.26 +exception MTERM of string * mterm list
11.27
11.28 (* string -> unit *)
11.29 fun print_g (_ : string) = ()
11.30 +(* val print_g = tracing *)
11.31
11.32 (* var -> string *)
11.33 val string_for_var = signed_string_of_int
11.34 @@ -70,7 +76,7 @@
11.35
11.36 (* sign_atom -> string *)
11.37 fun string_for_sign_atom (S sn) = string_for_sign sn
11.38 - | string_for_sign_atom (V j) = string_for_var j
11.39 + | string_for_sign_atom (V x) = string_for_var x
11.40
11.41 (* literal -> string *)
11.42 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
11.43 @@ -83,7 +89,7 @@
11.44 | is_MRec _ = false
11.45 (* mtyp -> mtyp * sign_atom * mtyp *)
11.46 fun dest_MFun (MFun z) = z
11.47 - | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
11.48 + | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
11.49
11.50 val no_prec = 100
11.51
11.52 @@ -157,13 +163,18 @@
11.53 | mtype_of_mterm (MApp (m1, _)) =
11.54 case mtype_of_mterm m1 of
11.55 MFun (_, _, M12) => M12
11.56 - | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
11.57 + | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
11.58
11.59 -(* hol_context -> bool -> typ -> mdata *)
11.60 -fun initial_mdata hol_ctxt binarize alpha_T =
11.61 +(* mterm -> mterm * mterm list *)
11.62 +fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
11.63 + | strip_mcomb m = (m, [])
11.64 +
11.65 +(* hol_context -> bool -> bool -> typ -> mdata *)
11.66 +fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
11.67 ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
11.68 - max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
11.69 - constr_cache = Unsynchronized.ref []} : mdata)
11.70 + no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
11.71 + datatype_mcache = Unsynchronized.ref [],
11.72 + constr_mcache = Unsynchronized.ref []} : mdata)
11.73
11.74 (* typ -> typ -> bool *)
11.75 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
11.76 @@ -215,7 +226,7 @@
11.77 else repair_mtype cache (M :: seen) M
11.78
11.79 (* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
11.80 -fun repair_datatype_cache cache =
11.81 +fun repair_datatype_mcache cache =
11.82 let
11.83 (* (string * typ list) * mtyp -> unit *)
11.84 fun repair_one (z, M) =
11.85 @@ -224,20 +235,41 @@
11.86 in List.app repair_one (rev (!cache)) end
11.87
11.88 (* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
11.89 -fun repair_constr_cache dtype_cache constr_cache =
11.90 +fun repair_constr_mcache dtype_cache constr_mcache =
11.91 let
11.92 (* styp * mtyp -> unit *)
11.93 fun repair_one (x, M) =
11.94 - Unsynchronized.change constr_cache
11.95 + Unsynchronized.change constr_mcache
11.96 (AList.update (op =) (x, repair_mtype dtype_cache [] M))
11.97 - in List.app repair_one (!constr_cache) end
11.98 + in List.app repair_one (!constr_mcache) end
11.99 +
11.100 +(* typ -> bool *)
11.101 +fun is_fin_fun_supported_type @{typ prop} = true
11.102 + | is_fin_fun_supported_type @{typ bool} = true
11.103 + | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
11.104 + | is_fin_fun_supported_type _ = false
11.105 +(* typ -> typ -> term -> term option *)
11.106 +fun fin_fun_body _ _ (t as @{term False}) = SOME t
11.107 + | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
11.108 + | fin_fun_body dom_T ran_T
11.109 + ((t0 as Const (@{const_name If}, _))
11.110 + $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
11.111 + $ t2 $ t3) =
11.112 + (if loose_bvar1 (t1', 0) then
11.113 + NONE
11.114 + else case fin_fun_body dom_T ran_T t3 of
11.115 + NONE => NONE
11.116 + | SOME t3 =>
11.117 + SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
11.118 + $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
11.119 + | fin_fun_body _ _ _ = NONE
11.120
11.121 (* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
11.122 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
11.123 let
11.124 val M1 = fresh_mtype_for_type mdata T1
11.125 val M2 = fresh_mtype_for_type mdata T2
11.126 - val a = if is_boolean_type (body_type T2) andalso
11.127 + val a = if is_fin_fun_supported_type (body_type T2) andalso
11.128 exists_alpha_sub_mtype_fresh M1 then
11.129 V (Unsynchronized.inc max_fresh)
11.130 else
11.131 @@ -245,25 +277,23 @@
11.132 in (M1, a, M2) end
11.133 (* mdata -> typ -> mtyp *)
11.134 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
11.135 - datatype_cache, constr_cache, ...}) =
11.136 + datatype_mcache, constr_mcache, ...}) =
11.137 let
11.138 - (* typ -> typ -> mtyp *)
11.139 - val do_fun = MFun oo fresh_mfun_for_fun_type mdata
11.140 (* typ -> mtyp *)
11.141 fun do_type T =
11.142 if T = alpha_T then
11.143 MAlpha
11.144 else case T of
11.145 - Type ("fun", [T1, T2]) => do_fun T1 T2
11.146 - | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
11.147 - | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
11.148 + Type (@{type_name fun}, [T1, T2]) =>
11.149 + MFun (fresh_mfun_for_fun_type mdata T1 T2)
11.150 + | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
11.151 | Type (z as (s, _)) =>
11.152 if could_exist_alpha_sub_mtype thy alpha_T T then
11.153 - case AList.lookup (op =) (!datatype_cache) z of
11.154 + case AList.lookup (op =) (!datatype_mcache) z of
11.155 SOME M => M
11.156 | NONE =>
11.157 let
11.158 - val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
11.159 + val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
11.160 val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
11.161 val (all_Ms, constr_Ms) =
11.162 fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
11.163 @@ -279,15 +309,15 @@
11.164 end)
11.165 xs ([], [])
11.166 val M = MType (s, all_Ms)
11.167 - val _ = Unsynchronized.change datatype_cache
11.168 + val _ = Unsynchronized.change datatype_mcache
11.169 (AList.update (op =) (z, M))
11.170 - val _ = Unsynchronized.change constr_cache
11.171 + val _ = Unsynchronized.change constr_mcache
11.172 (append (xs ~~ constr_Ms))
11.173 in
11.174 - if forall (not o is_MRec o snd) (!datatype_cache) then
11.175 - (repair_datatype_cache datatype_cache;
11.176 - repair_constr_cache (!datatype_cache) constr_cache;
11.177 - AList.lookup (op =) (!datatype_cache) z |> the)
11.178 + if forall (not o is_MRec o snd) (!datatype_mcache) then
11.179 + (repair_datatype_mcache datatype_mcache;
11.180 + repair_constr_mcache (!datatype_mcache) constr_mcache;
11.181 + AList.lookup (op =) (!datatype_mcache) z |> the)
11.182 else
11.183 M
11.184 end
11.185 @@ -300,7 +330,7 @@
11.186 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
11.187 | prodM_factors M = [M]
11.188 (* mtyp -> mtyp list * mtyp *)
11.189 -fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
11.190 +fun curried_strip_mtype (MFun (M1, _, M2)) =
11.191 curried_strip_mtype M2 |>> append (prodM_factors M1)
11.192 | curried_strip_mtype M = ([], M)
11.193 (* string -> mtyp -> mtyp *)
11.194 @@ -311,36 +341,34 @@
11.195 end
11.196
11.197 (* mdata -> styp -> mtyp *)
11.198 -fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
11.199 +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
11.200 ...}) (x as (_, T)) =
11.201 if could_exist_alpha_sub_mtype thy alpha_T T then
11.202 - case AList.lookup (op =) (!constr_cache) x of
11.203 + case AList.lookup (op =) (!constr_mcache) x of
11.204 SOME M => M
11.205 | NONE => if T = alpha_T then
11.206 let val M = fresh_mtype_for_type mdata T in
11.207 - (Unsynchronized.change constr_cache (cons (x, M)); M)
11.208 + (Unsynchronized.change constr_mcache (cons (x, M)); M)
11.209 end
11.210 else
11.211 (fresh_mtype_for_type mdata (body_type T);
11.212 - AList.lookup (op =) (!constr_cache) x |> the)
11.213 + AList.lookup (op =) (!constr_mcache) x |> the)
11.214 else
11.215 fresh_mtype_for_type mdata T
11.216 fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
11.217 x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
11.218 |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
11.219
11.220 +(* literal list -> sign_atom -> sign_atom *)
11.221 +fun resolve_sign_atom lits (V x) =
11.222 + x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
11.223 + | resolve_sign_atom _ a = a
11.224 (* literal list -> mtyp -> mtyp *)
11.225 -fun instantiate_mtype lits =
11.226 +fun resolve_mtype lits =
11.227 let
11.228 (* mtyp -> mtyp *)
11.229 fun aux MAlpha = MAlpha
11.230 - | aux (MFun (M1, V x, M2)) =
11.231 - let
11.232 - val a = case AList.lookup (op =) lits x of
11.233 - SOME sn => S sn
11.234 - | NONE => V x
11.235 - in MFun (aux M1, a, aux M2) end
11.236 - | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
11.237 + | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
11.238 | aux (MPair Mp) = MPair (pairself aux Mp)
11.239 | aux (MType (s, Ms)) = MType (s, map aux Ms)
11.240 | aux (MRec z) = MRec z
11.241 @@ -417,11 +445,12 @@
11.242 accum =
11.243 (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
11.244 handle Library.UnequalLengths =>
11.245 - raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
11.246 + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
11.247 | do_mtype_comp _ _ (MType _) (MType _) accum =
11.248 accum (* no need to compare them thanks to the cache *)
11.249 - | do_mtype_comp _ _ M1 M2 _ =
11.250 - raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
11.251 + | do_mtype_comp cmp _ M1 M2 _ =
11.252 + raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
11.253 + [M1, M2], [])
11.254
11.255 (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
11.256 fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
11.257 @@ -471,20 +500,20 @@
11.258 | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
11.259 accum |> fold (do_notin_mtype_fv sn sexp) Ms
11.260 | do_notin_mtype_fv _ _ M _ =
11.261 - raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
11.262 + raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
11.263
11.264 (* sign -> mtyp -> constraint_set -> constraint_set *)
11.265 fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
11.266 | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
11.267 - (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
11.268 - (case sn of Minus => "unique" | Plus => "total") ^ ".");
11.269 + (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
11.270 + (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
11.271 case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
11.272 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
11.273 | SOME (lits, sexps) => CSet (lits, comps, sexps))
11.274
11.275 (* mtyp -> constraint_set -> constraint_set *)
11.276 -val add_mtype_is_right_unique = add_notin_mtype_fv Minus
11.277 -val add_mtype_is_right_total = add_notin_mtype_fv Plus
11.278 +val add_mtype_is_concrete = add_notin_mtype_fv Minus
11.279 +val add_mtype_is_complete = add_notin_mtype_fv Plus
11.280
11.281 val bool_from_minus = true
11.282
11.283 @@ -574,34 +603,35 @@
11.284
11.285 type mtype_schema = mtyp * constraint_set
11.286 type mtype_context =
11.287 - {bounds: mtyp list,
11.288 + {bound_Ts: typ list,
11.289 + bound_Ms: mtyp list,
11.290 frees: (styp * mtyp) list,
11.291 consts: (styp * mtyp) list}
11.292
11.293 type accumulator = mtype_context * constraint_set
11.294
11.295 -val initial_gamma = {bounds = [], frees = [], consts = []}
11.296 +val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
11.297 val unsolvable_accum = (initial_gamma, UnsolvableCSet)
11.298
11.299 -(* mtyp -> mtype_context -> mtype_context *)
11.300 -fun push_bound M {bounds, frees, consts} =
11.301 - {bounds = M :: bounds, frees = frees, consts = consts}
11.302 +(* typ -> mtyp -> mtype_context -> mtype_context *)
11.303 +fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
11.304 + {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
11.305 + consts = consts}
11.306 (* mtype_context -> mtype_context *)
11.307 -fun pop_bound {bounds, frees, consts} =
11.308 - {bounds = tl bounds, frees = frees, consts = consts}
11.309 - handle List.Empty => initial_gamma
11.310 +fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
11.311 + {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
11.312 + consts = consts}
11.313 + handle List.Empty => initial_gamma (* FIXME: needed? *)
11.314
11.315 (* mdata -> term -> accumulator -> mterm * accumulator *)
11.316 fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
11.317 - def_table, ...},
11.318 + def_table, ...},
11.319 alpha_T, max_fresh, ...}) =
11.320 let
11.321 - (* typ -> typ -> mtyp * sign_atom * mtyp *)
11.322 - val mfun_for = fresh_mfun_for_fun_type mdata
11.323 (* typ -> mtyp *)
11.324 val mtype_for = fresh_mtype_for_type mdata
11.325 (* mtyp -> mtyp *)
11.326 - fun pos_set_mtype_for_dom M =
11.327 + fun plus_set_mtype_for_dom M =
11.328 MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
11.329 (* typ -> accumulator -> mterm * accumulator *)
11.330 fun do_all T (gamma, cset) =
11.331 @@ -610,13 +640,13 @@
11.332 val body_M = mtype_for (body_type T)
11.333 in
11.334 (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
11.335 - (gamma, cset |> add_mtype_is_right_total abs_M))
11.336 + (gamma, cset |> add_mtype_is_complete abs_M))
11.337 end
11.338 fun do_equals T (gamma, cset) =
11.339 let val M = mtype_for (domain_type T) in
11.340 (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
11.341 mtype_for (nth_range_type 2 T))),
11.342 - (gamma, cset |> add_mtype_is_right_unique M))
11.343 + (gamma, cset |> add_mtype_is_concrete M))
11.344 end
11.345 fun do_robust_set_operation T (gamma, cset) =
11.346 let
11.347 @@ -633,25 +663,25 @@
11.348 val set_T = domain_type T
11.349 val set_M = mtype_for set_T
11.350 (* typ -> mtyp *)
11.351 - fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
11.352 + fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
11.353 if T = set_T then set_M
11.354 else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
11.355 | custom_mtype_for T = mtype_for T
11.356 in
11.357 - (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
11.358 + (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
11.359 end
11.360 (* typ -> accumulator -> mtyp * accumulator *)
11.361 fun do_pair_constr T accum =
11.362 case mtype_for (nth_range_type 2 T) of
11.363 M as MPair (a_M, b_M) =>
11.364 (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
11.365 - | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
11.366 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
11.367 (* int -> typ -> accumulator -> mtyp * accumulator *)
11.368 fun do_nth_pair_sel n T =
11.369 case mtype_for (domain_type T) of
11.370 M as MPair (a_M, b_M) =>
11.371 pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
11.372 - | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
11.373 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
11.374 (* mtyp * accumulator *)
11.375 val mtype_unsolvable = (dummy_M, unsolvable_accum)
11.376 (* term -> mterm * accumulator *)
11.377 @@ -661,8 +691,9 @@
11.378 fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
11.379 let
11.380 val abs_M = mtype_for abs_T
11.381 - val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
11.382 - val expected_bound_M = pos_set_mtype_for_dom abs_M
11.383 + val (bound_m, accum) =
11.384 + accum |>> push_bound abs_T abs_M |> do_term bound_t
11.385 + val expected_bound_M = plus_set_mtype_for_dom abs_M
11.386 val (body_m, accum) =
11.387 accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
11.388 |> do_term body_t ||> apfst pop_bound
11.389 @@ -678,7 +709,8 @@
11.390 end
11.391 (* term -> accumulator -> mterm * accumulator *)
11.392 and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
11.393 - | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
11.394 + | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
11.395 + cset)) =
11.396 (case t of
11.397 Const (x as (s, T)) =>
11.398 (case AList.lookup (op =) consts x of
11.399 @@ -714,12 +746,12 @@
11.400 let
11.401 val set_T = domain_type (range_type T)
11.402 val M1 = mtype_for (domain_type set_T)
11.403 - val M1' = pos_set_mtype_for_dom M1
11.404 + val M1' = plus_set_mtype_for_dom M1
11.405 val M2 = mtype_for set_T
11.406 val M3 = mtype_for set_T
11.407 in
11.408 (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
11.409 - (gamma, cset |> add_mtype_is_right_unique M1
11.410 + (gamma, cset |> add_mtype_is_concrete M1
11.411 |> add_is_sub_mtype M1' M3
11.412 |> add_is_sub_mtype M2 M3))
11.413 end
11.414 @@ -738,7 +770,7 @@
11.415 | @{const_name finite} =>
11.416 if is_finite_type hol_ctxt T then
11.417 let val M1 = mtype_for (domain_type (domain_type T)) in
11.418 - (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
11.419 + (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
11.420 end
11.421 else
11.422 (print_g "*** finite"; mtype_unsolvable)
11.423 @@ -761,8 +793,8 @@
11.424 val b_M = mtype_for (range_type (domain_type T))
11.425 in
11.426 (MFun (MFun (a_M, S Minus, b_M), S Minus,
11.427 - MFun (pos_set_mtype_for_dom a_M, S Minus,
11.428 - pos_set_mtype_for_dom b_M)), accum)
11.429 + MFun (plus_set_mtype_for_dom a_M, S Minus,
11.430 + plus_set_mtype_for_dom b_M)), accum)
11.431 end
11.432 | @{const_name Sigma} =>
11.433 let
11.434 @@ -784,12 +816,8 @@
11.435 | @{const_name Tha} =>
11.436 let
11.437 val a_M = mtype_for (domain_type (domain_type T))
11.438 - val a_set_M = pos_set_mtype_for_dom a_M
11.439 + val a_set_M = plus_set_mtype_for_dom a_M
11.440 in (MFun (a_set_M, S Minus, a_M), accum) end
11.441 - | @{const_name FunBox} =>
11.442 - let val dom_M = mtype_for (domain_type T) in
11.443 - (MFun (dom_M, S Minus, dom_M), accum)
11.444 - end
11.445 | _ =>
11.446 if s = @{const_name minus_class.minus} andalso
11.447 is_set_type (domain_type T) then
11.448 @@ -800,7 +828,7 @@
11.449 in
11.450 (MFun (left_set_M, S Minus,
11.451 MFun (right_set_M, S Minus, left_set_M)),
11.452 - (gamma, cset |> add_mtype_is_right_unique right_set_M
11.453 + (gamma, cset |> add_mtype_is_concrete right_set_M
11.454 |> add_is_sub_mtype right_set_M left_set_M))
11.455 end
11.456 else if s = @{const_name ord_class.less_eq} andalso
11.457 @@ -811,50 +839,54 @@
11.458 is_set_type (domain_type T) then
11.459 do_robust_set_operation T accum
11.460 else if is_sel s then
11.461 - if constr_name_for_sel_like s = @{const_name FunBox} then
11.462 - let val dom_M = mtype_for (domain_type T) in
11.463 - (MFun (dom_M, S Minus, dom_M), accum)
11.464 - end
11.465 - else
11.466 - (mtype_for_sel mdata x, accum)
11.467 + (mtype_for_sel mdata x, accum)
11.468 else if is_constr thy stds x then
11.469 (mtype_for_constr mdata x, accum)
11.470 - else if is_built_in_const thy stds fast_descrs x then
11.471 + else if is_built_in_const thy stds fast_descrs x andalso
11.472 + s <> @{const_name is_unknown} andalso
11.473 + s <> @{const_name unknown} then
11.474 + (* the "unknown" part is a hack *)
11.475 case def_of_const thy def_table x of
11.476 SOME t' => do_term t' accum |>> mtype_of_mterm
11.477 | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
11.478 else
11.479 let val M = mtype_for T in
11.480 - (M, ({bounds = bounds, frees = frees,
11.481 - consts = (x, M) :: consts}, cset))
11.482 + (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
11.483 + frees = frees, consts = (x, M) :: consts}, cset))
11.484 end) |>> curry MRaw t
11.485 | Free (x as (_, T)) =>
11.486 (case AList.lookup (op =) frees x of
11.487 SOME M => (M, accum)
11.488 | NONE =>
11.489 let val M = mtype_for T in
11.490 - (M, ({bounds = bounds, frees = (x, M) :: frees,
11.491 - consts = consts}, cset))
11.492 + (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
11.493 + frees = (x, M) :: frees, consts = consts}, cset))
11.494 end) |>> curry MRaw t
11.495 | Var _ => (print_g "*** Var"; mterm_unsolvable t)
11.496 - | Bound j => (MRaw (t, nth bounds j), accum)
11.497 - | Abs (s, T, t' as @{const False}) =>
11.498 - let val (M1, a, M2) = mfun_for T bool_T in
11.499 - (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
11.500 - end
11.501 + | Bound j => (MRaw (t, nth bound_Ms j), accum)
11.502 | Abs (s, T, t') =>
11.503 - ((case t' of
11.504 - t1' $ Bound 0 =>
11.505 - if not (loose_bvar1 (t1', 0)) then
11.506 - do_term (incr_boundvars ~1 t1') accum
11.507 - else
11.508 - raise SAME ()
11.509 - | _ => raise SAME ())
11.510 - handle SAME () =>
11.511 - let
11.512 - val M = mtype_for T
11.513 - val (m', accum) = do_term t' (accum |>> push_bound M)
11.514 - in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
11.515 + (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
11.516 + SOME t' =>
11.517 + let
11.518 + val M = mtype_for T
11.519 + val a = V (Unsynchronized.inc max_fresh)
11.520 + val (m', accum) = do_term t' (accum |>> push_bound T M)
11.521 + in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
11.522 + | NONE =>
11.523 + ((case t' of
11.524 + t1' $ Bound 0 =>
11.525 + if not (loose_bvar1 (t1', 0)) then
11.526 + do_term (incr_boundvars ~1 t1') accum
11.527 + else
11.528 + raise SAME ()
11.529 + | _ => raise SAME ())
11.530 + handle SAME () =>
11.531 + let
11.532 + val M = mtype_for T
11.533 + val (m', accum) = do_term t' (accum |>> push_bound T M)
11.534 + in
11.535 + (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
11.536 + end))
11.537 | (t0 as Const (@{const_name All}, _))
11.538 $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
11.539 do_bounded_quantifier t0 s' T' t10 t11 t12 accum
11.540 @@ -872,6 +904,8 @@
11.541 (_, UnsolvableCSet) => mterm_unsolvable t
11.542 | _ =>
11.543 let
11.544 + val T11 = domain_type (fastype_of1 (bound_Ts, t1))
11.545 + val T2 = fastype_of1 (bound_Ts, t2)
11.546 val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
11.547 val M2 = mtype_of_mterm m2
11.548 in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
11.549 @@ -880,18 +914,38 @@
11.550 string_for_mterm ctxt m))
11.551 in do_term end
11.552
11.553 -(* mdata -> styp -> term -> term -> mterm * accumulator *)
11.554 -fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
11.555 +(*
11.556 + accum |> (case a of
11.557 + S Minus => accum
11.558 + | S Plus => unsolvable_accum
11.559 + | V x => do_literal (x, Minus) lits)
11.560 +*)
11.561 +
11.562 +(* int -> mtyp -> accumulator -> accumulator *)
11.563 +fun force_minus_funs 0 _ = I
11.564 + | force_minus_funs n (M as MFun (M1, _, M2)) =
11.565 + add_mtypes_equal M (MFun (M1, S Minus, M2))
11.566 + #> force_minus_funs (n - 1) M2
11.567 + | force_minus_funs _ M =
11.568 + raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
11.569 +(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
11.570 +fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
11.571 let
11.572 val (m1, accum) = consider_term mdata t1 accum
11.573 val (m2, accum) = consider_term mdata t2 accum
11.574 val M1 = mtype_of_mterm m1
11.575 val M2 = mtype_of_mterm m2
11.576 + val accum = accum ||> add_mtypes_equal M1 M2
11.577 val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
11.578 + val m = MApp (MApp (MRaw (Const x,
11.579 + MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
11.580 in
11.581 - (MApp (MApp (MRaw (Const x,
11.582 - MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
11.583 - accum ||> add_mtypes_equal M1 M2)
11.584 + (m, if def then
11.585 + let val (head_m, arg_ms) = strip_mcomb m1 in
11.586 + accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
11.587 + end
11.588 + else
11.589 + accum)
11.590 end
11.591
11.592 (* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
11.593 @@ -912,11 +966,13 @@
11.594 val abs_M = mtype_for abs_T
11.595 val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
11.596 val (body_m, accum) =
11.597 - accum ||> side_cond ? add_mtype_is_right_total abs_M
11.598 - |>> push_bound abs_M |> do_formula sn body_t
11.599 + accum ||> side_cond ? add_mtype_is_complete abs_M
11.600 + |>> push_bound abs_T abs_M |> do_formula sn body_t
11.601 val body_M = mtype_of_mterm body_m
11.602 in
11.603 - (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
11.604 + (MApp (MRaw (Const quant_x,
11.605 + MFun (MFun (abs_M, S Minus, body_M), S Minus,
11.606 + body_M)),
11.607 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
11.608 accum |>> pop_bound)
11.609 end
11.610 @@ -924,7 +980,7 @@
11.611 fun do_equals x t1 t2 =
11.612 case sn of
11.613 Plus => do_term t accum
11.614 - | Minus => consider_general_equals mdata x t1 t2 accum
11.615 + | Minus => consider_general_equals mdata false x t1 t2 accum
11.616 in
11.617 case t of
11.618 Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
11.619 @@ -947,7 +1003,7 @@
11.620 (case sn of
11.621 Plus => do_quantifier x0 s1 T1 t1'
11.622 | Minus =>
11.623 - (* ### do elsewhere *)
11.624 + (* FIXME: Move elsewhere *)
11.625 do_term (@{const Not}
11.626 $ (HOLogic.eq_const (domain_type T0) $ t1
11.627 $ Abs (Name.uu, T1, @{const False}))) accum)
11.628 @@ -981,23 +1037,24 @@
11.629 [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
11.630 val bounteous_consts = [@{const_name bisim}]
11.631
11.632 -(* term -> bool *)
11.633 -fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
11.634 - Term.add_consts t []
11.635 - |> filter_out (is_built_in_const thy stds fast_descrs)
11.636 - |> (forall (member (op =) harmless_consts o original_name o fst)
11.637 - orf exists (member (op =) bounteous_consts o fst))
11.638 +(* mdata -> term -> bool *)
11.639 +fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
11.640 + | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
11.641 + Term.add_consts t []
11.642 + |> filter_out (is_built_in_const thy stds fast_descrs)
11.643 + |> (forall (member (op =) harmless_consts o original_name o fst) orf
11.644 + exists (member (op =) bounteous_consts o fst))
11.645
11.646 (* mdata -> term -> accumulator -> mterm * accumulator *)
11.647 -fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
11.648 - if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
11.649 +fun consider_nondefinitional_axiom mdata t =
11.650 + if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
11.651 else consider_general_formula mdata Plus t
11.652
11.653 (* mdata -> term -> accumulator -> mterm * accumulator *)
11.654 -fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
11.655 +fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
11.656 if not (is_constr_pattern_formula thy t) then
11.657 consider_nondefinitional_axiom mdata t
11.658 - else if is_harmless_axiom hol_ctxt t then
11.659 + else if is_harmless_axiom mdata t then
11.660 pair (MRaw (t, dummy_M))
11.661 else
11.662 let
11.663 @@ -1010,10 +1067,11 @@
11.664 let
11.665 val abs_M = mtype_for abs_T
11.666 val (body_m, accum) =
11.667 - accum |>> push_bound abs_M |> do_formula body_t
11.668 + accum |>> push_bound abs_T abs_M |> do_formula body_t
11.669 val body_M = mtype_of_mterm body_m
11.670 in
11.671 - (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
11.672 + (MApp (MRaw (quant_t,
11.673 + MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
11.674 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
11.675 accum |>> pop_bound)
11.676 end
11.677 @@ -1039,16 +1097,20 @@
11.678 case t of
11.679 (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
11.680 do_all t0 s1 T1 t1 accum
11.681 - | @{const Trueprop} $ t1 => do_formula t1 accum
11.682 + | @{const Trueprop} $ t1 =>
11.683 + let val (m1, accum) = do_formula t1 accum in
11.684 + (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
11.685 + m1), accum)
11.686 + end
11.687 | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
11.688 - consider_general_equals mdata x t1 t2 accum
11.689 + consider_general_equals mdata true x t1 t2 accum
11.690 | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
11.691 | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
11.692 do_conjunction t0 t1 t2 accum
11.693 | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
11.694 do_all t0 s0 T1 t1 accum
11.695 | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
11.696 - consider_general_equals mdata x t1 t2 accum
11.697 + consider_general_equals mdata true x t1 t2 accum
11.698 | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
11.699 | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
11.700 | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
11.701 @@ -1057,8 +1119,7 @@
11.702
11.703 (* Proof.context -> literal list -> term -> mtyp -> string *)
11.704 fun string_for_mtype_of_term ctxt lits t M =
11.705 - Syntax.string_of_term ctxt t ^ " : " ^
11.706 - string_for_mtype (instantiate_mtype lits M)
11.707 + Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
11.708
11.709 (* theory -> literal list -> mtype_context -> unit *)
11.710 fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
11.711 @@ -1067,31 +1128,135 @@
11.712 |> cat_lines |> print_g
11.713
11.714 (* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
11.715 -fun gather f t (ms, accum) =
11.716 +fun amass f t (ms, accum) =
11.717 let val (m, accum) = f t accum in (m :: ms, accum) end
11.718
11.719 -(* hol_context -> bool -> typ -> term list * term list -> bool *)
11.720 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
11.721 - (nondef_ts, def_ts) =
11.722 +(* string -> bool -> hol_context -> bool -> typ -> term list * term list
11.723 + -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
11.724 +fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
11.725 + (nondef_ts, def_ts) =
11.726 let
11.727 - val _ = print_g ("****** Monotonicity analysis: " ^
11.728 + val _ = print_g ("****** " ^ which ^ " analysis: " ^
11.729 string_for_mtype MAlpha ^ " is " ^
11.730 Syntax.string_of_typ ctxt alpha_T)
11.731 - val mdata as {max_fresh, constr_cache, ...} =
11.732 - initial_mdata hol_ctxt binarize alpha_T
11.733 -
11.734 + val mdata as {max_fresh, constr_mcache, ...} =
11.735 + initial_mdata hol_ctxt binarize no_harmless alpha_T
11.736 val accum = (initial_gamma, slack)
11.737 val (nondef_ms, accum) =
11.738 - ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
11.739 - |> fold (gather (consider_nondefinitional_axiom mdata))
11.740 + ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
11.741 + |> fold (amass (consider_nondefinitional_axiom mdata))
11.742 (tl nondef_ts)
11.743 val (def_ms, (gamma, cset)) =
11.744 - ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
11.745 + ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
11.746 in
11.747 case solve (!max_fresh) cset of
11.748 - SOME lits => (print_mtype_context ctxt lits gamma; true)
11.749 - | _ => false
11.750 + SOME lits => (print_mtype_context ctxt lits gamma;
11.751 + SOME (lits, (nondef_ms, def_ms), !constr_mcache))
11.752 + | _ => NONE
11.753 end
11.754 - handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
11.755 + handle MTYPE (loc, Ms, Ts) =>
11.756 + raise BAD (loc, commas (map string_for_mtype Ms @
11.757 + map (Syntax.string_of_typ ctxt) Ts))
11.758 + | MTERM (loc, ms) =>
11.759 + raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
11.760 +
11.761 +(* hol_context -> bool -> typ -> term list * term list -> bool *)
11.762 +val formulas_monotonic = is_some oooo infer "Monotonicity" false
11.763 +
11.764 +(* typ -> typ -> styp *)
11.765 +fun fin_fun_constr T1 T2 =
11.766 + (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
11.767 +
11.768 +(* hol_context -> bool -> (typ option * bool option) list -> typ
11.769 + -> term list * term list -> term list * term list *)
11.770 +fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
11.771 + binarize finitizes alpha_T tsp =
11.772 + case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
11.773 + SOME (lits, msp, constr_mtypes) =>
11.774 + let
11.775 + (* typ -> sign_atom -> bool *)
11.776 + fun should_finitize T a =
11.777 + case triple_lookup (type_match thy) finitizes T of
11.778 + SOME (SOME false) => false
11.779 + | _ => resolve_sign_atom lits a = S Plus
11.780 + (* typ -> mtyp -> typ *)
11.781 + fun type_from_mtype T M =
11.782 + case (M, T) of
11.783 + (MAlpha, _) => T
11.784 + | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
11.785 + Type (if should_finitize T a then @{type_name fin_fun}
11.786 + else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
11.787 + | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
11.788 + Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
11.789 + | (MType _, _) => T
11.790 + | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
11.791 + [M], [T])
11.792 + (* styp -> styp *)
11.793 + fun finitize_constr (x as (s, T)) =
11.794 + (s, case AList.lookup (op =) constr_mtypes x of
11.795 + SOME M => type_from_mtype T M
11.796 + | NONE => T)
11.797 + (* typ list -> mterm -> term *)
11.798 + fun term_from_mterm Ts m =
11.799 + case m of
11.800 + MRaw (t, M) =>
11.801 + let
11.802 + val T = fastype_of1 (Ts, t)
11.803 + val T' = type_from_mtype T M
11.804 + in
11.805 + case t of
11.806 + Const (x as (s, T)) =>
11.807 + if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
11.808 + Const (s, T')
11.809 + else if is_built_in_const thy stds fast_descrs x then
11.810 + coerce_term hol_ctxt Ts T' T t
11.811 + else if is_constr thy stds x then
11.812 + Const (finitize_constr x)
11.813 + else if is_sel s then
11.814 + let
11.815 + val n = sel_no_from_name s
11.816 + val x' = x |> binarized_and_boxed_constr_for_sel hol_ctxt
11.817 + binarize
11.818 + |> finitize_constr
11.819 + val x'' = binarized_and_boxed_nth_sel_for_constr hol_ctxt
11.820 + binarize x' n
11.821 + in Const x'' end
11.822 + else
11.823 + Const (s, T')
11.824 + | Free (s, T) => Free (s, type_from_mtype T M)
11.825 + | Bound _ => t
11.826 + | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
11.827 + [m])
11.828 + end
11.829 + | MAbs (s, T, M, a, m') =>
11.830 + let
11.831 + val T = type_from_mtype T M
11.832 + val t' = term_from_mterm (T :: Ts) m'
11.833 + val T' = fastype_of1 (T :: Ts, t')
11.834 + in
11.835 + Abs (s, T, t')
11.836 + |> should_finitize (T --> T') a
11.837 + ? construct_value thy stds (fin_fun_constr T T') o single
11.838 + end
11.839 + | MApp (m1, m2) =>
11.840 + let
11.841 + val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
11.842 + val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
11.843 + val (t1', T2') =
11.844 + case T1 of
11.845 + Type (s, [T11, T12]) =>
11.846 + (if s = @{type_name fin_fun} then
11.847 + select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 0
11.848 + (T11 --> T12)
11.849 + else
11.850 + t1, T11)
11.851 + | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
11.852 + [T1], [])
11.853 + in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
11.854 + in
11.855 + Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
11.856 + pairself (map (term_from_mterm [])) msp
11.857 + end
11.858 + | NONE => tsp
11.859
11.860 end;
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 08 15:20:40 2010 -0800
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 09:25:23 2010 +0100
12.3 @@ -287,8 +287,9 @@
12.4 "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
12.5 implode (map sub us)
12.6 | Construct (us', T, R, us) =>
12.7 - "Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^
12.8 - " " ^ string_for_rep R ^ " " ^ implode (map sub us)
12.9 + "Construct " ^ implode (map sub us') ^ " " ^
12.10 + Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
12.11 + implode (map sub us)
12.12 | BoundName (j, T, R, nick) =>
12.13 "BoundName " ^ signed_string_of_int j ^ " " ^
12.14 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
12.15 @@ -459,7 +460,8 @@
12.16 (res_T, Const (@{const_name snd}, T --> res_T) $ t)
12.17 end
12.18 (* typ * term -> (typ * term) list *)
12.19 -fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
12.20 +fun factorize (z as (Type (@{type_name "*"}, _), _)) =
12.21 + maps factorize [mk_fst z, mk_snd z]
12.22 | factorize z = [z]
12.23
12.24 (* hol_context -> op2 -> term -> nut *)
12.25 @@ -623,7 +625,8 @@
12.26 if is_built_in_const thy stds false x then Cst (Add, T, Any)
12.27 else ConstName (s, T, Any)
12.28 | (Const (@{const_name minus_class.minus},
12.29 - Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
12.30 + Type (@{type_name fun},
12.31 + [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
12.32 [t1, t2]) =>
12.33 Op2 (SetDifference, T1, Any, sub t1, sub t2)
12.34 | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
12.35 @@ -642,7 +645,8 @@
12.36 else
12.37 do_apply t0 ts
12.38 | (Const (@{const_name ord_class.less_eq},
12.39 - Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
12.40 + Type (@{type_name fun},
12.41 + [Type (@{type_name fun}, [_, @{typ bool}]), _])),
12.42 [t1, t2]) =>
12.43 Op2 (Subset, bool_T, Any, sub t1, sub t2)
12.44 (* FIXME: find out if this case is necessary *)
12.45 @@ -666,7 +670,7 @@
12.46 | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
12.47 | (Const (@{const_name is_unknown}, _), [t1]) =>
12.48 Op1 (IsUnknown, bool_T, Any, sub t1)
12.49 - | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
12.50 + | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
12.51 Op1 (Tha, T2, Any, sub t1)
12.52 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
12.53 | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
12.54 @@ -676,11 +680,13 @@
12.55 T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
12.56 Cst (NatToInt, T, Any)
12.57 | (Const (@{const_name semilattice_inf_class.inf},
12.58 - Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
12.59 + Type (@{type_name fun},
12.60 + [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
12.61 [t1, t2]) =>
12.62 Op2 (Intersect, T1, Any, sub t1, sub t2)
12.63 | (Const (@{const_name semilattice_sup_class.sup},
12.64 - Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
12.65 + Type (@{type_name fun},
12.66 + [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
12.67 [t1, t2]) =>
12.68 Op2 (Union, T1, Any, sub t1, sub t2)
12.69 | (t0 as Const (x as (s, T)), ts) =>
12.70 @@ -956,7 +962,7 @@
12.71 if ok then Cst (Num j, T, Atom (k, j0))
12.72 else Cst (Unrep, T, Opt (Atom (k, j0)))
12.73 end)
12.74 - | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
12.75 + | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
12.76 let val R = Atom (spec_of_type scope T1) in
12.77 Cst (Suc, T, Func (R, Opt R))
12.78 end
12.79 @@ -1306,12 +1312,13 @@
12.80 in (w :: ws, pool, NameTable.update (v, w) table) end
12.81
12.82 (* typ -> rep -> nut list -> nut *)
12.83 -fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us =
12.84 +fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
12.85 + us =
12.86 let val arity1 = arity_of_rep R1 in
12.87 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
12.88 shape_tuple T2 R2 (List.drop (us, arity1))])
12.89 end
12.90 - | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
12.91 + | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
12.92 Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
12.93 | shape_tuple T _ [u] =
12.94 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 08 15:20:40 2010 -0800
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 09:25:23 2010 +0100
13.3 @@ -9,7 +9,9 @@
13.4 sig
13.5 type hol_context = Nitpick_HOL.hol_context
13.6 val preprocess_term :
13.7 - hol_context -> term -> term list * term list * bool * bool * bool
13.8 + hol_context -> (typ option * bool option) list
13.9 + -> (typ option * bool option) list -> term
13.10 + -> term list * term list * bool * bool * bool
13.11 end
13.12
13.13 structure Nitpick_Preproc : NITPICK_PREPROC =
13.14 @@ -17,6 +19,7 @@
13.15
13.16 open Nitpick_Util
13.17 open Nitpick_HOL
13.18 +open Nitpick_Mono
13.19
13.20 (* polarity -> string -> bool *)
13.21 fun is_positive_existential polar quant_s =
13.22 @@ -115,88 +118,15 @@
13.23
13.24 (** Boxing **)
13.25
13.26 -(* hol_context -> typ -> term -> term *)
13.27 -fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
13.28 - (case head_of t of
13.29 - Const x => if is_constr_like thy x then t else raise SAME ()
13.30 - | _ => raise SAME ())
13.31 - handle SAME () =>
13.32 - let
13.33 - val x' as (_, T') =
13.34 - if is_pair_type T then
13.35 - let val (T1, T2) = HOLogic.dest_prodT T in
13.36 - (@{const_name Pair}, T1 --> T2 --> T)
13.37 - end
13.38 - else
13.39 - datatype_constrs hol_ctxt T |> hd
13.40 - val arg_Ts = binder_types T'
13.41 - in
13.42 - list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
13.43 - (index_seq 0 (length arg_Ts)) arg_Ts)
13.44 - end
13.45 -
13.46 -(* (term -> term) -> int -> term -> term *)
13.47 -fun coerce_bound_no f j t =
13.48 - case t of
13.49 - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
13.50 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
13.51 - | Bound j' => if j' = j then f t else t
13.52 - | _ => t
13.53 -(* hol_context -> typ -> typ -> term -> term *)
13.54 -fun coerce_bound_0_in_term hol_ctxt new_T old_T =
13.55 - old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
13.56 -(* hol_context -> typ list -> typ -> typ -> term -> term *)
13.57 -and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
13.58 - if old_T = new_T then
13.59 - t
13.60 - else
13.61 - case (new_T, old_T) of
13.62 - (Type (new_s, new_Ts as [new_T1, new_T2]),
13.63 - Type ("fun", [old_T1, old_T2])) =>
13.64 - (case eta_expand Ts t 1 of
13.65 - Abs (s, _, t') =>
13.66 - Abs (s, new_T1,
13.67 - t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
13.68 - |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
13.69 - |> Envir.eta_contract
13.70 - |> new_s <> "fun"
13.71 - ? construct_value thy stds
13.72 - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
13.73 - o single
13.74 - | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
13.75 - | (Type (new_s, new_Ts as [new_T1, new_T2]),
13.76 - Type (old_s, old_Ts as [old_T1, old_T2])) =>
13.77 - if old_s = @{type_name fun_box} orelse
13.78 - old_s = @{type_name pair_box} orelse old_s = "*" then
13.79 - case constr_expand hol_ctxt old_T t of
13.80 - Const (old_s, _) $ t1 =>
13.81 - if new_s = "fun" then
13.82 - coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
13.83 - else
13.84 - construct_value thy stds
13.85 - (old_s, Type ("fun", new_Ts) --> new_T)
13.86 - [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
13.87 - (Type ("fun", old_Ts)) t1]
13.88 - | Const _ $ t1 $ t2 =>
13.89 - construct_value thy stds
13.90 - (if new_s = "*" then @{const_name Pair}
13.91 - else @{const_name PairBox}, new_Ts ---> new_T)
13.92 - [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
13.93 - coerce_term hol_ctxt Ts new_T2 old_T2 t2]
13.94 - | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
13.95 - else
13.96 - raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
13.97 - | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
13.98 -
13.99 (* hol_context -> bool -> term -> term *)
13.100 fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
13.101 orig_t =
13.102 let
13.103 (* typ -> typ *)
13.104 - fun box_relational_operator_type (Type ("fun", Ts)) =
13.105 - Type ("fun", map box_relational_operator_type Ts)
13.106 - | box_relational_operator_type (Type ("*", Ts)) =
13.107 - Type ("*", map (box_type hol_ctxt InPair) Ts)
13.108 + fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
13.109 + Type (@{type_name fun}, map box_relational_operator_type Ts)
13.110 + | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
13.111 + Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
13.112 | box_relational_operator_type T = T
13.113 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
13.114 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
13.115 @@ -320,12 +250,13 @@
13.116 val T2 = fastype_of1 (new_Ts, t2)
13.117 val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
13.118 in
13.119 - betapply (if s1 = "fun" then
13.120 + betapply (if s1 = @{type_name fun} then
13.121 t1
13.122 else
13.123 select_nth_constr_arg thy stds
13.124 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
13.125 - (Type ("fun", Ts1)), t2)
13.126 + (@{const_name FunBox},
13.127 + Type (@{type_name fun}, Ts1) --> T1) t1 0
13.128 + (Type (@{type_name fun}, Ts1)), t2)
13.129 end
13.130 | t1 $ t2 =>
13.131 let
13.132 @@ -336,12 +267,13 @@
13.133 val T2 = fastype_of1 (new_Ts, t2)
13.134 val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
13.135 in
13.136 - betapply (if s1 = "fun" then
13.137 + betapply (if s1 = @{type_name fun} then
13.138 t1
13.139 else
13.140 select_nth_constr_arg thy stds
13.141 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
13.142 - (Type ("fun", Ts1)), t2)
13.143 + (@{const_name FunBox},
13.144 + Type (@{type_name fun}, Ts1) --> T1) t1 0
13.145 + (Type (@{type_name fun}, Ts1)), t2)
13.146 end
13.147 | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
13.148 | Var (z as (x, T)) =>
13.149 @@ -597,7 +529,7 @@
13.150 if pass1 then do_eq false t2 t1 else raise SAME ()
13.151 else case t1 of
13.152 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
13.153 - | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
13.154 + | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
13.155 if j' = j andalso
13.156 s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
13.157 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
13.158 @@ -1141,8 +1073,8 @@
13.159 (* int -> typ -> accumulator -> accumulator *)
13.160 and add_axioms_for_type depth T =
13.161 case T of
13.162 - Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
13.163 - | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
13.164 + Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
13.165 + | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
13.166 | @{typ prop} => I
13.167 | @{typ bool} => I
13.168 | @{typ unit} => I
13.169 @@ -1399,11 +1331,29 @@
13.170 | _ => t
13.171 in aux "" [] [] end
13.172
13.173 +(** Inference of finite functions **)
13.174 +
13.175 +(* hol_context -> bool -> (typ option * bool option) list
13.176 + -> (typ option * bool option) list -> term list * term list
13.177 + -> term list * term list *)
13.178 +fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
13.179 + (nondef_ts, def_ts) =
13.180 + let
13.181 + val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
13.182 + |> filter_out (fn Type (@{type_name fun_box}, _) => true
13.183 + | T => is_small_finite_type hol_ctxt T orelse
13.184 + triple_lookup (type_match thy) monos T
13.185 + = SOME (SOME false))
13.186 + in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
13.187 +
13.188 (** Preprocessor entry point **)
13.189
13.190 -(* hol_context -> term -> term list * term list * bool * bool * bool *)
13.191 +(* hol_context -> (typ option * bool option) list
13.192 + -> (typ option * bool option) list -> term
13.193 + -> term list * term list * bool * bool * bool *)
13.194 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
13.195 - boxes, skolemize, uncurry, ...}) t =
13.196 + boxes, skolemize, uncurry, ...})
13.197 + finitizes monos t =
13.198 let
13.199 val skolem_depth = if skolemize then 4 else ~1
13.200 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
13.201 @@ -1442,6 +1392,9 @@
13.202 #> Term.map_abs_vars shortest_name
13.203 val nondef_ts = map (do_rest false) nondef_ts
13.204 val def_ts = map (do_rest true) def_ts
13.205 + val (nondef_ts, def_ts) =
13.206 + finitize_all_types_of_funs hol_ctxt binarize finitizes monos
13.207 + (nondef_ts, def_ts)
13.208 in
13.209 (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
13.210 end
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 08 15:20:40 2010 -0800
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Mar 09 09:25:23 2010 +0100
14.3 @@ -158,9 +158,9 @@
14.4 | smart_range_rep _ _ _ (Func (_, R2)) = R2
14.5 | smart_range_rep ofs T ran_card (Opt R) =
14.6 Opt (smart_range_rep ofs T ran_card R)
14.7 - | smart_range_rep ofs (Type ("fun", [_, T2])) _ (Atom (1, _)) =
14.8 + | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
14.9 Atom (1, offset_of_type ofs T2)
14.10 - | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
14.11 + | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
14.12 Atom (ran_card (), offset_of_type ofs T2)
14.13 | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
14.14
14.15 @@ -183,10 +183,10 @@
14.16 | one_rep _ _ (Vect z) = Vect z
14.17 | one_rep ofs T (Opt R) = one_rep ofs T R
14.18 | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
14.19 -fun optable_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
14.20 +fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
14.21 Func (R1, optable_rep ofs T2 R2)
14.22 | optable_rep ofs T R = one_rep ofs T R
14.23 -fun opt_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
14.24 +fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
14.25 Func (R1, opt_rep ofs T2 R2)
14.26 | opt_rep ofs T R = Opt (optable_rep ofs T R)
14.27 (* rep -> rep *)
14.28 @@ -264,11 +264,11 @@
14.29
14.30 (* scope -> typ -> rep *)
14.31 fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
14.32 - (Type ("fun", [T1, T2])) =
14.33 + (Type (@{type_name fun}, [T1, T2])) =
14.34 (case best_one_rep_for_type scope T2 of
14.35 Unit => Unit
14.36 | R2 => Vect (card_of_type card_assigns T1, R2))
14.37 - | best_one_rep_for_type scope (Type ("*", [T1, T2])) =
14.38 + | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
14.39 (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
14.40 (Unit, Unit) => Unit
14.41 | (R1, R2) => Struct [R1, R2])
14.42 @@ -284,12 +284,12 @@
14.43 (* Datatypes are never represented by Unit, because it would confuse
14.44 "nfa_transitions_for_ctor". *)
14.45 (* scope -> typ -> rep *)
14.46 -fun best_opt_set_rep_for_type scope (Type ("fun", [T1, T2])) =
14.47 +fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
14.48 Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
14.49 | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
14.50 opt_rep ofs T (best_one_rep_for_type scope T)
14.51 fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
14.52 - (Type ("fun", [T1, T2])) =
14.53 + (Type (@{type_name fun}, [T1, T2])) =
14.54 (case (best_one_rep_for_type scope T1,
14.55 best_non_opt_set_rep_for_type scope T2) of
14.56 (_, Unit) => Unit
14.57 @@ -302,7 +302,7 @@
14.58 (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
14.59 else best_opt_set_rep_for_type) scope T
14.60 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
14.61 - (Type ("fun", [T1, T2])) =
14.62 + (Type (@{type_name fun}, [T1, T2])) =
14.63 (optable_rep ofs T1 (best_one_rep_for_type scope T1),
14.64 optable_rep ofs T2 (best_one_rep_for_type scope T2))
14.65 | best_non_opt_symmetric_reps_for_fun_type _ T =
14.66 @@ -325,11 +325,11 @@
14.67 fun type_schema_of_rep _ (Formula _) = []
14.68 | type_schema_of_rep _ Unit = []
14.69 | type_schema_of_rep T (Atom _) = [T]
14.70 - | type_schema_of_rep (Type ("*", [T1, T2])) (Struct [R1, R2]) =
14.71 + | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
14.72 type_schema_of_reps [T1, T2] [R1, R2]
14.73 - | type_schema_of_rep (Type ("fun", [_, T2])) (Vect (k, R)) =
14.74 + | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
14.75 replicate_list k (type_schema_of_rep T2 R)
14.76 - | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
14.77 + | type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
14.78 type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
14.79 | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
14.80 | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 08 15:20:40 2010 -0800
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Mar 09 09:25:23 2010 +0100
15.3 @@ -106,22 +106,26 @@
15.4 | NONE => constr_spec dtypes x
15.5
15.6 (* dtype_spec list -> bool -> typ -> bool *)
15.7 -fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
15.8 +fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
15.9 is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
15.10 - | is_complete_type dtypes facto (Type ("*", Ts)) =
15.11 + | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
15.12 + is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
15.13 + | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
15.14 forall (is_complete_type dtypes facto) Ts
15.15 | is_complete_type dtypes facto T =
15.16 not (is_integer_like_type T) andalso not (is_bit_type T) andalso
15.17 fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
15.18 handle Option.Option => true
15.19 -and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
15.20 +and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
15.21 is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
15.22 - | is_concrete_type dtypes facto (Type ("*", Ts)) =
15.23 + | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
15.24 + is_concrete_type dtypes facto T2
15.25 + | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
15.26 forall (is_concrete_type dtypes facto) Ts
15.27 | is_concrete_type dtypes facto T =
15.28 fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
15.29 handle Option.Option => true
15.30 -fun is_exact_type dtypes facto =
15.31 +and is_exact_type dtypes facto =
15.32 is_complete_type dtypes facto andf is_concrete_type dtypes facto
15.33
15.34 (* int Typtab.table -> typ -> int *)
15.35 @@ -528,15 +532,15 @@
15.36
15.37 (* theory -> typ list -> (typ option * int list) list
15.38 -> (typ option * int list) list *)
15.39 -fun repair_cards_assigns_wrt_boxing _ _ [] = []
15.40 - | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
15.41 +fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
15.42 + | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) =
15.43 (if is_fun_type T orelse is_pair_type T then
15.44 - Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
15.45 - |> map (rpair ks o SOME)
15.46 + Ts |> filter (curry (type_match thy o swap) T) |> map (rpair ks o SOME)
15.47 else
15.48 - [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
15.49 - | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
15.50 - (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
15.51 + [(SOME T, ks)]) @
15.52 + repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
15.53 + | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
15.54 + (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
15.55
15.56 val max_scopes = 4096
15.57 val distinct_threshold = 512
15.58 @@ -548,8 +552,8 @@
15.59 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
15.60 deep_dataTs finitizable_dataTs =
15.61 let
15.62 - val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
15.63 - cards_assigns
15.64 + val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts
15.65 + cards_assigns
15.66 val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
15.67 iters_assigns bitss bisim_depths mono_Ts
15.68 nonmono_Ts