--- 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
--- 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 \<tau>}"} prints a well-formed type @{text "\<tau>"}.
- \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 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
- \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
- @{text "1, \<dots>, 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 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
\end{description}
--- 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}%
--- 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}.
*}
(*<*)
--- 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%
%
--- 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,
--- 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$
--- 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};
--- 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
--- 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 *)
--- 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
--- 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
--- 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");
--- 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;
--- 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;
--- 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
--- 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 **)