The C(Char) construct is incompatible with the code and retrieve in Fahad's thesis.
This causes the exception.
Two ways of fixing this: delete C(C) construct (easy way around) or amend retrieve code etc.
since the C(C) construct is intended for decoding Pred, and we don't use pred now, we shall delete this.
This is the last veersion that contains C(CHAR)
--- a/Spiral.scala Sat Mar 23 11:53:09 2019 +0000
+++ b/Spiral.scala Wed Apr 10 16:34:34 2019 +0100
@@ -434,14 +434,15 @@
}
//simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set)
def pushbits(r: ARexp): ARexp = r match {
- case AALTS(bs, rs) => AALTS(Nil, rs.map(fuse(bs, _)))
+ case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+ case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
case r => r
}
def correctness_proof_convenient_path(){
- for(i <- 1 to 1)
+ for(i <- 1 to 10000)
{
- val s = "baa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
- val r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),'c'), ACHAR(List(S),'b'))),ASEQ(List(),ASTAR(List(),ACHAR(List(),'a')),AALTS(List(),List(ACHAR(List(Z),'a'), ACHAR(List(S),'a'))))))//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)
+ val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+ 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)
for(j <- 0 to s.length - 1){
val ss = s.slice(0, j+ 1)
val nangao = ders_simp(r, ss.toList)
@@ -463,6 +464,18 @@
}
}
}
+ def retrieve_experience(){
+ val rg = 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"))))
+ val st = "abaab"
+ val vl = blexing_simp(erase(rg), st)
+ val bts = retrieve(rg, vl)
+ val cdbts = code(vl)
+ if(bts != cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
+ println(bts)
+ println(cdbts)
+ println("NOoooooo.....!")
+ }
+ }
def radical_correctness(){
enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
@@ -470,7 +483,8 @@
def main(args: Array[String]) {
//check_all()
//radical_correctness()
- correctness_proof_convenient_path()
+ //correctness_proof_convenient_path()
+ retrieve_experience()
}
}
Binary file corr_pr_sketch.pdf has changed
--- a/corr_pr_sketch.tex Sat Mar 23 11:53:09 2019 +0000
+++ b/corr_pr_sketch.tex Wed Apr 10 16:34:34 2019 +0100
@@ -314,50 +314,129 @@
\begin{theorem}{
This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\
-Define pushbits as the following:\\
-$pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_))) \ else\ r$.\\
+Define pushbits as the following:\\
+\begin{verbatim}
+def pushbits(r: ARexp): ARexp = r match {
+ case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+ case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
+ case r => r
+ }
+ \end{verbatim}
Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\
Unfortunately this does not hold. A counterexample is\\
\begin{verbatim}
-r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),c), ACHAR(List(S),b))),ASEQ(List(),ASTAR(List(),ACHAR(List(),a)),AALTS(List(),List(ACHAR(List(Z),a), ACHAR(List(S),a))))))
+baa
+original regex
+STA
+ └-ALT
+ └-STA List(Z)
+ | └-a
+ └-ALT List(S)
+ └-b List(Z)
+ └-a List(S)
regex after ders simp
-
-SEQ
- └-ALT List(S, S, C(b))
- | └-SEQ
- | | └-STA List(S, C(a), S, C(a))
- | | | └-a
- | | └-a List(Z)
- | └-ONE List(S, C(a), Z, Z, C(a))
- └-STA
+ALT List(S, S, Z, C(b))
+ └-SEQ
+ | └-STA List(S, Z, S, C(a), S, C(a))
+ | | └-a
+ | └-STA
+ | └-ALT
+ | └-STA List(Z)
+ | | └-a
+ | └-ALT List(S)
+ | └-b List(Z)
+ | └-a List(S)
+ └-SEQ List(S, Z, S, C(a), Z)
+ └-ALT List(S)
+ | └-STA List(Z, S, C(a))
+ | | └-a
+ | └-ONE List(S, S, C(a))
+ └-STA
+ └-ALT
+ └-STA List(Z)
+ | └-a
+ └-ALT List(S)
+ └-b List(Z)
+ └-a List(S)
+regex after ders
+ALT
+ └-SEQ
+ | └-ALT List(S)
+ | | └-SEQ List(Z)
+ | | | └-ZERO
+ | | | └-STA
+ | | | └-a
+ | | └-ALT List(S)
+ | | └-ZERO
+ | | └-ZERO
+ | └-STA
+ | └-ALT
+ | └-STA List(Z)
+ | | └-a
+ | └-ALT List(S)
+ | └-b List(Z)
+ | └-a List(S)
+ └-ALT List(S, S, Z, C(b))
└-SEQ
- └-ALT
- | └-c List(Z)
- | └-b List(S)
- └-SEQ
- └-STA
- | └-a
+ | └-ALT List(S)
+ | | └-ALT List(Z)
+ | | | └-SEQ
+ | | | | └-ZERO
+ | | | | └-STA
+ | | | | └-a
+ | | | └-SEQ List(S, C(a))
+ | | | └-ONE List(S, C(a))
+ | | | └-STA
+ | | | └-a
+ | | └-ALT List(S)
+ | | └-ZERO
+ | | └-ZERO
+ | └-STA
+ | └-ALT
+ | └-STA List(Z)
+ | | └-a
+ | └-ALT List(S)
+ | └-b List(Z)
+ | └-a List(S)
+ └-SEQ List(S, Z, S, C(a), Z)
+ └-ALT List(S)
+ | └-SEQ List(Z)
+ | | └-ONE List(S, C(a))
+ | | └-STA
+ | | └-a
+ | └-ALT List(S)
+ | └-ZERO
+ | └-ONE List(S, C(a))
+ └-STA
└-ALT
- └-a List(Z)
- └-a List(S)
+ └-STA List(Z)
+ | └-a
+ └-ALT List(S)
+ └-b List(Z)
+ └-a List(S)
regex after ders and then a single simp
-SEQ
- └-ALT List(S)
- | └-SEQ List(S, C(b))
- | | └-STA List(S, C(a), S, C(a))
- | | | └-a
- | | └-a List(Z)
- | └-ONE List(S, C(b), S, C(a), Z, Z, C(a))
- └-STA
- └-SEQ
+ALT
+ └-SEQ List(S, S, Z, C(b))
+ | └-STA List(S, Z, S, C(a), S, C(a))
+ | | └-a
+ | └-STA
+ | └-ALT
+ | └-STA List(Z)
+ | | └-a
+ | └-ALT List(S)
+ | └-b List(Z)
+ | └-a List(S)
+ └-SEQ List(S, S, Z, C(b), S, Z, S, C(a), Z)
+ └-ALT List(S)
+ | └-STA List(Z, S, C(a))
+ | | └-a
+ | └-ONE List(S, S, C(a))
+ └-STA
└-ALT
- | └-c List(Z)
- | └-b List(S)
- └-SEQ
- └-STA
+ └-STA List(Z)
| └-a
- └-ALT
- └-a List(Z)
+ └-ALT List(S)
+ └-b List(Z)
└-a List(S)
\end{verbatim}
\end{theorem}
--- a/lex_blex_Frankensteined.scala Sat Mar 23 11:53:09 2019 +0000
+++ b/lex_blex_Frankensteined.scala Wed Apr 10 16:34:34 2019 +0100
@@ -92,7 +92,7 @@
def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
case (ONE, bs) => (Empty, bs)
case (CHAR(f), C(c)::bs) => (Chr(c), bs)
- case (ALTS(r::Nil), bs) => decode_aux(r, bs)//this case seems tailor made for those who want to simplify the regex before der or simp
+ //case (ALTS(r::Nil), bs) => decode_aux(r, bs)//this case seems only used when we simp a regex before derivatives and it contains things like alt("a")
case (ALTS(rs), bs) => bs match {
case Z::bs1 => {
val (v, bs2) = decode_aux(rs.head, bs1)
@@ -126,7 +126,25 @@
case _ => throw new Exception("Not decodable")
}
+ def code(v: Val): Bits = v match {
+ case Empty => Nil
+ case Left(v) => Z :: code(v)
+ case Right(v) => S :: code(v)
+ case Sequ(v1, v2) => code(v1) ::: code(v2)
+ case Stars(Nil) => Z::Nil
+ case Stars(v::vs) => S::code(v) ::: code(Stars(vs))
+ }
+
+ def retrieve(r: ARexp, v: Val): Bits = (r,v) match {
+ case (AONE(bs), Empty) => bs
+ case (ACHAR(bs, c), Chr(d)) => bs
+ case (AALTS(bs, as), Left(v)) => bs ++ retrieve(as.head,v)
+ case (AALTS(bs, as), Right(v)) => bs ++ retrieve(AALTS(Nil,as.tail),v)
+ case (ASEQ(bs, a1, a2), Sequ(v1, v2)) => bs ++ retrieve(a1, v1) ++ retrieve(a2, v2)
+ case (ASTAR(bs, a), Stars(Nil)) => bs ++ List(Z)
+ case (ASTAR(bs, a), Stars(v::vs)) => bs ++ List(S) ++ retrieve(a, v) ++ retrieve(ASTAR(Nil, a), Stars(vs))
+ }
//erase function: extracts the regx from Aregex
def erase(r:ARexp): Rexp = r match{
case AZERO => ZERO
@@ -397,8 +415,8 @@
case ASEQ(bs1, r1, r2) => (super_bsimp(r1), super_bsimp(r2)) match {
case (AZERO, _) => AZERO
case (_, AZERO) => AZERO
- case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
- case (AALTS(bs2, rs), r2) => AALTS(bs1 ++ bs2, rs.map(r => r match {case AONE(bs3) => fuse(bs3, r2) case r => ASEQ(Nil, r, r2)}) )
+ case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)//万一是(r1, alts(rs))这种形式呢
+ case (AALTS(bs2, rs), r2) => AALTS(bs1 ++ bs2, rs.map(r => r match {case AONE(bs3) => fuse(bs3, r2) case r => ASEQ(Nil, r, r2)} ) )
case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
}
case AALTS(bs1, rs) => {