diff -r 4f169d2cf6f3 -r 782f0b662cae src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 07 21:28:24 2014 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 07 21:29:59 2014 +0200 @@ -2,9 +2,9 @@ imports Base Main begin -chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *} +chapter \Inner syntax --- the term language \label{ch:inner-syntax}\ -text {* The inner syntax of Isabelle provides concrete notation for +text \The inner syntax of Isabelle provides concrete notation for the main entities of the logical framework, notably @{text "\"}-terms with types and type classes. Applications may either extend existing syntactic categories by additional notation, or @@ -25,14 +25,14 @@ distinction of lexical language versus context-free grammar (see \secref{sec:pure-syntax}), and various mechanisms for \emph{syntax transformations} (see \secref{sec:syntax-transformations}). -*} +\ -section {* Printing logical entities *} +section \Printing logical entities\ -subsection {* Diagnostic commands \label{sec:print-diag} *} +subsection \Diagnostic commands \label{sec:print-diag}\ -text {* +text \ \begin{matharray}{rcl} @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -115,12 +115,12 @@ Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic way to include formal items into the printed text document. -*} +\ -subsection {* Details of printed content *} +subsection \Details of printed content\ -text {* +text \ \begin{tabular}{rcll} @{attribute_def show_markup} & : & @{text attribute} \\ @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\ @@ -241,12 +241,12 @@ relevant for user interfaces). \end{description} -*} +\ -subsection {* Alternative print modes \label{sec:print-modes} *} +subsection \Alternative print modes \label{sec:print-modes}\ -text {* +text \ \begin{mldecls} @{index_ML print_mode_value: "unit -> string list"} \\ @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\ @@ -312,12 +312,12 @@ alternative output notation. \end{itemize} -*} +\ -section {* Mixfix annotations \label{sec:mixfix} *} +section \Mixfix annotations \label{sec:mixfix}\ -text {* Mixfix annotations specify concrete \emph{inner syntax} of +text \Mixfix annotations specify concrete \emph{inner syntax} of Isabelle types and terms. Locally fixed parameters in toplevel theorem statements, locale and class specifications also admit mixfix annotations in a fairly uniform manner. A mixfix annotation @@ -352,12 +352,12 @@ 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. *} + ``@{verbatim "++"}'' for an infix symbol.\ -subsection {* The general mixfix form *} +subsection \The general mixfix form\ -text {* In full generality, mixfix declarations work as follows. +text \In full generality, mixfix declarations work as follows. Suppose a constant @{text "c :: \\<^sub>1 \ \ \\<^sub>n \ \"} is annotated by @{text "(mixfix [p\<^sub>1, \, p\<^sub>n] p)"}, where @{text "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \ _ d\<^sub>n"} consisting of delimiters that surround @@ -436,12 +436,12 @@ The general idea of pretty printing with blocks and breaks is also described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}. -*} +\ -subsection {* Infixes *} +subsection \Infixes\ -text {* Infix operators are specified by convenient short forms that +text \Infix operators are specified by convenient short forms that abbreviate general mixfix annotations as follows: \begin{center} @@ -468,12 +468,12 @@ The alternative notation @{verbatim "op"}~@{text sy} is introduced in addition. Thus any infix operator may be written in prefix form (as in ML), independently of the number of arguments in the term. -*} +\ -subsection {* Binders *} +subsection \Binders\ -text {* A \emph{binder} is a variable-binding construct such as a +text \A \emph{binder} is a variable-binding construct such as a quantifier. The idea to formalize @{text "\x. b"} as @{text "All (\x. b)"} for @{text "All :: ('a \ bool) \ bool"} already goes back to @{cite church40}. Isabelle declarations of certain higher-order @@ -509,12 +509,12 @@ Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1 \ x\<^sub>n b"} into iterated application @{text "c (\x\<^sub>1. \ c (\x\<^sub>n. b)\)"}. - This works in both directions, for parsing and printing. *} + This works in both directions, for parsing and printing.\ -section {* Explicit notation \label{sec:notation} *} +section \Explicit notation \label{sec:notation}\ -text {* +text \ \begin{matharray}{rcll} @{command_def "type_notation"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "no_type_notation"} & : & @{text "local_theory \ local_theory"} \\ @@ -562,14 +562,14 @@ works within an Isar proof body. \end{description} -*} +\ -section {* The Pure syntax \label{sec:pure-syntax} *} +section \The Pure syntax \label{sec:pure-syntax}\ -subsection {* Lexical matters \label{sec:inner-lex} *} +subsection \Lexical matters \label{sec:inner-lex}\ -text {* The inner lexical syntax vaguely resembles the outer one +text \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: @@ -617,12 +617,12 @@ The derived categories @{syntax_def (inner) num_const}, and @{syntax_def (inner) float_const}, provide robust access to the respective tokens: the syntax tree holds a syntactic constant instead of a free variable. -*} +\ -subsection {* Priority grammars \label{sec:priority-grammar} *} +subsection \Priority grammars \label{sec:priority-grammar}\ -text {* A context-free grammar consists of a set of \emph{terminal +text \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 @{text "A = \"}, where @{text A} is a nonterminal and @{text \} is a string of @@ -692,12 +692,12 @@ & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ \end{tabular} \end{center} -*} +\ -subsection {* The Pure grammar \label{sec:pure-grammar} *} +subsection \The Pure grammar \label{sec:pure-grammar}\ -text {* The priority grammar of the @{text "Pure"} theory is defined +text \The priority grammar of the @{text "Pure"} theory is defined approximately like this: \begin{center} @@ -896,12 +896,12 @@ translation rules (\secref{sec:syn-trans}), notably on the LHS. \end{itemize} -*} +\ -subsection {* Inspecting the syntax *} +subsection \Inspecting the syntax\ -text {* +text \ \begin{matharray}{rcl} @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} @@ -956,12 +956,12 @@ \end{description} \end{description} -*} +\ -subsection {* Ambiguity of parsed expressions *} +subsection \Ambiguity of parsed expressions\ -text {* +text \ \begin{tabular}{rcll} @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\ @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\ @@ -991,12 +991,12 @@ in case of an ambiguity. \end{description} -*} +\ -section {* Syntax transformations \label{sec:syntax-transformations} *} +section \Syntax transformations \label{sec:syntax-transformations}\ -text {* The inner syntax engine of Isabelle provides separate +text \The inner syntax engine of Isabelle provides separate mechanisms to transform parse trees either via rewrite systems on first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs or syntactic @{text "\"}-terms (\secref{sec:tr-funs}). This works @@ -1042,12 +1042,12 @@ or constants needs to be implemented as syntax transformation (see below). Anything else is better done via check/uncheck: a prominent example application is the @{command abbreviation} concept of - Isabelle/Pure. *} + Isabelle/Pure.\ -subsection {* Abstract syntax trees \label{sec:ast} *} +subsection \Abstract syntax trees \label{sec:ast}\ -text {* The ML datatype @{ML_type Ast.ast} explicitly represents the +text \The ML datatype @{ML_type Ast.ast} explicitly represents the intermediate AST format that is used for syntax rewriting (\secref{sec:syn-trans}). It is defined in ML as follows: \begin{ttbox} @@ -1081,12 +1081,12 @@ where @{verbatim "(\"_abs\" x t)"} becomes an @{ML Abs} node and occurrences of @{verbatim x} in @{verbatim t} are replaced by bound variables (represented as de-Bruijn indices). -*} +\ -subsubsection {* AST constants versus variables *} +subsubsection \AST constants versus variables\ -text {* Depending on the situation --- input syntax, output syntax, +text \Depending on the situation --- input syntax, output syntax, translation patterns --- the distinction of atomic ASTs as @{ML Ast.Constant} versus @{ML Ast.Variable} serves slightly different purposes. @@ -1121,12 +1121,12 @@ corresponds to an AST application of some constant for @{text foo} and variable arguments for @{text "'a"} and @{text "'b"}. Note that the postfix application is merely a feature of the concrete syntax, - while in the AST the constructor occurs in head position. *} + while in the AST the constructor occurs in head position.\ -subsubsection {* Authentic syntax names *} +subsubsection \Authentic syntax names\ -text {* Naming constant entities within ASTs is another delicate +text \Naming constant entities within ASTs is another delicate issue. Unqualified names are resolved in the name space tables in the last stage of parsing, after all translations have been applied. Since syntax transformations do not know about this later name @@ -1160,12 +1160,12 @@ In other words, syntax transformations that operate on input terms written as prefix applications are difficult to make robust. Luckily, this case rarely occurs in practice, because syntax forms - to be translated usually correspond to some concrete notation. *} + to be translated usually correspond to some concrete notation.\ -subsection {* Raw syntax and translations \label{sec:syn-trans} *} +subsection \Raw syntax and translations \label{sec:syn-trans}\ -text {* +text \ \begin{tabular}{rcll} @{command_def "nonterminal"} & : & @{text "theory \ theory"} \\ @{command_def "syntax"} & : & @{text "theory \ theory"} \\ @@ -1337,11 +1337,11 @@ List} in Isabelle/HOL. \end{itemize} -*} +\ -subsubsection {* Applying translation rules *} +subsubsection \Applying translation rules\ -text {* As a term is being parsed or printed, an AST is generated as +text \As a term is being parsed or printed, an AST is generated as an intermediate form according to \figref{fig:parse-print}. The AST is normalized by applying translation rules in the manner of a first-order term rewriting system. We first examine how a single @@ -1410,12 +1410,12 @@ functions (see also \secref{sec:tr-funs}), which is in fact the same mechanism used in built-in @{keyword "binder"} declarations. \end{warn} -*} +\ -subsection {* Syntax translation functions \label{sec:tr-funs} *} +subsection \Syntax translation functions \label{sec:tr-funs}\ -text {* +text \ \begin{matharray}{rcl} @{command_def "parse_ast_translation"} & : & @{text "theory \ theory"} \\ @{command_def "parse_translation"} & : & @{text "theory \ theory"} \\ @@ -1492,12 +1492,12 @@ names occurring in parse trees (unqualified constants etc.). \end{description} -*} +\ -subsubsection {* The translation strategy *} +subsubsection \The translation strategy\ -text {* The different kinds of translation functions are invoked during +text \The different kinds of translation functions are invoked during the transformations between parse trees, ASTs and syntactic terms (cf.\ \figref{fig:parse-print}). Whenever a combination of the form @{text "c x\<^sub>1 \ x\<^sub>n"} is encountered, and a translation function @@ -1545,20 +1545,20 @@ the status of constant versus variable is not yet know during parsing. This is in contrast to print translations, where constants are explicitly known from the given term in its fully internal form. -*} +\ -subsection {* Built-in syntax transformations *} +subsection \Built-in syntax transformations\ -text {* +text \ Here are some further details of the main syntax transformation phases of \figref{fig:parse-print}. -*} +\ -subsubsection {* Transforming parse trees to ASTs *} +subsubsection \Transforming parse trees to ASTs\ -text {* The parse tree is the raw output of the parser. It is +text \The parse tree is the raw output of the parser. It is transformed into an AST according to some basic scheme that may be augmented by AST translation functions as explained in \secref{sec:tr-funs}. @@ -1598,12 +1598,12 @@ translations need to be ready to cope with them. The built-in syntax transformation from parse trees to ASTs insert additional constraints that represent source positions. -*} +\ -subsubsection {* Transforming ASTs to terms *} +subsubsection \Transforming ASTs to terms\ -text {* After application of macros (\secref{sec:syn-trans}), the AST +text \After application of macros (\secref{sec:syn-trans}), the AST is transformed into a term. This term still lacks proper type information, but it might contain some constraints consisting of applications with head @{verbatim "_constrain"}, where the second @@ -1620,12 +1620,12 @@ bound variables are introduced by parse translations associated with certain syntax constants. Thus @{verbatim "(_abs x x)"} eventually becomes a de-Bruijn term @{verbatim "Abs (\"x\", _, Bound 0)"}. -*} +\ -subsubsection {* Printing of terms *} +subsubsection \Printing of terms\ -text {* The output phase is essentially the inverse of the input +text \The output phase is essentially the inverse of the input phase. Terms are translated via abstract syntax trees into pretty-printed text. @@ -1672,6 +1672,6 @@ \medskip White space is \emph{not} inserted automatically. If blanks (or breaks) are required to separate tokens, they need to be specified in the mixfix declaration (\secref{sec:mixfix}). -*} +\ end