Spiral.scala
changeset 107 b1e365afa29c
parent 103 aeb0bc2d1812
child 109 79f347cb8b4d
equal deleted inserted replaced
106:e0db3242d8b5 107:b1e365afa29c
   556     }
   556     }
   557     case _ => println("No simp at this level")
   557     case _ => println("No simp at this level")
   558   }
   558   }
   559   def tellmewhy(){
   559   def tellmewhy(){
   560     //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(ALTS(List(CHAR('a'), CHAR('a'))), STAR(CHAR('a'))))) 
   560     //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(ALTS(List(CHAR('a'), CHAR('a'))), STAR(CHAR('a'))))) 
   561     val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(CHAR('a'), STAR(CHAR('a')) ) ))
   561     //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(CHAR('a'), STAR(CHAR('a')) ) ))
       
   562     val r = ("ab" | (  (("a")%) | "aa")  )
   562     //val r = ("a"|"b")~("a")
   563     //val r = ("a"|"b")~("a")
   563     val s = "aa"
   564     val s = "aa"
   564     for(i <- 0 to s.length-1){
   565     for(i <- 0 to s.length-1){
   565       val ss = s.slice(0, i+1)
   566       val ss = s.slice(0, i+1)
   566       val nangao = ders_simp(internalise(r), ss.toList)
   567       val nangao = bders_simp_rf(ss.toList, internalise(r))
   567       val easy = (bders(ss.toList, internalise(r)))
   568       val easy = (bders(ss.toList, internalise(r)))
   568       println(bits_print(nangao))
   569       println(bits_print(nangao))
       
   570       println()
   569       println(bits_print(easy))
   571       println(bits_print(easy))
   570       println()
   572       println()
   571       bsimp_print(easy)
   573       println(bits_print(bsimp_rf(easy)))
       
   574       println()
   572     }
   575     }
   573     println(bits_print(bsimp(bders(s.toList, internalise(r)))))
   576     println(bits_print(bsimp(bders(s.toList, internalise(r)))))
   574     println(bits_print(ders_simp(internalise(r), s.toList)))
   577     println(bits_print(ders_simp(internalise(r), s.toList)))
   575   }
   578   }
   576   def find_re(){
   579   def find_re(){
   589     case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
   592     case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
   590     case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
   593     case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
   591     case r => r
   594     case r => r
   592   }
   595   }
   593   def correctness_proof_convenient_path(){
   596   def correctness_proof_convenient_path(){
   594         val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
   597     for(i <- 1 to 19999){
   595         val r = ("ab"| SEQ(ONE, "ab"))//internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
   598         val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
       
   599         val r = internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
   596         for(j <- 0 to s.length - 1){
   600         for(j <- 0 to s.length - 1){
   597           val ss = s.slice(0, j+ 1)
   601           val ss = s.slice(0, j+ 1)
   598           val nangao = ders_simp(internalise(r), ss.toList)
   602           val nangao = bders_simp_rf(ss.toList, r)
   599           val easy = bsimp(bders(ss.toList, internalise(r)))
   603           val easy = bsimp_rf(bders_rf(ss.toList, r))
   600           if(!(nangao == easy || pushbits(nangao) == (easy))){
   604           if(!(nangao == easy)){
   601             println(j)
   605             println(j)
   602             println("not equal")
   606             println("not equal")
   603             println("string")
   607             println("string")
   604             println(ss)
   608             println(ss)
   605             println("original regex")
   609             println("original regex")
   606             println(regx_tree(r))
   610             println(annotated_tree(r))
   607             println("regex after ders simp")
   611             println("regex after ders simp")
   608             println(annotated_tree(nangao))
   612             println(annotated_tree(nangao))
   609             println("regex after ders")
   613             println("regex after ders")
   610             println(annotated_tree(bders(ss.toList, internalise(r))))//flats' fuse when opening up AALTS causes the difference
   614             println(annotated_tree(bders(ss.toList, r)))//flats' fuse when opening up AALTS causes the difference
   611             println("regex after ders and then a single simp")
   615             println("regex after ders and then a single simp")
   612             println(annotated_tree(easy))
   616             println(annotated_tree(easy))
   613           }
   617           }
   614         }
   618         }
       
   619       }
   615   }
   620   }
   616   /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
   621   /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
   617       println(bts)
   622       println(bts)
   618       println(cdbts)
   623       println(cdbts)
   619       println("code v = retrieve internalise(r) v if |- v : r")
   624       println("code v = retrieve internalise(r) v if |- v : r")
   837   }
   842   }
   838 
   843 
   839   def main(args: Array[String]) {
   844   def main(args: Array[String]) {
   840     //println(S.toString)
   845     //println(S.toString)
   841     //find_re()
   846     //find_re()
       
   847     //tellmewhy()
       
   848     //correctness_proof_convenient_path()
   842     tellmewhy()
   849     tellmewhy()
   843     //string_der_test()
   850     //string_der_test()
   844     //comp(rd_string_gen(3,6).toList, random_struct_gen(7))
   851     //comp(rd_string_gen(3,6).toList, random_struct_gen(7))
   845     //newxp1()
   852     //newxp1()
   846   //contains7()
   853   //contains7()