programs documentation (a quick start)

Makefile.in

@@ -989,7 +989,8 @@ ifeq (@enable_doc@,yes)
 doc: doc/manual.pdf
 # doc/manual.html
 
-BNF = qualid constant operator term type formula theory
+BNF = qualid constant operator term type formula theory why_file  \
+      typev expr module whyml_file
 BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
 
 doc/%_bnf.tex: doc/%.bnf doc/bnf

doc/expr.bnf

+\begin{syntax}
+  expr ::= integer                                ; integer constant
+       | real 			                  ; real constant
+       | lqualid 		                  ; symbol
+       | prefix-op expr 	                  ;
+       | expr infix-op expr 	                  ;
+       | expr "[" expr "]"                        ; brackets
+       | 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
+       | "if" expr "then" expr ("else" expr)?     ; conditional
+       | expr ";" expr                            ; sequence
+       | "label" uident ":" expr                  ; label
+       | "loop" loop-annot "end"                  ; infinite loop
+       | "while" expr "do" loop-annot expr "done" ; while loop
+       | "for" lident "=" expr to-downto expr     ; for loop
+         "do" loop-inv expr "done"                ;
+       | assert annotation                        ; assertion
+       | "absurd"                                 ;
+       | "raise" uqualid                          ; exception raising
+       | "raise" "(" uqualid expr ")"             ;
+       | "try" expr "with" ("|" handler)+ "end"   ; exception catching
+       | "any" type-c                             ; 
+       | "let" pattern "=" expr "in" expr         ; local binding
+       | "match" expr ("," expr)* "with"          ; pattern matching
+         ("|" expr-case)+ "end"                   ;
+       | "(" expr ("," expr)+ ")"                 ; tuple
+       | "{|" field-value+ "|}"                   ; record
+       | exopr "." lqualid                        ; field access
+       | expr "." lqualid "<-" expr               ; field assignment
+       | "{|" expr "with" field-value+ "|}"       ; field update
+       | expr ":" type 	                          ; cast
+       | "(" expr ")" 	      	                  ; parentheses
+  \
+  expr-case ::= pattern "->" expr                 ;
+  \
+  field-value ::= lqualid "=" expr                ;
+  \
+  triple ::= expr                                 ;
+    | pre expr post                               ; Hoare triple
+  \
+  assert ::= "assert" | "assume" | "check"
+  \
+  to-downto ::= "to" | "downto"
+  \
+  loop-annot ::= loop-inv? variant?
+  \
+  loop-inv ::= "invariant" annotation
+  \
+  variant ::= "variant" "{" term "}" ("with" lqualid)?
+\end{syntax}
\ No newline at end of file

doc/macros.tex

 
 
 \newcommand{\why}{\textsf{Why3}}
+\newcommand{\whyml}{\textsf{Why3ML}}
 \newcommand{\eg}{\emph{e.g.}}
 
 % BNF grammar

doc/manpages.tex

@@ -137,7 +137,7 @@ provers and to replace them in the configuration file. The option
 \label{sec:why3ref}
 
 \why\ is primarily used to call provers on goals contained in an
-input file. By default, such a file must be written in \why language
+input file. By default, such a file must be written in \why\ language
 and have the extension \texttt{.why}. However, a dynamically loaded
 plugin can register a parser for some other format of logical problems,
 \eg{} TPTP or SMTlib.
@@ -295,16 +295,20 @@ The preferences window allows you customize
 
 \section{The \texttt{why3ml} tool}
 
-The \texttt{why3ml} is an additional layer on \why\ library for
-generating verification conditions from WhyML programs. This tool and
-the syntax of WhyML programs is intentionally left undocumented since
-it might evolve significantly in the near future.
-
-For those who want to experiment with it, examples are provided in
-\texttt{examples/\ programs}. The files \texttt{*.mlw} can be loaded in
-the GUI.
-
-[TO BE COMPLETED LATER]
+\texttt{why3ml} is an additional layer on \why\ library for
+generating verification conditions from \whyml\ programs.
+The command-line of \texttt{why3ml} is identical to that of
+\texttt{why3}, but also accepts files with extension \texttt{.mlw} as
+input files containing \whyml\ modules (see chapter~\ref{chap:whyml}
+and section~\ref{sec:syntax:whyml}). Modules are turned into
+theories containing verification conditions as goals, and then
+\texttt{why3ml} behaves exactly as \texttt{why3} for the remaining of
+the process.
+Note that files with extension \texttt{.mlw} can also be loaded in
+\texttt{why3ide}.
+
+For those who want to experiment with \whyml, many examples are provided in
+\texttt{examples/programs}.
 
 \section{The \texttt{why3bench} tool}
 

doc/manual.tex

@@ -202,7 +202,7 @@ are the following.
 
 % \input{ide.tex}
 
-% \input{whyml.tex}
+\input{whyml.tex}
 
 \input{api.tex}
 

doc/module.bnf

