Commit af2bce08 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

doc: syntax of constants

parent 9d874a63
......@@ -749,7 +749,7 @@ clean::
DOC = doc/manual.pdf
# doc/manual.html
BNF = qualid type term formula theory
BNF = qualid constant term type formula theory
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
......
\begin{syntax}
digit ::= "0" - "9" ;
\
hex-digit ::= digit | "a" - "f" | "A" - "F" ;
\
oct-digit ::= "0" - "7"
\
bin-digit ::= "0" | "1"
\
integer ::= digit (digit | "_")* ; decimal
| ("0x" | "0X") hex-digit (hex-digit | "_")* ; hexadecimal
| ("0o" | "0O") oct-digit (oct-digit | "_")* ; octal
| ("0b" | "0B") bin-digit (bin-digit | "_")* ; octal
\
real ::= digit+ exponent ; decimal
| digit+ "." digit* exponent? ;
| digit* "." digit+ exponent? ;
| ("0x" | "0X") hex-real h-exponent ; hexadecimal
\
hex-real ::= hex-digit+ ;
| hex-digit+ "." hex-digit* ;
| hex-digit* "." hex-digit+ ;
\
exponent ::= ("e" | "E") ("-" | "+")? digit+ ;
\
h-exponent ::= ("p" | "P") ("-" | "+")? digit+ ;
| ; %
\end{syntax}
\ No newline at end of file
......@@ -3,10 +3,14 @@
\
ualpha ::= "A"-"Z"
\
alpha ::= lalpha | ualpha
\
lident ::= lalpha (alpha | digit | "'")*
\
uident ::= ualpha (alpha | digit | "'")*
\
ident ::= lident | uident
\
lqualid ::= lident | uqualid "." lident ;
\
uqualid ::= uident | uqualid "." uident ;%
......
\chapter{Syntax Reference}
\label{chap:syntaxref}
This chapter gives the grammar for the input files.
This chapter gives the grammar for \why\ input files.
TODO: constants
% TODO: blanks
\paragraph{Comments.}
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
\paragraph{Strings.}
Strings are enclosed by double quotes (\verb!"!).
% TODO: escape sequences for strings
\paragraph{Identifiers.} The syntax distinguishes lowercase and
uppercase identifiers and, consequently, lowercase and uppercase
uppercase identifiers and, similarly, lowercase and uppercase
qualified identifiers.
\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}
\paragraph{Type Expressions.} The syntax for type
expressions notably differs from the usual ML syntax.
\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
\paragraph{Constants.}
The syntax for constants is given Figure~\ref{fig:bnf:constant}.
\paragraph{Terms and Types.}
\begin{figure}[p]
\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center}
\caption{Syntax for constants.}
\label{fig:bnf:constant}
\end{figure}
\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
% TODO: prefix and infix operators
\begin{figure}
\begin{figure}[p]
\begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
\caption{Syntax for terms.}
\label{fig:bnf:term}
\end{figure}
\paragraph{Type Expressions.} The syntax for type
expressions notably differs from the usual ML syntax.
\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
\paragraph{Formulas.}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
\begin{figure}
\begin{figure}[p]
\begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
\caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}
% TODO: triggers
\paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}.
\begin{figure}
\begin{figure}[p]
\begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
\caption{Syntax for theories.}
\label{fig:bnf:theory}
......
\begin{syntax}
theory ::= "theory" uident label* decl* "end"
\
decl ::= %
decl ::= "type" ("with" type-decl)+ ;
| "logic" ("with" logic-decl)+ ;
| "inductive" ("with" inductive-decl)+ ;
| "axiom" uident ":" formula ;
| "lemma" uident ":" formula ;
| "goal" uident ":" formula ;
| "use" imp-exp tqualid ("as" uident-opt)? ;
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "namespace" "import"? uident-opt decl* "end" ;
\
imp-exp ::= ("import" | "export")?
\
uident-opt ::= uident | "_"
\
subst ::= "with" ("," subst-elt)+
\
subst-elt ::= "type" lqualid "=" lqualid ;
| "logic" lqualid "=" lqualid ;
| "namespace" (uqualid | ".") "=" (uqualid | ".") ;
| "lemma" uqualid ;
| "goal" uqualid ;
\
tqualid ::= uident | ("." ident)+ "." uident ; %
\end{syntax}
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