@@ -1,7 +1,29 @@
1−\section{Reversing Elaboration: From \TT{} to \Idris{}}
1+\section{Reversing Elaboration}
3\label{sect:delab}
3\label{sect:delab}
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:
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
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).
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.
25+\subsection{From \TT{} to \Idris{}}
5\subsection{Elaboration Properties}
27\subsection{Elaboration Properties}
7\todo[inline]{
29\todo[inline]{
@@ -11,3 +33,10 @@ an expression yields the original expression.
11(Works for expressions but not declarations)
33(Works for expressions but not declarations)
38+\item Elaboration produces a well-typed term
39+\item $\ve \MO{Matches} \uninterp{\ttinterp{\ve}}$