cleanup

.gitignore

@@ -1,2 +1,8 @@
-thesis.run.xml
-thesis.bbl
+**/*.synctex.gz
+**/*.bbl
+**/*.run.xml
+**/*.snm
+**/*.nav
+**/*.vrb
+doc/*
+**/interpreters/out

interpreters/out/cek.rkt

@@ -9,7 +9,6 @@
   {Abs String Term}
   {App Term Term})
 
-(def-struct {Fun body env x})
 (def-struct {App2 cont var2})
 (def-struct {App1 arg cont env})
 (def-struct {Halt })
@@ -24,15 +23,13 @@
 (def eval (env term cont)
   (match term
     ([String x] (continue1 cont (env x)))
-    ({Abs x body} (continue1 cont {Fun body env x}))
+    ({Abs x body}
+      (continue1 cont (fun (v cont1) (eval (extend env x v) body cont1))))
     ({App fn arg} (eval env fn {App1 arg cont env}))))
 
-(def apply (fn1 v cont1)
-  (match fn1 ({Fun body env x} (eval (extend env x v) body cont1))))
-
-(def continue1 (fn2 var3)
-  (match fn2
-    ({App2 cont var2} (apply var2 var3 cont))
+(def continue1 (fn1 var3)
+  (match fn1
+    ({App2 cont var2} (var2 var3 cont))
     ({App1 arg cont env} (eval env arg {App2 cont var3}))
     ({Halt } var3)))
 

interpreters/out/normalization-by-evaluation.rkt

@@ -24,7 +24,7 @@
   (fun (n)
     (match n
       (0 val)
-      (_ (env (- n 1))))))
+    (_ (env (- n 1))))))
 
 (def reify (ceil val cont)
   (match val
@@ -43,27 +43,28 @@
     ({App f arg} (eval f env {App3 arg cont2 env}))
     ({Abs body} (continue cont2 {Fun {Closure body env}}))))
 
+;; evaluation
+(def continue (fn2 var13)
+  (match fn2
+    ({Fun1 cont var3} (reify var3 var13 {Fun2 cont}))
+    ({App4 cont2 var12} (apply var12 var13 cont2))
+    ({App3 arg cont2 env} (eval arg env {App4 cont2 var13}))
+    ({Cont cont4 var16} (reify var16 var13 cont4))))
+
 (def run (term cont4) (eval term (fun (x) (error "empty env")) {Cont cont4 0}))
 
 (def apply1 (fn x cont3)
   (match fn ({Closure body env} (eval body (cons x env) cont3))))
 
+;; reification
 (def continue1 (fn1 var11)
   (match fn1
     ({Fun2 cont} (continue1 cont {Abs var11}))
     ({App2 cont var10} (continue1 cont {App var10 var11}))
     ({App1 arg ceil cont} (reify ceil arg {App2 cont var11}))
     ({Halt } var11)))
 
-(def continue (fn2 var13)
-  (match fn2
-    ({Fun1 cont var3} (reify var3 var13 {Fun2 cont}))
-    ({App4 cont2 var12} (apply var12 var13 cont2))
-    ({App3 arg cont2 env} (eval arg env {App4 cont2 var13}))
-    ({Cont cont4 var16} (reify var16 var13 cont4))))
-
 (def main ([Term term]) (run term {Halt }))
