doc: lexical conventions, types and terms (1/3)

Makefile.in

@@ -1857,7 +1857,8 @@ ifeq (@enable_doc@,yes)
 
 doc: doc/manual.pdf doc/html/index.html
 
-BNF = ident qualid tag constant operator term type formula theory theory2 \
+BNF = ident qualid attribute constant operator type term1 term2 term3 \
+	theory theory2 \
 	why_file spec expr expr2 module whyml_file term_old_at
 BNFTEX = $(BNF:%=doc/%_bnf.tex)
 

bench/ce/jlamp0.mlw

@@ -8,9 +8,10 @@ module M
   let p1 (b : ref int)
     requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 }
     ensures  { 17 <= !a <= 42 }
-  = a := !a + !b;
-    assert { 5 <= !a <= 15 };
-    if !a >= 10 then a := !a - 1
+  =
+    a.contents <- !a + !b;
+    (*assert { 5 <= !a <= 15 };*)
+    (*if !a >= 10 then a.contents <- !a - 1*) ()
 
   val c : ref int
 

doc/attribute.bnf

+\begin{syntax}
+  attribute ::= "[@" ~... "]" ; attribute
+        | "[#" string digit+ digit+ digit+ "]" ; location %
+\end{syntax}

doc/operator.bnf

@@ -13,16 +13,14 @@
   \
   op-char-34 ::= op-char-3 | op-char-4 ;
   \
-  infix-op-1 ::= op-char-234* op-char-1 op-char-1234* ;
+  infix-op-1 ::= op-char-1234* op-char-1 op-char-1234* ;
   \
-  infix-op-2 ::= op-char-34* op-char-2 op-char-234* ;
+  infix-op-2 ::= op-char-234* op-char-2 op-char-234* ;
   \
-  infix-op-3 ::= op-char-4* op-char-3 op-char-34* ;
+  infix-op-3 ::= op-char-34* op-char-3 op-char-34* ;
   \
   infix-op-4 ::= op-char-4+ ;
   \
-  infix-op ::= infix-op-1 | infix-op-2 | infix-op-3 | infix-op-4 ;
-  \
   prefix-op ::= op-char-1234+ ;
   \
   bang-op ::= ("!" | "?") op-char-4* ; %

doc/qualid.bnf

 \begin{syntax}
-  lident-ext ::= lident | "(" op-char-1234+ ")"
+  lqualid ::= (uident ".")* lident
+  \
+  uqualid ::= (uident ".")* uident
   \
   qualid ::= (uident ".")* (lident-ext | uident)
   \
-  lqualid ::= (uident ".")* lident
+  lident-ext ::= lident | "(" lident-op ")"
   \
-  uqualid ::= (uident ".")* uident %
+  lident-op ::= op-char-1234+     ;   infix or bang operator
+              | op-char-1234+ "_" ;   prefix (non-bang) operator
+              | "[]"              ;   collection access
+              | "[<-]"            ;   collection update
+              | "[]<-"            ;   in-place collection update
+              | "[_.._]"          ;   collection slice
+              | "[_..]"           ;   right-open slice
+              | "[.._]"           ;   left-open slice %
 \end{syntax}

doc/syntaxref.tex

@@ -5,6 +5,7 @@
 In this chapter, we describe the syntax and semantics of \whyml.
 
 \section{Lexical Conventions}
+\label{sec:lexer}
 
 %Lexical conventions of \whyml are similar to those of OCaml.
 %
