Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge branch 'master' of https://github.com/edwinb/EpiVM

  • Loading branch information...
commit b744d34801aa72c017ee5873855beb8682d18f33 2 parents 121edc2 + 8b113af
Olle authored
View
4 Epic/Language.lhs
@@ -34,6 +34,8 @@ Raw data types. Int, Char, Bool are unboxed.
> | TyData -- generic data type
> | TyCType String -- Exported, C typedef
> | TyFun -- any function
+> | TyLin Type -- guarantee at most one instance
+> | TyEval Type -- guarantee evaluated
> deriving Eq
> instance Show Type where
@@ -50,6 +52,8 @@ Raw data types. Int, Char, Bool are unboxed.
> show TyData = "Data"
> show (TyCType s) = "CType " ++ s
> show TyFun = "Fun"
+> show (TyLin s) = "Linear(" ++ show s ++ ")"
+> show (TyEval s) = "Eval(" ++ show s ++ ")"
> data Const = MkInt Int
> | MkBigInt Integer
View
4 Epic/Lexer.lhs
@@ -64,6 +64,8 @@
> | TokenAnyType
> | TokenDataType
> | TokenTyCType
+> | TokenTyLinear
+> | TokenTyEval
> | TokenFunType
> | TokenForeign
> | TokenCInclude
@@ -248,6 +250,8 @@
> ("Unit",rest) -> cont TokenUnitType rest
> ("Data",rest) -> cont TokenDataType rest
> ("CType",rest) -> cont TokenTyCType rest
+> ("Linear",rest) -> cont TokenTyLinear rest
+> ("Eval",rest) -> cont TokenTyEval rest
> ("Fun",rest) -> cont TokenFunType rest
> ("Any",rest) -> cont TokenAnyType rest
> -- values
View
4 Epic/Parser.y
@@ -41,6 +41,8 @@ import Epic.Lexer
funtype { TokenFunType }
datatype { TokenDataType }
tyctype { TokenTyCType }
+ tylinear { TokenTyLinear }
+ tyeval { TokenTyEval }
anytype { TokenAnyType }
unit { TokenUnit }
con { TokenCon }
@@ -147,6 +149,8 @@ Type : inttype { TyInt }
| anytype { TyAny }
| datatype { TyData }
| tyctype string { TyCType $2 }
+ | tylinear '(' Type ')' { TyLin $3 }
+ | tyeval '(' Type ')' { TyEval $3 }
| funtype { TyFun }
Declaration :: { Decl }
View
0  main/Main.lhs → Main.lhs
File renamed without changes
View
36 Papers/Epic-TFP/Makefile
@@ -0,0 +1,36 @@
+PAPER = epic
+
+all: ${PAPER}.pdf
+
+TEXFILES = ${PAPER}.tex intro.tex language.tex example.tex \
+ implementation.tex performance.tex conclusions.tex bigexample.tex
+
+DIAGS =
+
+SOURCES = ${TEXFILES} ${DIAGS} macros.ltx literature.bib
+
+DITAA = java -jar ~/Downloads/ditaa.jar
+
+${PAPER}.pdf: ${SOURCES}
+# dvipdf ${PAPER}.dvi
+ pdflatex ${PAPER}
+ -bibtex ${PAPER}
+ -pdflatex ${PAPER}
+ -pdflatex ${PAPER}
+
+${PAPER}.ps: ${PAPER}.dvi
+ dvips -o ${PAPER}.ps ${PAPER}
+
+${PAPER}.dvi: $(SOURCES)
+ -latex ${PAPER}
+ -bibtex ${PAPER}
+ -latex ${PAPER}
+ -latex ${PAPER}
+
+progress: .PHONY
+ wc -w ${TEXFILES}
+
+%.png : %.diag
+ $(DITAA) -o -E $<
+
+.PHONY:
View
394 Papers/Epic-TFP/bigexample.tex
@@ -0,0 +1,394 @@
+\section{Atuin --- A Dynamically Typed Graphics Language}
+
+In this section we present a more detailed example language,
+Atuin\footnote{\url{http://hackage.haskell.org/package/atuin}}, and
+outline how to use Epic to implement a compiler for it. Atuin is a simple
+imperative language with higher order procedures and dynamic type
+checking, with primitive operations implementing turtle graphics.
+The following example illustrates the basic features of the
+language. The procedure \texttt{repeat} executes a code block a given
+number of times:
+
+\begin{SaveVerbatim}{turtleex1}
+
+repeat(num, block) {
+ if num > 0 {
+ eval block
+ repeat(num-1, block)
+ }
+}
+
+\end{SaveVerbatim}
+\begin{SaveVerbatim}{turtleex2}
+
+polygon(sides, size, col) {
+ if sides > 2 {
+ colour col
+ angle = 360/sides
+ repeat(sides, {
+ forward size
+ right angle
+ })
+ }
+}
+
+\end{SaveVerbatim}
+
+\useverb{turtleex1}
+
+\noindent
+Using \texttt{repeat}, \texttt{polygon} draws a polygon
+with the given number of sides, a size and a colour:
+
+\useverb{turtleex2}
+
+\noindent
+Programs consist of a number of procedure definitions, one of which
+must be called \texttt{main} and take no arguments:
+
+\begin{SaveVerbatim}{atuinmain}
+
+main() {
+ polygon(10,25,red)
+}
+
+\end{SaveVerbatim}
+\useverb{atuinmain}
+
+\subsection{Abstract Syntax}
+
+In this section we discuss the abstract syntax of Atuin, as algebraic
+data types constructed by a Happy-generated parser. Constants can be
+one of four types: integers, characters, booleans and colours:
+
+\begin{SaveVerbatim}{consts}
+
+data Const = MkInt Int
+ | MkChar Char
+ | MkBool Bool
+ | MkCol Colour
+
+data Colour = Black | Red | Green | Blue | ...
+
+\end{SaveVerbatim}
+\useverb{consts}
+
+\noindent
+Atuin is an imperative language, consisting of sequences of commands
+applied to expressions, therefore we define expressions (\texttt{Exp})
+and procedures (\texttt{Turtle}) mutually. Expressions can be constants
+or variables, and combined by infix operators. Additionally, we have
+code blocks in expressions to pass to higher order procedures.
+
+\begin{SaveVerbatim}{expr}
+
+data Exp = Infix Op Exp Exp
+ | Var Id
+ | Const Const
+ | Block Turtle
+
+data Op = Plus | Minus | Times | Divide | ...
+
+\end{SaveVerbatim}
+\useverb{expr}
+
+\noindent
+Procedures define sequences of potentially side-effecting turtle
+operations. There can be procedure calls, turtle commands, and some
+simple control structures. \texttt{Pass} defines an empty code block:
+
+\begin{SaveVerbatim}{turtle}
+
+data Turtle = Call Id [Exp]
+ | Turtle Command
+ | Seq Turtle Turtle
+ | If Exp Turtle Turtle
+ | Let Id Exp Turtle
+ | Eval Exp
+ | Pass
+
+\end{SaveVerbatim}
+\useverb{turtle}
+
+\noindent
+The turtle can be moved forward, turned left or right, or given a
+different pen colour. The pen can also be raised, to allow the turtle
+to move without drawing.
+
+\begin{SaveVerbatim}{turtlecmd}
+
+data Command = Fd Exp | RightT Exp | LeftT Exp
+ | Colour Exp | PenUp | PenDown
+
+\end{SaveVerbatim}
+\useverb{turtlecmd}
+
+\noindent
+As with the $\lambda$-calculus compiler in Section \ref{sec:lc}, a
+complete program consists of a collection of definitions,
+where definitions include a list of formal parameters and the
+program definition:
+
+\begin{SaveVerbatim}{atuinprog}
+
+type Proc = ([Id], Turtle)
+type Defs = [(Id, Proc)]
+
+\end{SaveVerbatim}
+\useverb{atuinprog}
+
+\subsection{Compiling}
+
+While Atuin is a different kind of language from the
+$\lambda$-calculus, with complicating factors such as a global state
+(the turtle). imperative features, and dynamic type checking, the
+process of constructing a compiler follows the same general recipe, i.e.
+define primitive operations as Epic functions, then convert each Atuin
+definition into the corresponding Epic definition.
+
+\subsubsection{Compiling Primitives}
+
+The first step in defining a compiler for Atuin is to define primitive
+operations as Epic functions.
+The language is dynamically
+typed, therefore we will need primitive operations to check that they
+are operating on the correct types. We define functions which
+construct Epic code for
+building values, effectively using a single algebraic datatype to
+capture all possible run-time values (i.e. values are
+``uni-typed''~\cite{wadlerblame}).
+
+\begin{SaveVerbatim}{valadt}
+
+mkint i = con_ 0 @@ i
+mkchar c = con_ 1 @@ c
+mkbool b = con_ 2 @@ b
+mkcol c = con_ 3 @@ c
+
+\end{SaveVerbatim}
+\useverb{valadt}
+
+\noindent
+Correspondingly, we can extract the concrete values safely from this
+structure, checking that the value is the required type:
+
+\begin{SaveVerbatim}{epicgetval}
+
+getInt x = case_ x
+ [con 0 (\ (x :: Expr) -> x),
+ defaultcase (error_ "Not an Int")]
+
+\end{SaveVerbatim}
+\useverb{epicgetval}
+
+\noindent
+Similarly, \texttt{getChar}, \texttt{getBool} and \texttt{getCol}
+check and extract values of the appropriate type.
+Using these, it is simple to define primitve arithmetic operations
+which check they are operating on the correct type, and report an
+error if not.
+
+\begin{SaveVerbatim}{primops}
+
+primPlus x y = mkint $ op_ plus_ (getInt x) (getInt y)
+primMinus x y = mkint $ op_ minus_ (getInt x) (getInt y)
+primTimes x y = mkint $ op_ times_ (getInt x) (getInt y)
+primDivide x y = mkint $ op_ divide_ (getInt x) (getInt y)
+
+\end{SaveVerbatim}
+\useverb{primops}
+
+\subsubsection{Graphics Operations}
+
+We use the Simple DirectMedia Layer\footnote{\url{http://libsdl.org/}}
+(SDL) to implement graphics operations. We implement C functions to
+interact with SDL, and use Epic's foreign function interface to
+call these functions. For example:
+
+\begin{SaveVerbatim}{sdlglue}
+
+void* startSDL(int x, int y);
+void drawLine(void* surf,
+ int x, int y, int ex, int ey,
+ int r, int g, int b, int a);
+
+\end{SaveVerbatim}
+\useverb{sdlglue}
+
+\noindent
+The \texttt{startSDL} function opens a window with the given
+dimensions, and returns a pointer to a \emph{surface}, on which we can
+draw; \texttt{drawLine} draws a line on a surface, between the given
+locations, and in the given colour, specified as red, green, blue and
+alpha channels.
+
+We represent colours as a 4-tuple $(\vr,\vg,\vb,\va)$. Drawing a line
+in Epic involves extracting the red, green, blue and alpha components
+from this tuple, then calling the C \texttt{drawLine} function. Recall
+that to make a foreign function call, we give the types of each
+argument explicitly so that Epic will know how to convert from
+internal values to C values:
+
+\begin{SaveVerbatim}{drawline}
+
+drawLine :: Expr -> Expr -> Expr ->
+ Expr -> Expr -> Expr -> Term
+drawLine surf x y ex ey col
+ = case_ (rgba col)
+ [tuple (\ r g b a ->
+ foreign_ tyUnit "drawLine"
+ [(surf, tyPtr),
+ (x, tyInt), (y, tyInt), (ex, tyInt), (ey, tyInt),
+ (r, tyInt), (g, tyInt), (b, tyInt), (a, tyInt)]) ]
+
+\end{SaveVerbatim}
+\useverb{drawline}
+
+When we compile Atuin programs, we treat the turtle state as a tuple
+$(\vs,\vx,\vy,\vd,\vc,\vp)$ where $\vs$ is a pointer to the SDL
+surface, $\vx$ and $\vy$ give the turtle's location, $\vd$ gives the
+turtle's direction, $\vc$ gives the colour and $\vp$ gives the pen
+state (a boolean, false for up and true for down). Note that this
+state is not accessible by the programmer, so we do not need any
+dynamic type checking of each component.
+
+To implement the \texttt{forward} operation, for example, we take the
+current turtle state, update the position according to the distance
+given and the current direction, and if the pen us down, draws a line
+from the old position to the new position.
+
+\begin{SaveVerbatim}{drawfwd}
+
+forward :: Expr -> Expr -> Term
+forward st dist = case_ st
+ [tuple (\ (surf :: Expr) (x :: Expr) (y :: Expr)
+ (dir :: Expr) (col :: Expr) (pen :: Expr) ->
+ let_ (op_ plus_ x (op_ times_ (getInt dist) (esin dir)))
+ (\x' -> let_ (op_ plus_ y (op_ timesF_ (getInt dist) (ecos dir)))
+ (\y' -> if_ pen (fn "drawLine" @@ surf @@ x @@ y
+ @@ x' @@ y' @@ col) unit_ +>
+ tuple_ @@ surf @@ x' @@ y' @@ dir @@ col @@ pen)))]
+
+\end{SaveVerbatim}
+\useverb{drawfwd}
+
+\noindent
+Note that there is a distinction between Epic code fragments, and Epic
+functions. We have used \texttt{getInt}, \texttt{esin} and
+\texttt{ecos} as inline Haskell functions, using Haskell application,
+but \texttt{drawLine} is applied as a separately defined Epic
+function, using Epic's application operator (\texttt{@@}).
+
+\subsubsection{Compiling Programs}
+
+Programs return an updated turtle state, and possibly perform some
+side-effects such as drawing. We can think of Atuin definitions with
+arguments $\va_1$ to $\va_n$ as being translated to an Epic function
+with a type of the following form:
+
+\DM{
+\vf \Hab \VV{State} \to \va_1 \to \ldots \to \va_n \to \VV{State}
+}
+
+To compile a complete program, we add the primitive functions we have
+defined above (line drawing, turtle movement, etc) to the list of
+basic Epic definitions, and convert the user defined procedures to Epic.
+
+\begin{SaveVerbatim}{prims}
+
+prims = basic_defs ++
+ [EpicFn (name "initSDL") initSDL,
+ EpicFn (name "drawLine") drawLine,
+ EpicFn (name "forward") forward, ... ]
+
+\end{SaveVerbatim}
+\useverb{prims}
+
+\noindent
+We will need to convert expressions, commands and full programs into
+Epic terms, so define a type class to capture all of these. Programs
+maintain the turtle's state (an Epic \texttt{Expr}), and return a new
+state, so we pass this state to the compiler.
+
+\begin{SaveVerbatim}{compileclass}
+
+class Compile a where
+ compile :: Expr -> a -> Term
+
+\end{SaveVerbatim}
+\useverb{compileclass}
+
+In general, since we have set up all of the primitive operations as
+Epic functions, compiling an Atuin program consists of directly
+translating the abstract syntax to the Epic equivalent, making sure
+the state is maintained. For example, to compile a call, we
+build an Epic function call and add the current state as the first
+argument. Epic takes strings as identifiers, so we use \texttt{fullId
+ :: Id -> String} to convert an Atuin identifier to an Epic identifier.
+
+\begin{SaveVerbatim}{compfn}
+
+compile state (Call i es)
+ = app (fn fullId i) @@ state) es
+ where app f [] = f
+ app f (e:es) = app (f @@ compile state e) es
+
+\end{SaveVerbatim}
+\useverb{compfn}
+
+\noindent
+Where operations are sequenced, we make sure that the state returned
+by the first operation is passed to the next:
+
+\begin{SaveVerbatim}{compseq}
+
+compile state (Seq x y)
+ = let_ (compile state x) (\state' -> compile state' y)
+
+\end{SaveVerbatim}
+\useverb{compseq}
+
+Atuin has higher order procedures which accept code blocks as
+arguments. To compile a code block, we simply create a function which
+takes the turtle state (that is, the state at the time the block is
+executed, not the state at the time the block is created). Then when
+it is time to evaluate the block, we pass in the current state. Epic's
+\texttt{effect\_} function ensures that a closure is evaluated, but
+the result is not updated as evaluating the closure may have side
+effects which may need to be executed again --- consider the
+\texttt{repeat} function above, for example, where the code block
+should be evaluated on each iteration.
+
+\begin{SaveVerbatim}{blockeval}
+
+compile state (Block t) = lazy_ (\st -> compile st t)
+compile state (Eval e) = effect_ (compile state e @@ state)
+
+\end{SaveVerbatim}
+\useverb{blockeval}
+
+\noindent
+The rest of the operations are compiled by a direct mapping to the
+primitives defined earlier. Finally, the main program sets up an SDL
+surface, creates an initial turtle state, and passes that state to the
+user defined \texttt{main} function:
+
+\begin{SaveVerbatim}{runmain}
+
+init_turtle surf = tuple_ @@ surf @@
+ int 320 @@ int 240 @@ int 180 @@
+ col_white @@ bool True
+
+runMain :: Term
+runMain = let_ (fn "initSDL" @@ int 640 @@ int 480)
+ (\surface ->
+ (fn (fullId (mkId "main")) @@ (init_turtle surface)) +>
+ flipBuffers surface +> pressAnyKey)
+
+\end{SaveVerbatim}
+\useverb{runmain}
+
+The full source code for Atuin and its compiler is available from
+Hackage (\url{http://hackage.haskell.org/package/atuin}), which
+covers the remaining technical details of linking compiled programs
+with SDL.
View
29 Papers/Epic-TFP/comments.sty
@@ -0,0 +1,29 @@
+% $id$
+% KH: created comments style file to allow alternative versions of a document.
+
+% \newcommand{\red}[1]{#1}
+
+\usepackage{color}
+\definecolor{BrickRed}{cmyk}{0, .89, .5, 0}
+\newcommand{\red}{\color{BrickRed}}
+
+\newcommand{\eucommentary}[1]{\(\spadesuit\){\red{\textbf{EC Commentary}: \emph{#1}}\(\spadesuit\)}}
+\newcommand{\euevaluation}[2]{\(\spadesuit\){\red{\textbf{Evaluation Criteria ({#1})}: \emph{#2}}\(\spadesuit\)}}
+
+\newcommand{\comment}[2]{\(\spadesuit\){\bf #1: }{\rm \sf #2}\(\spadesuit\)}
+\newcommand{\draftpage}{\newpage}
+
+\newcommand{\FIXME}[1]{[\textbf{FIXME}: #1]}
+
+%\newcommand{\FIXME}[1]{\wibble}
+\newcommand{\nocomments}{
+\renewcommand{\eucommentary}[1]{}
+\renewcommand{\euevaluation}[2]{}
+\renewcommand{\comment}[2]{}
+\renewcommand{\draftpage}{}
+\renewcommand{\FIXME}[1]{}
+}
+
+\DeclareOption{final}{\nocomments}
+\DeclareOption{draft}{}
+\ProcessOptions*
View
58 Papers/Epic-TFP/conclusions.tex
@@ -0,0 +1,58 @@
+\section{Related Work}
+
+%% GHC's run-time system~\cite{stg, evalpush}, ABC
+%% machine~\cite{abc-machine} and why we don't just use one of them
+%% (no useful interface, imposes constraints on the type system).
+%% Some influence from GRIN~\cite{grin-project}.
+
+Epic is currently used by Agda and Idris~\cite{plpv11}, as well as the
+development version of Epigram~\cite{levitation}. Initial
+benchmarking~\cite{scrap-engine} shows that the code generated by Epic
+can be competitive with Java and is not significantly worse than C.
+Epic uses techniques from other functional language back
+ends~\cite{evalpush,stg,abc-machine} but deliberately exposes its core
+language as an API to make it as reusable as possible. Although there
+is likely to always be a trade off between reusability and efficiency,
+exposing the API will make it easier for other language researchers to
+build a new compiler quickly. The Lazy Virtual Machine~\cite{lvm} has
+similar goals but it designed as a lower level target language, rather
+than a high level API.
+
+%C--~\cite{c--} and LLVM~\cite{llvm}
+%as possible code generation strategies. Supercompilation for
+%optimisations~\cite{mitchell-super}.
+
+\section{Conclusion}
+
+Epic provides a simple path for language researchers to convert
+experimental languages (e.g. experimenting with new type systems or
+domain specific language design) into larger scale, usable tools, by
+providing an API for generating a compiler, dealing with
+well-understood but difficult to implement problems such as lambda
+lifting, code generation, interfacing with foreign functions and
+garbage collection.
+
+In this paper we have seen two examples of languages which can be
+compiled via Epic, both functionally based, but with different
+features. The high-level recipe for each is the same: define primitive
+functions as run-time support, then translate the abstract syntax into
+concrete Epic functions, using a combinator style API.
+
+\subsubsection{Future work}
+
+Epic is currently used in practice by a dependently typed functional
+language, Idris~\cite{idris-plpv}, and experimentally by
+Agda~\cite{norell-thesis} and Epigram~\cite{levitation}. Future work
+will therefore have an emphasis on providing an efficient executable
+environment for these and related languages. An interesting research
+question, for example, is whether the rich type systems of these languages
+can be used to guide optimisation, and if so how to present the
+information gained by the type system to the compiler.
+
+Currently, Epic compiles to machine code via C, using the Boehm
+conservative garbage collector~\cite{boehm-gc}. While this has been
+reasonably efficient in practice, we believe that an LLVM based
+implementation~\cite{llvm,llvm-haskell} with accurate garbage
+collection would be more appropriate. Of course, any language which
+uses Epic as a back end will stand to gain from future optimisation
+efforts!
View
151 Papers/Epic-TFP/dtp.bib
@@ -0,0 +1,151 @@
+@phdthesis{ brady-thesis,
+ author = {Edwin Brady},
+ title = {Practical Implementation of a Dependently Typed Functional Programming Language},
+ year = 2005,
+ school = {University of Durham}
+}
+
+@article{view-left,
+ journal = {Journal of Functional Programming},
+ number = {1},
+ volume = {14},
+ title = {The View From The Left},
+ year = {2004},
+ author = {Conor McBride and James McKinna},
+ pages = {69--111}
+}
+
+@misc{epigram-afp,
+ author = {Conor McBride},
+ title = {Epigram: Practical Programming with Dependent Types},
+ year = {2004},
+ howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
+}
+
+@misc{coq-manual,
+ howpublished = {\verb+http://coq.inria.fr/+},
+ title = {The {Coq} Proof Assistant --- Reference Manual},
+ year = {2004},
+ author = {{Coq Development Team}}
+}
+
+@inproceedings{extraction-coq,
+ title = {A New Extraction for {Coq}},
+ year = {2002},
+ booktitle = {Types for proofs and programs},
+ editor = {Herman Geuvers and Freek Wiedijk},
+ publisher = {Springer},
+ author = {Pierre Letouzey},
+ series = {LNCS}
+}
+
+@techreport{lego-manual,
+ title = {\textsc{Lego} Proof Development System: User's Manual},
+ year = {1992},
+ institution = {Department of Computer Science, University of Edinburgh},
+ author = {Zhaohui Luo and Robert Pollack}
+}
+
+@book{luo94,
+ title = {Computation and Reasoning -- A Type Theory for Computer Science},
+ year = {1994},
+ publisher = {OUP},
+ author = {Zhaohui Luo},
+ series = {International Series of Monographs on Computer Science}
+}
+
+@phdthesis{goguen-thesis,
+ school = {University of Edinburgh},
+ title = {A Typed Operational Semantics for Type Theory},
+ year = {1994},
+ author = {Healfdene Goguen}
+}
+
+@phdthesis{mcbride-thesis,
+ month = {May},
+ school = {University of Edinburgh},
+ title = {Dependently Typed Functional Programs and their proofs},
+ year = {2000},
+ author = {Conor McBride}
+}
+
+@misc{mckinnabrady-phase,
+ title = {Phase Distinctions in the Compilation of {Epigram}},
+ year = 2005,
+ author = {James McKinna and Edwin Brady},
+ note = {Draft}
+}
+
+@article{pugh-omega,
+ title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
+ author = "William Pugh",
+ journal = "Communication of the ACM",
+ year = 1992,
+ pages = {102--114}
+}
+
+@Article{RegionTypes,
+ refkey = "C1753",
+ title = "Region-Based Memory Management",
+ author = "M. Tofte and J.-P. Talpin",
+ pages = "109--176",
+ journal = "Information and Computation",
+ month = "1~" # feb,
+ year = "1997",
+ volume = "132",
+ number = "2"
+}
+
+@phdthesis{ pedro-thesis,
+ author = {Pedro Vasconcelos},
+ title = {Space Cost Modelling for Concurrent Resource Sensitive Systems},
+ year = 2006,
+ school = {University of St Andrews}
+}
+
+@book{curry-feys,
+ title = {Combinatory Logic, volume 1},
+ year = {1958},
+ publisher = {North Holland},
+ author = {Haskell B. Curry and Robert Feys}
+}
+@inproceedings{howard,
+ title = {The formulae-as-types notion of construction},
+ year = {1980},
+ booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
+ editor = {Jonathan P. Seldin and J. Roger Hindley},
+ publisher = {Academic Press},
+ author = {William A. Howard},
+ note = {A reprint of an unpublished manuscript from 1969}
+}
+
+@misc{ydtm,
+ author = {Thorsten Altenkirch and Conor McBride and James McKinna},
+ title = {Why Dependent Types Matter},
+ note = {Submitted for publication},
+ year = 2005}
+
+@inproceedings{regular-types,
+ author = { Peter Morris and Conor McBride and Thorsten Altenkirch},
+ title = {Exploring The Regular Tree Types},
+ year = 2005,
+ booktitle = {Types for Proofs and Programs 2004}
+}
+
+@inproceedings{xi_arraybounds,
+author = "Hongwei Xi and Frank Pfenning",
+title = {Eliminating Array Bound Checking through Dependent Types},
+booktitle = "Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation",
+year = 1998,
+month = "June",
+address = "Montreal",
+pages = "249--257",
+}
+
+@misc{interp-cayenne,
+ url = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
+ title = {An exercise in dependent types: A well-typed interpreter},
+ year = {1999},
+ author = {Lennart Augustsson and Magnus Carlsson}
+}
+
View
279 Papers/Epic-TFP/embounded.bib
@@ -0,0 +1,279 @@
+@Book{BurnsWellings,
+author = {A. Burns and A.J. Wellings},
+title = {{Real-Time Systems and Programming Languages (Third Edition)}},
+publisher = {Addison Wesley Longman},
+year = 2001
+}
+
+@Book{Ganssle:Book,
+author = {J.G. Ganssle},
+title = {{The Art of Programming Embedded Systems}},
+publisher = {Academic Press},
+year = {1992},
+note = {ISBN 0-12274880-8},
+}
+
+@Book{Ganssle:Design,
+author = {J.G. Ganssle},
+title = {{The Art of Designing Embedded Systems}},
+publisher = {Newnes},
+year = {1999},
+note = {ISBN 0-75069869-1},
+}
+
+@article{Ganssle:OnLanguage,
+author = {J.G. Ganssle},
+title = {{On Language}},
+journal ={{Electronic Eng. Times}},
+month = "March",
+year = {2003}
+}
+
+@article{Ganssle:MicroMinis,
+author = {J.G. Ganssle},
+title = {{Micro Minis}},
+journal ={{Embedded Systems Programming}},
+month = "March",
+year = {2003}
+}
+
+@article{Barr:EmbeddedSystProg,
+author = {M. Barr},
+title = {{The Long Winter}},
+journal ={{Electronic Systems Programming}},
+month = "January",
+year = {2003}
+}
+
+@unpublished{Ganssle:WebSite,
+author = {The Ganssle Group},
+title = {{Perfecting the Art of Building Embedded Systems}},
+month = "May",
+year = 2003,
+note = {\url{http://www.ganssle.com}}
+}
+
+@article{Schoitsch,
+author = {E. Schoitsch},
+title = {{Embedded Systems -- Introduction}},
+journal = {ERCIM News},
+pages = {10--11},
+volume = 52,
+month = jan,
+year = 2003
+}
+
+@article{UMLESE,
+author = {C. Holland},
+title = {{Telelogic Second Generation Tools}},
+journal = {Embedded Systems Europe},
+month = aug,
+year = 2002
+}
+
+@article{DSL,
+author = {P. Hudak},
+title = {{Building Domain-Specific Embedded Languages}},
+journal = {ACM Computing Surveys},
+volume = 28,
+number = 4,
+month = dec,
+year = 1996
+}
+
+@article{DSL:devicedriver,
+author = {C. Conway},
+title = {{A Domain-Specific Language for Device Drivers}},
+journal = {ACM Computing Surveys},
+volume = 28,
+number = 4,
+month = dec,
+year = 1996
+}
+
+@unpublished{Klocwork,
+author = {Klocwork},
+year = 2003,
+}
+
+@inproceedings{Bernat1,
+author = {Bernat, G. and Burns, A. and Wellings, A.},
+title = {{Portable Worst-Case Execution Time Analysis Using Java Byte Code}},
+booktitle = {Proc. 12th Euromicro International Conf. on
+ Real-Time Systems},
+address = {Stockholm},
+year = 2000,
+month = {June}
+}
+
+@inproceedings{Bernat2,
+author = {Bernat, G. and Colin, A. and Petters, S. M.},
+title = {{WCET Analysis of Probabilistic Hard Real-Time Systems}},
+booktitle = {Proc. 23rd IEEE Real-Time Systems Symposium (RTSS 2002)},
+address = {Austin, TX. (USA)},
+year = 2002,
+month = {December}
+}
+
+@inproceedings{SizedRecursion,
+author = {P. Vasconcelos and K. Hammond},
+title = {{Inferring Costs for Recursive, Polymorphic and Higher-Order Functions}},
+booktitle = {Proc. Implementation of Functional Languages (IFL 2003)},
+publisher = {Springer-Verlag},
+year = {2003}
+}
+
+@inproceedings{HAM,
+author = {K. Hammond and G.J. Michaelson},
+title = {{An Abstract Machine Implementation for Hume}},
+booktitle = {submitted to Intl. Conf. on Compilers, Architectures and Synthesis for Embedded Systems (CASES~03)},
+year = {2003}
+}
+
+@unpublished{EmbeddedSystSurvey,
+author = {Embedded.com},
+title = {Poll: What Language do you use for embedded work?},
+note = {\url{http://www.embedded.com/pollArchive/?surveyno=2228}},
+year = 2003,
+}
+
+@inproceedings{ESP,
+author = {S. Kumar and K. Li},
+title = {Automatic Memory Management for Programmable Devices},
+booktitle = {Proc. ACM Intl. Symp. on Memory Management, Berlin, Germany},
+month = jun,
+year = 2002,
+pages = {245--255},
+}
+
+@inproceedings{RegionJava,
+author = {F. Qian and L. Hendrie},
+title = {An Adaptive Region-Based Allocator for Java},
+booktitle = {Proc. ACM Intl. Symp. on Memory Management, Berlin, Germany},
+month = jun,
+year = 2002,
+pages = {233--244},
+}
+
+@inproceedings{RegionsRTSJ,
+author = {M. Deters and R.K. Cytron},
+title = {Automated Discovery of Scoped Memory Regions for Real-Time Java},
+booktitle = {Proc. ACM Intl. Symp. on Memory Management, Berlin, Germany},
+month = jun,
+year = 2002,
+pages = {132--141},
+}
+
+@inproceedings{RTGC,
+author = {S. Nettles and J. O'Toole},
+title = {{Real-Time Replication Garbage Collection}},
+booktitle = {ACM Sigplan Notices},
+volume = 28,
+number = 6,
+month = jun,
+year = 1993,
+pages = {217--226},
+}
+
+@inproceedings{Blelloch,
+author = {P. Cheng and G. Blelloch},
+title = {{A Parallel, Real-Time Garbage Collector}},
+booktitle = {ACM Sigplan Notices},
+volume = 36,
+number = 5,
+month = may,
+year = 2001,
+pages = {125--136},
+}
+
+@inproceedings{RegionsGC,
+author = {N. Hallenberg and M. Elsman and M. Tofte},
+title = {{Combining Region Inference and Garbage Collection}},
+booktitle = {Proc. ACM Conf. on Prog. Lang. Design and Impl. (PLDI~'02), Berlin, Germany},
+month = jun,
+year = 2002,
+}
+
+
+@article{RTSJIssues,
+author = {K. Nilsen},
+title = {{Issues in the Design and Implementation of Real-Time Java}},
+booktitle = {Java Developers' Journal},
+volume = 1,
+number = 1,
+year = 1996,
+pages = 44
+}
+
+
+
+@unpublished{CyCab,
+author = {RoboSoft SA},
+title = {{CyCab Outdoor Vehicle, for Road and/or All-terrain Use}},
+note = {\url{http://www.robosoft.fr/SHEET/01Mobil/2001Cycab/CyCab.html}},
+year = 2003,
+month = may
+}
+
+
+@unpublished{Joyner,
+author = {I. Joyner},
+title = {{C++??: a Critique of C++, 3rd Edition}},
+year = 1996,
+institution = {Unisys - ACUS, Australia},
+note = {\url{http://www.kcl.ac.uk/kis/support/cit//fortran/cpp/cppcritique.ps}}
+}
+
+@unpublished{Sakkinen,
+author = {M. Sakkinen},
+title = {{The Darker Side of C++ Revisited}},
+year = 1993,
+institution = {Univerity of Jyv\"{a}skyl\"{a}},
+note = {Technical Report 1993-I-13, \url{http://www.kcl.ac.uk/kis/support/cit//fortran/cpp/dark-cpl.ps}},
+}
+
+@TechReport{BCLogicDelvb,
+ author = {Hans-Wolfgang Loidl and Olha Shkaravska and Lennart Beringer},
+ title = {Preliminary investigations into a bytecode logic for Grail},
+ institution = {Institut f{\"u}r Informatik, LMU University and LFCS, Edinburgh University},
+ year = 2003,
+ month = jan,
+ note = {Project Deliverable}
+}
+
+@InProceedings{HWLtofillin,
+ author = {Lennart Beringer and Kenneth MacKenzie and Ian Stark},
+ title = {Grail: a functional form for imperative mobile code},
+ booktitle = {FGC03 --- Workshop on Foundations of Global Computing},
+ year = 2003,
+ address = {28--29 June 2003, Eindhoven, The Netherlands},
+ note = {Submitted}
+}
+
+
+@inproceedings{AbsInt:EmsoftTahoe,
+ author = "C. Ferdinand and R. Heckmann and M. Langenbach and
+ F. Martin and M. Schmidt and
+ H. Theiling and S. Thesing and R. Wilhelm",
+ title = {Reliable and Precise {WCET} Determination for a Real-Life Processor},
+ booktitle = {Proc. EMSOFT 2001, First Workshop on Embedded Software},
+ publisher = {Springer-Verlag},
+ series = {LNCS},
+ volume = 2211,
+ pages = {469--485},
+ year = 2001
+}
+
+
+@inproceedings{AbsInt:Avionics,
+ author = "S. Thesing and J. Souyris and R. Heckmann and
+ F. Randimbivololona and M. Langenbach and
+ R. Wilhelm and C. Ferdinand",
+ title = {An Abstract Interpretation-Based Timing Validation
+ of Hard Real-Time Avionics Software},
+ booktitle = {Proc. 2003 Intl. Conf.
+ on Dependable Systems and Networks (DSN 2003)},
+ pages = {625--632},
+ year = 2003
+}
+
View
110 Papers/Epic-TFP/epic.tex
@@ -0,0 +1,110 @@
+%\documentclass{llncs}
+\documentclass[orivec,dvips,10pt]{llncs}
+
+\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{amsmath,amssymb}
+\usepackage{fancyvrb}
+
+\newenvironment{template}{\sffamily}
+
+\usepackage{graphics,epsfig}
+\usepackage{stmaryrd}
+
+\input{./macros.ltx}
+\input{./library.ltx}
+
+\NatPackage
+\FinPackage
+
+\newcounter{per}
+\setcounter{per}{1}
+
+\newcommand{\Ivor}{\textsc{Ivor}}
+\newcommand{\Idris}{\textsc{Idris}}
+\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}}
+
+\begin{document}
+
+\title{Epic --- A Library for Generating Compilers\\(Research Paper)}
+\author{Edwin Brady}
+
+\institute{University of St Andrews, KY16 9SX, Scotland/UK,\\
+\email{eb@cs.st-andrews.ac.uk}}
+
+\maketitle
+
+\begin{abstract}
+Compilers for functional languages, whether strict or non-strict,
+typed or untyped, need to handle many of the same problems, for
+example thunks, lambda lifting, optimisation, garbage collection, and
+system interaction. Although implementation techniques are by now
+well understood, it remains difficult for a new functional language to
+exploit these techniques without either implementing a compiler from
+scratch, or attempting fit the new language around another existing
+compiler.
+Epic is a compiled functional language which exposes functional
+compilation techniques to a language implementor, with a Haskell
+API. In this paper we describe Epic and outline how it may
+be used to implement a high level language compiler, illustrating our
+approach using a dynamically typed graphics language.
+
+\end{abstract}
+
+\input{intro}
+
+\input{language}
+
+\input{example}
+
+\input{bigexample}
+
+%\input{implementation}
+
+%\input{performance}
+
+\input{conclusions}
+
+%\vspace{-0.2in}
+%% \section*{Acknowledgments}
+
+%% This work was partly funded by the Scottish Informatics and Computer
+%% Science Alliance (SICSA) and by EU Framework 7 Project No. 248828
+%% (ADVANCE). I thanks James McKinna, Kevin Hammond and Anil
+%% Madhavapeddy for several helpful discussions, and the anonymous
+%% reviewers for their constructive suggestions.
+
+\bibliographystyle{abbrv}
+\begin{small}
+\bibliography{literature.bib}
+
+\appendix
+
+%\input{code}
+
+\end{small}
+\end{document}
View
205 Papers/Epic-TFP/example.tex
@@ -0,0 +1,205 @@
+\section{Example --- Compiling the $\lambda$-Calculus}
+
+\label{sec:lc}
+
+In this section we present a compiler for a simple high level
+language.
+This is a compiler for the untyped $\lambda$-calculus using Higher Order
+Abstract Syntax, which shows the fundamental features of Epic required
+to implement a complete compiler. We have also implemented compilers
+for \LamPi{}~\cite{simply-easy}, a dependently typed language, which
+shows how Epic can handle languages with more expressive type systems,
+and a dynamically typed graphics language\footnote{\url{http://hackage.haskell.org/package/atuin}}, which shows how Epic can be
+used for languages with run-time type checking and which require
+foreign function calls.
+
+\subsection{Representation}
+
+Our example is an implementation of the untyped
+$\lambda$-calculus, plus primitive integers and strings, and
+arithmetic and string operators. The language is represented in
+Haskell using higher order abstract syntax (HOAS). That is, we
+represent $\lambda$-bindings (\texttt{Lam}) as Haskell functions,
+using a Haskell variable name to refer to the locally bound
+variable. We also include global references (\texttt{Ref}) which refer
+to top level functions, function application (\texttt{App}), constants
+(\texttt{Const}) and binary operators (\texttt{Op}):
+
+\begin{SaveVerbatim}{llang}
+
+data Lang = Lam (Lang -> Lang)
+ | Ref Name
+ | App Lang Lang
+ | Const Const
+ | Op Infix Lang Lang
+
+\end{SaveVerbatim}
+\useverb{llang}
+
+\noindent
+Constants can be either integers or strings:
+
+\begin{SaveVerbatim}{lconsts}
+
+data Const = CInt Int | CStr String
+
+\end{SaveVerbatim}
+\useverb{lconsts}
+
+\noindent
+There are infix operators for arithmetic (\texttt{Plus},
+\texttt{Minus}, \texttt{Times} and \texttt{Divide}), string
+manipulation (\texttt{Append}) and comparison (\texttt{Eq},
+\texttt{Lt} and \texttt{Gt}). The comparison operators return an
+integer --- zero if the comparison is true, non-zero otherwise:
+
+\begin{SaveVerbatim}{lops}
+
+data Infix = Plus | Minus | Times | Divide | Append | Eq | Lt | Gt
+
+\end{SaveVerbatim}
+\useverb{lops}
+
+\noindent
+A complete program consists of a collection of named \texttt{Lang}
+definitions:
+
+\begin{SaveVerbatim}{lprogs}
+
+type Defs = [(Name, Lang)]
+\end{SaveVerbatim}
+\useverb{lprogs}
+
+\subsection{Compilation}
+
+Our aim is to convert a collection of \texttt{Defs} into an
+executable, using the \texttt{compile} or \texttt{run} function from
+the Epic API.
+Given an Epic \texttt{Program}, \texttt{compile} will generate an
+executable, and \texttt{run} will generate an executable then run it.
+Recall that a program is a collection of named Epic declarations:
+
+\begin{SaveVerbatim}{eprogs}
+
+data EpicDecl = forall e. EpicExpr e => EpicFn Name e
+ | ...
+
+type Program = [EpicDecl]
+
+\end{SaveVerbatim}
+\useverb{eprogs}
+
+\noindent
+Our goal is to convert a \texttt{Lang} definition into
+something which is an instance of \texttt{EpicExpr}. We use
+\texttt{Term}, which is an Epic expression which carries a name
+supply. Most of the term construction functions in the Epic API return
+a \texttt{Term}.
+
+\begin{SaveVerbatim}{buildtype}
+
+build :: Lang -> Term
+
+\end{SaveVerbatim}
+\useverb{buildtype}
+
+\noindent
+The full implementation of \texttt{build} is given in Figure \ref{lcompile}.
+In general, this is a straightforward traversal of the \texttt{Lang}
+program, converting \texttt{Lang} constants to Epic constants,
+\texttt{Lang} application to Epic application, and \texttt{Lang}
+operators to the appropriate built-in Epic operators.
+
+\begin{SaveVerbatim}{lcompile}
+build :: Lang -> Term
+build (Lam f) = term (\x -> build (f (EpicRef x)))
+build (EpicRef x) = term x
+build (Ref n) = ref n
+build (App f a) = build f @@ build a
+build (Const (CInt x)) = int x
+build (Const (CStr x)) = str x
+build (Op Append l r) = fn "append" @@ build l @@ build r
+build (Op op l r) = op_ (eOp op) (build l) (build r)
+ where eOp Plus = plus_
+ eOp Minus = minus_
+ ...
+\end{SaveVerbatim}
+\codefig{lcompile}{Compiling Untyped $\lambda$-calculus}
+
+%\noindent
+The cases worth noting are the compilation of $\lambda$-bindings and
+string concatenation. Using HOAS has the advantage that Haskell can
+manage scoping, but the disadvantage that it is not straightforward to
+convert the abstract syntax into another form. The Epic API also
+allows scope management using HOAS, so we need to convert a function
+where the bound name refers to a \texttt{Lang} value into a function
+where the bound name refers to an Epic value. The easiest solution is
+to extend the \texttt{Lang} datatype with an Epic reference:
+
+\begin{SaveVerbatim}{lextend}
+
+data Lang = ...
+ | EpicRef Expr
+
+build (Lam f) = term (\x -> build (f (EpicRef x)))
+
+\end{SaveVerbatim}
+\useverb{lextend}
+
+\noindent
+To convert a \texttt{Lang} function to an Epic function, we build an
+Epic function in which we apply the \texttt{Lang} function to the Epic
+reference for its argument. Every reference to a name in \texttt{Lang}
+is converted to the equivalent reference to the name in Epic. While
+there may be neater solutions involving an environment, or avoiding
+HOAS, this solution is very simple to implement, and preserves the
+desirable feature that Haskell manages scope.
+Compiling string append uses a built in function provided by the Epic
+interface in \texttt{basic\_defs}:
+
+\begin{SaveVerbatim}{lappend}
+
+build (Op Append l r) = fn "append" @@ build l @@ build r
+
+\end{SaveVerbatim}
+\useverb{lappend}
+
+\noindent
+Given \texttt{build}, we can translate a collection of HOAS
+definitions into an Epic program, add the built-in Epic definitions
+and execute it directly. Recall that there must be a function called
+\texttt{"main"} or Epic will report an error.
+
+\begin{SaveVerbatim}{lmain}
+
+mkProgram :: Defs -> Program
+mkProgram ds = basic_defs ++
+ map (\ (n, d) -> EpicFn n (build d)) ds
+
+execute :: Defs -> IO ()
+execute p = run (mkProgram p)
+
+\end{SaveVerbatim}
+\useverb{lmain}
+
+\noindent
+Alternatively, we can generate an executable. Again, the entry point
+is the Epic function called \texttt{"main"}:
+
+\begin{SaveVerbatim}{lcomp}
+
+comp :: Defs -> IO ()
+comp p = compile "a.out" (mkProgram p)
+
+\end{SaveVerbatim}
+\useverb{lcomp}
+
+\noindent
+This is a compiler for a very simple language, but a compiler for any
+more complex language follows the same pattern: convert the abstract
+syntax for each named definition into a named Epic \texttt{Term}, add
+any required primitives (we have just used \texttt{basic\_defs} here),
+and pass the collection of definitions to \texttt{run} or
+\texttt{compile}.
+
+
View
16 Papers/Epic-TFP/implementation.tex
@@ -0,0 +1,16 @@
+\section{Implementation}
+
+How it's implemented is not really important to the user --- a
+compiler can target Epic without knowing, and we could drop in a new
+back end at any time in principle.
+
+There is currently one back end, but more are planned. Compiled via
+C. Garbage collection with Boehm~\cite{boehm-gc},
+\texttt{\%memory}. (Note that a non-moving collector makes things
+easier for foreign functions, but may not be the best choice in the
+long run).
+
+Later plans: compile via LLVM, allow plug in garbage collectors
+(important for embedded systems, device drivers, operating system
+services, for example).
+
View
40 Papers/Epic-TFP/intro.tex
@@ -0,0 +1,40 @@
+\section{Introduction}
+
+When implementing a new language, whether for research purposes or as
+a realistic general purpose language, we are inevitably faced with the
+problem of executing the language. Ideally, we would like execution to
+be as fast as possible, and exploit known techniques from many years
+of compiler research. However, it is difficult to make use of the
+existing available back ends for functional langauges, such as the
+STG~\cite{evalpush,stg,llvm-haskell} or ABC~\cite{abc-machine}
+machines. They may be too low level, they may make assumptions about
+the source language (e.g. its type system) or there may simply be no
+clearly defined API. As a result, experimental languages such as
+Agda~\cite{norell-thesis} have resorted to generating Haskell, using
+\texttt{unsafeCoerce} to bypass the type system. Similarly,
+Cayenne~\cite{cayenne-icfp} used LML with the type checker switched
+off. This is not ideal for several reasons: we cannot expect to use
+the full power and optimisations of the underlying compiler, nor can
+we expect it to exploit any specific features of our new source
+language, such as the optimisation opportunities presented by rich
+dependent type systems.
+
+Epic aims to provide the necessary features for implementing the
+back-end of a functional language --- thunks, closures, algebraic data
+types, scope management, lambda lifting --- without imposing
+\remph{any} design choices on the high level language designer, with
+the obvious exception that a functional style is encouraged! The
+library provides \remph{compiler combinators}, which guarantee that
+any output code will be syntactically correct and well-scoped. This
+gives a simple method for building a compiler for a new functional
+language, e.g. for experimentation with new type systems or new domain
+specific languages.
+
+Epic was originally written as a back end for
+Epigram~\cite{levitation} (the name\footnote{Coined by James McKinna}
+is short for ``\textbf{Epi}gram \textbf{C}ompiler''). It is now used
+by Idris~\cite{idris-plpv} and as an experimental back end for
+Agda. It is specifically designed for reuse by other source languages.
+
+
+
View
480 Papers/Epic-TFP/language.tex
@@ -0,0 +1,480 @@
+\section{The Epic Language}
+
+Epic is based on the $\lambda$-calculus with some extensions.
+It supports primitives such as strings and integers, as well as tagged
+unions. There are additional control structures for specifying
+evaluation order, primitive loop constructs, and calling foreign
+functions. Foreign function calls are annotated with types, to assist
+with marshaling values between Epic and C, but otherwise there are no
+type annotations and there is no type checking --- as Epic is intended
+as an intermediate language, it is assumed that the high level
+language has already performed any necessary type checking. The
+abstract syntax of the core language is given in Figure \ref{epicsyn}.
+As a shorthand, we use de Bruijn telescope notation, $\tx$, to denote
+a sequence of $\vx$.
+We use $\vx$ to stand for variable names, and $\vi$, $\vb$, $\vf$,
+$\vc$, and $\VV{str}$ to stand for integer, boolean, floating
+point, character and string literals respectively.
+
+\newcommand{\Con}[2]{\DC{Con}\:#1(#2)}
+
+\FFIG{
+\AR{
+\begin{array}{rcllcll}\\
+\vp & ::= & \vec{\VV{def}} & \mbox{(Epic program)} &
+\VV{def} ::= & \vx(\tx) = \vt &
+\mbox{(Definition)} \\
+\\
+\vt & ::= & \vx & \mbox{(Variable)}
+& \mid & \vt(\ttt) & \mbox{(Application)} \\
+& \mid & \lambda\vx\SC\vt & \mbox{(Lambda binding)}
+& \mid & \RW{let}\:\vx\:=\:\vt\:\RW{in}\:\vt & \mbox{(Let
+ binding)} \\
+& \mid & \Con{\vi}{\ttt} & \mbox{(Constructor)}
+& \mid & \vt ! \vi & \mbox{(Projection)} \\
+& \mid & \vt\:\VV{op}\:\vt & \mbox{(Infix operator)}
+& \mid & \RW{if}\:\vt\:\RW{then}\:\vt\:\RW{else}\:\vt & \mbox{(Conditional)}\\
+& \mid & \RW{case}\:\vt\:\RW{of}\:\vec{\VV{alt}} & \mbox{(Case expressions)}
+& \mid & \RW{lazy}(\vt) & \mbox{(Lazy evaluation)} \\
+& \mid & \RW{effect}(\vt) & \mbox{(Effectful term)}
+& \mid & \RW{while}\:\vt\:\vt & \mbox{(While loops)} \\
+& \mid & \vx := \:\vt\:\RW{in}\:\vt & \mbox{(Variable update)}
+& \mid & \RW{foreign}\:\vT\:\VV{str}\:\vec{(\vt\Hab\vT)} & \mbox{(Foreign
+call)} \\
+& \mid & \RW{malloc}\:\vt\:\vt & \mbox{(Allocation)}
+& \mid & \vi \mid \vf \mid \vc \mid \vb \mid \VV{str} & \mbox{(Constants)} \\
+\\
+\VV{alt} & ::= &
+\Con{\vi}{\tx} \cq \vt & \mbox{(Constructors)}
+& \mid & \vi \cq \vt & \mbox{(Constants)} \\
+& \mid & \RW{default} \cq \vt & \mbox{(Match anything)} \\
+\end{array}
+\medskip
+\\
+\begin{array}{rcll}
+\VV{op} & ::= & + \mid - \mid \times \mid / \mid\:
+==\: \mid \:<\: \mid \:\le\: \mid \:>\: \mid \:\ge \: \mid \: << \:
+\mid \: >>\\
+\end{array}
+\medskip
+\\
+\begin{array}{rcll}
+\vT & ::= & \TC{Int} \mid \TC{Char} \mid \TC{Bool} \mid \TC{Float}
+\mid \TC{String} & \mbox{(Primitives)} \\
+ & \mid & \TC{Unit} & \mbox{(Unit type)} \\
+ & \mid & \TC{Ptr} & \mbox{(Foreign pointers)} \\
+% & \mid & \TC{Fun} & \mbox{(Any function type)} \\
+% & \mid & \TC{Data} & \mbox{(Any data type)} \\
+ & \mid & \TC{Any} & \mbox{(Polymorphic type)} \\
+\end{array}
+}
+}
+{Epic syntax}
+{epicsyn}
+
+\subsection{Definitions}
+
+An Epic program consists of a sequence of \remph{untyped} function
+definitions, with zero or more arguments. The entry point is the
+function $\VV{main}$, which takes no arguments. For example:
+
+\DM{
+\begin{array}{ll}
+\VV{factorial}(\vx)&\:=\:
+\RW{if}\:\vx==0\:\AR{\RW{then}\:1\\
+\RW{else}\:\vx\:\times\:\VV{factorial}(\vx-1)}
+\medskip
+\\
+\VV{main}()&\:=\:\VV{putStrLn}(\VV{intToString}(\VV{factorial}(10)))
+\end{array}
+}
+
+\noindent
+The right hand side of a definition is an expression consisting of
+function applications, operators (arithmetic, comparison, and
+bit-shifting), bindings and control structures (some low level and
+imperative). Functions may be partially applied.
+
+\subsubsection*{Values}
+
+Values in an Epic program are either one of the primitives (an
+integer, floating point number, character, boolean or string) or a
+\remph{tagged union}. Tagged unions are of the form $\DC{Con}\:
+\vi(\vt_1,\ldots,\vt_n)$, where $\vi$ is the \remph{tag} and the $\ttt$
+are the \remph{fields}. The name $\DC{Con}$ is to suggest
+``Constructor''. For example, we could represent a list using tagged
+unions, with $\DC{Con}\:0()$ representing the empty list and
+$\DC{Con}\:1(\vx,\:\vxs)$ representing a cons cell, where $\vx$
+is the element and $\vxs$ is the tail of the list.
+
+Tagged unions are inspected either using field projection ($\vt!\vi$
+projects the $\vi$th field from a tagged union $\vt$) or by case
+analysis. e.g., to append two lists:
+
+\DM{
+\AR{
+\VV{append}(\vxs,\vys)\:=
+\RW{case}\:\vxs\:\RW{of}\\
+\hg\hg\begin{array}{ll}
+\DC{Con}\:0()&\cq\:\vys\\
+\DC{Con}\:1(\vx,\vxs')&\cq\:\DC{Con}\:1(\vx,\VV{append}(\vxs',\vys))
+\end{array}
+}
+}
+
+\subsubsection*{Evaluation Strategy}
+
+By default, expressions are evaluated eagerly (in applicative order),
+i.e. arguments to functions and tagged unions are evaluated
+immediately, left to right. Evaluation can instead be delayed using
+the $\RW{lazy}$ construct. An expression $\RW{lazy}(\vt)$ will not be
+evaluated until it is required by one of:
+
+\begin{itemize}
+\item Inspection in a $\RW{case}$ expression or the condition in an
+ $\RW{if}$ statement.
+\item Field projection.
+\item Being passed to a foreign function.
+% FIXME: you haven't explained thunks yet...
+\item Explicit evaluation with $\RW{effect}$. This evaluates
+ side-effecting code (and does not update the thunk).
+\end{itemize}
+
+
+\subsubsection*{Higher order functions}
+
+Finally, expressions may contain $\lambda$ and $\RW{let}$
+bindings. Higher order functions such as $\VV{map}$ are also permitted:
+
+\DM{
+\AR{
+\VV{map}(\vf,\vxs)\:=\:
+\RW{case}\:\vxs\:\RW{of}\\
+\hg\hg\begin{array}{ll}
+\DC{Con}\:0() & \cq\:\DC{Con}\:0()\\
+\DC{Con}\:1(\vx,\vxs') & \cq\:\DC{Con}\:1(\vf(\vx), \VV{map}(\vf,\vxs'))
+\end{array}
+\medskip
+\\
+\VV{evens}(\vn)\:=\:\RW{let}\:\AR{\VV{nums}\:=\:
+\VV{take}(\vn, \VV{countFrom}(1))\:\RW{in}\\
+\VV{map}(\lambda\vx\SC\vx\:\times \:2, \VV{nums})
+}
+}
+}
+
+\subsection{Foreign Functions}
+
+Most programs eventually need to interact with the operating
+system. Epic provides a lightweight foreign function interface which
+allows interaction with external C code.
+Since Epic does no type checking or inference,
+a foreign call requires the argument and return types to be given
+explicitly. e.g. the C function:
+
+\begin{SaveVerbatim}{csin}
+
+double sin(double x);
+
+\end{SaveVerbatim}
+\useverb{csin}
+
+\noindent
+We can call this function from Epic by giving the C name, the return
+type (an Epic $\TC{Float}$) and the argument type (also an Epic
+$\TC{Float}$).
+
+\DM{
+\VV{sin}(\vx)\:=\:\RW{foreign}\:\TC{Float}\:\mathtt{"sin"}\:(\vx\Hab\TC{Float})
+}
+
+\subsection{Low Level Features}
+
+Epic emphasises control over safety, and therefore provides some low
+level features to give language implementations more control over
+generated code. A high level language may wish to use these features
+in some performance critical contexts, whether for sequencing side
+effects, implementing optimisations, or to provide run-time support
+code.
+Epic allows sequencing, $\RW{while}$ loops and variable update, and
+provides a $\RW{malloc}$ construct for memory allocation. The
+behaviour of $\RW{malloc}\:\vn\:\vt$ is to create a fixed pool of
+$\vn$ bytes, and allocate only from this pool when evaluating
+$\vt$.
+
+\subsection{Haskell API}
+
+The primary interface to Epic is through a Haskell API, which is used
+to build expressions and programs, and to compile them to executables.
+Implementing a compiler for a high level language is then a matter of
+converting the abstract syntax of a high level program into an Epic
+program, through these ``compiler combinators'', and implementing any
+run-time support as Epic functions.
+
+\subsubsection*{Programs and expressions}
+
+The API allows the building of Epic programs with an Embedded Domain
+Specific Language (EDSL) style interface, i.e. we try to exploit
+Haskell's syntax as far as possible. There are several
+possible representations of Epic expressions.
+\texttt{Expr} is the internal abstract representation, and
+\texttt{Term} is a representation which carries a name supply. We have
+a type class \texttt{EpicExpr} which provides a function \texttt{term}
+for building a concrete expression using a name supply:
+
+\begin{SaveVerbatim}{exprclass}
+
+type Term = State Int Expr
+
+class EpicExpr e where
+ term :: e -> Term
+
+\end{SaveVerbatim}
+\useverb{exprclass}
+
+There are straightforward instances of \texttt{EpicExpr} for the
+internal representations \texttt{Expr} and \texttt{Term}. There is also
+an instance for \texttt{String}, which parses concrete syntax, which
+is beyond the scope of this paper. More interestingly, we can build an
+instance of the type class which allows Haskell functions to be used
+to build Epic functions. This means we can use Haskell names for Epic
+references, and not need to worry about scoping or ambiguous name
+choices.
+
+\begin{SaveVerbatim}{exprinstance}
+
+instance EpicExpr e => EpicExpr (Expr -> e) where
+
+\end{SaveVerbatim}
+\useverb{exprinstance}
+
+\noindent
+If we have explicit names for arguments, it can be more convenient to
+pass these to Epic directly rather than to use the name supply. We
+provide an instance to allow a user to give argument names explicitly:
+
+\begin{SaveVerbatim}{exprnamed}
+
+instance EpicExpr e => EpicExpr ([Name], e) where
+
+\end{SaveVerbatim}
+\useverb{exprnamed}
+
+\noindent
+Both forms, using Haskell functions or explicit names, can be mixed
+freely in an expression. A program is a collection of named Epic
+expressions built using the \texttt{EpicExpr} class:
+
+\begin{SaveVerbatim}{eprogs}
+
+type Program = [EpicDecl]
+
+data EpicDecl = forall e. EpicExpr e => EpicFn Name e
+
+\end{SaveVerbatim}
+\useverb{eprogs}
+
+\noindent
+The library provides a number of built-in definitions for some common
+operations such as outputting strings and converting data types:
+
+\begin{SaveVerbatim}{bdefs}
+
+basic_defs :: [EpicDecl]
+
+\end{SaveVerbatim}
+\useverb{bdefs}
+
+\noindent
+In this paper we use $\VV{putStr}$ and $\VV{putStrLn}$ for outputting
+strings, $\VV{append}$ for concatenating strings, and
+$\VV{intToString}$ for integer to string conversion.
+We can compile a collection of definitions to an executable, or simply
+execute them directly. Execution begins with the function called
+\texttt{"main"} --- Epic reports an error if this function is not
+defined:
+
+\begin{SaveVerbatim}{compepic}
+
+compile :: Program -> FilePath -> IO ()
+run :: Program -> IO ()
+
+\end{SaveVerbatim}
+\useverb{compepic}
+
+\subsubsection*{Building expressions}
+
+We have seen how to build $\lambda$ bindings with the
+\texttt{EpicExpr} class, using either Haskell's $\lambda$ or pairing
+explicitly bound names with their scope. We now add further
+sub-expressions. Firstly, we introduce functions for referring to
+explicitly bound names --- \texttt{ref} build a reference to a
+\texttt{Name}, \texttt{name} converts a string into the internal form,
+and \texttt{fn} combines these operations.
+
+\begin{SaveVerbatim}{nameapi}
+
+ref :: Name -> Term
+name :: String -> Name
+fn :: String -> Term
+
+\end{SaveVerbatim}
+\useverb{nameapi}
+
+\noindent
+We would refer to the $\VV{putStrLn}$ function, for example, with
+\texttt{fn~"putStrLn"}.
+The general form of functions which build expressions is to create a
+\texttt{Term} --- i.e. an expression which manages its own name supply
+--- by combining arbitrary Epic expressions (i.e. instances of
+\texttt{EpicExpr}). For example, to apply a function to an argument,
+we provide an \texttt{EpicExpr} for the function and the argument:
+
+\begin{SaveVerbatim}{appapi}
+
+infixl 5 @@
+(@@) :: (EpicExpr f, EpicExpr a) => f -> a -> Term
+
+\end{SaveVerbatim}
+\useverb{appapi}
+
+\noindent
+Since \texttt{Term} itself is an instance of \texttt{EpicExpr}, we can
+apply a function to several arguments through nested applications of
+\texttt{@@}, which associates to the left as with normal Haskell
+function application. We have several arithmetic operators, including
+arithmetic, comparison and bitwise operators, e.g.:
+
+\begin{SaveVerbatim}{opsapi}
+
+plus_, minus_, times_, divide_, :: Op
+
+\end{SaveVerbatim}
+\useverb{opsapi}
+
+\noindent
+We follow the convention that Epic keywords and primitive
+operators are represented by a Haskell function with an underscore
+suffix. This convention arises because we cannot use Haskell keywords
+such as \texttt{if}, \texttt{let} and \texttt{case} as function names.
+For consistency, we have extended the convention to all functions and
+operators. \texttt{if...then...else} expressions are built using the
+\texttt{if\_} function:
+
+\begin{SaveVerbatim}{ifexp}
+
+if_ :: (EpicExpr a, EpicExpr t, EpicExpr e) => a -> t -> e -> Term
+
+\end{SaveVerbatim}
+\useverb{ifexp}
+
+\noindent
+For $\RW{let}$ bindings, we can either use higher order syntax or bind
+an explicit name. To achieve this, as before, we implement a type
+class and instances which support both:
+
+\begin{SaveVerbatim}{letapi}
+
+class LetExpr e where
+ let_ :: EpicExpr val => val -> e -> State Int Expr
+
+instance EpicExpr sc => LetExpr (Name, sc)
+instance LetExpr (Expr -> Term)
+
+\end{SaveVerbatim}
+\useverb{letapi}
+
+%% \noindent
+%% Occasionally, especially in imperative code, we use $\RW{let}$
+%% bindings for sequencing actions. We provide a shorthand for this
+%% common case:
+
+%% \begin{SaveVerbatim}{seqapi}
+
+%% (+>) :: (EpicExpr c) => c -> Term -> Term
+%% (+>) c k = let_ c (\x -> k)
+
+%% \end{SaveVerbatim}
+%% \useverb{seqapi}
+
+\noindent
+To build a constructor form, we apply a constructor with an integer
+\remph{tag} to its arguments. We build a constructor using the
+\texttt{con\_} function, and provide a shorthand \texttt{tuple\_} for
+the common case where the tag can be ignored --- as the name suggests,
+this happens when building tuples and records:
+
+\begin{SaveVerbatim}{conapi}
+
+con_ :: Int -> Term
+tuple_ :: Term
+
+\end{SaveVerbatim}
+\useverb{conapi}
+
+\subsubsection*{Case analysis}
+
+\noindent
+To inspect constructor forms, or to deconstruct tuples, we use
+$\RW{case}$ expressions. A case expression chooses one of the
+alternative executions path depending on the value of the scrutinee,
+which can be any Epic expression:
+
+\begin{SaveVerbatim}{caseapi}
+
+case_ :: EpicExpr e => e -> [Case] -> Term
+
+\end{SaveVerbatim}
+\useverb{caseapi}
+
+\noindent
+We leave the definition of \texttt{Case} abstract (although it is
+simply an Epic expression carrying a name supply) and provide an
+interface for building case branches.
+The scrutinee is matched against each branch, in order. To match
+against a constructor form, we use the same trick as we did for
+$\lambda$-bindings, either allowing Haskell to manage to scope of
+constructor arguments, or giving names explicitly to arguments, or a
+mixture:
+
+\begin{SaveVerbatim}{conalt}
+
+class Alternative e where
+ mkAlt :: Tag -> e -> Case
+
+\end{SaveVerbatim}
+\begin{SaveVerbatim}{conalt2}
+
+instance Alternative Expr
+instance Alternative Term
+
+instance Alternative e => Alternative (Expr -> e)
+instance Alternative e => Alternative ([Name], e)
+
+\end{SaveVerbatim}
+\useverb{conalt}
+
+\useverb{conalt2}
+
+\noindent
+We can build case alternatives for constructor forms (matching a
+specific tag), tuples, or integer constants (matching a specific
+constant), as well as a default case if all other alternatives fail to
+match. In each of the following, \texttt{e} is an expression which
+gives the argument bindings, if any, and the right hand side of the
+match.
+
+%(We have to use \texttt{Alternative} rather than
+%\texttt{EpicExpr} to ensure that we get arguments bound in the match,
+%rather than a $\lambda$ binding on the right hand side).
+
+\begin{SaveVerbatim}{altsapi}
+
+con :: Alternative e => Int -> e -> Case
+tuple :: Alternative e => e -> Case
+constcase :: EpicExpr e => Int -> e -> Case
+defaultcase :: EpicExpr e => e -> Case
+
+\end{SaveVerbatim}
+\useverb{altsapi}
+
View
325 Papers/Epic-TFP/library.ltx
@@ -0,0 +1,325 @@
+%%%%%%%%%%%%%%% library file for datatypes etc.
+
+%%% Identifiers
+
+\newcommand{\va}{\VV{a}}
+\newcommand{\vb}{\VV{b}}
+\newcommand{\vc}{\VV{c}}
+\newcommand{\vd}{\VV{d}}
+\newcommand{\ve}{\VV{e}}
+\newcommand{\vf}{\VV{f}}
+\newcommand{\vg}{\VV{g}}
+\newcommand{\vh}{\VV{h}}
+\newcommand{\vi}{\VV{i}}
+\newcommand{\vj}{\VV{j}}
+\newcommand{\vk}{\VV{k}}
+\newcommand{\vl}{\VV{l}}
+\newcommand{\vm}{\VV{m}}
+\newcommand{\vn}{\VV{n}}
+\newcommand{\vo}{\VV{o}}
+\newcommand{\vp}{\VV{p}}
+\newcommand{\vq}{\VV{q}}
+\newcommand{\vr}{\VV{r}}
+\newcommand{\vs}{\VV{s}}
+\newcommand{\vt}{\VV{t}}
+\newcommand{\vu}{\VV{u}}
+\newcommand{\vv}{\VV{v}}
+\newcommand{\vw}{\VV{w}}
+\newcommand{\vx}{\VV{x}}
+\newcommand{\vy}{\VV{y}}
+\newcommand{\vz}{\VV{z}}
+\newcommand{\vA}{\VV{A}}
+\newcommand{\vB}{\VV{B}}
+\newcommand{\vC}{\VV{C}}
+\newcommand{\vD}{\VV{D}}
+\newcommand{\vE}{\VV{E}}
+\newcommand{\vF}{\VV{F}}
+\newcommand{\vG}{\VV{G}}
+\newcommand{\vH}{\VV{H}}
+\newcommand{\vI}{\VV{I}}
+\newcommand{\vJ}{\VV{J}}
+\newcommand{\vK}{\VV{K}}
+\newcommand{\vL}{\VV{L}}
+\newcommand{\vM}{\VV{M}}
+\newcommand{\vN}{\VV{N}}
+\newcommand{\vO}{\VV{O}}
+\newcommand{\vP}{\VV{P}}
+\newcommand{\vQ}{\VV{Q}}
+\newcommand{\vR}{\VV{R}}
+\newcommand{\vS}{\VV{S}}
+\newcommand{\vT}{\VV{T}}
+\newcommand{\vU}{\VV{U}}
+\newcommand{\vV}{\VV{V}}
+\newcommand{\vW}{\VV{W}}
+\newcommand{\vX}{\VV{X}}
+\newcommand{\vY}{\VV{Y}}
+\newcommand{\vZ}{\VV{Z}}
+\newcommand{\vas}{\VV{as}}
+\newcommand{\vbs}{\VV{bs}}
+\newcommand{\vcs}{\VV{cs}}
+\newcommand{\vds}{\VV{ds}}
+\newcommand{\ves}{\VV{es}}
+\newcommand{\vfs}{\VV{fs}}
+\newcommand{\vgs}{\VV{gs}}
+\newcommand{\vhs}{\VV{hs}}
+\newcommand{\vis}{\VV{is}}
+\newcommand{\vjs}{\VV{js}}
+\newcommand{\vks}{\VV{ks}}
+\newcommand{\vls}{\VV{ls}}
+\newcommand{\vms}{\VV{ms}}
+\newcommand{\vns}{\VV{ns}}
+\newcommand{\vos}{\VV{os}}
+\newcommand{\vps}{\VV{ps}}
+\newcommand{\vqs}{\VV{qs}}
+\newcommand{\vrs}{\VV{rs}}
+%\newcommand{\vss}{\VV{ss}}
+\newcommand{\vts}{\VV{ts}}
+\newcommand{\vus}{\VV{us}}
+\newcommand{\vvs}{\VV{vs}}
+\newcommand{\vws}{\VV{ws}}
+\newcommand{\vxs}{\VV{xs}}
+\newcommand{\vys}{\VV{ys}}
+\newcommand{\vzs}{\VV{zs}}
+
+%%% Telescope Identifiers
+
+\newcommand{\ta}{\vec{\VV{a}}}
+\newcommand{\tb}{\vec{\VV{b}}}
+\newcommand{\tc}{\vec{\VV{c}}}
+\newcommand{\td}{\vec{\VV{d}}}
+\newcommand{\te}{\vec{\VV{e}}}
+\newcommand{\tf}{\vec{\VV{f}}}
+\newcommand{\tg}{\vec{\VV{g}}}
+%\newcommand{\th}{\vec{\VV{h}}}
+\newcommand{\ti}{\vec{\VV{i}}}
+\newcommand{\tj}{\vec{\VV{j}}}
+\newcommand{\tk}{\vec{\VV{k}}}
+\newcommand{\tl}{\vec{\VV{l}}}
+\newcommand{\tm}{\vec{\VV{m}}}
+\newcommand{\tn}{\vec{\VV{n}}}
+%\newcommand{\to}{\vec{\VV{o}}}
+\newcommand{\tp}{\vec{\VV{p}}}
+\newcommand{\tq}{\vec{\VV{q}}}
+\newcommand{\tr}{\vec{\VV{r}}}
+\newcommand{\tts}{\vec{\VV{s}}}
+\newcommand{\ttt}{\vec{\VV{t}}}
+\newcommand{\tu}{\vec{\VV{u}}}
+%\newcommand{\tv}{\vec{\VV{v}}}
+\newcommand{\tw}{\vec{\VV{w}}}
+\newcommand{\tx}{\vec{\VV{x}}}
+\newcommand{\ty}{\vec{\VV{y}}}
+\newcommand{\tz}{\vec{\VV{z}}}
+\newcommand{\tA}{\vec{\VV{A}}}
+\newcommand{\tB}{\vec{\VV{B}}}
+\newcommand{\tC}{\vec{\VV{C}}}
+\newcommand{\tD}{\vec{\VV{D}}}
+\newcommand{\tE}{\vec{\VV{E}}}
+\newcommand{\tF}{\vec{\VV{F}}}
+\newcommand{\tG}{\vec{\VV{G}}}
+\newcommand{\tH}{\vec{\VV{H}}}
+\newcommand{\tI}{\vec{\VV{I}}}
+\newcommand{\tJ}{\vec{\VV{J}}}
+\newcommand{\tK}{\vec{\VV{K}}}
+\newcommand{\tL}{\vec{\VV{L}}}
+\newcommand{\tM}{\vec{\VV{M}}}
+\newcommand{\tN}{\vec{\VV{N}}}
+\newcommand{\tO}{\vec{\VV{O}}}
+\newcommand{\tP}{\vec{\VV{P}}}
+\newcommand{\tQ}{\vec{\VV{Q}}}
+\newcommand{\tR}{\vec{\VV{R}}}
+\newcommand{\tS}{\vec{\VV{S}}}
+\newcommand{\tT}{\vec{\VV{T}}}
+\newcommand{\tU}{\vec{\VV{U}}}
+\newcommand{\tV}{\vec{\VV{V}}}
+\newcommand{\tW}{\vec{\VV{W}}}
+\newcommand{\tX}{\vec{\VV{X}}}
+\newcommand{\tY}{\vec{\VV{Y}}}
+\newcommand{\tZ}{\vec{\VV{Z}}}
+
+
+
+%%% Nat
+
+\newcommand{\NatPackage}{
+ \newcommand{\Nat}{\TC{\mathbb{N}}}
+ \newcommand{\Z}{\DC{0}}
+ \newcommand{\suc}{\DC{s}}
+ \newcommand{\NatDecl}{
+ \Data \hg
+ \Axiom{\Nat\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\Z\Hab\Nat} \hg
+ \Rule{\vn\Hab\Nat}
+ {\suc\:\vn\Hab\Nat}
+}}
+
+%%% Bool
+
+\newcommand{\BoolPackage}{
+ \newcommand{\Bool}{\TC{Bool}}
+ \newcommand{\true}{\DC{true}}
+ \newcommand{\false}{\DC{false}}
+ \newcommand{\BoolDecl}{
+ \Data \hg
+ \Axiom{\Bool\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\true\Hab\Bool} \hg
+ \Axiom{\false\Hab\Bool}
+}}
+
+%%% So
+
+\newcommand{\SoPackage}{
+ \newcommand{\So}{\TC{So}}
+ \newcommand{\oh}{\DC{oh}}
+ \newcommand{\SoDecl}{
+ \Data \hg
+ \Rule{\vb\Hab\Bool}
+ {\So\:\vb\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\oh\Hab\So\:\true}
+}}
+
+%%% Unit
+
+\newcommand{\UnitPackage}{
+ \newcommand{\Unit}{\TC{Unit}}
+ \newcommand{\void}{\DC{void}}
+ \newcommand{\UnitDecl}{
+ \Data \hg
+ \Axiom{\Unit\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\void\Hab\Unit}
+}}
+
+%%% Maybe
+
+\newcommand{\MaybePackage}{
+ \newcommand{\Maybe}{\TC{Maybe}}
+ \newcommand{\yes}{\DC{yes}}
+ \newcommand{\no}{\DC{no}}
+ \newcommand{\MaybeDecl}{
+ \Data \hg
+ \Rule{\vA\Hab\Type}
+ {\Maybe\:\vA\Hab\Type} \hg
+ \Where \hg
+ \Rule{\va \Hab \vA}
+ {\yes\:\va\Hab\Maybe\:\vA} \hg
+ \Axiom{\no\Hab\Maybe\:\vA}
+}}
+
+%%% Cross
+
+\newcommand{\pr}[2]{(#1\DC{,}#2)} %grrrr
+\newcommand{\CrossPackage}{
+ \newcommand{\Cross}{\times}
+ \newcommand{\CrossDecl}{
+ \Data \hg
+ \Rule{\vA,\vB\Hab\Type}
+ {\vA\Cross\vB\Hab\Type} \hg
+ \Where \hg
+ \Rule{\va \Hab \vA \hg \vb\Hab\vB}
+ {\pr{\va}{\vb}\Hab\vA\Cross\vB}
+}}
+
+%%% Fin
+
+\newcommand{\FinPackage}{
+ \newcommand{\Fin}{\TC{Fin}}
+ \newcommand{\fz}{\DC{f0}}
+ \newcommand{\fs}{\DC{fs}}
+ \newcommand{\FinDecl}{
+ \AR{
+ \Data \hg
+ \Rule{\vn\Hab\Nat}
+ {\Fin\:\vn\Hab\Type} \hg \\
+ \Where \hg
+ \begin{array}[t]{c}
+ \Axiom{\fz\Hab\Fin\:(\suc\:\vn)} \hg
+ \Rule{\vi\Hab\Fin\:\vn}
+ {\fs\:\vi\Hab\Fin\:(\suc\:\vn)}
+ \end{array}
+ }
+}}
+
+%%% Vect
+
+\newcommand{\VectPackage}{
+ \newcommand{\Vect}{\TC{Vect}}
+ \newcommand{\vnil}{\varepsilon}
+ \newcommand{\vcons}{\,\dcolon\,}
+ \newcommand{\vsnoc}{\,\dcolon\,}
+ \newcommand{\VectConsDecl}{
+ \Data \hg
+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
+ {\Vect\:\vA\:\vn\Hab\Type} \hg
+ \Where \hg \begin{array}[t]{c}
+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
+ \Rule{\vx\Hab\vA \hg \vxs\Hab \Vect\:\vA\:\vn }
+ {\vx\vcons\vxs\Hab\Vect\:\vA\:(\suc\vn)}
+ \end{array}
+}
+ \newcommand{\VectSnocDecl}{
+ \Data \hg
+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
+ {\Vect\:\vA\:\vn\Hab\Type} \hg
+ \Where \hg \begin{array}[t]{c}
+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
+ \Rule{\vxs\Hab \Vect\:\vA\:\vn \hg \vx\Hab\vA}
+ {\vxs\vsnoc\vx\Hab\Vect\:\vA\:(\suc\vn)}
+ \end{array}
+}
+}
+
+%%% Compare
+
+%Data Compare : (x:nat)(y:nat)Type
+% = lt : (x:nat)(y:nat)(Compare x (plus (S y) x))
+% | eq : (x:nat)(Compare x x)
+% | gt : (x:nat)(y:nat)(Compare (plus (S x) y) y);
+
+
+\newcommand{\ComparePackage}{
+ \newcommand{\Compare}{\TC{Compare}}
+ \newcommand{\ltComp}{\DC{lt}}
+ \newcommand{\eqComp}{\DC{eq}}
+ \newcommand{\gtComp}{\DC{gt}}
+ \newcommand{\CompareDecl}{
+ \Data \hg
+ \Rule{\vm\Hab\Nat\hg\vn\Hab\Nat}
+ {\Compare\:\vm\:\vn\Hab\Type} \\
+ \Where \hg\begin{array}[t]{c}
+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
+ {\ltComp_{\vx}\:\vy\Hab\Compare\:\vx\:(\FN{plus}\:\vx\:(\suc\:\vy))} \\
+ \Rule{\vx\Hab\Nat}
+ {\eqComp_{\vx}\Hab\Compare\:\vx\:\vx}\\
+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
+ {\gtComp_{\vy}\:\vx\Hab\Compare\:(\FN{plus}\:\vy\:(\suc\:\vx))\:\vy} \\
+ \end{array}
+ }
+
+%Data CompareM : Type
+% = ltM : (ydiff:nat)CompareM
+% | eqM : CompareM
+% | gtM : (xdiff:nat)CompareM;
+
+ \newcommand{\CompareM}{\TC{Compare^-}}
+ \newcommand{\ltCompM}{\DC{lt^-}}
+ \newcommand{\eqCompM}{\DC{eq^-}}
+ \newcommand{\gtCompM}{\DC{gt^-}}
+ \newcommand{\CompareMDecl}{
+
+ \Data \hg
+ \Axiom{\CompareM\Hab\Type} \\
+ \Where \hg\begin{array}[t]{c}
+ \Rule{\vy\Hab\Nat}
+ {\ltCompM\:\vy\Hab\CompareM} \\
+ \Axiom{\eqCompM\Hab\CompareM}\\
+ \Rule{\vx\Hab\Nat}
+ {\gtCompM\:\vx\Hab\CompareM} \\
+ \end{array}
+ }
+ \newcommand{\CompareRec}{\FN{CompareRec}}
+ \newcommand{\CompareRecM}{\FN{CompareRec^-}}
+
+}
View
3,829 Papers/Epic-TFP/literature.bib
3,829 additions, 0 deletions not shown
View
1,207 Papers/Epic-TFP/llncs.cls
@@ -0,0 +1,1207 @@
+% LLNCS DOCUMENT CLASS -- version 2.17 (12-Jul-2010)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%% Digits \0\1\2\3\4\5\6\7\8\9
+%% Exclamation \! Double quote \" Hash (number) \#
+%% Dollar \$ Percent \% Ampersand \&
+%% Acute accent \' Left paren \( Right paren \)
+%% Asterisk \* Plus \+ Comma \,
+%% Minus \- Point \. Solidus \/
+%% Colon \: Semicolon \; Less than \<
+%% Equals \= Greater than \> Question mark \?
+%% Commercial at \@ Left bracket \[ Backslash \\
+%% Right bracket \] Circumflex \^ Underscore \_
+%% Grave accent \` Left brace \{ Vertical bar \|
+%% Right brace \} Tilde \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2010/07/12 v2.17
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openright\iftrue
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+\RequirePackage{aliascnt}
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+ \ifnum #1>\c@tocdepth \else
+ \vskip \z@ \@plus.2\p@
+ {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \parindent #2\relax\@afterindenttrue
+ \interlinepenalty\@M
+ \leavevmode
+ \@tempdima #3\relax
+ \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+ {#4}\nobreak
+ \leaders\hbox{$\m@th
+ \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+ mu$}\hfill
+ \nobreak
+ \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+ \par}%
+ \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Keywords:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+ \@setfontsize\small\@ixpt{11}%
+ \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+ \abovedisplayshortskip \z@ \@plus2\p@
+ \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \parsep 0\p@ \@plus1\p@ \@minus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep0\p@}%
+ \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin {63\p@}
+\setlength\evensidemargin {63\p@}
+\setlength\marginparwidth {90\p@}
+
+\setlength\headsep {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+ \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+ \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+ \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+ \thispagestyle{empty}%
+ \if@twocolumn
+ \onecolumn
+ \@tempswatrue
+ \else
+ \@tempswafalse
+ \fi
+ \null\vfil
+ \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+ \ifnum \c@secnumdepth >-2\relax
+ \refstepcounter{part}%
+ \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+ \else
+ \addcontentsline{toc}{part}{#1}%
+ \fi
+ \markboth{}{}%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \ifnum \c@secnumdepth >-2\relax
+ \huge\bfseries \partname~\thepart
+ \par
+ \vskip 20\p@
+ \fi
+ \Huge \bfseries #2\par}%
+ \@endpart}
+\def\@spart#1{%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \Huge \bfseries #1\par}%
+ \@endpart}
+\def\@endpart{\vfil\newpage
+ \if@twoside
+ \null
+ \thispagestyle{empty}%
+ \newpage
+ \fi
+ \if@tempswa
+ \twocolumn
+ \fi}
+
+\newcommand\chapter{\clearpage
+ \thispagestyle{empty}%
+ \global\@topnum\z@
+ \@afterindentfalse
+ \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+ \if@mainmatter
+ \refstepcounter{chapter}%
+ \typeout{\@chapapp\space\thechapter.}%
+ \addcontentsline{toc}{chapter}%
+ {\protect\numberline{\thechapter}#1}%
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \chaptermark{#1}%
+ \addtocontents{lof}{\protect\addvspace{10\p@}}%
+ \addtocontents{lot}{\protect\addvspace{10\p@}}%
+ \if@twocolumn