diff -r 8016a2480704 -r 7cf9f17aa179 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Thu Jun 09 12:57:53 2022 +0100
+++ b/thys2/blexer2.sc	Thu Jun 09 22:07:44 2022 +0100
@@ -21,6 +21,7 @@
 case object ANYCHAR extends Rexp
 case class CHAR(c: Char) extends Rexp
 case class ALTS(r1: Rexp, r2: Rexp) extends Rexp 
+case class ALTSS(rs: List[Rexp]) extends Rexp
 case class SEQ(r1: Rexp, r2: Rexp) extends Rexp 
 case class STAR(r: Rexp) extends Rexp 
 case class RECD(x: String, r: Rexp) extends Rexp  
@@ -270,6 +271,7 @@
   case CHAR(_) => false
   case ANYCHAR => false
   case ALTS(r1, r2) => nullable(r1) || nullable(r2)
+  case ALTSS(rs) => rs.exists(nullable)
   case SEQ(r1, r2) => nullable(r1) && nullable(r2)
   case STAR(_) => true
   case RECD(_, r1) => nullable(r1)
@@ -284,6 +286,7 @@
   case CHAR(d) => if (c == d) ONE else ZERO
   case ANYCHAR => ONE 
   case ALTS(r1, r2) => ALTS(der(c, r1), der(c, r2))
+  case ALTSS(rs) => ALTSS(rs.map(der(c, _)))
   case SEQ(r1, r2) => 
     if (nullable(r1)) ALTS(SEQ(der(c, r1), r2), der(c, r2))
     else SEQ(der(c, r1), r2)
@@ -294,6 +297,84 @@
   case NOT(r) =>  NOT(der(c, r))
 }
 
+def ders(s: List[Char], r: Rexp) : Rexp = s match {
+  case Nil => r
+  case c :: cs => ders(cs, der(c, r))
+}
+
+def ders_simp(s: List[Char], r: Rexp) : Rexp = s match {
+  case Nil => simp(r)
+  case c :: cs => ders_simp(cs, simp(der(c, r)))
+}
+
+
+def simp2(r: Rexp) : Rexp = r match {
+  case SEQ(r1, r2) => 
+    (simp2(r1), simp2(r2)) match {
+      case (ZERO, _) => ZERO
+      case (_, ZERO) => ZERO
+      case (ONE, r2s) => r2s
+      case (r1s, ONE) => r1s
+      case (r1s, r2s) => 
+        SEQ(r1s, r2s)
+    }
+  case ALTS(r1, r2) => 
+    val r1r2s = fltsplain(simp2(r1) :: simp2(r2) :: Nil).distinct 
+    r1r2s match {
+      case Nil => ZERO
+      case r :: Nil => r
+      case r1 :: r2 :: rs => 
+        ALTSS(r1 :: r2 :: rs)
+    }
+  case ALTSS(rs) => 
+    // println(rs)
+    (fltsplain(rs.map(simp2))).distinct match {
+      case Nil => ZERO
+      case r :: Nil => r
+      case r1 :: r2 :: rs =>
+        ALTSS(r1 :: r2 :: rs)
+    }
+  case r => r
+}
+
+
+def simp(r: Rexp) : Rexp = r match {
+  case SEQ(r1, r2) => 
+    (simp(r1), simp(r2)) match {
+      case (ZERO, _) => ZERO
+      case (_, ZERO) => ZERO
+      case (ONE, r2s) => r2s
+      case (r1s, ONE) => r1s
+      case (r1s, r2s) => SEQ(r1s, r2s)
+    }
+  case ALTS(r1, r2) => {
+    (simp(r1), simp(r2)) match {
+      case (ZERO, r2s) => r2s
+      case (r1s, ZERO) => r1s
+      case (r1s, r2s) =>
+        if(r1s == r2s) r1s else ALTS(r1s, r2s)
+    }
+  }
+  case r => r
+}
+
+def fltsplain(rs: List[Rexp]) : List[Rexp] = rs match {
+  case Nil => Nil
+  case ZERO :: rs => fltsplain(rs)
+  case ALTS(r1, r2) :: rs => r1 :: r2 :: fltsplain(rs) 
+  case ALTSS(rs) :: rs1 => rs ::: fltsplain(rs1)
+  case r :: rs => r :: fltsplain(rs)
+}
+
+
+
+
+def matcher(s: String, r: Rexp) : Boolean = 
+  nullable(ders(s.toList, r))
+
+def simp_matcher(s: String, r: Rexp) : Boolean = 
+  nullable(ders_simp(s.toList, r))
+
 
 // extracts a string from a value
 def flatten(v: Val) : String = v match {
@@ -1258,6 +1339,7 @@
       println(asize(bders_simp(prog0.toList, internalise(STARREG))))
       // println(asize(bdersStrong7(prog0.toList, internalise(STARREG))))
     }
+    
   }
 }
 // small()
@@ -1269,8 +1351,36 @@
     println(asize(bders_simp(prog.toList, internalise(r))))
   }
 }
-aaa_star()
+// aaa_star()
+def naive_matcher() {
+  val r = STAR(STAR("a") ~ STAR("a"))
 
+  for(i <- 0 to 20) {
+    val s = "a" * i 
+    val t1 = System.nanoTime
+    matcher(s, r)
+    val duration = (System.nanoTime - t1) / 1e9d
+    print(i)
+    print(" ")
+    // print(duration)
+    // print(" ")
+    print(asize(bders_simp(s.toList, internalise(r))))
+    //print(size(ders_simp(s.toList, r)))
+    println()
+  }
+  // for(i <- 1 to 40000000 by 500000) {
+  //   val s = "a" * i
+  //   val t1 = System.nanoTime
+  //   val derssimp_result = ders_simp(s.toList, r)
+  //   val duration = (System.nanoTime - t1) / 1e9d
+  //   print(i)
+  //   print(" ")
+  //   print(duration)
+  //   println()
+  // }
+  
+}
+naive_matcher()
 def generator_test() {
 
   test(rexp(4), 1000000) { (r: Rexp) =>