@@ -15,7 +16,7 @@ Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
 Note that \texttt{(*)} does not start a comment.
 
 Strings are enclosed in double quotes (\verb!"!). Double quotes can be
-escaped in strings using the backslash character (\verb!\!).
+escaped inside strings using the backslash character (\verb!\!).
 The other special sequences are \verb!\n! for line feed and \verb!\t!
 for horizontal tab.
 In the following, strings are referred to with the non-terminal
@@ -68,28 +69,157 @@ would have a higher precedence than the infix operator \texttt{->-}
 The so-called ``bang operators'' are prefix operators that have even
 higher precedence than the juxtaposition (application) operator,
 allowing us to write expressions like \texttt{inv !x}.
-Infix operators from the groups 2-4 are left-associative.
-Infix operators from the group 1 are non-associative and
-may instead be chained, as explained below.
-
-An operator inside parenthesis can act as a lowercase identifier.
-Qualified identifiers are prefixed with a sequence of uppercase
-identifiers, e.g., \texttt{App.S.get}:
+An operator from \textsl{infix-op-4} or \textsl{prefix-op}
+cannot start with \texttt{!} or \texttt{?}: such operators
+are always recognized as bang operators.
+%Infix operators from groups 2-4 are left-associative.
+%Infix operators from group 1 are non-associative and
+%may instead be chained, as explained in Section~\ref{sec:terms}.
+
+%An operator inside parenthesis can act as a lowercase identifier.
+%Qualified identifiers are prefixed with a sequence of uppercase
+%identifiers, e.g., \texttt{App.S.get}:
 %\begin{figure}[ht]
-\begin{center}\input{./qualid_bnf.tex}\end{center}
+%\begin{center}\input{./qualid_bnf.tex}\end{center}
 %\caption{Syntax for qualified identifiers.}
 %\label{fig:bnf:qualid}
 %\end{figure}
 
 Finally, any identifier, term, formula, or expression
-in a \whyml program can be tagged, either with a generic tag
-or a location tag:
-\begin{center}\input{./tag_bnf.tex}\end{center}
-A generic tag cannot contain newlines or closing square brackets;
+in a \whyml source can be tagged either with a string
+\textit{attribute} or a location:
+\begin{center}\input{./attribute_bnf.tex}\end{center}
+An attribute cannot contain newlines or closing square brackets;
 leading and trailing spaces are ignored.
-A location tag consists of a file name in double quotes,
+A location consists of a file name in double quotes,
 a line number, and starting and ending character positions.
 
+\section{Type expressions}
+\label{sec:types}
+
+\whyml features an ML-style type system with polymorphic types,
+variants (sum types), and records that can have mutable fields.
+The syntax for type expressions is the following:
+\begin{center}\input{./type_bnf.tex}\end{center}
+Built-in types are \texttt{int} (arbitrary precision integers),
+\texttt{real} (real numbers), \texttt{bool}, the arrow type
+(also called the \textit{mapping type}, right-associative),
+and the tuple types.
+The empty tuple type is also called the \textit{unit type}
+and can be written as \texttt{unit}.
+
+Note that the syntax for type expressions notably differs from
+the usual ML syntax. In particular, the type of polymorphic lists
+is written \texttt{list 'a}, and not \texttt{'a list}.
+
+\textit{Snapshot types} are specific to \whyml, they denote
+the types of ghost values produced by pure logical functions in
+\whyml programs. A snapshot of an immutable type is the type
+itself: thus, \texttt{\{int\}} is the same as \texttt{int} and
+\texttt{\{list 'a\}} is the same as \texttt{list 'a}.
+A snapshot of a mutable type, however, represents a snapshot
+value which cannot be modified anymore. Thus, a snapshot array
+\texttt{a} of type \texttt{\{array int\}} can be read from
+(\texttt{a[42]} is accepted) but not written into
+(\texttt{a[42] <- 0} is rejected). Generally speaking,
+a program function that expects an argument of a mutable type
+will accept an argument of the corresponding snapshot type
+as long as it is not modified by the function.
+
+\section{Logical expressions: terms and formulas}
+\label{sec:types}
+
+A significant part of a typical \whyml source file is occupied
+by non-executable logical content intended for specification
+and proof: function contracts, assertions, definitions of
+logical functions and predicates, axioms, lemmas, etc.
+
+Logical expressions are called \textit{terms}. Boolean
+terms are called \textit{formulas}. Internally, \why distinguishes
+the proper formulas (produced by predicate symbols, propositional
+connectives and quantifiers) and the terms of type \texttt{bool}
+(produced by Boolean variables and logical functions that return
+\texttt{bool}). However, this distinction is not enforced on the
+syntactical level, and \why will perform the necessary conversions
+behind the scenes.
+
+\begin{figure}[ht]
+\begin{center}\input{./term1_bnf.tex}\end{center}
+\caption{\whyml terms (part I).}
+\label{fig:bnf:term1}
+\end{figure}
+
+\begin{figure}[ht]
+\begin{center}\input{./term2_bnf.tex}\end{center}
+\caption{\whyml terms (part II).}
+\label{fig:bnf:term2}
+\end{figure}
+
+\begin{figure}[ht]
+\begin{center}\input{./term3_bnf.tex}\end{center}
+\caption{\whyml terms (part III).}
+\label{fig:bnf:term3}
+\end{figure}
+
+The syntax of \whyml terms is given in
+Figures~\ref{fig:bnf:term1}-\ref{fig:bnf:term3}.
+The constructions are listed in the order of
+decreasing precedence.
+For example, as was mentioned in the previous section,
+bang operators have the highest precedence of all operators,
+so that \texttt{-p.x} is parsed as the negation of the
+record field \texttt{p.x}, whereas \texttt{!p.x} is
+parsed as the field \texttt{x} of a record stored
+in the reference \texttt{p}.
+
+An operator inside parentheses can act as an identifier
+referring to that operator, for example, in a definition.
+To distinguish between prefix and infix operators, an
+underscore symbol is appended at the end: for example,
+\texttt{(-)} refers to the binary subtraction and
+\texttt{(-\_)} to the unary negation.
+Bang operators cannot be used as infix operators,
+and thus do not require disambiguation.
+
+In addition to prefix and infix operators, \whyml
+supports several mixfix bracket operators to
+manipulate various collection types: dictionaries,
+arrays, sequences, etc. Bracket operators do not have
+any predefined meaning and may be used to denote access
+and update operations for various user-defined collection types.
+Notice that the in-place update operator (\texttt{a[i] <- v})
+cannot be used inside logical terms: all effectful operations
+are restricted to program expressions. To represent the result
+of a collection update, we should use a pure logical update
+operator (\texttt{a[i <- v]}) instead.
+
+The \texttt{at} and \texttt{old} operators are used inside
+post-conditions and assertions to refer to the value of
+a mutable program variable at some past moment of execution
+(see the next section for details).
+These operators have higher precedence than the infix
+operators from group 1 (\textsl{infix-op-1}): \texttt{old i > j}
+is parsed as \texttt{(old i) > j} and not as \texttt{old (i > j)}.
+
+Infix operators from groups 2-4 are left-associative.
+Infix operators from group 1 are non-associative and
+can be chained. For example, the term \texttt{0 <= i < j < length a}
+is parsed as the conjunction of three inequalities \texttt{0 <= i},
+\texttt{i < j}, and \texttt{j < length a}.
+
+In order to refer to symbols introduced in different namespaces
+(\textit{scopes}), we can put a dot-separated
+``qualifier prefix'' in front of an identifier
+(e.g.~\texttt{Map.S.get m i}) or a term in parentheses
+(e.g.~\texttt{Map.S.(m[i])}, though parentheses can be omitted
+if the term is a record or a record update). This notation allows
+us to use the symbol \texttt{get} or the collection access operator
+\texttt{([])} from the scope \texttt{Map.S} without importing
+them in the current namespace.
+
+
+\newpage
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \section{The \why Language}
@@ -122,22 +252,6 @@ associativities, from lowest to greatest priority:
 Note the curryfied syntax for function application, though partial
 application is not allowed (rejected at typing).
 
-\begin{figure}
-  \begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
-  \caption{Syntax for terms.}
-\label{fig:bnf:term}
-\end{figure}
-
-\subsection{Type Expressions}
-
-The syntax for type expressions is the following:
-\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
-Built-in types are \texttt{int}, \texttt{real}, and tuple types.
-Note that the syntax for type
-expressions notably differs from the usual ML syntax (\eg the
-type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
-
-
 \subsection{Formulas}
 
 The syntax for formulas is given Figure~\ref{fig:bnf:formula}.

doc/tag.bnf

-\begin{syntax}
-  tag ::= "[@" ~... "]" ; generic tag
-        | "[#" string digit+ digit+ digit+ "]" ; location tag %
-\end{syntax}

doc/term.bnf

-\begin{syntax}
-  term ::= integer                ; integer constant
-       | real 			  ; real constant
-       | lqualid 		  ; symbol
-       | prefix-op term 	  ;
-       | bang-op term 	  ;
-       | term infix-op term 	  ;
-       | term "[" term "]"	  ; brackets
-       | term "[" term "<-" term "]" 	  ; ternary brackets
-       | lqualid term+ 		  ; function application
-       | "if" formula "then" term ;
-         "else" term              ; conditional
-       | "let" pattern "=" term "in" term
-                                  ; local binding
-       | "match" term ("," term)* "with" ;
-         ("|" term-case)+ "end"          ; pattern matching
-       | "(" term ("," term)+ ")" ; tuple
-       | "{" term-field+ "}"     ; record
-       | term "." lqualid         ; field access
-       | "{" term "with" term-field+ "}"      ; field update
-       | term ":" type 	          ; cast
-       | label term 	      	  ; label
-       | "'" uident    	      	  ; code mark
-       | "(" term ")" 	      	  ; parentheses
-  \
-  pattern ::= pattern "|" pattern ; or pattern
-            | pattern "," pattern ; tuple
-	    | "_"                 ; catch-all
-	    | lident              ; variable
-	    | uident pattern*     ; constructor
-	    | "(" pattern ")" 	  ; parentheses
-	    | pattern "as" lident ; binding
-  \
-  term-case ::= pattern "->" term ;
-  \
-  term-field ::= lqualid "=" term ";"
-\end{syntax}

doc/term1.bnf

+\begin{syntax}
+  term ::= integer            ; integer constant
+    | real                    ; real constant
+    | "true" | "false"        ; Boolean constant
+    | "()"                    ; empty tuple
+    | qualifier "(" term ")"        ; qualified term
+    | qualifier "begin" term "end"  ; \textit{idem}
+    | qualid                  ; qualified identifier
+    | bang-op term            ; bang operator
+    | "{" term-field+ "}"     ; record
+    | "{" term "with" term-field+ "}"
+                              ; record update
+    | term "." lqualid        ; record field access
+    | term "[" term "]"       ; collection access
+    | term "[" term "<-" term "]"  ; collection update
+    | term "[" term ".." term "]"  ; collection slice
+    | term "[" term ".." "]"  ; right-open slice
+    | term "[" ".." term "]"  ; left-open slice
+    | term term+              ; application
+    | prefix-op term          ; prefix operator
+    | term infix-op-4 term    ; infix operator 4
+    | term infix-op-3 term    ; infix operator 3
+    | term infix-op-2 term    ; infix operator 2
+    | term "at" uident        ; past value
+    | "old" term              ; initial value
+    | term infix-op-1 term    ; infix operator 1
+    | ...                     ; continued in Fig.~\ref{fig:bnf:term2}
+  \
+  term-field ::= lqualid "=" term ";" ; field \texttt{=} value
+  \
+  lqualid ::= qualifier lident    ; qualified \textsl{lident}
+  \
+  uqualid ::= qualifier uident    ; qualified \textsl{uident}
+  \
+  qualid ::= qualifier (lident-ext | uident)  ; qualified identifier
+  \
+  qualifier ::= (uident ".")*       ; qualifier prefix
+  \
+  lident-ext ::= lident             ; lowercase identifier
+               | "(" ident-op ")"   ; operator identifier
+  \
+  ident-op ::=  op-char-1234+     ;   infix or bang operator
+              | op-char-1234+ "_" ;   prefix or bang operator
+              | "[]"              ;   collection access
+              | "[<-]"            ;   collection update
+              | "[]<-"            ;   in-place update
+              | "[_.._]"          ;   collection slice
+              | "[_..]"           ;   right-open slice
+              | "[.._]"           ;   left-open slice %
+\end{syntax}

doc/term2.bnf

+\begin{syntax}
+  term ::= ...                ; see Fig.~\ref{fig:bnf:term1}
+    | "not" term              ; negation
+    | term "/\" term          ; conjunction
+    | term "&&" term          ; asymmetric conjunction
+    | term "\/" term          ; disjunction
+    | term "||" term          ; asymmetric disjunction
+    | term "by" term          ; proof indication
+    | term "so" term          ; consequence indication
+    | term "->" term          ; implication
+    | term "<->" term         ; equivalence
+    | term ":" type           ; type cast
+    | attribute term          ; attribute
+    | term ("," term)+        ; tuple
+    | quantifier quant-vars triggers? "." term ; quantifier
+    | ...                     ; continued in Fig.~\ref{fig:bnf:term3}
+  \
+  quantifier ::= "forall" | "exists"
+  \
+  quant-vars ::= quant-cast ("," quant-cast)*
+  \
+  quant-cast ::= lident+ (":" type)?
+  \
+  triggers ::= "[" trigger ("|" trigger)* "]" ;
+  \
+  trigger ::= term ("," term)*  ; %
+\end{syntax}

doc/term3.bnf

+\begin{syntax}
+  term ::= ...                ; see Fig.~\ref{fig:bnf:term1} and \ref{fig:bnf:term2}
+    | "if" term "then" term "else" term
+                              ; conditional
+    | "fun" binders "->" term ; mapping
+    | "let" term-let "in" term  ; local binding
+    | "match" term "with" term-case+ "end"  ; pattern matching
+  \
+  binders ::= ~... ;
+  \
+  term-let ::= pattern "=" term ;
+    | ~...
+  \
+  term-case ::= "|" pattern "->" term
+  \
+  pattern ::= "_"           ; catch-all
+    | "()"                  ; empty tuple
+    | "(" pattern ")"       ; parentheses
+    | "{" pat-field+ "}"    ; record
+    | "ghost"? tag? lident  ; variable
+    | uident pattern*       ; constructor
+    | pattern "," pattern   ; tuple
+    | pattern "as" lident   ; binding
+    | pattern "|" pattern   ; ``or'' pattern
+  \
+  pat-field ::= lqualid "=" pattern ";"
+\end{syntax}

doc/type.bnf

 \begin{syntax}
   type ::= lqualid type*     ; type symbol
        | "'" lident          ; type variable
-       | "()"		     ; empty tuple type
+       | type "->" type      ; mapping type
+       | "()"		     ; unit type
        | "(" type ("," type)+ ")" ; tuple type
+       | "{" type "}"        ; snapshot type
        | "(" type ")"        ; parentheses %
-\end{syntax}
\ No newline at end of file
+\end{syntax}

src/parser/parser.mly

@@ -1179,7 +1179,7 @@ lident_op:
 | MINUS     UNDERSCORE    { Ident.prefix "-" }
 | EQUAL                   { Ident.infix "=" }
 | MINUS                   { Ident.infix "-" }
-| OPPREF                  { Ident.prefix $1 }
+| OPPREF UNDERSCORE?      { Ident.prefix $1 }
 | LEFTSQ RIGHTSQ          { Ident.mixfix "[]" }
 | LEFTSQ LARROW RIGHTSQ   { Ident.mixfix "[<-]" }
 | LEFTSQ RIGHTSQ LARROW   { Ident.mixfix "[]<-" }