--- a/doc-src/Codegen/Thy/Further.thy Mon May 31 18:17:48 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon May 31 19:36:13 2010 +0200
@@ -94,7 +94,7 @@
whole @{text SML} is read, the necessary code is generated transparently
and the corresponding constant names are inserted. This technique also
allows to use pattern matching on constructors stemming from compiled
- @{text datatypes}.
+ @{text "datatypes"}.
For a less simplistic example, theory @{theory Ferrack} is
a good reference.
--- a/doc-src/Codegen/Thy/ML.thy Mon May 31 18:17:48 2010 +0200
+++ b/doc-src/Codegen/Thy/ML.thy Mon May 31 19:36:13 2010 +0200
@@ -30,9 +30,9 @@
-> theory -> theory"} \\
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
- @{index_ML Code.get_datatype: "theory -> string
+ @{index_ML Code.get_type: "theory -> string
-> (string * sort) list * (string * typ list) list"} \\
- @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"}
+ @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
\end{mldecls}
\begin{description}
@@ -61,7 +61,7 @@
a datatype to executable content, with generation
set @{text cs}.
- \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
+ \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
returns type constructor corresponding to
constructor @{text const}; returns @{text NONE}
if @{text const} is no constructor.
@@ -105,7 +105,7 @@
merge, which is a little bit nasty from an implementation
point of view. The framework provides a solution
to this technical challenge by providing a functorial
- data slot @{ML_functor CodeDataFun}; on instantiation
+ data slot @{ML_functor Code_Data}; on instantiation
of this functor, the following types and operations
are required:
@@ -131,7 +131,7 @@
\end{description}
- \noindent An instance of @{ML_functor CodeDataFun} provides the following
+ \noindent An instance of @{ML_functor Code_Data} provides the following
interface:
\medskip
--- a/doc-src/Codegen/Thy/Program.thy Mon May 31 18:17:48 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Mon May 31 19:36:13 2010 +0200
@@ -172,22 +172,22 @@
\item replacing non-executable constructs by executable ones:
*}
-lemma %quote [code_inline]:
- "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+ "x \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
text {*
\item eliminating superfluous constants:
*}
-lemma %quote [code_inline]:
- "1 = Suc 0" by simp
+lemma %quote [code_unfold]:
+ "1 = Suc 0" by (fact One_nat_def)
text {*
\item replacing executable but inconvenient constructs:
*}
-lemma %quote [code_inline]:
- "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+ "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
text_raw {*
\end{itemize}
--- a/doc-src/Codegen/Thy/document/ML.tex Mon May 31 18:17:48 2010 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex Mon May 31 19:36:13 2010 +0200
@@ -60,9 +60,9 @@
\verb| -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
- \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
\verb| -> (string * sort) list * (string * typ list) list| \\
- \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
\end{mldecls}
\begin{description}
@@ -91,7 +91,7 @@
a datatype to executable content, with generation
set \isa{cs}.
- \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
+ \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
returns type constructor corresponding to
constructor \isa{const}; returns \isa{NONE}
if \isa{const} is no constructor.
@@ -163,7 +163,7 @@
merge, which is a little bit nasty from an implementation
point of view. The framework provides a solution
to this technical challenge by providing a functorial
- data slot \verb|CodeDataFun|; on instantiation
+ data slot \verb|Code_Data|; on instantiation
of this functor, the following types and operations
are required:
@@ -189,7 +189,7 @@
\end{description}
- \noindent An instance of \verb|CodeDataFun| provides the following
+ \noindent An instance of \verb|Code_Data| provides the following
interface:
\medskip
--- a/doc-src/Codegen/Thy/document/Program.tex Mon May 31 18:17:48 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Mon May 31 19:36:13 2010 +0200
@@ -432,9 +432,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -453,9 +453,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp%
+\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -474,9 +474,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -763,7 +763,7 @@
%
\begin{isamarkuptext}%
\noindent The membership test during preprocessing is rewritten,
- resulting in \isa{op\ mem}, which itself
+ resulting in \isa{member}, which itself
performs an explicit equality check.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -781,7 +781,7 @@
\hspace*{0pt} ~type 'a eq\\
\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq -> 'a -> 'a list -> bool\\
+\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
\hspace*{0pt} ~val collect{\char95}duplicates :\\
\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
\hspace*{0pt}end = struct\\
@@ -791,13 +791,13 @@
\hspace*{0pt}\\
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt}fun member A{\char95}~[] y = false\\
+\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
\hspace*{0pt}\\
\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
-\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
-\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
+\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
+\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
\hspace*{0pt}\\
@@ -968,11 +968,10 @@
\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1290,7 +1289,7 @@
%
\begin{isamarkuptext}%
\begin{isabelle}%
-lexord\ r\ {\isasymequiv}\isanewline
+lexord\ r\ {\isacharequal}\isanewline
{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%
--- a/src/HOL/Nitpick.thy Mon May 31 18:17:48 2010 +0200
+++ b/src/HOL/Nitpick.thy Mon May 31 19:36:13 2010 +0200
@@ -69,6 +69,9 @@
apply (erule_tac x = y in allE)
by (auto simp: mem_def)
+lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
+by (simp add: prod_case_unfold split_def)
+
lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
by simp
@@ -245,12 +248,12 @@
less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
-hide_fact (open) 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
- nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
- num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
- uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
- of_frac_def
+hide_fact (open) If_def Ex1_def split_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 nat_lcm_def int_gcd_def int_lcm_def Frac_def
+ zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
+ plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
+ inverse_frac_def less_eq_frac_def of_frac_def
end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 18:17:48 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 19:36:13 2010 +0200
@@ -945,21 +945,32 @@
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
step subst orig_assm_ts orig_t =
- if getenv "KODKODI" = "" then
- (if auto then ()
- else warning (Pretty.string_of (plazy install_kodkodi_message));
- ("unknown", state))
- else
- let
- val deadline = Option.map (curry Time.+ (Time.now ())) timeout
- val outcome as (outcome_code, _) =
- time_limit (if debug then NONE else timeout)
- (pick_them_nits_in_term deadline state params auto i n step subst
- orig_assm_ts) orig_t
- in
- if expect = "" orelse outcome_code = expect then outcome
- else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
- end
+ let
+ val warning_m = if auto then K () else warning
+ val unknown_outcome = ("unknown", state)
+ in
+ if getenv "KODKODI" = "" then
+ (warning_m (Pretty.string_of (plazy install_kodkodi_message));
+ unknown_outcome)
+ else
+ let
+ val deadline = Option.map (curry Time.+ (Time.now ())) timeout
+ val outcome as (outcome_code, _) =
+ time_limit (if debug then NONE else timeout)
+ (pick_them_nits_in_term deadline state params auto i n step subst
+ orig_assm_ts) orig_t
+ handle TOO_LARGE (_, details) =>
+ (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ | TOO_SMALL (_, details) =>
+ (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ | Kodkod.SYNTAX (_, details) =>
+ (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
+ unknown_outcome)
+ in
+ if expect = "" orelse outcome_code = expect then outcome
+ else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ end
+ end
fun is_fixed_equation fixes
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon May 31 18:17:48 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon May 31 19:36:13 2010 +0200
@@ -1663,8 +1663,7 @@
(* TODO: Move to "Nitpick.thy" *)
val basic_ersatz_table =
- [(@{const_name prod_case}, @{const_name split}),
- (@{const_name card}, @{const_name card'}),
+ [(@{const_name card}, @{const_name card'}),
(@{const_name setsum}, @{const_name setsum'}),
(@{const_name fold_graph}, @{const_name fold_graph'}),
(@{const_name wf}, @{const_name wf'}),
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 31 18:17:48 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 31 19:36:13 2010 +0200
@@ -316,10 +316,6 @@
error ("Invalid term" ^ plural_s_for_list ts ^
" (" ^ quote loc ^ "): " ^
commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
- | TOO_LARGE (_, details) =>
- (warning ("Limit reached: " ^ details ^ "."); x)
- | TOO_SMALL (_, details) =>
- (warning ("Limit reached: " ^ details ^ "."); x)
| TYPE (loc, Ts, ts) =>
error ("Invalid type" ^ plural_s_for_list Ts ^
(if null ts then
@@ -329,8 +325,6 @@
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
" (" ^ quote loc ^ "): " ^
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
- | Kodkod.SYNTAX (_, details) =>
- (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")