y = \overrightarrow x \bullet \overrightarrow h
\]
\end{frame}
+\note[itemize]{
+\item FIR filter doet niks meer dat inproduct toepassen op een aantal waardes.
+\item Next sheet: uitleg dot product
+}
\begin{frame}
\frametitle{Dot Product}
\overrightarrow x \bullet \overrightarrow h = \sum\nolimits_{i = 1}^n {a_1 \cdot b_1 + a_2 \cdot b_2 + \ldots + a_n \cdot b_n }
\]
\end{frame}
+\note[itemize]{
+\item Inproduct is niks anders dan het paarsgewijs vermenigvuldigen en dan optellen van 2 lijsten.
+\item Next sheet: de operaties die same dotproduct vormen
+}
\begin{frame}
\frametitle{Dot Product}
\]
\begin{itemize}
\item \emph{Pairwise Multiplication}: \\
- \begin{verbatim}
+ \begin{code}
zipwith (*) xs hs =
< x0*h0, x1*h1, x(n-1)*h(n-1)>
- \end{verbatim}
+ \end{code}
\item \emph{Summation}: \\
- \begin{verbatim}
+ \begin{code}
foldl (+) 0 zs =
(..((0+z0)+z1)+..+z(n-1))
- \end{verbatim}
+ \end{code}
\end{itemize}
\end{itemize}
\end{frame}
+\note[itemize]{
+\item Paarsgewijs vermenigvuldigen gebeurd met zipWith functie. zipWith voegt twee lijsten samen door op de elementen uit de lijst en functie toe te passen. In dit voorbeeld dus vermenigvuldiging.
+\item Foldl vouwt een lijst op door een functie herhaaldelijk op elk opvolgend element toe te passen, en zo dus een lijst te reduceren tot een enkele waarde. Nu dus dmv optelling.
+\item Next sheet: samenvoegen tot 1 functie
+}
\begin{frame}
\frametitle{Dot Product}
\]
\begin{itemize}
\item \emph{Combine the two}: \\
- \begin{verbatim}
- xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
- \end{verbatim}
+ \begin{code}
+ xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
+ \end{code}
\end{itemize}
\end{itemize}
-\end{frame}
\ No newline at end of file
+\end{frame}
+\note[itemize]{
+\item Samen vormen deze operaties dus het inproduct.
+\item Next sheet: code FIR filter
+}
\ No newline at end of file
\]
\end{itemize}
\end{frame}
+\note[itemize]{
+\item FIR filter is een digitaal filter.
+\item Filters worden gebruik om bepaalde eigenschappen van een radiosignaal te versterken of te verzwakken.
+\item Filters zijn een belangrijk onderdeel in mobiele telefonie
+\item Next Sheet: Beschrijving formule
+}
\begin{frame}
\frametitle{FIR Filter}
y_t = \sum\nolimits_{i = 0}^{n - 1} {x_{t - i} \cdot h_i }
\]
\end{frame}
+\note[itemize]{
+\item De formule zegt niks meer dan:
+\item Vermenigvuldig het signaal van meerdere tijdsmomenten (X\_t t/m X\_(t-n)) met bepaalde (moglijk negatief) getallen (H\_i), en tel deze waarden bij elkaar op.
+\item Next Sheet: Dot-product
+}
\input{christiaan/dotproduct}
\[
y_t = \sum\nolimits_{i = 0}^{n - 1} {x_{t - i} \cdot h_i }
\] \\
- \begin{verbatim}
+ \begin{code}
fir (State pxs) x = (pxs**hs, State (pxs<++x))
where hs = $(vectorTH [2::Int16,3,-2,4])
- \end{verbatim}
+ \end{code}
\centerline{\begin{tabular}{rl}
|pxs| & Previous x's (state)\\
|x| & New input value\\
|pxs <++ x| & Remember new |x|, remove oldest\\
|pxs ** hs| & Output
\end{tabular}}
-
\end{frame}
+\note[itemize]{
+\item Zie hier dus de code voor het FIR filter
+\item Er zijn zoals je ziet 4 getallen, coefficienten, die vermenigvuldigt moeten worden.
+\item In |pxs| komen dus 4 waarden van X te staan.
+\item de |<++| operatie schuift er steeds een nieuwe X in, en gooit de oudste er uit.
+\item Je zie ook het inproduct, |**|, terug
+\item Next sheet: demo
+}
\begin{frame}
\frametitle{FIR Filter}
\centerline{\Huge{Demo}}
\end{frame}
+\note[itemize]{
+\item Code laten zien
+\item Code compilen
+\item Next sheet: synthese output
+}
\begin{frame}
\frametitle{Synthesized Output}
\vspace{-0.8em}
\begin{figure}
- \centerline{\includegraphics[width=\paperwidth,trim=9mm 14cm 14mm 16cm, clip=true]{fir0.png}}
- \end{figure}
-\end{frame}
-
-\begin{frame}
- \frametitle{Synthesized Output}
- \vspace{-0.8em}
- \begin{figure}
- \centerline{\includegraphics[width=\paperwidth,trim=9mm 15cm 16.5cm 11cm, clip=true]{fir1.png}}
+ \centerline{
+\includegraphics<1>[width=\paperwidth,trim=9mm 14cm 14mm 16cm, clip=true]{fir0.png}
+\includegraphics<2>[width=\paperwidth,trim=9mm 15cm 16.5cm 11cm, clip=true]{fir1.png}
+\includegraphics<3>[width=\paperwidth,trim=3cm 13cm 4cm 11cm, clip=true]{fir2.png}}
\end{figure}
\end{frame}
-
-\begin{frame}
- \frametitle{Synthesized Output}
- \vspace{-0.8em}
- \begin{figure}
- \centerline{\includegraphics[width=\paperwidth,trim=3cm 13cm 4cm 11cm, clip=true]{fir2.png}}
- \end{figure}
-\end{frame}
\ No newline at end of file
+\note[itemize]{
+\item Overzicht van de hardware
+\item De 4 geheugen elementen
+\item Aan de linkerkant de 4 vermenigvuldiger, rechts de 3 optellers
+\item Next Sheet: Structuur / grootte afleiden
+}
\ No newline at end of file
\section{Presentation Christiaan}
\frame{\titlepage \setcounter{framenumber}{1}}
+\note[itemize]{
+\item Beginnen met een voorbeeld
+\item Van een wiskundige beschrijving naar hardware
+\item Next Sheet: FIR
+}
\input{christiaan/fir}
\input{christiaan/structure}
\item Unexplored solution: Haskell language extensions, new source language
\end{itemize}
}
+\note[itemize]{
+\item Afsluitend nog het meest voor de hand liggende future work: het ondersteunen van recursie.
+\item Er zijn al wat mogelijkheden onderzocht: static loop unrolling, waar ik zo wat over vertel.
+\item Andere mogelijkheden zijn het op zoek gaan naar een taal die wel echt ondersteuning heeft voor dependent types. Daar later meer over.
+\item Next sheet: static loop unrolling
+}
\subsubsection{Static loop unrolling}
\frame{
\item Explored solution: Unrolling number-guided recursive functions using Template Haskell
\end{itemize}
}
+\note[itemize]{
+\item Static loop unrolling, is het op compile-time uitrollen van recursieve functies totdat er geen recursie meer is. Je moet de functies ook simplificeren omdat je de choice-logic die de recursie leidt wil verwijderen.
+\item Ik heb gekeken naar het uitrollen van number-guided recursive functies, met gehulp van Template Haskell.
+\item Next sheet: Template Haskell uitleg
+}
\frame{
\frametitle{Template Haskell}
\item All these functions are expressible in normal Haskell
\end{itemize}
}
+\note[itemize]{
+\item Ik heb vooral naar Template Haskell gekeken, omdat toekomstig gebruikes van \clash{} ook beschikking hebben om TH te kunnen gebruiken. Zonder dat ze direct de compiler in moeten duiken.
+\item TH staat het toe om code op compile-time te inspecteren, te creeeren en te veranderen.
+\item En dit kan allemaal met behulp van normale Haskell code
+\item Next sheet: voorbeeld uitrollen tree adder
+}
\frame{
\frametitle{Tree Adder}
-\begin{verbatim}
+\begin{code}
$(do
[typ, _] <- [d|{
-treeSum :: Vector D8 (SizedWord D8) -> SizedWord D8;
+{-"{\color<2>[rgb]{1,0,0}"-}treeSum :: Vector D8 (SizedWord D8) -> SizedWord D8;{-"}"-}
treeSum xs = undefined
}|]
[func] <- [d|{
-treeSum i xs | i < 1 = head xs
- | otherwise = let (a,b) = split xs
- in (treeSum (i-1) a) +
- (treeSum (i-1) b)
+{-"{\color<3>[rgb]{1,0,0}"-}treeSum i xs | i < 1 = head xs{-"}"-}
+{-"{\color<3>[rgb]{1,0,0}"-} | otherwise = let (a,b) = split xs{-"}"-}
+{-"{\color<3>[rgb]{1,0,0}"-} in (treeSum (i-1) a) +{-"}"-}
+{-"{\color<3>[rgb]{1,0,0}"-} (treeSum (i-1) b){-"}"-}
}|]
- let func' = unroll Nothing 0 (IntegerL 3) funct
- return [typ,func']
+{-"{\color<4>[rgb]{1,0,0}"-} let func' = unroll Nothing 0 (IntegerL 3) func{-"}"-}
+{-"{\color<5>[rgb]{1,0,0}"-} return [typ,func']{-"}"-}
)
-\end{verbatim}
+\end{code}
+}
+\note[itemize]{
+\item Zie hier een recursieve tree adder die ik uitroll naar 3 diep d.m.v. template haskell
+\item Zie de function signature bovenaan.
+\item Dan de de recursieve treeSum functie
+\item Dan de unroll functie die deze treeSum functie uitrolt
+\item En dan voegen we de uitegerolde functie weer in
+\item Next sheet: schema uitgerolde tree adder
}
\begin{frame}
\includegraphics[height=5cm]{treeadder}
\end{figure}
\end{frame}
+\note[itemize]{
+\item Hier een schema van uitgerolde tree-adder voor 3 diep
+\item Volgende sheet: Aanpassingen input taal voor \clash{}
+}
\subsubsection{Input Language}
\frame{
\item New source language: One of the problems is that Haskell does not properly support dependent types. Investigate languages with dependent type systems.
\item Haskell extentions: Invariant descriptions at the type-level.
\end{itemize}
+}
+\note[itemize]{
+\item Ondersteuning van dependent types is niet echt bestaand in Haskell. Is meer op een ad-hoc manier mogelijk, maar is bij ontwerp van het type-systeem nooit de bedoeling geweest.
+\item Daarom zou er gekeken moeten worden naar een echte dependently typed taal. Die het hopelijk makkelijker maakt om invarianten te specificeren, en is toe te voegen aan de code.
+\item Of er moet worden gekeken of er in Haskell de mogelijkheid bestaat om invarianten op type-niveau toe te voegen.
+\item Next sheet: vragen
}
\ No newline at end of file
\item Is \clash{} too restrictive given the fact that a designer can currently not define his own vector transformations, or recursive functions for that matter?
\end{itemize}
}
+\note[itemize]{
+\item Je kan je natuurlijk afvragen of er nu niet teveel restricties zijn binnen \clash{}. Dit valt op zich wel mee, gezien veel gebruikte lijst-functies, zoals: map, zipwith, fold, enzo wel beschikbaar zijn
+\item next sheet: expressief genoeg voor reductiecircuit
+}
\frame{
\frametitle{Too Restrictive?}
\item Example: Reduction circuit
\end{itemize}
}
+\note[itemize]{
+\item Recursieve functies zijn soms wel een gemis, en er is ook zeker ruimte om de expressiviteit van \clash{} uit te breiden. Maar we kunnen al wel niet-triviale ontwerpen maken, zoals het reductiecircuit wat ik nu ga laten zien.
+\item Next sheet: beschrijving reductie circuit
+}
\subsection{Reduction circuit}
\end{itemize}
\end{columns}
}
+\note[itemize]{
+\item Reductiecircuit telt voor alle rijen, de getallen uit zo'n rij bij elkaar op.
+\item Het probleem is niet triviaal, omdat resultaten met een bepaalde vertraging uit de opteller komen vanwege pipelining. Triviale oplossing zoals een simpel accumulate register zijn niet mogelijk omdat dan per ongelijk meerdere rijen bij elkaar opgeteld worden. Ook kan je niet wachten op het resultaat, omdat je mogelijk een oneindig grote input buffer nodig hebt.
+\item Daarom heb je speciale controle logica nodig die bijhoud welke waarden er in de opteller zitten.
+\item De grootste beperking in het ontwerp is niet het gebrek aan recursieve functies, maar het gebrek aan dynamishe lijsten.
+\item next sheet: synthese output reductie circuit
+}
\begin{frame}
\begin{figure}
\includegraphics[height=9cm]{reducerschematic}
\end{figure}
\end{frame}
-
+\note[itemize]{
+\item Zie hier het werkelijke circuit
+\item Next sheet: fifo buffer wens
+}
\begin{frame}
\frametitle{FIFO Buffer}
\begin{itemize}
\item Wish:
-\begin{verbatim}
+\begin{code}
fifo :: (State mem) (input, shift) =
(State mem', out1, out2)
where
| otherwise = head mem
out2 | length mem < 2 = NotValid
| otherwise = head (tail mem)
- mem' = drop shift mem ++ [input]
-\end{verbatim}
+ {-"{\color<2>[rgb]{1,0,0}"-}mem' = drop shift mem ++ [input]{-"}"-}
+\end{code}
\end{itemize}
\end{frame}
+\note[itemize]{
+\item Hier het gewenste ontwerp van de input (FIFO) buffer.
+\item Zie vooral de laatste regel. De lengte van mem' is afhankelijk van de waarde van shift. Dus dynamish.
+\item Next sheet: fifo buffer realiteit
+}
\begin{frame}
\frametitle{FIFO Buffer}
\begin{itemize}
\item Reality:
-\begin{verbatim}
+\begin{code}
fifo :: (State (Fifo {..})) (inp, shift) =
( State (Fifo { mem = mem'
, ptr = ptr'
, out1, out2
)
where
- ptr' = ptr - shift + 1
- mem'' = replace mem ptr (Valid inp)
- mem' | shift == 0 = mem''
- | shift == 1 = (tail mem'') <+ NotValid
- | otherwise = ((tail (tail mem'')
- <+ NotValid) <+ NotValid)
+ {-"{\color<2>[rgb]{1,0,0}"-}ptr' = ptr - shift + 1{-"}"-}
+ {-"{\color<2>[rgb]{1,0,0}"-}mem'' = replace mem ptr (Valid inp){-"}"-}
+ {-"{\color<2>[rgb]{1,0,0}"-}mem' | shift == 0 = mem''{-"}"-}
+ {-"{\color<2>[rgb]{1,0,0}"-} | shift == 1 = (tail mem'') <+ NotValid{-"}"-}
+ {-"{\color<2>[rgb]{1,0,0}"-} | otherwise = ((tail (tail mem''){-"}"-}
+ {-"{\color<2>[rgb]{1,0,0}"-} <+ NotValid) <+ NotValid){-"}"-}
out1 = head mem
out2 = head (tail mem)
-\end{verbatim}
+\end{code}
\end{itemize}
\end{frame}
+\note[itemize]{
+\item Die dynamishe lijsten hebben we dus niet in \clash{}
+\item Daarom moeten we heel veel logica toevoegen om iets te maken wat het gedrag van een dynamishe lijst emuleert.
+\item Next sheet: dynamish vs statisch
+}
\frame{
\frametitle{FIFO Buffer}
\item Reality: Statically sized vectors
\end{itemize}
}
+\note[itemize]{
+\item Dus, de wens is dynamishe lijsten, en de realiteit is statische lijsten. Dit omdat statische lijsten veel makelijker naar hardware zijn te mappen. Ze zijn gewoon 1-op-1 te kopieren.
+\item Dynamische lijsten moeilijk, ik kan niet op run-time extra hardware maken. Wat bij software wel gebeurd: gewoon meer RAM alloceren
+\item Next sheet: problemen/mogelijkheden dynamische lijsten
+}
\frame{
\frametitle{Dynamically Sized Vectors}
\item How do we determine maximum size?
\end{itemize}
\end{itemize}
+}
+\note[itemize]{
+\item Wat zijn dan mogelijkheden voor dynamische lijsten?
+\item Alle lijsten naar RAMs mappen... maar dan is er wel extra logica nodig om de lengte bij te houden. Wat gebeurd er als de RAM eenheid vol is?
+\item We kunnen ook proberen om de operaties te vertalen naar shift/circulaire buffers... Maar dan moeten we dus wel data-access analyse doen... en we moeten de maximale lengte kunnen bepalen...
+\item Allemaal niet triviaal dus
+\item Next sheet: belangrijkste future work, recursie
}
\ No newline at end of file
%include talk.fmt
\frame{
\frametitle{Structure}
-\begin{verbatim}
+\begin{code}
fir (State pxs) x = (pxs**hs, State (pxs<++x))
where hs = $(vectorTH [2::Int16,3,-2,4])
-\end{verbatim}
+\end{code}
\begin{itemize}
\item How did we know how big the circuit would have to be? e.g. How many multipliers?
\item The size of the circuit is determined by the size of the vectors!
\end{itemize}
}
+\note[itemize]{
+\item Wat bepaald nu precies de grootte van het circuit? het aantal optellers en het aantal vermenigvuldigers.
+\item De grootte van de vectoren is van een groot belang voor het bepalen van de grootte en aantal elementen in een circuit.
+\item Next sheet: hoe bepalen we grootte vectors?
+}
\frame{
\frametitle{Structure}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Hoe bepalen we nu de lengte van de vectoren?
+\item We kunnen proberen af te leiden of een ontwerper ze laten opgeven
+\item Next sheet: grootte afleiden
+}
\subsubsection{Size Inference}
\frame{
\item Requires a lot of bookkeeping.
\end{itemize}
}
+\note[itemize]{
+\item We kunnen het aantal elementen tellen van lijsten waarvan de elementen expliciet zijn opgegeven. Zoals de coefficenten in het FIR filter.
+\item Proberen om andere vectoren van deze vectoren af te leiden.
+\item Veel boekhoudwerk, we moeten alle afgeleide lengten opslaan, en daarbij vectoren uniek kunnen bepalen: Van welke vector willen we afleiden?
+\item Next sheet: problemen grootte afleiden
+}
\frame{
\frametitle{Infer Size}
\item Might not be possible in the general case?
\item What is the size of the combinatorial circuit seen below? Infinite? Zero?
\end{itemize}
-\begin{verbatim}
- xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
-\end{verbatim}
+\begin{code}
+ xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
+\end{code}
+}
+\note[itemize]{
+\item Kunnen we wel voor elke vector de lengte afleiden?
+\item Er vanuitgaande dat xs en hs van buiten de chip komen, wat zijn dan de lengten van xs en hs? Hoe moeten die worden afgeleid?
+\item Next sheet: grootte specificeren
}
\subsubsection{Size Specification}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Om (tijdelijk) deze problemen te voorkomen laten we de hardware ontwerper de lengte van de vector opgeven.
+\item Hier hebben we ook weer twee mogelijkheden:
+\item Bij elke instantie de lengte opgeven
+\item Een instantie van een voorafgedefineerd type laten zijn, waarbij het type de lengte informatie bevat.
+\item Next sheet: Basisconcepten programmeren
+}
\frame{
\frametitle{Some basic concepts}
\item Computations can be assigned types to indicate what kind of values to produce or manipulate
\end{itemize}
}
+\note[itemize]{
+\item Even, helaas, een paar defenities
+\item Met programmeertalen druk je dus berekeningen uit
+\item Berekening bewerken waarden
+\item Types worden gebruikt om sets van waarden aan te geven. Bijvoorbeeld het Integer type omvat alle waarden die behoren tot gehele getalen.
+\item Berekeningen kunnen we types toekennen, om aan te geven wat voor waarden ze op moeten leveren, en wat voor waarden ze bewerken
+\item Types geven dus extra informatie over een programma, en helpen bij het detecteren van fouten van de programmeur
+\item Next sheet: Specificeren term level
+}
\frame{
\frametitle{Specify Size (term-level)}
+\begin{code}
+data Vector a = Vec Int a
+\end{code}
\begin{itemize}
\item Size specification at the instance / term level suffers from the same problems as size inference:
\begin{itemize}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Als we per vector gaan specificeren wat de lengte is krijgen we weer dezelfde soort problemen als we hadden met het afleiden van lengten.
+\item We moeten weer vanalles bijhouden
+\item Ook is er weer het probleem dat we niet kunnen vastleggen wat lengte is van vectoren die van buiten komen.
+\item Next sheet: specificeren type-level
+}
\frame{
\frametitle{Specify Size (type-level)}
\item The size of the vector becomes part of the type:
\begin{itemize}
\item Unconstrained Vectors:
- \begin{verbatim}
+ \begin{code}
Nat n => Vector n a
- \end{verbatim}
+ \end{code}
\item Constrained Vectors:
- \begin{verbatim}
-Vector 4 a
- \end{verbatim}
+ \begin{code}
+Vector 4 Integer
+ \end{code}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Daarom leggen we de lengte vast in het type van de vector
+\item Nat n geeft aan dat n een natuurlijk getal moet zijn
+\item Nu kunnen we dus bijvoorbeeld aangeven, dat er een vector type moet zijn die aangeeft dat er het 4 element heeft, en dat deze elementen van het type Integer zijn
+\item Next sheet: we willen meer dan lengte specificeren
+}
\frame{
\frametitle{Specify Size (type-level)}
\item We also want to manipulate or query the size of a vector
\end{itemize}
}
+\note[itemize]{
+\item Maar we willen niet alleen de lengte vastleggen
+\item We willen ook dingen over de lengte kunnen vragen, of de lengte kunnen veranderen
+\item Next sheet: informatie over size opvragen
+}
\frame{
\frametitle{Size Query}
\begin{itemize}
\item Sometimes we want to know something about the size of the vector
\item Get the first element of the vector
- \begin{verbatim}
+ \begin{code}
first :: Positive n => Vector n a -> a
- \end{verbatim}
+ \end{code}
\item Only works for vectors that are not empty
\end{itemize}
}
+\note[itemize]{
+\item Soms willen we dus iets weten over de lengte van de vector
+\item Voor de functie first, die het eerste element uit een vector haalt, moeten we dus wel zeker weten dat de vector minimaal een element heeft.
+\item Daarom willen we weten of de lengte, n, Positief is
+\item Next sheet: lengtes afleiden van anderen, en manipuleren
+}
\frame{
\frametitle{Size Manipulation}
\begin{itemize}
\item Sometimes we want to relate the size of one or more vectors to the size of one or more other vectors
\item Combine 2 vectors into 1 large vector
- \begin{verbatim}
+ \begin{code}
combine :: Vector n1 a -> Vector n2 a ->
Vector (n1 + n2) a
- \end{verbatim}
+ \end{code}
\end{itemize}
}
+\note[itemize]{
+\item En we willen lengten ook wel eens aanpassen of construeren
+\item Zoals in de functie combine, die 2 vectoren aan elkaar plakt.
+\item We willen aangeven dat de lengte van de resulterende vector, de lengte van de andere twee vectoren bij elkaar opgeteld is.
+\item Next sheet: type-niveau getallen
+}
\frame{
\frametitle{Type-level numbers}
\item When dealing with type-level number,s each instance is a type in it’s own right! e.g. the type-level equivalent of 3 is D3.
\end{itemize}
}
+\note[itemize]{
+\item Eigenaardigheden in Haskell: de normale getalen mogen niet onderdeel zijn van een type, omdat het waarden zijn.
+\item Daarom moeten we speciale getallen gebruiken, zogeheette type-level nummers
+\item Deze type-level nummers stellen dus het getal 3 voor! maar hebben niet de waarde 3! Het is nu een type op zichzelf.
+\item Next sheet: problemen met type-niveau getallen
+}
\frame{
\frametitle{Type-level problems}
\item For example, commutativity of addition:\\ a + b = b + a
\end{itemize}
}
+\note[itemize]{
+\item Wij interpreteren bepaalde types als getallen, maar het blijven types, en daarom moeten ze blijven voldoen aan de eisen van het type systeem.
+\item Omdat het type systeem garanties moet geven over de correctheid vereist het bewijzen. Als ze zomaar alles zouden accepteren heb je er niks aan.
+\item Als gevolg moeten we dus opeens invarianten bewijzen die voor ons heel natuurlijk zijn. Die iedereen eigenlijk voor lief neemt. Zoals de communicativiteit van het optellen.
+\item Next sheet: Geen proofs, daarom geen eigen transformaties
+}
\frame{
\frametitle{Consequences}
\item Result: a (limited) set of vector transformations is exposed to a developer.
\end{itemize}
}
+\note[itemize]{
+\item Er is binnen Haskell niet echt goede ondersteuning om dit soort invarianten op te schrijven. Op dit moment moet je bewijsopbouwers aanroepen in de functie zelf.
+\item Wij hebben er voor gekozen om de gebruiker niet aan dit soort manier van bewijzen op te bouwen en te gebruiken binnen functies.
+\item Dit betekent dus ook dat gebruikers niet zelf functies kunnen schrijven die de lengte van de vector aanpassen.
+\item Als gevolg is er een aantal vooraf gedefineerde vector transformatie functies gemaakt en samengevoegd in een library. Een gebruiker kan geen nieuwe transformaties maken.
+\item Next sheet: geen eigen transformaties, daarom geen eigen recursieve functies
+}
\frame{
\frametitle{Consequences}
\begin{itemize}
\item The largest consequence of not allowing any type of vector transforming functions is that a developer can no longer specify recursive functions!
\end{itemize}
+}
+\note[itemize]{
+\item Het grootste gevolg is dat gebruikers nu helaas geen eigen recursieve functies mogen maken. Omdat ze de structuur van een vector niet mogen aanpassen.
+\item Next sheet: is \clash{} te beperkt?
}
\ No newline at end of file
\frame{\titlepage}
\note[itemize]{
-\item De taal Cλash
-\item De compiler voor Cλash
+\item De taal \clash{}
+\item De compiler voor \clash{}
\item Eerst hardware introductie (gezamenlijk)
}
\includegraphics<1>[height=8cm]{figures/cpus/pmiphone_boardtopbig}
\includegraphics<2>[height=8cm]{figures/cpus/Intel_core_i7}
\includegraphics<3>[height=8cm]{figures/cpus/6600GT_GPU}
-\includegraphics<4>[height=8cm]{figures/cpus/Altera_StratixIV}
+% \includegraphics<4>[height=8cm]{figures/cpus/Altera_StratixIV}
}
\label{img:chips}
\end{figure}
\item TODO
}
-\subsection{\clash}
+\subsection{\texorpdfstring{\clash{}}{CLasH}}
\frame{
\begin{center}
-%include polycode.fmt
+%include lhs2TeX.fmt
-%if style == newcode
-%format ANN(x) = "{-# ANN " x " #-}"
-%format CXT(x) = "(" x ")"
-%format ` = "''"
-%format ^^ = " "
-%else
-%format ANN(x) = "\{-\#\ \mathit{ANN}\ " x "\ \#-\}"
-%format CXT(x) = "(Some\ context...)"
-%format ` = "''"
-%format ^^ = "\; "
-%format :>: = "\ensuremath{>}"
-%format :<: = "\ensuremath{<}"
-%format :==: = "\ensuremath{\equiv}"
-%format :-: = "\ensuremath{-}"
-%format :+: = "\ensuremath{+}"
-%format :*: = "\ensuremath{*}"
-%format :<=: = "\ensuremath{\leq}"
-%format SPL(x) = "\$" ( x )
-%format QU(x) = "\llbracket " x "\rrbracket "
-%format QUd(x) = "[d|" x "\rrbracket "
-%format QUt(x) = "[t|" x "\rrbracket "
-%format ^^ = "\; "
-%endif
\ No newline at end of file
projects / matthijs / master-project / final-presentation.git / commitdiff