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