From: Matthijs Kooijman <m.kooijman@student.utwente.nl>
Date: Mon, 27 Jul 2009 11:38:04 +0000 (+0200)
Subject: Use the transformation pretty printer.
X-Git-Tag: final-thesis~310
X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=e9dcbb3cec03ea21a3d26842ba9d4f3c006bb864

Use the transformation pretty printer.

This changes two transformations to use the new pretty printer, the rest
still needs to be converted.
---

diff --git a/Core2Core.tex b/Core2Core.tex
index b404a03..5df2487 100644
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -60,6 +60,9 @@
 \definetyping[lambda][option=LAM,style=sans]
 \definetype[lam][option=LAM,style=sans]
 
+\installprettytype [TRANS] [TRANS]
+\definetyping[trans][option=TRANS,style=normal,before=,after=]
+
 % An (invisible) frame to hold a lambda expression
 \define[1]\lamframe{
         % Put a frame around lambda expressions, so they can have multiple
@@ -269,20 +272,12 @@ expression are named, by introducing lambda expressions. When combined with
 β-reduction and function inlining below, all function-typed expressions should
 be lambda abstractions or global identifiers.
 
-\transform{η-abstraction}
-{
-\lam{E :: * -> *}
-
-\lam{E} is not the first argument of an application.
-
-\lam{E} is not a lambda abstraction.
-
-\lam{x} is a variable that does not occur free in E.
-
-\conclusion
-
-\trans{E}{λx.E x}
-}
+\starttrans
+E                 \lam{E :: * -> *}
+--------------    \lam{E} is not the first argument of an application.
+λx.E x            \lam{E} is not a lambda abstraction.
+                  \lam{x} is a variable that does not occur free in \lam{E}.
+\stoptrans
 
 \startbuffer[from]
 foo = λa -> case a of 
@@ -579,6 +574,17 @@ Definition: A builtin function is a function for which a builtin
 hardware translation is available, because its actual definition is not
 translatable. A user-defined function is any other function.
 
+\starttrans
+x = E
+~
+x Y0 ... Yi ... Yn                               \lam{Y_i} is not of a runtime representable type
+---------------------------------------------    \lam{Y_i} is not a local variable reference
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
+      E y0 ... yi-1 Yi yi+1 ... yn   
+~
+x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
+\stoptrans
+
 \transform{Argument propagation}
 {
 \lam{x} is a global variable, bound to a user-defined function
diff --git a/SConstruct b/SConstruct
index d805605..4e2e3e5 100644
--- a/SConstruct
+++ b/SConstruct
@@ -67,6 +67,7 @@ env['ENV']['SSH_AUTH_SOCK'] = os.environ['SSH_AUTH_SOCK']
 ## Context PDF build
 pdfOutput = env.Context(LATEX_PROJECT)
 Depends(pdfOutput, 'pret-lam.lua')
+Depends(pdfOutput, 'pret-trans.lua')
 env.Alias('pdf', LATEX_PROJECT + '.pdf')
 
 # Keep below code happy