# HG changeset patch # User wenzelm # Date 1275327373 -7200 # Node ID 91dfe7dccfdfd6948af3a516bd9143de0d569f5d # Parent 47d1ee50205b44bf19bce1e362cc64a1abca29b9# Parent 1c8cf00489347baff3bcec248e79e3af21f5b9c2 merged diff -r 1c8cf0048934 -r 91dfe7dccfdf doc-src/Codegen/Thy/Further.thy --- 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. diff -r 1c8cf0048934 -r 91dfe7dccfdf doc-src/Codegen/Thy/ML.thy --- 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 diff -r 1c8cf0048934 -r 91dfe7dccfdf doc-src/Codegen/Thy/Program.thy --- 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 \ set xs \ x mem xs" by (induct xs) simp_all +lemma %quote [code_unfold]: + "x \ set xs \ 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 = [] \ List.null xs" by (induct xs) simp_all +lemma %quote [code_unfold]: + "xs = [] \ List.null xs" by (fact empty_null) text_raw {* \end{itemize} diff -r 1c8cf0048934 -r 91dfe7dccfdf doc-src/Codegen/Thy/document/ML.tex --- 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 diff -r 1c8cf0048934 -r 91dfe7dccfdf doc-src/Codegen/Thy/document/Program.tex --- 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}% diff -r 1c8cf0048934 -r 91dfe7dccfdf src/HOL/Nitpick.thy --- 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 = (\p. f (fst p) (snd p))" +by (simp add: prod_case_unfold split_def) + lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \ (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 diff -r 1c8cf0048934 -r 91dfe7dccfdf src/HOL/Tools/Nitpick/nitpick.ML --- 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 _) = diff -r 1c8cf0048934 -r 91dfe7dccfdf src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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'}), diff -r 1c8cf0048934 -r 91dfe7dccfdf src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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 ^ ".")