more on built-in syntax transformations, based on reduced version of old material;
authorwenzelm
Tue Jun 18 15:15:36 2013 +0200 (2013-06-18)
changeset 524148429123bc58a
parent 52413 a59ba6de9687
child 52415 d9fed6e99a57
more on built-in syntax transformations, based on reduced version of old material;
src/Doc/IsarRef/Inner_Syntax.thy
src/Doc/ROOT
src/Doc/Ref/document/root.tex
src/Doc/Ref/document/syntax.tex
src/HOL/Tools/reflection.ML
     1.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Jun 18 12:21:57 2013 +0200
     1.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Jun 18 15:15:36 2013 +0200
     1.3 @@ -1579,4 +1579,131 @@
     1.4    are explicitly known from the given term in its fully internal form.
     1.5  *}
     1.6  
     1.7 +
     1.8 +subsection {* Built-in syntax transformations *}
     1.9 +
    1.10 +text {*
    1.11 +  Here are some further details of the main syntax transformation
    1.12 +  phases of \figref{fig:parse-print}.
    1.13 +*}
    1.14 +
    1.15 +
    1.16 +subsubsection {* Transforming parse trees to ASTs *}
    1.17 +
    1.18 +text {* The parse tree is the raw output of the parser.  It is
    1.19 +  transformed into an AST according to some basic scheme that may be
    1.20 +  augmented by AST translation functions as explained in
    1.21 +  \secref{sec:tr-funs}.
    1.22 +
    1.23 +  The parse tree is constructed by nesting the right-hand sides of the
    1.24 +  productions used to recognize the input.  Such parse trees are
    1.25 +  simply lists of tokens and constituent parse trees, the latter
    1.26 +  representing the nonterminals of the productions.  Ignoring AST
    1.27 +  translation functions, parse trees are transformed to ASTs by
    1.28 +  stripping out delimiters and copy productions, while retaining some
    1.29 +  source position information from input tokens.
    1.30 +
    1.31 +  The Pure syntax provides predefined AST translations to make the
    1.32 +  basic @{text "\<lambda>"}-term structure more apparent within the
    1.33 +  (first-order) AST representation, and thus facilitate the use of
    1.34 +  @{command translations} (see also \secref{sec:syn-trans}).  This
    1.35 +  covers ordinary term application, type application, nested
    1.36 +  abstraction, iterated meta implications and function types.  The
    1.37 +  effect is illustrated on some representative input strings is as
    1.38 +  follows:
    1.39 +
    1.40 +  \begin{center}
    1.41 +  \begin{tabular}{ll}
    1.42 +  input source & AST \\
    1.43 +  \hline
    1.44 +  @{text "f x y z"} & @{verbatim "(f x y z)"} \\
    1.45 +  @{text "'a ty"} & @{verbatim "(ty 'a)"} \\
    1.46 +  @{text "('a, 'b)ty"} & @{verbatim "(ty 'a 'b)"} \\
    1.47 +  @{text "\<lambda>x y z. t"} & @{verbatim "(\"_abs\" x (\"_abs\" y (\"_abs\" z t)))"} \\
    1.48 +  @{text "\<lambda>x :: 'a. t"} & @{verbatim "(\"_abs\" (\"_constrain\" x 'a) t)"} \\
    1.49 +  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim "(\"==>\" P (\"==>\" Q (\"==>\" R S)))"} \\
    1.50 +   @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim "(\"fun\" 'a (\"fun\" 'b (\"fun\" 'c 'd)))"} \\
    1.51 +  \end{tabular}
    1.52 +  \end{center}
    1.53 +
    1.54 +  Note that type and sort constraints may occur in further places ---
    1.55 +  translations need to be ready to cope with them.  The built-in
    1.56 +  syntax transformation from parse trees to ASTs insert additional
    1.57 +  constraints that represent source positions.
    1.58 +*}
    1.59 +
    1.60 +
    1.61 +subsubsection {* Transforming ASTs to terms *}
    1.62 +
    1.63 +text {* After application of macros (\secref{sec:syn-trans}), the AST
    1.64 +  is transformed into a term.  This term still lacks proper type
    1.65 +  information, but it might contain some constraints consisting of
    1.66 +  applications with head @{verbatim "_constrain"}, where the second
    1.67 +  argument is a type encoded as a pre-term within the syntax.  Type
    1.68 +  inference later introduces correct types, or indicates type errors
    1.69 +  in the input.
    1.70 +
    1.71 +  Ignoring parse translations, ASTs are transformed to terms by
    1.72 +  mapping AST constants to term constants, AST variables to term
    1.73 +  variables or constants (according to the name space), and AST
    1.74 +  applications to iterated term applications.
    1.75 +
    1.76 +  The outcome is still a first-order term.  Proper abstractions and
    1.77 +  bound variables are introduced by parse translations associated with
    1.78 +  certain syntax constants.  Thus @{verbatim "(_abs x x)"} eventually
    1.79 +  becomes a de-Bruijn term @{verbatim "Abs (\"x\", _, Bound 0)"}.
    1.80 +*}
    1.81 +
    1.82 +
    1.83 +subsubsection {* Printing of terms *}
    1.84 +
    1.85 +text {* The output phase is essentially the inverse of the input
    1.86 +  phase.  Terms are translated via abstract syntax trees into
    1.87 +  pretty-printed text.
    1.88 +
    1.89 +  Ignoring print translations, the transformation maps term constants,
    1.90 +  variables and applications to the corresponding constructs on ASTs.
    1.91 +  Abstractions are mapped to applications of the special constant
    1.92 +  @{verbatim "_abs"} as seen before.  Type constraints are represented
    1.93 +  via special @{verbatim "_constrain"} forms, according to various
    1.94 +  policies of type annotation determined elsewhere.  Sort constraints
    1.95 +  of type variables are handled in a similar fashion.
    1.96 +
    1.97 +  After application of macros (\secref{sec:syn-trans}), the AST is
    1.98 +  finally pretty-printed.  The built-in print AST translations reverse
    1.99 +  the corresponding parse AST translations.
   1.100 +
   1.101 +  \medskip For the actual printing process, the priority grammar
   1.102 +  (\secref{sec:priority-grammar}) plays a vital role: productions are
   1.103 +  used as templates for pretty printing, with argument slots stemming
   1.104 +  from nonterminals, and syntactic sugar stemming from literal tokens.
   1.105 +
   1.106 +  Each AST application with constant head @{text "c"} and arguments
   1.107 +  @{text "t\<^sub>1"}, \dots, @{text "t\<^sub>n"} (for @{text "n = 0"} the AST is
   1.108 +  just the constant @{text "c"} itself) is printed according to the
   1.109 +  first grammar production of result name @{text "c"}.  The required
   1.110 +  syntax priority of the argument slot is given by its nonterminal
   1.111 +  @{text "A\<^sup>(\<^sup>p\<^sup>)"}.  The argument @{text "t\<^sub>i"} that corresponds to the
   1.112 +  position of @{text "A\<^sup>(\<^sup>p\<^sup>)"} is printed recursively, and then put in
   1.113 +  parentheses \emph{if} its priority @{text "p"} requires this.  The
   1.114 +  resulting output is concatenated with the syntactic sugar according
   1.115 +  to the grammar production.
   1.116 +
   1.117 +  If an AST application @{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} has more arguments than
   1.118 +  the corresponding production, it is first split into @{text "((c x\<^sub>1
   1.119 +  \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots> x\<^sub>m)"} and then printed recursively as above.
   1.120 +
   1.121 +  Applications with too few arguments or with non-constant head or
   1.122 +  without a corresponding production are printed in prefix-form like
   1.123 +  @{text "f t\<^sub>1 \<dots> t\<^sub>n"} for terms.
   1.124 +
   1.125 +  Multiple productions associated with some name @{text "c"} are tried
   1.126 +  in order of appearance within the grammar.  An occurrence of some
   1.127 +  AST variable @{text "x"} is printed as @{text "x"} outright.
   1.128 +
   1.129 +  \medskip White space is \emph{not} inserted automatically.  If
   1.130 +  blanks (or breaks) are required to separate tokens, they need to be
   1.131 +  specified in the mixfix declaration (\secref{sec:mixfix}).
   1.132 +*}
   1.133 +
   1.134  end
     2.1 --- a/src/Doc/ROOT	Tue Jun 18 12:21:57 2013 +0200
     2.2 +++ b/src/Doc/ROOT	Tue Jun 18 15:15:36 2013 +0200
     2.3 @@ -257,7 +257,6 @@
     2.4      "../manual.bib"
     2.5      "document/build"
     2.6      "document/root.tex"
     2.7 -    "document/syntax.tex"
     2.8  
     2.9  session Sledgehammer (doc) in "Sledgehammer" = Pure +
    2.10    options [document_variants = "sledgehammer"]
     3.1 --- a/src/Doc/Ref/document/root.tex	Tue Jun 18 12:21:57 2013 +0200
     3.2 +++ b/src/Doc/Ref/document/root.tex	Tue Jun 18 15:15:36 2013 +0200
     3.3 @@ -41,8 +41,6 @@
     3.4  
     3.5  \pagenumbering{roman} \tableofcontents \clearfirst
     3.6  
     3.7 -\input{syntax}
     3.8 -
     3.9  %%seealso's must be last so that they appear last in the index entries
    3.10  \index{meta-rewriting|seealso{tactics, theorems}}
    3.11  
     4.1 --- a/src/Doc/Ref/document/syntax.tex	Tue Jun 18 12:21:57 2013 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,240 +0,0 @@
     4.4 -
     4.5 -\chapter{Syntax Transformations} \label{chap:syntax}
     4.6 -\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
     4.7 -\newcommand\mtt[1]{\mbox{\tt #1}}
     4.8 -\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits}
     4.9 -\newcommand\Constant{\ttfct{Constant}}
    4.10 -\newcommand\Variable{\ttfct{Variable}}
    4.11 -\newcommand\Appl[1]{\ttfct{Appl}\,[#1]}
    4.12 -\index{syntax!transformations|(}
    4.13 -
    4.14 -
    4.15 -\section{Transforming parse trees to ASTs}\label{sec:astofpt}
    4.16 -\index{ASTs!made from parse trees}
    4.17 -\newcommand\astofpt[1]{\lbrakk#1\rbrakk}
    4.18 -
    4.19 -The parse tree is the raw output of the parser.  Translation functions,
    4.20 -called {\bf parse AST translations}\indexbold{translations!parse AST},
    4.21 -transform the parse tree into an abstract syntax tree.
    4.22 -
    4.23 -The parse tree is constructed by nesting the right-hand sides of the
    4.24 -productions used to recognize the input.  Such parse trees are simply lists
    4.25 -of tokens and constituent parse trees, the latter representing the
    4.26 -nonterminals of the productions.  Let us refer to the actual productions in
    4.27 -the form displayed by {\tt print_syntax} (see \S\ref{sec:inspct-thy} for an
    4.28 -example).
    4.29 -
    4.30 -Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
    4.31 -by stripping out delimiters and copy productions.  More precisely, the
    4.32 -mapping $\astofpt{-}$ is derived from the productions as follows:
    4.33 -\begin{itemize}
    4.34 -\item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id},
    4.35 -  \ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{num}, \ndx{xnum} or \ndx{xstr} token,
    4.36 -  and $s$ its associated string.  Note that for {\tt xstr} this does not
    4.37 -  include the quotes.
    4.38 -
    4.39 -\item Copy productions:\index{productions!copy}
    4.40 -  $\astofpt{\ldots P \ldots} = \astofpt{P}$.  Here $\ldots$ stands for
    4.41 -  strings of delimiters, which are discarded.  $P$ stands for the single
    4.42 -  constituent that is not a delimiter; it is either a nonterminal symbol or
    4.43 -  a name token.
    4.44 -
    4.45 -  \item 0-ary productions: $\astofpt{\ldots \mtt{=>} c} = \Constant c$.
    4.46 -    Here there are no constituents other than delimiters, which are
    4.47 -    discarded.
    4.48 -
    4.49 -  \item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
    4.50 -    the remaining constituents $P@1$, \ldots, $P@n$ are built into an
    4.51 -    application whose head constant is~$c$:
    4.52 -    \[ \astofpt{\ldots P@1 \ldots P@n \ldots \mtt{=>} c} =
    4.53 -       \Appl{\Constant c, \astofpt{P@1}, \ldots, \astofpt{P@n}}
    4.54 -    \]
    4.55 -\end{itemize}
    4.56 -Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
    4.57 -{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.
    4.58 -These examples illustrate the need for further translations to make \AST{}s
    4.59 -closer to the typed $\lambda$-calculus.  The Pure syntax provides
    4.60 -predefined parse \AST{} translations\index{translations!parse AST} for
    4.61 -ordinary applications, type applications, nested abstractions, meta
    4.62 -implications and function types.  Figure~\ref{fig:parse_ast_tr} shows their
    4.63 -effect on some representative input strings.
    4.64 -
    4.65 -
    4.66 -\begin{figure}
    4.67 -\begin{center}
    4.68 -\tt\begin{tabular}{ll}
    4.69 -\rm input string    & \rm \AST \\\hline
    4.70 -"f"                 & f \\
    4.71 -"'a"                & 'a \\
    4.72 -"t == u"            & ("==" t u) \\
    4.73 -"f(x)"              & ("_appl" f x) \\
    4.74 -"f(x, y)"           & ("_appl" f ("_args" x y)) \\
    4.75 -"f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
    4.76 -"\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
    4.77 -\end{tabular}
    4.78 -\end{center}
    4.79 -\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast}
    4.80 -\end{figure}
    4.81 -
    4.82 -\begin{figure}
    4.83 -\begin{center}
    4.84 -\tt\begin{tabular}{ll}
    4.85 -\rm input string            & \rm \AST{} \\\hline
    4.86 -"f(x, y, z)"                & (f x y z) \\
    4.87 -"'a ty"                     & (ty 'a) \\
    4.88 -"('a, 'b) ty"               & (ty 'a 'b) \\
    4.89 -"\%x y z.\ t"               & ("_abs" x ("_abs" y ("_abs" z t))) \\
    4.90 -"\%x ::\ 'a.\ t"            & ("_abs" ("_constrain" x 'a) t) \\
    4.91 -"[| P; Q; R |] => S"        & ("==>" P ("==>" Q ("==>" R S))) \\
    4.92 -"['a, 'b, 'c] => 'd"        & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
    4.93 -\end{tabular}
    4.94 -\end{center}
    4.95 -\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
    4.96 -\end{figure}
    4.97 -
    4.98 -The names of constant heads in the \AST{} control the translation process.
    4.99 -The list of constants invoking parse \AST{} translations appears in the
   4.100 -output of {\tt print_syntax} under {\tt parse_ast_translation}.
   4.101 -
   4.102 -
   4.103 -\section{Transforming ASTs to terms}\label{sec:termofast}
   4.104 -\index{terms!made from ASTs}
   4.105 -\newcommand\termofast[1]{\lbrakk#1\rbrakk}
   4.106 -
   4.107 -The \AST{}, after application of macros (see \S\ref{sec:macros}), is
   4.108 -transformed into a term.  This term is probably ill-typed since type
   4.109 -inference has not occurred yet.  The term may contain type constraints
   4.110 -consisting of applications with head {\tt "_constrain"}; the second
   4.111 -argument is a type encoded as a term.  Type inference later introduces
   4.112 -correct types or rejects the input.
   4.113 -
   4.114 -Another set of translation functions, namely parse
   4.115 -translations\index{translations!parse}, may affect this process.  If we
   4.116 -ignore parse translations for the time being, then \AST{}s are transformed
   4.117 -to terms by mapping \AST{} constants to constants, \AST{} variables to
   4.118 -schematic or free variables and \AST{} applications to applications.
   4.119 -
   4.120 -More precisely, the mapping $\termofast{-}$ is defined by
   4.121 -\begin{itemize}
   4.122 -\item Constants: $\termofast{\Constant x} = \ttfct{Const} (x,
   4.123 -  \mtt{dummyT})$.
   4.124 -
   4.125 -\item Schematic variables: $\termofast{\Variable \mtt{"?}xi\mtt"} =
   4.126 -  \ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$
   4.127 -  the index extracted from~$xi$.
   4.128 -
   4.129 -\item Free variables: $\termofast{\Variable x} = \ttfct{Free} (x,
   4.130 -  \mtt{dummyT})$.
   4.131 -
   4.132 -\item Function applications with $n$ arguments:
   4.133 -    \[ \termofast{\Appl{f, x@1, \ldots, x@n}} =
   4.134 -       \termofast{f} \ttapp
   4.135 -         \termofast{x@1} \ttapp \ldots \ttapp \termofast{x@n}
   4.136 -    \]
   4.137 -\end{itemize}
   4.138 -Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and
   4.139 -\verb|$|\index{$@{\tt\$}} are constructors of the datatype \mltydx{term},
   4.140 -while \ttindex{dummyT} stands for some dummy type that is ignored during
   4.141 -type inference.
   4.142 -
   4.143 -So far the outcome is still a first-order term.  Abstractions and bound
   4.144 -variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
   4.145 -by parse translations.  Such translations are attached to {\tt "_abs"},
   4.146 -{\tt "!!"} and user-defined binders.
   4.147 -
   4.148 -
   4.149 -\section{Printing of terms}
   4.150 -\newcommand\astofterm[1]{\lbrakk#1\rbrakk}\index{ASTs!made from terms}
   4.151 -
   4.152 -The output phase is essentially the inverse of the input phase.  Terms are
   4.153 -translated via abstract syntax trees into strings.  Finally the strings are
   4.154 -pretty printed.
   4.155 -
   4.156 -Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
   4.157 -terms into \AST{}s.  Ignoring those, the transformation maps
   4.158 -term constants, variables and applications to the corresponding constructs
   4.159 -on \AST{}s.  Abstractions are mapped to applications of the special
   4.160 -constant {\tt _abs}.
   4.161 -
   4.162 -More precisely, the mapping $\astofterm{-}$ is defined as follows:
   4.163 -\begin{itemize}
   4.164 -  \item $\astofterm{\ttfct{Const} (x, \tau)} = \Constant x$.
   4.165 -
   4.166 -  \item $\astofterm{\ttfct{Free} (x, \tau)} = constrain (\Variable x,
   4.167 -    \tau)$.
   4.168 -
   4.169 -  \item $\astofterm{\ttfct{Var} ((x, i), \tau)} = constrain (\Variable
   4.170 -    \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
   4.171 -    the {\tt indexname} $(x, i)$.
   4.172 -
   4.173 -  \item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
   4.174 -    of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
   4.175 -    be obtained from~$t$ by replacing all bound occurrences of~$x$ by
   4.176 -    the free variable $x'$.  This replaces corresponding occurrences of the
   4.177 -    constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
   4.178 -    \mtt{dummyT})$:
   4.179 -   \[ \astofterm{\ttfct{Abs} (x, \tau, t)} =
   4.180 -      \Appl{\Constant \mtt{"_abs"},
   4.181 -        constrain(\Variable x', \tau), \astofterm{t'}}
   4.182 -    \]
   4.183 -
   4.184 -  \item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.
   4.185 -    The occurrence of constructor \ttindex{Bound} should never happen
   4.186 -    when printing well-typed terms; it indicates a de Bruijn index with no
   4.187 -    matching abstraction.
   4.188 -
   4.189 -  \item Where $f$ is not an application,
   4.190 -    \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} =
   4.191 -       \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}}
   4.192 -    \]
   4.193 -\end{itemize}
   4.194 -%
   4.195 -Type constraints\index{type constraints} are inserted to allow the printing
   4.196 -of types.  This is governed by the boolean variable \ttindex{show_types}:
   4.197 -\begin{itemize}
   4.198 -  \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
   4.199 -    \ttindex{show_types} is set to {\tt false}.
   4.200 -
   4.201 -  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x,
   4.202 -         \astofterm{\tau}}$ \ otherwise.
   4.203 -
   4.204 -    Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type
   4.205 -    constructors go to {\tt Constant}s; type identifiers go to {\tt
   4.206 -      Variable}s; type applications go to {\tt Appl}s with the type
   4.207 -    constructor as the first element.  If \ttindex{show_sorts} is set to
   4.208 -    {\tt true}, some type variables are decorated with an \AST{} encoding
   4.209 -    of their sort.
   4.210 -\end{itemize}
   4.211 -%
   4.212 -The \AST{}, after application of macros (see \S\ref{sec:macros}), is
   4.213 -transformed into the final output string.  The built-in {\bf print AST
   4.214 -  translations}\indexbold{translations!print AST} reverse the
   4.215 -parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
   4.216 -
   4.217 -For the actual printing process, the names attached to productions
   4.218 -of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
   4.219 -a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
   4.220 -$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
   4.221 -for~$c$.  Each argument~$x@i$ is converted to a string, and put in
   4.222 -parentheses if its priority~$(p@i)$ requires this.  The resulting strings
   4.223 -and their syntactic sugar (denoted by \dots{} above) are joined to make a
   4.224 -single string.
   4.225 -
   4.226 -If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments
   4.227 -than the corresponding production, it is first split into
   4.228 -$((\mtt"c\mtt"~ x@1 \ldots x@n) ~ x@{n+1} \ldots x@m)$.  Applications
   4.229 -with too few arguments or with non-constant head or without a
   4.230 -corresponding production are printed as $f(x@1, \ldots, x@l)$ or
   4.231 -$(\alpha@1, \ldots, \alpha@l) ty$.  Multiple productions associated
   4.232 -with some name $c$ are tried in order of appearance.  An occurrence of
   4.233 -$\Variable x$ is simply printed as~$x$.
   4.234 -
   4.235 -Blanks are {\em not\/} inserted automatically.  If blanks are required to
   4.236 -separate tokens, specify them in the mixfix declaration, possibly preceded
   4.237 -by a slash~({\tt/}) to allow a line break.
   4.238 -\index{ASTs|)}
   4.239 -
   4.240 -%%% Local Variables: 
   4.241 -%%% mode: latex
   4.242 -%%% TeX-master: "ref"
   4.243 -%%% End: