From 8821711ab53c9f3b9989262a11c003766011e96c Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Tue, 25 Aug 2009 16:49:41 +0200 Subject: [PATCH 1/1] Make Core2Core a chapter in the report. This removes some old definitions in the file and disables some content that needs rewriting. --- Core2Core.tex => Chapters/Normalization.tex | 329 +++++++------------- Report.tex | 1 + 2 files changed, 113 insertions(+), 217 deletions(-) rename Core2Core.tex => Chapters/Normalization.tex (74%) diff --git a/Core2Core.tex b/Chapters/Normalization.tex similarity index 74% rename from Core2Core.tex rename to Chapters/Normalization.tex index 5df2487..d36556b 100644 --- a/Core2Core.tex +++ b/Chapters/Normalization.tex @@ -1,103 +1,4 @@ -\mainlanguage [en] -\setuppapersize[A4][A4] - -% 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|} -\define[2]\app{#1\;#2} -\define[2]\lam{λ#1 \xrightarrow #2} -\define[2]\letexpr{{\bold let}\;#1\;{\bold in}\;#2} -\define[2]\case{{\bold case}\;#1\;{\bold of}\;#2} -\define[2]\alt{#1 \xrightarrow #2} -\define[2]\bind{#1:#2} -\define[1]\where{{\bold where}\;#1} -% A transformation -\definefloat[transformation][transformations] -\define[2]\transform{ - \startframedtext[width=\textwidth] - #2 - \stopframedtext -} - -\define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]} -\define\nextrule{\vskip1cm} - -\define[2]\transformold{ - %\placetransformation[here]{#1} - \startframedtext[width=\textwidth] - \startformula \startalign - #2 - \stopalign \stopformula - \stopframedtext -} - -% A shortcut for italicized e.g. and i.e. -\define[0]\eg{{\em e.g.}} -\define[0]\ie{{\em i.e.}} - -\definedescription - [desc] - [location=hanging,hang=20,width=broad] - %command=\hskip-1cm,margin=1cm] - -% Install the lambda calculus pretty-printer, as defined in pret-lam.lua. -\installprettytype [LAM] [LAM] - -\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 - % 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]\transbuf{ - % 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] -} -% This is the same as \transbuf above, but it accepts text directly instead -% of through buffers. This only works for single lines, however. -\define[2]\trans{ - \dontleavehmode - \lamframe{\lam{#1}} - \lamframe{\Rightarrow} - \lamframe{\lam{#2}} -} - +\chapter{Normalization} % 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. @@ -125,30 +26,24 @@ {\example{#3}}{Transformed program} \stopcombination } - -\define[3]\transexampleh{ -% \placeexample[here]{#1} -% \startcombination[1*2] -% {\example{#2}}{Original program} -% {\example{#3}}{Transformed program} -% \stopcombination -} - -% Define a custom description format for the builtinexprs below -\definedescription[builtindesc][headstyle=bold,style=normal,location=top] - -\starttext -\title {Core transformations for hardware generation} -Matthijs Kooijman - -\section{Introduction} -As a new approach to translating Core to VHDL, we investigate a number of -transforms on our Core program, which should bring the program into a -well-defined {\em normal} form, which is subsequently trivial to -translate to VHDL. - -The transforms as presented here are far from complete, but are meant as -an exploration of possible transformations. +% +%\define[3]\transexampleh{ +%% \placeexample[here]{#1} +%% \startcombination[1*2] +%% {\example{#2}}{Original program} +%% {\example{#3}}{Transformed program} +%% \stopcombination +%} + +The first step in the core to VHDL translation process, is normalization. We +aim to bring the core description into a simpler form, which we can +subsequently translate into VHDL easily. This normal form is needed because +the full core language is more expressive than VHDL in some areas and because +core can describe expressions that do not have a direct hardware +interpretation. + +TODO: Describe core properties not supported in VHDL, and describe how the +VHDL we want to generate should look like. \section{Goal} The transformations described here have a well-defined goal: To bring the @@ -205,29 +100,29 @@ constraints. TODO: Update this section, this is probably not completely accurate or relevant anymore. \startitemize[R,inmargin] -\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$. -$fun$ is an identifier that will be bound as a global identifier. -\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or -$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$. -\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$. -\item $letbinds$ is a list with elements of the form -$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is -an identifier that will be bound as local identifier. The type of the bound -value must be a $hardware\;type$. -\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an -equivalent VHDL expression. Since there are many supported forms for this, -these are defined in a separate table. -\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$, -where $fun$ is a global identifier and $x$ is a local identifier. -\item[retexpr] A $retexpr$ has the form $\expr{x}$ or $\expr{tupexpr}$, where $x$ is a local identifier that is bound as an $argument$ or $result$. A $retexpr$ must -be of a $hardware\;type$. -\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$, -where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is -a local identifier. -\item A $hardware\;type$ is a type that can be directly translated to -hardware. This includes the types $Bit$, $SizedWord$, tuples containing -elements of $hardware\;type$s, and will include others. This explicitely -excludes function types. +%\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$. +%$fun$ is an identifier that will be bound as a global identifier. +%\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or +%$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$. +%\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$. +%\item $letbinds$ is a list with elements of the form +%$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is +%an identifier that will be bound as local identifier. The type of the bound +%value must be a $hardware\;type$. +%\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an +%equivalent VHDL expression. Since there are many supported forms for this, +%these are defined in a separate table. +%\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$, +%where $fun$ is a global identifier and $x$ is a local identifier. +%\item[retexpr] A $retexpr$ has the form $\expr{x}$ or $\expr{tupexpr}$, where $x$ is a local identifier that is bound as an $argument$ or $result$. A $retexpr$ must +%be of a $hardware\;type$. +%\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$, +%where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is +%a local identifier. +%\item A $hardware\;type$ is a type that can be directly translated to +%hardware. This includes the types $Bit$, $SizedWord$, tuples containing +%elements of $hardware\;type$s, and will include others. This explicitely +%excludes function types. \stopitemize TODO: Say something about uniqueness of identifiers @@ -236,12 +131,12 @@ TODO: Say something about uniqueness of identifiers A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms. \startitemize[m,inmargin] -\item -$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$, -where $t$ can be any local identifier, $con$ is a tuple constructor ({\em -e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can -be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$. -\item TODO: Many more! +%\item +%$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$, +%where $t$ can be any local identifier, $con$ is a tuple constructor ({\em +%e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can +%be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$. +%\item TODO: Many more! \stopitemize \section{Transform passes} @@ -312,19 +207,19 @@ case x of pn -> En M \stopbuffer -\transform{Extended β-reduction} -{ -\conclusion -\trans{(λx.E) M}{E[M/x]} - -\nextrule -\conclusion -\trans{(let binds in E) M}{let binds in E M} - -\nextrule -\conclusion -\transbuf{from}{to} -} +%\transform{Extended β-reduction} +%{ +%\conclusion +%\trans{(λx.E) M}{E[M/x]} +% +%\nextrule +%\conclusion +%\trans{(let binds in E) M}{let binds in E M} +% +%\nextrule +%\conclusion +%\transbuf{from}{to} +%} \startbuffer[from] let a = (case x of @@ -482,16 +377,16 @@ a new let expression around the application, which binds the complex expression to a new variable. The original function is then applied to this variable. -\transform{Argument extract} -{ -\lam{Y} is of a hardware representable type - -\lam{Y} is not a variable referene - -\conclusion - -\trans{X Y}{let z = Y in X z} -} +%\transform{Argument extract} +%{ +%\lam{Y} is of a hardware representable type +% +%\lam{Y} is not a variable referene +% +%\conclusion +% +%\trans{X Y}{let z = Y in X z} +%} \subsubsection{Function extraction} This transform deals with function-typed arguments to builtin functions. @@ -503,24 +398,24 @@ parameters to the new global function. The original argument is replaced with a reference to the new function, applied to any free variables from the original argument. -\transform{Function extraction} -{ -\lam{X} is a (partial application of) a builtin function - -\lam{Y} is not an application - -\lam{Y} is not a variable reference - -\conclusion - -\lam{f0 ... fm} = free local vars of \lam{Y} - -\lam{y} is a new global variable - -\lam{y = λf0 ... fn.Y} - -\trans{X Y}{X (y f0 ... fn)} -} +%\transform{Function extraction} +%{ +%\lam{X} is a (partial application of) a builtin function +% +%\lam{Y} is not an application +% +%\lam{Y} is not a variable reference +% +%\conclusion +% +%\lam{f0 ... fm} = free local vars of \lam{Y} +% +%\lam{y} is a new global variable +% +%\lam{y = λf0 ... fn.Y} +% +%\trans{X Y}{X (y f0 ... fn)} +%} \subsubsection{Argument propagation} This transform deals with arguments to user-defined functions that are @@ -585,29 +480,29 @@ x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local v 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 - -\lam{x = E} - -\lam{Y_i} is not of a runtime representable type - -\lam{Y_i} is not a local variable reference - -\conclusion - -\lam{f0 ... fm} = free local vars of \lam{Y_i} - -\lam{x'} is a new global variable - -\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn} - -\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn} -} - -TODO: The above definition looks too complicated... Can we find -something more concise? +%\transform{Argument propagation} +%{ +%\lam{x} is a global variable, bound to a user-defined function +% +%\lam{x = E} +% +%\lam{Y_i} is not of a runtime representable type +% +%\lam{Y_i} is not a local variable reference +% +%\conclusion +% +%\lam{f0 ... fm} = free local vars of \lam{Y_i} +% +%\lam{x'} is a new global variable +% +%\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn} +% +%\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn} +%} +% +%TODO: The above definition looks too complicated... Can we find +%something more concise? \subsection{Cast propagation} This transform pushes casts down into the expression as far as possible. diff --git a/Report.tex b/Report.tex index 1ef9fee..c80a916 100644 --- a/Report.tex +++ b/Report.tex @@ -18,6 +18,7 @@ Matthijs Kooijman \completecontent \chapter{Introduction} +\input Chapters/Normalization \input Chapters/State \chapter{Normalization} \chapter{VHDL generation} -- 2.30.2