-
 ; end interpreter
 
 (module+ test

interpreters/src/cek.rkt

@@ -19,7 +19,7 @@
 (def eval (env term)
   (match term
     ([String x] (env x))
-    ({Abs x body} (fun #:name Fun #:apply apply (v) (eval (extend env x v) body)))
+    ({Abs x body} (fun #:name Fun #:apply apply #:no-defun (v) (eval (extend env x v) body)))
     ({App fn arg} ((eval env fn) (eval env arg)))))
 
 (def main ([Term term]) (eval init term))

seminar/slides.tex

@@ -1,4 +1,4 @@
-\documentclass{beamer}
+\documentclass[handout]{beamer}
 
 \mode<presentation>
 {
@@ -91,7 +91,7 @@
 \title[The Functional Correspondence Applied]{The Functional Correspondence Applied:\\ An Implementation of a Semantics Transformer}
 \author[Maciej Buszka]{Maciej Buszka}
 \institute[II UWr]{Instytut Informatyki UWr}
-\date{05.11.2020}
+\date{18.11.2020}
 
 \begin{document}
 
@@ -118,7 +118,7 @@ \section{Introduction}
     \item Produces an encoding of an abstract machine\pause
     \item Introduced by Danvy et~al. in \textit{A functional correspondence between evaluators and abstract machines}
     \pause
-    \item Based on two source-to-source transformations
+    \item Based on two source-to-source transformations \pause
     \begin{itemize}
       \item Translation to continuation-passing style (CPS)
       \item Defunctionalization
@@ -191,9 +191,9 @@ \section{Introduction}
 
 \begin{frame}{The Result}
   \begin{itemize}
-    \item An abstract machine encoded as mutually tail-recursive functions
+    \item An abstract machine encoded as mutually tail-recursive functions \pause
     \item Uses abstract environment (encoded as a function)
-    \begin{itemize}
+    \begin{itemize} \pause
       \item \lstinline{extend} is still higer-order
       \item \lstinline{extend} and functions representing environment remain in direct style
     \end{itemize}
@@ -202,22 +202,22 @@ \section{Introduction}
 
 \begin{frame}{Desired Features}
   \begin{itemize}
-    \item Metalanguage expressivity
+    \item Metalanguage expressivity \pause
     \begin{itemize}
-      \item Mutually recursive, anonymous and higher-order functions
-      \item Records and pattern matching
-      \item Dynamic (strong) typing
+      \item Mutually recursive, anonymous and higher-order functions \pause
+      \item Records and pattern matching \pause
+      \item Dynamic (strong) typing \pause
     \end{itemize}\pause
-    \item Automation
+    \item Automation \pause
     \begin{itemize}
-      \item Function space detection
-      \item CPS and defunctionalization
+      \item Function space detection\pause
+      \item CPS and defunctionalization\pause
       \item Sensible name generation
     \end{itemize}\pause
-    \item User's control over transformation
+    \item User's control over transformation\pause
     \begin{itemize}
-      \item Naming of records for defunctionalized lambdas, apply functions
-      \item Disabling defunctionalization and/or cps transformation of chosen functions
+      \item Naming of records for defunctionalized lambdas, apply functions\pause
+      \item Disabling defunctionalization and/or cps transformation of chosen functions \pause
     \end{itemize}
   \end{itemize}
 \end{frame}
@@ -265,10 +265,10 @@ \section{Introduction}
 
 \begin{frame}[fragile]{Transformation to ANF}
   \begin{itemize}
-    \item Assumes left-to-right call-by-value semantics
+    \item Assumes left-to-right call-by-value semantics \pause
     \item Let-bind every intermediate result \pause
     \item Eases program analysis and further transformations \pause
-    \item Preserves tail calls \pause
+    \item Preserves tail calls
   \end{itemize}\pause
   \vspace{1\baselineskip}
   \begin{beamerboxesrounded}{Abstract syntax of the meta-language}
@@ -312,7 +312,7 @@ \section{Introduction}
       \endgroup
       \end{center}
   \end{beamerboxesrounded}
-  \vspace{\baselineskip}
+  \vspace{\baselineskip}\pause
   \begin{beamerboxesrounded}{ANF translation}
     \begin{center}
       \begingroup
@@ -356,7 +356,7 @@ \section{Introduction}
       \endgroup
       \end{center}
   \end{beamerboxesrounded}
-  \vspace{\baselineskip}
+  \vspace{\baselineskip}\pause
   \begin{beamerboxesrounded}{Sequencing multiple terms}
     \begin{center}
       \begingroup
@@ -392,13 +392,13 @@ \section{Introduction}
 
 \begin{frame}{Control Flow Analysis}
   \begin{itemize}
-    \item For each expression in a program, find the over-approximation of~the~set of functions it may evaluate to
-    \item Detects function spaces for defunctionalization
+    \item For each expression in a program, find the over-approximation of~the~set of functions it may evaluate to\pause
+    \item Detects function spaces for defunctionalization\pause
     \item Enables selective cps translation
     \pause
-    \item Textbook approaches:
+    \item Textbook approaches:\pause
     \begin{itemize}
-      \item Constraint systems
+      \item Constraint systems\pause
       \item Annotated type systems
     \end{itemize}
   \end{itemize}
@@ -408,12 +408,12 @@ \section{Introduction}
   \begin{itemize}
     \item Begin with a CESK* machine extended with patern matching\\
       (Control Environment Store Kontinuation pointer)\pause
-    \item Because the program is in ANF:
+    \item Because the program is in ANF:\pause
     \begin{itemize}
-      \item There are only two types of continuations
+      \item There are only two types of continuations\pause
       \item Every proper subexpression will allocate a value in the store
     \end{itemize}\pause
-    \item Provide finite approximations for base types
+    \item Provide finite approximations for base types\pause
     \item Let the store map to sets of value approximations\pause
     \item Compute the set of configurations reachable from the initial one\pause
     \item Now for every variable in function position the store contains a set of values to which it may evaluate\pause
@@ -431,10 +431,10 @@ \section{Introduction}
 
 \begin{frame}{Selective Translation to CPS}
   \begin{itemize}
-    \item Allows the user to specify which functions should be left in direct style
+    \item Allows the user to specify which functions should be left in direct style \pause
     \item Functions in direct style may call CPS ones and vice versa \pause
     \item Quite simple since the program is already in ANF \pause
-    \item Designed not to duplicate code
+    \item Designed not to duplicate code \pause
     \item Produces a program in ANF
   \end{itemize}
 \end{frame}
@@ -555,12 +555,12 @@ \section{Introduction}
 \begin{frame}[fragile]{Selective Defunctionalization}
   \begin{itemize}
     \item Control flow analysis provides all the necessary information\pause
-    \item Trade-offs and gotchas
+    \item Trade-offs and gotchas \pause
     \begin{itemize}
       \item Direct vs indirect calls to top-level functions\pause
       \item Primitive operations\pause
     \end{itemize}
-    \item Record name generation
+    \item Record name generation \pause
     \begin{itemize}
       \item For anonymous functions: let the user decide\pause
       \item For continuations: use the constructor of current branch (heuristic)\pause
@@ -642,7 +642,7 @@ \section{Introduction}
 
   $\mkBranch(x\ldots,$&$\lstinline!(fun ($y\ldots$) $e$)$^l$!)$
   &= \lstinline!({Fun$_l$ $\mathit{fvs}(e)$} $\bb{e}[y\mapsto x\ldots]$)!\\
-\end{tabular}
+\end{tabular} \pause
 \begin{tabular}{rl}
   $\mkApply(l, \mathit{fn}\ldots)$ 
   &= \begin{lstlisting}
@@ -684,7 +684,7 @@ \section{Introduction}
 \begin{frame}{Finishing Touches}
   \begin{itemize}
     \item Inline let-bindings generated by transformation\\
-    Only if the variable is used exactly once
+    Only if the variable is used exactly once \pause
     \item Future work: sugar single branch matches as let bindings
   \end{itemize}
 \end{frame}
@@ -754,24 +754,24 @@ \section{Conclusion}
 
 \begin{frame}{Conclusion}
   \begin{itemize}
-    \item Algorithm
+    \item Algorithm \pause
     \begin{itemize}
-      \item Fully automatic transformation
-      \item Works with interpreters expressed in a higher-order language
-      \item Allows for fine-grained control over the resulting machine
+      \item Fully automatic transformation \pause
+      \item Works with interpreters expressed in a higher-order language \pause
+      \item Allows for fine-grained control over the resulting machine \pause
     \end{itemize}
     \pause
-    \item Implementation
+    \item Implementation \pause
     \begin{itemize}
-      \item Interpreters embedded in \textit{Racket} source files
-      \item Users influence transformation using annotations
+      \item Interpreters embedded in \textit{Racket} source files \pause
+      \item Users influence transformation using annotations \pause
       \item Tested on a selection of interpreters
     \end{itemize}
     \pause
-    \item Current work: \textit{Coq} formalization
+    \item Current work: \textit{Coq} formalization \pause
     \begin{itemize}
-      \item First version: encodings of natural semantics
-      \item Define transformation on a deeply embedded language
+      \item First version: encodings of natural semantics \pause
+      \item Define transformation on a deeply embedded language \pause
       \item Leverage \textit{MetaCoq} library to transform to and from shallow embeddings
     \end{itemize}
   \end{itemize}