<commit_before>\chapter{Extensions of {\sf Gallina}}
\label{Gallina-extension}\index{Gallina}

{\gallina} is the kernel language of {\Coq}. We describe here extensions of
the Gallina's syntax.

\section{Record types}\comindex{Record}
\label{Record}

The \verb+Record+ construction is a macro allowing the definition of
records as is done in many programming languages.  Its syntax is
described on figure \ref{record-syntax}.  In fact, the \verb+Record+
macro is more general than the usual record types, since it allows
also for ``manifest'' expressions. In this sense, the \verb+Record+
construction allows to define ``signatures''.

\begin{figure}
\begin{tabular}{|lcl|}
\hline
{\sentence} & ::= & {\record}\\
  & & \\
{\record} & ::= &  {\tt Record} {\ident} \zeroone{{\tt [} {\params} {\tt ]}} {\tt :} {\sort}
    \verb.:=. \zeroone{\ident} \verb!{! 
    \zeroone{\nelist{\field}{;}}
    \verb!}! \verb:.:\\
  & & \\
{\field} & ::= & {\ident} \verb.:. {\type} \\
 & $|$ & {\ident} \verb.:=. {\term} \\
 & $|$ & {\ident} \verb.:. {\type} \verb.:=. {\term} \\
\hline
\end{tabular}
\caption{Syntax for the definition of {\tt Record}}
\label{record-syntax}
\end{figure}

\noindent In the expression

\smallskip
{\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} 
   {\sort} := {\ident$_0$} \verb+{+
 {\ident$_1$} \texttt{:} {\term$_1$}; 
              \dots
  {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.
\smallskip
 
\noindent the identifier {\ident} is the name of the defined record and {\sort}
is its type. The identifier {\ident$_0$} is the name of its
constructor. If {\ident$_0$} is omitted, the default name {\tt
Build\_{\ident}} is used. The identifiers {\ident$_1$}, ..,
{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$}
their respective types. Remark that the type of {\ident$_i$} may
depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
fields is important. Finally, {\params} are the parameters of the
record.

More generally, a record may have explicitly defined (a.k.a.
manifest) fields. For instance, {\tt Record} {\ident} {\tt [}
{\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$}
\texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$} \verb+;+.
{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$}  of  {\ident$_2$ and  {\term$_2$}  in turn may depend on {\ident$_1$}.


\Example
The set of rational numbers may be defined as:
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Record Rat : Set := mkRat {
 sign     : bool;
 top      : nat;
 bottom   : nat;
 Rat_bottom_cond : ~O=bottom;
 Rat_irred_cond:(x,y,z:nat)(mult x y)=top/\(mult x z)=bottom->x=(S O)}.
\end{coq_example}

Remark here that the field
\verb+Rat_cond+ depends on the field \verb+bottom+. 

Let us now see the work done by the {\tt Record} macro.
First the macro generates a inductive definition
with just one constructor:

\medskip
\noindent
{\tt Inductive {\ident} [ {\params} ] : {\sort} := \\
\mbox{}\hspace{0.4cm} {\ident$_0$} : ({\ident$_1$}:{\term$_1$}) .. 
({\ident$_n$}:{\term$_n$})({\ident} {\rm\sl params}).}
\medskip<commit_msg>\} manquant<commit_after>\chapter{Extensions of {\sf Gallina}}
\label{Gallina-extension}\index{Gallina}

{\gallina} is the kernel language of {\Coq}. We describe here extensions of
the Gallina's syntax.

\section{Record types}\comindex{Record}
\label{Record}

The \verb+Record+ construction is a macro allowing the definition of
records as is done in many programming languages.  Its syntax is
described on figure \ref{record-syntax}.  In fact, the \verb+Record+
macro is more general than the usual record types, since it allows
also for ``manifest'' expressions. In this sense, the \verb+Record+
construction allows to define ``signatures''.

\begin{figure}
\begin{tabular}{|lcl|}
\hline
{\sentence} & ::= & {\record}\\
  & & \\
{\record} & ::= &  {\tt Record} {\ident} \zeroone{{\tt [} {\params} {\tt ]}} {\tt :} {\sort}
    \verb.:=. \zeroone{\ident} \verb!{! 
    \zeroone{\nelist{\field}{;}}
    \verb!}! \verb:.:\\
  & & \\
{\field} & ::= & {\ident} \verb.:. {\type} \\
 & $|$ & {\ident} \verb.:=. {\term} \\
 & $|$ & {\ident} \verb.:. {\type} \verb.:=. {\term} \\
\hline
\end{tabular}
\caption{Syntax for the definition of {\tt Record}}
\label{record-syntax}
\end{figure}

\noindent In the expression

\smallskip
{\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} 
   {\sort} := {\ident$_0$} \verb+{+
 {\ident$_1$} \texttt{:} {\term$_1$}; 
              \dots
  {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.
\smallskip
 
\noindent the identifier {\ident} is the name of the defined record and {\sort}
is its type. The identifier {\ident$_0$} is the name of its
constructor. If {\ident$_0$} is omitted, the default name {\tt
Build\_{\ident}} is used. The identifiers {\ident$_1$}, ..,
{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$}
their respective types. Remark that the type of {\ident$_i$} may
depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
fields is important. Finally, {\params} are the parameters of the
record.

More generally, a record may have explicitly defined (a.k.a.
manifest) fields. For instance, {\tt Record} {\ident} {\tt [}
{\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$}
\texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$} \verb+;+.
{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$}  of  {\ident$_2$} and  {\term$_2$}  in turn may depend on {\ident$_1$}.


\Example
The set of rational numbers may be defined as:
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Record Rat : Set := mkRat {
 sign     : bool;
 top      : nat;
 bottom   : nat;
 Rat_bottom_cond : ~O=bottom;
 Rat_irred_cond:(x,y,z:nat)(mult x y)=top/\(mult x z)=bottom->x=(S O)}.
\end{coq_example}

Remark here that the field
\verb+Rat_cond+ depends on the field \verb+bottom+. 

Let us now see the work done by the {\tt Record} macro.
First the macro generates a inductive definition
with just one constructor:

\medskip
\noindent
{\tt Inductive {\ident} [ {\params} ] : {\sort} := \\
\mbox{}\hspace{0.4cm} {\ident$_0$} : ({\ident$_1$}:{\term$_1$}) .. 
({\ident$_n$}:{\term$_n$})({\ident} {\rm\sl params}).}
\medskip
{'fraction_non_alphanumeric': 0.20370079974909833, 'fraction_numerical': 0.007213423239767916, 'mean_word_length': 3.565497494631353, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, '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': '5729278', 'n_tokens_mistral': 2215, 'n_tokens_neox': 2158, 'n_words': 730}