# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1765823546 0
# Node ID 0b4a34ebd5742f58df3ca0d500865b89f67b9d65
# Parent  b84e794b9e88c36cc021f5e1b9c3a702c59acdb0
added

diff -r b84e794b9e88 -r 0b4a34ebd574 Admin/feedback-2016.pdf
Binary file Admin/feedback-2016.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 Admin/feedback-2022.pdf
Binary file Admin/feedback-2022.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 Admin/feedback-2023.pdf
Binary file Admin/feedback-2023.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 Admin/feedback-2024.pdf
Binary file Admin/feedback-2024.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 Admin/feedback-2025.pdf
Binary file Admin/feedback-2025.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 progs/Matcher.thy
--- 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
 
diff -r b84e794b9e88 -r 0b4a34ebd574 progs/fun/fun_llvm.sc
--- 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
diff -r b84e794b9e88 -r 0b4a34ebd574 slides/slides10.pdf
Binary file slides/slides10.pdf has changed
diff -r b84e794b9e88 -r 0b4a34ebd574 slides/slides10.tex
--- 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}