--- a/exps/bit.scala Wed Mar 13 12:31:03 2019 +0000
+++ b/exps/bit.scala Sat Mar 16 11:15:22 2019 +0000
@@ -32,7 +32,9 @@
abstract class Rexp
case object ZERO extends Rexp
case object ONE extends Rexp
-case class PRED(f: Char => Boolean, s: String = "_") extends Rexp
+case class PRED(f: Char => Boolean, s: String = "_") extends Rexp {
+ override def toString = "'" ++ s ++ "'"
+}
case class ALTS(rs: List[Rexp]) extends Rexp
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp
case class STAR(r: Rexp) extends Rexp
@@ -49,7 +51,9 @@
abstract class ARexp
case object AZERO extends ARexp
case class AONE(bs: Bits) extends ARexp
-case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp
+case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp {
+ override def toString = "'" ++ s ++ "'"
+}
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp
case class ASTAR(bs: Bits, r: ARexp) extends ARexp
@@ -94,29 +98,39 @@
// string of a regular expressions - for testing purposes
-def string(r: Rexp): String = r match {
+def string(r: Rexp, s: String = ""): String = r match {
case ZERO => "0"
case ONE => "1"
- case PRED(_, s) => s
- case ALTS(rs) => rs.map(string).mkString("[", "|", "]")
- case SEQ(r1, r2) => s"(${string(r1)} ~ ${string(r2)})"
- case STAR(r) => s"{${string(r)}}*"
- case RECD(x, r) => s"(${x}! ${string(r)})"
+ case PRED(_, s1) => s1
+ case ALTS(rs) => rs.map(string(_, s ++ " ")).mkString("[", ",\n" ++ s ++ "|", "]")
+ case SEQ(r1, r2) => {
+ val s1 = string(r1, s)
+ val i = (s1 ++ "\n").toList.indexOf('\n')
+ val s2 = string(r2, (" " * i) + " ")
+ s"${s1} ~ ${s2}"
+ }
+ case STAR(r) => s"<${string(r, s ++ " ")}>*"
+ case RECD(x, r) => s"(${x}! ${string(r, s)})"
}
def strings(rs: Set[Rexp]): String =
- rs.map(string).mkString("{", "|", "}")
+ rs.map(string(_, "")).mkString("{", ",\n|", "}")
// string of an annotated regular expressions - for testing purposes
-
-def astring(a: ARexp): String = a match {
+def astring(a: ARexp, s: String = ""): String = a match {
case AZERO => "0"
case AONE(_) => "1"
case APRED(_, _, s) => s
- case AALTS(_, rs) => rs.map(astring).mkString("[", "|", "]")
- case ASEQ(_, r1, r2) => s"(${astring(r1)} ~ ${astring(r2)})"
- case ASTAR(_, r) => s"{${astring(r)}}*"
+ case AALTS(_, rs) => rs.map(astring(_, s ++ " ")).mkString("[", ",\n" ++ s ++ "|", "]")
+ case ASEQ(_, r1, r2) => {
+ val s1 = astring(r1, s)
+ val i = (s1 ++ "\n").toList.indexOf('\n')
+ val s2 = astring(r2, (" " * i) + " ")
+ s"${s1} ~ ${s2}"
+ }
+ case ASTAR(_, r) => s"<${astring(r, s ++ " ")}>*"
}
+
//--------------------------------------------------------------
@@ -302,8 +316,6 @@
case c::cs => pder(c, r).flatMap(pders_simp(cs, _)).map(simp(_)._1)
}
-def psize(rs: Set[Rexp]) =
- rs.map(size).sum
//--------------------------------------------------------------------
// BITCODED PART
@@ -323,6 +335,8 @@
case ZERO => AZERO
case ONE => AONE(Nil)
case PRED(f, s) => APRED(Nil, f, s)
+ case ALTS(List(r1)) =>
+ AALTS(Nil, List(fuse(List(Z), internalise(r1))))
case ALTS(List(r1, r2)) =>
AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))))
case ALTS(r1::rs) => {
@@ -433,19 +447,24 @@
case r1 :: rs2 => r1 :: flats(rs2)
}
+def stack(r1: ARexp, r2: ARexp) = r1 match {
+ case AONE(bs2) => fuse(bs2, r2)
+ case _ => ASEQ(Nil, r1, r2)
+}
+
def bsimp(r: ARexp): ARexp = r match {
case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
case (AZERO, _) => AZERO
case (_, AZERO) => AZERO
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
- //case (AALTS(bs2, rs), r2s) =>
- // AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s)))
+ case (AALTS(bs2, rs), r2s) =>
+ AALTS(bs1 ++ bs2, rs.map(stack(_, r2s)))
case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
}
case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp)), erase) match {
case Nil => AZERO
case r :: Nil => fuse(bs1, r)
- case rs => AALTS(bs1, rs)
+ case rs2 => AALTS(bs1, rs2)
}
//case ASTAR(bs1, r1) => ASTAR(bs1, bsimp(r1))
case r => r
@@ -479,8 +498,8 @@
case (AZERO, _) => AZERO
case (_, AZERO) => AZERO
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
- //case (AALTS(bs2, rs), r2s) =>
- // AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s)))
+ case (AALTS(bs2, rs), r2s) =>
+ AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s)))
case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
}
case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp_full)), erase) match {
@@ -636,6 +655,8 @@
def asize(a: ARexp) = size(erase(a))
+def psize(rs: Set[Rexp]) = rs.map(size).sum
+
// Lexing Rules for a Small While Language
@@ -679,10 +700,29 @@
// Some Small Tests
//==================
+// string of a regular expressions - for testing purposes
+
+
+string(ALTS(List("a","b",ALTS(List("0","1","2")),"c")))
+string(ALTS(List("a","b",ALTS(List("0","1",ALTS(List("X","Y")),"2")),"c")))
+string(ALTS(List("aa","b",ALTS(List("0","1","2")),"c")))
+string(ALTS(List("aa","b",SEQ("Q", ALTS(List("0","1","2"))),"c")))
+string(ALTS(List("aa","b",SEQ(SEQ("Q", ALTS(List("0","1","2"))),"W"),"c")))
+string(ALTS(List("aa","b",SEQ("Q", STAR(ALTS(List("0","1","2")))),"c")))
+string(ALTS(List("aaa","bbbb",ALTS(List("000","1111","2222")),"ccccc")))
+
println("Small tests")
-val q = STAR(STAR("bb" | ("a" | "b")))
-val qs = "bb"
+val q = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c')))))))
+val qs = "cccc"
+
+//val q = STAR(STAR("bb" | ("a" | "b")))
+//val qs = "bbbbbbb"
+
+println("Size Bit " + asize(bders_simp(qs.toList, internalise(q))))
+println("Size Pder " + psize(pders_simp(qs.toList, q)))
+println(astring(bders_simp(qs.toList, internalise(q))))
+println(strings(pders_simp(qs.toList, q)))
println("Size Bit " + asize(bders_simp(qs.toList, internalise(q))))
println("Size Bitf " + asize(bders_simp_full(qs.toList, internalise(q))))
@@ -692,11 +732,13 @@
println("Size Pder simp " + psize(pders_simp(qs.toList, q)))
println(astring(bders_simp(qs.toList, internalise(q))))
-println(astring(bders_simp_full(qs.toList, internalise(q))))
-println(string(ders_simp(qs.toList, q)))
-println(strings(pders(qs.toList, q)))
+//println(astring(bders_simp_full(qs.toList, internalise(q))))
+//println(string(ders_simp(qs.toList, q)))
+//println(strings(pders(qs.toList, q)))
println(strings(pders_simp(qs.toList, q)))
+
+
System.exit(0)
val re1 = STAR("a" | "aa")