@@ -1,12 +1,133 @@
1+\newcommand{\ttinterp}[1]{\mathcal{E}\interp{#1}}
2+
13\section{Elaborating \Idris{}}
24
5+An \Idris{} program consists of a series of declarations --- data types, functions,
6+type classes and instances. In this section, we describe how these high level declarations
7+are translated into a \TT{} program consisting of inductive families and pattern matching
8+function definitions. We will need to work at the \remph{declaration} level, and at
9+the \remph{expression} level, defining the following meta-operations:
10+
11+\begin{itemize}
12+\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression
13+\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating
14+one or more \TT{} declarations.
15+\end{itemize}
16+
317\subsection{The Development Calculus \TTdev}
418
5−\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.
19+We build \TT{} expressions by using high level \Idris{} expressions to
20+direct a tactic based theorem prover, which builds the \TT{} expressions
21+step by step, by refinement. In order to build expressions in this way,
22+the type theory needs to support
23+\remph{incomplete} terms, and a method for term construction.
24+To achieve this, we extend \TT{} with \remph{holes},
25+calling the extended calculus \TTdev{}.
26+Holes stand for the parts of programs which have not yet been
27+instantiated; this largely follows the \Oleg{} development
28+calculus~\cite{McBride1999}.
29+
30+The basic idea is to extend the syntax for binders with a \remph{hole}
31+binding and a \remph{guess} binding.
32+These extensions are given in Figure \ref{ttdev}.
33+The \remph{guess} binding is
34+similar to a $\LET$ binding, but without any computational force,
35+i.e. the bound names do not reduce.
36+Using binders to represent holes is useful in a dependently typed setting since
37+one value may determine another. Attaching a ``guess'' to a binder ensures that
38+instantiating one such value also instantiates all of its dependencies. The
39+typing rules for binders ensure that no $?$ bindings leak into types.
40+
41+\FFIG{
42+\AR{
43+\vb ::= \ldots
44+ \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:
45+ \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})
46+\medskip\\
47+\Rule{
48+\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT
49+}
50+{
51+\Gamma\proves\hole{\vx}{\vS}\SC\ve\Hab\vT
52+}
53+\hspace*{0.1cm}\vx\not\in\vT
54+\hspace*{0.1in}\mathsf{Hole}
55+\hg
56+\Rule{
57+\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT
58+}
59+{
60+\Gamma\proves\guess{\vx}{\vS}{\ve_1}\SC\ve_2\Hab\vT
61+}
62+\hspace*{0.1cm}\vx\not\in\vT
63+\hspace*{0.1in}\mathsf{Guess}
64+}
65+}
66+{\TTdev{} extensions}
67+{ttdev}
668
7−\subsection{The $\MO{Elab}$ meta-language}
869
70+\subsection{Proof State}
71+
72+A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
973
1074\begin{itemize}
11−\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$
75+\item A global context, $\vC$, containing pattern matching definitions
76+\item A local context, $\Delta$, containing pattern bindings
77+\item A proof term, $\vT$, in \TTdev{}
78+\item A hole queue, $\vQ$
79+%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
1280\end{itemize}
81+
82+The \remph{hole queue} is a list of names of hole and guess binders in the proof term ---
83+we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
84+in the proof.
85+When this queue is empty, the proof term is complete.
86+Creating a \TT{} expression from an \Idris{} expresson involves creating
87+a new proof state, with an empty proof term, and using the high level definition
88+to direct the building of a final proof state, with a complete proof term.
89+
90+In the implementation, the proof state is captured in an elaboration monad,
91+\texttt{Elab}, which includes various operations for querying and updating
92+the proof state, manipulating terms, generating fresh names, etc. However, we will
93+describe \Idris{} elaboration in terms of meta-operations on the proof state,
94+in order to capture the essence of the elaboration process without being distracted
95+by implementation details. These meta-operations include:
96+
97+\begin{itemize}
98+\item \demph{Queries} which retrieve values from the proof state, without modifying
99+the state. For example, we can:
100+\begin{itemize}
101+\item Retrieve the local context $\Gamma$ at the current sub goal
102+\item Type check or normalise a term relative to $\Gamma$
103+\item Unify two terms (potentially solving sub goals) relative to $\Gamma$
104+\end{itemize}
105+\item \demph{Tactics} which update the proof term. Tactics operate on the sub term
106+at the binder specified by the head of the hole queue $\vQ$.
107+\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the
108+head of the hole queue.
109+\item \demph{Deferring} a sub goal, which adds a new definition to the global context
110+$\vC$ which solves the sub goal.
111+\end{itemize}
112+
113+Elaboration of an \Idris{} expression involves creating a new proof state, running
114+a series of tactics to build a complete proof term, then retrieving and \remph{rechecking}
115+the final proof term, which must be a \TT{} program (i.e. does not contain any of the
116+\TTdev{} extensions).
117+
118+\subsection{System State}
119+
120+We need the global state, for implicits, global context.
121+
122+\subsection{Elaborating Expressions}
123+
124+
125+\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation, etc).
126+
127+Implicit and type class arguments? Expanded at the application site (we need to know
128+it's the global name after all and we do that by type).
129+
130+\subsection{Elaborating Data Types}
131+
132+\subsection{Elaborating Pattern Matching}
133+