<commit_before>\documentclass[a4paper,12pt]{report}

\usepackage{fullpage}
\usepackage{url}
\usepackage{makeidx}
\usepackage{verbatim}
\usepackage{graphicx}
\input{./version.tex}
\input{./macros.tex}

\makeindex

\begin{document}

%%% coverpage
\whytitlepage{The WHY verification tool}{Tutorial and Reference
  Manual}{\whyversion}{Team-Project ProVal}


\tableofcontents

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter*{Foreword}
\addcontentsline{toc}{chapter}{Foreword}



\subsection*{License}

The \why\ tool is \copyright\ 2002--2010 team-project ProVal
(\url{proval.lri.fr}).
It is open source and freely available under the terms of the Gnu
Library General Public License Version 2.1 (see the file
\texttt{LICENSE} included in the distribution).

\subsection*{Availability}

The \why\ tool is available from \url{http://why.lri.fr/}, in source
and binary formats, together with this documentation and many
examples.


\subsection*{Contact}

There is a mailing list for \why;
see \url{http://lists.lri.fr/mailman/listinfo/why}.

% TODO BTS


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Syntax of input files}
\label{syntax}

\section{Lexical conventions}

Comments are opened with \texttt{(*}, closed
with \texttt{*)} and can be nested.

Identifiers are made of letters, digits,
the underscore character \texttt{\_} and the single quote \texttt{'},
starting with a letter. In many cases, identifiers starting with
lowercase or uppercase characters are distinguished.

\begin{center}\framebox{\begin{syntax}
  \nt{lident}\indexnt{lident}
      \is \te{a}..\te{z} \nt{ident\_char}\repstar \\
  \nt{uident}\indexnt{uident}
      \is \te{A}..\te{Z} \nt{ident\_char}\repstar \\
  \nt{ident\_char} 
      \is \te{A}..\te{Z} \orelse \te{a}..\te{z} \orelse
      \te{0}..\te{9} \orelse \te{\_} \orelse \te{'} \\[0.1em]
  \nt{ident} 
      \is \nt{lident} \orelse\ \nt{uident}
\end{syntax}}\end{center}

Keywords are the following:
\begin{center}
{\tt\begin{tabular}{l@{\qquad}l@{\qquad}l@{\qquad}l@{\qquad}l}
        absurd &
	and &
        array &
	as &
	assert \\
	axiom &
	begin &
        bool &
	do &
	done \\
        else &
	end &
	exception &
	exists &
	external \\
        false &
	for &
	forall &
	fun &
	function \\
	goal &
	if &
	in &
	int &
	invariant \\
%	label &
	let &
	logic &
	not &
	of \\
	or &
	parameter &
	predicate &
	prop &
	raise \\
	raises &
	reads &
	real &
	rec &
	ref \\
	returns &
	then &
	true &
	try &
	type \\
	unit &
	variant &
	void &
	while &
	with \\
        writes &
\end{tabular}}
\end{center}

\section{Grammar}

\subsection{Qualified names}

\begin{center}\framebox{\begin{syntax}
  \nt{lqualid} \is 
\end{syntax}}\end{center}

\subsection{Terms}


\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
  \nt{term}\indexnt{term}
    \is   \nt{constant} 
    \newl \nt{term} \nt{arith\_op} \nt{term} \\
      & $|$ & \te{-} \nt{term} \\
      & $|$ & \nt{lab\_identifier} \\
      & $|$ & \nt{identifier} \te{(} \nt{term}\repplussep{\te{,}} \te{)} \\
      & $|$ & \nt{lab\_identifier} \te{[} \nt{term} \te{]} \\
      & $|$ & \te{if} \nt{term} \te{then} \nt{term} \te{else} \nt{term} \\<commit_msg>un peu de definition de syntax<commit_after>\documentclass[a4paper,12pt]{report}

\usepackage{fullpage}
\usepackage{url}
\usepackage{makeidx}
\usepackage{verbatim}
\usepackage{graphicx}
\input{./version.tex}
\input{./macros.tex}

\makeindex

\begin{document}

%%% coverpage
\whytitlepage{The WHY verification tool}{Tutorial and Reference
  Manual}{\whyversion}{Team-Project ProVal}


\tableofcontents

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter*{Foreword}
\addcontentsline{toc}{chapter}{Foreword}



\subsection*{License}

The \why\ tool is \copyright\ 2002--2010 team-project ProVal
(\url{proval.lri.fr}).
It is open source and freely available under the terms of the Gnu
Library General Public License Version 2.1 (see the file
\texttt{LICENSE} included in the distribution).

\subsection*{Availability}

The \why\ tool is available from \url{http://why.lri.fr/}, in source
and binary formats, together with this documentation and many
examples.


\subsection*{Contact}

There is a mailing list for \why;
see \url{http://lists.lri.fr/mailman/listinfo/why}.

% TODO BTS


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Syntax of input files}
\label{syntax}

\section{Lexical conventions}

Comments are opened with \texttt{(*}, closed
with \texttt{*)} and can be nested.

Identifiers are made of letters, digits,
the underscore character \texttt{\_} and the single quote \texttt{'},
starting with a letter. In many cases, identifiers starting with
lowercase or uppercase characters are distinguished.

\begin{center}\framebox{\begin{syntax}
  \nt{lident}\indexnt{lident}
      \is \te{a}..\te{z} \nt{ident\_char}\repstar \\
  \nt{uident}\indexnt{uident}
      \is \te{A}..\te{Z} \nt{ident\_char}\repstar \\
  \nt{ident\_char} 
      \is \te{A}..\te{Z} \orelse \te{a}..\te{z} \orelse
      \te{0}..\te{9} \orelse \te{\_} \orelse \te{'} \\[0.1em]
  \nt{ident} 
      \is \nt{lident} \orelse\ \nt{uident}
\end{syntax}}\end{center}

Keywords are the following:
\begin{center}
{\tt\begin{tabular}{l@{\qquad}l@{\qquad}l@{\qquad}l@{\qquad}l}
        absurd &
	and &
        array &
	as &
	assert \\
	axiom &
	begin &
        bool &
	do &
	done \\
        else &
	end &
	exception &
	exists &
	external \\
        false &
	for &
	forall &
	fun &
	function \\
	goal &
	if &
	in &
	int &
	invariant \\
%	label &
	let &
	logic &
	not &
	of \\
	or &
	parameter &
	predicate &
	prop &
	raise \\
	raises &
	reads &
	real &
	rec &
	ref \\
	returns &
	then &
	true &
	try &
	type \\
	unit &
	variant &
	void &
	while &
	with \\
        writes &
\end{tabular}}
\end{center}

\section{Grammar}
%% file := decl*
%% decl := | "theory" uident decl* "end"
%%         | "theory" uident "." uqualid ("with" instance+ )?
%%         | "use" "open"?  uqualid ("as" ident)
%%         | "use" "include" uqualid %% pas de as pour include
%%         | ("axiom"|"lemma"|"goal") ident ":" fmla
%%         | "type" typarams lident ("=" (ty-alg | ty))?
%%           ("and" typarams lident ("=" (ty-alg | ty))?)* 
%% Il faut verifier qu'il y a toujours un constructeur entre deux
%% définitions récursives. 
%%         | "logic" def ("and" def)*
%%         | "inductive" ...

%% def := lident_ou_infix ("(" formal+, ")")? (":" ty)? ("=" lexpr)?
%% formal := ((lident|_)":")? ty         

%% instance := | lqualid "=" lqualid
%% ty-alg := | uident ("(" ty,+ ")")? ("|" uident ...)*

\subsection{Qualified names}

\begin{center}\framebox{\begin{syntax}
  \nt{lqualid} \is 
\end{syntax}}\end{center}

\subsection{Terms}


\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
  \nt{term}\indexnt{term}
    \is   \nt{constant} 
    \newl \nt{term} \nt{arith\_op} \nt{term} \\
      & $|$ & \te{-} \nt{term} \\
      & $|$ & \nt{lab\_identifier} \\
      & $|$ & \nt{identifier} \te{(} \nt{term}\repplussep{\te{,}} \te{)} \\
      & $|$ & \nt{lab\_identifier} \te{[} \nt{term} \te{]} \\
      & $|$ & \te{if} \nt{term} \te{then} \nt{term} \te{else} \nt{term} \\
{'fraction_non_alphanumeric': 0.21644063105452532, 'fraction_numerical': 0.004705231109880985, 'mean_word_length': 3.120296465222349, 'pattern_counts': {'":': 3, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '54936', 'n_tokens_mistral': 2746, 'n_tokens_neox': 2624, 'n_words': 602}