Spiral.scala
changeset 17 3241b1e71633
parent 16 c51178fa85fe
child 72 83b021fc7d29
equal deleted inserted replaced
16:c51178fa85fe 17:3241b1e71633
   486       println("v = ")
   486       println("v = ")
   487       println(unsimplified_vl)
   487       println(unsimplified_vl)
   488       println("frect v = ")
   488       println("frect v = ")
   489       println(frectv)
   489       println(frectv)
   490     }
   490     }
   491     */
   491     *///KH8W5BXL
   492   def retrieve_experience(){
   492   def nice_lex(r: Rexp, s: List[Char], ar: ARexp) : Val = s match {
   493     for(i <- 1 to 100){
   493     case Nil => 
   494       val rg = internalise(balanced_struct_gen(1))//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")))) 
   494     if (nullable(r)){
   495       val st = "ab"//"abaab"
   495       val vr = mkeps(r)
   496       val r_der_s = ders(st.toList, erase(rg))
   496       val bits1 = retrieve(ar, vr)
   497       if(nullable(r_der_s)){
   497       val av = bsimp2(ar, vr)
   498         val unsimplified_vl = mkeps(r_der_s)
   498       val bits2 = retrieve(av._1, av._2)
   499         val r_bder_s = bders( st.toList, rg)
   499       if(bits1 != bits2) throw new Exception("bsimp2 does not work")
   500         val s_r_bder_s = bsimp(r_bder_s)
   500       vr
   501         val bits1 = retrieve(internalise(r_der_s), unsimplified_vl)
   501     }  
   502         println("The property: ")
   502     else throw new Exception("Not matched")
   503         println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
   503     case c::cs => { 
   504         println("does not hold.")
   504       val vr = inj(r, c, nice_lex(der(c, r), cs, bder(c, ar)));
   505         println("Here v == mkeps r\\s and r == r\\s")
   505       val bits1 = retrieve(ar, vr);
   506         println("regular expression is")
   506       val av = bsimp2(ar, vr);
   507         println(rg)
   507       val bits2 = retrieve(av._1, av._2);
   508         println("string is")
   508       if(bits1 != bits2) throw new Exception("bsimp2 does not work");
   509         println(st)
   509       vr 
   510         println("derivative without simplification is ")
   510     }
   511         
   511   }
   512         println(r_bder_s)
   512   def test_bsimp2(){
   513 
   513     for(i <- 1 to 1000){
   514         println("after erase of this derivative")
   514       val rg = (balanced_struct_gen(9))//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")))) 
   515         println(erase(r_bder_s))
   515       val st = rd_string_gen(3, 4)
   516         println("simplification of derivative (bsimp(ar))")
   516       val a = internalise(rg)
   517         println(s_r_bder_s)
   517       val final_derivative = ders(st.toList, rg)
   518         println("after erase of simplified derivative (erase(bsimp(ar))")
   518       if(nullable(final_derivative))
   519         println(erase(s_r_bder_s))
   519         nice_lex(rg, st.toList, a)
   520         println("decode says the above regex and the below bits(code(v)) are not decodable")
   520     }
   521         println(unsimplified_vl)
   521   }
   522         println(code(unsimplified_vl))
   522 
   523         println(bits1)
   523   def neat_retrieve(){
   524         val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl)))
   524     for(i <- 1 to 1000){
   525           if(bits1 == bits2){
   525       val rg = internalise(balanced_struct_gen(6))//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")))) 
   526             println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
   526       val st = rd_string_gen(3, 5)
   527             println("Here v == mkeps r\\s and r == r\\s")
   527       val final_derivative = ders(st.toList, erase(rg))
   528             println(r_der_s, unsimplified_vl)
   528       if(nullable(final_derivative)){
   529             println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl))
   529         val unsimplified_vl = mkeps(final_derivative)
   530           }
   530         val arexp_for_retrieve = bders( st.toList, rg)
   531         }
   531         val simp_ar_vl = bsimp2(arexp_for_retrieve, unsimplified_vl)
   532       }
   532         val bits1 = retrieve(arexp_for_retrieve, unsimplified_vl)
   533     }
   533         val bits2 = retrieve(simp_ar_vl._1, simp_ar_vl._2)
       
   534         if(bits1 != bits2){
       
   535           println("nOOOOOOOOOO!")
       
   536         }
       
   537       }
       
   538     }
       
   539   }
       
   540 
   534   def radical_correctness(){
   541   def radical_correctness(){
   535     enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
   542     enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
   536     random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
   543     random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
   537   }
   544   }
   538   def christian_def(){
   545   def christian_def(){
   539     val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE))
   546     val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE))
   540     val v = Right(Empty)
   547     val v = Right(Empty)
   541     val a = internalise(r)
   548     val a = internalise(r)
   542     val as = bsimp(a)
   549     val a_v = bsimp2(a,v)
   543     println(s"Testing ${r} and ${v}")
   550     println(s"Testing ${r} and ${v}")
   544     println(s"internalise(r) = ${a}")
   551     println(s"internalise(r) = ${a}")
       
   552     println(s"a_v = ${a_v}")
   545     val bs1 = retrieve(a, v)
   553     val bs1 = retrieve(a, v)
   546     println(bs1)
   554     println(bs1)
   547     println(s"as = ${as}")
   555     println(s"as = ${a_v._1}")
   548     //val bs2 = retrieve(as, decode(erase(as), bs1))
   556     //val bs2 = retrieve(as, decode(erase(as), bs1))
   549     val bs3 = retrieve(as, decode(erase(as), bs1.tail))
   557     val bs3 = retrieve(a_v._1, a_v._2)//decode(erase(as), bs1) does not work
   550     println(decode(erase(as), bs1.tail))
   558     //println(decode(erase(as), bs1))
   551     println(bs3)
   559     println(s"bs1=${bs1}, bs3=${bs3}")
       
   560     //println(decode(erase(a_v._1), bs3))
   552   }
   561   }
   553   def essence_posix(){
   562   def essence_posix(){
   554     //val s = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
   563     //val s = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
   555     val s0 = "a"
   564     val s0 = "a"
   556     val r = SEQ(STAR(ALT("a", "aa")), "b")//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)
   565     val r = SEQ(STAR(ALT("a", "aa")), "b")//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)
   565   def main(args: Array[String]) {
   574   def main(args: Array[String]) {
   566     //check_all()   
   575     //check_all()   
   567     //radical_correctness()
   576     //radical_correctness()
   568     //correctness_proof_convenient_path()
   577     //correctness_proof_convenient_path()
   569     //retrieve_experience()
   578     //retrieve_experience()
       
   579     //neat_retrieve()
       
   580     test_bsimp2()
   570     //christian_def()
   581     //christian_def()
   571     essence_posix()
   582     //essence_posix()
   572   } 
   583   } 
   573 }
   584 }
   574 
   585