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