src/Doc/Isar_Ref/Inner_Syntax.thy

 theory Inner_Syntax
 imports Base Main
 begin
 
-chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}
-
-text {* The inner syntax of Isabelle provides concrete notation for
+chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
+
+text \<open>The inner syntax of Isabelle provides concrete notation for
   the main entities of the logical framework, notably @{text
   "\<lambda>"}-terms with types and type classes.  Applications may either
   extend existing syntactic categories by additional notation, or
   define new sub-languages that are linked to the standard term
   language via some explicit markers.  For example @{verbatim

 
   Further details of the syntax engine involves the classical
   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 *}
-
-subsection {* Diagnostic commands \label{sec:print-diag} *}
-
-text {*
+\<close>
+
+
+section \<open>Printing logical entities\<close>
+
+subsection \<open>Diagnostic commands \label{sec:print-diag}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

   @{cite "isabelle-sys"}.
 
   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 *}
-
-text {*
+\<close>
+
+
+subsection \<open>Details of printed content\<close>
+
+text \<open>
   \begin{tabular}{rcll}
     @{attribute_def show_markup} & : & @{text attribute} \\
     @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
     @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
     @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\

   question mark is affected, the remaining text is unchanged
   (including proper markup for schematic variables that might be
   relevant for user interfaces).
 
   \end{description}
-*}
-
-
-subsection {* Alternative print modes \label{sec:print-modes} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Alternative print modes \label{sec:print-modes}\<close>
+
+text \<open>
   \begin{mldecls}
     @{index_ML print_mode_value: "unit -> string list"} \\
     @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   \end{mldecls}
 

   \item @{verbatim latex}: additional mode that is active in {\LaTeX}
   document preparation of Isabelle theory sources; allows to provide
   alternative output notation.
 
   \end{itemize}
-*}
-
-
-section {* Mixfix annotations \label{sec:mixfix} *}
-
-text {* Mixfix annotations specify concrete \emph{inner syntax} of
+\<close>
+
+
+section \<open>Mixfix annotations \label{sec:mixfix}\<close>
+
+text \<open>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
   describes the concrete syntax, the translation to abstract
   syntax, and the pretty printing.  Special case annotations provide a

   fixed variables may be declared as @{keyword "structure"}.
 
   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.  *}
-
-
-subsection {* The general mixfix form *}
-
-text {* In full generality, mixfix declarations work as follows.
+  ``@{verbatim "++"}'' for an infix symbol.\<close>
+
+
+subsection \<open>The general mixfix form\<close>
+
+text \<open>In full generality, mixfix declarations work as follows.
   Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is annotated by
   @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text "mixfix"} is a string
   @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of delimiters that surround
   argument positions as indicated by underscores.
 

 
   \end{description}
 
   The general idea of pretty printing with blocks and breaks is also
   described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
-*}
-
-
-subsection {* Infixes *}
-
-text {* Infix operators are specified by convenient short forms that
+\<close>
+
+
+subsection \<open>Infixes\<close>
+
+text \<open>Infix operators are specified by convenient short forms that
   abbreviate general mixfix annotations as follows:
 
   \begin{center}
   \begin{tabular}{lll}
 

   pretty printing block.
 
   The alternative notation @{verbatim "op"}~@{text sy} is introduced
   in addition.  Thus any infix operator may be written in prefix form
   (as in ML), independently of the number of arguments in the term.
-*}
-
-
-subsection {* Binders *}
-
-text {* A \emph{binder} is a variable-binding construct such as a
+\<close>
+
+
+subsection \<open>Binders\<close>
+
+text \<open>A \emph{binder} is a variable-binding construct such as a
   quantifier.  The idea to formalize @{text "\<forall>x. b"} as @{text "All
   (\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back
   to @{cite church40}.  Isabelle declarations of certain higher-order
   operators may be annotated with @{keyword_def "binder"} annotations
   as follows:

   syntax ends with a token that may be continued by an identifier
   token at the start of @{syntax (inner) idts}.
 
   Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1
   \<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}.
-  This works in both directions, for parsing and printing.  *}
-
-
-section {* Explicit notation \label{sec:notation} *}
-
-text {*
+  This works in both directions, for parsing and printing.\<close>
+
+
+section \<open>Explicit notation \label{sec:notation}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

 
   \item @{command "write"} is similar to @{command "notation"}, but
   works within an Isar proof body.
 
   \end{description}
-*}
-
-
-section {* The Pure syntax \label{sec:pure-syntax} *}
-
-subsection {* Lexical matters \label{sec:inner-lex} *}
-
-text {* The inner lexical syntax vaguely resembles the outer one
+\<close>
+
+
+section \<open>The Pure syntax \label{sec:pure-syntax}\<close>
+
+subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
+
+text \<open>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}
 

   "~~/src/HOL/Tools/string_syntax.ML"}).
 
   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} *}
