doc: tex from bnf

.gitignore

@@ -68,11 +68,18 @@ why.conf
 /doc/manual.ilg
 /doc/manual.idx
 /doc/manual.rel
+/doc/manual.glg
+/doc/manual.glo
+/doc/manual.gls
+/doc/manual.ist
 /doc/*.haux
 /doc/*.pdf
 /doc/manual.html
 /doc/*.hind
 /doc/*.htoc
+/doc/bnf
+/doc/bnf.ml
+/doc/*_bnf.tex
 
 # /share/
 /share/*.cm*
@@ -171,4 +178,6 @@ why.conf
 /examples/programs/my_cosine/*.gappa
 /examples/scottish-private-club/
 /examples/hello_proof/
- 
\ No newline at end of file
+/examples/einstein/
+/examples/programs/isqrt/
+/examples/programs/course/

Makefile.in

@@ -749,11 +749,20 @@ clean::
 DOC = doc/manual.pdf
 # doc/manual.html
 
+BNF=doc/term_bnf.tex
+
+doc/%_bnf.tex: doc/%.bnf doc/bnf
+	doc/bnf $< > $@
+
+doc/bnf: doc/bnf.mll
+	$(OCAMLLEX) $<
+	$(OCAMLOPT) -o $@ doc/bnf.ml
+
 doc: $(DOC)
 
 .PHONY:$(DOC)
 
-doc/manual.pdf: doc/apidoc.tex doc/manual.tex doc/version.tex
+doc/manual.pdf: $(BNF) 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/bnf.mll

+(* $Id: transf.mll,v 1.11 2009-03-03 09:53:08 uid562 Exp $ *)
+
+{ open Lexing;;
+  let idx = Buffer.create 5
+  let full_kw = Buffer.create 5
+
+  let modern = ref false
+
+  let escape_keyword s =
+    let buf = Buffer.create 5 in
+    String.iter
+      (function
+           c when ('A' <= c && c <= 'Z') ||
+                  ('a' <= c && c <= 'z') ||
+                  ('0' <= c && c <= '9')
+             -> Buffer.add_char buf c
+         | c -> Buffer.add_string buf
+             (Printf.sprintf "\\char%d" (int_of_char c))) s;
+    Buffer.contents buf
+
+  let make_keyword () =
+    let keyword = Buffer.contents full_kw in
+    let index = Buffer.contents idx in
+    print_string "\\addspace";
+    if !modern then
+      Printf.printf
+        "\\lstinline$%s$" keyword
+    else
+      Printf.printf "\\texttt{%s}" (escape_keyword keyword);
+    if index <> "" then
+      Printf.printf "\\indextt%s{%s}"
+        (if keyword.[0] = '\\' then "bs" else "") index;
+    print_string "\\spacetrue";
+    Buffer.clear idx;
+    Buffer.clear full_kw
+}
+
+rule main = parse
+    "\\begin{syntax}" {
+      print_string "\\begin{syntax}";
+      syntax lexbuf }
+  | "\\@" {
+      print_string "@";
+      main lexbuf }
+  | _ {
+      print_char (lexeme_char lexbuf 0); main lexbuf }
+  | eof {
+      () }
+
+and syntax = parse
+    "\\end{syntax}" {
+      print_string "\\end{syntax}";
+      main lexbuf }
+  | ";" ([^ '\n']* as s) '\n' [' ''\t']* '|' {
+      print_string "& \\textrm{";
+      print_string s;
+      print_string "} \\alt{}";
+      syntax lexbuf }
+  | ";" ([^ '\n']* as s) '\n' [' ''\t']* '\\' [' ''\t']* '\n' {
+      print_string "& \\textrm{";
+      print_string s;
+      print_string "} \\sep{}";
+      syntax lexbuf }
+  | ";" ([^ '\n']* as s) '\n' {
+      print_string "& \\textrm{";
+      print_string s;
+      print_string "} \\newl{}";
+      syntax lexbuf }
+  | "@" {
+      print_string "}";
+      main lexbuf }
+  | '\'' {
+      Buffer.clear idx;
+      Buffer.clear full_kw;
+      inquote lexbuf }
+  | '"' {
+      Buffer.clear idx;
+      Buffer.clear full_kw;
+      indoublequote lexbuf }
+  | "below" { print_string "\\below"; syntax lexbuf }
+  | "epsilon" { print_string "\\emptystring"; syntax lexbuf }
+  | ['A'-'Z''a'-'z''-'] + {
+      print_string "\\nonterm{";
+      print_string (lexeme lexbuf);
+      print_string"}";
+      check_nonterm_note lexbuf }
+  | '\\' ['a'-'z''A'-'Z'] + {
+      print_string (lexeme lexbuf);
+      syntax lexbuf }
+  | ['_' '^'] _ {
+      print_string (lexeme lexbuf);
+      syntax lexbuf }
+  | "*" { print_string "\\repetstar{}"; syntax lexbuf }
+  | "+" { print_string "\\repetplus{}"; syntax lexbuf }
+  | "?" { print_string "\\repetone{}"; syntax lexbuf }
+  | "(" { print_string "\\lparen{}"; syntax lexbuf }
+  | ")" { print_string "\\rparen{}"; syntax lexbuf }
+  | "::=" { print_string "\\is{}"; syntax lexbuf }
+  | "|" { print_string "\\orelse{}"; syntax lexbuf }
+  | "\\" { print_string "\\sep{}"; syntax lexbuf }
+  | "{" { print_string "\\begin{notimplementedenv}"; check_implementation_note lexbuf }
+  | "}" { print_string "\\end{notimplementedenv}"; syntax lexbuf }
+  | _ {
+      print_char (lexeme_char lexbuf 0);
+      syntax lexbuf }
+
+and inquote = parse
+    ['A'-'Z' 'a'-'z' '0'-'9' '?'] as c {
+      Buffer.add_char full_kw c;
+      Buffer.add_char idx c;
+      inquote lexbuf }
+  | '\'' {
+      make_keyword ();
+      syntax lexbuf }
+  | '_' {
+      Buffer.add_char full_kw '_';
+      Buffer.add_string idx "\\_";
+      inquote lexbuf
+    }
+  | _ as c {
+      Buffer.add_char full_kw c;
+      inquote lexbuf }
+
+and indoublequote = parse
+    ['A'-'Z' 'a'-'z' '0'-'9' '?'] as c {
+      Buffer.add_char full_kw c;
+      Buffer.add_char idx c;
+      indoublequote lexbuf }
+  | '"' {
+      make_keyword();
+      syntax lexbuf }
+  | '_' {
+      Buffer.add_char full_kw '_';
+      Buffer.add_string idx "\\_";
+      indoublequote lexbuf
+    }
+  | _ as c {
+      Buffer.add_char full_kw c;
+      indoublequote lexbuf }
+and check_implementation_note = parse
+  | "[" { print_string "["; implementation_note lexbuf }
+  | "" { syntax lexbuf }
+and implementation_note = parse
+    "]" { print_string "]"; syntax lexbuf }
+  | _  { print_char (lexeme_char lexbuf 0);
+           implementation_note lexbuf }
+and check_nonterm_note = parse
+  | "[" { print_string "{"; nonterm_note lexbuf }
+  | ""  { print_string "{}"; syntax lexbuf }
+and nonterm_note = parse
+    "]" { print_string "}"; syntax lexbuf }
+  | _  { print_char (lexeme_char lexbuf 0);
+           nonterm_note lexbuf }
+
+{
+
+  let () = Arg.parse
+    [ "-modern", Arg.Set modern, "set modern style"; ]
+    (fun f ->
+       let cin = open_in f in
+       let lb = from_channel cin in
+       main lb;
+       close_in cin)
+    "transf [-modern] file"
+
+}

doc/macros.tex

 
-\newtheorem{example}{Example}[chapter]
 
-% common Why title page
-
-\newcommand{\whytitlepage}[4]{%
-\begin{titlepage}
-\begin{center}
-~\vfill
-\rule\textwidth{0.1cm}\\[0.5cm]
-\begin{Huge}\sffamily
-#1 % title
-\end{Huge}
-\\[1cm]
-\begin{Large}\sffamily
-#2
-\end{Large}
-\\[0.1cm]
-\rule\textwidth{0.1cm}\\[1cm]
-Version #3\\[3cm]
-#4
-\vfill
-\today\\
-INRIA Team-Project \emph{Proval} \url{http://proval.lri.fr} \\
-INRIA Saclay - \^Ile-de-France \& LRI, CNRS UMR 8623\\ 
-4, rue Jacques Monod, 91893 Orsay cedex, France
-\end{center}
-\end{titlepage}}
-
-\newcommand{\why}{\textsf{Why}}
-\newcommand{\Why}{\why}
-\newcommand{\java}{\textsc{Java}\index{Java@\textsf{Java}}}
-\newcommand{\Java}{\java}
-\newcommand{\krakatoa}{\textsf{Krakatoa}\index{Krakatoa@\textsf{Krakatoa}}}
-\newcommand{\Krakatoa}{\krakatoa}
-\newcommand{\caduceus}{\textsf{Caduceus}\index{Caduceus@\textsf{Caduceus}}}
-\newcommand{\Caduceus}{\caduceus}
-\newcommand{\coq}{\textsf{Coq}\index{Coq@\textsf{Coq}}}
-\newcommand{\Coq}{\coq}
-\newcommand{\pvs}{\textsf{PVS}\index{PVS@\textsf{PVS}}}
-
-%
-
-\newcommand{\kw}[1]{\ensuremath{\mathsf{#1}}}
-
-% types
-\newcommand{\bool}{\kw{bool}}
-\newcommand{\unit}{\kw{unit}}
-%\newcommand{\tref}[1]{\ensuremath{#1~\kw{ref}}}
-\newcommand{\tref}[1]{\ensuremath{#1~\mathsf{ref}}}
-\newcommand{\tarray}[2]{\ensuremath{\kw{array}~#1~\kw{of}~#2}}
-
-% constructs
-\newcommand{\prepost}[3]{\ensuremath{\{#1\}\,#2\,\{#3\}}}
-\newcommand{\result}{\ensuremath{\mathit{result}}}
-
-\newcommand{\void}{\kw{void}}
-\newcommand{\access}[1]{\ensuremath{!#1}}
-\newcommand{\assign}[2]{\ensuremath{#1~:=~#2}}
-\newcommand{\pref}[1]{\ensuremath{\kw{ref}~#1}}
-\newcommand{\taccess}[2]{\ensuremath{#1\texttt{[}#2\texttt{]}}}
-\newcommand{\tassign}[3]{\ensuremath{#1\texttt{[}#2\texttt{]}~\texttt{:=}~#3}}
-\newcommand{\faccess}[2]{\ensuremath{(\mathit{access}~#1~#2)}}
-\newcommand{\fupdate}[3]{\ensuremath{(\mathit{update}~#1~#2~#3)}}
-%\newcommand{\taccess}[2]{\ensuremath{#1[#2]}}
-%\newcommand{\tassign}[3]{\ensuremath{#1[#2]~:=~#3}}
-%\newcommand{\faccess}[2]{\ensuremath{(\mathit{access}~#1~#2)}}
-%\newcommand{\fupdate}[3]{\ensuremath{(\mathit{update}~#1~#2~#3)}}
-% \newcommand{\block}[1]{\ensuremath{\kw{begin}~#1~\kw{end}}}
-\newcommand{\seq}[2]{\ensuremath{#1;~#2}}
-%\newcommand{\plabel}[2]{\ensuremath{#1:#2}}
-\newcommand{\plabel}[2]{\ensuremath{#1\texttt{:}#2}}
-\newcommand{\assert}[2]{\ensuremath{\kw{assert}~\{#1\};~#2}}
-\newcommand{\while}[4]{\ensuremath{\kw{while}~#1~\kw{do}~\{\kw{invariant}~#2~\kw{variant}~#3\}~#4~\kw{done}}}
-\newcommand{\ite}[3]{\ensuremath{\kw{if}~#1~\kw{then}~#2~\kw{else}~#3}}
-\newcommand{\fun}[3]{\ensuremath{\kw{fun}~#1:#2\rightarrow#3}}
-\newcommand{\app}[2]{\ensuremath{(#1~#2)}}
-\newcommand{\rec}[4]{\ensuremath{\kw{rec}~#1:#2~\{\kw{variant}~#3\}=#4}}
-\newcommand{\letin}[3]{\ensuremath{\kw{let}~#1=#2~\kw{in}~#3}}
-\newcommand{\raisex}[2]{\ensuremath{\kw{raise}~(#1~#2)}}
-\newcommand{\exn}[1]{\ensuremath{\kw{Exn}~#1}}
-\newcommand{\try}[2]{\ensuremath{\kw{try}~#1~\kw{with}~#2~\kw{end}}}
-\newcommand{\coerce}[2]{\ensuremath{(#1:#2)}}
-
-\newcommand{\statement}{\textit{statement}}
-\newcommand{\program}{\textit{program}}
-\newcommand{\expression}{\textit{expression}}
-\newcommand{\predicate}{\textit{predicate}}
-
-% inference rules
-\newcommand{\espacev}{\rule{0in}{1em}}
-\newcommand{\espacevn}{\rule[-0.4em]{0in}{1em}}
-\newcommand{\irule}[2]
-  {\frac{\espacevn\displaystyle#1}{\espacev\displaystyle#2}}
-\newcommand{\typage}[3]{#1 \, \vdash \, #2 : #3}
-\newcommand{\iname}[1]{\textsf{#1}}
-
-\newcommand{\emptyef}{\bot}
-\newcommand{\wf}[1]{#1~\kw{wf}}
-\newcommand{\pur}[1]{#1~\kw{pure}}
-\newcommand{\variant}[1]{#1~\kw{variant}}
-
-\newcommand{\wpre}[2]{\ensuremath{\mathit{wp}(#1,#2)}}
-\newcommand{\wprx}[3]{\ensuremath{\mathit{wp}(#1,#2,#3)}}
-
-\newcommand{\barre}[1]{\ensuremath{\overline{#1}}}
-
-
-% backslash keywords
-
-\newcommand{\ttkw}[1]{\texttt{#1}}
-\newcommand{\bskw}[1]{\ttkw{\char'134 #1}}
-\newcommand{\bkw}[1]{\ttkw{\textbf{#1}}}
-
-
-\newcommand{\caml}{\textsf{Caml}}
-\newcommand{\ergo}{\textsf{Ergo}\index{Ergo@\textsf{Ergo}}}
-\newcommand{\yices}{\textsf{Yices}\index{Yices@\textsf{Yices}}}
-\newcommand{\harvey}{\textsf{haRVey}\index{haRVey@\textsf{haRVey}}}
-\newcommand{\simplify}{\textsf{Simplify}\index{Simplify@\textsf{Simplify}}}
-\newcommand{\mizar}{\textsf{Mizar}\index{Mizar@\textsf{Mizar}}}
-\newcommand{\hollight}{\textsf{HOL Light}\index{HOL Light@\textsf{HOL Light}}}
-\newcommand{\isabelle}{\textsf{Isabelle/HOL}\index{Isabelle/HOL@\textsf{Isabelle/HOL}}}
-\newcommand{\holfour}{\textsf{HOL 4}\index{HOL 4@\textsf{HOL 4}}}
-\newcommand{\cvclite}{\textsf{CVC Lite}\index{CVC Lite@\textsf{CVC Lite}}}
-\newcommand{\cvcthree}{\textsf{CVC 3}\index{CVC 3@\textsf{CVC 3}}}
-\newcommand{\zenon}{\textsf{Zenon}\index{Zenon@\textsf{Zenon}}}
-\newcommand{\jml}{\textsc{JML}\index{JML@\textsf{JML}}}
-\newcommand{\caveat}{\paragraph{Caveat.}}
-\newcommand{\caveats}{\paragraph{Caveats.}}
-
-% BNF syntax
-
-\newenvironment{syntax}{\begin{tabular}{lrll}}{\end{tabular}}
-\newcommand{\te}[1]{\texttt{#1}}
-\newcommand{\nt}[1]{$\langle$\textsl{#1}$\rangle$}
-\newcommand{\indexnt}[1]{\index{#1@\textsl{#1}, grammar entry}}
-\newcommand{\indextt}[1]{\index{#1@\texttt{#1}}}
-\newcommand{\repstar}{$^{\star}$}
-\newcommand{\repstarsep}[1]{$^{\star}_#1$}
-\newcommand{\repplus}{$^+$}
-\newcommand{\repplussep}[1]{$^+_#1$}
-\newcommand{\orelse}{$\mid$}
-\newcommand{\is}{ & $::=$ &}
-\newcommand{\newl}{ \\ & $|$ &}
+\newcommand{\why}{\textsf{Why3}}
+\newcommand{\eg}{\emph{e.g.}}
+
+% BNF grammar
+\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
+\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
+\newif\ifspace
+\newif\ifnewentry
+\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
+\newcommand{\term}[2]{\addspace\hbox{\lstinline|#1|%
+\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
+\newcommand{\nonterm}[2]{%
+  \ifthenelse{\equal{#2}{}}%
+             {\addspace\hbox{\textsl{#1}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}%
+             {\addspace\hbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
+\newcommand{\repetstar}{$^*$\spacetrue}
+\newcommand{\repetplus}{$^+$\spacetrue}
+\newcommand{\repetone}{$^?$\spacetrue}
+\newcommand{\lparen}{\addspace(}
+\newcommand{\rparen}{)}
+\newcommand{\orelse}{\addspace$\mid$\spacetrue}
+\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
+\newcommand{\newl}{ \\ & & \spacefalse}
+\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
+\newcommand{\is}{ & $::=$ & \newentryfalse}
+\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
+\newcommand{\synt}[1]{$\spacefalse#1$}
+\newcommand{\emptystring}{$\epsilon$}
+\newcommand{\below}{See\; below}
 
 %%% Local Variables: 
 %%% mode: latex
-%%% TeX-master: "doc"
+%%% TeX-master: "manual"
 %%% End: 

doc/manual.tex

@@ -13,8 +13,8 @@
 \let\tt\ttfamily
 \let\bf\bfseries
 
-\newcommand{\why}{\textsf{Why3}}
-\newcommand{\eg}{\emph{e.g.}}
+\usepackage{ifthen}
+\input{./macros.tex}
 
 \input{./version.tex}
 

doc/syntaxref.tex

@@ -3,6 +3,7 @@
 
 This chapter gives the grammar for the input files
 
+\input{./term_bnf.tex}
 
 %%% Local Variables:
 %%% mode: latex

doc/term.bnf

+\begin{syntax}
+  bin-op ::= "+" | "-" | "*" | "/" | "%" ;
+       | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
+       | "&&" | "||" |   ; boolean operations
+       | "&" | "|" | "-->" ;
+       | "<-->" | "^"; bitwise operations
+       \
+  unary-op ::= "+" | "-" ; unary plus and minus
+       | "!" ; boolean negation
+       | "~" ;  bitwise complementation
+       | "*" ; pointer dereferencing
+       | "&" ; address-of operator
+       \
+  term ::= "\true" | "\false" ;
+       | integer ; integer constants
+       | real ; real constants
+       | id ; variables
+       | unary-op term ;
+       | term bin-op term ;
+       | term "[" term "]" ; array access
+       | "{" term "\with" "[" term "]" "=" term "}" ; array functional modifier
+       | term "." id  ; structure field access
+       | "{" term "\with" "."id "=" term "}" ; field functional modifier
+       | term "->" id ;
+       | "(" type-expr ")" term  ; cast
+       | id "(" term ("," term)* ")" ; function application
+       | "(" term ")" ; parentheses
+       | term "?" term ":" term ; ternary condition
+       | "\let" id "=" term ";" term ; local binding
+       | "sizeof" "(" term ")" ;
+       | "sizeof" "(" C-type-expr ")" ;
+       | id ":" term ; syntactic naming
+\end{syntax}