Mercurial Mercurial > hg > lexing / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys2/blexer2.sc
changeset 543 b2bea5968b89
parent 541 5bf9f94c02e1
child 545 333013923c5a 
--- a/thys2/blexer2.sc	Tue Jun 14 18:06:33 2022 +0100
+++ b/thys2/blexer2.sc	Thu Jun 23 16:09:40 2022 +0100
@@ -617,7 +617,7 @@
             case rs => AALTS(bs1, rs)  
           }
     }
-    case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
+    //(erase(r0))) => AONE(bs)
     case r => r
   }
 }
@@ -781,7 +781,7 @@
 
 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
 //   where
-// "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) ⊆ (L (erase (AALTs [] rsa))) then AZERO else
+// "pAKC_aux rsa r ctx = (if (regConcat (SEQ (erase r) ( ctx) )) ⊆ (regConcat (erase (AALTs [] rsa))) then AZERO else
 //                           case r of (ASEQ bs r1 r2) ⇒ 
 //                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
 //                                     (AALTs bs rs) ⇒ 
@@ -796,13 +796,13 @@
 
 
 //the "fake" Language interpretation: just concatenates!
-def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
+def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
   case Nil => acc
   case r :: rs1 => 
     // if(acc == ONE) 
-    //   L(r, rs1) 
+    //   regConcat(r, rs1) 
     // else
-      L(SEQ(acc, r), rs1)
+      regConcat(SEQ(acc, r), rs1)
 }
 
 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
@@ -819,9 +819,9 @@
   // println("ctx---------")
   // rsprint(ctx)
   // println("ctx---------end")
-  // rsprint(breakIntoTerms(L(erase(r), ctx)).map(oneSimp))
+  // rsprint(breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp))
 
-  if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
+  if (breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
     AZERO
   }
   else{
@@ -900,47 +900,70 @@
 
 }
 
+def isOne1(r: Rexp) : Boolean = r match {
+  case ONE => true
+  case SEQ(r1, r2) => false//isOne1(r1) && isOne1(r2)
+  case ALTS(r1, r2) => false//(isOne1(r1) || isOne1(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
+  case STAR(r0) => false//atMostEmpty(r0)
+  case CHAR(c) => false
+  case ZERO => false
+
+}
+
 def turnIntoTerms(r: Rexp): List[Rexp] = r match {
-  case SEQ(r1, r2)  => if(isOne(r1)) 
+  case SEQ(r1, r2)  => if(isOne1(r1)) 
                           turnIntoTerms(r2) 
                        else 
-                          turnIntoTerms(r1).map(r11 => SEQ(r11, r2))
+                          turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
   case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
   case ZERO => Nil
   case _ => r :: Nil
 }
 
-def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
-  val res = turnIntoTerms((L(erase(r), ctx))).map(oneSimp)
-  res.toSet
+def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
+  if(r11 == ONE)
+    turnIntoTerms(r2)
+  else
+    SEQ(r11, r2) :: Nil
 }
 
-def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = {
-  val res = turnIntoTerms((L(r, ctx))).map(oneSimp)
-  res.toSet
+def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
+  turnIntoTerms((regConcat(erase(r), ctx)))
+    .toSet
 }
 
-def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = {
+def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
+  turnIntoTerms(regConcat(r, ctx)).toSet
+
+def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 
+subseteqPred: (C, C) => Boolean) : Boolean = {
   subseteqPred(f(a, b), c)
 }
