# HG changeset patch
# User wenzelm
# Date 1226609691 -3600
# Node ID 8fc228f2186158a4845ad2d92d33ac99b6ec84ef
# Parent  a056077b65a1f8e7ab50d65c16d73bf69a8dfde5
added section "Priority grammars" (variant from old ref manual);

diff -r a056077b65a1 -r 8fc228f21861 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:53:54 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:54:51 2008 +0100
@@ -381,6 +381,87 @@
   \end{description}
 *}
 
+section {* The Pure syntax *}
+
+subsection {* Priority grammars *}
+
+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 = \<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
+  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:
+  @{text "A\<^sup>(\<^sup>p\<^sup>)"}.  In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
+  using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}.  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 @{text G}
+  induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows.  Let @{text
+  \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
+  Then
+  \[
+    @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"}
+  \]
+  if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"}
+  for @{text "p \<le> q"}.
+
+  \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}
+  @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
+  @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
+  @{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
+  @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
+  @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
+  \end{tabular}
+  \end{center}
+  The choice of priorities determines that @{verbatim "-"} binds
+  tighter than @{verbatim "*"}, which binds tighter than @{verbatim
+  "+"}.  Furthermore @{verbatim "+"} associates to the left and
+  @{verbatim "*"} 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 @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
+  (p)"}, i.e.\ the priority of the left-hand side actually appears in
+  a column on the far right.
+
+  \item Alternatives are separated by @{text "|"}.
+
+  \item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
+  but obvious way.
+
+  \end{itemize}
+
+  Using these conventions, the example grammar specification above
+  takes the form:
+  \begin{center}
+  \begin{tabular}{rclc}
+    @{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\
+              & @{text "|"} & @{verbatim "("} @{text A} @{verbatim ")"} \\
+              & @{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}
+*}
+
+
 section {* Syntax and translations \label{sec:syn-trans} *}
 
 text {*