doc: syntax of constants

parent af2bce08
......@@ -749,7 +749,7 @@ clean::
DOC = doc/manual.pdf
# doc/manual.html
BNF = qualid constant term type formula theory
BNF = qualid constant operator term type formula theory
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
......
......@@ -17,7 +17,7 @@
| "match" ("," term)+ "with" ;
"|"? ("|" formula-case)+ "end" ; pattern matching
| quantifier ("," binders )+ ;
triggers "." formula ; quantifier
triggers? "." formula ; quantifier
| label formula ; label
| "(" formula ")" ; parentheses
\
......@@ -25,5 +25,9 @@
\
binders ::= lident+ ":" type
\
triggers ::= "[" ("|" trigger)+ "]" ;
\
trigger ::= ("," (term | formula))+;
\
formula-case ::= pattern "->" formula ; %
\end{syntax}
......@@ -28,13 +28,27 @@ The syntax for constants is given Figure~\ref{fig:bnf:constant}.
\label{fig:bnf:constant}
\end{figure}
\paragraph{Operators.} Prefix operators have greater priority than
infix operators. Infix operators are left associative and have
priorities set as follows, from greatest to lowest priorities:
\begin{itemize}
\item operators containing only characters from
\textit{op-char-4};
\item those containing
characters from \textit{op-char-3} or \textit{op-char-4};
\item those containing
characters from \textit{op-char-2}, \textit{op-char-3} or
\textit{op-char-4};
\item all other operators.
\end{itemize}
\begin{center}\framebox{\input{./operator_bnf.tex}}\end{center}
\paragraph{Terms.}
The syntax for terms is given Figure~\ref{fig:bnf:term}.
Note the curryfied syntax for function application, though partial
application is not allowed (rejected at typing).
% TODO: prefix and infix operators
\begin{figure}[p]
\begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
\caption{Syntax for terms.}
......@@ -54,8 +68,6 @@ The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
\label{fig:bnf:formula}
\end{figure}
% TODO: triggers
\paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment