...

parent 66ff65a1
We give only an extremely dense explanation of the Coq language and refer to Appendix~\ref{app:coq} and \cite{coq} for details.
We use a \textbf{grammar} for the \emph{abstract} syntax seen by the Coq kernel (Fig.~\ref{fig:coqgrammar}) because that is the one that our translation works with.
Even though we do not have space to describe all aspects of the translation in detail, we give the entire grammar here in order to document which language features we translate.
Even though we do not have space to describe all aspects of the translation in detail, we give an almost entire grammar here in order to document most of the language features we translate. A slightly more comprehensive grammar is presented in the companion paper~\cite{coqtoxml_csc}: the omitted features do not pose additional problems to the translation to MMT and are omitted to simplify the presentation.
\renewcommand{\bnf}[1]{{\color{red}#1}}
......@@ -49,31 +49,34 @@ Even though we do not have space to describe all aspects of the translation in d
\begin{figure}[hbt]
\[\begin{array}{lcl}
\decl & \bbc & \textit{base logic declarations} \\
\decl & \bbc & \textit{--- base logic declarations} \\
& & \uid@\{\rep{y}\}:\term \opt{:=\term}\\
& \bnfalt & \Univ\;\uu \\
& \bnfalt & \Constraint\; \qu \bnfbracket{{<}\bnfalt{\leq}\bnfalt{=}} \qu\\
& \bnfalt & \bnfbracket{\Inductive\bnfalt\CoInductive}\;\brep{\uid@\{\rep{y}\} :\term := \brep{\uid@\{\rep{y}\}:\term}}\\
& & \multicolumn{1}{l}{\textit{section declarations and variables in sections}} \\
& & \multicolumn{1}{l}{\textit{--- section declarations and variables in sections}} \\
& \bnfalt & \Section\;\us \;:=\;\body\\
& \bnfalt & \Variable\;x:\term \\
& \bnfalt & \Polymorphic\;\Univ\;y \\
& \bnfalt & \Polymorphic\;\Constraint\;\bnfbracket{\qu \bnfalt y}\bnfbracket{{<}\bnfalt{\leq}\bnfalt{=}}\bnfbracket{\qu \bnfalt y} \\
& & \multicolumn{1}{l}{\textit{module (type) declarations}} \\
& & \multicolumn{1}{l}{\textit{--- module (type) declarations}} \\
& \bnfalt & \ModTyp \um \;\mbind <:\rep{\mte}\; := \bnfbracket{\mte\bnfalt\body} \\
& \bnfalt & \ModuleP \umt \;\mbind\; \opt{:\mte} \; <:\rep{\mte}\; \opt{:= \bnfbracket{\me\bnfalt\body}} \\
& & \multicolumn{1}{l}{\textit{base logic expressions $\term$ and universes $\univ$}}\\
\term & \bbc & \qid@\{\rep{\univ}\} \bnfalt x \bnfalt \Prop \bnfalt\USet\bnfalt\Tp{\univ} \bnfalt \Pi x:\term.\term \bnfalt \lambda x:\term.\term \bnfalt \term\;\term \\
\term & \bbc & \multicolumn{1}{l}{\textit{--- base logic expressions}}\\
& & \qid@\{\rep{\univ}\} \bnfalt x \bnfalt \Prop \bnfalt\USet\bnfalt\Tp{\univ} \bnfalt \Pi x:\term.\term \bnfalt \lambda x:\term.\term \bnfalt \term\;\term \\
& \bnfalt & \Match\,\qid\,\term\,\term\,\rep{\term} \bnfalt \bnfbracket{\Fix\bnfalt\CoFix}\,\N\,\brep{\uid:\term:=\term}
\bnfalt \texttt{let } x:\term := \term \texttt{ in } \term\\
& \bnfalt & \term.\mathbb{N} \bnfalt (\term : \term)\\
\univ & \bbc & \qu \bnfalt y \bnfalt \max\,\univ\,\univ \bnfalt \cn{succ}\, \univ\\ % \brep{\qu+\N\bnfalt x+\N}\\
& & \multicolumn{1}{l}{\textit{module type expressions $\mte$ and module expressions $\me$}}\\
\mte & \bbc & \opt{!}\;\qmt\;\rep{\qm} \bnfalt \mte\;\with\; \rqid := \term \bnfalt \mte\;\with\; \rqm := \me\\
\me & \bbc & \opt{!}\;\qm\;\rep{\qm}\\
\qid,\qu,\qm,\qmt & \bbc & \text{qualified identifiers of expressions, universes, modules, module types}\\
\univ & \bbc & \multicolumn{1}{l}{\textit{--- universes}}\\
& & \qu \bnfalt y \bnfalt \max\,\univ\,\univ \bnfalt \cn{succ}\, \univ\\ % \brep{\qu+\N\bnfalt x+\N}\\
\mte & \bbc & \multicolumn{1}{l}{\textit{--- module type expressions}}\\
& & \opt{!}\;\qmt\;\rep{\qm} \bnfalt \mte\;\with\; \rqid := \term \bnfalt \mte\;\with\; \rqm := \me\\
\me & \bbc & \multicolumn{1}{l}{\textit{--- module expressions}}\\
& & \opt{!}\;\qm\;\rep{\qm}\\
x,y & \bbc & \text{variables for term, universe respectively}\\
\qid,\qu,\qm,\qmt,s & \bbc & \text{qualified identifiers of expressions, universes, modules, module types, sections}\\
\rqid,\rqm & \bbc & \text{relative qualified identifiers of expressions, modules}\\
\uid,\uu,\um,\umt & \bbc & \text{fresh (unqualified) identifiers}\\
\uid,\uu,\um,\umt,\us & \bbc & \text{fresh (unqualified) identifiers}\\
\end{array}\]
\caption{Coq Kernel Grammar}\label{fig:coqgrammar}
\end{figure}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment