--- a/doc-src/Nitpick/nitpick.tex Mon Mar 08 15:20:40 2010 -0800
+++ b/doc-src/Nitpick/nitpick.tex Tue Mar 09 09:25:23 2010 +0100
@@ -136,8 +136,8 @@
suggesting several textual improvements.
% and Perry James for reporting a typo.
-\section{First Steps}
-\label{first-steps}
+\section{Overview}
+\label{overview}
This section introduces Nitpick by presenting small examples. If possible, you
should try out the examples on your workstation. Your theory file should start
@@ -145,7 +145,7 @@
\prew
\textbf{theory}~\textit{Scratch} \\
-\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
+\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
\textbf{begin}
\postw
@@ -677,7 +677,7 @@
\hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
\postw
@@ -704,8 +704,6 @@
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
\postw
-
-
Finally, Nitpick provides rudimentary support for rationals and reals using a
similar approach:
@@ -940,9 +938,10 @@
\label{coinductive-datatypes}
While Isabelle regrettably lacks a high-level mechanism for defining coinductive
-datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
-list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
-these lazy lists seamlessly and provides a hook, described in
+datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
+\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
+``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
+supports these lazy lists seamlessly and provides a hook, described in
\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
datatypes.
@@ -1165,10 +1164,11 @@
{\looseness=-1
Boxing can be enabled or disabled globally or on a per-type basis using the
-\textit{box} option. Moreover, setting the cardinality of a function or
-product type implicitly enables boxing for that type. Nitpick usually performs
-reasonable choices about which types should be boxed, but option tweaking
-sometimes helps.
+\textit{box} option. Nitpick usually performs reasonable choices about which
+types should be boxed, but option tweaking sometimes helps. A related optimization,
+``finalization,'' attempts to wrap functions that constant at all but finitely
+many points (e.g., finite sets); see the documentation for the \textit{finalize}
+option in \S\ref{scope-of-search} for details.
}
@@ -1850,7 +1850,7 @@
The number of options can be overwhelming at first glance. Do not let that worry
you: Nitpick's defaults have been chosen so that it almost always does the right
thing, and the most important options have been covered in context in
-\S\ref{first-steps}.
+\S\ref{overview}.
The descriptions below refer to the following syntactic quantities:
@@ -1936,14 +1936,10 @@
Specifies the sequence of cardinalities to use for a given type.
For free types, and often also for \textbf{typedecl}'d types, it usually makes
sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
-Although function and product types are normally mapped directly to the
-corresponding Kodkod concepts, setting
-the cardinality of such types is also allowed and implicitly enables ``boxing''
-for them, as explained in the description of the \textit{box}~\qty{type}
-and \textit{box} (\S\ref{scope-of-search}) options.
\nopagebreak
-{\small See also \textit{mono} (\S\ref{scope-of-search}).}
+{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
+(\S\ref{scope-of-search}).}
\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
Specifies the default sequence of cardinalities to use. This can be overridden
@@ -2062,8 +2058,8 @@
Specifies whether Nitpick should attempt to wrap (``box'') a given function or
product type in an isomorphic datatype internally. Boxing is an effective mean
to reduce the search space and speed up Nitpick, because the isomorphic datatype
-is approximated by a subset of the possible function or pair values;
-like other drastic optimizations, it can also prevent the discovery of
+is approximated by a subset of the possible function or pair values.
+Like other drastic optimizations, it can also prevent the discovery of
counterexamples. The option can take the following values:
\begin{enum}
@@ -2075,30 +2071,68 @@
higher-order functions are good candidates for boxing.
\end{enum}
-Setting the \textit{card}~\qty{type} option for a function or product type
-implicitly enables boxing for that type.
-
\nopagebreak
-{\small See also \textit{verbose} (\S\ref{output-format})
-and \textit{debug} (\S\ref{output-format}).}
+{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
\opsmart{box}{dont\_box}
Specifies the default boxing setting to use. This can be overridden on a
per-type basis using the \textit{box}~\qty{type} option described above.
+\opargboolorsmart{finitize}{type}{dont\_finitize}
+Specifies whether Nitpick should attempt to finitize a given type, which can be
+a function type or an infinite ``shallow datatype'' (an infinite datatype whose
+constructors don't appear in the problem).
+
+For function types, Nitpick performs a monotonicity analysis to detect functions
+that are constant at all but finitely many points (e.g., finite sets) and treats
+such occurrences specially, thereby increasing the precision. The option can
+then take the following values:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
+\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
+type wherever possible.
+\end{enum}
+
+The semantics of the option is somewhat different for infinite shallow
+datatypes:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
+unsound, counterexamples generated under these conditions are tagged as ``likely
+genuine.''
+\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
+\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
+detect whether the datatype can be safely finitized before finitizing it.
+\end{enum}
+
+Like other drastic optimizations, finitization can sometimes prevent the
+discovery of counterexamples.
+
+\nopagebreak
+{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
+(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
+\textit{debug} (\S\ref{output-format}).}
+
+\opsmart{finitize}{dont\_finitize}
+Specifies the default finitization setting to use. This can be overridden on a
+per-type basis using the \textit{finitize}~\qty{type} option described above.
+
\opargboolorsmart{mono}{type}{non\_mono}
-Specifies whether the given type should be considered monotonic when
-enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
-monotonicity check on the type. Setting this option to \textit{true} can reduce
-the number of scopes tried, but it also diminishes the theoretical chance of
+Specifies whether the given type should be considered monotonic when enumerating
+scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
+performs a monotonicity check on the type. Setting this option to \textit{true}
+can reduce the number of scopes tried, but it can also diminish the chance of
finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
\nopagebreak
{\small See also \textit{card} (\S\ref{scope-of-search}),
+\textit{finitize} (\S\ref{scope-of-search}),
\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
(\S\ref{output-format}).}
-\opsmart{mono}{non\_box}
+\opsmart{mono}{non\_mono}
Specifies the default monotonicity setting to use. This can be overridden on a
per-type basis using the \textit{mono}~\qty{type} option described above.
--- a/doc-src/manual.bib Mon Mar 08 15:20:40 2010 -0800
+++ b/doc-src/manual.bib Tue Mar 09 09:25:23 2010 +0100
@@ -1759,3 +1759,12 @@
key = "Wikipedia",
title = "Wikipedia: {AA} Tree",
note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
+
+@incollection{lochbihler-2010,
+ title = "Coinduction",
+ author = "Andreas Lochbihler",
+ booktitle = "The Archive of Formal Proofs",
+ editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+ publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+ month = "Feb.",
+ year = 2010}
--- a/src/HOL/Nitpick.thy Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Nitpick.thy Tue Mar 09 09:25:23 2010 +0100
@@ -38,8 +38,9 @@
and Quot :: "'a \<Rightarrow> 'b"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
+datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
datatype ('a, 'b) pair_box = PairBox 'a 'b
-datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
typedecl unsigned_bit
typedecl signed_bit
@@ -220,8 +221,8 @@
use "Tools/Nitpick/kodkod_sat.ML"
use "Tools/Nitpick/nitpick_util.ML"
use "Tools/Nitpick/nitpick_hol.ML"
+use "Tools/Nitpick/nitpick_mono.ML"
use "Tools/Nitpick/nitpick_preproc.ML"
-use "Tools/Nitpick/nitpick_mono.ML"
use "Tools/Nitpick/nitpick_scope.ML"
use "Tools/Nitpick/nitpick_peephole.ML"
use "Tools/Nitpick/nitpick_rep.ML"
@@ -236,11 +237,12 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
- wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
- Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
+ bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
+ wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
+ Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
-hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
+hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
+ word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 09:25:23 2010 +0100
@@ -8,7 +8,7 @@
header {* Examples from the Nitpick Manual *}
theory Manual_Nits
-imports Main Coinductive_List Quotient_Product RealDef
+imports Main Quotient_Product RealDef
begin
chapter {* 3. First Steps *}
@@ -173,13 +173,35 @@
subsection {* 3.9. Coinductive Datatypes *}
+(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
+we cannot rely on its presence, we expediently provide our own axiomatization.
+The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
+
+typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
+
+definition LNil where "LNil = Abs_llist (Inl [])"
+definition LCons where
+"LCons y ys = Abs_llist (case Rep_llist ys of
+ Inl ys' \<Rightarrow> Inl (y # ys')
+ | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
+
+axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
+
+lemma iterates_def [nitpick_simp]:
+"iterates f a = LCons a (iterates f (f a))"
+sorry
+
+setup {*
+Nitpick.register_codatatype @{typ "'a llist"} ""
+ (map dest_Const [@{term LNil}, @{term LCons}])
+*}
+
lemma "xs \<noteq> LCons a xs"
nitpick
oops
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
nitpick [verbose]
-nitpick [bisim_depth = -1, verbose]
oops
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Mar 09 09:25:23 2010 +0100
@@ -36,8 +36,10 @@
datatype rep = SRep | RRep
(* Proof.context -> typ -> unit *)
-fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
- | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts
+fun check_type ctxt (Type (@{type_name fun}, Ts)) =
+ List.app (check_type ctxt) Ts
+ | check_type ctxt (Type (@{type_name "*"}, Ts)) =
+ List.app (check_type ctxt) Ts
| check_type _ @{typ bool} = ()
| check_type _ (TFree (_, @{sort "{}"})) = ()
| check_type _ (TFree (_, @{sort HOL.type})) = ()
@@ -45,13 +47,14 @@
raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
(* rep -> (typ -> int) -> typ -> int list *)
-fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =
+fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
replicate_list (card T1) (atom_schema_of SRep card T2)
- | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =
+ | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
atom_schema_of SRep card T1
- | atom_schema_of RRep card (Type ("fun", [T1, T2])) =
+ | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
- | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts
+ | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
+ maps (atom_schema_of SRep card) Ts
| atom_schema_of _ card T = [card T]
(* rep -> (typ -> int) -> typ -> int *)
val arity_of = length ooo atom_schema_of
@@ -89,7 +92,7 @@
fun kodkod_formula_from_term ctxt card frees =
let
(* typ -> rel_expr -> rel_expr *)
- fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
+ fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
let
val jss = atom_schema_of SRep card T1 |> map (rpair 0)
|> all_combinations
@@ -100,7 +103,7 @@
(index_seq 0 (length jss)) jss
|> foldl1 Union
end
- | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =
+ | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
let
val jss = atom_schema_of SRep card T1 |> map (rpair 0)
|> all_combinations
@@ -115,7 +118,7 @@
end
| R_rep_from_S_rep _ r = r
(* typ list -> typ -> rel_expr -> rel_expr *)
- fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =
+ fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
Comprehension (decls_for SRep card Ts T,
RelEq (R_rep_from_S_rep T
(rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
@@ -137,7 +140,9 @@
| Const (@{const_name "op ="}, _) $ t1 $ t2 =>
RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name ord_class.less_eq},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
Subset (to_R_rep Ts t1, to_R_rep Ts t2)
| @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
| @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
@@ -179,7 +184,8 @@
| Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name ord_class.less_eq},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name ord_class.less_eq}, _) =>
to_R_rep Ts (eta_expand Ts t 2)
@@ -190,7 +196,7 @@
| @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
| @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name bot_class.bot},
- T as Type ("fun", [_, @{typ bool}])) =>
+ T as Type (@{type_name fun}, [_, @{typ bool}])) =>
empty_n_ary_rel (arity_of RRep card T)
| Const (@{const_name insert}, _) $ t1 $ t2 =>
Union (to_S_rep Ts t1, to_R_rep Ts t2)
@@ -203,27 +209,35 @@
raise NOT_SUPPORTED "transitive closure for function or pair type"
| Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name semilattice_inf_class.inf},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name semilattice_inf_class.inf}, _) =>
to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name semilattice_sup_class.sup},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
Union (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name semilattice_sup_class.sup}, _) =>
to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name minus_class.minus},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ $ t1 $ t2 =>
Difference (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name minus_class.minus},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name minus_class.minus},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
| Const (@{const_name Pair}, _) $ _ => raise SAME ()
@@ -277,7 +291,8 @@
end
(* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
-fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =
+fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
+ r =
if body_type T2 = bool_T then
True
else
@@ -294,8 +309,9 @@
let
val thy = ProofContext.theory_of ctxt
(* typ -> int *)
- fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
- | card (Type ("*", [T1, T2])) = card T1 * card T2
+ fun card (Type (@{type_name fun}, [T1, T2])) =
+ reasonable_power (card T2) (card T1)
+ | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
| card @{typ bool} = 2
| card T = Int.max (1, raw_card T)
val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 09:25:23 2010 +0100
@@ -15,6 +15,7 @@
bitss: int list,
bisim_depths: int list,
boxes: (typ option * bool option) list,
+ finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
@@ -87,6 +88,7 @@
bitss: int list,
bisim_depths: int list,
boxes: (typ option * bool option) list,
+ finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
@@ -200,13 +202,13 @@
error "You must import the theory \"Nitpick\" to use Nitpick"
*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
- boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
- user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
- specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
- peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
- max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
- max_potential, max_genuine, check_potential, check_genuine, batch_size,
- ...} =
+ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
+ verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
+ destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
+ fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
+ flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
+ evals, formats, max_potential, max_genuine, check_potential,
+ check_genuine, batch_size, ...} =
params
val state_ref = Unsynchronized.ref state
(* Pretty.T -> unit *)
@@ -289,7 +291,7 @@
val _ = null (Term.add_tvars assms_t []) orelse
raise NOT_SUPPORTED "schematic type variables"
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
- binarize) = preprocess_term hol_ctxt assms_t
+ binarize) = preprocess_term hol_ctxt finitizes monos assms_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -321,7 +323,11 @@
fold add_free_and_const_names (nondef_us @ def_us) ([], [])
val (sel_names, nonsel_names) =
List.partition (is_sel o nickname_of) const_names
- val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
+ val sound_finitizes =
+ none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
+ | _ => false) finitizes)
+ val genuine_means_genuine =
+ got_all_user_axioms andalso none_true wfs andalso sound_finitizes
val standard = forall snd stds
(*
val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
@@ -340,21 +346,30 @@
". " ^ extra
end
(* typ -> bool *)
- fun is_type_always_monotonic T =
+ fun is_type_fundamentally_monotonic T =
(is_datatype thy stds T andalso not (is_quot_type thy T) andalso
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_actually_monotonic T =
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
+ fun is_type_kind_of_monotonic T =
+ case triple_lookup (type_match thy) monos T of
+ SOME (SOME false) => false
+ | _ => is_type_actually_monotonic T
fun is_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
- | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
- fun is_type_finitizable T =
- case triple_lookup (type_match thy) monos T of
- SOME (SOME false) => false
- | _ => is_type_actually_monotonic T
+ | _ => is_type_fundamentally_monotonic T orelse
+ is_type_actually_monotonic T
+ fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
+ is_type_kind_of_monotonic T
+ | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
+ is_type_kind_of_monotonic T
+ | is_shallow_datatype_finitizable T =
+ case triple_lookup (type_match thy) finitizes T of
+ SOME (SOME b) => b
+ | _ => is_type_kind_of_monotonic T
fun is_datatype_deep T =
not standard orelse T = nat_T orelse is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names
@@ -371,7 +386,7 @@
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
val _ =
if verbose andalso not unique_scope then
- case filter_out is_type_always_monotonic mono_Ts of
+ case filter_out is_type_fundamentally_monotonic mono_Ts of
[] => ()
| interesting_mono_Ts =>
print_v (K (monotonicity_message interesting_mono_Ts
@@ -382,7 +397,7 @@
all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
val finitizable_dataTs =
shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
- |> filter is_type_finitizable
+ |> filter is_shallow_datatype_finitizable
val _ =
if verbose andalso not (null finitizable_dataTs) then
print_v (K (monotonicity_message finitizable_dataTs
@@ -649,6 +664,8 @@
? cons ("user_axioms", "\"true\"")
|> not (none_true wfs)
? cons ("wf", "\"smart\" or \"false\"")
+ |> not sound_finitizes
+ ? cons ("finitize", "\"smart\" or \"false\"")
|> not codatatypes_ok
? cons ("bisim_depth", "a nonnegative value")
val ss =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 09:25:23 2010 +0100
@@ -65,8 +65,8 @@
val strip_any_connective : term -> term list * term
val conjuncts_of : term -> term list
val disjuncts_of : term -> term list
- val unarize_and_unbox_type : typ -> typ
- val unarize_unbox_and_uniterize_type : typ -> typ
+ val unarize_unbox_etc_type : typ -> typ
+ val uniterize_unarize_unbox_etc_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
val shortest_name : string -> string
@@ -148,11 +148,13 @@
theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
val construct_value :
theory -> (typ option * bool) list -> styp -> term list -> term
+ val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_exact_card_of_type :
hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
val is_finite_type : hol_context -> typ -> bool
+ val is_small_finite_type : hol_context -> typ -> bool
val special_bounds : term list -> (indexname * typ) list
val abs_var : indexname * typ -> term -> term
val is_funky_typedef : theory -> typ -> bool
@@ -401,22 +403,24 @@
| unarize_type @{typ "signed_bit word"} = int_T
| unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
| unarize_type T = T
-fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
- unarize_and_unbox_type (Type ("fun", Ts))
- | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
- Type ("*", map unarize_and_unbox_type Ts)
- | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
- | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
- | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
- Type (s, map unarize_and_unbox_type Ts)
- | unarize_and_unbox_type T = T
+fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
+ unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
+ | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
+ unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
+ | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
+ Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
+ | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
+ | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
+ | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
+ Type (s, map unarize_unbox_etc_type Ts)
+ | unarize_unbox_etc_type T = T
fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
| uniterize_type @{typ bisim_iterator} = nat_T
| uniterize_type T = T
-val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
+val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
(* Proof.context -> typ -> string *)
-fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
+fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
@@ -439,9 +443,10 @@
#> map_types shorten_names_in_type
(* theory -> typ * typ -> bool *)
-fun type_match thy (T1, T2) =
+fun strict_type_match thy (T1, T2) =
(Sign.typ_match thy (T2, T1) Vartab.empty; true)
handle Type.TYPE_MATCH => false
+fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
(* theory -> styp * styp -> bool *)
fun const_match thy ((s1, T1), (s2, T2)) =
s1 = s2 andalso type_match thy (T1, T2)
@@ -454,14 +459,14 @@
(* typ -> bool *)
fun is_TFree (TFree _) = true
| is_TFree _ = false
-fun is_higher_order_type (Type ("fun", _)) = true
+fun is_higher_order_type (Type (@{type_name fun}, _)) = true
| is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
| is_higher_order_type _ = false
-fun is_fun_type (Type ("fun", _)) = true
+fun is_fun_type (Type (@{type_name fun}, _)) = true
| is_fun_type _ = false
-fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
+fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
| is_set_type _ = false
-fun is_pair_type (Type ("*", _)) = true
+fun is_pair_type (Type (@{type_name "*"}, _)) = true
| is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
| is_lfp_iterator_type _ = false
@@ -494,19 +499,20 @@
(* int -> typ -> typ list * typ *)
fun strip_n_binders 0 T = ([], T)
- | strip_n_binders n (Type ("fun", [T1, T2])) =
+ | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
strip_n_binders (n - 1) T2 |>> cons T1
| strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
- strip_n_binders n (Type ("fun", Ts))
+ strip_n_binders n (Type (@{type_name fun}, Ts))
| strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
(* typ -> typ *)
val nth_range_type = snd oo strip_n_binders
(* typ -> int *)
-fun num_factors_in_type (Type ("*", [T1, T2])) =
+fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
fold (Integer.add o num_factors_in_type) [T1, T2] 0
| num_factors_in_type _ = 1
-fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
+fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
+ 1 + num_binder_types T2
| num_binder_types _ = 0
(* typ -> typ list *)
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
@@ -515,7 +521,7 @@
(* typ -> term list -> term *)
fun mk_flat_tuple _ [t] = t
- | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
+ | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
| mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
(* int -> term -> term list *)
@@ -595,7 +601,7 @@
val (co_s, co_Ts) = dest_Type co_T
val _ =
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
- co_s <> "fun" andalso
+ co_s <> @{type_name fun} andalso
not (is_basic_datatype thy [(NONE, true)] co_s) then
()
else
@@ -669,7 +675,7 @@
find_index (curry (op =) s o fst)
(Record.get_extT_fields thy T1 ||> single |> op @)
(* theory -> styp -> bool *)
-fun is_record_get thy (s, Type ("fun", [T1, _])) =
+fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
exists (curry (op =) s o fst) (all_record_fields thy T1)
| is_record_get _ _ = false
fun is_record_update thy (s, T) =
@@ -677,30 +683,33 @@
exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
-fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
+fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
(case typedef_info thy s' of
SOME {Abs_name, ...} => s = Abs_name
| NONE => false)
| is_abs_fun _ _ = false
-fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
+fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
(case typedef_info thy s' of
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
+fun is_quot_abs_fun ctxt
+ (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
(try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
= SOME (Const x))
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
+fun is_quot_rep_fun ctxt
+ (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
(try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
= SOME (Const x))
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
-fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
+fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
+ [T1 as Type (s', _), T2]))) =
(case typedef_info thy s' of
- SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
+ SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
(* theory -> typ -> typ *)
@@ -729,10 +738,10 @@
end
handle TYPE ("dest_Type", _, _) => false
fun is_constr_like thy (s, T) =
- member (op =) [@{const_name FunBox}, @{const_name PairBox},
- @{const_name Quot}, @{const_name Zero_Rep},
- @{const_name Suc_Rep}] s orelse
- let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
+ member (op =) [@{const_name FinFun}, @{const_name FunBox},
+ @{const_name PairBox}, @{const_name Quot},
+ @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
+ let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
is_coconstr thy x
@@ -749,8 +758,8 @@
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
- String.isPrefix sel_prefix
- orf (member (op =) [@{const_name fst}, @{const_name snd}])
+ String.isPrefix sel_prefix orf
+ (member (op =) [@{const_name fst}, @{const_name snd}])
(* boxability -> boxability *)
fun in_fun_lhs_for InConstr = InSel
@@ -763,10 +772,10 @@
(* hol_context -> boxability -> typ -> bool *)
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
case T of
- Type ("fun", _) =>
+ Type (@{type_name fun}, _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
not (is_boolean_type (body_type T))
- | Type ("*", Ts) =>
+ | Type (@{type_name "*"}, Ts) =>
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
((boxy = InExpr orelse boxy = InFunLHS) andalso
exists (is_boxing_worth_it hol_ctxt InPair)
@@ -780,7 +789,7 @@
(* hol_context -> boxability -> typ -> typ *)
and box_type hol_ctxt boxy T =
case T of
- Type (z as ("fun", [T1, T2])) =>
+ Type (z as (@{type_name fun}, [T1, T2])) =>
if boxy <> InConstr andalso boxy <> InSel andalso
should_box_type hol_ctxt boxy z then
Type (@{type_name fun_box},
@@ -788,12 +797,13 @@
else
box_type hol_ctxt (in_fun_lhs_for boxy) T1
--> box_type hol_ctxt (in_fun_rhs_for boxy) T2
- | Type (z as ("*", Ts)) =>
+ | Type (z as (@{type_name "*"}, Ts)) =>
if boxy <> InConstr andalso boxy <> InSel
andalso should_box_type hol_ctxt boxy z then
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
else
- Type ("*", map (box_type hol_ctxt
+ Type (@{type_name "*"},
+ map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
| _ => T
@@ -979,7 +989,7 @@
else
let
(* int -> typ -> int * term *)
- fun aux m (Type ("*", [T1, T2])) =
+ fun aux m (Type (@{type_name "*"}, [T1, T2])) =
let
val (m, t1) = aux m T1
val (m, t2) = aux m T2
@@ -1018,10 +1028,85 @@
| _ => list_comb (Const x, args)
end
+(* hol_context -> typ -> term -> term *)
+fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
+ (case head_of t of
+ Const x => if is_constr_like thy x then t else raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let
+ val x' as (_, T') =
+ if is_pair_type T then
+ let val (T1, T2) = HOLogic.dest_prodT T in
+ (@{const_name Pair}, T1 --> T2 --> T)
+ end
+ else
+ datatype_constrs hol_ctxt T |> hd
+ val arg_Ts = binder_types T'
+ in
+ list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
+ (index_seq 0 (length arg_Ts)) arg_Ts)
+ end
+
+(* (term -> term) -> int -> term -> term *)
+fun coerce_bound_no f j t =
+ case t of
+ t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+ | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+ | Bound j' => if j' = j then f t else t
+ | _ => t
+(* hol_context -> typ -> typ -> term -> term *)
+fun coerce_bound_0_in_term hol_ctxt new_T old_T =
+ old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
+(* hol_context -> typ list -> typ -> typ -> term -> term *)
+and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+ if old_T = new_T then
+ t
+ else
+ case (new_T, old_T) of
+ (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type (@{type_name fun}, [old_T1, old_T2])) =>
+ (case eta_expand Ts t 1 of
+ Abs (s, _, t') =>
+ Abs (s, new_T1,
+ t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
+ |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
+ |> Envir.eta_contract
+ |> new_s <> @{type_name fun}
+ ? construct_value thy stds
+ (if new_s = @{type_name fin_fun} then @{const_name FinFun}
+ else @{const_name FunBox},
+ Type (@{type_name fun}, new_Ts) --> new_T)
+ o single
+ | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
+ | (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type (old_s, old_Ts as [old_T1, old_T2])) =>
+ if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
+ old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
+ case constr_expand hol_ctxt old_T t of
+ Const (old_s, _) $ t1 =>
+ if new_s = @{type_name fun} then
+ coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
+ else
+ construct_value thy stds
+ (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
+ [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
+ (Type (@{type_name fun}, old_Ts)) t1]
+ | Const _ $ t1 $ t2 =>
+ construct_value thy stds
+ (if new_s = @{type_name "*"} then @{const_name Pair}
+ else @{const_name PairBox}, new_Ts ---> new_T)
+ (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
+ [t1, t2])
+ | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
+ else
+ raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
+ | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
+
(* (typ * int) list -> typ -> int *)
-fun card_of_type assigns (Type ("fun", [T1, T2])) =
+fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
- | card_of_type assigns (Type ("*", [T1, T2])) =
+ | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
card_of_type assigns T1 * card_of_type assigns T2
| card_of_type _ (Type (@{type_name itself}, _)) = 1
| card_of_type _ @{typ prop} = 2
@@ -1033,7 +1118,8 @@
| NONE => if T = @{typ bisim_iterator} then 0
else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
(* int -> (typ * int) list -> typ -> int *)
-fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
+fun bounded_card_of_type max default_card assigns
+ (Type (@{type_name fun}, [T1, T2])) =
let
val k1 = bounded_card_of_type max default_card assigns T1
val k2 = bounded_card_of_type max default_card assigns T2
@@ -1041,7 +1127,8 @@
if k1 = max orelse k2 = max then max
else Int.min (max, reasonable_power k2 k1)
end
- | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
+ | bounded_card_of_type max default_card assigns
+ (Type (@{type_name "*"}, [T1, T2])) =
let
val k1 = bounded_card_of_type max default_card assigns T1
val k2 = bounded_card_of_type max default_card assigns T2
@@ -1064,7 +1151,7 @@
else if member (op =) finitizable_dataTs T then
raise SAME ()
else case T of
- Type ("fun", [T1, T2]) =>
+ Type (@{type_name fun}, [T1, T2]) =>
let
val k1 = aux avoid T1
val k2 = aux avoid T2
@@ -1073,7 +1160,7 @@
else if k1 >= max orelse k2 >= max then max
else Int.min (max, reasonable_power k2 k1)
end
- | Type ("*", [T1, T2]) =>
+ | Type (@{type_name "*"}, [T1, T2]) =>
let
val k1 = aux avoid T1
val k2 = aux avoid T2
@@ -1104,9 +1191,16 @@
AList.lookup (op =) assigns T |> the_default default_card
in Int.min (max, aux [] T) end
+val small_type_max_card = 5
+
(* hol_context -> typ -> bool *)
fun is_finite_type hol_ctxt T =
- bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
+ bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
+(* hol_context -> typ -> bool *)
+fun is_small_finite_type hol_ctxt T =
+ let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
+ n > 0 andalso n <= small_type_max_card
+ end
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -1144,7 +1238,8 @@
is_typedef_axiom thy boring t2
| is_typedef_axiom thy boring
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
- $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
+ $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
+ $ Const _ $ _)) =
boring <> is_funky_typedef_name thy s andalso is_typedef thy s
| is_typedef_axiom _ _ _ = false
@@ -1538,8 +1633,8 @@
fun is_inductive_pred hol_ctxt =
is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
fun is_equational_fun hol_ctxt =
- (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
- orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
+ (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
+ (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
(* term * term -> term *)
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1586,7 +1681,7 @@
fun do_term depth Ts t =
case t of
(t0 as Const (@{const_name Int.number_class.number_of},
- Type ("fun", [_, ran_T]))) $ t1 =>
+ Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
((if is_number_type thy ran_T then
let
val j = t1 |> HOLogic.dest_numeral
@@ -1612,7 +1707,7 @@
betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
map (do_term depth Ts) [t1, t2])
| Const (x as (@{const_name distinct},
- Type ("fun", [Type (@{type_name list}, [T']), _])))
+ Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
$ (t1 as _ $ _) =>
(t1 |> HOLogic.dest_list |> distinctness_formula T'
handle TERM _ => do_const depth Ts t x [t1])
@@ -1969,7 +2064,7 @@
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
val set_T = tuple_T --> bool_T
val curried_T = tuple_T --> set_T
- val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
+ val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
@@ -2092,8 +2187,8 @@
let
fun aux T accum =
case T of
- Type ("fun", Ts) => fold aux Ts accum
- | Type ("*", Ts) => fold aux Ts accum
+ Type (@{type_name fun}, Ts) => fold aux Ts accum
+ | Type (@{type_name "*"}, Ts) => fold aux Ts accum
| Type (@{type_name itself}, [T1]) => aux T1 accum
| Type (_, Ts) =>
if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
@@ -2161,7 +2256,7 @@
(* int list -> int list -> typ -> typ *)
fun format_type default_format format T =
let
- val T = unarize_unbox_and_uniterize_type T
+ val T = uniterize_unarize_unbox_etc_type T
val format = format |> filter (curry (op <) 0)
in
if forall (curry (op =) 1) format then
@@ -2200,7 +2295,7 @@
(* term -> term *)
val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
val (x' as (_, T'), js, ts) =
- AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
+ AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
|> the_single
val max_j = List.last js
val Ts = List.take (binder_types T', max_j + 1)
@@ -2294,7 +2389,7 @@
let val t = Const (original_name s, T) in
(t, format_term_type thy def_table formats t)
end)
- |>> map_types unarize_unbox_and_uniterize_type
+ |>> map_types uniterize_unarize_unbox_etc_type
|>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Mar 09 09:25:23 2010 +0100
@@ -39,6 +39,7 @@
("bits", ["1,2,3,4,6,8,10,12"]),
("bisim_depth", ["7"]),
("box", ["smart"]),
+ ("finitize", ["smart"]),
("mono", ["smart"]),
("std", ["true"]),
("wf", ["smart"]),
@@ -78,6 +79,7 @@
val negated_params =
[("dont_box", "box"),
+ ("dont_finitize", "finitize"),
("non_mono", "mono"),
("non_std", "std"),
("non_wf", "wf"),
@@ -111,8 +113,8 @@
AList.defined (op =) negated_params s orelse
s = "max" orelse s = "eval" orelse s = "expect" orelse
exists (fn p => String.isPrefix (p ^ " ") s)
- ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
- "non_std", "wf", "non_wf", "format"]
+ ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
@@ -297,14 +299,8 @@
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
val bitss = lookup_int_seq "bits" 1
val bisim_depths = lookup_int_seq "bisim_depth" ~1
- val boxes =
- lookup_bool_option_assigns read_type_polymorphic "box" @
- map_filter (fn (SOME T, _) =>
- if is_fun_type T orelse is_pair_type T then
- SOME (SOME T, SOME true)
- else
- NONE
- | (NONE, _) => NONE) cards_assigns
+ val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
+ val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
val stds = lookup_bool_assigns read_type_polymorphic "std"
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
@@ -349,8 +345,8 @@
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
- boxes = boxes, monos = monos, stds = stds, wfs = wfs,
- sat_solver = sat_solver, blocking = blocking, falsify = falsify,
+ boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
+ wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
debug = debug, verbose = verbose, overlord = overlord,
user_axioms = user_axioms, assms = assms,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 09:25:23 2010 +0100
@@ -301,8 +301,8 @@
(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
fun bound_for_sel_rel ctxt debug dtypes
- (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
- nick)) =
+ (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
+ R as Func (Atom (_, j0), R2), nick)) =
let
val {delta, epsilon, exclusive, explicit_max, ...} =
constr_spec dtypes (original_name nick, T1)
@@ -1208,7 +1208,7 @@
(rel_expr_from_rel_expr kk min_R R2 r2))
end
| Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
- | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
+ | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
| Cst (Num j, T, R) =>
if is_word_type T then
@@ -1229,36 +1229,36 @@
| Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
| Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
- | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
- | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
- | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
+ | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
+ | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
- | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
to_bit_word_binary_op T R
(SOME (fn i1 => fn i2 => fn i3 =>
kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
(KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
(SOME (curry KK.Add))
- | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
+ | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>
KK.Rel nat_subtract_rel
- | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
+ | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>
KK.Rel int_subtract_rel
- | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
to_bit_word_binary_op T R NONE
(SOME (fn i1 => fn i2 =>
KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
- | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
to_bit_word_binary_op T R
(SOME (fn i1 => fn i2 => fn i3 =>
kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
(KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
(SOME (curry KK.Sub))
- | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
+ | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>
KK.Rel nat_multiply_rel
- | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
+ | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>
KK.Rel int_multiply_rel
| Cst (Multiply,
- T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
+ T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>
to_bit_word_binary_op T R
(SOME (fn i1 => fn i2 => fn i3 =>
kk_or (KK.IntEq (i2, KK.Num 0))
@@ -1267,14 +1267,14 @@
? kk_and (KK.LE (KK.Num 0,
foldl1 KK.BitAnd [i1, i2, i3])))))
(SOME (curry KK.Mult))
- | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
- | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
- | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
+ | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel
+ | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
to_bit_word_binary_op T R NONE
(SOME (fn i1 => fn i2 =>
KK.IntIf (KK.IntEq (i2, KK.Num 0),
KK.Num 0, KK.Div (i1, i2))))
- | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
to_bit_word_binary_op T R
(SOME (fn i1 => fn i2 => fn i3 =>
KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
@@ -1293,9 +1293,9 @@
| Cst (Fracs, _, Func (Struct _, _)) =>
kk_project_seq (KK.Rel norm_frac_rel) 2 2
| Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
- | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
+ | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>
KK.Iden
- | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
+ | Cst (NatToInt, Type (_, [@{typ nat}, _]),
Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
if nat_j0 = int_j0 then
kk_intersect KK.Iden
@@ -1303,9 +1303,9 @@
KK.Univ)
else
raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
- | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
to_bit_word_unary_op T R I
- | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
+ | Cst (IntToNat, Type (_, [@{typ int}, _]),
Func (Atom (int_k, int_j0), nat_R)) =>
let
val abs_card = max_int_for_card int_k + 1
@@ -1321,7 +1321,7 @@
else
raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
end
- | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
to_bit_word_unary_op T R
(fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
| Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 09 09:25:23 2010 +0100
@@ -110,48 +110,53 @@
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
(* term -> term *)
-fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
- unarize_and_unbox_term t1
- | unarize_and_unbox_term (Const (@{const_name PairBox},
- Type ("fun", [T1, Type ("fun", [T2, _])]))
- $ t1 $ t2) =
- let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
- Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
- $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
+fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
+ unarize_unbox_etc_term t1
+ | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
+ unarize_unbox_etc_term t1
+ | unarize_unbox_etc_term
+ (Const (@{const_name PairBox},
+ Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
+ $ t1 $ t2) =
+ let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
+ Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
+ $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
end
- | unarize_and_unbox_term (Const (s, T)) =
- Const (s, unarize_unbox_and_uniterize_type T)
- | unarize_and_unbox_term (t1 $ t2) =
- unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
- | unarize_and_unbox_term (Free (s, T)) =
- Free (s, unarize_unbox_and_uniterize_type T)
- | unarize_and_unbox_term (Var (x, T)) =
- Var (x, unarize_unbox_and_uniterize_type T)
- | unarize_and_unbox_term (Bound j) = Bound j
- | unarize_and_unbox_term (Abs (s, T, t')) =
- Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
+ | unarize_unbox_etc_term (Const (s, T)) =
+ Const (s, uniterize_unarize_unbox_etc_type T)
+ | unarize_unbox_etc_term (t1 $ t2) =
+ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
+ | unarize_unbox_etc_term (Free (s, T)) =
+ Free (s, uniterize_unarize_unbox_etc_type T)
+ | unarize_unbox_etc_term (Var (x, T)) =
+ Var (x, uniterize_unarize_unbox_etc_type T)
+ | unarize_unbox_etc_term (Bound j) = Bound j
+ | unarize_unbox_etc_term (Abs (s, T, t')) =
+ Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
(* typ -> typ -> (typ * typ) * (typ * typ) *)
-fun factor_out_types (T1 as Type ("*", [T11, T12]))
- (T2 as Type ("*", [T21, T22])) =
+fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
+ (T2 as Type (@{type_name "*"}, [T21, T22])) =
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
if n1 = n2 then
let
val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
in
- ((Type ("*", [T11, T11']), opt_T12'),
- (Type ("*", [T21, T21']), opt_T22'))
+ ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
+ (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
end
else if n1 < n2 then
case factor_out_types T1 T21 of
(p1, (T21', NONE)) => (p1, (T21', SOME T22))
| (p1, (T21', SOME T22')) =>
- (p1, (T21', SOME (Type ("*", [T22', T22]))))
+ (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
else
swap (factor_out_types T2 T1)
end
- | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
- | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
+ | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
+ ((T11, SOME T12), (T2, NONE))
+ | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
+ ((T1, NONE), (T21, SOME T22))
| factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
(* bool -> typ -> typ -> (term * term) list -> term *)
@@ -188,10 +193,11 @@
val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
(* typ -> term -> term -> term *)
-fun pair_up (Type ("*", [T1', T2']))
+fun pair_up (Type (@{type_name "*"}, [T1', T2']))
(t1 as Const (@{const_name Pair},
- Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
- t2 =
+ Type (@{type_name fun},
+ [_, Type (@{type_name fun}, [_, T1])]))
+ $ t11 $ t12) t2 =
if T1 = T1' then HOLogic.mk_prod (t1, t2)
else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
| pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
@@ -199,7 +205,7 @@
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
(* typ -> typ -> typ -> term -> term *)
-fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
+fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
let
(* typ -> typ -> typ -> typ -> term -> term *)
fun do_curry T1 T1a T1b T2 t =
@@ -238,9 +244,11 @@
t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
| _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
(* typ -> typ -> term -> term *)
- and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
+ and do_term (Type (@{type_name fun}, [T1', T2']))
+ (Type (@{type_name fun}, [T1, T2])) t =
do_fun T1' T2' T1 T2 t
- | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
+ | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
+ (Type (@{type_name "*"}, [T1, T2]))
(Const (@{const_name Pair}, _) $ t1 $ t2) =
Const (@{const_name Pair}, Ts' ---> T')
$ do_term T1' T1 t1 $ do_term T2' T2 t2
@@ -257,7 +265,7 @@
| truth_const_sort_key _ = "1"
(* typ -> term list -> term *)
-fun mk_tuple (Type ("*", [T1, T2])) ts =
+fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
HOLogic.mk_prod (mk_tuple T1 ts,
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
| mk_tuple _ (t :: _) = t
@@ -307,8 +315,8 @@
else
aux tps
end
- (* typ -> typ -> typ -> (term * term) list -> term *)
- fun make_map T1 T2 T2' =
+ (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
+ fun make_map maybe_opt T1 T2 T2' =
let
val update_const = Const (@{const_name fun_upd},
(T1 --> T2) --> T1 --> T2 --> T1 --> T2)
@@ -319,7 +327,7 @@
Const (@{const_name None}, _) => aux' ps
| _ => update_const $ aux' ps $ t1 $ t2)
fun aux ps =
- if not (is_complete_type datatypes false T1) then
+ if maybe_opt andalso not (is_complete_type datatypes false T1) then
update_const $ aux' ps $ Const (unrep, T1)
$ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
else
@@ -328,7 +336,7 @@
(* typ list -> term -> term *)
fun polish_funs Ts t =
(case fastype_of1 (Ts, t) of
- Type ("fun", [T1, T2]) =>
+ Type (@{type_name fun}, [T1, T2]) =>
if is_plain_fun t then
case T2 of
@{typ bool} =>
@@ -341,9 +349,9 @@
end
| Type (@{type_name option}, [T2']) =>
let
- val ts_pair = snd (dest_plain_fun t)
- |> pairself (map (polish_funs Ts))
- in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
+ val (maybe_opt, ts_pair) =
+ dest_plain_fun t ||> pairself (map (polish_funs Ts))
+ in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
| _ => raise SAME ()
else
raise SAME ()
@@ -356,7 +364,7 @@
else polish_funs Ts t1 $ polish_funs Ts t2
| t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
| Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
- | Const (s, Type ("fun", [T1, T2])) =>
+ | Const (s, Type (@{type_name fun}, [T1, T2])) =>
if s = opt_flag orelse s = non_opt_flag then
Abs ("x", T1, Const (unknown, T2))
else
@@ -366,24 +374,24 @@
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
|> make_plain_fun maybe_opt T1 T2
- |> unarize_and_unbox_term
- |> typecast_fun (unarize_unbox_and_uniterize_type T')
- (unarize_unbox_and_uniterize_type T1)
- (unarize_unbox_and_uniterize_type T2)
+ |> unarize_unbox_etc_term
+ |> typecast_fun (uniterize_unarize_unbox_etc_type T')
+ (uniterize_unarize_unbox_etc_type T1)
+ (uniterize_unarize_unbox_etc_type T2)
(* (typ * int) list -> typ -> typ -> int -> term *)
- fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
+ fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
let
val k1 = card_of_type card_assigns T1
val k2 = card_of_type card_assigns T2
in
- term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
+ term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
[nth_combination (replicate k1 (k2, 0)) j]
handle General.Subscript =>
raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
signed_string_of_int j ^ " for " ^
string_for_rep (Vect (k1, Atom (k2, 0))))
end
- | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
+ | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
let
val k1 = card_of_type card_assigns T1
val k2 = k div k1
@@ -461,8 +469,9 @@
if length arg_Ts = 0 then
[]
else
- map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
- arg_jsss
+ map3 (fn Ts =>
+ term_for_rep (constr_s <> @{const_name FinFun})
+ seen Ts Ts) arg_Ts arg_Rs arg_jsss
|> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
|> dest_n_tuple (length uncur_arg_Ts)
val t =
@@ -519,50 +528,54 @@
and term_for_vect seen k R T1 T2 T' js =
make_fun true T1 T2 T'
(map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
- (map (term_for_rep seen T2 T2 R o single)
+ (map (term_for_rep true seen T2 T2 R o single)
(batch_list (arity_of_rep R) js))
- (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
- and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
- | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
+ (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
+ and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
+ | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
- | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
+ | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
+ (Struct [R1, R2]) [js] =
let
val arity1 = arity_of_rep R1
val (js1, js2) = chop arity1 js
in
list_comb (HOLogic.pair_const T1 T2,
- map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
+ map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
[[js1], [js2]])
end
- | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
+ | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
+ (Vect (k, R')) [js] =
term_for_vect seen k R' T1 T2 T' js
- | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
- jss =
+ | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
+ (Func (R1, Formula Neut)) jss =
let
val jss1 = all_combinations_for_rep R1
- val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
+ val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
val ts2 =
- map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
+ map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
[[int_from_bool (member (op =) jss js)]])
jss1
in make_fun false T1 T2 T' ts1 ts2 end
- | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
+ | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
+ (Func (R1, R2)) jss =
let
val arity1 = arity_of_rep R1
val jss1 = all_combinations_for_rep R1
- val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
+ val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
- val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
+ val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
o AList.lookup (op =) grouped_jss2) jss1
- in make_fun true T1 T2 T' ts1 ts2 end
- | term_for_rep seen T T' (Opt R) jss =
- if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
- | term_for_rep _ T _ R jss =
+ in make_fun maybe_opt T1 T2 T' ts1 ts2 end
+ | term_for_rep _ seen T T' (Opt R) jss =
+ if null jss then Const (unknown, T)
+ else term_for_rep true seen T T' R jss
+ | term_for_rep _ _ T _ R jss =
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
- in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
+ in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
-> nut -> term *)
@@ -689,7 +702,7 @@
val (oper, (t1, T'), T) =
case name of
FreeName (s, T, _) =>
- let val t = Free (s, unarize_unbox_and_uniterize_type T) in
+ let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
("=", (t, format_term_type thy def_table formats t), T)
end
| ConstName (s, T, _) =>
@@ -710,12 +723,17 @@
(* dtype_spec -> Pretty.T *)
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
Pretty.block (Pretty.breaks
- [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
- Pretty.str "=",
- Pretty.enum "," "{" "}"
- (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
- (if fun_from_pair complete false then []
- else [Pretty.str unrep]))])
+ (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
+ (case typ of
+ Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
+ | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
+ | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
+ | _ => []) @
+ [Pretty.str "=",
+ Pretty.enum "," "{" "}"
+ (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
+ (if fun_from_pair complete false then []
+ else [Pretty.str unrep]))]))
(* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
@@ -752,13 +770,14 @@
val (eval_names, noneval_nonskolem_nonsel_names) =
List.partition (String.isPrefix eval_prefix o nickname_of)
nonskolem_nonsel_names
- ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
+ ||> filter_out (member (op =) [@{const_name bisim},
+ @{const_name bisim_iterator_max}]
o nickname_of)
val free_names =
map (fn x as (s, T) =>
case filter (curry (op =) x
o pairf nickname_of
- (unarize_unbox_and_uniterize_type o type_of))
+ (uniterize_unarize_unbox_etc_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 09:25:23 2010 +0100
@@ -11,6 +11,9 @@
val formulas_monotonic :
hol_context -> bool -> typ -> term list * term list -> bool
+ val finitize_funs :
+ hol_context -> bool -> (typ option * bool option) list -> typ
+ -> term list * term list -> term list * term list
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -42,14 +45,17 @@
{hol_ctxt: hol_context,
binarize: bool,
alpha_T: typ,
+ no_harmless: bool,
max_fresh: int Unsynchronized.ref,
- datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
- constr_cache: (styp * mtyp) list Unsynchronized.ref}
+ datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
+ constr_mcache: (styp * mtyp) list Unsynchronized.ref}
-exception MTYPE of string * mtyp list
+exception MTYPE of string * mtyp list * typ list
+exception MTERM of string * mterm list
(* string -> unit *)
fun print_g (_ : string) = ()
+(* val print_g = tracing *)
(* var -> string *)
val string_for_var = signed_string_of_int
@@ -70,7 +76,7 @@
(* sign_atom -> string *)
fun string_for_sign_atom (S sn) = string_for_sign sn
- | string_for_sign_atom (V j) = string_for_var j
+ | string_for_sign_atom (V x) = string_for_var x
(* literal -> string *)
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
@@ -83,7 +89,7 @@
| is_MRec _ = false
(* mtyp -> mtyp * sign_atom * mtyp *)
fun dest_MFun (MFun z) = z
- | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
+ | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
val no_prec = 100
@@ -157,13 +163,18 @@
| mtype_of_mterm (MApp (m1, _)) =
case mtype_of_mterm m1 of
MFun (_, _, M12) => M12
- | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
+ | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
+
+(* mterm -> mterm * mterm list *)
+fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
+ | strip_mcomb m = (m, [])
-(* hol_context -> bool -> typ -> mdata *)
-fun initial_mdata hol_ctxt binarize alpha_T =
+(* hol_context -> bool -> bool -> typ -> mdata *)
+fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
- max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
- constr_cache = Unsynchronized.ref []} : mdata)
+ no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
+ datatype_mcache = Unsynchronized.ref [],
+ constr_mcache = Unsynchronized.ref []} : mdata)
(* typ -> typ -> bool *)
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -215,7 +226,7 @@
else repair_mtype cache (M :: seen) M
(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
-fun repair_datatype_cache cache =
+fun repair_datatype_mcache cache =
let
(* (string * typ list) * mtyp -> unit *)
fun repair_one (z, M) =
@@ -224,20 +235,41 @@
in List.app repair_one (rev (!cache)) end
(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
-fun repair_constr_cache dtype_cache constr_cache =
+fun repair_constr_mcache dtype_cache constr_mcache =
let
(* styp * mtyp -> unit *)
fun repair_one (x, M) =
- Unsynchronized.change constr_cache
+ Unsynchronized.change constr_mcache
(AList.update (op =) (x, repair_mtype dtype_cache [] M))
- in List.app repair_one (!constr_cache) end
+ in List.app repair_one (!constr_mcache) end
+
+(* typ -> bool *)
+fun is_fin_fun_supported_type @{typ prop} = true
+ | is_fin_fun_supported_type @{typ bool} = true
+ | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
+ | is_fin_fun_supported_type _ = false
+(* typ -> typ -> term -> term option *)
+fun fin_fun_body _ _ (t as @{term False}) = SOME t
+ | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
+ | fin_fun_body dom_T ran_T
+ ((t0 as Const (@{const_name If}, _))
+ $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
+ $ t2 $ t3) =
+ (if loose_bvar1 (t1', 0) then
+ NONE
+ else case fin_fun_body dom_T ran_T t3 of
+ NONE => NONE
+ | SOME t3 =>
+ SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
+ $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
+ | fin_fun_body _ _ _ = NONE
(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
let
val M1 = fresh_mtype_for_type mdata T1
val M2 = fresh_mtype_for_type mdata T2
- val a = if is_boolean_type (body_type T2) andalso
+ val a = if is_fin_fun_supported_type (body_type T2) andalso
exists_alpha_sub_mtype_fresh M1 then
V (Unsynchronized.inc max_fresh)
else
@@ -245,25 +277,23 @@
in (M1, a, M2) end
(* mdata -> typ -> mtyp *)
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
- datatype_cache, constr_cache, ...}) =
+ datatype_mcache, constr_mcache, ...}) =
let
- (* typ -> typ -> mtyp *)
- val do_fun = MFun oo fresh_mfun_for_fun_type mdata
(* typ -> mtyp *)
fun do_type T =
if T = alpha_T then
MAlpha
else case T of
- Type ("fun", [T1, T2]) => do_fun T1 T2
- | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
- | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
+ Type (@{type_name fun}, [T1, T2]) =>
+ MFun (fresh_mfun_for_fun_type mdata T1 T2)
+ | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
if could_exist_alpha_sub_mtype thy alpha_T T then
- case AList.lookup (op =) (!datatype_cache) z of
+ case AList.lookup (op =) (!datatype_mcache) z of
SOME M => M
| NONE =>
let
- val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
+ val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
val (all_Ms, constr_Ms) =
fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
@@ -279,15 +309,15 @@
end)
xs ([], [])
val M = MType (s, all_Ms)
- val _ = Unsynchronized.change datatype_cache
+ val _ = Unsynchronized.change datatype_mcache
(AList.update (op =) (z, M))
- val _ = Unsynchronized.change constr_cache
+ val _ = Unsynchronized.change constr_mcache
(append (xs ~~ constr_Ms))
in
- if forall (not o is_MRec o snd) (!datatype_cache) then
- (repair_datatype_cache datatype_cache;
- repair_constr_cache (!datatype_cache) constr_cache;
- AList.lookup (op =) (!datatype_cache) z |> the)
+ if forall (not o is_MRec o snd) (!datatype_mcache) then
+ (repair_datatype_mcache datatype_mcache;
+ repair_constr_mcache (!datatype_mcache) constr_mcache;
+ AList.lookup (op =) (!datatype_mcache) z |> the)
else
M
end
@@ -300,7 +330,7 @@
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
| prodM_factors M = [M]
(* mtyp -> mtyp list * mtyp *)
-fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
+fun curried_strip_mtype (MFun (M1, _, M2)) =
curried_strip_mtype M2 |>> append (prodM_factors M1)
| curried_strip_mtype M = ([], M)
(* string -> mtyp -> mtyp *)
@@ -311,36 +341,34 @@
end
(* mdata -> styp -> mtyp *)
-fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
+fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
...}) (x as (_, T)) =
if could_exist_alpha_sub_mtype thy alpha_T T then
- case AList.lookup (op =) (!constr_cache) x of
+ case AList.lookup (op =) (!constr_mcache) x of
SOME M => M
| NONE => if T = alpha_T then
let val M = fresh_mtype_for_type mdata T in
- (Unsynchronized.change constr_cache (cons (x, M)); M)
+ (Unsynchronized.change constr_mcache (cons (x, M)); M)
end
else
(fresh_mtype_for_type mdata (body_type T);
- AList.lookup (op =) (!constr_cache) x |> the)
+ AList.lookup (op =) (!constr_mcache) x |> the)
else
fresh_mtype_for_type mdata T
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
|> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
+(* literal list -> sign_atom -> sign_atom *)
+fun resolve_sign_atom lits (V x) =
+ x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
+ | resolve_sign_atom _ a = a
(* literal list -> mtyp -> mtyp *)
-fun instantiate_mtype lits =
+fun resolve_mtype lits =
let
(* mtyp -> mtyp *)
fun aux MAlpha = MAlpha
- | aux (MFun (M1, V x, M2)) =
- let
- val a = case AList.lookup (op =) lits x of
- SOME sn => S sn
- | NONE => V x
- in MFun (aux M1, a, aux M2) end
- | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
+ | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
| aux (MPair Mp) = MPair (pairself aux Mp)
| aux (MType (s, Ms)) = MType (s, map aux Ms)
| aux (MRec z) = MRec z
@@ -417,11 +445,12 @@
accum =
(accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
handle Library.UnequalLengths =>
- raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
+ raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
| do_mtype_comp _ _ (MType _) (MType _) accum =
accum (* no need to compare them thanks to the cache *)
- | do_mtype_comp _ _ M1 M2 _ =
- raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
+ | do_mtype_comp cmp _ M1 M2 _ =
+ raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
+ [M1, M2], [])
(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
@@ -471,20 +500,20 @@
| do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
accum |> fold (do_notin_mtype_fv sn sexp) Ms
| do_notin_mtype_fv _ _ M _ =
- raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
+ raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
(* sign -> mtyp -> constraint_set -> constraint_set *)
fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
| add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
- (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
- (case sn of Minus => "unique" | Plus => "total") ^ ".");
+ (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
+ (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
| SOME (lits, sexps) => CSet (lits, comps, sexps))
(* mtyp -> constraint_set -> constraint_set *)
-val add_mtype_is_right_unique = add_notin_mtype_fv Minus
-val add_mtype_is_right_total = add_notin_mtype_fv Plus
+val add_mtype_is_concrete = add_notin_mtype_fv Minus
+val add_mtype_is_complete = add_notin_mtype_fv Plus
val bool_from_minus = true
@@ -574,34 +603,35 @@
type mtype_schema = mtyp * constraint_set
type mtype_context =
- {bounds: mtyp list,
+ {bound_Ts: typ list,
+ bound_Ms: mtyp list,
frees: (styp * mtyp) list,
consts: (styp * mtyp) list}
type accumulator = mtype_context * constraint_set
-val initial_gamma = {bounds = [], frees = [], consts = []}
+val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
val unsolvable_accum = (initial_gamma, UnsolvableCSet)
-(* mtyp -> mtype_context -> mtype_context *)
-fun push_bound M {bounds, frees, consts} =
- {bounds = M :: bounds, frees = frees, consts = consts}
+(* typ -> mtyp -> mtype_context -> mtype_context *)
+fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
+ {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
+ consts = consts}
(* mtype_context -> mtype_context *)
-fun pop_bound {bounds, frees, consts} =
- {bounds = tl bounds, frees = frees, consts = consts}
- handle List.Empty => initial_gamma
+fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
+ {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
+ consts = consts}
+ handle List.Empty => initial_gamma (* FIXME: needed? *)
(* mdata -> term -> accumulator -> mterm * accumulator *)
fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
- def_table, ...},
+ def_table, ...},
alpha_T, max_fresh, ...}) =
let
- (* typ -> typ -> mtyp * sign_atom * mtyp *)
- val mfun_for = fresh_mfun_for_fun_type mdata
(* typ -> mtyp *)
val mtype_for = fresh_mtype_for_type mdata
(* mtyp -> mtyp *)
- fun pos_set_mtype_for_dom M =
+ fun plus_set_mtype_for_dom M =
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
(* typ -> accumulator -> mterm * accumulator *)
fun do_all T (gamma, cset) =
@@ -610,13 +640,13 @@
val body_M = mtype_for (body_type T)
in
(MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
- (gamma, cset |> add_mtype_is_right_total abs_M))
+ (gamma, cset |> add_mtype_is_complete abs_M))
end
fun do_equals T (gamma, cset) =
let val M = mtype_for (domain_type T) in
(MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
mtype_for (nth_range_type 2 T))),
- (gamma, cset |> add_mtype_is_right_unique M))
+ (gamma, cset |> add_mtype_is_concrete M))
end
fun do_robust_set_operation T (gamma, cset) =
let
@@ -633,25 +663,25 @@
val set_T = domain_type T
val set_M = mtype_for set_T
(* typ -> mtyp *)
- fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
+ fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
if T = set_T then set_M
else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
| custom_mtype_for T = mtype_for T
in
- (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
+ (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
end
(* typ -> accumulator -> mtyp * accumulator *)
fun do_pair_constr T accum =
case mtype_for (nth_range_type 2 T) of
M as MPair (a_M, b_M) =>
(MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
- | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
+ | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
(* int -> typ -> accumulator -> mtyp * accumulator *)
fun do_nth_pair_sel n T =
case mtype_for (domain_type T) of
M as MPair (a_M, b_M) =>
pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
- | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
+ | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
(* mtyp * accumulator *)
val mtype_unsolvable = (dummy_M, unsolvable_accum)
(* term -> mterm * accumulator *)
@@ -661,8 +691,9 @@
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
let
val abs_M = mtype_for abs_T
- val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
- val expected_bound_M = pos_set_mtype_for_dom abs_M
+ val (bound_m, accum) =
+ accum |>> push_bound abs_T abs_M |> do_term bound_t
+ val expected_bound_M = plus_set_mtype_for_dom abs_M
val (body_m, accum) =
accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
|> do_term body_t ||> apfst pop_bound
@@ -678,7 +709,8 @@
end
(* term -> accumulator -> mterm * accumulator *)
and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
- | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
+ | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
+ cset)) =
(case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
@@ -714,12 +746,12 @@
let
val set_T = domain_type (range_type T)
val M1 = mtype_for (domain_type set_T)
- val M1' = pos_set_mtype_for_dom M1
+ val M1' = plus_set_mtype_for_dom M1
val M2 = mtype_for set_T
val M3 = mtype_for set_T
in
(MFun (M1, S Minus, MFun (M2, S Minus, M3)),
- (gamma, cset |> add_mtype_is_right_unique M1
+ (gamma, cset |> add_mtype_is_concrete M1
|> add_is_sub_mtype M1' M3
|> add_is_sub_mtype M2 M3))
end
@@ -738,7 +770,7 @@
| @{const_name finite} =>
if is_finite_type hol_ctxt T then
let val M1 = mtype_for (domain_type (domain_type T)) in
- (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
+ (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
end
else
(print_g "*** finite"; mtype_unsolvable)
@@ -761,8 +793,8 @@
val b_M = mtype_for (range_type (domain_type T))
in
(MFun (MFun (a_M, S Minus, b_M), S Minus,
- MFun (pos_set_mtype_for_dom a_M, S Minus,
- pos_set_mtype_for_dom b_M)), accum)
+ MFun (plus_set_mtype_for_dom a_M, S Minus,
+ plus_set_mtype_for_dom b_M)), accum)
end
| @{const_name Sigma} =>
let
@@ -784,12 +816,8 @@
| @{const_name Tha} =>
let
val a_M = mtype_for (domain_type (domain_type T))
- val a_set_M = pos_set_mtype_for_dom a_M
+ val a_set_M = plus_set_mtype_for_dom a_M
in (MFun (a_set_M, S Minus, a_M), accum) end
- | @{const_name FunBox} =>
- let val dom_M = mtype_for (domain_type T) in
- (MFun (dom_M, S Minus, dom_M), accum)
- end
| _ =>
if s = @{const_name minus_class.minus} andalso
is_set_type (domain_type T) then
@@ -800,7 +828,7 @@
in
(MFun (left_set_M, S Minus,
MFun (right_set_M, S Minus, left_set_M)),
- (gamma, cset |> add_mtype_is_right_unique right_set_M
+ (gamma, cset |> add_mtype_is_concrete right_set_M
|> add_is_sub_mtype right_set_M left_set_M))
end
else if s = @{const_name ord_class.less_eq} andalso
@@ -811,50 +839,54 @@
is_set_type (domain_type T) then
do_robust_set_operation T accum
else if is_sel s then
- if constr_name_for_sel_like s = @{const_name FunBox} then
- let val dom_M = mtype_for (domain_type T) in
- (MFun (dom_M, S Minus, dom_M), accum)
- end
- else
- (mtype_for_sel mdata x, accum)
+ (mtype_for_sel mdata x, accum)
else if is_constr thy stds x then
(mtype_for_constr mdata x, accum)
- else if is_built_in_const thy stds fast_descrs x then
+ else if is_built_in_const thy stds fast_descrs x andalso
+ s <> @{const_name is_unknown} andalso
+ s <> @{const_name unknown} then
+ (* the "unknown" part is a hack *)
case def_of_const thy def_table x of
SOME t' => do_term t' accum |>> mtype_of_mterm
| NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
else
let val M = mtype_for T in
- (M, ({bounds = bounds, frees = frees,
- consts = (x, M) :: consts}, cset))
+ (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
+ frees = frees, consts = (x, M) :: consts}, cset))
end) |>> curry MRaw t
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
SOME M => (M, accum)
| NONE =>
let val M = mtype_for T in
- (M, ({bounds = bounds, frees = (x, M) :: frees,
- consts = consts}, cset))
+ (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
+ frees = (x, M) :: frees, consts = consts}, cset))
end) |>> curry MRaw t
| Var _ => (print_g "*** Var"; mterm_unsolvable t)
- | Bound j => (MRaw (t, nth bounds j), accum)
- | Abs (s, T, t' as @{const False}) =>
- let val (M1, a, M2) = mfun_for T bool_T in
- (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
- end
+ | Bound j => (MRaw (t, nth bound_Ms j), accum)
| Abs (s, T, t') =>
- ((case t' of
- t1' $ Bound 0 =>
- if not (loose_bvar1 (t1', 0)) then
- do_term (incr_boundvars ~1 t1') accum
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- let
- val M = mtype_for T
- val (m', accum) = do_term t' (accum |>> push_bound M)
- in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
+ (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
+ SOME t' =>
+ let
+ val M = mtype_for T
+ val a = V (Unsynchronized.inc max_fresh)
+ val (m', accum) = do_term t' (accum |>> push_bound T M)
+ in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
+ | NONE =>
+ ((case t' of
+ t1' $ Bound 0 =>
+ if not (loose_bvar1 (t1', 0)) then
+ do_term (incr_boundvars ~1 t1') accum
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let
+ val M = mtype_for T
+ val (m', accum) = do_term t' (accum |>> push_bound T M)
+ in
+ (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
+ end))
| (t0 as Const (@{const_name All}, _))
$ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
@@ -872,6 +904,8 @@
(_, UnsolvableCSet) => mterm_unsolvable t
| _ =>
let
+ val T11 = domain_type (fastype_of1 (bound_Ts, t1))
+ val T2 = fastype_of1 (bound_Ts, t2)
val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
val M2 = mtype_of_mterm m2
in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
@@ -880,18 +914,38 @@
string_for_mterm ctxt m))
in do_term end
-(* mdata -> styp -> term -> term -> mterm * accumulator *)
-fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
+(*
+ accum |> (case a of
+ S Minus => accum
+ | S Plus => unsolvable_accum
+ | V x => do_literal (x, Minus) lits)
+*)
+
+(* int -> mtyp -> accumulator -> accumulator *)
+fun force_minus_funs 0 _ = I
+ | force_minus_funs n (M as MFun (M1, _, M2)) =
+ add_mtypes_equal M (MFun (M1, S Minus, M2))
+ #> force_minus_funs (n - 1) M2
+ | force_minus_funs _ M =
+ raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
+(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
+fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
let
val (m1, accum) = consider_term mdata t1 accum
val (m2, accum) = consider_term mdata t2 accum
val M1 = mtype_of_mterm m1
val M2 = mtype_of_mterm m2
+ val accum = accum ||> add_mtypes_equal M1 M2
val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+ val m = MApp (MApp (MRaw (Const x,
+ MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
in
- (MApp (MApp (MRaw (Const x,
- MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
- accum ||> add_mtypes_equal M1 M2)
+ (m, if def then
+ let val (head_m, arg_ms) = strip_mcomb m1 in
+ accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
+ end
+ else
+ accum)
end
(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
@@ -912,11 +966,13 @@
val abs_M = mtype_for abs_T
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
val (body_m, accum) =
- accum ||> side_cond ? add_mtype_is_right_total abs_M
- |>> push_bound abs_M |> do_formula sn body_t
+ accum ||> side_cond ? add_mtype_is_complete abs_M
+ |>> push_bound abs_T abs_M |> do_formula sn body_t
val body_M = mtype_of_mterm body_m
in
- (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
+ (MApp (MRaw (Const quant_x,
+ MFun (MFun (abs_M, S Minus, body_M), S Minus,
+ body_M)),
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
accum |>> pop_bound)
end
@@ -924,7 +980,7 @@
fun do_equals x t1 t2 =
case sn of
Plus => do_term t accum
- | Minus => consider_general_equals mdata x t1 t2 accum
+ | Minus => consider_general_equals mdata false x t1 t2 accum
in
case t of
Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
@@ -947,7 +1003,7 @@
(case sn of
Plus => do_quantifier x0 s1 T1 t1'
| Minus =>
- (* ### do elsewhere *)
+ (* FIXME: Move elsewhere *)
do_term (@{const Not}
$ (HOLogic.eq_const (domain_type T0) $ t1
$ Abs (Name.uu, T1, @{const False}))) accum)
@@ -981,23 +1037,24 @@
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
val bounteous_consts = [@{const_name bisim}]
-(* term -> bool *)
-fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
- Term.add_consts t []
- |> filter_out (is_built_in_const thy stds fast_descrs)
- |> (forall (member (op =) harmless_consts o original_name o fst)
- orf exists (member (op =) bounteous_consts o fst))
+(* mdata -> term -> bool *)
+fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
+ | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
+ Term.add_consts t []
+ |> filter_out (is_built_in_const thy stds fast_descrs)
+ |> (forall (member (op =) harmless_consts o original_name o fst) orf
+ exists (member (op =) bounteous_consts o fst))
(* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
- if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
+fun consider_nondefinitional_axiom mdata t =
+ if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
else consider_general_formula mdata Plus t
(* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
+fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
consider_nondefinitional_axiom mdata t
- else if is_harmless_axiom hol_ctxt t then
+ else if is_harmless_axiom mdata t then
pair (MRaw (t, dummy_M))
else
let
@@ -1010,10 +1067,11 @@
let
val abs_M = mtype_for abs_T
val (body_m, accum) =
- accum |>> push_bound abs_M |> do_formula body_t
+ accum |>> push_bound abs_T abs_M |> do_formula body_t
val body_M = mtype_of_mterm body_m
in
- (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
+ (MApp (MRaw (quant_t,
+ MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
accum |>> pop_bound)
end
@@ -1039,16 +1097,20 @@
case t of
(t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
do_all t0 s1 T1 t1 accum
- | @{const Trueprop} $ t1 => do_formula t1 accum
+ | @{const Trueprop} $ t1 =>
+ let val (m1, accum) = do_formula t1 accum in
+ (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+ m1), accum)
+ end
| Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
- consider_general_equals mdata x t1 t2 accum
+ consider_general_equals mdata true x t1 t2 accum
| (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
do_conjunction t0 t1 t2 accum
| (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
do_all t0 s0 T1 t1 accum
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
- consider_general_equals mdata x t1 t2 accum
+ consider_general_equals mdata true x t1 t2 accum
| (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
| (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
@@ -1057,8 +1119,7 @@
(* Proof.context -> literal list -> term -> mtyp -> string *)
fun string_for_mtype_of_term ctxt lits t M =
- Syntax.string_of_term ctxt t ^ " : " ^
- string_for_mtype (instantiate_mtype lits M)
+ Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
(* theory -> literal list -> mtype_context -> unit *)
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
@@ -1067,31 +1128,135 @@
|> cat_lines |> print_g
(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
-fun gather f t (ms, accum) =
+fun amass f t (ms, accum) =
let val (m, accum) = f t accum in (m :: ms, accum) end
-(* hol_context -> bool -> typ -> term list * term list -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
- (nondef_ts, def_ts) =
+(* string -> bool -> hol_context -> bool -> typ -> term list * term list
+ -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
+fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
+ (nondef_ts, def_ts) =
let
- val _ = print_g ("****** Monotonicity analysis: " ^
+ val _ = print_g ("****** " ^ which ^ " analysis: " ^
string_for_mtype MAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
- val mdata as {max_fresh, constr_cache, ...} =
- initial_mdata hol_ctxt binarize alpha_T
-
+ val mdata as {max_fresh, constr_mcache, ...} =
+ initial_mdata hol_ctxt binarize no_harmless alpha_T
val accum = (initial_gamma, slack)
val (nondef_ms, accum) =
- ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
- |> fold (gather (consider_nondefinitional_axiom mdata))
+ ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
+ |> fold (amass (consider_nondefinitional_axiom mdata))
(tl nondef_ts)
val (def_ms, (gamma, cset)) =
- ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
+ ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
in
case solve (!max_fresh) cset of
- SOME lits => (print_mtype_context ctxt lits gamma; true)
- | _ => false
+ SOME lits => (print_mtype_context ctxt lits gamma;
+ SOME (lits, (nondef_ms, def_ms), !constr_mcache))
+ | _ => NONE
end
- handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
+ handle MTYPE (loc, Ms, Ts) =>
+ raise BAD (loc, commas (map string_for_mtype Ms @
+ map (Syntax.string_of_typ ctxt) Ts))
+ | MTERM (loc, ms) =>
+ raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
+
+(* hol_context -> bool -> typ -> term list * term list -> bool *)
+val formulas_monotonic = is_some oooo infer "Monotonicity" false
+
+(* typ -> typ -> styp *)
+fun fin_fun_constr T1 T2 =
+ (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
+
+(* hol_context -> bool -> (typ option * bool option) list -> typ
+ -> term list * term list -> term list * term list *)
+fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
+ binarize finitizes alpha_T tsp =
+ case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
+ SOME (lits, msp, constr_mtypes) =>
+ let
+ (* typ -> sign_atom -> bool *)
+ fun should_finitize T a =
+ case triple_lookup (type_match thy) finitizes T of
+ SOME (SOME false) => false
+ | _ => resolve_sign_atom lits a = S Plus
+ (* typ -> mtyp -> typ *)
+ fun type_from_mtype T M =
+ case (M, T) of
+ (MAlpha, _) => T
+ | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
+ Type (if should_finitize T a then @{type_name fin_fun}
+ else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
+ | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
+ Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
+ | (MType _, _) => T
+ | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
+ [M], [T])
+ (* styp -> styp *)
+ fun finitize_constr (x as (s, T)) =
+ (s, case AList.lookup (op =) constr_mtypes x of
+ SOME M => type_from_mtype T M
+ | NONE => T)
+ (* typ list -> mterm -> term *)
+ fun term_from_mterm Ts m =
+ case m of
+ MRaw (t, M) =>
+ let
+ val T = fastype_of1 (Ts, t)
+ val T' = type_from_mtype T M
+ in
+ case t of
+ Const (x as (s, T)) =>
+ if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
+ Const (s, T')
+ else if is_built_in_const thy stds fast_descrs x then
+ coerce_term hol_ctxt Ts T' T t
+ else if is_constr thy stds x then
+ Const (finitize_constr x)
+ else if is_sel s then
+ let
+ val n = sel_no_from_name s
+ val x' = x |> binarized_and_boxed_constr_for_sel hol_ctxt
+ binarize
+ |> finitize_constr
+ val x'' = binarized_and_boxed_nth_sel_for_constr hol_ctxt
+ binarize x' n
+ in Const x'' end
+ else
+ Const (s, T')
+ | Free (s, T) => Free (s, type_from_mtype T M)
+ | Bound _ => t
+ | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
+ [m])
+ end
+ | MAbs (s, T, M, a, m') =>
+ let
+ val T = type_from_mtype T M
+ val t' = term_from_mterm (T :: Ts) m'
+ val T' = fastype_of1 (T :: Ts, t')
+ in
+ Abs (s, T, t')
+ |> should_finitize (T --> T') a
+ ? construct_value thy stds (fin_fun_constr T T') o single
+ end
+ | MApp (m1, m2) =>
+ let
+ val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
+ val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
+ val (t1', T2') =
+ case T1 of
+ Type (s, [T11, T12]) =>
+ (if s = @{type_name fin_fun} then
+ select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 0
+ (T11 --> T12)
+ else
+ t1, T11)
+ | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
+ [T1], [])
+ in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
+ in
+ Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
+ pairself (map (term_from_mterm [])) msp
+ end
+ | NONE => tsp
end;
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 09:25:23 2010 +0100
@@ -287,8 +287,9 @@
"Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
implode (map sub us)
| Construct (us', T, R, us) =>
- "Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^
- " " ^ string_for_rep R ^ " " ^ implode (map sub us)
+ "Construct " ^ implode (map sub us') ^ " " ^
+ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
+ implode (map sub us)
| BoundName (j, T, R, nick) =>
"BoundName " ^ signed_string_of_int j ^ " " ^
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
@@ -459,7 +460,8 @@
(res_T, Const (@{const_name snd}, T --> res_T) $ t)
end
(* typ * term -> (typ * term) list *)
-fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
+fun factorize (z as (Type (@{type_name "*"}, _), _)) =
+ maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
(* hol_context -> op2 -> term -> nut *)
@@ -623,7 +625,8 @@
if is_built_in_const thy stds false x then Cst (Add, T, Any)
else ConstName (s, T, Any)
| (Const (@{const_name minus_class.minus},
- Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ Type (@{type_name fun},
+ [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
[t1, t2]) =>
Op2 (SetDifference, T1, Any, sub t1, sub t2)
| (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
@@ -642,7 +645,8 @@
else
do_apply t0 ts
| (Const (@{const_name ord_class.less_eq},
- Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
+ Type (@{type_name fun},
+ [Type (@{type_name fun}, [_, @{typ bool}]), _])),
[t1, t2]) =>
Op2 (Subset, bool_T, Any, sub t1, sub t2)
(* FIXME: find out if this case is necessary *)
@@ -666,7 +670,7 @@
| (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
| (Const (@{const_name is_unknown}, _), [t1]) =>
Op1 (IsUnknown, bool_T, Any, sub t1)
- | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
+ | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
Op1 (Tha, T2, Any, sub t1)
| (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
| (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
@@ -676,11 +680,13 @@
T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
Cst (NatToInt, T, Any)
| (Const (@{const_name semilattice_inf_class.inf},
- Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ Type (@{type_name fun},
+ [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
[t1, t2]) =>
Op2 (Intersect, T1, Any, sub t1, sub t2)
| (Const (@{const_name semilattice_sup_class.sup},
- Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ Type (@{type_name fun},
+ [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
[t1, t2]) =>
Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
@@ -956,7 +962,7 @@
if ok then Cst (Num j, T, Atom (k, j0))
else Cst (Unrep, T, Opt (Atom (k, j0)))
end)
- | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
+ | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
let val R = Atom (spec_of_type scope T1) in
Cst (Suc, T, Func (R, Opt R))
end
@@ -1306,12 +1312,13 @@
in (w :: ws, pool, NameTable.update (v, w) table) end
(* typ -> rep -> nut list -> nut *)
-fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us =
+fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
+ us =
let val arity1 = arity_of_rep R1 in
Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
shape_tuple T2 R2 (List.drop (us, arity1))])
end
- | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
+ | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
| shape_tuple T _ [u] =
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 09:25:23 2010 +0100
@@ -9,7 +9,9 @@
sig
type hol_context = Nitpick_HOL.hol_context
val preprocess_term :
- hol_context -> term -> term list * term list * bool * bool * bool
+ hol_context -> (typ option * bool option) list
+ -> (typ option * bool option) list -> term
+ -> term list * term list * bool * bool * bool
end
structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -17,6 +19,7 @@
open Nitpick_Util
open Nitpick_HOL
+open Nitpick_Mono
(* polarity -> string -> bool *)
fun is_positive_existential polar quant_s =
@@ -115,88 +118,15 @@
(** Boxing **)
-(* hol_context -> typ -> term -> term *)
-fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
- (case head_of t of
- Const x => if is_constr_like thy x then t else raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- let
- val x' as (_, T') =
- if is_pair_type T then
- let val (T1, T2) = HOLogic.dest_prodT T in
- (@{const_name Pair}, T1 --> T2 --> T)
- end
- else
- datatype_constrs hol_ctxt T |> hd
- val arg_Ts = binder_types T'
- in
- list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
- (index_seq 0 (length arg_Ts)) arg_Ts)
- end
-
-(* (term -> term) -> int -> term -> term *)
-fun coerce_bound_no f j t =
- case t of
- t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
- | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
- | Bound j' => if j' = j then f t else t
- | _ => t
-(* hol_context -> typ -> typ -> term -> term *)
-fun coerce_bound_0_in_term hol_ctxt new_T old_T =
- old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-(* hol_context -> typ list -> typ -> typ -> term -> term *)
-and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
- if old_T = new_T then
- t
- else
- case (new_T, old_T) of
- (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type ("fun", [old_T1, old_T2])) =>
- (case eta_expand Ts t 1 of
- Abs (s, _, t') =>
- Abs (s, new_T1,
- t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
- |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
- |> Envir.eta_contract
- |> new_s <> "fun"
- ? construct_value thy stds
- (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- o single
- | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
- | (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = "*" then
- case constr_expand hol_ctxt old_T t of
- Const (old_s, _) $ t1 =>
- if new_s = "fun" then
- coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
- else
- construct_value thy stds
- (old_s, Type ("fun", new_Ts) --> new_T)
- [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
- (Type ("fun", old_Ts)) t1]
- | Const _ $ t1 $ t2 =>
- construct_value thy stds
- (if new_s = "*" then @{const_name Pair}
- else @{const_name PairBox}, new_Ts ---> new_T)
- [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
- coerce_term hol_ctxt Ts new_T2 old_T2 t2]
- | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
- else
- raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
- | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
-
(* hol_context -> bool -> term -> term *)
fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
orig_t =
let
(* typ -> typ *)
- fun box_relational_operator_type (Type ("fun", Ts)) =
- Type ("fun", map box_relational_operator_type Ts)
- | box_relational_operator_type (Type ("*", Ts)) =
- Type ("*", map (box_type hol_ctxt InPair) Ts)
+ fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
+ Type (@{type_name fun}, map box_relational_operator_type Ts)
+ | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
+ Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
| box_relational_operator_type T = T
(* indexname * typ -> typ * term -> typ option list -> typ option list *)
fun add_boxed_types_for_var (z as (_, T)) (T', t') =
@@ -320,12 +250,13 @@
val T2 = fastype_of1 (new_Ts, t2)
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
- betapply (if s1 = "fun" then
+ betapply (if s1 = @{type_name fun} then
t1
else
select_nth_constr_arg thy stds
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
+ (@{const_name FunBox},
+ Type (@{type_name fun}, Ts1) --> T1) t1 0
+ (Type (@{type_name fun}, Ts1)), t2)
end
| t1 $ t2 =>
let
@@ -336,12 +267,13 @@
val T2 = fastype_of1 (new_Ts, t2)
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
- betapply (if s1 = "fun" then
+ betapply (if s1 = @{type_name fun} then
t1
else
select_nth_constr_arg thy stds
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
+ (@{const_name FunBox},
+ Type (@{type_name fun}, Ts1) --> T1) t1 0
+ (Type (@{type_name fun}, Ts1)), t2)
end
| Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
| Var (z as (x, T)) =>
@@ -597,7 +529,7 @@
if pass1 then do_eq false t2 t1 else raise SAME ()
else case t1 of
Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
- | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+ | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
if j' = j andalso
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
@@ -1141,8 +1073,8 @@
(* int -> typ -> accumulator -> accumulator *)
and add_axioms_for_type depth T =
case T of
- Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
- | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
+ Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
+ | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
| @{typ prop} => I
| @{typ bool} => I
| @{typ unit} => I
@@ -1399,11 +1331,29 @@
| _ => t
in aux "" [] [] end
+(** Inference of finite functions **)
+
+(* hol_context -> bool -> (typ option * bool option) list
+ -> (typ option * bool option) list -> term list * term list
+ -> term list * term list *)
+fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
+ (nondef_ts, def_ts) =
+ let
+ val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
+ |> filter_out (fn Type (@{type_name fun_box}, _) => true
+ | T => is_small_finite_type hol_ctxt T orelse
+ triple_lookup (type_match thy) monos T
+ = SOME (SOME false))
+ in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
+
(** Preprocessor entry point **)
-(* hol_context -> term -> term list * term list * bool * bool * bool *)
+(* hol_context -> (typ option * bool option) list
+ -> (typ option * bool option) list -> term
+ -> term list * term list * bool * bool * bool *)
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
- boxes, skolemize, uncurry, ...}) t =
+ boxes, skolemize, uncurry, ...})
+ finitizes monos t =
let
val skolem_depth = if skolemize then 4 else ~1
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1442,6 +1392,9 @@
#> Term.map_abs_vars shortest_name
val nondef_ts = map (do_rest false) nondef_ts
val def_ts = map (do_rest true) def_ts
+ val (nondef_ts, def_ts) =
+ finitize_all_types_of_funs hol_ctxt binarize finitizes monos
+ (nondef_ts, def_ts)
in
(nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
end
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Mar 09 09:25:23 2010 +0100
@@ -158,9 +158,9 @@
| smart_range_rep _ _ _ (Func (_, R2)) = R2
| smart_range_rep ofs T ran_card (Opt R) =
Opt (smart_range_rep ofs T ran_card R)
- | smart_range_rep ofs (Type ("fun", [_, T2])) _ (Atom (1, _)) =
+ | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
Atom (1, offset_of_type ofs T2)
- | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
+ | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
Atom (ran_card (), offset_of_type ofs T2)
| smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
@@ -183,10 +183,10 @@
| one_rep _ _ (Vect z) = Vect z
| one_rep ofs T (Opt R) = one_rep ofs T R
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
-fun optable_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
+fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, optable_rep ofs T2 R2)
| optable_rep ofs T R = one_rep ofs T R
-fun opt_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
+fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, opt_rep ofs T2 R2)
| opt_rep ofs T R = Opt (optable_rep ofs T R)
(* rep -> rep *)
@@ -264,11 +264,11 @@
(* scope -> typ -> rep *)
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
- (Type ("fun", [T1, T2])) =
+ (Type (@{type_name fun}, [T1, T2])) =
(case best_one_rep_for_type scope T2 of
Unit => Unit
| R2 => Vect (card_of_type card_assigns T1, R2))
- | best_one_rep_for_type scope (Type ("*", [T1, T2])) =
+ | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
(case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
(Unit, Unit) => Unit
| (R1, R2) => Struct [R1, R2])
@@ -284,12 +284,12 @@
(* Datatypes are never represented by Unit, because it would confuse
"nfa_transitions_for_ctor". *)
(* scope -> typ -> rep *)
-fun best_opt_set_rep_for_type scope (Type ("fun", [T1, T2])) =
+fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
opt_rep ofs T (best_one_rep_for_type scope T)
fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
- (Type ("fun", [T1, T2])) =
+ (Type (@{type_name fun}, [T1, T2])) =
(case (best_one_rep_for_type scope T1,
best_non_opt_set_rep_for_type scope T2) of
(_, Unit) => Unit
@@ -302,7 +302,7 @@
(if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
else best_opt_set_rep_for_type) scope T
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
- (Type ("fun", [T1, T2])) =
+ (Type (@{type_name fun}, [T1, T2])) =
(optable_rep ofs T1 (best_one_rep_for_type scope T1),
optable_rep ofs T2 (best_one_rep_for_type scope T2))
| best_non_opt_symmetric_reps_for_fun_type _ T =
@@ -325,11 +325,11 @@
fun type_schema_of_rep _ (Formula _) = []
| type_schema_of_rep _ Unit = []
| type_schema_of_rep T (Atom _) = [T]
- | type_schema_of_rep (Type ("*", [T1, T2])) (Struct [R1, R2]) =
+ | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
type_schema_of_reps [T1, T2] [R1, R2]
- | type_schema_of_rep (Type ("fun", [_, T2])) (Vect (k, R)) =
+ | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
replicate_list k (type_schema_of_rep T2 R)
- | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
+ | type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R
| type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Mar 09 09:25:23 2010 +0100
@@ -106,22 +106,26 @@
| NONE => constr_spec dtypes x
(* dtype_spec list -> bool -> typ -> bool *)
-fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
+fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
- | is_complete_type dtypes facto (Type ("*", Ts)) =
+ | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
+ is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
+ | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
forall (is_complete_type dtypes facto) Ts
| is_complete_type dtypes facto T =
not (is_integer_like_type T) andalso not (is_bit_type T) andalso
fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
handle Option.Option => true
-and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
+and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
- | is_concrete_type dtypes facto (Type ("*", Ts)) =
+ | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
+ is_concrete_type dtypes facto T2
+ | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
forall (is_concrete_type dtypes facto) Ts
| is_concrete_type dtypes facto T =
fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
handle Option.Option => true
-fun is_exact_type dtypes facto =
+and is_exact_type dtypes facto =
is_complete_type dtypes facto andf is_concrete_type dtypes facto
(* int Typtab.table -> typ -> int *)
@@ -528,15 +532,15 @@
(* theory -> typ list -> (typ option * int list) list
-> (typ option * int list) list *)
-fun repair_cards_assigns_wrt_boxing _ _ [] = []
- | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
+fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
+ | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) =
(if is_fun_type T orelse is_pair_type T then
- Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
- |> map (rpair ks o SOME)
+ Ts |> filter (curry (type_match thy o swap) T) |> map (rpair ks o SOME)
else
- [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
- | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
- (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
+ [(SOME T, ks)]) @
+ repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
+ | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
+ (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
val max_scopes = 4096
val distinct_threshold = 512
@@ -548,8 +552,8 @@
maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
deep_dataTs finitizable_dataTs =
let
- val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
- cards_assigns
+ val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts
+ cards_assigns
val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts
nonmono_Ts