--- a/progs/scala/re.scala	Tue Sep 13 11:49:22 2016 +0100
+++ b/progs/scala/re.scala	Thu Sep 22 00:40:03 2016 +0100
@@ -182,10 +182,24 @@
   case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
   case (ALT(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
   case (ALT(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
-  case (CHAR(d), Empty) => Chr(c) 
+  case (CHAR(d), Empty) => Chr(d) 
   case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
 }
 
+def prj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
+  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(prj(r, c, v1)::vs)
+  case (SEQ(r1, r2), Sequ(v1, v2)) => 
+    if (flatten(v1) == "") Right(prj(r2, c, v2))      
+    else { if (nullable(r1)) Left(Sequ(prj(r1, c, v1), v2))
+           else Sequ(prj(r1, c, v1), v2)
+    }
+  case (ALT(r1, r2), Left(v1)) => Left(prj(r1, c, v1))
+  case (ALT(r1, r2), Right(v2)) => Right(prj(r2, c, v2))
+  case (CHAR(d), _) => Empty 
+  case (RECD(x, r1), _) => Rec(x, prj(r1, c, v))
+}
+
+
 // main lexing function (produces a value)
 def lex(r: Rexp, s: List[Char]) : Val = s match {
   case Nil => if (nullable(r)) mkeps(r) else throw new Exception("Not matched")
@@ -255,7 +269,11 @@
 
 def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
 
-lexing_sim(("a" + "ab") | ("b" + ""), "ab")
+lexing(("a" | "ab") ~ ("b" | ""), "ab")
+lexing_simp(("a" | "ab") ~ ("b" | ""), "ab")
+
+
+
 // brute force search infrastructure
 
 // enumerates regular expressions until a certain depth
@@ -294,6 +312,11 @@
 }     
 
 // exhaustively tests values of a regular expression
+def vfilter1(f: Rexp => Val => Boolean)(r: Rexp) : Set[(Rexp, Val)] = {
+  val vs = values(r)
+  for (v <- vs; if (f(r)(v))) yield (r, v)
+}
+
 def vfilter2(f: Rexp => Val => Val => Boolean)(r: Rexp) : Set[(Rexp, Val, Val)] = {
   val vs = values(r)
   for (v1 <- vs; v2 <- vs; if (f(r)(v1)(v2))) yield (r, v1, v2)
@@ -310,6 +333,18 @@
 enum(2, "abc").size
 //enum(3, "ab").size
 
+// test for inj/prj
+def injprj_test(r:Rexp)(v:Val) : Boolean =
+  if (flatten(v) != "") (inj(r, 'a', prj(r, 'a', v)) != v) else false
+
+val injprj_tst = enum(2, "ab").flatMap(vfilter1(injprj_test))
+val injprj_smallest = injprj_tst.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head
+
+prj(CHAR('b'), 'a', Chr('b'))
+inj(CHAR('b'), 'a', Empty)
+
+prj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Sequ(Right(Empty),Chr('a')))
+inj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Right(Empty))
 
 // tests for totality
 def totality_test(r: Rexp)(v1: Val)(v2: Val) : Boolean =