doc: syntax of formulas

Makefile.in

@@ -749,7 +749,8 @@ clean::
 DOC = doc/manual.pdf
 # doc/manual.html
 
-BNF=doc/term_bnf.tex
+BNF = qualid term formula
+BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
 
 doc/%_bnf.tex: doc/%.bnf doc/bnf
 	doc/bnf $< > $@
@@ -762,7 +763,7 @@ doc: $(DOC)
 
 .PHONY:$(DOC)
 
-doc/manual.pdf: $(BNF) doc/apidoc.tex doc/manual.tex doc/version.tex
+doc/manual.pdf: $(BNFTEX) doc/apidoc.tex doc/manual.tex doc/version.tex
 	cd doc; rubber -d manual.tex
 
 # doc/manual.html: doc/manual.tex doc/version.tex

doc/formula.bnf

+\begin{syntax}
+  formula ::= "true" | "false" ;
+       | formula "->"  formula ; implication
+       | formula "<->" formula ; equivalence
+       | formula "and" formula ; conjunction
+       | formula "/\"  formula ; asymmetric conjunction
+       | formula "or"  formula ; disjunction
+       | formula "\/"  formula ; asymmetric disjunction
+       | "not" formula         ; negation
+       | lqualid 	       ; symbol
+       | prefix-op term        ;
+       | term infix-op term    ;
+       | lqualid term+         ; predicate application
+       | "if" formula "then" formula ;
+         "else" formula        ; conditional
+       | "let" pattern "=" term "in" formula ; local binding
+       | "match" ("," term)+ "with" ;
+         "|"? ("|" formula-case)+ "end" ; pattern matching
+       | quantifier ("," binders )+ ;
+         triggers "." formula  ; quantifier
+       | label formula ; label
+       | "(" formula ")" ; parentheses
+       \
+   quantifier ::= "forall" | "exists"
+       \
+   binders ::= lident+ ":" type
+       \
+   formula-case ::= pattern "->" formula ; %
+\end{syntax}

doc/qualid.bnf

+\begin{syntax}
+  lalpha ::= "a"-"z" | "_"
+  \
+  ualpha ::= "A"-"Z"
+  \
+  lident ::= lalpha (alpha | digit | "'")*
+  \
+  uident ::= ualpha (alpha | digit | "'")*
+  \
+  lqualid ::= lident | uqualid "." lident ;
+  \
+  uqualid ::= uident | uqualid "." uident ;%
+\end{syntax}

doc/syntaxref.tex

 \chapter{Syntax Reference}
 \label{chap:syntaxref}
 
-This chapter gives the grammar for the input files
+This chapter gives the grammar for the input files.
 
-\framebox{\input{./term_bnf.tex}}
+TODO: constants
+
+\paragraph{Identifiers.} 
+\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}
+
+\paragraph{Terms.}
+The syntax of terms is given Figure~\ref{fig:bnf:term}.
+
+TODO: prefix and infix operators
+
+\begin{figure}
+  \begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
+  \caption{Syntax of terms.}
+\label{fig:bnf:term}
+\end{figure}
+
+\paragraph{Formulas.}
+The syntax of terms is given Figure~\ref{fig:bnf:formula}.
+
+\begin{figure}
+  \begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
+  \caption{Syntax of formulas.}
+\label{fig:bnf:formula}
+\end{figure}
 
 %%% Local Variables:
 %%% mode: latex

doc/term.bnf

 \begin{syntax}
-  term ::= integer ; integer constant
-       | real ; real constant
-       | qualid ; symbol
-       | prefix-op term ;
-       | term infix-op term ;
-       | lqualid term+ ; function application
-       | "if" formula "then" term "else" term ; conditional
-       | "let" pattern "=" term "in" term ; local binding
-       | "match" ("," term)+ "with" "|"? match-cases "end" ;
+  term ::= integer                ; integer constant
+       | real 			  ; real constant
+       | lqualid 		  ; symbol
+       | prefix-op term 	  ;
+       | term infix-op term 	  ;
+       | lqualid term+ 		  ; function application
+       | "if" formula "then" term ;
+         "else" term              ; conditional
+       | "let" pattern "=" term "in" term 
+                                  ; local binding
+       | "match" ("," term)+ "with" ;
+         "|"? ("|" term-case)+ "end" ; pattern matching
        | "(" term ("," term)* ")" ; tuple
-       | term ":" type ; cast
-       | label term ; label
-       | "(" term ")" ; parentheses%
-\end{syntax}
+       | term ":" type 	          ; cast
+       | label term 	      	  ; label
+       | "(" term ")" 	      	  ; parentheses
+  \
+  term-case ::= pattern "->" term ; 
+  \
+  pattern ::= pattern "|" pattern ; or pattern
+            | pattern "," pattern ; tuple 
+	    | "_"                 ; catch-all
+	    | lident              ; variable
+	    | uident pattern*     ; constructor
+	    | "(" pattern ")" 	  ; parentheses
+	    | pattern "as" lident ; binding %
+\end{syntax}
\ No newline at end of file

tests/test-jcf.why

@@ -6,7 +6,8 @@ theory List
 
   use import bool.Bool
 
-  logic x : int = if true then 1 else 3
+  logic x : int = match 1,2 with X u,y -> 3 end
+
 
 end