# HG changeset patch
# User Chengsong
# Date 1642455090 0
# Node ID 549257d0b8b2ff97df2128d79f47cf2c7fbb6d31
# Parent  d7f0153f5770facfa5bfc1e728ffa952f3219443
zre7correct

diff -r d7f0153f5770 -r 549257d0b8b2 thys2/zre7.sc
--- a/thys2/zre7.sc	Mon Jan 17 20:51:03 2022 +0000
+++ b/thys2/zre7.sc	Mon Jan 17 21:31:30 2022 +0000
@@ -69,11 +69,14 @@
 
 //parse r[p...q] --> v
 
-
+//(a+aa)*
+//aaa
+//[R(Sequ(a, a)), vs]
+//[L(a), L(a), vs]
 def check_before_down(c: Ctx, r: Rexp, d: Int = 0) : List[Zipper] = {
     mems.get((pos, r)) match {
         case Some(m) => 
-            m.parents = c::Nil//c::m.parents
+            //m.parents = c::m.parents
             m.result.find(tup2 => tup2._1 == pos) match {
                 // case Some((i, v)) => 
                 //   original_up(v, c, d)
@@ -87,6 +90,11 @@
     }
 }
 
+//mems  pstart r  --> m parents [(pend, vres), ...]
+//aaa
+//012
+//seq a a 
+//0 a~a --> m ... [(2, Sequ a a)]
 
 
 def mem_up(vres: Val, m: Mem, rec_depth : Int = 0) : List[Zipper] = {
@@ -341,28 +349,28 @@
 
 mems.clear()
 val re1 = ("a" | "aa").%
-val re1ss = lex(re1, "aa")
+val re1ss = lex(re1, "aaaaa")
 
-// drawZippers(re1ss)
-// println(actualZipperSize(re1ss))
-// println(re1ss)
-//val re1S = zipperSimp(re1ss)
+//drawZippers(re1ss)
+println(actualZipperSize(re1ss))
+//println(re1ss)
+val re1S = zipperSimp(re1ss)
 //println(actualZipperSize(re1S))
 
 
-val re2 = SEQ(ONE, "a")
-val re2res = lex(re2, "a")
-//lex(1~a, "a") --> lexRecurse((1v, m  (SeqC(m (RootC, Nil) ))))
+// val re2 = SEQ(ONE, "a")
+// val re2res = lex(re2, "a")
+// //lex(1~a, "a") --> lexRecurse((1v, m  (SeqC(m (RootC, Nil), Nil, [1~a] ) )))
 
 
-println(re2res)
+// println(re2res)
 
-val re2resPlugged = plug_all(re2res)
-re2resPlugged.foreach(v => {
-        val Sequ(Empty, vp) = v
-        println(vp)
-}
-)
+// val re2resPlugged = plug_all(re2res)
+// re2resPlugged.foreach(v => {
+//         val Sequ(Empty, vp) = v
+//         println(vp)
+// }
+// )
 
 // println("remaining regex")
 // println(re1ss.flatMap(z => zipBackMem(z._2)))