@@ -1,7 +1,29 @@
1−\section{Reversing Elaboration: From \TT{} to \Idris{}}
1+\section{Reversing Elaboration}
22
33\label{sect:delab}
44
5+As well as translating from \Idris{} to \TT{}, so that programs can be type
6+checked and evaluated, it is valuable to define the reverse transformation. This
7+serves two principal purposes:
8+
9+\begin{itemize}
10+\item To assist the user, it is preferable that the results of evaluation, and any
11+error messages produced by the elaborator, are presented in \Idris{} syntax
12+rather than \TT{}.
13+\item For correctness, we would like to ensure as far as possible that the
14+result of elaboration is equivalent to the original program. Informally, we can
15+achieve this by checking that reversing the elaboration process yields the original
16+program (with implicit arguments expanded).
17+\end{itemize}
18+
19+\noindent
20+In this section, we describe the process for reversing elaboration and the required
21+properties of the elaboration process as a whole. Fortunately, translating from
22+\TT{} to \Idris{} is significantly easier than \Idris{} to \TT{}, because it is
23+primarily \emph{erasing} information.
24+
25+\subsection{From \TT{} to \Idris{}}
26+
527\subsection{Elaboration Properties}
628
729\todo[inline]{
@@ -11,3 +33,10 @@ an expression yields the original expression.
1133(Works for expressions but not declarations)
1234}
1335
36+Properties:
37+\begin{itemize}
38+\item Elaboration produces a well-typed term
39+\item $\ve \MO{Matches} \uninterp{\ttinterp{\ve}}$
40+\end{itemize}
41+
42+