% !TEX program = xelatex\documentclass{article}\usepackage{../style}\usepackage{../langs}\usepackage{../graphics}\usepackage{../grammar}\begin{document}\fnote{\copyright{} Christian Urban, King's College London, 2019, 2023}% CPS translations% https://felleisen.org/matthias/4400-s20/lecture17.html%% pattern matching resources%% https://www.reddit.com/r/ProgrammingLanguages/comments/g1vno3/beginner_resources_for_compiling_pattern_matching/\section*{Handout 9 (LLVM, SSA and CPS)}Reflecting on our two tiny compilers targetting the JVM, the codegeneration part was actually not so hard, no? Pretty much just somepost-traversal of the abstract syntax tree, yes? One of the reasonsfor this ease is that the JVM is a stack-based virtual machine and itis therefore not hard to translate deeply-nested arithmeticexpressions into a sequence of instructions manipulating thestack. The problem is that ``real'' CPUs, although supporting stackoperations, are not really designed to be \emph{stack machines}. Thedesign of CPUs is more like: Here are some operations and a chunk ofmemory---compiler, or better compiler writers, do something withthem. Consequently, modern compilers need to go the extra mile inorder to generate code that is much easier and faster to process byactual CPUs, rather than running code on virtual machines thatintroduce an additional layer of indirection. To make this alltractable for this module, we target the LLVM IntermediateLanguage. In this way we can take advantage of the tools coming withLLVM.\footnote{\url{http://llvm.org}} For example we do not have toworry about things like register allocations. By using LLVM, however,we also have to pay price in the sense that generating code getsharder\ldots{}unfortunately.\subsection*{LLVM and LLVM-IR}\noindent LLVM is a beautiful examplethat projects from Academia can make a difference in the World. LLVMstarted in 2000 as a project by two researchers at the University ofIllinois at Urbana-Champaign. At the time the behemoth of compilers wasgcc with its myriad of front-ends for different programming languages (C++, Fortran,Ada, Go, Objective-C, Pascal etc). The problem was that gcc morphed overtime into a monolithic gigantic piece of m\ldots ehm complicatedsoftware, which youcould not mess about in an afternoon. In contrast, LLVM is designed tobe a modular suite of tools with which you can play around easily andtry out something new. LLVM became a big player once Apple hired one ofthe original developers (I cannot remember the reason why Apple did notwant to use gcc, but maybe they were also just disgusted by gcc's bigmonolithic codebase). Anyway, LLVM is now the big player and gcc is moreor less legacy. This does not mean that programming languages like C andC++ are dying out any time soon---they are nicely supported by LLVM.We will target the LLVM Intermediate Language, or LLVM IntermediateRepresentation (short LLVM-IR). The LLVM-IR looks very similar to theassembly language of Jasmin and Krakatau. Targetting LLVM-IR will alsoallow us to benefit from the modular structure of the LLVM compilerand we can let, for example, the compiler generate code for differentCPUs, say X86 or ARM. That means we can be agnostic about where ourcode is actually going to run.\footnote{Anybody want to try to run our programs on Android phones?} We can also be somewhat ignorant aboutoptimising our code and about allocating memory efficiently: the LLVMtools will take care of all this.However, what we have to do in order to make LLVM to play ball is togenerate code in \emph{Static Single-Assignment} format (short SSA),because that is what the LLVM-IR expects from us. A reason why LLVMuses the SSA format, rather than JVM-like stack instructions, is thatstack instructions are difficult to optimise---you cannot justre-arrange instructions without messing about with what is calculatedon the stack. Also it is hard to find out if all the calculations onthe stack are actually necessary and not by chance dead code. The JVMhas for all these obstacles sophisticated machinery to make such``high-level'' code still run fast, but let's say that for the sake ofargument we do not want to rely on it. We want to generate fast codeourselves. This means we have to work around the intricacies of whatinstructions CPUs can actually process fast. This is what the SSAformat is designed for.The main idea behind the SSA format is to use very simple variableassignments where every tmp-variable is assigned only once. Theassignments also need to be primitive in the sense that they can bejust simple operations like addition, multiplication, jumps,comparisons, function calls and so on. Say, we have an expression$((1 + a) + (foo(3 + 2) + (b * 5)))$, then the corresponding SSA format is\begin{lstlisting}[language=LLVMIR,numbers=left]let tmp0 = add 1 a inlet tmp1 = add 3 2 in let tmp2 = call foo(tmp1) let tmp3 = mul b 5 in let tmp4 = add tmp2 tmp3 in let tmp5 = add tmp0 tmp4 in return tmp5 \end{lstlisting}\noindent where every tmp-variable is used only once (we could, forexample, not write \texttt{tmp1 = add tmp2 tmp3} in Line 5 even if thiswould not change the overall result).There are sophisticated algorithms for imperative languages, like C,that efficiently transform a high-level program into SSA format. Butwe can ignore them here. We want to compile a functional language andthere things get much more interesting than just sophisticated. Wewill need to have a look at CPS translations, where the CPS stands forContinuation-Passing-Style---basically black programming art orabracadabra programming. So sit tight.\subsection*{LLVM-IR}Before we start, let's however first have a look at the \emph{LLVM IntermediateRepresentation} in more detail. The LLVM-IR is in between the frontendsand backends of the LLVM framework. It allows compilation of multiplesource languages to multiple targets. It is also the place where most ofthe target independent optimisations are performed. What is good about our toy Fun-language is that it basically onlycontains expressions (be they arithmetic expressions, booleanexpressions or if-expressions). The exception are function definitions.Luckily, for them we can use the mechanism of defining functions in theLLVM-IR (this is similar to using JVM methods for functions in ourearlier compiler). For example the simple Fun-program \begin{lstlisting}[language=Scala,numbers=none]def sqr(x) = x * x\end{lstlisting}\noindentcan be compiled to the following LLVM-IR function:\begin{lstlisting}[language=LLVM]define i32 @sqr(i32 %x) { %tmp = mul i32 %x, %x ret i32 %tmp} \end{lstlisting}\noindent First notice that all ``local'' variable names, in this case\texttt{x} and \texttt{tmp}, are prefixed with \texttt{\%} in theLLVM-IR. Temporary variables can be named with an identifier, such as\texttt{tmp}, or numbers. In contrast, function names, since they are``global'', need to be prefixed with an @-symbol. Also, the LLVM-IR isa fully typed language. The \texttt{i32} type stands for 32-bitintegers. There are also types for 64-bit integers (\texttt{i64}),chars (\texttt{i8}), floats, arrays and even pointer types. In thecode above, \texttt{sqr} takes an argument of type \texttt{i32} andproduces a result of type \texttt{i32} (the result type is in front ofthe function name, like in C). Each arithmetic operation, for exampleaddition and multiplication, are also prefixed with the type theyoperate on. Obviously these types need to match up\ldots{} but sincewe have in our programs only integers, for the moment \texttt{i32}everywhere will do. We do not have to generate any other types, butobviously this is a limitation in our Fun-language (and which welift in the final CW).There are a few interesting instructions in the LLVM-IR which are quitedifferent than what we have seen in the JVM. Can you remember thekerfuffle we had to go through with boolean expressions and negating thecondition? In the LLVM-IR, branching if-conditions are implementeddifferently: there is a separate \texttt{br}-instruction as follows:\begin{lstlisting}[language=LLVM]br i1 %var, label %if_br, label %else_br\end{lstlisting}\noindentThe type \texttt{i1} stands for booleans. If the variable is true,then this instruction jumps to the if-branch, which needs an explicitlabel; otherwise it jumps to the else-branch, again with its ownlabel. This allows us to keep the meaning of the boolean expression``as is'' when compiling if's---thanks god no more negating ofbooleans.A value of type boolean is generated in the LLVM-IR by the\texttt{icmp}-instruction. This instruction is for integers (hence the\texttt{i}) and takes the comparison operation as argument. For example\begin{lstlisting}[language=LLVM]icmp eq i32 %x, %y ; for equalicmp sle i32 %x, %y ; signed less or equalicmp slt i32 %x, %y ; signed less thanicmp ult i32 %x, %y ; unsigned less than \end{lstlisting}\noindentNote that in some operations the LLVM-IR distinguishes between signed and unsigned representations of integers. I assume you know what this means,otherwise just ask.It is also easy to call another function in LLVM-IR: as can be seen from Figure~\ref{lli} we can just call a function with the instruction \texttt{call} and can also assign the result to a variable. The syntax is as follows\begin{lstlisting}[language=LLVM]%var = call i32 @foo(...args...)\end{lstlisting}\noindentwhere the arguments can only be simple variables and numbers, but not compoundexpressions.Conveniently, you can use the program \texttt{lli}, which comes withLLVM, to interpret programs written in the LLVM-IR. So you can easilycheck whether the code you produced actually works. To get a runningprogram that does something interesting you need to add some boilerplateabout printing out numbers and a main-function that is the entry pointfor the program (see Figure~\ref{lli} for a complete listing of the square function). Againthis is very similar to the boilerplate we needed to add in our JVMcompiler. You can generate a binary for the program in Figure~\ref{lli} by usingthe \texttt{llc}-compiler and then \texttt{gcc}/\texttt{clang}, whereby \texttt{llc} generatesan object file and \texttt{gcc} (that is actually \texttt{clang} on my Mac) generates theexecutable binary:\begin{lstlisting}[language=bash,numbers=none]llc -filetype=obj sqr.llgcc sqr.o -o a.out./a.out> 25\end{lstlisting}\begin{figure}[t]\small \lstinputlisting[language=LLVM,numbers=left]{../progs/sqr.ll}\caption{An LLVM-IR program for calculating the square function. It calls the sqr-function in \texttt{@main} with the argument \texttt{5} (Line 20). The code for the \texttt{sqr} function is in Lines 13 -- 16. It stores the result of sqr in the variable called \texttt{\%i} and then prints out the contents of this variable in Line 21. The other code is boilerplate for printing out integers.\label{lli}}\end{figure} \subsection*{Our Own Intermediate Language}Let's get back to our compiler: Remember compilers have to solve theproblem of bridging the gap between ``high-level'' programs and``low-level'' hardware. If the gap is too wide for one step, then agood strategy is to lay a stepping stone somewhere in between. TheLLVM-IR itself is such a stepping stone to make the task of generatingand optimising code easier. Like a real compiler we will use our ownstepping stone which I call the \emph{K-language}.\begin{center} \begin{tikzpicture}[scale=0.9,font=\bf, node/.style={ rectangle,rounded corners=3mm, ultra thick,draw=black!50,minimum height=16mm, minimum width=20mm, top color=white,bottom color=black!20}] %\node (0) at (-3,0) {}; \node (A) at (0.0,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}source}] {Fun-Language}; \node (B) at (3.5,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}stepping stone}] {K-Language}; \node (C) at (7.0,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}target}] {LLVM-IR}; \draw [->,line width=2.5mm] (A) -- node [above,pos=0.35] {} (B); \draw [->,line width=2.5mm] (B) -- node [above,pos=0.35] {} (C); \end{tikzpicture} \end{center} \noindent To see why we need a stepping stone for generating code in SSA-format, considder again arithmetic expressions such as $((1 + a) + (3 + (b * 5)))$. They need to be broken up into smaller ``atomic'' steps, like so\begin{lstlisting}[language=LLVMIR,numbers=none]let tmp0 = add 1 a in let tmp1 = mul b 5 in let tmp2 = add 3 tmp1 in let tmp3 = add tmp0 tmp2 in return tmp3 \end{lstlisting}\noindentHere \texttt{tmp3} will contain the result of what the wholeexpression stands for. In each individual step we can only perform an``atomic'' or ``trival'' operation, like addition or multiplication ofa number or a variable. We are not allowed to have for example anested addition or an if-condition on the right-hand side of anassignment. Such constraints are forced upon us because of how the SSAformat works in the LLVM-IR. To simplify matters we representassignments with two kinds of syntactic entities, namely\emph{K-values} and \emph{K-expressions}. K-values are all ``things''that can appear on the right-hand side of an equal. Say we havethe following definition for K-values:\begin{lstlisting}[language=Scala,numbers=none]enum KVal { case KVar(s: String) case KNum(n: Int) case KAop(op: String, v1: KVal, v2: KVal) case KCall(fname: String, args: List[KVal])}\end{lstlisting}\noindentwhere a K-value can be a variable, a number or a ``trivial'' binaryoperation, such as addition or multiplication. The two arguments of abinary operation need to be K-values as well. Finally, we havefunction calls, but again each argument of the function call needs tobe a K-value. One point we need to be careful, however, is that thearguments of the binary operations and function calls are in fact onlyvariables or numbers. To encode this constraint into the type-systemof Scala would make things too complicated---to satisfy thisconstraint is therefore on us. For our Fun-language, we will later onconsider some further K-values.Our K-expressions will encode the \texttt{let} and the \texttt{return}from the SSA-format (again for the moment we only consider these twoconstructors---later on we will have if-branches as well).\begin{lstlisting}[language=Scala,numbers=none]enum KExp { case KLet(x: String, v: KVal, e: KExp) case KReturn(v: KVal)}\end{lstlisting}\noindentBy having in \texttt{KLet} taking first a string (standing for anintermediate variable) and second a value, we can fulfil the SSAconstraint in assignments ``by construction''---there is no way wecould write anything else than a K-value. Note that the thirdargument of a \texttt{KLet} is again a K-expression, meaning eitheranother \texttt{KLet} or a \texttt{KReturn}. In this way we canconstruct a sequence of computations and return a final result. Ofcourse we also have to ensure that all intermediary computations aregiven (fresh) names---we will use an (ugly) counter for this.To sum up, K-values are the atomic operations that can be on theright-hand side of assignemnts. The K-language is restricted such thatit is easy to generate the SSA format for the LLVM-IR. What remains tobe done is a translation of our Fun-language into the K-language. Themain difficulty is that we need to order the computationa---in tehK-language we only have linear sequence of instructions to need to befollowed. Before we explain this, we have a look at someCPS-translation.\subsection*{CPS-Translations}CPS stands for Continuation-Passing-Style. It is a kind of programmingtechnique often used in advanced functional programming. Before we delveinto the CPS-translation for our Fun-language, let us look at CPS-versions of some well-known functions. Consider\begin{lstlisting}[language=Scala, numbers=none]def fact(n: Int) : Int = if (n == 0) 1 else n * fact(n - 1) \end{lstlisting}\noindent This is clearly the usual factorial function. But now consider thefollowing version of the factorial function:\begin{lstlisting}[language=Scala, numbers=none]def factC(n: Int, ret: Int => Int) : Int = if (n == 0) ret(1) else factC(n - 1, x => ret(n * x)) factC(3, identity)\end{lstlisting}\noindentThis function is called with the number, in this case 3, and theidentity-function (which returns just its input). The recursivecalls are:\begin{lstlisting}[language=Scala, numbers=none]factC(2, x => identity(3 * x))factC(1, x => identity(3 * (2 * x)))factC(0, x => identity(3 * (2 * (1 * x))))\end{lstlisting}\noindentHaving reached 0, we get out of the recursion and apply 1 to thecontinuation (see if-branch above). This gives\begin{lstlisting}[language=Scala, numbers=none]identity(3 * (2 * (1 * 1)))= 3 * (2 * (1 * 1))= 6\end{lstlisting}\noindentwhich is the expected result. If this looks somewhat familiar to you,than this is because functions with continuations can beseen as a kind of generalisation of tail-recursive functions.So far we did not look at this generalisation in earnest.Anywaynotice how the continuations is ``stacked up'' during the recursion andthen ``unrolled'' when we apply 1 to the continuation. Interestingly, wecan do something similar to the Fibonacci function where in the traditionalversion we have two recursive calls. Consider the following function\begin{lstlisting}[language=Scala, numbers=none]def fibC(n: Int, ret: Int => Int) : Int = if (n == 0 || n == 1) ret(1) else fibC(n - 1, r1 => fibC(n - 2, r2 => ret(r1 + r2)))\end{lstlisting}\noindentHere the continuation is a nested function essentially wrapping up the second recursive call. Let us check how the recursion unfoldswhen called with 3 and the identity function:\begin{lstlisting}[language=Scala, numbers=none]fibC(3, id)fibC(2, r1 => fibC(1, r2 => id(r1 + r2)))fibC(1, r1 => fibC(0, r2 => fibC(1, r2a => id((r1 + r2) + r2a))))fibC(0, r2 => fibC(1, r2a => id((1 + r2) + r2a)))fibC(1, r2a => id((1 + 1) + r2a))id((1 + 1) + 1)(1 + 1) + 13\end{lstlisting}\noindentThe point of this section is that you are playing around with thesesimple definitions and make sure they calculate the expected result.In the next step, you should understand \emph{how} these functionscalculate the result with the continuations. \section*{Worked Example}Let us now come back to the CPS-translations for the Fun-language. Themain difficulty of generating instructions in SSA format is that largecompound expressions need to be broken up into smaller pieces andintermediate results need to be chained into later instructions. To dothis conveniently, we use the CPS-translation mechanism. What continuationsessentially solve is the following problem: Given an expressions\begin{equation}\label{exp}(1 + 2) * (3 + 4)\end{equation} \noindentwhich of the subexpressions should be calculated first? We just arbitrarilygoing to decide that it will be from left to right. This means we haveto tear the expression shown in \eqref{exp} apart as follows:\[(1 + 2) \qquad\text{and}\qquad \Box * (3 + 4)\] \noindentThe first one will give us a result, but the second one is notreally an expression that makes sense. It will only make senseas the next step in the computation when we fill-in the result of$1+2$ into the ``hole'' indicated by $\Box$. Such incompleteexpressions can be represented in Scala as functions\begin{lstlisting}[language=Scala, numbers=none]r => r * (3 + 4)\end{lstlisting} \noindentwhere \texttt{r} is any result that has been computed earlier. By theway in lambda-calculus notation we would write$\lambda r.\, r * (3 + 4)$ for the same function. To sum up, we usefunctions (``continuations'') to represent what is coming next in asequence of instructions. In our case, continuations are functions oftype \code{KVal} to \code{KExp}. They can be seen as a sequence of\code{KLet}s where there is a ``hole'' that needs to befilled. Consider for example\begin{lstlisting}[language=LLVMIR,numbers=left,escapeinside={(*@}{@*)}]let tmp0 = add 1 a in let tmp1 = mul (*@$\Box$@*) 5 in let tmp2 = add 3 tmp1 in let tmp3 = add tmp0 tmp2 in retrun tmp3 \end{lstlisting}\noindentwhere in the second line is a $\Box$ which still expects a \code{KVal}to be filled in before it becomes a ``proper'' \code{KExp}. When we apply an argument to the continuation (remember they are functions)we essentially fill something into the corresponding hole.Lets look at concrete code. To simplify matters first, suppose our source language consists just of three kinds of expressions\begin{lstlisting}[language=Scala,numbers=none]enum Expr { case Num(n: Int) case Bop(op: String, e1: Expr, e2: Expr) case Call(fname: String, args: List[Expr])}\end{lstlisting}\noindentThe code of the CPS-translation is then of the form\begin{lstlisting}[language=Scala,numbers=none]def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { ... }\end{lstlisting}\noindent where \code{k} is the continuation and \code{e} is the expression tobe compiled. In case we have numbers, we can just pass them to thecontinuations because numbers need not be further teared apart as theyare already atomic. Passing the number to the continuation means we apply the continuation like \begin{lstlisting}[language=Scala,numbers=none] case Num(i) => k(KNum(i))\end{lstlisting}\noindent This would just fill in the $\Box$ in a \code{KLet}-expression.There is no need to create a temporary variable for simple numbers.More interesting is the case for arithmetic operations.\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=0mm]case Aop(op, e1, e2) => { val z = Fresh("tmp") CPS(e1)(r1 => CPS(e2)(r2 => KLet(z, KAop(op, r1, r2), k(KVar(z)))))}\end{lstlisting}\noindentWhat we essentially have to do in this case is the following: compilethe subexpressions \texttt{e1} and \texttt{e2}. They will produce someresult that is stored in two temporary variables (assuming they are morecomplicated than just numbers). We need to use these two temporaryvariables and feed them into a new assignment of the form\begin{lstlisting}[language=LLVMIR,numbers=none,escapeinside={(*@}{@*)}]let z = op (*@$\Box_\texttt{r1}$@*) (*@$\Box_\texttt{r2}$@*) in...\end{lstlisting}\noindentNote that this assignment has two ``holes'', one for the leftsubexpression and one for the right subexpression. We can fill bothholes by calling the CPS function twice---this is a bit of the blackart in CPS. We can use the second call of CPS as the continuationof the first call: The reason is that\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=0mm]r1 => CPS(e2)(r2 => KLet(z, KAop(op, r1, r2), k(KVar(z))))\end{lstlisting}\noindent is a function from \code{KVal} to \code{KExp}. Oncewe created the assignment with the fresh temporary variable\texttt{z}, we need to ``communicate'' that the result of thecomputation of the arithmetic expression is stored in \texttt{z} to thecomputations that follow. In this way we apply the continuation \texttt{k} with thisnew variable (essentially we are plugging in a hole further down the line).The last case we need to consider in our small expression language arefunction calls.\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=0mm]case Call(fname, args) => { def aux(args: List[Expr], vs: List[KVal]): KExp = args match { case Nil => { val z = Fresh("tmp") KLet(z, KCall(fname, vs), k(KVar(z))) } case a::as => CPS(a)(r => aux(as, vs ::: List(r))) } aux(args, Nil) }\end{lstlisting}\noindentFor them we introduce an auxiliary function that compiles first allfunction arguments---remember in our source language we can have callssuch as $foo(3 + 4, g(3))$ where we first have to create temporaryvariables (and computations) for each argument. Therefore \texttt{aux}analyses the arguments from left to right. In case there is an argument\texttt{a} on the front of the list (the case \texttt{a::as}), we callCPS recursively for the corresponding subexpression. The temporary variablecontaining the result for this argument we add to the end of the K-values wehave already analysed before. Again very conveniently we can use therecursive call to \texttt{aux} as the continuation for the computationsthat follow. If we reach the end of the argument list (the \texttt{Nil}-case),then we collect all the K-values \texttt{v1} to \texttt{vn} and call thefunction in the K-language like so\begin{lstlisting}[language=LLVMIR,numbers=none,escapeinside={(*@}{@*)}]let z = call foo(v1,...,vn) in...\end{lstlisting}\noindentAgain we need to communicate the result of the function call, namely thefresh temporary variable \texttt{z}, to the rest of the computation. Thereforewe apply the continuation \texttt{k} with this variable.\begin{figure}[p]\small \lstinputlisting[numbers=left,firstline=1,lastline=24]{../progs/fun/simple-cps.sc} \hspace{10mm}... \lstinputlisting[numbers=left,firstline=32,firstnumber=32,lastline=51]{../progs/fun/simple-cps.sc}\caption{CPS-translation for a simple expression language.\label{cps}}\end{figure}The last question we need to answer in the code (see Figure~\ref{cps}) is how westart the CPS-translation function, or more precisely with which continuation weshould start CPS? It turns out that this initial continuation will be the last one that iscalled. What should be the last step in the computation? Yes, we need to return thetemporary variable where the last result is stored (if it is a simple number, then we canjust return this number). Therefore we cal CPS with the code\begin{lstlisting}[language=Scala,numbers=none]def CPSi(e: Expr) : KExp = CPS(e)(KReturn(_))\end{lstlisting}\noindentwhere we give the function \code{KReturn(_)}. \begin{figure}[p]\small\begin{lstlisting}[language=Scala,numbers=none]// Fun language (expressions)abstract class Exp abstract class BExp case class Call(name: String, args: List[Exp]) extends Expcase class If(a: BExp, e1: Exp, e2: Exp) extends Expcase class Write(e: Exp) extends Expcase class Var(s: String) extends Expcase class Num(i: Int) extends Expcase class Aop(o: String, a1: Exp, a2: Exp) extends Expcase class Sequence(e1: Exp, e2: Exp) extends Expcase class Bop(o: String, a1: Exp, a2: Exp) extends BExp // K-language (K-expressions, K-values)abstract class KExpabstract class KValcase class KVar(s: String) extends KValcase class KNum(i: Int) extends KValcase class Kop(o: String, v1: KVal, v2: KVal) extends KValcase class KCall(o: String, vrs: List[KVal]) extends KValcase class KWrite(v: KVal) extends KValcase class KIf(x1: String, e1: KExp, e2: KExp) extends KExpcase class KLet(x: String, v: KVal, e: KExp) extends KExpcase class KReturn(v: KVal) extends KExp\end{lstlisting}\caption{Abstract syntax trees for the Fun-language.\label{absfun}}\end{figure}\noindent\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: