# HG changeset patch # User wenzelm # Date 1328376784 -3600 # Node ID 465851ba524e4829c491c8d56558f4ef437c12fc # Parent d0199d9f9c5b42535b10a4c3682238d0f0ef8a4b updated/unified section on mixfix annotations; diff -r d0199d9f9c5b -r 465851ba524e doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 16:08:19 2012 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 18:33:04 2012 +0100 @@ -335,8 +335,15 @@ text {* Mixfix annotations specify concrete \emph{inner syntax} of Isabelle types and terms. Locally fixed parameters in toplevel - theorem statements, locale specifications etc.\ also admit mixfix - annotations. + theorem statements, locale and class specifications also admit + mixfix annotations in a fairly uniform manner. A mixfix annotation + describes describes the concrete syntax, the translation to abstract + syntax, and the pretty printing. Special case annotations provide a + simple means of specifying infix operators and binders. + + Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows + to specify any context-free priority grammar, which is more general + than the fixity declarations of ML and Prolog. @{rail " @{syntax_def mixfix}: '(' mfix ')' @@ -344,29 +351,34 @@ @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')' ; - mfix: @{syntax string} prios? @{syntax nat}? | - (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} | - @'binder' @{syntax string} prios? @{syntax nat} + mfix: @{syntax template} prios? @{syntax nat}? | + (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} | + @'binder' @{syntax template} prios? @{syntax nat} + ; + template: string ; prios: '[' (@{syntax nat} + ',') ']' "} - Here the @{syntax string} specifications refer to the actual mixfix - template, which may include literal text, spacing, blocks, and - arguments (denoted by ``@{text _}''); the special symbol - ``@{verbatim "\"}'' (printed as ``@{text "\"}'') represents an index - argument that specifies an implicit structure reference (see also - \secref{sec:locale}). Infix and binder declarations provide common - abbreviations for particular mixfix declarations. So in practice, - mixfix templates mostly degenerate to literal text for concrete - syntax, such as ``@{verbatim "++"}'' for an infix symbol. + The string given as @{text template} may include literal text, + spacing, blocks, and arguments (denoted by ``@{text _}''); the + special symbol ``@{verbatim "\"}'' (printed as ``@{text "\"}'') + represents an index argument that specifies an implicit structure + reference (see also \secref{sec:locale}). Infix and binder + declarations provide common abbreviations for particular mixfix + declarations. So in practice, mixfix templates mostly degenerate to + literal text for concrete syntax, such as ``@{verbatim "++"}'' for + an infix symbol. +*} - \medskip In full generality, mixfix declarations work as follows. - Suppose a constant @{text "c :: \\<^sub>1 \ \ \\<^sub>n \ \"} is - annotated by @{text "(mixfix [p\<^sub>1, \, p\<^sub>n] p)"}, where @{text - "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \ _ d\<^sub>n"} consisting of - delimiters that surround argument positions as indicated by - underscores. + +subsection {* The general mixfix form *} + +text {* In full generality, mixfix declarations work as follows. + Suppose a constant @{text "c :: \\<^sub>1 \ \ \\<^sub>n \ \"} is annotated by + @{text "(mixfix [p\<^sub>1, \, p\<^sub>n] p)"}, where @{text "mixfix"} is a string + @{text "d\<^sub>0 _ d\<^sub>1 _ \ _ d\<^sub>n"} consisting of delimiters that surround + argument positions as indicated by underscores. Altogether this determines a production for a context-free priority grammar, where for each argument @{text "i"} the syntactic category @@ -437,16 +449,84 @@ \end{description} - For example, the template @{verbatim "(_ +/ _)"} specifies an infix - operator. There are two argument positions; the delimiter - @{verbatim "+"} is preceded by a space and followed by a space or - line break; the entire phrase is a pretty printing block. - The general idea of pretty printing with blocks and breaks is also described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}. *} +subsection {* Infixes *} + +text {* Infix operators are specified by convenient short forms that + abbreviate general mixfix annotations as follows: + + \begin{center} + \begin{tabular}{lll} + + @{verbatim "("}@{keyword "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} + & @{text "\"} & + @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ + @{verbatim "("}@{keyword "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} + & @{text "\"} & + @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ + @{verbatim "("}@{keyword "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} + & @{text "\"} & + @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ + + \end{tabular} + \end{center} + + The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ + _)\""} specifies two argument positions; the delimiter is preceded + by a space and followed by a space or line break; the entire phrase + is a pretty printing block. + + The alternative notation @{verbatim "op"}~@{text sy} is introduced + in addition. Thus any infix operator may be written in prefix form + (as in ML), independently of the number of arguments in the term. +*} + + +subsection {* Binders *} + +text {* A \emph{binder} is a variable-binding construct such as a + quantifier. The idea to formalize @{text "\x. b"} as @{text "All + (\x. b)"} for @{text "All :: ('a \ bool) \ bool"} already goes back + to \cite{church40}. Isabelle declarations of certain higher-order + operators may be annotated with @{keyword "binder"} annotations as + follows: + + \begin{center} + @{text "c :: "}@{verbatim "\""}@{text "(\\<^sub>1 \ \\<^sub>2) \ \\<^sub>3"}@{verbatim "\" ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"} + \end{center} + + This introduces concrete binder syntax @{text "sy x. b"}, where + @{text x} is a bound variable of type @{text "\\<^sub>1"}, the body @{text + b} has type @{text "\\<^sub>2"} and the whole term has type @{text "\\<^sub>3"}. + The optional integer @{text p} specifies the syntactic priority of + the body; the default is @{text "q"}, which is also the priority of + the whole construct. + + Internally, the binder syntax is expanded to something like this: + \begin{center} + @{text "c_binder :: "}@{verbatim "\""}@{text "idts \ \\<^sub>2 \ \\<^sub>3"}@{verbatim "\" (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"} + \end{center} + + Here @{syntax (inner) idts} is the nonterminal symbol for a list of + identifiers with optional type constraints (see also + \secref{sec:pure-grammar}). The mixfix template @{verbatim + "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions + for the bound identifiers and the body, separated by a dot with + optional line break; the entire phrase is a pretty printing block of + indentation level 3. Note that there is no extra space after @{text + "sy"}, so it needs to be included user specification if the binder + syntax ends with a token that may be continued by an identifier + token at the start of @{syntax (inner) idts}. + + Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1 + \ x\<^sub>n b"} into iterated application @{text "c (\x\<^sub>1. \ c (\x\<^sub>n. b)\)"}. + This works in both directions, for parsing and printing. *} + + section {* Explicit notation \label{sec:notation} *} text {* @@ -630,7 +710,7 @@ *} -subsection {* The Pure grammar *} +subsection {* The Pure grammar \label{sec:pure-grammar} *} text {* The priority grammar of the @{text "Pure"} theory is defined approximately like this: diff -r d0199d9f9c5b -r 465851ba524e doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 16:08:19 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 18:33:04 2012 +0100 @@ -412,8 +412,15 @@ \begin{isamarkuptext}% Mixfix annotations specify concrete \emph{inner syntax} of Isabelle types and terms. Locally fixed parameters in toplevel - theorem statements, locale specifications etc.\ also admit mixfix - annotations. + theorem statements, locale and class specifications also admit + mixfix annotations in a fairly uniform manner. A mixfix annotation + describes describes the concrete syntax, the translation to abstract + syntax, and the pretty printing. Special case annotations provide a + simple means of specifying infix operators and binders. + + Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows + to specify any context-free priority grammar, which is more general + than the fixity declarations of ML and Prolog. \begin{railoutput} \rail@begin{1}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}} @@ -432,7 +439,7 @@ \rail@end \rail@begin{7}{\isa{mfix}} \rail@bar -\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] +\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\isa{prios}}[] @@ -449,11 +456,11 @@ \rail@nextbar{4} \rail@term{\isa{\isakeyword{infixr}}}[] \rail@endbar -\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] +\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@nextbar{5} \rail@term{\isa{\isakeyword{binder}}}[] -\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] +\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] \rail@bar \rail@nextbar{6} \rail@nont{\isa{prios}}[] @@ -461,6 +468,9 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end +\rail@begin{1}{\isa{template}} +\rail@nont{\isa{string}}[] +\rail@end \rail@begin{2}{\isa{prios}} \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[] \rail@plus @@ -473,21 +483,28 @@ \end{railoutput} - Here the \hyperlink{syntax.string}{\mbox{\isa{string}}} specifications refer to the actual mixfix - template, which may include literal text, spacing, blocks, and - arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the special symbol - ``\verb|\|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'') represents an index - argument that specifies an implicit structure reference (see also - \secref{sec:locale}). Infix and binder declarations provide common - abbreviations for particular mixfix declarations. So in practice, - mixfix templates mostly degenerate to literal text for concrete - syntax, such as ``\verb|++|'' for an infix symbol. - - \medskip In full generality, mixfix declarations work as follows. - Suppose a constant \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} is - annotated by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mixfix\ {\isaliteral{5B}{\isacharbrackleft}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}mixfix{\isaliteral{22}{\isachardoublequote}}} is a string \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} consisting of - delimiters that surround argument positions as indicated by - underscores. + The string given as \isa{template} may include literal text, + spacing, blocks, and arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the + special symbol ``\verb|\|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'') + represents an index argument that specifies an implicit structure + reference (see also \secref{sec:locale}). Infix and binder + declarations provide common abbreviations for particular mixfix + declarations. So in practice, mixfix templates mostly degenerate to + literal text for concrete syntax, such as ``\verb|++|'' for + an infix symbol.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The general mixfix form% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +In full generality, mixfix declarations work as follows. + Suppose a constant \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} is annotated by + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mixfix\ {\isaliteral{5B}{\isacharbrackleft}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}mixfix{\isaliteral{22}{\isachardoublequote}}} is a string + \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} consisting of delimiters that surround + argument positions as indicated by underscores. Altogether this determines a production for a context-free priority grammar, where for each argument \isa{{\isaliteral{22}{\isachardoublequote}}i{\isaliteral{22}{\isachardoublequote}}} the syntactic category @@ -558,16 +575,86 @@ \end{description} - For example, the template \verb|(_ +/ _)| specifies an infix - operator. There are two argument positions; the delimiter - \verb|+| is preceded by a space and followed by a space or - line break; the entire phrase is a pretty printing block. - The general idea of pretty printing with blocks and breaks is also described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.% \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Infixes% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Infix operators are specified by convenient short forms that + abbreviate general mixfix annotations as follows: + + \begin{center} + \begin{tabular}{lll} + + \verb|(|\hyperlink{keyword.infix}{\mbox{\isa{\isakeyword{infix}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)| + & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & + \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\ + \verb|(|\hyperlink{keyword.infixl}{\mbox{\isa{\isakeyword{infixl}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)| + & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & + \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\ + \verb|(|\hyperlink{keyword.infixr}{\mbox{\isa{\isakeyword{infixr}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)| + & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & + \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\ + + \end{tabular} + \end{center} + + The mixfix template \verb|"(_ |\isa{sy}\verb|/|\isasep\isanewline% +\verb| _)"| specifies two argument positions; the delimiter is preceded + by a space and followed by a space or line break; the entire phrase + is a pretty printing block. + + The alternative notation \verb|op|~\isa{sy} is introduced + in addition. Thus any infix operator may be written in prefix form + (as in ML), independently of the number of arguments in the term.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Binders% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +A \emph{binder} is a variable-binding construct such as a + quantifier. The idea to formalize \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}} as \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} for \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} already goes back + to \cite{church40}. Isabelle declarations of certain higher-order + operators may be annotated with \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} annotations as + follows: + + \begin{center} + \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|" (|\hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}}\verb| "|\isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}\verb|" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)| + \end{center} + + This introduces concrete binder syntax \isa{{\isaliteral{22}{\isachardoublequote}}sy\ x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}}, where + \isa{x} is a bound variable of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, the body \isa{b} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} and the whole term has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}. + The optional integer \isa{p} specifies the syntactic priority of + the body; the default is \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}, which is also the priority of + the whole construct. + + Internally, the binder syntax is expanded to something like this: + \begin{center} + \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}idts\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|" ("(3|\isa{sy}\verb|_./ _)" [0, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)| + \end{center} + + Here \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} is the nonterminal symbol for a list of + identifiers with optional type constraints (see also + \secref{sec:pure-grammar}). The mixfix template \verb|"(3|\isa{sy}\verb|_./ _)"| defines argument positions + for the bound identifiers and the body, separated by a dot with + optional line break; the entire phrase is a pretty printing block of + indentation level 3. Note that there is no extra space after \isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}, so it needs to be included user specification if the binder + syntax ends with a token that may be continued by an identifier + token at the start of \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}. + + Furthermore, a syntax translation to transforms \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ b{\isaliteral{22}{\isachardoublequote}}} into iterated application \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. + This works in both directions, for parsing and printing.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Explicit notation \label{sec:notation}% } \isamarkuptrue% @@ -805,7 +892,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{The Pure grammar% +\isamarkupsubsection{The Pure grammar \label{sec:pure-grammar}% } \isamarkuptrue% % diff -r d0199d9f9c5b -r 465851ba524e doc-src/Ref/defining.tex --- a/doc-src/Ref/defining.tex Sat Feb 04 16:08:19 2012 +0100 +++ b/doc-src/Ref/defining.tex Sat Feb 04 18:33:04 2012 +0100 @@ -2,19 +2,6 @@ \chapter{Defining Logics} \label{Defining-Logics} \section{Mixfix declarations} \label{sec:mixfix} -\index{mixfix declarations|(} - -When defining a theory, you declare new constants by giving their names, -their type, and an optional {\bf mixfix annotation}. Mixfix annotations -allow you to extend Isabelle's basic $\lambda$-calculus syntax with -readable notation. They can express any context-free priority grammar. -Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more -general than the priority declarations of \ML\ and Prolog. - -A mixfix annotation defines a production of the priority grammar. It -describes the concrete syntax, the translation to abstract syntax, and the -pretty printing. Special case annotations provide a simple means of -specifying infix operators and binders. \subsection{The general mixfix form} Here is a detailed account of mixfix declarations. Suppose the following @@ -33,18 +20,6 @@ $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th argument. - \item The constant $c$, if non-empty, is declared to have type $\sigma$ - ({\tt consts} section only). - - \item The string $template$ specifies the right-hand side of - the production. It has the form - \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \] - where each occurrence of {\tt_} denotes an argument position and - the~$w@i$ do not contain~{\tt _}. (If you want a literal~{\tt _} in - the concrete syntax, you must escape it as described below.) The $w@i$ - may consist of \rmindex{delimiters}, spaces or - \rmindex{pretty printing} annotations (see below). - \item The type $\sigma$ specifies the production's nonterminal symbols (or name tokens). If $template$ is of the form above then $\sigma$ must be a function type with at least~$n$ argument positions, say @@ -52,15 +27,6 @@ derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described below. Any of these may be function types. - \item The optional list~$ps$ may contain at most $n$ integers, say {\tt - [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal - priority\indexbold{priorities} required of any phrase that may appear - as the $i$-th argument. Missing priorities default to~0. - - \item The integer $p$ is the priority of this production. If - omitted, it defaults to the maximal priority. Priorities range - between 0 and \ttindexbold{max_pri} (= 1000). - \end{itemize} % The resulting production is \[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, @@ -72,15 +38,6 @@ is taken into account). Finally, the nonterminal of a type variable is {\tt any}. -\begin{warn} - Theories must sometimes declare types for purely syntactic purposes --- - merely playing the role of nonterminals. One example is \tydx{type}, the - built-in type of types. This is a `type of all types' in the syntactic - sense only. Do not declare such types under {\tt arities} as belonging to - class {\tt logic}\index{*logic class}, for that would make them useless as - separate nonterminal symbols. -\end{warn} - Associating nonterminals with types allows a constant's type to specify syntax as well. We can declare the function~$f$ to have type $[\tau@1, \ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the layout @@ -95,20 +52,10 @@ \medskip -As a special case of the general mixfix declaration, the form -\begin{center} - {\tt $c$ ::\ "$\sigma$" ("$template$")} -\end{center} -specifies no priorities. The resulting production puts no priority -constraints on any of its arguments and has maximal priority itself. -Omitting priorities in this manner is prone to syntactic ambiguities unless +Omitting priorities is prone to syntactic ambiguities unless the production's right-hand side is fully bracketed, as in \verb|"if _ then _ else _ fi"|. -Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"}, -is sensible only if~$c$ is an identifier. Otherwise you will be unable to -write terms involving~$c$. - \subsection{Example: arithmetic expressions} \index{examples!of mixfix declarations} @@ -136,93 +83,6 @@ {\out exp = "-" exp[3] => "-" (3)} \end{ttbox} -Note that because {\tt exp} is not of class {\tt logic}, it has been -retained as a separate nonterminal. This also entails that the syntax -does not provide for identifiers or paranthesized expressions. -Normally you would also want to add the declaration {\tt arities - exp::logic} after {\tt types} and use {\tt consts} instead of {\tt - syntax}. Try this as an exercise and study the changes in the -grammar. - - -\subsection{Infixes} -\indexbold{infixes} - -Infix operators associating to the left or right can be declared using -{\tt infixl} or {\tt infixr}. Basically, the form {\tt $c$ ::\ - $\sigma$ (infixl $p$)} abbreviates the mixfix declarations -\begin{ttbox} -"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) -"op \(c\)" :: \(\sigma\) ("op \(c\)") -\end{ttbox} -and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations -\begin{ttbox} -"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) -"op \(c\)" :: \(\sigma\) ("op \(c\)") -\end{ttbox} -The infix operator is declared as a constant with the prefix {\tt op}. -Thus, prefixing infixes with \sdx{op} makes them behave like ordinary -function symbols, as in \ML. Special characters occurring in~$c$ must be -escaped, as in delimiters, using a single quote. - -A slightly more general form of infix declarations allows constant -names to be independent from their concrete syntax, namely \texttt{$c$ - ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}. As -an example consider: -\begin{ttbox} -and :: [bool, bool] => bool (infixr "&" 35) -\end{ttbox} -The internal constant name will then be just \texttt{and}, without any -\texttt{op} prefixed. - - -\subsection{Binders} -\indexbold{binders} -\begingroup -\def\Q{{\cal Q}} -A {\bf binder} is a variable-binding construct such as a quantifier. The -constant declaration -\begin{ttbox} -\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\)) -\end{ttbox} -introduces a constant~$c$ of type~$\sigma$, which must have the form -$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where -$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ -and the whole term has type~$\tau@3$. The optional integer $pb$ -specifies the body's priority, by default~$p$. Special characters -in $\Q$ must be escaped using a single quote. - -The declaration is expanded internally to something like -\begin{ttbox} -\(c\)\hskip3pt :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\) -"\(\Q\)" :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) -\end{ttbox} -Here \ndx{idts} is the nonterminal symbol for a list of identifiers with -\index{type constraints} -optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The -declaration also installs a parse translation\index{translations!parse} -for~$\Q$ and a print translation\index{translations!print} for~$c$ to -translate between the internal and external forms. - -A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a -list of variables. The external form $\Q~x@1~x@2 \ldots x@n. P$ -corresponds to the internal form -\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \] - -\medskip -For example, let us declare the quantifier~$\forall$:\index{quantifiers} -\begin{ttbox} -All :: ('a => o) => o (binder "ALL " 10) -\end{ttbox} -This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL - $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall -back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL - $x$.$P$} have type~$o$, the type of formulae, while the bound variable -can be polymorphic. -\endgroup - -\index{mixfix declarations|)} - \section{Ambiguity of parsed expressions} \label{sec:ambiguity} \index{ambiguity!of parsed expressions}