# HG changeset patch # User haftmann # Date 1255072465 -7200 # Node ID 2b2c56530d257256c60aaee4236fe35578b5f0a3 # Parent c7cd4d3852dd4c8300d16dd5daf561333429b5a9# Parent 99cd75a18b78bbe2d68b56e3e9688116952851b3 merged diff -r c7cd4d3852dd -r 2b2c56530d25 NEWS --- a/NEWS Thu Oct 08 20:56:40 2009 +0200 +++ b/NEWS Fri Oct 09 09:14:25 2009 +0200 @@ -24,6 +24,12 @@ in proofs are not shown. +*** document preparation *** + +* New generalized style concept for printing terms: +write @{foo (style) ...} instead of @{foo_style style ...}. + + *** HOL *** * Most rules produced by inductive and datatype package diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Oct 09 09:14:25 2009 +0200 @@ -145,8 +145,6 @@ @{antiquotation_def abbrev} & : & @{text antiquotation} \\ @{antiquotation_def typeof} & : & @{text antiquotation} \\ @{antiquotation_def typ} & : & @{text antiquotation} \\ - @{antiquotation_def thm_style} & : & @{text antiquotation} \\ - @{antiquotation_def term_style} & : & @{text antiquotation} \\ @{antiquotation_def "text"} & : & @{text antiquotation} \\ @{antiquotation_def goals} & : & @{text antiquotation} \\ @{antiquotation_def subgoals} & : & @{text antiquotation} \\ @@ -182,16 +180,14 @@ antiquotation: 'theory' options name | - 'thm' options thmrefs | + 'thm' options styles thmrefs | 'lemma' options prop 'by' method | - 'prop' options prop | - 'term' options term | + 'prop' options styles prop | + 'term' options styles term | 'const' options term | 'abbrev' options term | 'typeof' options term | 'typ' options type | - 'thm\_style' options name thmref | - 'term\_style' options name term | 'text' options name | 'goals' options | 'subgoals' options | @@ -205,6 +201,10 @@ ; option: name | name '=' name ; + styles: '(' (style + ',') ')' + ; + style: (name +) + ; \end{rail} Note that the syntax of antiquotations may \emph{not} include source @@ -241,12 +241,6 @@ \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. - \item @{text "@{thm_style s a}"} prints theorem @{text a}, - previously applying a style @{text s} to it (see below). - - \item @{text "@{term_style s t}"} prints a well-typed term @{text t} - after applying a style @{text s} to it (see below). - \item @{text "@{text s}"} prints uninterpreted source text @{text s}. This is particularly useful to print portions of text according to the Isabelle document style, without demanding well-formedness, @@ -285,9 +279,11 @@ subsubsection {* Styled antiquotations *} -text {* Some antiquotations like @{text thm_style} and @{text - term_style} admit an extra \emph{style} specification to modify the - printed result. The following standard styles are available: +text {* The antiquotations @{text thm}, @{text prop} and @{text + term} admit an extra \emph{style} specification to modify the + printed result. A style is specified by a name with a possibly + empty number of arguments; multiple styles can be sequenced with + commas. The following standard styles are available: \begin{description} @@ -301,8 +297,8 @@ \item @{text "concl"} extracts the conclusion @{text C} from a rule in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"}. - \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number - @{text "1, \, 9"}, respectively, from from a rule in Horn-clause + \item @{text "prem"} @{text n} extract premise number + @{text "n"} from from a rule in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} \end{description} diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Oct 09 09:14:25 2009 +0200 @@ -163,8 +163,6 @@ \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\ - \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\ - \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\ @@ -200,16 +198,14 @@ antiquotation: 'theory' options name | - 'thm' options thmrefs | + 'thm' options styles thmrefs | 'lemma' options prop 'by' method | - 'prop' options prop | - 'term' options term | + 'prop' options styles prop | + 'term' options styles term | 'const' options term | 'abbrev' options term | 'typeof' options term | 'typ' options type | - 'thm\_style' options name thmref | - 'term\_style' options name term | 'text' options name | 'goals' options | 'subgoals' options | @@ -223,6 +219,10 @@ ; option: name | name '=' name ; + styles: '(' (style + ',') ')' + ; + style: (name +) + ; \end{rail} Note that the syntax of antiquotations may \emph{not} include source @@ -257,12 +257,6 @@ \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. - \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}} prints theorem \isa{a}, - previously applying a style \isa{s} to it (see below). - - \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{t} - after applying a style \isa{s} to it (see below). - \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}} prints uninterpreted source text \isa{s}. This is particularly useful to print portions of text according to the Isabelle document style, without demanding well-formedness, e.g.\ small pieces of terms that should not be parsed or @@ -301,8 +295,10 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Some antiquotations like \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} admit an extra \emph{style} specification to modify the - printed result. The following standard styles are available: +The antiquotations \isa{thm}, \isa{prop} and \isa{term} admit an extra \emph{style} specification to modify the + printed result. A style is specified by a name with a possibly + empty number of arguments; multiple styles can be sequenced with + commas. The following standard styles are available: \begin{description} @@ -316,8 +312,8 @@ \item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}. - \item \isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}} extract premise number - \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in Horn-clause + \item \isa{{\isachardoublequote}prem{\isachardoublequote}} \isa{n} extract premise number + \isa{{\isachardoublequote}n{\isachardoublequote}} from from a rule in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}} \end{description}% diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Oct 09 09:14:25 2009 +0200 @@ -296,20 +296,20 @@ own way, you can extract the premises and the conclusion explicitly and combine them as you like: \begin{itemize} -\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}! -prints premise 1 of $thm$ (and similarly up to \texttt{prem9}). -\item \verb!@!\verb!{thm_style concl! $thm$\verb!}! +\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! +prints premise 1 of $thm$. +\item \verb!@!\verb!{thm (concl)! $thm$\verb!}! prints the conclusion of $thm$. \end{itemize} -For example, ``from @{thm_style prem2 conjI} and -@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}'' +For example, ``from @{thm (prem 2) conjI} and +@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}'' is produced by \begin{quote} -\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\ -\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}! +\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ +\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! \end{quote} Thus you can rearrange or hide premises and typeset the theorem as you like. -The \verb!thm_style! antiquotation is a general mechanism explained +Styles like !(prem 1)! are a general mechanism explained in \S\ref{sec:styles}. *} @@ -394,26 +394,27 @@ ``styles'': \begin{quote} - \verb!@!\verb!{thm_style stylename thm}!\\ - \verb!@!\verb!{term_style stylename term}! + \verb!@!\verb!{thm (style) thm}!\\ + \verb!@!\verb!{prop (style) thm}!\\ + \verb!@!\verb!{term (style) term}! \end{quote} A ``style'' is a transformation of propositions. There are predefined - styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!. + styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. For example, the output \begin{center} \begin{tabular}{l@ {~~@{text "="}~~}l} - @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\ - @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons} + @{thm (lhs) foldl_Nil} & @{thm (rhs) foldl_Nil}\\ + @{thm (lhs) foldl_Cons} & @{thm (rhs) foldl_Cons} \end{tabular} \end{center} is produced by the following code: \begin{quote} \verb!\begin{center}!\\ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ - \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\ - \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\ + \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\ + \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\ \verb!\end{tabular}!\\ \verb!\end{center}! \end{quote} @@ -431,12 +432,12 @@ \end{center} To print just the conclusion, \begin{center} - @{thm_style [show_types] concl hd_Cons_tl} + @{thm [show_types] (concl) hd_Cons_tl} \end{center} type \begin{quote} \verb!\begin{center}!\\ - \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\ + \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\ \verb!\end{center}! \end{quote} Beware that any options must be placed \emph{before} @@ -445,49 +446,7 @@ Further use cases can be found in \S\ref{sec:yourself}. If you are not afraid of ML, you may also define your own styles. - A style is implemented by an ML function of type - \verb!Proof.context -> term -> term!. - Have a look at the following example: - -*} -(*<*) -setup {* -let - fun my_concl ctxt = Logic.strip_imp_concl - in TermStyle.add_style "my_concl" my_concl -end; -*} -(*>*) -text {* - - \begin{quote} - \verb!setup {!\verb!*!\\ - \verb!let!\\ - \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\ - \verb! in TermStyle.add_style "my_concl" my_concl!\\ - \verb!end;!\\ - \verb!*!\verb!}!\\ - \end{quote} - - \noindent - This example shows how the \verb!concl! style is implemented - and may be used as as a ``copy-and-paste'' pattern to write your own styles. - - The code should go into your theory file, separate from the \LaTeX\ text. - The \verb!let! expression avoids polluting the - ML global namespace. Each style receives the current proof context - as first argument; this is helpful in situations where the - style has some object-logic specific behaviour for example. - - The mapping from identifier name to the style function - is done by the @{ML TermStyle.add_style} expression which expects the desired - style name and the style function as arguments. - - After this \verb!setup!, - there will be a new style available named \verb!my_concl!, thus allowing - antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}! - yielding @{thm_style my_concl hd_Cons_tl}. - + Have a look at module @{ML_struct Term_Style}. *} (*<*) diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Oct 09 09:14:25 2009 +0200 @@ -390,20 +390,20 @@ own way, you can extract the premises and the conclusion explicitly and combine them as you like: \begin{itemize} -\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}! -prints premise 1 of $thm$ (and similarly up to \texttt{prem9}). -\item \verb!@!\verb!{thm_style concl! $thm$\verb!}! +\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! +prints premise 1 of $thm$. +\item \verb!@!\verb!{thm (concl)! $thm$\verb!}! prints the conclusion of $thm$. \end{itemize} For example, ``from \isa{Q} and \isa{P} we conclude \isa{P\ {\isasymand}\ Q}'' is produced by \begin{quote} -\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\ -\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}! +\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ +\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! \end{quote} Thus you can rearrange or hide premises and typeset the theorem as you like. -The \verb!thm_style! antiquotation is a general mechanism explained +Styles like !(prem 1)! are a general mechanism explained in \S\ref{sec:styles}.% \end{isamarkuptext}% \isamarkuptrue% @@ -516,12 +516,13 @@ ``styles'': \begin{quote} - \verb!@!\verb!{thm_style stylename thm}!\\ - \verb!@!\verb!{term_style stylename term}! + \verb!@!\verb!{thm (style) thm}!\\ + \verb!@!\verb!{prop (style) thm}!\\ + \verb!@!\verb!{term (style) term}! \end{quote} A ``style'' is a transformation of propositions. There are predefined - styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!. + styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. For example, the output \begin{center} @@ -534,8 +535,8 @@ \begin{quote} \verb!\begin{center}!\\ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ - \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\ - \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\ + \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\ + \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\ \verb!\end{tabular}!\\ \verb!\end{center}! \end{quote} @@ -558,7 +559,7 @@ type \begin{quote} \verb!\begin{center}!\\ - \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\ + \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\ \verb!\end{center}! \end{quote} Beware that any options must be placed \emph{before} @@ -567,53 +568,7 @@ Further use cases can be found in \S\ref{sec:yourself}. If you are not afraid of ML, you may also define your own styles. - A style is implemented by an ML function of type - \verb!Proof.context -> term -> term!. - Have a look at the following example:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% -\begin{isamarkuptext}% -\begin{quote} - \verb!setup {!\verb!*!\\ - \verb!let!\\ - \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\ - \verb! in TermStyle.add_style "my_concl" my_concl!\\ - \verb!end;!\\ - \verb!*!\verb!}!\\ - \end{quote} - - \noindent - This example shows how the \verb!concl! style is implemented - and may be used as as a ``copy-and-paste'' pattern to write your own styles. - - The code should go into your theory file, separate from the \LaTeX\ text. - The \verb!let! expression avoids polluting the - ML global namespace. Each style receives the current proof context - as first argument; this is helpful in situations where the - style has some object-logic specific behaviour for example. - - The mapping from identifier name to the style function - is done by the \verb|TermStyle.add_style| expression which expects the desired - style name and the style function as arguments. - - After this \verb!setup!, - there will be a new style available named \verb!my_concl!, thus allowing - antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}! - yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.% + Have a look at module \verb|Term_Style|.% \end{isamarkuptext}% \isamarkuptrue% % diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Fri Oct 09 09:14:25 2009 +0200 @@ -185,7 +185,7 @@ Even with its use of the function \isa{lists}, the premise of our introduction rule is positive: -@{thm_style [display,indent=0] prem1 step [no_vars]} +@{thm [display,indent=0] (prem 1) step [no_vars]} To apply the rule we construct a list @{term args} of previously constructed well-formed terms. We obtain a new term, @{term "Apply f args"}. Because @{term lists} is monotone, diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/TutorialI/Inductive/Star.thy --- a/doc-src/TutorialI/Inductive/Star.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/TutorialI/Inductive/Star.thy Fri Oct 09 09:14:25 2009 +0200 @@ -54,7 +54,7 @@ To prove transitivity, we need rule induction, i.e.\ theorem @{thm[source]rtc.induct}: @{thm[display]rtc.induct} -It says that @{text"?P"} holds for an arbitrary pair @{thm_style prem1 rtc.induct} +It says that @{text"?P"} holds for an arbitrary pair @{thm (prem 1) rtc.induct} if @{text"?P"} is preserved by all rules of the inductive definition, i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the premises. In general, rule induction for an $n$-ary inductive relation $R$ diff -r c7cd4d3852dd -r 2b2c56530d25 doc-src/TutorialI/Protocol/NS_Public.thy --- a/doc-src/TutorialI/Protocol/NS_Public.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy Fri Oct 09 09:14:25 2009 +0200 @@ -375,7 +375,7 @@ From similar assumptions, we can prove that @{text A} started the protocol run by sending an instance of message~1 involving the nonce~@{text NA}\@. For this theorem, the conclusion is -@{thm_style [display] concl B_trusts_protocol [no_vars]} +@{thm [display] (concl) B_trusts_protocol [no_vars]} Analogous theorems can be proved for~@{text A}, stating that nonce~@{text NA} remains secret and that message~2 really originates with~@{text B}. Even the flawed protocol establishes these properties for~@{text A}; diff -r c7cd4d3852dd -r 2b2c56530d25 src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Thu Oct 08 20:56:40 2009 +0200 +++ b/src/HOL/Library/OptionalSugar.thy Fri Oct 09 09:14:25 2009 +0200 @@ -29,7 +29,7 @@ "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" -(* deprecated, use thm_style instead, will be removed *) +(* deprecated, use thm with style instead, will be removed *) (* aligning equations *) notation (tab output) "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and diff -r c7cd4d3852dd -r 2b2c56530d25 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 09 09:14:25 2009 +0200 @@ -22,7 +22,7 @@ val the_spec : theory -> string -> (string * sort) list * (string * typ list) list val get_constrs : theory -> string -> (string * typ) list option val get_all : theory -> info Symtab.table - val info_of_constr : theory -> string -> info option + val info_of_constr : theory -> string * typ -> info option val info_of_case : theory -> string -> info option val interpretation : (config -> string list -> theory -> theory) -> theory -> theory val distinct_simproc : simproc @@ -47,7 +47,7 @@ ( type T = {types: info Symtab.table, - constrs: info Symtab.table, + constrs: (string * info) list Symtab.table, cases: info Symtab.table}; val empty = @@ -58,7 +58,7 @@ ({types = types1, constrs = constrs1, cases = cases1}, {types = types2, constrs = constrs2, cases = cases2}) = {types = Symtab.merge (K true) (types1, types2), - constrs = Symtab.merge (K true) (constrs1, constrs2), + constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2), cases = Symtab.merge (K true) (cases1, cases2)}; ); @@ -68,18 +68,32 @@ SOME info => info | NONE => error ("Unknown datatype " ^ quote name)); -val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get; +fun info_of_constr thy (c, T) = + let + val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c; + val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE; + val default = if null tab then NONE + else SOME (snd (Library.last_elem tab)) + (*conservative wrt. overloaded constructors*); + in case hint + of NONE => default + | SOME tyco => case AList.lookup (op =) tab tyco + of NONE => default (*permissive*) + | SOME info => SOME info + end; + val info_of_case = Symtab.lookup o #cases o DatatypesData.get; fun register (dt_infos : (string * info) list) = DatatypesData.map (fn {types, constrs, cases} => - {types = fold Symtab.update dt_infos types, - constrs = fold Symtab.default (*conservative wrt. overloaded constructors*) - (maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst) - (#3 (the (AList.lookup op = descr index)))) dt_infos) constrs, - cases = fold Symtab.update - (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos) - cases}); + {types = types |> fold Symtab.update dt_infos, + constrs = constrs |> fold (fn (constr, dtname_info) => + Symtab.map_default (constr, []) (cons dtname_info)) + (maps (fn (dtname, info as {descr, index, ...}) => + map (rpair (dtname, info) o fst) + (#3 (the (AList.lookup op = descr index)))) dt_infos), + cases = cases |> fold Symtab.update + (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}); (* complex queries *) diff -r c7cd4d3852dd -r 2b2c56530d25 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Oct 09 09:14:25 2009 +0200 @@ -8,14 +8,14 @@ signature DATATYPE_CASE = sig datatype config = Error | Warning | Quiet; - val make_case: (string -> DatatypeAux.info option) -> + val make_case: (string * typ -> DatatypeAux.info option) -> Proof.context -> config -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list val dest_case: (string -> DatatypeAux.info option) -> bool -> string list -> term -> (term * (term * term) list) option val strip_case: (string -> DatatypeAux.info option) -> bool -> term -> (term * (term * term) list) option - val case_tr: bool -> (theory -> string -> DatatypeAux.info option) + val case_tr: bool -> (theory -> string * typ -> DatatypeAux.info option) -> Proof.context -> term list -> term val case_tr': (theory -> string -> DatatypeAux.info option) -> string -> Proof.context -> term list -> term @@ -34,9 +34,9 @@ * Get information about datatypes *---------------------------------------------------------------------------*) -fun ty_info (tab : string -> DatatypeAux.info option) s = - case tab s of - SOME {descr, case_name, index, sorts, ...} => +fun ty_info tab sT = + case tab sT of + SOME ({descr, case_name, index, sorts, ...} : DatatypeAux.info) => let val (_, (tname, dts, constrs)) = nth descr index; val mk_ty = DatatypeAux.typ_of_dtyp descr sorts; @@ -216,7 +216,7 @@ pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows); val (pref_patl, tm) = mk {path = rstp, rows = rows'} in (map v_to_pats pref_patl, tm) end - | SOME (Const (cname, cT), i) => (case ty_info tab cname of + | SOME (Const (cname, cT), i) => (case ty_info tab (cname, cT) of NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i) | SOME {case_name, constructors} => let diff -r c7cd4d3852dd -r 2b2c56530d25 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Oct 09 09:14:25 2009 +0200 @@ -281,7 +281,7 @@ if is_some (get_assoc_code thy (s, T)) then NONE else SOME (pretty_case thy defs dep module brack (#3 (the (AList.lookup op = descr index))) c ts gr ) - | NONE => case (Datatype.info_of_constr thy s, strip_type T) of + | NONE => case (Datatype.info_of_constr thy (s, T), strip_type T) of (SOME {index, descr, ...}, (_, U as Type (tyname, _))) => if is_some (get_assoc_code thy (s, T)) then NONE else let diff -r c7cd4d3852dd -r 2b2c56530d25 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Fri Oct 09 09:14:25 2009 +0200 @@ -40,7 +40,7 @@ let val (hd, args) = strip_comb t in - (((case Datatype.info_of_constr thy (fst (dest_Const hd)) of + (((case Datatype.info_of_constr thy (dest_Const hd) of SOME _ => () | NONE => err "Non-constructor pattern") handle TERM ("dest_Const", _) => err "Non-constructor patterns"); diff -r c7cd4d3852dd -r 2b2c56530d25 src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/Pure/Thy/term_style.ML Fri Oct 09 09:14:25 2009 +0200 @@ -1,18 +1,17 @@ (* Title: Pure/Thy/term_style.ML Author: Florian Haftmann, TU Muenchen -Styles for terms, to use with the "term_style" and "thm_style" -antiquotations. +Styles for term printing. *) signature TERM_STYLE = sig - val the_style: theory -> string -> (Proof.context -> term -> term) - val add_style: string -> (Proof.context -> term -> term) -> theory -> theory - val print_styles: theory -> unit + val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory + val parse: (term -> term) context_parser + val parse_bare: (term -> term) context_parser end; -structure TermStyle: TERM_STYLE = +structure Term_Style: TERM_STYLE = struct (* style data *) @@ -22,7 +21,7 @@ structure StyleData = TheoryDataFun ( - type T = ((Proof.context -> term -> term) * stamp) Symtab.table; + type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; val empty = Symtab.empty; val copy = I; val extend = I; @@ -30,9 +29,6 @@ handle Symtab.DUP dup => err_dup_style dup; ); -fun print_styles thy = - Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy))); - (* accessors *) @@ -41,51 +37,83 @@ NONE => error ("Unknown antiquote style: " ^ quote name) | SOME (style, _) => style); -fun add_style name style thy = +fun setup name style thy = StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy handle Symtab.DUP _ => err_dup_style name; +(* style parsing *) + +fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse) + >> (fn x as ((name, _), _) => fst (Args.context_syntax "style" + (Scan.lift (the_style (ProofContext.theory_of ctxt) name)) + (Args.src x) ctxt |>> (fn f => f ctxt))); + +val parse = Args.context :|-- (fn ctxt => Scan.lift + (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt)) + >> fold I + || Scan.succeed I)); + +val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name + >> (fn name => fst (Args.context_syntax "style" + (Scan.lift (the_style (ProofContext.theory_of ctxt) name)) + (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))); + + (* predefined styles *) -fun style_binargs ctxt t = +fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => let val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t) in - case concl of (_ $ l $ r) => (l, r) + case concl of (_ $ l $ r) => proj (l, r) | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) - end; + end); -fun style_parm_premise i ctxt t = - let val prems = Logic.strip_imp_prems t in +val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t => + let + val i = (the o Int.fromString) raw_i; + val prems = Logic.strip_imp_prems t; + in + if i <= length prems then nth prems (i - 1) + else error ("Not enough premises for prem " ^ string_of_int i ^ + " in propositon: " ^ Syntax.string_of_term ctxt t) + end); + +fun style_parm_premise i = Scan.succeed (fn ctxt => fn t => + let + val i_str = string_of_int i; + val prems = Logic.strip_imp_prems t; + in if i <= length prems then nth prems (i - 1) else error ("Not enough premises for prem" ^ string_of_int i ^ " in propositon: " ^ Syntax.string_of_term ctxt t) - end; + end); val _ = Context.>> (Context.map_theory - (add_style "lhs" (fst oo style_binargs) #> - add_style "rhs" (snd oo style_binargs) #> - add_style "prem1" (style_parm_premise 1) #> - add_style "prem2" (style_parm_premise 2) #> - add_style "prem3" (style_parm_premise 3) #> - add_style "prem4" (style_parm_premise 4) #> - add_style "prem5" (style_parm_premise 5) #> - add_style "prem6" (style_parm_premise 6) #> - add_style "prem7" (style_parm_premise 7) #> - add_style "prem8" (style_parm_premise 8) #> - add_style "prem9" (style_parm_premise 9) #> - add_style "prem10" (style_parm_premise 10) #> - add_style "prem11" (style_parm_premise 11) #> - add_style "prem12" (style_parm_premise 12) #> - add_style "prem13" (style_parm_premise 13) #> - add_style "prem14" (style_parm_premise 14) #> - add_style "prem15" (style_parm_premise 15) #> - add_style "prem16" (style_parm_premise 16) #> - add_style "prem17" (style_parm_premise 17) #> - add_style "prem18" (style_parm_premise 18) #> - add_style "prem19" (style_parm_premise 19) #> - add_style "concl" (K Logic.strip_imp_concl))); + (setup "lhs" (style_lhs_rhs fst) #> + setup "rhs" (style_lhs_rhs snd) #> + setup "prem" style_prem #> + setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #> + setup "prem1" (style_parm_premise 1) #> + setup "prem2" (style_parm_premise 2) #> + setup "prem3" (style_parm_premise 3) #> + setup "prem4" (style_parm_premise 4) #> + setup "prem5" (style_parm_premise 5) #> + setup "prem6" (style_parm_premise 6) #> + setup "prem7" (style_parm_premise 7) #> + setup "prem8" (style_parm_premise 8) #> + setup "prem9" (style_parm_premise 9) #> + setup "prem10" (style_parm_premise 10) #> + setup "prem11" (style_parm_premise 11) #> + setup "prem12" (style_parm_premise 12) #> + setup "prem13" (style_parm_premise 13) #> + setup "prem14" (style_parm_premise 14) #> + setup "prem15" (style_parm_premise 15) #> + setup "prem16" (style_parm_premise 16) #> + setup "prem17" (style_parm_premise 17) #> + setup "prem18" (style_parm_premise 18) #> + setup "prem19" (style_parm_premise 19))); end; diff -r c7cd4d3852dd -r 2b2c56530d25 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Oct 09 09:14:25 2009 +0200 @@ -470,11 +470,11 @@ fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; -fun pretty_term_style ctxt (name, t) = - pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t); +fun pretty_term_style ctxt (style, t) = + pretty_term ctxt (style t); -fun pretty_thm_style ctxt (name, th) = - pretty_term_style ctxt (name, Thm.full_prop_of th); +fun pretty_thm_style ctxt (style, th) = + pretty_term_style ctxt (style, Thm.full_prop_of th); fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full; @@ -513,15 +513,19 @@ fun basic_entities name scan pretty = antiquotation name scan (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source); +fun basic_entities_style name scan pretty = antiquotation name scan + (fn {source, context, ...} => fn (style, xs) => + output (maybe_pretty_source (fn x => pretty context (style, x)) source xs)); + fun basic_entity name scan = basic_entities name (scan >> single); in -val _ = basic_entities "thm" Attrib.thms pretty_thm; -val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style; -val _ = basic_entity "prop" Args.prop pretty_term; -val _ = basic_entity "term" Args.term pretty_term; -val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style; +val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style; +val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style; +val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style; +val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style; +val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style; val _ = basic_entity "term_type" Args.term pretty_term_typ; val _ = basic_entity "typeof" Args.term pretty_term_typeof; val _ = basic_entity "const" Args.const_proper pretty_const; diff -r c7cd4d3852dd -r 2b2c56530d25 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/Tools/Code/code_target.ML Fri Oct 09 09:14:25 2009 +0200 @@ -386,21 +386,6 @@ local -fun labelled_name thy program name = case Graph.get_node program name - of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c) - | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) - | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c) - | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class) - | Code_Thingol.Classrel (sub, super) => let - val Code_Thingol.Class (sub, _) = Graph.get_node program sub - val Code_Thingol.Class (super, _) = Graph.get_node program super - in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end - | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c) - | Code_Thingol.Classinst ((class, (tyco, _)), _) => let - val Code_Thingol.Class (class, _) = Graph.get_node program class - val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco - in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end - fun activate_syntax lookup_name src_tab = Symtab.empty |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier of SOME name => (SOME name, @@ -440,7 +425,7 @@ val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); in - serializer module args (labelled_name thy program2) reserved includes + serializer module args (Code_Thingol.labelled_name thy program2) reserved includes (Symtab.lookup module_alias) (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const') program4 names2 diff -r c7cd4d3852dd -r 2b2c56530d25 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Oct 08 20:56:40 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Oct 09 09:14:25 2009 +0200 @@ -78,6 +78,10 @@ val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_cons: program -> string -> bool val contr_classparam_typs: program -> string -> itype option list + val labelled_name: theory -> program -> string -> string + val group_stmts: theory -> program + -> ((string * stmt) list * (string * stmt) list + * ((string * stmt) list * (string * stmt) list)) list val expand_eta: theory -> int -> thm -> thm val clean_thms: theory -> thm list -> thm list @@ -492,6 +496,45 @@ end | _ => []; +fun labelled_name thy program name = case Graph.get_node program name + of Fun (c, _) => quote (Code.string_of_const thy c) + | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) + | Datatypecons (c, _) => quote (Code.string_of_const thy c) + | Class (class, _) => "class " ^ quote (Sign.extern_class thy class) + | Classrel (sub, super) => let + val Class (sub, _) = Graph.get_node program sub + val Class (super, _) = Graph.get_node program super + in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end + | Classparam (c, _) => quote (Code.string_of_const thy c) + | Classinst ((class, (tyco, _)), _) => let + val Class (class, _) = Graph.get_node program class + val Datatype (tyco, _) = Graph.get_node program tyco + in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end + +fun group_stmts thy program = + let + fun is_fun (_, Fun _) = true | is_fun _ = false; + fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; + fun is_datatype (_, Datatype _) = true | is_datatype _ = false; + fun is_class (_, Class _) = true | is_class _ = false; + fun is_classrel (_, Classrel _) = true | is_classrel _ = false; + fun is_classparam (_, Classparam _) = true | is_classparam _ = false; + fun is_classinst (_, Classinst _) = true | is_classinst _ = false; + fun group stmts = + if forall (is_datatypecons orf is_datatype) stmts + then (filter is_datatype stmts, [], ([], [])) + else if forall (is_class orf is_classrel orf is_classparam) stmts + then ([], filter is_class stmts, ([], [])) + else if forall (is_fun orf is_classinst) stmts + then ([], [], List.partition is_fun stmts) + else error ("Illegal mutual dependencies: " ^ + (commas o map (labelled_name thy program o fst)) stmts) + in + rev (Graph.strong_conn program) + |> map (AList.make (Graph.get_node program)) + |> map group + end; + (** translation kernel **)