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