diff options
| -rw-r--r-- | def.tex | 1 | ||||
| -rw-r--r-- | defio.tex | 9 | ||||
| -rw-r--r-- | defstate.tex | 6 | ||||
| -rw-r--r-- | intro.tex | 27 | ||||
| -rw-r--r-- | introexmp.tex | 7 | ||||
| -rw-r--r-- | rulescat.tex | 2 | ||||
| -rw-r--r-- | rulesquotify.tex | 4 | ||||
| -rw-r--r-- | werkstuk.tex | 2 |
8 files changed, 38 insertions, 20 deletions
@@ -2,6 +2,7 @@ \section{Definities} \label{sec:def} +\input{defmeta} \input{defsyn} \input{defio} \input{defstate} @@ -6,17 +6,18 @@ Allereerst definiëren we het type $\Stack{a}$, omdat stacks we veel met stacks doen in onze semantiek regels. Een $\Stack{a}$ (lees: een stack van elementen van type $a$) is een simpel datatype met de volgende syntax: +\def\inbrackets#1{$\mathrm{[}#1\mathrm{]}$} +\def\bracka{\inbrackets{a}} \begin{grammar} - <Stack[a]> ::= [<a>:<Stack[a]>] | `Nil' - %todo formatting + <Stack \bracka> ::= [<a>:<Stack \bracka>] | `Nil' \end{grammar} Op een stack zijn twee instructies gedefinieerd: \begin{gather*} \pushop : a \times \Stack{a} \to \Stack{a} \\ - \push{e}{s} \isdef [e:s] \\[1em] + \push{e}{\stk} \isdef [e:\stk] \\[1em] \popop : \Stack{a} \hookrightarrow a \times \Stack{a} \\ - \pop{[e:s]} \isdef (e,s) \\ + \pop{[e:\stk]} \isdef (e,\stk) \\ \end{gather*} $\popop$ is een partiële functie omdat $\pop\Nil$ niet gebruikt mag worden in diff --git a/defstate.tex b/defstate.tex index e54c888..b748c98 100644 --- a/defstate.tex +++ b/defstate.tex @@ -29,10 +29,10 @@ $\str~k$. Vervolgens definiëren we $\putop:\SynString \times \SynString \times waarde en een oude store een nieuwe store oplevert: $$ - \put{\var}{\val}{\str} k = + \put{\var}{\val}{\str} \var' = \begin{cases} - \val & \text{als $k=\var$} \\ - \str~k & \text{als $k\ne\var$} + \val & \text{als $\var'=\var$} \\ + \str~\var' & \text{als $\var'\ne\var$} \end{cases} $$ @@ -3,7 +3,7 @@ \label{sec:intro} Smurf is een esoterische programmeertaal oorspronkelijk ontworpen door Matthew -Westcott. In de specificatie \cite{safalra} beschrijft hij kort wat Smurf is: +Westcott. In de specificatie~\cite{safalra} beschrijft hij kort wat Smurf is: \begin{quote} Smurf = String-based MURiel Forthoid @@ -11,12 +11,20 @@ Westcott. In de specificatie \cite{safalra} beschrijft hij kort wat Smurf is: The only native data type is the string, and operations are carried out on strings in a forty manner. \end{quote} -We hebben dus te maken met een Forth-achtige programmeertaal. De eigenschappen -die we hiervan terugzien in Smurf zijn voornamelijk reflection, -stackgeörienteerd en `geconcateneerd programmeren'. We kunnen het programma dus -dynamisch aanpassen, werken met een stack en schrijven een programma als één -grote functiecompositie (zonder met functieapplicaties te werken). Voordat we -alle commando's bespreken is een voorbeeld op zijn plaats. +Voor iemand die niet in de materie zit is deze beschrijving misschien wat +overweldigend. Het gaat om een Forth-achtige programmeertaal. De eigenschappen +van Forth die belangrijk zijn in Smurf, zijn de volgende: +\begin{itemize} + \item Stack-geörienteerd: alle operaties werken op een stack van strings. + \item Reflection: het is mogelijk (en in veel gevallen zelfs noodzakelijk) + het programma zichzelf dynamisch aan te laten passen. + \item `Geconcateneerd programmeren': de taal kent geen functieapplicatie maar + alleen functiecompositie. Een programma is een functie, opgebouwd uit + kleinere functies. Bij het uitvoeren wordt die grote functie toegepast op + de initiële toestand. Bij deze initiële toestand hoort bijvoorbeeld een + lege stack. +\end{itemize} +Voordat we alle commando's bespreken is een klein voorbeeld op zijn plaats. \begin{exmp} We bekijken het volgende programma: @@ -47,8 +55,9 @@ illustreren met een voorbeeld: om de variabele `papa' de waarde `smurf' te geven. Hierna is de stack weer leeg. Vervolgens zetten we `papa' op de stack en gebruiken we \smurfinline{g} om het bovenste element als variabele op te zoeken in de variable store en de - waarde ervan op de stack te zetten. Hierbij wordt het bovenste element van de stack verwijdert. De stack bestaat nu dus uit het element - `smurf'. Met \smurfinline{o} sturen we deze string naar de output. + waarde ervan op de stack te zetten. Hierbij wordt het bovenste element van de + stack verwijdert. De stack bestaat nu dus uit het element `smurf'. Met + \smurfinline{o} sturen we deze string naar de output. \end{exmp} \input{introcoms} diff --git a/introexmp.tex b/introexmp.tex index 94c0afc..2ebe1eb 100644 --- a/introexmp.tex +++ b/introexmp.tex @@ -43,6 +43,13 @@ aangeven hoe conditionele executie kan worden behaald in Smurf. \smurfinline{+"o"+} bouwen we hiervan het programma \smurfinline{"mijn string"ho}, wat we met \smurfinline{x} uitvoeren. De uitvoer van het programma is dus `m', in dit geval. + + Wat gebeurt er als de gebruiker iets anders dan `head' of `tail' invoert? In + dit geval bestaat er geen variabele met de naam die de gebruiker had + ingevoerd. Het commando \smurfinline{g} levert dan de lege string op. Dit + betekent dat we het programma \smurfinline{"mijn string"o} bouwen. Als de + gebruiker dus geen correcte keuze maakt, dan zal de hele string worden + teruggegeven. \end{exmp} \begin{exmp} diff --git a/rulescat.tex b/rulescat.tex index 48dcddf..f36f0ec 100644 --- a/rulescat.tex +++ b/rulescat.tex @@ -16,7 +16,7 @@ Dit geeft de volgende regel: $$ \begin{prooftree} \trans - {\pgm}{\ip}{(\push{s1~s2}{\stk''}, \str)} + {\pgm}{\ip}{(\push{s_1~s_2}{\stk''}, \str)} {\ip'}{\op}{\st} \justifies \trans diff --git a/rulesquotify.tex b/rulesquotify.tex index e0bdd4c..8ebe567 100644 --- a/rulesquotify.tex +++ b/rulesquotify.tex @@ -19,11 +19,11 @@ $$ \begin{prooftree} \trans {\pgm}{\ip}{(\push{\texttt{"}\escape{s}\texttt{"}}{\stk'}, \str) } - {\ip}{\op}{\st} + {\ip'}{\op}{\st} \justifies \trans {\StmQuotify:\pgm}{\ip}{(\stk,\str)} - {\ip}{\op}{\st} + {\ip'}{\op}{\st} \using{\rquotifyns} \qquad \text{met $\pop{\stk} = (s, stk')$.} diff --git a/werkstuk.tex b/werkstuk.tex index 632d685..24a290f 100644 --- a/werkstuk.tex +++ b/werkstuk.tex @@ -35,7 +35,7 @@ parent=section, spacebelow=1em, preheadhook=\nobreak\noindent\hrulefill, - prefoothook=\vspace*{\dimexpr-\baselineskip+\topsep\relax}\endgraf\nobreak\noindent\hrulefill + prefoothook=\vspace*{\dimexpr-\baselineskip+\topsep\relax}\endgraf\nobreak\noindent\hrulefill% ]{lined} \declaretheorem[style=lined]{exmp} |