X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=fd0e2cb294a074dd2a101a62fdb68f47a2ea057d;hp=445c32389ad91ccd8f874ddbd49ebb8f7fa71682;hb=a9c202b10658a4993aae80b8fc986da14c6fe19e;hpb=9c009df865db69a97c1eac0d2de4a8fdab692c41 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 445c323..fd0e2cb 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -606,31 +606,44 @@ notations, which we will define here. \subsubsection{Other concepts} A \emph{global variable} is any variable that is bound at the -top level of a program, or an external module. A local variable is any other -variable (\eg, variables local to a function, which can be bound by lambda -abstractions, let expressions and case expressions). - -A \emph{hardware representable} type is a type that we can generate -a signal for in hardware. For example, a bit, a vector of bits, a 32 bit -unsigned word, etc. Types that are not runtime representable notably -include (but are not limited to): Types, dictionaries, functions. - -A \emph{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. +top level of a program, or an external module. A \emph{local variable} is any +other variable (\eg, variables local to a function, which can be bound by +lambda abstractions, let expressions and pattern matches of case +alternatives). Note that this is a slightly different notion of global versus +local than what \small{GHC} uses internally. +\defref{global variable} \defref{local variable} + +A \emph{hardware representable} (or just \emph{representable}) type or value +is (a value of) a type that we can generate a signal for in hardware. For +example, a bit, a vector of bits, a 32 bit unsigned word, etc. Types that are +not runtime representable notably include (but are not limited to): Types, +dictionaries, functions. +\defref{representable} + +A \emph{builtin function} is a function supplied by the Cλash framework, whose +implementation is not valid Cλash. The implementation is of course valid +Haskell, for simulation, but it is not expressable in Cλash. +\defref{builtin function} \defref{user-defined function} + +For these functions, Cλash has a \emph{builtin hardware translation}, so calls +to these functions can still be translated. These are functions like +\lam{map}, \lam{hwor} and \lam{length}. + +A \emph{user-defined} function is a function for which we do have a Cλash +implementation available. \subsubsection{Functions} Here, we define a number of functions that can be used below to concisely specify conditions. -\emph{gvar(expr)} is true when \emph{expr} is a variable that references a +\refdef{global variable}\emph{gvar(expr)} is true when \emph{expr} is a variable that references a global variable. It is false when it references a local variable. -\emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr} +\refdef{local variable}\emph{lvar(expr)} is the complement of \emph{gvar}; it is true when \emph{expr} references a local variable, false when it references a global variable. -\emph{representable(expr)} or \emph{representable(var)} is true when -\emph{expr} or \emph{var} has a type that is representable at runtime. +\refdef{representable}\emph{representable(expr)} or \emph{representable(var)} is true when +\emph{expr} or \emph{var} is \emph{representable}. \subsection{Binder uniqueness} A common problem in transformation systems, is binder uniqueness. When not