\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|}
\stopframedtext
}
+% Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
+\installprettytype [LAM] [LAM]
+
+\definetyping[lambda][option=LAM,style=sans]
+
+% An (invisible) frame to hold a lambda expression
+\define[1]\lamframe{
+ % Put a frame around lambda expressions, so they can have multiple
+ % lines and still appear inline.
+ % The align=right option really does left-alignment, but without the
+ % program will end up on a single line. The strut=no option prevents a
+ % bunch of empty space at the start of the frame.
+ \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
+}
+
+\define[2]\trans{
+ % Make \typebuffer uses the LAM pretty printer and a sans-serif font
+ % Also prevent any extra spacing above and below caused by the default
+ % before=\blank and after=\blank.
+ \setuptyping[option=LAM,style=sans,before=,after=]
+ % Prevent the arrow from ending up below the first frame (a \framed
+ % at the start of a line defaults to using vmode).
+ \dontleavehmode
+ % Put the elements in frames, so they can have multiple lines and be
+ % middle-aligned
+ \lamframe{\typebuffer[#1]}
+ \lamframe{\Rightarrow}
+ \lamframe{\typebuffer[#2]}
+ % Reset the typing settings to their defaults
+ \setuptyping[option=none,style=\tttf]
+}
+
% 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.
%
\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
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
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}
\item More builtin expressions should be added and these should be evaluated
by the compiler. For example, map, fold, +.
\stopitemize
+
+Initial example
+
+\startlambda
+ λx.
+ let s = foo x
+ in
+ case s of
+ (a, b) ->
+ case a of
+ High -> add
+ Low -> let
+ op' = case b of
+ High -> sub
+ Low -> λc.λd.c
+ in
+ λc.λd.op' d c
+\stoplambda
+
+After top-level η-abstraction:
+
+\startlambda
+ λx.λc.λd.
+ (let s = foo x
+ in
+ case s of
+ (a, b) ->
+ case a of
+ High -> add
+ Low -> let
+ op' = case b of
+ High -> sub
+ Low -> λc.λd.c
+ in
+ λc.λd.op' d c
+ ) c d
+\stoplambda
+
+After (extended) β-reduction:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ in
+ case s of
+ (a, b) ->
+ case a of
+ High -> add c d
+ Low -> let
+ op' = case b of
+ High -> sub
+ Low -> λc.λd.c
+ in
+ op' d c
+\stoplambda
+
+After return value extraction:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ r = case s of
+ (a, b) ->
+ case a of
+ High -> add c d
+ Low -> let
+ op' = case b of
+ High -> sub
+ Low -> λc.λd.c
+ in
+ op' d c
+ in
+ r
+\stoplambda
+
+Scrutinee simplification does not apply.
+
+After case binder wildening:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) ->
+ case a of
+ High -> add c d
+ Low -> let op' = case b of
+ High -> sub
+ Low -> λc.λd.c
+ in
+ op' d c
+ in
+ r
+\stoplambda
+
+After case value simplification
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = let rll = λc.λd.c
+ op' = case b of
+ High -> sub
+ Low -> rll
+ in
+ op' d c
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After let flattening:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = op' d c
+ rll = λc.λd.c
+ op' = case b of
+ High -> sub
+ Low -> rll
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After function inlining:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = (case b of
+ High -> sub
+ Low -> λc.λd.c) d c
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After (extended) β-reduction again:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = case b of
+ High -> sub d c
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After case value simplification again:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After case removal:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After let bind removal:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r'
+\stoplambda
+
+Application simplification is not applicable.
\stoptext
projects / matthijs / master-project / report.git / blobdiff