Commit fd64d61e authored by Andrei Paskevich's avatar Andrei Paskevich

update bnf files for WhyML

parent 6050c62b
......@@ -1200,7 +1200,7 @@ doc: doc/manual.pdf
# doc/manual.html
BNF = qualid label constant operator term type formula theory theory2 \
why_file typev expr expr2 module whyml_file
why_file spec expr expr2 module whyml_file
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
......
......@@ -8,38 +8,40 @@
| expr "[" expr "]" "<-" expr ; brackets assignment
| expr "[" expr infix-op-1 expr "]" ; ternary brackets
| expr expr+ ; function application
| "fun" type-v-param+ "->" triple ; lambda abstraction
| "let" "rec" recfun ("with" recfun)* ; recursive functions
| "fun" binder+ spec* "->" spec* expr ; lambda abstraction
| "let" "rec" rec-defn "in" expr ; recursive functions
| "let" fun-defn "in" expr ; local function
| "if" expr "then" expr ("else" expr)? ; conditional
| expr ";" expr ; sequence
| "loop" loop-annot "end" ; infinite loop
| "loop" invariant* variant? expr "end" ; infinite loop
| "while" expr ; while loop
"do" loop-annot expr "done" ;
"do" invariant* variant? expr "done" ;
| "for" lident "=" expr to-downto expr ; for loop
"do" loop-inv expr "done" ;
| assert annotation ; assertion
| "absurd" ;
"do" invariant* expr "done" ;
| assertion ; assertion
| "raise" uqualid ; exception raising
| "raise" "(" uqualid expr ")" ;
| "try" expr "with" ("|" handler)+ "end" ; exception catching
| "any" type-c ;
| "any" type spec* ;
| "abstract" expr spec* ; blackbox
| "let" pattern "=" expr "in" expr ; local binding
| "match" expr ("," expr)* "with" ; pattern matching
("|" expr-case)+ "end" ;
"|"? expr-case ("|" expr-case)* "end" ;
| "(" expr ("," expr)+ ")" ; tuple
| "{" field-value+ "}" ; record
| "{" expr-field+ "}" ; record
| expr "." lqualid ; field access
| expr "." lqualid "<-" expr ; field assignment
| "{" expr "with" field-value+ "}" ; field update
| "{" expr "with" expr-field+ "}" ; field update
| expr ":" type ; cast
| "ghost" expr ; ghost expression
| label expr ; label
| "'" uident ":" expr ; code mark
| "(" expr ")" ; parentheses
\
expr-case ::= pattern "->" expr ;
\
field-value ::= lqualid "=" expr ";" ;
expr-field ::= lqualid "=" expr ";" ;
\
handler ::= uqualid pattern? "->" expr
\
triple ::= expr ;
| pre expr post ; Hoare triple
\end{syntax}
\begin{syntax}
assert ::= "assert" | "assume" | "check"
rec-defn ::= fun-defn ("with" fun-defn)* ;
\
to-downto ::= "to" | "downto"
fun-defn ::= "ghost"? lident label* fun-body ;
\
loop-annot ::= loop-inv? variant?
fun-body ::= binder+ (":" type)? spec* "=" spec* expr ;
\
loop-inv ::= "invariant" annotation
binder ::= "ghost"? lident label*
| param
\
param ::= "(" ("ghost"? lident label*)+ ":" type ")" ;
\
variant ::= "variant" "{" term "}" ("with" lqualid)?
\end{syntax}
......@@ -18,7 +18,7 @@
\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
\newif\ifspace
\newif\ifnewentry
\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
\newcommand{\addspace}{\ifspace \: \spacefalse \fi}
\newcommand{\term}[2]{\addspace\mbox{\lstinline|#1|%
\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
\newcommand{\nonterm}[2]{%
......
......@@ -3,29 +3,28 @@
\
mdecl ::= decl ; theory declaration
| "type" mtype-decl ("with" mtype-decl)* ; mutable types
| "let" lident label* pgm-defn ;
| "let" "rec" recfun ("with" recfun)* ;
| "val" lident label* pgm-decl ;
| "type" lident ("'" lident)* invariant+ ; added invariant
| "let" "ghost"? lident label* pgm-defn ;
| "let" "rec" rec-defn ;
| "val" "ghost"? lident label* pgm-decl ;
| "exception" lident label* type? ;
| "use" imp-exp "module" tqualid ;
("as" uident-opt)? ;
| "namespace" "import"? uident-opt ;
mdecl* "end" ;
| "namespace" "import"? uident mdecl* "end" ;
\
mtype-decl ::= lident label* ("'" lident label*)* ;
mtype-defn ;
\
mtype-defn ::= ; abstract type
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{" mrecord-field ; record type
(";" mrecord-field)* "}" ;
| "=" "|"? type-case ("|" type-case)* invariant* ; algebraic type
| "=" "{" mrecord-field (";" mrecord-field)* "}" ; record type
invariant*
\
mrecord-field ::= "mutable"? lident label* ":" type
mrecord-field ::= "ghost"? "mutable"? lident label* ":" type
\
pgm-decl ::= ":" type-v ;
| type-v-param+ ":" type-c ;
pgm-defn ::= fun-body ;
| "=" "fun" binder+ spec* "->" spec* expr ;
\
pgm-decl ::= ":" type ; global variable
| param (spec* param)+ ":" type spec* ; abstract function
\
pgm-defn ::= type-v-param+ (":" type)? "=" triple ;
| "=" "fun" type-v-param+ "->" triple ;
\end{syntax}
\begin{syntax}
spec ::= requires | ensures | returns | raises ;
| reads | writes | variant
\
requires ::= "requires" "{" formula "}"
\
ensures ::= "ensures" "{" formula "}"
\
returns ::= "returns" "{" "|"? formula-case ("|" formula-case)* "}"
\
reads ::= "reads" "{" term ( "," term )* "}"
\
writes ::= "writes" "{" term ( "," term )* "}"
\
raises ::= "raises" "{" "|"? raises-case ("|" raises-case)* "}" ;
| "raises" "{" uqualid ("," uqualid)* "}"
\
raises-case ::= uqualid pattern? "->" formula
\
variant ::= "variant" "{" one-variant ("," one-variant)+ "}"
\
one-variant ::= term ("with" variant-rel)?
\
variant-rel ::= lqualid
\
invariant ::= "invariant" "{" formula "}" ;
\
assertion ::= ("assert" | "assume" | "check") "{" formula "}" ;
| "absurd"
\
\end{syntax}
......@@ -170,13 +170,14 @@ A \why input file is a (possibly empty) list of theories.
\clearpage
\section{WhyML Language}\label{sec:syntax:whyml}
\subsection{Types}
\subsection{Specification}
The syntax for program types is given in Figure~\ref{fig:bnf:typev}.
The syntax for specification clauses in programs
is given in Figure~\ref{fig:bnf:spec}.
\begin{figure}
\begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
\caption{Syntax for program types.}
\label{fig:bnf:typev}
\begin{center}\framebox{\input{./spec_bnf.tex}}\end{center}
\caption{Specification clauses in programs.}
\label{fig:bnf:spec}
\end{figure}
\subsection{Expressions}
......
......@@ -15,16 +15,14 @@
| "match" term ("," term)* "with" ;
("|" term-case)+ "end" ; pattern matching
| "(" term ("," term)+ ")" ; tuple
| "{" field-value+ "}" ; record
| "{" term-field+ "}" ; record
| term "." lqualid ; field access
| "{" term "with" field-value+ "}" ; field update
| "{" term "with" term-field+ "}" ; field update
| term ":" type ; cast
| label term ; label
| "'" uident ; code mark
| "(" term ")" ; parentheses
\
term-case ::= pattern "->" term ;
\
pattern ::= pattern "|" pattern ; or pattern
| pattern "," pattern ; tuple
| "_" ; catch-all
......@@ -33,5 +31,7 @@
| "(" pattern ")" ; parentheses
| pattern "as" lident ; binding
\
field-value ::= lqualid "=" term ";"
term-case ::= pattern "->" term ;
\
term-field ::= lqualid "=" term ";"
\end{syntax}
......@@ -10,9 +10,9 @@
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
| "goal" ident ":" formula ;
| "use" imp-exp tqualid ("as" uident-opt)? ;
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "namespace" "import"? uident-opt decl* "end" ;
| "use" imp-exp tqualid ("as" uident)? ;
| "clone" imp-exp tqualid ("as" uident)? subst? ;
| "namespace" "import"? uident decl* "end" ;
\
logic-decl ::= function-decl ;
| predicate-decl
......@@ -33,8 +33,6 @@
\
imp-exp ::= ("import" | "export")?
\
uident-opt ::= uident | "_"
\
subst ::= "with" ("," subst-elt)+
\
subst-elt ::= "type" lqualid "=" lqualid ;
......
\begin{syntax}
type-v ::= type
| "(" type-v ")" ; parentheses
| type-v "->" type-c ;
| type-v-binder "->" type-c
\
type-v-binder ::= lident label* ":" type-v
\
type-v-param ::= "(" type-v-binder ")"
\
type-c ::= type-v ;
| pre type-v effect post
\
effect ::= reads? writes? raises?
\
reads ::= "reads" tr-term+
\
writes ::= "writes" tr-term+
\
raises ::= "raises" uqualid+
\
pre ::= annotation
\
post ::= annotation post-exn*
\
post-exn ::= "|" uqualid "->" annotation
\
annotation ::= "{}" | "{" formula "}"
\
\end{syntax}
\ No newline at end of file
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