@@ -1,12 +1,133 @@
1+\newcommand{\ttinterp}[1]{\mathcal{E}\interp{#1}}
1\section{Elaborating \Idris{}}
3\section{Elaborating \Idris{}}
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:
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.
3\subsection{The Development Calculus \TTdev}
17\subsection{The Development Calculus \TTdev}
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}.
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.
44+ \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:
45+ \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})
48+\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT
51+\Gamma\proves\hole{\vx}{\vS}\SC\ve\Hab\vT
53+\hspace*{0.1cm}\vx\not\in\vT
54+\hspace*{0.1in}\mathsf{Hole}
57+\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT
60+\Gamma\proves\guess{\vx}{\vS}{\ve_1}\SC\ve_2\Hab\vT
62+\hspace*{0.1cm}\vx\not\in\vT
63+\hspace*{0.1in}\mathsf{Guess}
7−\subsection{The $\MO{Elab}$ meta-language}
70+\subsection{Proof State}
72+A proof state is a tuple, $(\vC, \Delta, \vT, \vQ)$, containing:
10\begin{itemize}
74\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
12\end{itemize}
80\end{itemize}
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}
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.
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:
98+\item \demph{Queries} which retrieve values from the proof state, without modifying
99+the state. For example, we can:
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$
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.
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).
118+\subsection{System State}
120+We need the global state, for implicits, global context.
122+\subsection{Elaborating Expressions}
125+\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation, etc).
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).
130+\subsection{Elaborating Data Types}
132+\subsection{Elaborating Pattern Matching}