thys2/blexer2.sc
author Chengsong
Mon, 10 Jul 2023 01:51:46 +0100
changeset 661 71502e4d8691
parent 640 bd1354127574
permissions -rw-r--r--
overview of finiteness proof Gerog comment "not helpful", adding more intuitions of "closed forms"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
     1
//Strong Bsimp to obtain Antimirov's cubic bound
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
     2
431
Chengsong
parents:
diff changeset
     3
// A simple lexer inspired by work of Sulzmann & Lu
Chengsong
parents:
diff changeset
     4
//==================================================
Chengsong
parents:
diff changeset
     5
//
Chengsong
parents:
diff changeset
     6
// Call the test cases with 
Chengsong
parents:
diff changeset
     7
//
Chengsong
parents:
diff changeset
     8
//   amm lexer.sc small
Chengsong
parents:
diff changeset
     9
//   amm lexer.sc fib
Chengsong
parents:
diff changeset
    10
//   amm lexer.sc loops
Chengsong
parents:
diff changeset
    11
//   amm lexer.sc email
Chengsong
parents:
diff changeset
    12
//
Chengsong
parents:
diff changeset
    13
//   amm lexer.sc all
Chengsong
parents:
diff changeset
    14
514
036600af4c30 chapter2
Chengsong
parents: 500
diff changeset
    15
431
Chengsong
parents:
diff changeset
    16
Chengsong
parents:
diff changeset
    17
// regular expressions including records
Chengsong
parents:
diff changeset
    18
abstract class Rexp 
Chengsong
parents:
diff changeset
    19
case object ZERO extends Rexp
Chengsong
parents:
diff changeset
    20
case object ONE extends Rexp
Chengsong
parents:
diff changeset
    21
case object ANYCHAR extends Rexp
Chengsong
parents:
diff changeset
    22
case class CHAR(c: Char) extends Rexp
Chengsong
parents:
diff changeset
    23
case class ALTS(r1: Rexp, r2: Rexp) extends Rexp 
539
Chengsong
parents: 536
diff changeset
    24
case class ALTSS(rs: List[Rexp]) extends Rexp
431
Chengsong
parents:
diff changeset
    25
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp 
Chengsong
parents:
diff changeset
    26
case class STAR(r: Rexp) extends Rexp 
Chengsong
parents:
diff changeset
    27
case class RECD(x: String, r: Rexp) extends Rexp  
Chengsong
parents:
diff changeset
    28
case class NTIMES(n: Int, r: Rexp) extends Rexp
Chengsong
parents:
diff changeset
    29
case class OPTIONAL(r: Rexp) extends Rexp
Chengsong
parents:
diff changeset
    30
case class NOT(r: Rexp) extends Rexp
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    31
// records for extracting strings or tokens
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    32
431
Chengsong
parents:
diff changeset
    33
// values  
Chengsong
parents:
diff changeset
    34
abstract class Val
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    35
case object Failure extends Val
431
Chengsong
parents:
diff changeset
    36
case object Empty extends Val
Chengsong
parents:
diff changeset
    37
case class Chr(c: Char) extends Val
Chengsong
parents:
diff changeset
    38
case class Sequ(v1: Val, v2: Val) extends Val
Chengsong
parents:
diff changeset
    39
case class Left(v: Val) extends Val
Chengsong
parents:
diff changeset
    40
case class Right(v: Val) extends Val
Chengsong
parents:
diff changeset
    41
case class Stars(vs: List[Val]) extends Val
Chengsong
parents:
diff changeset
    42
case class Rec(x: String, v: Val) extends Val
Chengsong
parents:
diff changeset
    43
case class Ntime(vs: List[Val]) extends Val
Chengsong
parents:
diff changeset
    44
case class Optionall(v: Val) extends Val
Chengsong
parents:
diff changeset
    45
case class Nots(s: String) extends Val
Chengsong
parents:
diff changeset
    46
Chengsong
parents:
diff changeset
    47
Chengsong
parents:
diff changeset
    48
Chengsong
parents:
diff changeset
    49
abstract class Bit
Chengsong
parents:
diff changeset
    50
case object Z extends Bit
Chengsong
parents:
diff changeset
    51
case object S extends Bit
Chengsong
parents:
diff changeset
    52
Chengsong
parents:
diff changeset
    53
Chengsong
parents:
diff changeset
    54
type Bits = List[Bit]
Chengsong
parents:
diff changeset
    55
Chengsong
parents:
diff changeset
    56
abstract class ARexp 
Chengsong
parents:
diff changeset
    57
case object AZERO extends ARexp
Chengsong
parents:
diff changeset
    58
case class AONE(bs: Bits) extends ARexp
Chengsong
parents:
diff changeset
    59
case class ACHAR(bs: Bits, c: Char) extends ARexp
Chengsong
parents:
diff changeset
    60
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp 
Chengsong
parents:
diff changeset
    61
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp 
Chengsong
parents:
diff changeset
    62
case class ASTAR(bs: Bits, r: ARexp) extends ARexp 
Chengsong
parents:
diff changeset
    63
case class ANOT(bs: Bits, r: ARexp) extends ARexp
Chengsong
parents:
diff changeset
    64
case class AANYCHAR(bs: Bits) extends ARexp
Chengsong
parents:
diff changeset
    65
514
036600af4c30 chapter2
Chengsong
parents: 500
diff changeset
    66
import scala.util.Try
036600af4c30 chapter2
Chengsong
parents: 500
diff changeset
    67
