Binary file Admin/feedback-2016.pdf has changed
Binary file Admin/feedback-2022.pdf has changed
Binary file Admin/feedback-2023.pdf has changed
Binary file Admin/feedback-2024.pdf has changed
Binary file Admin/feedback-2025.pdf has changed
--- a/progs/Matcher.thy Thu Dec 11 12:34:03 2025 +0000
+++ b/progs/Matcher.thy Mon Dec 15 18:32:26 2025 +0000
@@ -88,48 +88,6 @@
lemma nullable_correctness:
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
apply(induct r)
-(* ZERO case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-(* ONE case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-(* CHAR case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-prefer 2
-(* ALT case *)
-apply(simp (no_asm) only: nullable.simps)
-apply(simp only:)
-apply(simp only: L.simps)
-apply(simp)
-(* SEQ case *)
-apply(simp only: L.simps)
-apply(simp)
-oops
-
-lemma nullable_correctness:
- shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
-apply(simp_all)
-(* all easy subgoals are proved except the last 2 *)
-(* where the definition of Seq needs to be unfolded. *)
-oops
-
-lemma nullable_correctness:
- shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
-apply(simp_all add: Seq_def)
-(* except the star case every thing is proved *)
-(* we need to use the rule for Star.start *)
-oops
-
-lemma nullable_correctness:
- shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
apply(simp_all add: Seq_def Star.start)
done
--- a/progs/fun/fun_llvm.sc Thu Dec 11 12:34:03 2025 +0000
+++ b/progs/fun/fun_llvm.sc Mon Dec 15 18:32:26 2025 +0000
@@ -1,3 +1,28 @@
+
+env = [i => 0, i => 1]
+
+
+def time_needed[T](code: => T) = {
+ val start = System.nanoTime()
+ code
+ val end = System.nanoTime()
+ (end - start)/(1.0e9)
+}
+
+time_needed(1, 1 + 2)
+
+def time_needed[T](f: T => T, arg: T) = {
+ val start = System.nanoTime()
+ f(arg)
+ val end = System.nanoTime()
+ (end - start)/(1.0e9)
+}
+
+
+
+
+
+
// A Small LLVM Compiler for a Simple Functional Language
// (includes a lexer and parser)
//
@@ -103,9 +128,9 @@
// val k1 = KVar("foo")
// val k2 = KNum(1)
-// val k3 = Kop("-", Kop("+", k1, k2), KNum(2))
-// println(draw(k3).mkString)
-// println(draw(KCall("bar", List(k1,k2,k3,k2,k1))).mkString)
+// val k3 = Kop("-", Kop("+", k1, k2), KNum(2)) // not in SSA-form
+// println(draw(k3))
+// println(draw(KCall("bar", List(k1,k2,k3,k2,k1))))
// CPS translation from Exps to KExps using a
@@ -143,9 +168,10 @@
}
//initial continuation
-def CPSi(e: Exp) = CPS(e)(KReturn(_))
+def CPSi(e: Exp) = CPS(e)(x => KReturn(x))
-
+//write (1 + a)
+println(CPSi(Write(Aop("+", Num(1), Var("a")))).toString)
//some testcases:
// (1 + 2) * 3
Binary file slides/slides10.pdf has changed
--- a/slides/slides10.tex Thu Dec 11 12:34:03 2025 +0000
+++ b/slides/slides10.tex Mon Dec 15 18:32:26 2025 +0000
@@ -974,9 +974,15 @@
\begin{quote}\it
``Overall, CFL was without a doubt the most interesting subject I have taken\ldots''
\end{quote}
+\end{minipage}\medskip}
+
+\only<3>{
+\begin{minipage}{13cm}
+\begin{quote}\it
+``I like the lecture videos on KEATS, I think they are very engaging and I like the lecturers sense of humour.''
+\end{quote}
\end{minipage}}
-
\hfill\includegraphics[scale=0.12]{thanks.png}
\end{frame}