+\begin{syntax}
+  module ::= "module" uident label* mdecl* "end"
+  \
+  mdecl ::= decl                                ; theory declaration
+    | "type" mtype-decl ("with" mtype-decl)*    ; mutable types
+    | "let" lident label* pgm-defn              ;
+    | "let" "rec" recfun ("with" recfun)*  ;
+    | "parameter" lident label* pgm-decl        ;
+    | "exception" lident label* type?           ;
+    | "use" imp-exp "module" tqualid ("as" uident-opt)?     ;
+    | "namespace" "import"? uident-opt 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 (";" mrecord-field)* "|}" ; record type
+  \
+  mrecord-field ::= "mutable"? lident label* ":" type
+  \
+  pgm-decl ::= ":" type-v    ;
+    | type-v-param+ ":" type-c    ;
+  \
+  pgm-defn ::= type-v-param+ (":" type)? "=" triple ;
+    | "=" "fun" type-v-param+ "->" triple ;
+\end{syntax}

doc/syntaxref.tex

 \chapter{Syntax Reference}
 \label{chap:syntaxref}
 
-This chapter gives the grammar for \why\ input files.
+This chapter gives the grammar for \why\ and \whyml\ input files.
+
+\section{Lexical conventions}
+
+Lexical conventions are common to \why\ and \whyml.
 
 % TODO: blanks
 
@@ -49,6 +53,9 @@ characters they are built from:
 \item level 1: all other operators (non-terminal \textit{infix-op-1}).
 \end{itemize}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Why3 Language}
+
 \paragraph{Terms.}
 The syntax for terms is given in Figure~\ref{fig:bnf:term}.
 The various constructs have the following priorities and
@@ -134,6 +141,43 @@ The syntax for theories is given Figure~\ref{fig:bnf:theory}.
 \label{fig:bnf:theory}
 \end{figure}
 
+\paragraph{Files.}
+A \why\ input file is a (possibly empty) list of theories.
+\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Why3ML Language}\label{sec:syntax:whyml}
+
+\paragraph{Types.}
+The syntax for program types is given in figure~\ref{fig:bnf:typev}.
+\begin{figure}[p]
+  \begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
+  \caption{Syntax for program types.}
+\label{fig:bnf:typev}
+\end{figure}
+
+\paragraph{Expressions.}
+The syntax for program expressions is given in figure~\ref{fig:bnf:expr}.
+\begin{figure}[p]
+  \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
+  \caption{Syntax for program expressions.}
+\label{fig:bnf:expr}
+\end{figure}
+
+\paragraph{Modules.}
+The syntax for modules is given in figure~\ref{fig:bnf:module}.
+\begin{figure}[p]
+  \begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
+  \caption{Syntax for modules.}
+\label{fig:bnf:module}
+\end{figure}
+
+\paragraph{Files.}
+A \whyml\ input file is a (possibly empty) list of theories and modules.
+\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-PDF-mode: t

doc/term.bnf

@@ -15,6 +15,9 @@
        | "match" term ("," term)* "with" ;
          ("|" term-case)+ "end"          ; pattern matching
        | "(" term ("," term)+ ")" ; tuple
+       | "{|" field-value+ "|}"   ; record 
+       | term "." lqualid         ; field access
+       | "{|" term "with" field-value+ "|}"    ; field update
        | term ":" type 	          ; cast
        | label term 	      	  ; label
        | "(" term ")" 	      	  ; parentheses
@@ -27,5 +30,7 @@
 	    | lident              ; variable
 	    | uident pattern*     ; constructor
 	    | "(" pattern ")" 	  ; parentheses
-	    | pattern "as" lident ; binding %
+	    | pattern "as" lident ; binding
+  \
+  field-value ::= lqualid "=" term
 \end{syntax}
\ No newline at end of file

doc/typev.bnf

+\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

doc/why_file.bnf

+\begin{syntax}
+  file ::= theory*
+\end{syntax}

doc/whyml.tex

-\chapter{Why ML and Verification Condition Generator}
+\chapter{The Why3ML Programming Language}
 \label{chap:whyml}
 
+This chapter describes the \whyml\ programming language.
 
+% simple message = all Why3 language + mutable record fields + model
+
+% files .mlw
+% command line
+% tutorial with an example (same fringe)
 
 %%% Local Variables:
 %%% mode: latex

doc/whyml_file.bnf

+\begin{syntax}
+  file ::= (theory | module)*
+\end{syntax}

src/core/term.mli

@@ -332,10 +332,10 @@ module TermTF : sig
   (** [t_selecti fnT fnF acc t] is [t_select (fnT acc) (fnF acc) t] *)
 
   val t_map : (term -> term) -> (term -> term) -> term -> term
-  (** [t_map fnT fnF = t_map (t_select fnT fnF) *)
+  (** [t_map fnT fnF = t_map (t_select fnT fnF)] *)
 
   val t_fold : ('a -> term -> 'a) -> ('a -> term -> 'a) -> 'a -> term -> 'a
-  (** [t_fold fnT fnF = t_fold (t_selecti fnT fnF) *)
+  (** [t_fold fnT fnF = t_fold (t_selecti fnT fnF)] *)
 
   val t_map_fold : ('a -> term -> 'a * term) ->
     ('a -> term -> 'a * term) -> 'a -> term -> 'a * term