Add support for pretty printing lambda calculus.

[matthijs/master-project/report.git] / Core2Core.tex

diff --git a/Core2Core.tex b/Core2Core.tex
index d62807715c21bd530530fd2077cb5a285136a9f9..bc385a68324b210e435dbe1f42cbfed975099f8a 100644 (file)
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -1,9 +1,20 @@
 \mainlanguage [en]
 \setuppapersize[A4][A4]
 
-\setupbodyfont[10pt]
-%\usetypescript [lbr][ec]
-%\switchtotypeface [lbr] [10pt]
+% Define a custom typescript. We could also have put the \definetypeface's
+% directly in the script, without a typescript, but I guess this is more
+% elegant...
+\starttypescript[Custom]
+% This is a sans font that supports greek symbols
+\definetypeface [Custom] [ss] [sans]  [iwona]                [default]
+\definetypeface [Custom] [rm] [serif] [antykwa-torunska]     [default]
+\definetypeface [Custom] [tt] [mono]  [modern]               [default]
+\definetypeface [Custom] [mm] [math]  [modern]               [default]
+\stoptypescript
+\usetypescript [Custom]
+
+% Use our custom typeface
+\switchtotypeface [Custom] [10pt]
 
 % The function application operator, which expands to a space in math mode
 \define[1]\expr{|#1|}
@@ -25,6 +36,9 @@
   \stopframedtext
 }
 
+% Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
+\installprettytype [LAM] [LAM]
+
 % A helper to print a single example in the half the page width. The example
 % text should be in a buffer whose name is given in an argument.
 %
@@ -63,7 +77,7 @@ Matthijs Kooijman
 \section{Introduction}
 As a new approach to translating Core to VHDL, we investigate a number of
 transformations on our Core program, which should bring the program into a
-well-defined "canonical" state, which is subsequently trivial to translate to
+well-defined "canonical" form, which is subsequently trivial to translate to
 VHDL.
 
 The transformations as presented here are far from complete, but are meant as
@@ -73,16 +87,16 @@ apparent from the end result, there will be additional transformations needed
 to fully reach our goal, and some transformations must be applied more than
 once. How exactly to (efficiently) do this, has not been investigated.
 
-Lastly, I hope to be able to state a number of pre- and postconditinos for
+Lastly, I hope to be able to state a number of pre- and postconditions for
 each transformation. If these can be proven for each transformation, and it
-can be shown that ther exists some ordering of transformations for which the
+can be shown that there exists some ordering of transformations for which the
 postcondition implies the canonical form, we can show that the transformations
 do indeed transform any program (probably satisfying a number of
 preconditions) to the canonical form.
 
 \section{Goal}
 The transformations described here have a well-defined goal: To bring the
-program in a well-defined program that is directly translatable to hardware,
+program in a well-defined form that is directly translatable to hardware,
 while fully preserving the semantics of the program.
 
 This {\em canonical form} is again a Core program, but with a very specific
@@ -214,14 +228,14 @@ canonical form.
     in
       case s of
         (a, b) ->
-          r = case a of
-                High -> add
-                Low -> let
-                  op' = case b of
-                    High -> sub
-                    Low  -> \c d -> c
-                  in
-                    \c d -> op' d c
+          case a of
+            High -> add
+            Low -> let
+              op' = case b of
+                High -> sub
+                Low  -> \c d -> c
+              in
+                \c d -> op' d c
 \stoptyping
 
 \subsection{Argument extraction}