@@ -24,6 +24,98 @@ primarily \emph{erasing} information.
2424
2525\subsection{From \TT{} to \Idris{}}
2626
27+We define a meta-operation $\uninterp{\vt}$, which converts a \TT{} expression
28+$\vt$ to an \Idris{} expression which would elaborate to $\vt$:
29+
30+\DM{
31+\AR{
32+\begin{array}{rl}
33+\uninterp{\vx} &\mq\:\vx\\
34+\uninterp{\vc} &\mq\:\vc\\
35+\uninterp{\vx\;\ta} &\mq\:\vx\;(\vec{\MO{Impl}}\:\vx\:\ta) \\
36+\uninterp{\vf\:\va} &\mq\:\uninterp{\vf}\:\uninterp{\va}\\
37+\uninterp{\lam{\vx}{\vT}\SC\ve} &\mq \:\ilam{\vx}\uninterp{\ve} \\
38+\uninterp{\all{\vx}{\vT}\SC\ve} &\mq \:\piexp{\vx}{\uninterp{\vT}}\uninterp{\ve} \\
39+\uninterp{\LET\:\vx\defq\vt\Hab\vT\SC\ve} &\mq
40+\ilet{\vx}{\uninterp{\vt}}\uninterp{\ve}\\
41+\end{array}
42+\medskip\\
43+\begin{array}{rll}
44+\MO{Impl}\:\vx\:\va_i\:\mq
45+&
46+\iarg{\vn}{\ttinterp{\va_i}}&
47+\mbox{(if the $i$th argument to $\vx$ is implicit argument $\vn$)}\\
48+& \carg{\ttinterp{\va_i}} &
49+\mbox{(if the $i$th argument to $\vx$ is a constraint argument)}\\
50+& \ttinterp{\va_i} & \mbox{(otherwise)}
51+\end{array}
52+}
53+}
54+
55+\noindent
56+This is mostly a straightforward
57+traversal of the \TT{} expression, translating directly to an \Idris{} equivalent.
58+The interesting case is for applications of named functions,
59+$\uninterp{\vx\:\ta}$, where the arguments are translated to either implicit,
60+constraint or explicit arguments according to the definition of $\vx$.
61+Since only type declarations are allowed to have implicit or constraint arguments,
62+and $\uninterp{\cdot}$ translates \emph{expressions},
63+all function types are assumed to take explicit arguments.
64+
65+We also define an operation $\MO{Unelab}$, which translates \TT{} declarations
66+to corresponding \Idris{} declarations. This generates data declarations and
67+pattern matching definitions only --- it makes no attempt to reconstruct
68+\texttt{class}
69+or \texttt{instance} declarations, or rebuild \texttt{case} expressions.
70+First, we define the reverse elaboration of type declarations, which must reconstruct
71+which arguments are implicit or constraint arguments:
72+
73+\DM{
74+\AR{
75+\begin{array}{l}
76+\MO{UnelabType}\:(\vx\Hab\vt)\:\mq\:\vx\Hab\MO{UnelabTyDecl}\:0\:\vt
77+\end{array}
78+\medskip\\
79+\begin{array}{ll}
80+\MO{UnelabTyDecl}\:\vi\:(\all{\vx}{\vT}\SC\ve)
81+\mq & \piimp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
82+ & \hg\mbox{(if the $i$th argument to $\vx$ is an implicit argument)} \\
83+ & \piconst{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
84+ & \hg\mbox{(if the $i$th argument to $\vx$ is a constraint argument)} \\
85+ & \piexp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
86+ & \hg\mbox{(otherwise)} \\
87+\end{array}
88+}
89+}
90+
91+\noindent
92+Using this, we define $\MO{Unelab}$ for top level declarations. For pattern
93+matching clauses, we reverse elaborate as follows, discarding the explicit
94+pattern variable bindings and applying $\MO{UnelabType}$ to reconstruct
95+the type declaration:
96+
97+\DM{
98+\AR{
99+\MO{Unelab}\:(\vx\Hab\vt)\:\mq\:\MO{UnelabType}\:(\vx\Hab\vt)\\
100+\MO{Unelab}\:(\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
101+\:\mq\:\uninterp{\FN{f}\:\tts}\:=\:\uninterp{\ve}
102+}
103+}
104+
105+\noindent
106+For data type declarations, we unelaborate as follows, applying $\MO{UnelabType}$
107+for each of the top level type declarations:
108+
109+\DM{
110+\AR{
111+\MO{Unelab}\:(\Data\;\TC{T}\:(\tx\Hab\ttt)\Hab\vT\;\Where\;\vec{\VV{cons}})
112+\:\\
113+\hg\hg\mq\:\idata\:\MO{UnelabType}\:(\TC{T}\Hab\all{\tx}{\ttt}\SC\vT)\:\iwhere\:
114+(\vec{\MO{UnelabType}}\:\vec{\VV{cons}})
115+}
116+}
117+
118+
27119\subsection{Elaboration Properties}
28120
29121\todo[inline]{