-
-text {* A context-free grammar consists of a set of \emph{terminal
+\<close>
+
+
+subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
+
+text \<open>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 = \<gamma>"},
   where @{text A} is a nonterminal and @{text \<gamma>} is a string of
   terminals and nonterminals.  One designated nonterminal is called
   the \emph{root symbol}.  The language defined by the grammar

               & @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
               & @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
               & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
   \end{tabular}
   \end{center}
-*}
-
-
-subsection {* The Pure grammar \label{sec:pure-grammar} *}
-
-text {* The priority grammar of the @{text "Pure"} theory is defined
+\<close>
+
+
+subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
+
+text \<open>The priority grammar of the @{text "Pure"} theory is defined
   approximately like this:
 
   \begin{center}
   \begin{supertabular}{rclr}
 

   \item @{verbatim XCONST} is similar to @{verbatim CONST}, but
   retains the constant name as given.  This is only relevant to
   translation rules (\secref{sec:syn-trans}), notably on the LHS.
 
   \end{itemize}
-*}
-
-
-subsection {* Inspecting the syntax *}
-
-text {*
+\<close>
+
+
+subsection \<open>Inspecting the syntax\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
   \begin{description}

   functions; see \secref{sec:tr-funs}.
 
   \end{description}
 
   \end{description}
-*}
-
-
-subsection {* Ambiguity of parsed expressions *}
-
-text {*
+\<close>
+
+
+subsection \<open>Ambiguity of parsed expressions\<close>
+
+text \<open>
   \begin{tabular}{rcll}
     @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
     @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
   \end{tabular}
 

   \item @{attribute syntax_ambiguity_limit} determines the number of
   resulting parse trees that are shown as part of the printed message
   in case of an ambiguity.
 
   \end{description}
-*}
-
-
-section {* Syntax transformations \label{sec:syntax-transformations} *}
-
-text {* The inner syntax engine of Isabelle provides separate
+\<close>
+
+
+section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
+
+text \<open>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 "\<lambda>"}-terms (\secref{sec:tr-funs}).  This works
   both for parsing and printing, as outlined in
   \figref{fig:parse-print}.

 
   As a rule of thumb, anything that manipulates bindings of variables
   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. *}
-
-
-subsection {* Abstract syntax trees \label{sec:ast} *}
-
-text {* The ML datatype @{ML_type Ast.ast} explicitly represents the
+  Isabelle/Pure.\<close>
+
+
+subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
+
+text \<open>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}
   datatype ast =
     Constant of string |

   @{verbatim "\"_abs\""} does not bind the @{verbatim x} in any way.
   Proper bindings are introduced in later stages of the term syntax,
   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 *}
-
-text {* Depending on the situation --- input syntax, output syntax,
+\<close>
+
+
+subsubsection \<open>AST constants versus variables\<close>
+
+text \<open>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.
 
   Input syntax of a term such as @{text "f a b = c"} does not yet

   since the concrete syntax already distinguishes type variables from
   type constants (constructors).  So @{text "('a, 'b) foo"}
   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.  *}
-
-
-subsubsection {* Authentic syntax names *}
-
-text {* Naming constant entities within ASTs is another delicate
+  while in the AST the constructor occurs in head position.\<close>
+
+
+subsubsection \<open>Authentic syntax names\<close>
+
+text \<open>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
   resolution, there can be surprises in boundary cases.
 

   \end{itemize}
 
   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. *}
-
-
-subsection {* Raw syntax and translations \label{sec:syn-trans} *}
-
-text {*
+  to be translated usually correspond to some concrete notation.\<close>
+
+
+subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
+
+text \<open>
   \begin{tabular}{rcll}
     @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\

   syntax translations.  For example, consider list filter
   comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
   List} in Isabelle/HOL.
 
   \end{itemize}
-*}
-
-subsubsection {* Applying translation rules *}
-
-text {* As a term is being parsed or printed, an AST is generated as
+\<close>
+
+subsubsection \<open>Applying translation rules\<close>
+
+text \<open>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
   rule is applied.
 

   to @{text "Ball A P"} and the standard print rule would fail to
   apply.  This problem can be avoided by hand-written ML translation
   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} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Syntax translation functions \label{sec:tr-funs}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\

   that the usual naming convention makes syntax constants start with
   underscore, to reduce the chance of accidental clashes with other
   names occurring in parse trees (unqualified constants etc.).
 
   \end{description}
-*}
-
-
-subsubsection {* The translation strategy *}
-
-text {* The different kinds of translation functions are invoked during
+\<close>
+
+
+subsubsection \<open>The translation strategy\<close>
+
+text \<open>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 \<dots> x\<^sub>n"} is encountered, and a translation function
   @{text "f"} of appropriate kind is declared for @{text "c"}, the
   result is produced by evaluation of @{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} in ML.

   heads of concrete syntax, or syntactic constants introduced via
   other translations.  For plain identifiers within the term language,
   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 *}
-
-text {*
+\<close>
+
+
+subsection \<open>Built-in syntax transformations\<close>
+
+text \<open>
   Here are some further details of the main syntax transformation
   phases of \figref{fig:parse-print}.
-*}
-
-
-subsubsection {* Transforming parse trees to ASTs *}
-
-text {* The parse tree is the raw output of the parser.  It is
+\<close>
+
+
+subsubsection \<open>Transforming parse trees to ASTs\<close>
+
+text \<open>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}.
 
   The parse tree is constructed by nesting the right-hand sides of the

 
   Note that type and sort constraints may occur in further places ---
   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 *}
-
-text {* After application of macros (\secref{sec:syn-trans}), the AST
+\<close>
+
+
+subsubsection \<open>Transforming ASTs to terms\<close>
+
+text \<open>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
   argument is a type encoded as a pre-term within the syntax.  Type
   inference later introduces correct types, or indicates type errors

 
   The outcome is still a first-order term.  Proper abstractions and
   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 *}
-
-text {* The output phase is essentially the inverse of the input
+\<close>
+
+
+subsubsection \<open>Printing of terms\<close>
+
+text \<open>The output phase is essentially the inverse of the input
   phase.  Terms are translated via abstract syntax trees into
   pretty-printed text.
 
   Ignoring print translations, the transformation maps term constants,
   variables and applications to the corresponding constructs on ASTs.

   AST variable @{text "x"} is printed as @{text "x"} outright.
 
   \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}).
-*}
+\<close>
 
 end