-def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = {
-  val res = rs1.forall(rs2.contains)
-  res
-}
-def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
+  //rs1 \subseteq rs2
+  rs1.forall(rs2.contains)
+
+def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
+  // if (erase(r) == ONE &&  acc != Set()) 
+  // {
+  //   println("ctx")
+  //   rsprint(ctx)
+  //   println("acc")
+  //   rsprint(acc)
+  //   println("acc-end")
+  // }
   if (ABIncludedByC(a = r, b = ctx, c = acc, 
                     f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
-  {//acc.flatMap(breakIntoTerms
+  {
     AZERO
   }
   else{
     r match {
-      case ASEQ(bs, r1, r2) => 
-      (prune6(acc, r1, erase(r2) :: ctx)) match{
+      case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
         case AZERO => 
           AZERO
-        case AONE(bs1) => 
-          fuse(bs1, r2)
+        case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
+          prune6(acc, fuse(bs1, r2), ctx)
         case r1p => 
           ASEQ(bs, r1p, r2)
       }
@@ -949,7 +972,7 @@
           case Nil => 
             AZERO
           case r :: Nil => 
-            r 
+            fuse(bs, r) 
           case rs0p => 
             AALTS(bs, rs0p)
         }
@@ -989,7 +1012,8 @@
   }
 }
 
-def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : List[ARexp] = xs match {
+def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : 
+List[ARexp] = xs match {
   case Nil => 
     Nil
   case x :: xs => {
@@ -998,13 +1022,13 @@
       distinctBy6(xs, acc)
     }
     else{
-      val pruned = prune6(acc, x, Nil)
+      val pruned = prune6(acc, x)
       val newTerms = turnIntoTerms(erase(pruned))
       pruned match {
         case AZERO => 
           distinctBy6(xs, acc)
         case xPrime => 
-          xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
+          xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
       }
     }
   }
@@ -1037,6 +1061,12 @@
   case _ => r::Nil
 }
 
+def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
+  //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
+  case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
+  case ZERO => Nil
+  case _ => r::Nil
+}
 
 
 def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
@@ -1245,7 +1275,7 @@
   }
   def cir_prod(l: Lin, t: Rexp): Lin = t match {//remember this Lin is different from the Lin in Antimirov's paper. Here it does not mean the set of all subsets of linear forms that does not contain zero, but rather the type a set of linear forms
     case ZERO => Set()
-    case ONE => l
+    // case ONE => l
     case t => l.map( m => m._2 match 
       {
         case ZERO => m 
@@ -1255,6 +1285,39 @@
     
     )
   }
+  def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
+    case ZERO => Nil
+    case ONE => l
+    case t => l.map(m => m._2 match
+      {
+        case ZERO => m
+        case ONE => (m._1, t)
+        case p => (m._1, SEQ(p, t))
+      }
+    )
+
+  }
+  def lfList(r: Rexp) : List[Mon] = r match {
+    case ZERO => Nil
+    case ONE => Nil
+    case CHAR(f) => {
+      (f, ONE) :: Nil
+    }
+    case ALTS(r1, r2) => {
+      lfList(r1) ++ lfList(r2)
+    }
+    case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
+    case SEQ(r1, r2) => {
+      if(nullable(r1))
+        cir_prodList(lfList(r1), r2) ++ lfList(r2)
+      else
+        cir_prodList(lfList(r1), r2)
+    }
+  }
+  def lfprint(ls: Lin) = ls.foreach(m =>{
+    println(m._1)
+    rprint(m._2)
+    })
   def lf(r: Rexp): Lin = r match {
     case ZERO => Set()
     case ONE => Set()
@@ -1403,9 +1466,11 @@
 
 def aaa_star() = {
   val r = STAR(("a" | "aa"))
-  for(i <- 0 to 100) {
+  for(i <- 0 to 20) {
     val prog = "a" * i
+    print(i+" ")
     println(asize(bders_simp(prog.toList, internalise(r))))
+    //println(size(ders_simp(prog.toList, r)))
   }
 }
 // aaa_star()
@@ -1438,29 +1503,35 @@
   
 }
 // naive_matcher()
+//single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+//  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
+
+
+//STAR(SEQ(ALTS(CHAR(b),STAR(CHAR(b))),ALTS(ALTS(ONE,CHAR(b)),SEQ(CHAR(c),ONE))))
 def generator_test() {
 
-  test(single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
-  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))), 1) { (r: Rexp) => 
+  test(single(STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))), 1) { (r: Rexp) => 
   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
-    val ss = stringsFromRexp(r)
+    val ss = Set("ab")//stringsFromRexp(r)
     val boolList = ss.map(s => {
       //val bdStrong = bdersStrong(s.toList, internalise(r))
       val bdStrong6 = bdersStrong6(s.toList, internalise(r))
-      val bdStrong6Set = turnIntoTerms(erase(bdStrong6))
+      val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
       val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
       val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
-      rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
-      //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
-      //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
+      (rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList)) ||
+      bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
+      rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken))//|| bdStrong6Set.size <= pdersSetBroken.size
+      
     })
     //!boolList.exists(b => b == false)
     !boolList.exists(b => b == false)
   }
 }
 // small()
-//  generator_test()
-  
+// generator_test()
+
+
   
   //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
           //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
@@ -1471,13 +1542,14 @@
 //new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
 //new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
 //new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
+//circular double-nullable STAR(SEQ((STAR("b") | "a" | "b"), ("b" | ONE)))
 def counterexample_check() {
-  val r = SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
-  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
+  val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
+    ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
     //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
-  val s = "b"
-  val bdStrong5 = bdersStrong7(s.toList, internalise(r))
-  val bdStrong5Set = turnIntoTerms(erase(bdStrong5))
+  val s = "ab"
+  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
   val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
   val apdersSet = pdersSet.map(internalise)
   println("original regex ")
@@ -1490,7 +1562,7 @@
   rsprint(pdersSet.toList)
   println("pderUNIV distinctBy6")
   //asprint(distinctBy6(apdersSet.toList))
-  rsprint(distinctByacc(pdersSet.toList))
+  rsprint((pdersSet.toList).flatMap(turnIntoTerms))
   // rsprint(turnIntoTerms(pdersSet.toList(3)))
   // println("NO 3 not into terms")
   // rprint((pdersSet.toList()))
@@ -1498,7 +1570,23 @@
   // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
 
 }
-counterexample_check()
+
+// counterexample_check()
+
+def lf_display() {
+  val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
+    ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
+    //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
+  val s = "ab"
+  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
+  val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+  val apdersSet = pdersSet.map(internalise)
+  lfprint(lf(r))
+
+}
+
+lf_display()
 
 def breakable(r: Rexp) : Boolean = r match {
   case SEQ(ALTS(_, _), _) => true
@@ -1535,4 +1623,37 @@
 
 
 // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
-// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
\ No newline at end of file
+// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
+
+
+
+
+
+def bders_bderssimp() {
+
+  test(single(SEQ(ALTS(ONE,CHAR('c')),
+  SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 1) { (r: Rexp) => 
+  // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
+    val ss = Set("aa")//stringsFromRexp(r)
+    val boolList = ss.map(s => {
+      //val bdStrong = bdersStrong(s.toList, internalise(r))
+      val bds = bsimp(bders(s.toList, internalise(r)))
+      val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
+      //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
+      //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
+      //rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
+      //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
+      //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
+      rprint(r)
+      println(bds)
+      println(bdssimp)
+      bds == bdssimp
+    })
+    //!boolList.exists(b => b == false)
+    !boolList.exists(b => b == false)
+  }
+}
+//  bders_bderssimp()
+  
+
+
lexing