\RequirePackage{amsmath}
\documentclass{jfp1}
%\documentclass[acmtoplas]{acmtrans2m}

\usepackage[draft]{comments}
%\usepackage[final]{comments}
% \newcommand{\comment}[2]{[#1: #2]}
\newcommand{\khcomment}[1]{\comment{KH}{#1}}
\newcommand{\ebcomment}[1]{\comment{EB}{#1}}

\usepackage{epsfig}
%\usepackage{path}
\usepackage{url}
\usepackage{fancyvrb}

\newenvironment{template}{\sffamily}

%\usepackage{graphics,epsfig}
\usepackage{stmaryrd}
\usepackage{amsmath} 

\input{./macros.ltx}
\input{./library.ltx}

\NatPackage
\FinPackage

\newcounter{per}
\setcounter{per}{1}

\newcommand{\Ivor}{\textsc{Ivor}}
\newcommand{\Idris}{\textsc{Idris}}
\newcommand{\IdrisM}{\textsc{Idris}$^-$}
\newcommand{\TT}{\textsf{TT}}
\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
\newcommand{\Funl}{\textsc{Funl}}
\newcommand{\Agda}{\textsc{Agda}}
\newcommand{\LamPi}{$\lambda_\Pi$}

\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
\begin{center}
\fbox{
\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
\end{minipage}}
\end{center}
\vspace*{0.1cm}
}

\newcommand{\mysubsubsection}[1]{
\noindent
\textbf{#1}
}
\newcommand{\hdecl}[1]{\texttt{#1}}


\title
[Idris, a General Purpose Dependently Typed Programming Language]
{Idris, a General Purpose Dependently Typed Programming Language:
Design and Implementation}
%Implementing General Purpose Dependently Typed Programming Languages}
%\subtitle{Implementing Domain Specific Languages by Overloading}

\author[Edwin Brady]
{EDWIN BRADY\\
School of Computer Science, University of St Andrews, St Andrews,
KY16 9SX, UK}

\begin{document}

\maketitle

\begin{abstract}
Many components of a dependently-typed programming language are by now well
understood, for example the underlying type theory, type checking, unification and
evaluation.  How to combine these components into a realistic and usable 
high-level language is, however, folklore, discovered anew by successive
language implementators.  In this paper, I describe the implementation of 
\Idris{}, a new dependently-typed functional programming language.
\Idris{} is intended to be a \emph{general purpose} programming language
and as such provides high-level concepts such as implicit syntax, 
type classes and \texttt{do} notation. 
I describe the high-level language and the underlying type theory, and present
a tactic-based method for \emph{elaborating} concrete high-level syntax with
implicit arguments and type classes into a fully explicit type theory.
Furthermore, I show how this method facilitates the implementation of new 
high-level language constructs.

%I describe the implementation of a dependently typed functional
%programming language, \Idris{}. Much has been written about various
%aspects of dependently typed language implementation (e.g. checking
%dependent types, unification, optimisation) but nothing yet about how
%to bring it all together into a complete, practical, usable tool. This paper
%attempts to do so. In particular, I explain what is needed to turn 
%concrete syntax with implicit arguments into fully elaborated type
%theory, using unification and a tactic engine.
\end{abstract}


%\category{D.3.2}{Programming Languages}{Language
%  Classifications}[Applicative (functional) Languages]
%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
%\terms{Languages, Verification, Performance}
%\keywords{Dependent Types, Typechecking}


%\begin{bottomstuff}
%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
%KY16 9SX
%\end{bottomstuff}

\input{intro.tex}

%\input{overview.tex}

\input{hll.tex}

\input{typechecking.tex}

%\input{proofstate.tex}

\input{elaboration.tex}

\input{delab.tex}

%\input{compiling.tex}

%\input{syntax.tex}

\input{conclusions.tex}

\section*{Acknowledgements}

This work was funded by the Scottish Informatics and Computer Science Alliance
(SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE).  My thanks to
Philip H\"{o}lzenspies, Kevin Hammond, Vilhelm Sj\"{o}berg, Falko Spiller
and Nathan Collins
for their comments on an earlier draft of this paper, and to the anonymous
referees for their many insightful and constructive comments.

\bibliographystyle{jfp}
\bibliography{library.bib}

\appendix

%\section{TODOs}
%\listoftodos{}

%\section{Elaboration meta-operations}

%It's possible that it would be useful to have a quick reference of meta-operations
%used by the elaborator here.

%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
%$\MO{NewProof}$, $\MO{NewTerm}$,
%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.

%\input{code}

\end{document}