# HG changeset patch # User wenzelm # Date 1226609299 -3600 # Node ID f5d79aeffd819e0894c23a93387d65484665615b # Parent 9ec4482c9201225d57bc85e9eee6980767d95a36 separate chapter "Inner syntax --- the term language"; diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/IsaMakefile --- a/doc-src/IsarRef/IsaMakefile Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/IsaMakefile Thu Nov 13 21:48:19 2008 +0100 @@ -22,9 +22,10 @@ HOL-IsarRef: $(LOG)/HOL-IsarRef.gz $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \ - Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy \ - Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/ML_Tactic.thy + Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy \ + Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy \ + Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy \ + Thy/ML_Tactic.thy @$(USEDIR) -s IsarRef HOL Thy diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/Makefile Thu Nov 13 21:48:19 2008 +0100 @@ -17,11 +17,12 @@ Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \ Thy/document/ML_Tactic.tex Thy/document/Proof.tex \ Thy/document/Quick_Reference.tex Thy/document/Spec.tex \ - Thy/document/ZF_Specific.tex Thy/document/Introduction.tex \ - Thy/document/Document_Preparation.tex Thy/document/Misc.tex \ - Thy/document/Outer_Syntax.tex ../isar.sty ../rail.sty \ - ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty \ - ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty ../manual.bib + Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \ + Thy/document/Introduction.tex Thy/document/Document_Preparation.tex \ + Thy/document/Misc.tex Thy/document/Outer_Syntax.tex ../isar.sty \ + ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \ + ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \ + ../manual.bib dvi: $(NAME).dvi diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/Inner_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 21:48:19 2008 +0100 @@ -0,0 +1,351 @@ +(* $Id$ *) + +theory Inner_Syntax +imports Main +begin + +chapter {* Inner syntax --- the term language *} + +section {* Printing logical entities *} + +subsection {* Diagnostic commands *} + +text {* + \begin{matharray}{rcl} + @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + \end{matharray} + + These diagnostic commands assist interactive development by printing + internal logical entities in a human-readable fashion. + + \begin{rail} + 'pr' modes? nat? (',' nat)? + ; + 'thm' modes? thmrefs + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'typ' modes? type + ; + 'prf' modes? thmrefs? + ; + 'full\_prf' modes? thmrefs? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{description} + + \item @{command "pr"}~@{text "goals, prems"} prints the current + proof state (if present), including the proof context, current facts + and goals. The optional limit arguments affect the number of goals + and premises to be displayed, which is initially 10 for both. + Omitting limit values leaves the current setting unchanged. + + \item @{command "thm"}~@{text "a\<^sub>1 \ a\<^sub>n"} retrieves + theorems from the current theory or proof context. Note that any + attributes included in the theorem specifications are applied to a + temporary context derived from the current theory or proof; the + result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, + \, a\<^sub>n"} do not have any permanent effect. + + \item @{command "term"}~@{text t} and @{command "prop"}~@{text \} + read, type-check and print terms or propositions according to the + current theory or proof context; the inferred type of @{text t} is + output as well. Note that these commands are also useful in + inspecting the current environment of term abbreviations. + + \item @{command "typ"}~@{text \} reads and prints types of the + meta-logic according to the current theory or proof context. + + \item @{command "prf"} displays the (compact) proof term of the + current proof state (if present), or of the given theorems. Note + that this requires proof terms to be switched on for the current + object logic (see the ``Proof terms'' section of the Isabelle + reference manual for information on how to do this). + + \item @{command "full_prf"} is like @{command "prf"}, but displays + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``@{text _}'' placeholders + there. + + \end{description} + + All of the diagnostic commands above admit a list of @{text modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, @{command + "pr"}~@{text "(latex xsymbols)"} would print the current proof state + with mathematical symbols and special characters represented in + {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document. +*} + + +section {* Mixfix annotations *} + +text {* Mixfix annotations specify concrete \emph{inner syntax} of + Isabelle types and terms. Some commands such as @{command "types"} + (see \secref{sec:types-pure}) admit infixes only, while @{command + "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see + \secref{sec:syn-trans}) support the full range of general mixfixes + and binders. + + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} + \begin{rail} + infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' + ; + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' + ; + structmixfix: mixfix | '(' 'structure' ')' + ; + + prios: '[' (nat + ',') ']' + ; + \end{rail} + + Here the \railtok{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. + + \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. + + Altogether this determines a production for a context-free priority + grammar, where for each argument @{text "i"} the syntactic category + is determined by @{text "\\<^sub>i"} (with priority @{text "p\<^sub>i"}), and + the result category is determined from @{text "\"} (with + priority @{text "p"}). Priority specifications are optional, with + default 0 for arguments and 1000 for the result. + + Since @{text "\"} may be again a function type, the constant + type scheme may have more argument positions than the mixfix + pattern. Printing a nested application @{text "c t\<^sub>1 \ t\<^sub>m"} for + @{text "m > n"} works by attaching concrete notation only to the + innermost part, essentially by printing @{text "(c t\<^sub>1 \ t\<^sub>n) \ t\<^sub>m"} + instead. If a term has fewer arguments than specified in the mixfix + template, the concrete syntax is ignored. + + \medskip A mixfix template may also contain additional directives + for pretty printing, notably spaces, blocks, and breaks. The + general template format is a sequence over any of the following + entities. + + \begin{itemize} + + \item @{text "\<^bold>d"} is a delimiter, namely a non-empty + sequence of characters other than the special characters @{text "'"} + (single quote), @{text "_"} (underscore), @{text "\"} (index + symbol), @{text "/"} (slash), @{text "("} and @{text ")"} + (parentheses). + + A single quote escapes the special meaning of these meta-characters, + producing a literal version of the following character, unless that + is a blank. A single quote followed by a blank separates + delimiters, without affecting printing, but input tokens may have + additional white space here. + + \item @{text "_"} is an argument position, which stands for a + certain syntactic category in the underlying grammar. + + \item @{text "\"} is an indexed argument position; this is + the place where implicit structure arguments can be attached. + + \item @{text "\<^bold>s"} is a non-empty sequence of spaces for + printing. This and the following specifications do not affect + parsing at all. + + \item @{text "(\<^bold>n"} opens a pretty printing block. The + optional number specifies how much indentation to add when a line + break occurs within the block. If the parenthesis is not followed + by digits, the indentation defaults to 0. A block specified via + @{text "(00"} is unbreakable. + + \item @{text ")"} closes a pretty printing block. + + \item @{text "//"} forces a line break. + + \item @{text "/\<^bold>s"} allows a line break. Here @{text + "\<^bold>s"} stands for the string of spaces (zero or more) right + after the slash. These spaces are printed if the break is + \emph{not} taken. + + \end{itemize} + + For example, the template @{text "(_ +/ _)"} specifies an infix + operator. There are two argument positions; the delimiter @{text + "+"} 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}. +*} + + +section {* Additional term notation *} + +text {* + \begin{matharray}{rcll} + @{command_def "notation"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "no_notation"} & : & @{text "local_theory \ local_theory"} \\ + \end{matharray} + + \begin{rail} + ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') + ; + \end{rail} + + \begin{description} + + \item @{command "notation"}~@{text "c (mx)"} associates mixfix + syntax with an existing constant or fixed variable. This is a + robust interface to the underlying @{command "syntax"} primitive + (\secref{sec:syn-trans}). Type declaration and internal syntactic + representation of the given entity is retrieved from the context. + + \item @{command "no_notation"} is similar to @{command "notation"}, + but removes the specified syntax annotation from the present + context. + + \end{description} +*} + +section {* Syntax and translations \label{sec:syn-trans} *} + +text {* + \begin{matharray}{rcl} + @{command_def "nonterminals"} & : & @{text "theory \ theory"} \\ + @{command_def "syntax"} & : & @{text "theory \ theory"} \\ + @{command_def "no_syntax"} & : & @{text "theory \ theory"} \\ + @{command_def "translations"} & : & @{text "theory \ theory"} \\ + @{command_def "no_translations"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + \begin{rail} + 'nonterminals' (name +) + ; + ('syntax' | 'no\_syntax') mode? (constdecl +) + ; + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) + ; + + mode: ('(' ( name | 'output' | name 'output' ) ')') + ; + transpat: ('(' nameref ')')? string + ; + \end{rail} + + \begin{description} + + \item @{command "nonterminals"}~@{text c} declares a type + constructor @{text c} (without arguments) to act as purely syntactic + type: a nonterminal symbol of the inner syntax. + + \item @{command "syntax"}~@{text "(mode) decls"} is similar to + @{command "consts"}~@{text decls}, except that the actual logical + signature extension is omitted. Thus the context free grammar of + Isabelle's inner syntax may be augmented in arbitrary ways, + independently of the logic. The @{text mode} argument refers to the + print mode that the grammar rules belong; unless the @{keyword_ref + "output"} indicator is given, all productions are added both to the + input and output grammar. + + \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar + declarations (and translations) resulting from @{text decls}, which + are interpreted in the same manner as for @{command "syntax"} above. + + \item @{command "translations"}~@{text rules} specifies syntactic + translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), + parse rules (@{text "\"}), or print rules (@{text "\"}). + Translation patterns may be prefixed by the syntactic category to be + used for parsing; the default is @{text logic}. + + \item @{command "no_translations"}~@{text rules} removes syntactic + translation rules, which are interpreted in the same manner as for + @{command "translations"} above. + + \end{description} +*} + + +section {* Syntax translation functions *} + +text {* + \begin{matharray}{rcl} + @{command_def "parse_ast_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "parse_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "print_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "typed_print_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "print_ast_translation"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + \begin{rail} + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text + ; + \end{rail} + + Syntax translation functions written in ML admit almost arbitrary + manipulations of Isabelle's inner syntax. Any of the above commands + have a single \railqtok{text} argument that refers to an ML + expression of appropriate type, which are as follows by default: + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation : (string * (ast list -> ast)) list +val parse_translation : (string * (term list -> term)) list +val print_translation : (string * (term list -> term)) list +val typed_print_translation : + (string * (bool -> typ -> term list -> term)) list +val print_ast_translation : (string * (ast list -> ast)) list +\end{ttbox} + + If the @{text "(advanced)"} option is given, the corresponding + translation functions may depend on the current theory or proof + context. This allows to implement advanced syntax mechanisms, as + translations functions may refer to specific theory declarations or + auxiliary proof data. + + See also \cite[\S8]{isabelle-ref} for more information on the + general concept of syntax transformations in Isabelle. + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation: + (string * (Proof.context -> ast list -> ast)) list +val parse_translation: + (string * (Proof.context -> term list -> term)) list +val print_translation: + (string * (Proof.context -> term list -> term)) list +val typed_print_translation: + (string * (Proof.context -> bool -> typ -> term list -> term)) list +val print_ast_translation: + (string * (Proof.context -> ast list -> ast)) list +\end{ttbox} +*} + +end diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/Misc.thy --- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:48:19 2008 +0100 @@ -6,95 +6,6 @@ chapter {* Other commands \label{ch:pure-syntax} *} -section {* Diagnostics *} - -text {* - \begin{matharray}{rcl} - @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \"} \\ - @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - \end{matharray} - - These diagnostic commands assist interactive development. Note that - @{command undo} does not apply here, the theory or proof - configuration is not changed. - - \begin{rail} - 'pr' modes? nat? (',' nat)? - ; - 'thm' modes? thmrefs - ; - 'term' modes? term - ; - 'prop' modes? prop - ; - 'typ' modes? type - ; - 'prf' modes? thmrefs? - ; - 'full\_prf' modes? thmrefs? - ; - - modes: '(' (name + ) ')' - ; - \end{rail} - - \begin{description} - - \item @{command "pr"}~@{text "goals, prems"} prints the current - proof state (if present), including the proof context, current facts - and goals. The optional limit arguments affect the number of goals - and premises to be displayed, which is initially 10 for both. - Omitting limit values leaves the current setting unchanged. - - \item @{command "thm"}~@{text "a\<^sub>1 \ a\<^sub>n"} retrieves - theorems from the current theory or proof context. Note that any - attributes included in the theorem specifications are applied to a - temporary context derived from the current theory or proof; the - result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, - \, a\<^sub>n"} do not have any permanent effect. - - \item @{command "term"}~@{text t} and @{command "prop"}~@{text \} - read, type-check and print terms or propositions according to the - current theory or proof context; the inferred type of @{text t} is - output as well. Note that these commands are also useful in - inspecting the current environment of term abbreviations. - - \item @{command "typ"}~@{text \} reads and prints types of the - meta-logic according to the current theory or proof context. - - \item @{command "prf"} displays the (compact) proof term of the - current proof state (if present), or of the given theorems. Note - that this requires proof terms to be switched on for the current - object logic (see the ``Proof terms'' section of the Isabelle - reference manual for information on how to do this). - - \item @{command "full_prf"} is like @{command "prf"}, but displays - the full proof term, i.e.\ also displays information omitted in the - compact proof term, which is denoted by ``@{text _}'' placeholders - there. - - \end{description} - - All of the diagnostic commands above admit a list of @{text modes} - to be specified, which is appended to the current print mode (see - also \cite{isabelle-ref}). Thus the output behavior may be modified - according particular print mode features. For example, @{command - "pr"}~@{text "(latex xsymbols symbols)"} would print the current - proof state with mathematical symbols and special characters - represented in {\LaTeX} source, according to the Isabelle style - \cite{isabelle-sys}. - - Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more - systematic way to include formal items into the printed text - document. -*} - - section {* Inspecting the context *} text {* diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 21:48:19 2008 +0100 @@ -307,117 +307,6 @@ *} -subsection {* Mixfix annotations *} - -text {* - Mixfix annotations specify concrete \emph{inner} syntax of Isabelle - types and terms. Some commands such as @{command "types"} (see - \secref{sec:types-pure}) admit infixes only, while @{command - "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see - \secref{sec:syn-trans}) support the full range of general mixfixes - and binders. - - \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} - \begin{rail} - infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' - ; - mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' - ; - structmixfix: mixfix | '(' 'structure' ')' - ; - - prios: '[' (nat + ',') ']' - ; - \end{rail} - - Here the \railtok{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. - - \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. - - Altogether this determines a production for a context-free priority - grammar, where for each argument @{text "i"} the syntactic category - is determined by @{text "\\<^sub>i"} (with priority @{text "p\<^sub>i"}), and - the result category is determined from @{text "\"} (with - priority @{text "p"}). Priority specifications are optional, with - default 0 for arguments and 1000 for the result. - - Since @{text "\"} may be again a function type, the constant - type scheme may have more argument positions than the mixfix - pattern. Printing a nested application @{text "c t\<^sub>1 \ t\<^sub>m"} for - @{text "m > n"} works by attaching concrete notation only to the - innermost part, essentially by printing @{text "(c t\<^sub>1 \ t\<^sub>n) \ t\<^sub>m"} - instead. If a term has fewer arguments than specified in the mixfix - template, the concrete syntax is ignored. - - \medskip A mixfix template may also contain additional directives - for pretty printing, notably spaces, blocks, and breaks. The - general template format is a sequence over any of the following - entities. - - \begin{itemize} - - \item @{text "\<^bold>d"} is a delimiter, namely a non-empty - sequence of characters other than the special characters @{text "'"} - (single quote), @{text "_"} (underscore), @{text "\"} (index - symbol), @{text "/"} (slash), @{text "("} and @{text ")"} - (parentheses). - - A single quote escapes the special meaning of these meta-characters, - producing a literal version of the following character, unless that - is a blank. A single quote followed by a blank separates - delimiters, without affecting printing, but input tokens may have - additional white space here. - - \item @{text "_"} is an argument position, which stands for a - certain syntactic category in the underlying grammar. - - \item @{text "\"} is an indexed argument position; this is - the place where implicit structure arguments can be attached. - - \item @{text "\<^bold>s"} is a non-empty sequence of spaces for - printing. This and the following specifications do not affect - parsing at all. - - \item @{text "(\<^bold>n"} opens a pretty printing block. The - optional number specifies how much indentation to add when a line - break occurs within the block. If the parenthesis is not followed - by digits, the indentation defaults to 0. A block specified via - @{text "(00"} is unbreakable. - - \item @{text ")"} closes a pretty printing block. - - \item @{text "//"} forces a line break. - - \item @{text "/\<^bold>s"} allows a line break. Here @{text - "\<^bold>s"} stands for the string of spaces (zero or more) right - after the slash. These spaces are printed if the break is - \emph{not} taken. - - \end{itemize} - - For example, the template @{text "(_ +/ _)"} specifies an infix - operator. There are two argument positions; the delimiter @{text - "+"} 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}. -*} - - subsection {* Attributes and theorems \label{sec:syn-att} *} text {* Attributes have their own ``semi-inner'' syntax, in the sense diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/ROOT.ML --- a/doc-src/IsarRef/Thy/ROOT.ML Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/Thy/ROOT.ML Thu Nov 13 21:48:19 2008 +0100 @@ -9,6 +9,7 @@ use_thy "Document_Preparation"; use_thy "Spec"; use_thy "Proof"; +use_thy "Inner_Syntax"; use_thy "Misc"; use_thy "Generic"; use_thy "HOL_Specific"; diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:48:19 2008 +0100 @@ -148,8 +148,6 @@ @{attribute_def "defn"} & : & @{text attribute} \\ @{command_def "abbreviation"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ - @{command_def "notation"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "no_notation"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} These specification mechanisms provide a slightly more abstract view @@ -165,8 +163,6 @@ ; 'abbreviation' target? mode? (decl 'where')? prop ; - ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') - ; fixes: ((name ('::' type)? mixfix? | vars) + 'and') ; @@ -223,20 +219,7 @@ \item @{command "print_abbrevs"} prints all constant abbreviations of the current context. - \item @{command "notation"}~@{text "c (mx)"} associates mixfix - syntax with an existing constant or fixed variable. This is a - robust interface to the underlying @{command "syntax"} primitive - (\secref{sec:syn-trans}). Type declaration and internal syntactic - representation of the given entity is retrieved from the context. - - \item @{command "no_notation"} is similar to @{command "notation"}, - but removes the specified syntax annotation from the present - context. - \end{description} - - All of these specifications support local theory targets (cf.\ - \secref{sec:target}). *} @@ -924,7 +907,6 @@ \begin{matharray}{rcll} @{command_def "types"} & : & @{text "theory \ theory"} \\ @{command_def "typedecl"} & : & @{text "theory \ theory"} \\ - @{command_def "nonterminals"} & : & @{text "theory \ theory"} \\ @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} @@ -933,8 +915,6 @@ ; 'typedecl' typespec infix? ; - 'nonterminals' (name +) - ; 'arities' (nameref '::' arity +) ; \end{rail} @@ -952,11 +932,6 @@ type constructor @{text t}, intended as an actual logical type (of the object-logic, if available). - \item @{command "nonterminals"}~@{text c} declares type constructors - @{text c} (without arguments) to act as purely syntactic types, - i.e.\ nonterminal symbols of Isabelle's inner syntax of terms or - types. - \item @{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s"} augments Isabelle's order-sorted signature of types by new type constructor arities. This is done axiomatically! The @{command_ref "instance"} @@ -1206,112 +1181,4 @@ \end{description} *} - -section {* Syntax and translations \label{sec:syn-trans} *} - -text {* - \begin{matharray}{rcl} - @{command_def "syntax"} & : & @{text "theory \ theory"} \\ - @{command_def "no_syntax"} & : & @{text "theory \ theory"} \\ - @{command_def "translations"} & : & @{text "theory \ theory"} \\ - @{command_def "no_translations"} & : & @{text "theory \ theory"} \\ - \end{matharray} - - \begin{rail} - ('syntax' | 'no\_syntax') mode? (constdecl +) - ; - ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) - ; - - mode: ('(' ( name | 'output' | name 'output' ) ')') - ; - transpat: ('(' nameref ')')? string - ; - \end{rail} - - \begin{description} - - \item @{command "syntax"}~@{text "(mode) decls"} is similar to - @{command "consts"}~@{text decls}, except that the actual logical - signature extension is omitted. Thus the context free grammar of - Isabelle's inner syntax may be augmented in arbitrary ways, - independently of the logic. The @{text mode} argument refers to the - print mode that the grammar rules belong; unless the @{keyword_ref - "output"} indicator is given, all productions are added both to the - input and output grammar. - - \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar - declarations (and translations) resulting from @{text decls}, which - are interpreted in the same manner as for @{command "syntax"} above. - - \item @{command "translations"}~@{text rules} specifies syntactic - translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), - parse rules (@{text "\"}), or print rules (@{text "\"}). - Translation patterns may be prefixed by the syntactic category to be - used for parsing; the default is @{text logic}. - - \item @{command "no_translations"}~@{text rules} removes syntactic - translation rules, which are interpreted in the same manner as for - @{command "translations"} above. - - \end{description} -*} - - -section {* Syntax translation functions *} - -text {* - \begin{matharray}{rcl} - @{command_def "parse_ast_translation"} & : & @{text "theory \ theory"} \\ - @{command_def "parse_translation"} & : & @{text "theory \ theory"} \\ - @{command_def "print_translation"} & : & @{text "theory \ theory"} \\ - @{command_def "typed_print_translation"} & : & @{text "theory \ theory"} \\ - @{command_def "print_ast_translation"} & : & @{text "theory \ theory"} \\ - \end{matharray} - - \begin{rail} - ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | - 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text - ; - \end{rail} - - Syntax translation functions written in ML admit almost arbitrary - manipulations of Isabelle's inner syntax. Any of the above commands - have a single \railqtok{text} argument that refers to an ML - expression of appropriate type, which are as follows by default: - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation : (string * (ast list -> ast)) list -val parse_translation : (string * (term list -> term)) list -val print_translation : (string * (term list -> term)) list -val typed_print_translation : - (string * (bool -> typ -> term list -> term)) list -val print_ast_translation : (string * (ast list -> ast)) list -\end{ttbox} - - If the @{text "(advanced)"} option is given, the corresponding - translation functions may depend on the current theory or proof - context. This allows to implement advanced syntax mechanisms, as - translations functions may refer to specific theory declarations or - auxiliary proof data. - - See also \cite[\S8]{isabelle-ref} for more information on the - general concept of syntax transformations in Isabelle. - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation: - (string * (Proof.context -> ast list -> ast)) list -val parse_translation: - (string * (Proof.context -> term list -> term)) list -val print_translation: - (string * (Proof.context -> term list -> term)) list -val typed_print_translation: - (string * (Proof.context -> bool -> typ -> term list -> term)) list -val print_ast_translation: - (string * (Proof.context -> ast list -> ast)) list -\end{ttbox} -*} - end diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Nov 13 21:48:19 2008 +0100 @@ -0,0 +1,910 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Inner{\isacharunderscore}Syntax}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Inner{\isacharunderscore}Syntax\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}% +} +\isamarkuptrue% +% +\isamarkupsection{Printing logical entities% +} +\isamarkuptrue% +% +\isamarkupsubsection{Diagnostic commands% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ + \end{matharray} + + These diagnostic commands assist interactive development by printing + internal logical entities in a human-readable fashion. + + \begin{rail} + 'typ' modes? type + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'thm' modes? thmrefs + ; + ( 'prf' | 'full\_prf' ) modes? thmrefs? + ; + 'pr' modes? nat? (',' nat)? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{description} + + \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}} reads and prints types of the + meta-logic according to the current theory or proof context. + + \item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}} + read, type-check and print terms or propositions according to the + current theory or proof context; the inferred type of \isa{t} is + output as well. Note that these commands are also useful in + inspecting the current environment of term abbreviations. + + \item \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} retrieves + theorems from the current theory or proof context. Note that any + attributes included in the theorem specifications are applied to a + temporary context derived from the current theory or proof; the + result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect. + + \item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the + current proof state (if present), or of the given theorems. Note + that this requires proof terms to be switched on for the current + object logic (see the ``Proof terms'' section of the Isabelle + reference manual for information on how to do this). + + \item \hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}} is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders + there. + + \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current + proof state (if present), including the proof context, current facts + and goals. The optional limit arguments affect the number of goals + and premises to be displayed, which is initially 10 for both. + Omitting limit values leaves the current setting unchanged. + + \end{description} + + All of the diagnostic commands above admit a list of \isa{modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols{\isacharparenright}{\isachardoublequote}} would print the current proof state + with mathematical symbols and special characters represented in + {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Details of printed content% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\ + \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\ + \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\ + \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\ + \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\ + \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\ + \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\ + \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\ + \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\ + \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\ + \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\ + \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\ + \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\ + \end{mldecls} + + These global ML variables control the detail of information that is + displayed for types, terms, theorems, goals etc. + + In interactive sessions, the user interface usually manages these + global parameters of the Isabelle process, even with some concept of + persistence. Nonetheless it is occasionally useful to manipulate ML + variables directly, e.g.\ using \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}. + + Batch-mode logic sessions may be configured by putting appropriate + ML text directly into the \verb|ROOT.ML| file. + + \begin{description} + + \item \verb|show_types| and \verb|show_sorts| control printing of type + constraints for term variables, and sort constraints for type + variables. By default, neither of these are shown in output. If + \verb|show_sorts| is set to \verb|true|, types are always shown as + well. + + Note that displaying types and sorts may explain why a polymorphic + inference rule fails to resolve with some goal, or why a rewrite + rule does not apply as expected. + + \item \verb|show_consts| controls printing of types of constants when + displaying a goal state. + + Note that the output can be enormous, because polymorphic constants + often occur at several different type instances. + + \item \verb|long_names|, \verb|short_names|, and \verb|unique_names| + control the way of printing fully qualified internal names in + external form. See also \secref{sec:antiq} for the document + antiquotation options of the same names. + + \item \verb|show_brackets| controls bracketing in pretty printed + output. If set to \verb|true|, all sub-expressions of the pretty + printing tree will be parenthesized, even if this produces malformed + term syntax! This crude way of showing the internal structure of + pretty printed entities may occasionally help to diagnose problems + with operator priorities, for example. + + \item \verb|eta_contract| controls \isa{{\isachardoublequote}{\isasymeta}{\isachardoublequote}}-contracted printing of + terms. + + The \isa{{\isasymeta}}-contraction law asserts \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x{\isacharparenright}\ {\isasymequiv}\ f{\isachardoublequote}}, + provided \isa{x} is not free in \isa{f}. It asserts + \emph{extensionality} of functions: \isa{{\isachardoublequote}f\ {\isasymequiv}\ g{\isachardoublequote}} if \isa{{\isachardoublequote}f\ x\ {\isasymequiv}\ g\ x{\isachardoublequote}} for all \isa{x}. Higher-order unification frequently puts + terms into a fully \isa{{\isasymeta}}-expanded form. For example, if \isa{F} has type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}{\isacharparenright}\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} then its expanded form is \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}}. + + Setting \verb|eta_contract| makes Isabelle perform \isa{{\isasymeta}}-contractions before printing, so that \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}} + appears simply as \isa{F}. + + Note that the distinction between a term and its \isa{{\isasymeta}}-expanded + form occasionally matters. While higher-order resolution and + rewriting operate modulo \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion, some other tools + might look at terms more discretely. + + \item \verb|goals_limit| controls the maximum number of subgoals to + be shown in goal output. + + \item \verb|Proof.show_main_goal| controls whether the main result to + be proven should be displayed. This information might be relevant + for schematic goals, to inspect the current claim that has been + synthesized so far. + + \item \verb|show_hyps| controls printing of implicit hypotheses of + local facts. Normally, only those hypotheses are displayed that are + \emph{not} covered by the assumptions of the current context: this + situation indicates a fault in some tool being used. + + By setting \verb|show_hyps| to \verb|true|, output of \emph{all} + hypotheses can be enforced, which is occasionally useful for + diagnostic purposes. + + \item \verb|show_tags| controls printing of extra annotations within + theorems, such as internal position information, or the case names + being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}. + + Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} + attributes provide low-level access to the collection of tags + associated with a theorem. + + \item \verb|show_question_marks| controls printing of question marks + for schematic variables, such as \isa{{\isacharquery}x}. Only the leading + question mark is affected, the remaining text is unchanged + (including proper markup for schematic variables that might be + relevant for user interfaces). + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Printing limits% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\ + \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\ + \indexml{print\_depth}\verb|print_depth: int -> unit| \\ + \end{mldecls} + + These ML functions set limits for pretty printed text. + + \begin{description} + + \item \verb|Pretty.setdepth|~\isa{d} tells the pretty printer to + limit the printing depth to \isa{d}. This affects the display of + types, terms, theorems etc. The default value is 0, which permits + printing to an arbitrary depth. Other useful values for \isa{d} + are 10 and 20. + + \item \verb|Pretty.setmargin|~\isa{m} tells the pretty printer to + assume a right margin (page width) of \isa{m}. The initial margin + is 76, but user interfaces might adapt the margin automatically when + resizing windows. + + \item \verb|print_depth|~\isa{n} limits the printing depth of the + ML toplevel pretty printer; the precise effect depends on the ML + compiler and run-time system. Typically \isa{n} should be less + than 10. Bigger values such as 100--1000 are useful for debugging. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Mixfix annotations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Mixfix annotations specify concrete \emph{inner syntax} of + Isabelle types and terms. Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\ + support the full range of general mixfixes and binders. Fixed + parameters in toplevel theorem statements, locale specifications + also admit mixfix annotations. + + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} + \begin{rail} + infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' + ; + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' + ; + structmixfix: mixfix | '(' 'structure' ')' + ; + + prios: '[' (nat + ',') ']' + ; + \end{rail} + + Here the \railtok{string} specifications refer to the actual mixfix + template, which may include literal text, spacing, blocks, and + arguments (denoted by ``\isa{{\isacharunderscore}}''); the special symbol + ``\verb|\|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\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{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymtau}\isactrlsub n\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} is + annotated by \isa{{\isachardoublequote}{\isacharparenleft}mixfix\ {\isacharbrackleft}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isacharbrackright}\ p{\isacharparenright}{\isachardoublequote}}, where \isa{{\isachardoublequote}mixfix{\isachardoublequote}} is a string \isa{{\isachardoublequote}d\isactrlsub {\isadigit{0}}\ {\isacharunderscore}\ d\isactrlsub {\isadigit{1}}\ {\isacharunderscore}\ {\isasymdots}\ {\isacharunderscore}\ d\isactrlsub n{\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{{\isachardoublequote}i{\isachardoublequote}} the syntactic category + is determined by \isa{{\isachardoublequote}{\isasymtau}\isactrlsub i{\isachardoublequote}} (with priority \isa{{\isachardoublequote}p\isactrlsub i{\isachardoublequote}}), and + the result category is determined from \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} (with + priority \isa{{\isachardoublequote}p{\isachardoublequote}}). Priority specifications are optional, with + default 0 for arguments and 1000 for the result. + + Since \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} may be again a function type, the constant + type scheme may have more argument positions than the mixfix + pattern. Printing a nested application \isa{{\isachardoublequote}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} for + \isa{{\isachardoublequote}m\ {\isachargreater}\ n{\isachardoublequote}} works by attaching concrete notation only to the + innermost part, essentially by printing \isa{{\isachardoublequote}{\isacharparenleft}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isacharparenright}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} + instead. If a term has fewer arguments than specified in the mixfix + template, the concrete syntax is ignored. + + \medskip A mixfix template may also contain additional directives + for pretty printing, notably spaces, blocks, and breaks. The + general template format is a sequence over any of the following + entities. + + \begin{description} + + \item \isa{{\isachardoublequote}d{\isachardoublequote}} is a delimiter, namely a non-empty sequence of + characters other than the following special characters: + + \smallskip + \begin{tabular}{ll} + \verb|'| & single quote \\ + \verb|_| & underscore \\ + \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} & index symbol \\ + \verb|(| & open parenthesis \\ + \verb|)| & close parenthesis \\ + \verb|/| & slash \\ + \end{tabular} + \medskip + + \item \verb|'| escapes the special meaning of these + meta-characters, producing a literal version of the following + character, unless that is a blank. + + A single quote followed by a blank separates delimiters, without + affecting printing, but input tokens may have additional white space + here. + + \item \verb|_| is an argument position, which stands for a + certain syntactic category in the underlying grammar. + + \item \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} is an indexed argument position; this is the place + where implicit structure arguments can be attached. + + \item \isa{{\isachardoublequote}s{\isachardoublequote}} is a non-empty sequence of spaces for printing. + This and the following specifications do not affect parsing at all. + + \item \verb|(|\isa{n} opens a pretty printing block. The + optional number specifies how much indentation to add when a line + break occurs within the block. If the parenthesis is not followed + by digits, the indentation defaults to 0. A block specified via + \verb|(00| is unbreakable. + + \item \verb|)| closes a pretty printing block. + + \item \verb|//| forces a line break. + + \item \verb|/|\isa{s} allows a line break. Here \isa{s} + stands for the string of spaces (zero or more) right after the + slash. These spaces are printed if the break is \emph{not} taken. + + \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}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Explicit term notation% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcll} + \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ + \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ + \end{matharray} + + \begin{rail} + ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') + ; + \end{rail} + + \begin{description} + + \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix + syntax with an existing constant or fixed variable. This is a + robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive + (\secref{sec:syn-trans}). Type declaration and internal syntactic + representation of the given entity is retrieved from the context. + + \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, + but removes the specified syntax annotation from the present + context. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{The Pure syntax \label{sec:pure-syntax}% +} +\isamarkuptrue% +% +\isamarkupsubsection{Priority grammars \label{sec:priority-grammar}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +A context-free grammar consists of a set of \emph{terminal + symbols}, a set of \emph{nonterminal symbols} and a set of + \emph{productions}. Productions have the form \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}}, + where \isa{A} is a nonterminal and \isa{{\isasymgamma}} is a string of + terminals and nonterminals. One designated nonterminal is called + the \emph{root symbol}. The language defined by the grammar + consists of all strings of terminals that can be derived from the + root symbol by applying productions as rewrite rules. + + The standard Isabelle parser for inner syntax uses a \emph{priority + grammar}. Each nonterminal is decorated by an integer priority: + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}}. In a derivation, \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} may be rewritten + using a production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} only if \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}. Any + priority grammar can be translated into a normal context-free + grammar by introducing new nonterminals and productions. + + \medskip Formally, a set of context free productions \isa{G} + induces a derivation relation \isa{{\isachardoublequote}{\isasymlongrightarrow}\isactrlsub G{\isachardoublequote}} as follows. Let \isa{{\isasymalpha}} and \isa{{\isasymbeta}} denote strings of terminal or nonterminal symbols. + Then \isa{{\isachardoublequote}{\isasymalpha}\ A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isasymbeta}\ {\isasymlongrightarrow}\isactrlsub G\ {\isasymalpha}\ {\isasymgamma}\ {\isasymbeta}{\isachardoublequote}} holds if and only if \isa{G} + contains some production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} for \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}. + + \medskip The following grammar for arithmetic expressions + demonstrates how binding power and associativity of operators can be + enforced by priorities. + + \begin{center} + \begin{tabular}{rclr} + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|)| \\ + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|0| \\ + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ + \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ + \end{tabular} + \end{center} + The choice of priorities determines that \verb|-| binds + tighter than \verb|*|, which binds tighter than \verb|+|. Furthermore \verb|+| associates to the left and + \verb|*| to the right. + + \medskip For clarity, grammars obey these conventions: + \begin{itemize} + + \item All priorities must lie between 0 and 1000. + + \item Priority 0 on the right-hand side and priority 1000 on the + left-hand side may be omitted. + + \item The production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymalpha}{\isachardoublequote}} is written as \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymalpha}\ {\isacharparenleft}p{\isacharparenright}{\isachardoublequote}}, i.e.\ the priority of the left-hand side actually appears in + a column on the far right. + + \item Alternatives are separated by \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}. + + \item Repetition is indicated by dots \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}{\isacharparenright}{\isachardoublequote}} in an informal + but obvious way. + + \end{itemize} + + Using these conventions, the example grammar specification above + takes the form: + \begin{center} + \begin{tabular}{rclc} + \isa{A} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{A} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|0| & \qquad\qquad \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{A} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ + \end{tabular} + \end{center}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The Pure grammar% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The priority grammar of the \isa{{\isachardoublequote}Pure{\isachardoublequote}} theory is defined as follows: + + %FIXME syntax for "index" (?) + %FIXME "op" versions of ==> etc. (?) + + \begin{center} + \begin{supertabular}{rclr} + + \indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isachardoublequote}prop\ \ {\isacharbar}\ \ logic{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=?=| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[|\verb,|,\verb|| \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \verb||\verb,|,\verb|]| \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlbrakk}{\isachardoublequote}} \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \isa{{\isachardoublequote}{\isasymrbrakk}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|!!| \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|PROP| \isa{aprop} \\\\ + + \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isasymlambda}} \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\ + + \indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{id} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|_| \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{idts}\hypertarget{syntax.inner.idts}{\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}} & = & \isa{{\isachardoublequote}idt\ \ {\isacharbar}\ \ idt\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ idts{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\ + + \indexdef{inner}{syntax}{pttrns}\hypertarget{syntax.inner.pttrns}{\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}} & = & \isa{{\isachardoublequote}pttrn\ \ {\isacharbar}\ \ pttrn\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ pttrns{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ + & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ + + \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\ + \end{supertabular} + \end{center} + + \medskip Here literal terminals are printed \verb|verbatim|; + see also \secref{sec:inner-lex} for further token categories of the + inner syntax. The meaning of the nonterminals defined by the above + grammar is as follows: + + \begin{description} + + \item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term. + + \item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions, + which are terms of type \isa{prop}. The syntax of such formulae of + the meta-logic is carefully distinguished from usual conventions for + object-logics. In particular, plain \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-term notation is + \emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. + + \item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which + are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an + explicit \verb|PROP| token. + + Terms of type \isa{prop} with non-constant head, e.g.\ a plain + variable, are printed in this form. Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise + the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and + cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. + + \item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a + logical type, excluding type \isa{prop}. This is the main + syntactic category of object-logic entities, covering plain \isa{{\isasymlambda}}-term notation (variables, abstraction, application), plus + anything defined by the user. + + When specifying notation for logical entities, all logical types + (excluding \isa{prop}) are \emph{collapsed} to this single category + of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}. + + \item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly + constrained by types. + + \item \indexref{inner}{syntax}{idts}\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} denotes a sequence of \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}. This is the most basic category for variables in + iterated binders, such as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}} or \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}. + + \item \indexref{inner}{syntax}{pttrn}\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}} and \indexref{inner}{syntax}{pttrns}\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}} + denote patterns for abstraction, cases bindings etc. In Pure, these + categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and + \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively. Object-logics may add + additional productions for binding forms. + + \item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic. + + \item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts. + + \end{description} + + Here are some further explanations of certain syntax features. + + \begin{itemize} + + \item In \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, note that \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y{\isachardoublequote}} is + parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y{\isacharparenright}{\isachardoublequote}}, treating \isa{y} like a type + constructor applied to \isa{nat}. To avoid this interpretation, + write \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y{\isachardoublequote}} with explicit parentheses. + + \item Similarly, \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}. The correct form is \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}, or \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} if \isa{y} is last in the + sequence of identifiers. + + \item Type constraints for terms bind very weakly. For example, + \isa{{\isachardoublequote}x\ {\isacharless}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is normally parsed as \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}}, unless \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}} has a very low priority, in which case the + input is likely to be ambiguous. The correct form is \isa{{\isachardoublequote}x\ {\isacharless}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}. + + \item Constraints may be either written with two literal colons + ``\verb|::|'' or the double-colon symbol \verb|\|, + which actually looks exactly the same in some {\LaTeX} styles. + + \item Dummy variables (written as underscore) may occur in different + roles. + + \begin{description} + + \item A type ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}{\isacharunderscore}\ {\isacharcolon}{\isacharcolon}\ sort{\isachardoublequote}}'' acts like an + anonymous inference parameter, which is filled-in according to the + most general type produced by the type-checking phase. + + \item A bound ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to a vacuous abstraction, where + the body does not refer to the binding introduced here. As in the + term \isa{{\isachardoublequote}{\isasymlambda}x\ {\isacharunderscore}{\isachardot}\ x{\isachardoublequote}}, which is \isa{{\isachardoublequote}{\isasymalpha}{\isachardoublequote}}-equivalent to \isa{{\isachardoublequote}{\isasymlambda}x\ y{\isachardot}\ x{\isachardoublequote}}. + + \item A free ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to an implicit outer binding. + Higher definitional packages usually allow forms like \isa{{\isachardoublequote}f\ x\ {\isacharunderscore}\ {\isacharequal}\ x{\isachardoublequote}}. + + \item A schematic ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' (within a term pattern, see + \secref{sec:term-decls}) refers to an anonymous variable that is + implicitly abstracted over its context of locally bound variables. + For example, this allows pattern matching of \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ x{\isacharbraceright}{\isachardoublequote}} against \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}}, or even \isa{{\isachardoublequote}{\isacharbraceleft}{\isacharunderscore}{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}} by + using both bound and schematic dummies. + + \end{description} + + \item The three literal dots ``\verb|...|'' may be also + written as ellipsis symbol \verb|\|. In both cases this + refers to a special schematic variable, which is bound in the + context. This special term abbreviation works nicely with + calculational reasoning (\secref{sec:calculation}). + + \end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Lexical matters \label{sec:inner-lex}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The inner lexical syntax vaguely resembles the outer one + (\secref{sec:outer-lex}), but some details are different. There are + two main categories of inner syntax tokens: + + \begin{enumerate} + + \item \emph{delimiters} --- the literal tokens occurring in + productions of the given priority grammar (cf.\ + \secref{sec:priority-grammar}); + + \item \emph{named tokens} --- various categories of identifiers etc. + + \end{enumerate} + + Delimiters override named tokens and may thus render certain + identifiers inaccessible. Sometimes the logical context admits + alternative ways to refer to the same entity, potentially via + qualified names. + + \medskip The categories for named tokens are defined once and for + all as follows, reusing some categories of the outer token syntax + (\secref{sec:outer-lex}). + + \begin{center} + \begin{supertabular}{rcl} + \indexdef{inner}{syntax}{id}\hypertarget{syntax.inner.id}{\hyperlink{syntax.inner.id}{\mbox{\isa{id}}}} & = & \indexref{}{syntax}{ident}\hyperlink{syntax.ident}{\mbox{\isa{ident}}} \\ + \indexdef{inner}{syntax}{longid}\hypertarget{syntax.inner.longid}{\hyperlink{syntax.inner.longid}{\mbox{\isa{longid}}}} & = & \indexref{}{syntax}{longident}\hyperlink{syntax.longident}{\mbox{\isa{longident}}} \\ + \indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\ + \indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\ + \indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\ + \indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ + \indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ + + \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\ + \end{supertabular} + \end{center} + + The token categories \indexref{inner}{syntax}{num}\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \indexref{inner}{syntax}{xnum}\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \indexref{inner}{syntax}{xstr}\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are not used in Pure. + Object-logics may implement numerals and string constants by adding + appropriate syntax declarations, together with some translation + functions (e.g.\ see Isabelle/HOL).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Syntax and translations \label{sec:syn-trans}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \end{matharray} + + \begin{rail} + 'nonterminals' (name +) + ; + ('syntax' | 'no\_syntax') mode? (constdecl +) + ; + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) + ; + + mode: ('(' ( name | 'output' | name 'output' ) ')') + ; + transpat: ('(' nameref ')')? string + ; + \end{rail} + + \begin{description} + + \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type + constructor \isa{c} (without arguments) to act as purely syntactic + type: a nonterminal symbol of the inner syntax. + + \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} is similar to + \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical + signature extension is omitted. Thus the context free grammar of + Isabelle's inner syntax may be augmented in arbitrary ways, + independently of the logic. The \isa{mode} argument refers to the + print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the + input and output grammar. + + \item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} removes grammar + declarations (and translations) resulting from \isa{decls}, which + are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. + + \item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic + translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}), + parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}). + Translation patterns may be prefixed by the syntactic category to be + used for parsing; the default is \isa{logic}. + + \item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules} removes syntactic + translation rules, which are interpreted in the same manner as for + \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Syntax translation functions \label{sec:tr-funs}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \end{matharray} + + \begin{rail} + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text + ; + \end{rail} + + Syntax translation functions written in ML admit almost arbitrary + manipulations of Isabelle's inner syntax. Any of the above commands + have a single \railqtok{text} argument that refers to an ML + expression of appropriate type, which are as follows by default: + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation : (string * (ast list -> ast)) list +val parse_translation : (string * (term list -> term)) list +val print_translation : (string * (term list -> term)) list +val typed_print_translation : + (string * (bool -> typ -> term list -> term)) list +val print_ast_translation : (string * (ast list -> ast)) list +\end{ttbox} + + If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding + translation functions may depend on the current theory or proof + context. This allows to implement advanced syntax mechanisms, as + translations functions may refer to specific theory declarations or + auxiliary proof data. + + See also \cite[\S8]{isabelle-ref} for more information on the + general concept of syntax transformations in Isabelle. + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation: + (string * (Proof.context -> ast list -> ast)) list +val parse_translation: + (string * (Proof.context -> term list -> term)) list +val print_translation: + (string * (Proof.context -> term list -> term)) list +val typed_print_translation: + (string * (Proof.context -> bool -> typ -> term list -> term)) list +val print_ast_translation: + (string * (Proof.context -> ast list -> ast)) list +\end{ttbox}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Inspecting the syntax% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \end{matharray} + + \begin{description} + + \item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}} prints the inner syntax of the + current context. The output can be quite large; the most important + sections are explained below. + + \begin{description} + + \item \isa{{\isachardoublequote}lexicon{\isachardoublequote}} lists the delimiters of the inner token + language; see \secref{sec:inner-lex}. + + \item \isa{{\isachardoublequote}prods{\isachardoublequote}} lists the productions of the underlying + priority grammar; see \secref{sec:priority-grammar}. + + The nonterminal \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} is rendered in plain text as \isa{{\isachardoublequote}A{\isacharbrackleft}p{\isacharbrackright}{\isachardoublequote}}; delimiters are quoted. Many productions have an extra + \isa{{\isachardoublequote}{\isasymdots}\ {\isacharequal}{\isachargreater}\ name{\isachardoublequote}}. These names later become the heads of parse + trees; they also guide the pretty printer. + + Productions without such parse tree names are called \emph{copy + productions}. Their right-hand side must have exactly one + nonterminal symbol (or named token). The parser does not create a + new parse tree node for copy productions, but simply returns the + parse tree of the right-hand symbol. + + If the right-hand side of a copy production consists of a single + nonterminal without any delimiters, then it is called a \emph{chain + production}. Chain productions act as abbreviations: conceptually, + they are removed from the grammar by adding new productions. + Priority information attached to chain productions is ignored; only + the dummy value \isa{{\isachardoublequote}{\isacharminus}{\isadigit{1}}{\isachardoublequote}} is displayed. + + \item \isa{{\isachardoublequote}print{\isacharunderscore}modes{\isachardoublequote}} lists the alternative print modes + provided by this grammar; see \secref{sec:print-modes}. + + \item \isa{{\isachardoublequote}parse{\isacharunderscore}rules{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}rules{\isachardoublequote}} relate to + syntax translations (macros); see \secref{sec:syn-trans}. + + \item \isa{{\isachardoublequote}parse{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} list sets of constants that invoke + translation functions for abstract syntax trees, which are only + required in very special situations; see \secref{sec:tr-funs}. + + \item \isa{{\isachardoublequote}parse{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}translation{\isachardoublequote}} + list the sets of constants that invoke regular translation + functions; see \secref{sec:tr-funs}. + + \end{description} + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Thu Nov 13 21:45:40 2008 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Thu Nov 13 21:48:19 2008 +0100 @@ -79,6 +79,7 @@ \input{Thy/document/Document_Preparation.tex} \input{Thy/document/Spec.tex} \input{Thy/document/Proof.tex} +\input{Thy/document/Inner_Syntax.tex} \input{Thy/document/Misc.tex} \input{Thy/document/Generic.tex} \input{Thy/document/HOL_Specific.tex}