thys2/blexer2.sc
changeset 543 b2bea5968b89
parent 541 5bf9f94c02e1
child 545 333013923c5a
equal deleted inserted replaced
542:a7344c9afbaf 543:b2bea5968b89
   615             case Nil => AZERO
   615             case Nil => AZERO
   616             case s :: Nil => fuse(bs1, s)
   616             case s :: Nil => fuse(bs1, s)
   617             case rs => AALTS(bs1, rs)  
   617             case rs => AALTS(bs1, rs)  
   618           }
   618           }
   619     }
   619     }
   620     case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
   620     //(erase(r0))) => AONE(bs)
   621     case r => r
   621     case r => r
   622   }
   622   }
   623 }
   623 }
   624 
   624 
   625 def distinctWith(rs: List[ARexp], 
   625 def distinctWith(rs: List[ARexp], 
   779     }
   779     }
   780 }
   780 }
   781 
   781 
   782 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
   782 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
   783 //   where
   783 //   where
   784 // "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) ⊆ (L (erase (AALTs [] rsa))) then AZERO else
   784 // "pAKC_aux rsa r ctx = (if (regConcat (SEQ (erase r) ( ctx) )) ⊆ (regConcat (erase (AALTs [] rsa))) then AZERO else
   785 //                           case r of (ASEQ bs r1 r2) ⇒ 
   785 //                           case r of (ASEQ bs r1 r2) ⇒ 
   786 //                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
   786 //                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
   787 //                                     (AALTs bs rs) ⇒ 
   787 //                                     (AALTs bs rs) ⇒ 
   788 //                             bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) )    |
   788 //                             bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) )    |
   789 //                                     r             ⇒ r
   789 //                                     r             ⇒ r
   794 //   case r1::r2::Nil => SEQ(SEQ(r1, r2), acc)
   794 //   case r1::r2::Nil => SEQ(SEQ(r1, r2), acc)
   795 // }
   795 // }
   796 
   796 
   797 
   797 
   798 //the "fake" Language interpretation: just concatenates!
   798 //the "fake" Language interpretation: just concatenates!
   799 def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
   799 def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
   800   case Nil => acc
   800   case Nil => acc
   801   case r :: rs1 => 
   801   case r :: rs1 => 
   802     // if(acc == ONE) 
   802     // if(acc == ONE) 
   803     //   L(r, rs1) 
   803     //   regConcat(r, rs1) 
   804     // else
   804     // else
   805       L(SEQ(acc, r), rs1)
   805       regConcat(SEQ(acc, r), rs1)
   806 }
   806 }
   807 
   807 
   808 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
   808 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
   809 def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
   809 def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
   810 
   810 
   817   // println("acc")
   817   // println("acc")
   818   // rsprint(acc)
   818   // rsprint(acc)
   819   // println("ctx---------")
   819   // println("ctx---------")
   820   // rsprint(ctx)
   820   // rsprint(ctx)
   821   // println("ctx---------end")
   821   // println("ctx---------end")
   822   // rsprint(breakIntoTerms(L(erase(r), ctx)).map(oneSimp))
   822   // rsprint(breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp))
   823 
   823 
   824   if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
   824   if (breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
   825     AZERO
   825     AZERO
   826   }
   826   }
   827   else{
   827   else{
   828     r match {
   828     r match {
   829       case ASEQ(bs, r1, r2) => 
   829       case ASEQ(bs, r1, r2) => 
   898   case CHAR(c) => false
   898   case CHAR(c) => false
   899   case ZERO => false
   899   case ZERO => false
   900 
   900 
   901 }
   901 }
   902 
   902 
       
   903 def isOne1(r: Rexp) : Boolean = r match {
       
   904   case ONE => true
       
   905   case SEQ(r1, r2) => false//isOne1(r1) && isOne1(r2)
       
   906   case ALTS(r1, r2) => false//(isOne1(r1) || isOne1(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
       
   907   case STAR(r0) => false//atMostEmpty(r0)
       
   908   case CHAR(c) => false
       
   909   case ZERO => false
       
   910 
       
   911 }
       
   912 
   903 def turnIntoTerms(r: Rexp): List[Rexp] = r match {
   913 def turnIntoTerms(r: Rexp): List[Rexp] = r match {
   904   case SEQ(r1, r2)  => if(isOne(r1)) 
   914   case SEQ(r1, r2)  => if(isOne1(r1)) 
   905                           turnIntoTerms(r2) 
   915                           turnIntoTerms(r2) 
   906                        else 
   916                        else 
   907                           turnIntoTerms(r1).map(r11 => SEQ(r11, r2))
   917                           turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
   908   case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
   918   case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
   909   case ZERO => Nil
   919   case ZERO => Nil
   910   case _ => r :: Nil
   920   case _ => r :: Nil
   911 }
   921 }
   912 
   922 
       
   923 def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
       
   924   if(r11 == ONE)
       
   925     turnIntoTerms(r2)
       
   926   else
       
   927     SEQ(r11, r2) :: Nil
       
   928 }
       
   929 
   913 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
   930 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
   914   val res = turnIntoTerms((L(erase(r), ctx))).map(oneSimp)
   931   turnIntoTerms((regConcat(erase(r), ctx)))
   915   res.toSet
   932     .toSet
   916 }
   933 }
   917 
   934 
   918 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = {
   935 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
   919   val res = turnIntoTerms((L(r, ctx))).map(oneSimp)
   936   turnIntoTerms(regConcat(r, ctx)).toSet
   920   res.toSet
   937 
   921 }
   938 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 
   922 
   939 subseteqPred: (C, C) => Boolean) : Boolean = {
   923 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = {
       
   924   subseteqPred(f(a, b), c)
   940   subseteqPred(f(a, b), c)
   925 }
   941 }
   926 def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = {
   942 def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
   927   val res = rs1.forall(rs2.contains)
   943   //rs1 \subseteq rs2
   928   res
   944   rs1.forall(rs2.contains)
   929 }
   945 
   930 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
   946 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
       
   947   // if (erase(r) == ONE &&  acc != Set()) 
       
   948   // {
       
   949   //   println("ctx")
       
   950   //   rsprint(ctx)
       
   951   //   println("acc")
       
   952   //   rsprint(acc)
       
   953   //   println("acc-end")
       
   954   // }
   931   if (ABIncludedByC(a = r, b = ctx, c = acc, 
   955   if (ABIncludedByC(a = r, b = ctx, c = acc, 
   932                     f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
   956                     f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
   933   {//acc.flatMap(breakIntoTerms
   957   {
   934     AZERO
   958     AZERO
   935   }
   959   }
   936   else{
   960   else{
   937     r match {
   961     r match {
   938       case ASEQ(bs, r1, r2) => 
   962       case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
   939       (prune6(acc, r1, erase(r2) :: ctx)) match{
       
   940         case AZERO => 
   963         case AZERO => 
   941           AZERO
   964           AZERO
   942         case AONE(bs1) => 
   965         case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
   943           fuse(bs1, r2)
   966           prune6(acc, fuse(bs1, r2), ctx)
   944         case r1p => 
   967         case r1p => 
   945           ASEQ(bs, r1p, r2)
   968           ASEQ(bs, r1p, r2)
   946       }
   969       }
   947       case AALTS(bs, rs0) => 
   970       case AALTS(bs, rs0) => 
   948         rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
   971         rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
   949           case Nil => 
   972           case Nil => 
   950             AZERO
   973             AZERO
   951           case r :: Nil => 
   974           case r :: Nil => 
   952             r 
   975             fuse(bs, r) 
   953           case rs0p => 
   976           case rs0p => 
   954             AALTS(bs, rs0p)
   977             AALTS(bs, rs0p)
   955         }
   978         }
   956       case r => r
   979       case r => r
   957     }
   980     }
   987       case r => r
  1010       case r => r
   988     }
  1011     }
   989   }
  1012   }
   990 }
  1013 }
   991 
  1014 
   992 def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : List[ARexp] = xs match {
  1015 def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : 
       
  1016 List[ARexp] = xs match {
   993   case Nil => 
  1017   case Nil => 
   994     Nil
  1018     Nil
   995   case x :: xs => {
  1019   case x :: xs => {
   996     val erased = erase(x)
  1020     val erased = erase(x)
   997     if(acc.contains(erased)){
  1021     if(acc.contains(erased)){
   998       distinctBy6(xs, acc)
  1022       distinctBy6(xs, acc)
   999     }
  1023     }
  1000     else{
  1024     else{
  1001       val pruned = prune6(acc, x, Nil)
  1025       val pruned = prune6(acc, x)
  1002       val newTerms = turnIntoTerms(erase(pruned))
  1026       val newTerms = turnIntoTerms(erase(pruned))
  1003       pruned match {
  1027       pruned match {
  1004         case AZERO => 
  1028         case AZERO => 
  1005           distinctBy6(xs, acc)
  1029           distinctBy6(xs, acc)
  1006         case xPrime => 
  1030         case xPrime => 
  1007           xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
  1031           xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
  1008       }
  1032       }
  1009     }
  1033     }
  1010   }
  1034   }
  1011 }
  1035 }
  1012 
  1036 
  1035   case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
  1059   case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
  1036   case ZERO => Nil
  1060   case ZERO => Nil
  1037   case _ => r::Nil
  1061   case _ => r::Nil
  1038 }
  1062 }
  1039 
  1063 
       
  1064 def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
       
  1065   //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
       
  1066   case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
       
  1067   case ZERO => Nil
       
  1068   case _ => r::Nil
       
  1069 }
  1040 
  1070 
  1041 
  1071 
  1042 def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
  1072 def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
  1043   case (ONE, bs) => (Empty, bs)
  1073   case (ONE, bs) => (Empty, bs)
  1044   case (CHAR(f), bs) => (Chr(f), bs)
  1074   case (CHAR(f), bs) => (Chr(f), bs)
  1243     case ONE => rs
  1273     case ONE => rs
  1244     case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
  1274     case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
  1245   }
  1275   }
  1246   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
  1276   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
  1247     case ZERO => Set()
  1277     case ZERO => Set()
  1248     case ONE => l
  1278     // case ONE => l
  1249     case t => l.map( m => m._2 match 
  1279     case t => l.map( m => m._2 match 
  1250       {
  1280       {
  1251         case ZERO => m 
  1281         case ZERO => m 
  1252         case ONE => (m._1, t) 
  1282         case ONE => (m._1, t) 
  1253         case p => (m._1, SEQ(p, t)) 
  1283         case p => (m._1, SEQ(p, t)) 
  1254       }  
  1284       }  
  1255     
  1285     
  1256     )
  1286     )
  1257   }
  1287   }
       
  1288   def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
       
  1289     case ZERO => Nil
       
  1290     case ONE => l
       
  1291     case t => l.map(m => m._2 match
       
  1292       {
       
  1293         case ZERO => m
       
  1294         case ONE => (m._1, t)
       
  1295         case p => (m._1, SEQ(p, t))
       
  1296       }
       
  1297     )
       
  1298 
       
  1299   }
       
  1300   def lfList(r: Rexp) : List[Mon] = r match {
       
  1301     case ZERO => Nil
       
  1302     case ONE => Nil
       
  1303     case CHAR(f) => {
       
  1304       (f, ONE) :: Nil
       
  1305     }
       
  1306     case ALTS(r1, r2) => {
       
  1307       lfList(r1) ++ lfList(r2)
       
  1308     }
       
  1309     case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
       
  1310     case SEQ(r1, r2) => {
       
  1311       if(nullable(r1))
       
  1312         cir_prodList(lfList(r1), r2) ++ lfList(r2)
       
  1313       else
       
  1314         cir_prodList(lfList(r1), r2)
       
  1315     }
       
  1316   }
       
  1317   def lfprint(ls: Lin) = ls.foreach(m =>{
       
  1318     println(m._1)
       
  1319     rprint(m._2)
       
  1320     })
  1258   def lf(r: Rexp): Lin = r match {
  1321   def lf(r: Rexp): Lin = r match {
  1259     case ZERO => Set()
  1322     case ZERO => Set()
  1260     case ONE => Set()
  1323     case ONE => Set()
  1261     case CHAR(f) => {
  1324     case CHAR(f) => {
  1262       //val Some(c) = alphabet.find(f) 
  1325       //val Some(c) = alphabet.find(f) 
  1401 }
  1464 }
  1402 // small()
  1465 // small()
  1403 
  1466 
  1404 def aaa_star() = {
  1467 def aaa_star() = {
  1405   val r = STAR(("a" | "aa"))
  1468   val r = STAR(("a" | "aa"))
  1406   for(i <- 0 to 100) {
  1469   for(i <- 0 to 20) {
  1407     val prog = "a" * i
  1470     val prog = "a" * i
       
  1471     print(i+" ")
  1408     println(asize(bders_simp(prog.toList, internalise(r))))
  1472     println(asize(bders_simp(prog.toList, internalise(r))))
       
  1473     //println(size(ders_simp(prog.toList, r)))
  1409   }
  1474   }
  1410 }
  1475 }
  1411 // aaa_star()
  1476 // aaa_star()
  1412 def naive_matcher() {
  1477 def naive_matcher() {
  1413   val r = STAR(STAR("a") ~ STAR("a"))
  1478   val r = STAR(STAR("a") ~ STAR("a"))
  1436   //   println()
  1501   //   println()
  1437   // }
  1502   // }
  1438   
  1503   
  1439 }
  1504 }
  1440 // naive_matcher()
  1505 // naive_matcher()
       
  1506 //single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
       
  1507 //  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
       
  1508 
       
  1509 
       
  1510 //STAR(SEQ(ALTS(CHAR(b),STAR(CHAR(b))),ALTS(ALTS(ONE,CHAR(b)),SEQ(CHAR(c),ONE))))
  1441 def generator_test() {
  1511 def generator_test() {
  1442 
  1512 
  1443   test(single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
  1513   test(single(STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))), 1) { (r: Rexp) => 
  1444   SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))), 1) { (r: Rexp) => 
       
  1445   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
  1514   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
  1446     val ss = stringsFromRexp(r)
  1515     val ss = Set("ab")//stringsFromRexp(r)
  1447     val boolList = ss.map(s => {
  1516     val boolList = ss.map(s => {
  1448       //val bdStrong = bdersStrong(s.toList, internalise(r))
  1517       //val bdStrong = bdersStrong(s.toList, internalise(r))
  1449       val bdStrong6 = bdersStrong6(s.toList, internalise(r))
  1518       val bdStrong6 = bdersStrong6(s.toList, internalise(r))
  1450       val bdStrong6Set = turnIntoTerms(erase(bdStrong6))
  1519       val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
  1451       val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
  1520       val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
  1452       val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
  1521       val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
  1453       rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
  1522       (rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList)) ||
  1454       //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
  1523       bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
  1455       //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
  1524       rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken))//|| bdStrong6Set.size <= pdersSetBroken.size
       
  1525       
  1456     })
  1526     })
  1457     //!boolList.exists(b => b == false)
  1527     //!boolList.exists(b => b == false)
  1458     !boolList.exists(b => b == false)
  1528     !boolList.exists(b => b == false)
  1459   }
  1529   }
  1460 }
  1530 }
  1461 // small()
  1531 // small()
  1462 //  generator_test()
  1532 // generator_test()
  1463   
  1533 
       
  1534 
  1464   
  1535   
  1465   //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
  1536   //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
  1466           //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
  1537           //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
  1467           //  CHAR('c')))))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
  1538           //  CHAR('c')))))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
  1468 //counterexample1: STAR(SEQ(ALTS(STAR(ZERO),ALTS(CHAR(a),CHAR(b))),SEQ(ONE,ALTS(CHAR(a),CHAR(b)))))
  1539 //counterexample1: STAR(SEQ(ALTS(STAR(ZERO),ALTS(CHAR(a),CHAR(b))),SEQ(ONE,ALTS(CHAR(a),CHAR(b)))))
  1469 //counterexample2: SEQ(ALTS(SEQ(CHAR(a),STAR(ONE)),STAR(ONE)),ALTS(CHAR(a),SEQ(ALTS(CHAR(c),CHAR(a)),CHAR(b))))
  1540 //counterexample2: SEQ(ALTS(SEQ(CHAR(a),STAR(ONE)),STAR(ONE)),ALTS(CHAR(a),SEQ(ALTS(CHAR(c),CHAR(a)),CHAR(b))))
  1470 
  1541 
  1471 //new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
  1542 //new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
  1472 //new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
  1543 //new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
  1473 //new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
  1544 //new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
       
  1545 //circular double-nullable STAR(SEQ((STAR("b") | "a" | "b"), ("b" | ONE)))
  1474 def counterexample_check() {
  1546 def counterexample_check() {
  1475   val r = SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
  1547   val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
  1476   SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
  1548     ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
  1477     //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
  1549     //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
  1478   val s = "b"
  1550   val s = "ab"
  1479   val bdStrong5 = bdersStrong7(s.toList, internalise(r))
  1551   val bdStrong5 = bdersStrong6(s.toList, internalise(r))
  1480   val bdStrong5Set = turnIntoTerms(erase(bdStrong5))
  1552   val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
  1481   val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
  1553   val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
  1482   val apdersSet = pdersSet.map(internalise)
  1554   val apdersSet = pdersSet.map(internalise)
  1483   println("original regex ")
  1555   println("original regex ")
  1484   rprint(r)
  1556   rprint(r)
  1485   println("after strong bsimp")
  1557   println("after strong bsimp")
  1488   rsprint(bdStrong5Set)
  1560   rsprint(bdStrong5Set)
  1489   println("after pderUNIV")
  1561   println("after pderUNIV")
  1490   rsprint(pdersSet.toList)
  1562   rsprint(pdersSet.toList)
  1491   println("pderUNIV distinctBy6")
  1563   println("pderUNIV distinctBy6")
  1492   //asprint(distinctBy6(apdersSet.toList))
  1564   //asprint(distinctBy6(apdersSet.toList))
  1493   rsprint(distinctByacc(pdersSet.toList))
  1565   rsprint((pdersSet.toList).flatMap(turnIntoTerms))
  1494   // rsprint(turnIntoTerms(pdersSet.toList(3)))
  1566   // rsprint(turnIntoTerms(pdersSet.toList(3)))
  1495   // println("NO 3 not into terms")
  1567   // println("NO 3 not into terms")
  1496   // rprint((pdersSet.toList()))
  1568   // rprint((pdersSet.toList()))
  1497   // println("after pderUNIV broken")
  1569   // println("after pderUNIV broken")
  1498   // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
  1570   // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
  1499 
  1571 
  1500 }
  1572 }
  1501 counterexample_check()
  1573 
       
  1574 // counterexample_check()
       
  1575 
       
  1576 def lf_display() {
       
  1577   val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
       
  1578     ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
       
  1579     //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
       
  1580   val s = "ab"
       
  1581   val bdStrong5 = bdersStrong6(s.toList, internalise(r))
       
  1582   val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
       
  1583   val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
       
  1584   val apdersSet = pdersSet.map(internalise)
       
  1585   lfprint(lf(r))
       
  1586 
       
  1587 }
       
  1588 
       
  1589 lf_display()
  1502 
  1590 
  1503 def breakable(r: Rexp) : Boolean = r match {
  1591 def breakable(r: Rexp) : Boolean = r match {
  1504   case SEQ(ALTS(_, _), _) => true
  1592   case SEQ(ALTS(_, _), _) => true
  1505   case SEQ(r1, r2) => breakable(r1)
  1593   case SEQ(r1, r2) => breakable(r1)
  1506   case _ => false
  1594   case _ => false
  1534 // SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
  1622 // SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
  1535 
  1623 
  1536 
  1624 
  1537 // 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))
  1625 // 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))
  1538 // 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))
  1626 // 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))
       
  1627 
       
  1628 
       
  1629 
       
  1630 
       
  1631 
       
  1632 def bders_bderssimp() {
       
  1633 
       
  1634   test(single(SEQ(ALTS(ONE,CHAR('c')),
       
  1635   SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 1) { (r: Rexp) => 
       
  1636   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
       
  1637     val ss = Set("aa")//stringsFromRexp(r)
       
  1638     val boolList = ss.map(s => {
       
  1639       //val bdStrong = bdersStrong(s.toList, internalise(r))
       
  1640       val bds = bsimp(bders(s.toList, internalise(r)))
       
  1641       val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
       
  1642       //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
       
  1643       //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
       
  1644       //rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
       
  1645       //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
       
  1646       //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
       
  1647       rprint(r)
       
  1648       println(bds)
       
  1649       println(bdssimp)
       
  1650       bds == bdssimp
       
  1651     })
       
  1652     //!boolList.exists(b => b == false)
       
  1653     !boolList.exists(b => b == false)
       
  1654   }
       
  1655 }
       
  1656 //  bders_bderssimp()
       
  1657   
       
  1658 
       
  1659