640
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
    68
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    69
trait Generator[+T] {
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    70
  self => // an alias for "this"
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    71
    def generate(): T
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    72
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    73
    def gen(n: Int) : List[T] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    74
      if (n == 0) Nil else self.generate() :: gen(n - 1)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    75
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    76
    def map[S](f: T => S): Generator[S] = new Generator[S] {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    77
      def generate = f(self.generate())  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    78
    }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    79
    def flatMap[S](f: T => Generator[S]): Generator[S] = new Generator[S] {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    80
      def generate = f(self.generate()).generate()
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    81
    }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    82
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    83
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    84
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    85
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    86
// tests a property according to a given random generator
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    87
def test[T](r: Generator[T], amount: Int = 100)(pred: T => Boolean) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    88
  for (_ <- 0 until amount) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    89
    val value = r.generate()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    90
    assert(pred(value), s"Test failed for: $value")
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    91
  }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    92
  println(s"Test passed $amount times")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    93
}
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    94
def test2[T, S](r: Generator[T], s: Generator[S], amount: Int = 100)(pred: (T, S) => Boolean) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    95
  for (_ <- 0 until amount) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    96
    val valueR = r.generate()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    97
    val valueS = s.generate()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
    98
    assert(pred(valueR, valueS), s"Test failed for: $valueR, $valueS")
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
    99
  }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   100
  println(s"Test passed $amount times")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   101
}
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   102
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   103
// random integers
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   104
val integers = new Generator[Int] {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   105
  val rand = new java.util.Random
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   106
  def generate() = rand.nextInt()
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   107
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   108
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   109
// random booleans
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   110
val booleans = integers.map(_ > 0)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   111
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   112
// random integers in the range lo and high  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   113
def range(lo: Int, hi: Int): Generator[Int] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   114
  for (x <- integers) yield (lo + x.abs % (hi - lo)).abs
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   115
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   116
// random characters
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   117
def chars_range(lo: Char, hi: Char) = range(lo, hi).map(_.toChar)  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   118
val chars = chars_range('a', 'z')
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   119
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   120
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   121
def oneOf[T](xs: T*): Generator[T] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   122
  for (idx <- range(0, xs.length)) yield xs(idx)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   123
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   124
def single[T](x: T) = new Generator[T] {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   125
  def generate() = x
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   126
}   
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   127
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   128
def pairs[T, U](t: Generator[T], u: Generator[U]): Generator[(T, U)] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   129
  for (x <- t; y <- u) yield (x, y)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   130
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   131
// lists
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   132
def emptyLists = single(Nil) 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   133
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   134
def nonEmptyLists : Generator[List[Int]] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   135
  for (head <- integers; tail <- lists) yield head :: tail
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   136
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   137
def lists: Generator[List[Int]] = for {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   138
  kind <- booleans
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   139
  list <- if (kind) emptyLists else nonEmptyLists
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   140
} yield list
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   141
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   142
def char_list(len: Int): Generator[List[Char]] = {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   143
  if(len <= 0) single(Nil)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   144
  else{
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   145
    for { 
500
Chengsong
parents: 494
diff changeset
   146
      c <- chars_range('a', 'c')
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   147
      tail <- char_list(len - 1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   148
    } yield c :: tail
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   149
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   150
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   151
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   152
def strings(len: Int): Generator[String] = for(cs <- char_list(len)) yield cs.toString
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   153
493
Chengsong
parents: 492
diff changeset
   154
def sampleString(r: Rexp) : List[String] = r match {
Chengsong
parents: 492
diff changeset
   155
  case STAR(r) => stringsFromRexp(r).flatMap(s => List("", s, s ++ s))//only generate 0, 1, 2 reptitions
Chengsong
parents: 492
diff changeset
   156
  case SEQ(r1, r2) => stringsFromRexp(r1).flatMap(s1 => stringsFromRexp(r2).map(s2 => s1 ++ s2) )
Chengsong
parents: 492
diff changeset
   157
  case ALTS(r1, r2) => throw new Error(s" Rexp ${r} not expected: all alternatives are supposed to have been opened up")
Chengsong
parents: 492
diff changeset
   158
  case ONE => "" :: Nil
Chengsong
parents: 492
diff changeset
   159
  case ZERO => Nil
Chengsong
parents: 492
diff changeset
   160
  case CHAR(c) => c.toString :: Nil
Chengsong
parents: 492
diff changeset
   161
Chengsong
parents: 492
diff changeset
   162
}
Chengsong
parents: 492
diff changeset
   163
Chengsong
parents: 492
diff changeset
   164
def stringsFromRexp(r: Rexp) : List[String] = 
Chengsong
parents: 492
diff changeset
   165
  breakIntoTerms(r).flatMap(r => sampleString(r))
Chengsong
parents: 492
diff changeset
   166
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   167
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   168
// (simple) binary trees
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   169
trait Tree[T]
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   170
case class Inner[T](left: Tree[T], right: Tree[T]) extends Tree[T]
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   171
case class Leaf[T](x: T) extends Tree[T]
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   172
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   173
def leafs[T](t: Generator[T]): Generator[Leaf[T]] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   174
  for (x <- t) yield Leaf(x)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   175
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   176
def inners[T](t: Generator[T]): Generator[Inner[T]] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   177
  for (l <- trees(t); r <- trees(t)) yield Inner(l, r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   178
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   179
def trees[T](t: Generator[T]): Generator[Tree[T]] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   180
  for (kind <- range(0, 2);  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   181
       tree <- if (kind == 0) leafs(t) else inners(t)) yield tree
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   182
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   183
// regular expressions
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   184
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   185
// generates random leaf-regexes; prefers CHAR-regexes
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   186
def leaf_rexp() : Generator[Rexp] =
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   187
  for (kind <- range(0, 5);
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   188
       c <- chars_range('a', 'd')) yield
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   189
kind match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   190
  case 0 => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   191
  case 1 => ONE
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   192
  case _ => CHAR(c) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   193
}
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   194
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   195
// generates random inner regexes with maximum depth d
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   196
def inner_rexp(d: Int) : Generator[Rexp] =
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   197
  for (kind <- range(0, 3);
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   198
       l <- rexp(d); 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   199
       r <- rexp(d))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   200
yield kind match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   201
  case 0 => ALTS(l, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   202
  case 1 => SEQ(l, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   203
  case 2 => STAR(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   204
}
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   205
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   206
// generates random regexes with maximum depth d;
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   207
// prefers inner regexes in 2/3 of the cases
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   208
def rexp(d: Int = 100): Generator[Rexp] = 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   209
  for (kind <- range(0, 3);
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   210
       r <- if (d <= 0 || kind == 0) leaf_rexp() else inner_rexp(d - 1)) yield r
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   211
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   212
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   213
// some test functions for rexps
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   214
def height(r: Rexp) : Int = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   215
  case ZERO => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   216
  case ONE => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   217
  case CHAR(_) => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   218
  case ALTS(r1, r2) => 1 + List(height(r1), height(r2)).max
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   219
  case SEQ(r1, r2) =>  1 + List(height(r1), height(r2)).max
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   220
  case STAR(r) => 1 + height(r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   221
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   222
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   223
// def size(r: Rexp) : Int = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   224
//   case ZERO => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   225
//   case ONE => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   226
//   case CHAR(_) => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   227
//   case ALTS(r1, r2) => 1 + size(r1) + size(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   228
//   case SEQ(r1, r2) =>  1 + size(r1) + size(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   229
//   case STAR(r) => 1 + size(r) 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   230
// }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   231
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   232
// randomly subtracts 1 or 2 from the STAR case
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   233
def size_faulty(r: Rexp) : Int = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   234
  case ZERO => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   235
  case ONE => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   236
  case CHAR(_) => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   237
  case ALTS(r1, r2) => 1 + size_faulty(r1) + size_faulty(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   238
  case SEQ(r1, r2) =>  1 + size_faulty(r1) + size_faulty(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   239
  case STAR(r) => 1 + size_faulty(r) - range(0, 2).generate
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   240
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   241
431
Chengsong
parents:
diff changeset
   242
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   243
431
Chengsong
parents:
diff changeset
   244
// some convenience for typing in regular expressions
Chengsong
parents:
diff changeset
   245
Chengsong
parents:
diff changeset
   246
def charlist2rexp(s : List[Char]): Rexp = s match {
Chengsong
parents:
diff changeset
   247
  case Nil => ONE
Chengsong
parents:
diff changeset
   248
  case c::Nil => CHAR(c)
Chengsong
parents:
diff changeset
   249
  case c::s => SEQ(CHAR(c), charlist2rexp(s))
Chengsong
parents:
diff changeset
   250
}
Chengsong
parents:
diff changeset
   251
implicit def string2rexp(s : String) : Rexp = 
Chengsong
parents:
diff changeset
   252
  charlist2rexp(s.toList)
Chengsong
parents:
diff changeset
   253
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   254
  implicit def RexpOps(r: Rexp) = new {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   255
    def | (s: Rexp) = ALTS(r, s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   256
    def % = STAR(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   257
    def ~ (s: Rexp) = SEQ(r, s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   258
  }
431
Chengsong
parents:
diff changeset
   259
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   260
  implicit def stringOps(s: String) = new {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   261
    def | (r: Rexp) = ALTS(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   262
    def | (r: String) = ALTS(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   263
    def % = STAR(s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   264
    def ~ (r: Rexp) = SEQ(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   265
    def ~ (r: String) = SEQ(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   266
    def $ (r: Rexp) = RECD(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   267
  }
431
Chengsong
parents:
diff changeset
   268
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   269
  def nullable(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   270
    case ZERO => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   271
    case ONE => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   272
    case CHAR(_) => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   273
    case ANYCHAR => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   274
    case ALTS(r1, r2) => nullable(r1) || nullable(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   275
    case ALTSS(rs) => rs.exists(nullable)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   276
    case SEQ(r1, r2) => nullable(r1) && nullable(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   277
    case STAR(_) => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   278
    case RECD(_, r1) => nullable(r1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   279
    case NTIMES(n, r) => if (n == 0) true else nullable(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   280
    case OPTIONAL(r) => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   281
    case NOT(r) => !nullable(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   282
  }
431
Chengsong
parents:
diff changeset
   283
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   284
  def der(c: Char, r: Rexp) : Rexp = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   285
    case ZERO => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   286
    case ONE => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   287
    case CHAR(d) => if (c == d) ONE else ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   288
    case ANYCHAR => ONE 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   289
    case ALTS(r1, r2) => ALTS(der(c, r1), der(c, r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   290
    case ALTSS(rs) => ALTSS(rs.map(der(c, _)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   291
    case SEQ(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   292
      if (nullable(r1)) ALTS(SEQ(der(c, r1), r2), der(c, r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   293
      else SEQ(der(c, r1), r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   294
    case STAR(r) => SEQ(der(c, r), STAR(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   295
    case RECD(_, r1) => der(c, r1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   296
    case NTIMES(n, r) => if(n > 0) SEQ(der(c, r), NTIMES(n - 1, r)) else ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   297
    case OPTIONAL(r) => der(c, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   298
    case NOT(r) =>  NOT(der(c, r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   299
  }
431
Chengsong
parents:
diff changeset
   300
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   301
  def ders(s: List[Char], r: Rexp) : Rexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   302
    case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   303
    case c :: cs => ders(cs, der(c, r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   304
  }
539
Chengsong
parents: 536
diff changeset
   305
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   306
  def ders_simp(s: List[Char], r: Rexp) : Rexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   307
    case Nil => simp(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   308
    case c :: cs => ders_simp(cs, simp(der(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   309
  }
539
Chengsong
parents: 536
diff changeset
   310
Chengsong
parents: 536
diff changeset
   311
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   312
  def simp2(r: Rexp) : Rexp = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   313
    case SEQ(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   314
      (simp2(r1), simp2(r2)) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   315
        case (ZERO, _) => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   316
        case (_, ZERO) => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   317
        case (ONE, r2s) => r2s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   318
        case (r1s, ONE) => r1s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   319
        case (r1s, r2s) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   320
          SEQ(r1s, r2s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   321
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   322
        case ALTS(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   323
          val r1r2s = fltsplain(simp2(r1) :: simp2(r2) :: Nil).distinct 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   324
          r1r2s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   325
            case Nil => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   326
            case r :: Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   327
            case r1 :: r2 :: rs => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   328
              ALTSS(r1 :: r2 :: rs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   329
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   330
            case ALTSS(rs) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   331
              // println(rs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   332
              (fltsplain(rs.map(simp2))).distinct match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   333
                case Nil => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   334
                case r :: Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   335
                case r1 :: r2 :: rs =>
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   336
                  ALTSS(r1 :: r2 :: rs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   337
              }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   338
                case r => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   339
  }
539
Chengsong
parents: 536
diff changeset
   340
Chengsong
parents: 536
diff changeset
   341
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   342
  def simp(r: Rexp) : Rexp = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   343
    case SEQ(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   344
      (simp(r1), simp(r2)) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   345
        case (ZERO, _) => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   346
        case (_, ZERO) => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   347
        case (ONE, r2s) => r2s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   348
        case (r1s, ONE) => r1s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   349
        case (r1s, r2s) => SEQ(r1s, r2s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   350
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   351
        case ALTS(r1, r2) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   352
          (simp(r1), simp(r2)) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   353
            case (ZERO, r2s) => r2s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   354
            case (r1s, ZERO) => r1s
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   355
            case (r1s, r2s) =>
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   356
              if(r1s == r2s) r1s else ALTS(r1s, r2s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   357
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   358
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   359
            case r => r
539
Chengsong
parents: 536
diff changeset
   360
  }
Chengsong
parents: 536
diff changeset
   361
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   362
  def fltsplain(rs: List[Rexp]) : List[Rexp] = rs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   363
    case Nil => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   364
    case ZERO :: rs => fltsplain(rs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   365
    case ALTS(r1, r2) :: rs => r1 :: r2 :: fltsplain(rs) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   366
    case ALTSS(rs) :: rs1 => rs ::: fltsplain(rs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   367
    case r :: rs => r :: fltsplain(rs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   368
  }
539
Chengsong
parents: 536
diff changeset
   369
Chengsong
parents: 536
diff changeset
   370
Chengsong
parents: 536
diff changeset
   371
Chengsong
parents: 536
diff changeset
   372
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   373
  def matcher(s: String, r: Rexp) : Boolean = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   374
    nullable(ders(s.toList, r))
539
Chengsong
parents: 536
diff changeset
   375
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   376
  def simp_matcher(s: String, r: Rexp) : Boolean = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   377
    nullable(ders_simp(s.toList, r))
539
Chengsong
parents: 536
diff changeset
   378
431
Chengsong
parents:
diff changeset
   379
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   380
  // extracts a string from a value
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   381
  def flatten(v: Val) : String = v match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   382
    case Empty => ""
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   383
    case Chr(c) => c.toString
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   384
    case Left(v) => flatten(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   385
    case Right(v) => flatten(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   386
    case Sequ(v1, v2) => flatten(v1) ++ flatten(v2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   387
    case Stars(vs) => vs.map(flatten).mkString
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   388
    case Ntime(vs) => vs.map(flatten).mkString
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   389
    case Optionall(v) => flatten(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   390
    case Rec(_, v) => flatten(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   391
  }
431
Chengsong
parents:
diff changeset
   392
Chengsong
parents:
diff changeset
   393
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   394
  // extracts an environment from a value;
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   395
  // used for tokenising a string
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   396
  def env(v: Val) : List[(String, String)] = v match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   397
    case Empty => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   398
    case Chr(c) => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   399
    case Left(v) => env(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   400
    case Right(v) => env(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   401
    case Sequ(v1, v2) => env(v1) ::: env(v2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   402
    case Stars(vs) => vs.flatMap(env)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   403
    case Ntime(vs) => vs.flatMap(env)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   404
    case Rec(x, v) => (x, flatten(v))::env(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   405
    case Optionall(v) => env(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   406
    case Nots(s) => ("Negative", s) :: Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   407
  }
431
Chengsong
parents:
diff changeset
   408
Chengsong
parents:
diff changeset
   409
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   410
  // The injection and mkeps part of the lexer
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   411
  //===========================================
431
Chengsong
parents:
diff changeset
   412
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   413
  def mkeps(r: Rexp) : Val = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   414
    case ONE => Empty
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   415
    case ALTS(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   416
      if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   417
    case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   418
    case STAR(r) => Stars(Nil)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   419
    case RECD(x, r) => Rec(x, mkeps(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   420
    case NTIMES(n, r) => Ntime(List.fill(n)(mkeps(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   421
    case OPTIONAL(r) => Optionall(Empty)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   422
    case NOT(rInner) => if(nullable(rInner)) throw new Exception("error")  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   423
    else Nots("")//Nots(s.reverse.toString)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   424
    //   case NOT(ZERO) => Empty
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   425
    //   case NOT(CHAR(c)) => Empty
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   426
    //   case NOT(SEQ(r1, r2)) => Sequ(mkeps(NOT(r1)), mkeps(NOT(r2)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   427
    //   case NOT(ALTS(r1, r2)) => if(!nullable(r1)) Left(mkeps(NOT(r1))) else Right(mkeps(NOT(r2)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   428
    //   case NOT(STAR(r)) => Stars(Nil) 
431
Chengsong
parents:
diff changeset
   429
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   430
  }
431
Chengsong
parents:
diff changeset
   431
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   432
  def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   433
    case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   434
    case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   435
    case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   436
    case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   437
    case (ALTS(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   438
    case (ALTS(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   439
    case (CHAR(d), Empty) => Chr(c) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   440
    case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   441
    case (NTIMES(n, r), Sequ(v1, Ntime(vs))) => Ntime(inj(r, c, v1)::vs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   442
    case (OPTIONAL(r), v) => Optionall(inj(r, c, v))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   443
    case (NOT(r), Nots(s)) => Nots(c.toString ++ s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   444
    case (ANYCHAR, Empty) => Chr(c)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   445
  }
431
Chengsong
parents:
diff changeset
   446
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   447
  // some "rectification" functions for simplification
431
Chengsong
parents:
diff changeset
   448
Chengsong
parents:
diff changeset
   449
Chengsong
parents:
diff changeset
   450
Chengsong
parents:
diff changeset
   451
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   452
  // The Lexing Rules for the WHILE Language
431
Chengsong
parents:
diff changeset
   453
Chengsong
parents:
diff changeset
   454
  // bnullable function: tests whether the aregular 
Chengsong
parents:
diff changeset
   455
  // expression can recognise the empty string
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   456
  def bnullable (r: ARexp) : Boolean = r match {
431
Chengsong
parents:
diff changeset
   457
    case AZERO => false
Chengsong
parents:
diff changeset
   458
    case AONE(_) => true
Chengsong
parents:
diff changeset
   459
    case ACHAR(_,_) => false
Chengsong
parents:
diff changeset
   460
    case AALTS(_, rs) => rs.exists(bnullable)
Chengsong
parents:
diff changeset
   461
    case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2)
Chengsong
parents:
diff changeset
   462
    case ASTAR(_, _) => true
Chengsong
parents:
diff changeset
   463
    case ANOT(_, rn) => !bnullable(rn)
Chengsong
parents:
diff changeset
   464
  }
Chengsong
parents:
diff changeset
   465
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   466
  def mkepsBC(r: ARexp) : Bits = r match {
431
Chengsong
parents:
diff changeset
   467
    case AONE(bs) => bs
Chengsong
parents:
diff changeset
   468
    case AALTS(bs, rs) => {
Chengsong
parents:
diff changeset
   469
      val n = rs.indexWhere(bnullable)
Chengsong
parents:
diff changeset
   470
      bs ++ mkepsBC(rs(n))
Chengsong
parents:
diff changeset
   471
    }
Chengsong
parents:
diff changeset
   472
    case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)
Chengsong
parents:
diff changeset
   473
    case ASTAR(bs, r) => bs ++ List(Z)
Chengsong
parents:
diff changeset
   474
    case ANOT(bs, rn) => bs
Chengsong
parents:
diff changeset
   475
  }
Chengsong
parents:
diff changeset
   476
Chengsong
parents:
diff changeset
   477
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   478
  def bder(c: Char, r: ARexp) : ARexp = r match {
431
Chengsong
parents:
diff changeset
   479
    case AZERO => AZERO
Chengsong
parents:
diff changeset
   480
    case AONE(_) => AZERO
Chengsong
parents:
diff changeset
   481
    case ACHAR(bs, f) => if (c == f) AONE(bs) else AZERO
Chengsong
parents:
diff changeset
   482
    case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _)))
Chengsong
parents:
diff changeset
   483
    case ASEQ(bs, r1, r2) => 
Chengsong
parents:
diff changeset
   484
      if (bnullable(r1)) AALTS(bs, ASEQ(Nil, bder(c, r1), r2) :: fuse(mkepsBC(r1), bder(c, r2)) :: Nil )
Chengsong
parents:
diff changeset
   485
      else ASEQ(bs, bder(c, r1), r2)
Chengsong
parents:
diff changeset
   486
    case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r))
Chengsong
parents:
diff changeset
   487
    case ANOT(bs, rn) => ANOT(bs, bder(c, rn))
Chengsong
parents:
diff changeset
   488
    case AANYCHAR(bs) => AONE(bs)
Chengsong
parents:
diff changeset
   489
  } 
Chengsong
parents:
diff changeset
   490
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   491
  def fuse(bs: Bits, r: ARexp) : ARexp = r match {
431
Chengsong
parents:
diff changeset
   492
    case AZERO => AZERO
Chengsong
parents:
diff changeset
   493
    case AONE(cs) => AONE(bs ++ cs)
Chengsong
parents:
diff changeset
   494
    case ACHAR(cs, f) => ACHAR(bs ++ cs, f)
Chengsong
parents:
diff changeset
   495
    case AALTS(cs, rs) => AALTS(bs ++ cs, rs)
Chengsong
parents:
diff changeset
   496
    case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)
Chengsong
parents:
diff changeset
   497
    case ASTAR(cs, r) => ASTAR(bs ++ cs, r)
Chengsong
parents:
diff changeset
   498
    case ANOT(cs, r) => ANOT(bs ++ cs, r)
Chengsong
parents:
diff changeset
   499
  }
Chengsong
parents:
diff changeset
   500
Chengsong
parents:
diff changeset
   501
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   502
  def internalise(r: Rexp) : ARexp = r match {
431
Chengsong
parents:
diff changeset
   503
    case ZERO => AZERO
Chengsong
parents:
diff changeset
   504
    case ONE => AONE(Nil)
Chengsong
parents:
diff changeset
   505
    case CHAR(c) => ACHAR(Nil, c)
Chengsong
parents:
diff changeset
   506
    //case PRED(f) => APRED(Nil, f)
Chengsong
parents:
diff changeset
   507
    case ALTS(r1, r2) => 
Chengsong
parents:
diff changeset
   508
      AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   509
      // case ALTS(r1::rs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   510
      //   val AALTS(Nil, rs2) = internalise(ALTS(rs))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   511
      //   AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   512
      // }
431
Chengsong
parents:
diff changeset
   513
    case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2))
Chengsong
parents:
diff changeset
   514
    case STAR(r) => ASTAR(Nil, internalise(r))
Chengsong
parents:
diff changeset
   515
    case RECD(x, r) => internalise(r)
Chengsong
parents:
diff changeset
   516
    case NOT(r) => ANOT(Nil, internalise(r))
Chengsong
parents:
diff changeset
   517
    case ANYCHAR => AANYCHAR(Nil)
Chengsong
parents:
diff changeset
   518
  }
Chengsong
parents:
diff changeset
   519
Chengsong
parents:
diff changeset
   520
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   521
  def bsimp(r: ARexp): ARexp = 
431
Chengsong
parents:
diff changeset
   522
  {
Chengsong
parents:
diff changeset
   523
    r match {
Chengsong
parents:
diff changeset
   524
      case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   525
        case (AZERO, _) => AZERO
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   526
        case (_, AZERO) => AZERO
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   527
        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   528
        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   529
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   530
        case AALTS(bs1, rs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   531
          val rs_simp = rs.map(bsimp(_))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   532
          val flat_res = flats(rs_simp)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   533
          val dist_res = distinctBy(flat_res, erase)//strongDB(flat_res)//distinctBy(flat_res, erase)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   534
          dist_res match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   535
            case Nil => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   536
            case s :: Nil => fuse(bs1, s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   537
            case rs => AALTS(bs1, rs)  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   538
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   539
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   540
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   541
            case r => r
431
Chengsong
parents:
diff changeset
   542
    }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   543
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   544
  def strongBsimp(r: ARexp): ARexp =
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   545
  {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   546
    r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   547
      case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(r2)) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   548
        case (AZERO, _) => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   549
        case (_, AZERO) => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   550
        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   551
        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   552
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   553
        case AALTS(bs1, rs) => {
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   554
          val rs_simp = rs.map(strongBsimp(_))
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   555
          val flat_res = flats(rs_simp)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   556
          val dist_res = distinctBy4(flat_res)//distinctBy(flat_res, erase)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   557
          dist_res match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   558
            case Nil => AZERO
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   559
            case s :: Nil => fuse(bs1, s)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   560
            case rs => AALTS(bs1, rs)  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   561
          }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   562
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   563
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   564
            case r => r
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   565
    }
431
Chengsong
parents:
diff changeset
   566
  }
Chengsong
parents:
diff changeset
   567
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   568
  def strongBsimp5(r: ARexp): ARexp =
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   569
  {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   570
    // println("was this called?")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   571
    r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   572
      case ASEQ(bs1, r1, r2) => (strongBsimp5(r1), strongBsimp5(r2)) match {
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   573
        case (AZERO, _) => AZERO
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   574
        case (_, AZERO) => AZERO
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   575
        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   576
        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   577
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   578
        case AALTS(bs1, rs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   579
          // println("alts case")
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   580
          val rs_simp = rs.map(strongBsimp5(_))
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   581
          val flat_res = flats(rs_simp)
500
Chengsong
parents: 494
diff changeset
   582
          var dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   583
          // var dist2_res = distinctBy5(dist_res)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   584
          // while(dist_res != dist2_res){
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   585
          //   dist_res = dist2_res
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   586
          //   dist2_res = distinctBy5(dist_res)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   587
          // }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   588
          (dist_res) match {
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   589
            case Nil => AZERO
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   590
            case s :: Nil => fuse(bs1, s)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   591
            case rs => AALTS(bs1, rs)  
500
Chengsong
parents: 494
diff changeset
   592
          }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   593
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   594
            case r => r
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   595
    }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   596
  }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   597
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   598
  def strongBsimp6(r: ARexp): ARexp =
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   599
  {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   600
    // println("was this called?")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   601
    r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   602
      case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match {
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   603
        case (AZERO, _) => AZERO
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   604
        case (_, AZERO) => AZERO
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   605
        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
530
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
   606
        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //asserted bs2 == Nil
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   607
        //case (r1s, r2s) if(isOne(erase(r1s))) => fuse(bs1 ++ mkepsBC(r1s), r2s)
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   608
        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   609
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   610
        case AALTS(bs1, rs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   611
          // println("alts case")
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   612
          val rs_simp = rs.map(strongBsimp6(_))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   613
          val flat_res = flats(rs_simp)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   614
          var dist_res = distinctBy6(flat_res)//distinctBy(flat_res, erase)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   615
          (dist_res) match {
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   616
            case Nil => AZERO
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   617
            case s :: Nil => fuse(bs1, s)
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   618
            case rs => AALTS(bs1, rs)  
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   619
          }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   620
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   621
        //(erase(r0))) => AONE(bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   622
            case r => r
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   623
    }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   624
  }
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   625
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   626
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   627
    def atMostEmpty(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   628
      case ZERO => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   629
      case ONE => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   630
      case STAR(r) => atMostEmpty(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   631
      case SEQ(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   632
      case ALTS(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   633
      case CHAR(_) => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   634
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   635
533
Chengsong
parents: 532
diff changeset
   636
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   637
    def isOne(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   638
      case ONE => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   639
      case SEQ(r1, r2) => isOne(r1) && isOne(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   640
      case ALTS(r1, r2) => (isOne(r1) || isOne(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   641
      case STAR(r0) => atMostEmpty(r0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   642
      case CHAR(c) => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   643
      case ZERO => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   644
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   645
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   646
  def distinctWith(rs: List[ARexp], 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   647
    pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   648
    acc: Set[Rexp] = Set()) : List[ARexp] = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   649
      rs match{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   650
        case Nil => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   651
        case r :: rs => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   652
          if(acc(erase(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   653
            distinctWith(rs, pruneFunction, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   654
          else {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   655
            val pruned_r = pruneFunction(r, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   656
            pruned_r :: 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   657
            distinctWith(rs, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   658
              pruneFunction, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   659
              turnIntoTerms(erase(pruned_r)) ++: acc
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   660
              )
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   661
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   662
      }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   663
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   664
    //r = r' ~ tail' : If tail' matches tail => returns r'
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   665
    def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = 
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   666
      if (r == tail)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   667
        ONE
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   668
      else {
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   669
        r match {
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   670
          case SEQ(r1, r2) => 
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   671
            if(r2 == tail) 
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   672
              r1
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   673
            else
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   674
              ZERO
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   675
          case r => ZERO
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   676
        }
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   677
      }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   678
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   679
    def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   680
      case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != AZERO) match
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   681
      {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   682
        //all components have been removed, meaning this is effectively a duplicate
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   683
        //flats will take care of removing this AZERO 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   684
        case Nil => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   685
        case r::Nil => fuse(bs, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   686
        case rs1 => AALTS(bs, rs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   687
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   688
      case ASEQ(bs, r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   689
        //remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   690
        prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   691
          //after pruning, returns 0
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   692
          case AZERO => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   693
          //after pruning, got r1'.r2, where r1' is equal to 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   694
          case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   695
          //assemble the pruned head r1p with r2
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   696
          case r1p => ASEQ(bs, r1p, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   697
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   698
        //this does the duplicate component removal task
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   699
      case r => if(acc(erase(r))) AZERO else r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   700
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   701
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   702
    //a stronger version of simp
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   703
    def bsimpStrong(r: ARexp): ARexp =
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   704
    {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   705
      r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   706
        case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   707
          //normal clauses same as simp
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   708
        case (AZERO, _) => AZERO
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   709
        case (_, AZERO) => AZERO
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   710
        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   711
        //bs2 can be discarded
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   712
        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   713
        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   714
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   715
        case AALTS(bs1, rs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   716
          //distinctBy(flat_res, erase)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   717
          distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   718
            case Nil => AZERO
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   719
            case s :: Nil => fuse(bs1, s)
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   720
            case rs => AALTS(bs1, rs)  
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   721
          }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   722
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   723
        //stars that can be treated as 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   724
        case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   725
        case r => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   726
      }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
   727
    }
431
Chengsong
parents:
diff changeset
   728
Chengsong
parents:
diff changeset
   729
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   730
    def bders (s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   731
      case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   732
      case c::s => bders(s, bder(c, r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   733
    }
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   734
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   735
    def flats(rs: List[ARexp]): List[ARexp] = rs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   736
      case Nil => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   737
      case AZERO :: rs1 => flats(rs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   738
      case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   739
      case r1 :: rs2 => r1 :: flats(rs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   740
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   741
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   742
    def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   743
      case Nil => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   744
      case (x::xs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   745
        val res = f(x)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   746
        if (acc.contains(res)) distinctBy(xs, f, acc)  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   747
        else x::distinctBy(xs, f, res::acc)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   748
      }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   749
    } 
431
Chengsong
parents:
diff changeset
   750
Chengsong
parents:
diff changeset
   751
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   752
    def pruneRexp(r: ARexp, allowableTerms: List[Rexp]) : ARexp = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   753
      r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   754
        case ASEQ(bs, r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   755
          val termsTruncated = allowableTerms.collect(rt => rt match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   756
            case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2)) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   757
          })
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   758
          val pruned : ARexp = pruneRexp(r1, termsTruncated)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   759
          pruned match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   760
            case AZERO => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   761
            case AONE(bs1) => fuse(bs ++ bs1, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   762
            case pruned1 => ASEQ(bs, pruned1, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   763
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   764
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   765
            case AALTS(bs, rs) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   766
              //allowableTerms.foreach(a => println(shortRexpOutput(a)))        
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   767
              val rsp = rs.map(r => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   768
                  pruneRexp(r, allowableTerms)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   769
                  )
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   770
                    .filter(r => r != AZERO)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   771
                    rsp match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   772
                      case Nil => AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   773
                      case r1::Nil => fuse(bs, r1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   774
                      case rs1 => AALTS(bs, rs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   775
                    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   776
                      case r => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   777
                        if(allowableTerms.contains(erase(r))) r else AZERO //assert(r != AZERO)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   778
      }
431
Chengsong
parents:
diff changeset
   779
    }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   780
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   781
    def oneSimp(r: Rexp) : Rexp = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   782
      case SEQ(ONE, r) => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   783
      case SEQ(r1, r2) => SEQ(oneSimp(r1), r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   784
      case r => r//assert r != 0 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   785
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   786
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   787
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
   788
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   789
    def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   790
      case Nil => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   791
      case x :: xs =>
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   792
        //assert(acc.distinct == acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   793
        val erased = erase(x)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   794
        if(acc.contains(erased))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   795
          distinctBy4(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   796
        else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   797
          val addToAcc =  breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   798
          //val xp = pruneRexp(x, addToAcc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   799
          pruneRexp(x, addToAcc) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   800
            case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   801
            case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   802
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   803
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   804
    }
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   805
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   806
    // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   807
    //   where
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   808
    // "pAKC_aux rsa r ctx = (if (seqFold (SEQ (erase r) ( ctx) )) ⊆ (seqFold (erase (AALTs [] rsa))) then AZERO else
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   809
    //                           case r of (ASEQ bs r1 r2) ⇒ 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   810
    //                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   811
    //                                     (AALTs bs rs) ⇒ 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   812
    //                             bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) )    |
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   813
    //                                     r             ⇒ r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   814
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   815
    // def canonicalSeq(rs: List[Rexp], acc: Rexp) = rs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   816
    //   case r::Nil => SEQ(r, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   817
    //   case Nil => acc
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   818
    //   case r1::r2::Nil => SEQ(SEQ(r1, r2), acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   819
    // }
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   820
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   821
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   822
    //the "fake" Language interpretation: just concatenates!
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   823
    def seqFold(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   824
      case Nil => acc
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   825
      case r :: rs1 => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   826
        // if(acc == ONE) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   827
        //   seqFold(r, rs1) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   828
        // else
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   829
        seqFold(SEQ(acc, r), rs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   830
    }
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   831
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   832
    def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   833
    def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
500
Chengsong
parents: 494
diff changeset
   834
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   835
    def aprint(a: ARexp) = println(shortRexpOutput(erase(a)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   836
    def asprint(as: List[ARexp]) = as.foreach(a => println(shortRexpOutput(erase(a))))
500
Chengsong
parents: 494
diff changeset
   837
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   838
    def pAKC(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   839
      // println("pakc")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   840
      // println(shortRexpOutput(erase(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   841
      // println("acc")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   842
      // rsprint(acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   843
      // println("ctx---------")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   844
      // rsprint(ctx)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   845
      // println("ctx---------end")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   846
      // rsprint(breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   847
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   848
      if (breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   849
        AZERO
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   850
      }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   851
      else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   852
        r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   853
          case ASEQ(bs, r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   854
            (pAKC(acc, r1, erase(r2) :: ctx)) match{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   855
              case AZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   856
                AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   857
              case AONE(bs1) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   858
                fuse(bs1, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   859
              case r1p => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   860
                ASEQ(bs, r1p, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   861
            }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   862
              case AALTS(bs, rs0) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   863
                // println("before pruning")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   864
                // println(s"ctx is ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   865
                // ctx.foreach(r => println(shortRexpOutput(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   866
                // println(s"rs0 is ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   867
                // rs0.foreach(r => println(shortRexpOutput(erase(r))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   868
                // println(s"acc is ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   869
                // acc.foreach(r => println(shortRexpOutput(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   870
                rs0.map(r => pAKC(acc, r, ctx)).filter(_ != AZERO) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   871
                  case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   872
                    // println("after pruning Nil")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   873
                    AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   874
                  case r :: Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   875
                    // println("after pruning singleton")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   876
                    // println(shortRexpOutput(erase(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   877
                    r 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   878
                  case rs0p => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   879
                    // println("after pruning non-singleton")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   880
                    AALTS(bs, rs0p)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   881
                }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   882
                  case r => r
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   883
        }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   884
      }
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   885
    }
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   886
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   887
    def distinctBy5(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   888
      case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   889
        Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   890
      case x :: xs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   891
        val erased = erase(x)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   892
        if(acc.contains(erased)){
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   893
          distinctBy5(xs, acc)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   894
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   895
        else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   896
          val pruned = pAKC(acc, x, Nil)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   897
          val newTerms = breakIntoTerms(erase(pruned))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   898
          pruned match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   899
            case AZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   900
              distinctBy5(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   901
            case xPrime => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   902
              xPrime :: distinctBy5(xs, newTerms.map(oneSimp) ::: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   903
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   904
        }
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   905
      }
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
   906
    }
431
Chengsong
parents:
diff changeset
   907
Chengsong
parents:
diff changeset
   908
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   909
    def isOne1(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   910
      case ONE => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   911
      case SEQ(r1, r2) => false//isOne1(r1) && isOne1(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   912
      case ALTS(r1, r2) => false//(isOne1(r1) || isOne1(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   913
      case STAR(r0) => false//atMostEmpty(r0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   914
      case CHAR(c) => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   915
      case ZERO => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   916
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   917
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   918
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   919
    def turnIntoTerms(r: Rexp): List[Rexp] = r match {
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   920
      case SEQ(r1, r2)  => 
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   921
        turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   922
          case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   923
          case ZERO => Nil
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
   924
          case _ => r :: Nil
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   925
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   926
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   927
    def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   928
      if(r11 == ONE)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   929
        turnIntoTerms(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   930
      else
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   931
        SEQ(r11, r2) :: Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   932
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   933
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   934
    def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   935
      turnIntoTerms((seqFold(erase(r), ctx)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   936
        .toSet
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   937
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   938
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   939
    def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   940
      turnIntoTerms(seqFold(r, ctx)).toSet
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   941
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   942
    def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   943
      subseteqPred: (C, C) => Boolean) : Boolean = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   944
        subseteqPred(f(a, b), c)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   945
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   946
      def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   947
        //rs1 \subseteq rs2
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   948
      rs1.forall(rs2.contains)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   949
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   950
      def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   951
        if (ABIncludedByC(a = r, b = ctx, c = acc, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   952
          f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   953
          {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   954
            AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   955
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   956
          else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   957
            r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   958
              case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   959
                case AZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   960
                  AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   961
                case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   962
                  prune6(acc, fuse(bs1, r2), ctx)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   963
                case r1p => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   964
                  ASEQ(bs, r1p, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   965
              }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   966
                case AALTS(bs, rs0) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   967
                  rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   968
                    case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   969
                      AZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   970
                    case r :: Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   971
                      fuse(bs, r) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   972
                    case rs0p => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   973
                      AALTS(bs, rs0p)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   974
                  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   975
                    case r => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   976
            }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   977
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   978
      }
431
Chengsong
parents:
diff changeset
   979
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   980
      def prune6cc(acc: Set[Rexp], r: Rexp, ctx: List[Rexp]) : Rexp = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   981
        if (ABIncludedByC(a = r, b = ctx, c = acc, 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   982
          f = attachCtxcc, subseteqPred = rs1_subseteq_rs2)) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   983
          {//acc.flatMap(breakIntoTerms
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   984
            ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   985
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   986
          else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   987
            r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   988
              case SEQ(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   989
                (prune6cc(acc, r1, r2 :: ctx)) match{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   990
                  case ZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   991
                    ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   992
                  case ONE => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   993
                    r2
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   994
                  case r1p => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   995
                    SEQ(r1p, r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   996
                }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   997
                  case ALTS(r1, r2) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   998
                    List(r1, r2).map(r => prune6cc(acc, r, ctx)).filter(_ != AZERO) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
   999
                      case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1000
                        ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1001
                      case r :: Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1002
                        r 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1003
                      case ra :: rb :: Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1004
                        ALTS(ra, rb)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1005
                    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1006
                      case r => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1007
            }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1008
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1009
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1010
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1011
      def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1012
      List[ARexp] = xs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1013
        case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1014
          Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1015
        case x :: xs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1016
          val erased = erase(x)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1017
          if(acc.contains(erased)){
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1018
            distinctBy6(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1019
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1020
          else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1021
            val pruned = prune6(acc, x)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1022
            val newTerms = turnIntoTerms(erase(pruned))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1023
            pruned match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1024
              case AZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1025
                distinctBy6(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1026
              case xPrime => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1027
                xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1028
            }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1029
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1030
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1031
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1032
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1033
      def distinctByacc(xs: List[Rexp], acc: Set[Rexp] = Set()) : Set[Rexp] = xs match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1034
        case Nil => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1035
          acc
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1036
        case x :: xs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1037
          if(acc.contains(x)){
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1038
            distinctByacc(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1039
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1040
          else{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1041
            val pruned = prune6cc(acc, x, Nil)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1042
            val newTerms = turnIntoTerms(pruned)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1043
            pruned match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1044
              case ZERO => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1045
                distinctByacc(xs, acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1046
              case xPrime => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1047
                distinctByacc(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1048
            }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1049
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1050
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1051
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1052
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1053
      def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1054
        case SEQ(r1, r2)  => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1055
        case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1056
        case ZERO => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1057
        case _ => r::Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1058
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1059
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1060
      def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1061
        //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1062
        case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1063
        case ZERO => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1064
        case _ => r::Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1065
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1066
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1067
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1068
      def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1069
        case (ONE, bs) => (Empty, bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1070
        case (CHAR(f), bs) => (Chr(f), bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1071
        case (ALTS(r1, r2), Z::bs1) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1072
          val (v, bs2) = decode_aux(r1, bs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1073
          (Left(v), bs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1074
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1075
        case (ALTS(r1, r2), S::bs1) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1076
          val (v, bs2) = decode_aux(r2, bs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1077
          (Right(v), bs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1078
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1079
        case (SEQ(r1, r2), bs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1080
          val (v1, bs1) = decode_aux(r1, bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1081
          val (v2, bs2) = decode_aux(r2, bs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1082
          (Sequ(v1, v2), bs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1083
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1084
        case (STAR(r1), S::bs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1085
          val (v, bs1) = decode_aux(r1, bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1086
          //(v)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1087
          val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1088
          (Stars(v::vs), bs2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1089
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1090
        case (STAR(_), Z::bs) => (Stars(Nil), bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1091
        case (RECD(x, r1), bs) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1092
          val (v, bs1) = decode_aux(r1, bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1093
          (Rec(x, v), bs1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1094
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1095
        case (NOT(r), bs) => (Nots(r.toString), bs)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1096
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1097
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1098
      def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1099
        case (v, Nil) => v
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1100
        case _ => throw new Exception("Not decodable")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1101
      }
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1102
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1103
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1104
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1105
      def blexing_simp(r: Rexp, s: String) : Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1106
        val bit_code = blex_simp(internalise(r), s.toList)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1107
        decode(r, bit_code)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1108
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1109
      def simpBlexer(r: Rexp, s: String) : Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1110
        Try(blexing_simp(r, s)).getOrElse(Failure)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1111
      }
431
Chengsong
parents:
diff changeset
  1112
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1113
      def strong_blexing_simp(r: Rexp, s: String) : Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1114
        decode(r, strong_blex_simp(internalise(r), s.toList))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1115
      }
431
Chengsong
parents:
diff changeset
  1116
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1117
      def strong_blexing_simp5(r: Rexp, s: String) : Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1118
        decode(r, strong_blex_simp5(internalise(r), s.toList))
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1119
      }
431
Chengsong
parents:
diff changeset
  1120
Chengsong
parents:
diff changeset
  1121
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1122
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1123
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1124
      //def blexerStrong(r: ARexp, s: String) : Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1125
      //  Try(strong_blexing_simp(r, s)).getOrElse(Failure)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1126
      //}
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1127
      def strongBlexer5(r: Rexp, s: String): Val = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1128
        Try(strong_blexing_simp5(r, s)).getOrElse(Failure)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1129
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1130
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1131
      def strongBlexer(r: Rexp, s: String) : Option[Val] = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1132
        Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1133
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1134
      def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1135
        case Nil => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1136
          if (bnullable(r)) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1137
            mkepsBC(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1138
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1139
          else 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1140
            throw new Exception("Not matched")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1141
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1142
        case c::cs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1143
          strong_blex_simp(strongBsimp(bder(c, r)), cs)      
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1144
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1145
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1146
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1147
      def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1148
        case Nil => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1149
          if (bnullable(r)) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1150
            val bits = mkepsBC(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1151
            bits
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1152
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1153
          else 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1154
            throw new Exception("Not matched")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1155
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1156
        case c::cs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1157
          val der_res = bder(c,r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1158
          val simp_res = strongBsimp5(der_res)  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1159
          strong_blex_simp5(simp_res, cs)      
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1160
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1161
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1162
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1163
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1164
      def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1165
        case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1166
        case c::s => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1167
          //println(erase(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1168
          bders_simp(s, bsimp(bder(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1169
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1170
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1171
      def bdersStrong5(s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1172
        case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1173
        case c::s => bdersStrong5(s, strongBsimp5(bder(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1174
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1175
      def bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1176
        case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1177
        case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1178
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1179
      //Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1180
      def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1181
        case Nil => r
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1182
        case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1183
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1184
      def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1185
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1186
      //def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1187
      //  case Nil => r 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1188
      //  case c::s => bdersStrong(s, strongBsimp(bder(c, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1189
      //}
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1190
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1191
      def bdersStrongRexp(s: String, r: Rexp) : ARexp = bdersStrong(s.toList, internalise(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1192
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1193
      def erase(r:ARexp): Rexp = r match{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1194
        case AZERO => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1195
        case AONE(_) => ONE
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1196
        case ACHAR(bs, c) => CHAR(c)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1197
        case AALTS(bs, Nil) => ZERO
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1198
        case AALTS(bs, a::Nil) => erase(a)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1199
        case AALTS(bs, a::as) => ALTS(erase(a), erase(AALTS(bs, as)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1200
        case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1201
        case ASTAR(cs, r)=> STAR(erase(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1202
        case ANOT(bs, r) => NOT(erase(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1203
        case AANYCHAR(bs) => ANYCHAR
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1204
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1205
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1206
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1207
      def allCharSeq(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1208
        case CHAR(c) => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1209
        case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1210
        case _ => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1211
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1212
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1213
      def flattenSeq(r: Rexp) : String = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1214
        case CHAR(c) => c.toString
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1215
        case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1216
        case _ => throw new Error("flatten unflattenable rexp")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1217
      } 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1218
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1219
      def shortRexpOutput(r: Rexp) : String = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1220
        case CHAR(c) => c.toString
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1221
        case ONE => "1"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1222
        case ZERO => "0"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1223
        case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1224
        case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1225
        case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1226
        case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1227
        case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1228
        //case RTOP => "RTOP"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1229
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1230
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1231
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1232
      def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1233
        case Nil => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1234
          if (bnullable(r)) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1235
            val bits = mkepsBC(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1236
            bits
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1237
          }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1238
          else 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1239
            throw new Exception("Not matched")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1240
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1241
        case c::cs => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1242
          val der_res = bder(c,r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1243
          val simp_res = bsimp(der_res)  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1244
          blex_simp(simp_res, cs)      
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1245
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1246
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1247
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1248
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1249
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1250
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1251
      def size(r: Rexp) : Int = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1252
        case ZERO => 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1253
        case ONE => 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1254
        case CHAR(_) => 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1255
        case ANYCHAR => 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1256
        case NOT(r0) => 1 + size(r0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1257
        case SEQ(r1, r2) => 1 + size(r1) + size(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1258
        case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1259
        case STAR(r) => 1 + size(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1260
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1261
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1262
      def asize(a: ARexp) = size(erase(a))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1263
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1264
      //pder related
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1265
      type Mon = (Char, Rexp)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1266
      type Lin = Set[Mon]
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1267
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1268
      def dot_prod(rs: Set[Rexp], r: Rexp): Set[Rexp] = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1269
        case ZERO => Set()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1270
        case ONE => rs
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1271
        case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1272
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1273
      def cir_prod(l: Lin, t: Rexp): Lin = t match {//remember this Lin is different from the Lin in Antimirov's paper. Here it does not mean the set of all subsets of linear forms that does not contain zero, but rather the type a set of linear forms
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1274
        case ZERO => Set()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1275
        // case ONE => l
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1276
        case t => l.map( m => m._2 match 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1277
        {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1278
          case ZERO => m 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1279
          case ONE => (m._1, t) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1280
          case p => (m._1, SEQ(p, t)) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1281
        }  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1282
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1283
        )
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1284
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1285
      def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1286
        case ZERO => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1287
        case ONE => l
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1288
        case t => l.map(m => m._2 match
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1289
        {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1290
          case ZERO => m
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1291
          case ONE => (m._1, t)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1292
          case p => (m._1, SEQ(p, t))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1293
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1294
        )
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1295
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1296
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1297
      def lfList(r: Rexp) : List[Mon] = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1298
        case ZERO => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1299
        case ONE => Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1300
        case CHAR(f) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1301
          (f, ONE) :: Nil
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1302
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1303
        case ALTS(r1, r2) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1304
          lfList(r1) ++ lfList(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1305
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1306
        case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1307
        case SEQ(r1, r2) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1308
          if(nullable(r1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1309
            cir_prodList(lfList(r1), r2) ++ lfList(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1310
          else
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1311
            cir_prodList(lfList(r1), r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1312
        }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1313
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1314
      def lfprint(ls: Lin) = ls.foreach(m =>{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1315
        println(m._1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1316
        rprint(m._2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1317
      })
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1318
    def lf(r: Rexp): Lin = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1319
      case ZERO => Set()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1320
      case ONE => Set()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1321
      case CHAR(f) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1322
        //val Some(c) = alphabet.find(f) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1323
        Set((f, ONE))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1324
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1325
      case ALTS(r1, r2) => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1326
        lf(r1 ) ++ lf(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1327
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1328
      case STAR(r1) => cir_prod(lf(r1), STAR(r1)) //may try infix notation later......
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1329
      case SEQ(r1, r2) =>{
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1330
        if (nullable(r1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1331
          cir_prod(lf(r1), r2) ++ lf(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1332
        else
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1333
          cir_prod(lf(r1), r2) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1334
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1335
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1336
    def lfs(r: Set[Rexp]): Lin = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1337
      r.foldLeft(Set[Mon]())((acc, r) => acc ++ lf(r))
431
Chengsong
parents:
diff changeset
  1338
    }
Chengsong
parents:
diff changeset
  1339
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1340
    def pder(x: Char, t: Rexp): Set[Rexp] = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1341
      val lft = lf(t)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1342
      (lft.filter(mon => if(mon._1 == x) true else false)).map(mon => mon._2)
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1343
    }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1344
    def pders_single(s: List[Char], t: Rexp) : Set[Rexp] = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1345
      case x::xs => pders(xs, pder(x, t))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1346
      case Nil => Set(t)
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1347
    }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1348
    def pders(s: List[Char], ts: Set[Rexp]) : Set[Rexp] = s match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1349
      case x::xs => pders(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1350
      case Nil => ts 
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1351
    }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1352
    def pderss(ss: List[List[Char]], t: Rexp): Set[Rexp] = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1353
      ss.foldLeft( Set[Rexp]() )( (acc, s) => pders_single(s, t) ++ acc )
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1354
    def pdera(t: Rexp): Set[Rexp] = lf(t).map(mon => mon._2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1355
    //all implementation of partial derivatives that involve set union are potentially buggy
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1356
    //because they don't include the original regular term before they are pdered.
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1357
    //now only pderas is fixed.
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1358
    def pderas(t: Set[Rexp], d: Int): Set[Rexp] = 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1359
      if(d > 0) 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1360
        pderas(lfs(t).map(mon => mon._2), d - 1) ++ t 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1361
      else 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1362
        lfs(t).map(mon => mon._2) ++ t//repeated application of pderas over the newest set of pders.
431
Chengsong
parents:
diff changeset
  1363
  def pderUNIV(r: Rexp) : Set[Rexp] = pderas(Set(r), awidth(r) + 1)
Chengsong
parents:
diff changeset
  1364
  def awidth(r: Rexp) : Int = r match {
Chengsong
parents:
diff changeset
  1365
    case CHAR(c) => 1
Chengsong
parents:
diff changeset
  1366
    case SEQ(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents:
diff changeset
  1367
    case ALTS(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents:
diff changeset
  1368
    case ONE => 0
Chengsong
parents:
diff changeset
  1369
    case ZERO => 0
Chengsong
parents:
diff changeset
  1370
    case STAR(r) => awidth(r)
Chengsong
parents:
diff changeset
  1371
  }
Chengsong
parents:
diff changeset
  1372
  //def sigma_lf(l: Set[Mon]) : Rexp = ALTS(l.map(mon => SEQ(CHAR(mon._1),mon._2)).toList)
Chengsong
parents:
diff changeset
  1373
  //def sigma(rs: Set[Rexp]) : Rexp = ALTS(rs.toList)
Chengsong
parents:
diff changeset
  1374
  def o(r: Rexp) = if (nullable(r)) ONE else ZERO
Chengsong
parents:
diff changeset
  1375
  //def nlf(t: Rexp) : Rexp = ALTS(List( o(t), sigma_lf(lf(t)) ))
Chengsong
parents:
diff changeset
  1376
  def pdp(x: Char, r: Rexp) : Set[Rexp] = r match {
Chengsong
parents:
diff changeset
  1377
    case ZERO => Set[Rexp]()
Chengsong
parents:
diff changeset
  1378
    case ONE => Set[Rexp]()
Chengsong
parents:
diff changeset
  1379
    case CHAR(f) => if(x == f) Set(ONE) else Set[Rexp]()
Chengsong
parents:
diff changeset
  1380
    case ALTS(r1, r2) => pdp(x, r1) ++ pdp(x, r2)
Chengsong
parents:
diff changeset
  1381
    case STAR(r1) => pdp(x, r).map(a => SEQ(a, STAR(r1)))
Chengsong
parents:
diff changeset
  1382
    case SEQ(a0, b) => if(nullable(a0)) pdp(x, a0).map(a => SEQ(a, b)) ++ pdp(x, b) else pdp(x, a0).map(a => SEQ(a, b))
Chengsong
parents:
diff changeset
  1383
  }
Chengsong
parents:
diff changeset
  1384
  def pdps(s: List[Char], ts: Set[Rexp]): Set[Rexp] = s match {
Chengsong
parents:
diff changeset
  1385
    case x::xs => pdps(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
Chengsong
parents:
diff changeset
  1386
    case Nil => ts   
Chengsong
parents:
diff changeset
  1387
  }
Chengsong
parents:
diff changeset
  1388
  def pdpss(ss: List[List[Char]], t: Rexp): Set[Rexp] = ss.foldLeft( Set[Rexp]())((acc, s) => pdps(s, Set(t)) ++ acc)
Chengsong
parents:
diff changeset
  1389
Chengsong
parents:
diff changeset
  1390
Chengsong
parents:
diff changeset
  1391
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1392
  def starPrint(r: Rexp) : Unit = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1393
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1394
    case SEQ(head, rstar) =>
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1395
      println(shortRexpOutput(head) ++ "~STARREG")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1396
    case STAR(rstar) =>
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1397
      println("STARREG")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1398
    case ALTS(r1, r2) =>  
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1399
      println("(")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1400
      starPrint(r1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1401
      println("+")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1402
      starPrint(r2)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1403
      println(")")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1404
    case ZERO => println("0")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1405
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1406
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1407
  // @arg(doc = "small tests")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1408
  def n_astar_list(d: Int) : Rexp = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1409
    if(d == 0) STAR("a") 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1410
    else ALTS(STAR("a" * d), n_astar_list(d - 1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1411
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1412
  def n_astar_alts(d: Int) : Rexp = d match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1413
    case 0 => n_astar_list(0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1414
    case d => STAR(n_astar_list(d))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1415
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1416
  def n_astar_alts2(d: Int) : Rexp = d match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1417
    case 0 => n_astar_list(0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1418
    case d => STAR(STAR(n_astar_list(d)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1419
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1420
  def n_astar_aux(d: Int) = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1421
    if(d == 0) n_astar_alts(0)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1422
    else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1423
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1424
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1425
  def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1426
  //val STARREG = n_astar(3)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1427
  // ( STAR("a") | 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1428
  //                  ("a" | "aa").% | 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1429
  //                 ( "a" | "aa" | "aaa").% 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1430
  //                 ).%
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1431
  //( "a" | "aa" | "aaa" | "aaaa").% |
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1432
  //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1433
  (((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1434
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1435
  // @main
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1436
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1437
  def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1438
    (a, b) => b * a /
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1439
    Stream.iterate((a,b)){case (x,y) => (y, x%y)}.dropWhile(_._2 != 0).head._1.abs
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1440
  }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1441
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1442
  def small() = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1443
    //val pderSTAR = pderUNIV(STARREG)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1444
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1445
    //val refSize = pderSTAR.map(size(_)).sum
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1446
    for(n <- 5 to 5){
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1447
      val STARREG = n_astar_alts2(n)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1448
      val iMax = (lcm((1 to n).toList))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1449
      for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1450
        val prog0 = "a" * i
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1451
        //println(s"test: $prog0")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1452
        print(i)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1453
        print(" ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1454
        // print(i)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1455
        // print(" ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1456
        println(asize(bders_simp(prog0.toList, internalise(STARREG))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1457
        // println(asize(bdersStrong(prog0.toList, internalise(STARREG))))
431
Chengsong
parents:
diff changeset
  1458
      }
Chengsong
parents:
diff changeset
  1459
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1460
    }
533
Chengsong
parents: 532
diff changeset
  1461
  }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1462
  // small()
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1463
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1464
  def aaa_star() = {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1465
    val r = STAR(("a" | "aa"))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1466
    for(i <- 0 to 20) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1467
      val prog = "a" * i
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1468
      print(i+" ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1469
      println(asize(bders_simp(prog.toList, internalise(r))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1470
      //println(size(ders_simp(prog.toList, r)))
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1471
    }
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1472
  }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1473
  // aaa_star()
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1474
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1475
  def matching_ways_counting(n: Int): Int = 
573
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1476
  {
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1477
    if(n == 0) 1
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1478
    else if(n == 1) 2
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1479
    else (for(i <- 1 to n - 1) 
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1480
      yield matching_ways_counting(i) * matching_ways_counting(n - i) ).sum + (n + 1)
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1481
  }
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1482
  def naive_matcher() {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1483
    val r = STAR(STAR("a") ~ STAR("a"))
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1484
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1485
    // for(i <- 0 to 10) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1486
    //   val s = "a" * i 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1487
    //   val t1 = System.nanoTime
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1488
    //   matcher(s, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1489
    //   val duration = (System.nanoTime - t1) / 1e9d
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1490
    //   print(i)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1491
    //   print(" ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1492
    //   // print(duration)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1493
    //   // print(" ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1494
    //   (aprint(bders_simp(s.toList, internalise(r))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1495
    //   //print(size(ders_simp(s.toList, r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1496
    //   println()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1497
    // }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1498
    for(i <- 1 to 3) {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1499
      val s = "a" * i
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1500
      val t1 = System.nanoTime
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1501
      val derssimp_result = ders_simp(s.toList, r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1502
      println(i)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1503
      println(matching_ways_counting(i))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1504
      println(size(derssimp_result))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1505
      rprint(derssimp_result)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1506
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1507
573
454ced557605 chapter2 finished polishing
Chengsong
parents: 564
diff changeset
  1508
  }
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1509
  // naive_matcher()
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1510
  //single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1511
  //  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1512
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1513
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1514
  //STAR(SEQ(ALTS(CHAR(b),STAR(CHAR(b))),ALTS(ALTS(ONE,CHAR(b)),SEQ(CHAR(c),ONE))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1515
  def generator_test() {
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1516
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1517
    test(single(STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))), 1) { (r: Rexp) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1518
      // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1519
      val ss = Set("ab")//stringsFromRexp(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1520
      val boolList = ss.map(s => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1521
        //val bdStrong = bdersStrong(s.toList, internalise(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1522
        val bdStrong6 = bdersStrong6(s.toList, internalise(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1523
        val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1524
        val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1525
        val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1526
        (rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList)) ||
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1527
          bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1528
          rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken))//|| bdStrong6Set.size <= pdersSetBroken.size
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1529
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1530
      })
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1531
      //!boolList.exists(b => b == false)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1532
      !boolList.exists(b => b == false)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1533
      }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1534
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1535
    // small()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1536
    // generator_test()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1537
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1538
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1539
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1540
    //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1541
    //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1542
    //  CHAR('c')))))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1543
    //counterexample1: STAR(SEQ(ALTS(STAR(ZERO),ALTS(CHAR(a),CHAR(b))),SEQ(ONE,ALTS(CHAR(a),CHAR(b)))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1544
    //counterexample2: SEQ(ALTS(SEQ(CHAR(a),STAR(ONE)),STAR(ONE)),ALTS(CHAR(a),SEQ(ALTS(CHAR(c),CHAR(a)),CHAR(b))))
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1545
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1546
    //new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1547
    //new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1548
    //new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1549
    //circular double-nullable STAR(SEQ((STAR("b") | "a" | "b"), ("b" | ONE)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1550
    def counterexample_check() {
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1551
      val r : Rexp = SEQ(ALTS(ONE, 
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1552
        SEQ(ALTS(CHAR('f'), CHAR('b')), CHAR('g'))), SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e'))))//(1+(f +b)·g)·(a·(d·e))//STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1553
      val acc : Set[Rexp] = Set(SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e'))), SEQ(SEQ(CHAR('f'), CHAR('g')), SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e')))) )
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1554
      val a = internalise(r)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1555
      aprint(prune(a, acc));
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1556
        //ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1557
      //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1558
      // val s = "ab"
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1559
      // val bdStrong5 = bdersStrong6(s.toList, internalise(r))
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1560
      // val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1561
      // val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1562
      // val apdersSet = pdersSet.map(internalise)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1563
      // println("original regex ")
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1564
      // rprint(r)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1565
      // println("after strong bsimp")
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1566
      // aprint(bdStrong5)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1567
      // println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   ")
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1568
      // rsprint(bdStrong5Set)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1569
      // println("after pderUNIV")
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1570
      // rsprint(pdersSet.toList)
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1571
      // println("pderUNIV distinctBy6")
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1572
      // //asprint(distinctBy6(apdersSet.toList))
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1573
      // rsprint((pdersSet.toList).flatMap(turnIntoTerms))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1574
      // rsprint(turnIntoTerms(pdersSet.toList(3)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1575
      // println("NO 3 not into terms")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1576
      // rprint((pdersSet.toList()))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1577
      // println("after pderUNIV broken")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1578
      // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1579
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1580
    }
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1581
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1582
    // counterexample_check()
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1583
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1584
    def lf_display() {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1585
      val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1586
        ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1587
      //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1588
      val s = "ab"
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1589
      val bdStrong5 = bdersStrong6(s.toList, internalise(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1590
      val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1591
      val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1592
      val apdersSet = pdersSet.map(internalise)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1593
      lfprint(lf(r))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1594
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1595
    }
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1596
628
7af4e2420a8c ready to submit~~
Chengsong
parents: 591
diff changeset
  1597
    // lf_display()
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1598
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1599
    def breakable(r: Rexp) : Boolean = r match {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1600
      case SEQ(ALTS(_, _), _) => true
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1601
      case SEQ(r1, r2) => breakable(r1)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1602
      case _ => false
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1603
    }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1604
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1605
    def linform_test() {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1606
      val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1607
      val r_linforms = lf(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1608
      println(r_linforms.size)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1609
      val pderuniv = pderUNIV(r)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1610
      println(pderuniv.size)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1611
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1612
    // linform_test()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1613
    // 1
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1614
    def newStrong_test() {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1615
      val r2 = (CHAR('b') | ONE)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1616
      val r0 = CHAR('d')
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1617
      val r1 = (ONE | CHAR('c'))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1618
      val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1619
      println(s"original regex is: ")
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1620
      rprint(expRexp)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1621
      val expSimp5 = strongBsimp5(internalise(expRexp))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1622
      val expSimp6 = strongBsimp6(internalise(expRexp))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1623
      aprint(expSimp5)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1624
      aprint(expSimp6)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1625
    }
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1626
    // newStrong_test()
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1627
    // SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1628
    // SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1629
    // STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1630
    // SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
493
Chengsong
parents: 492
diff changeset
  1631
Chengsong
parents: 492
diff changeset
  1632
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1633
    // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1634
    // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1635
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1636
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1637
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1638
640
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1639
  def struct_regex(depth: Int) {
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1640
    if(depth <= 0) {
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1641
      ONE
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1642
    }
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1643
    else {
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1644
      val dice = 
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1645
    }
bd1354127574 more proofreading done, last version before submission
Chengsong
parents: 639
diff changeset
  1646
  }
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1647
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1648
    def bders_bderssimp() {
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1649
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1650
      
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1651
      val r = //(SEQ(ALTS(ONE,CHAR('c')),
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1652
        SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c')))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1653
          // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1654
      val ss = Set("aa")//stringsFromRexp(r)
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1655
          val boolList = ss.map(s => {
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1656
            //val bdStrong = bdersStrong(s.toList, internalise(r))
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1657
            val bds = (bders(s.toList, internalise(r)))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1658
            val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1659
            //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1660
            //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1661
            //rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1662
            //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1663
            //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1664
            rprint(r)
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1665
            println(asize(bds))
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1666
            println(asize(bdssimp))
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1667
            bds == bdssimp
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1668
          })
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1669
          //!boolList.exists(b => b == false)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1670
          !boolList.exists(b => b == false)
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1671
          }
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1672
        
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1673
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1674
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1675
        bders_bderssimp()
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1676
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1677
591
b2d0de6aee18 more polishing integrated comments chap2
Chengsong
parents: 573
diff changeset
  1678
639
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1679
// println("hi!!!!!")
80cc6dc4c98b until chap 7
Chengsong
parents: 629
diff changeset
  1680
// counterexample_check()