thys2/blexer2.sc
author Chengsong
Thu, 23 Jun 2022 16:09:40 +0100
changeset 543 b2bea5968b89
parent 541 5bf9f94c02e1
child 545 333013923c5a
permissions -rw-r--r--
thesis_thys
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
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   784
// "pAKC_aux rsa r ctx = (if (regConcat (SEQ (erase r) ( ctx) )) ⊆ (regConcat (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!
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   799
def regConcat(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) 
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   803
    //   regConcat(r, rs1) 
500
Chengsong
parents: 494
diff changeset
   804
    // else
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   805
      regConcat(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")
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   822
  // rsprint(breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp))
500
Chengsong
parents: 494
diff changeset
   823
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   824
  if (breakIntoTerms(regConcat(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] = {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   931
  turnIntoTerms((regConcat(erase(r), ctx)))
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] =
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   936
  turnIntoTerms(regConcat(r, ctx)).toSet
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 = {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   947
  // if (erase(r) == ONE &&  acc != Set()) 
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   948
  // {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   949
  //   println("ctx")
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   950
  //   rsprint(ctx)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   951
  //   println("acc")
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   952
  //   rsprint(acc)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   953
  //   println("acc-end")
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   954
  // }
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   955
  if (ABIncludedByC(a = r, b = ctx, c = acc, 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   956
                    f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   957
  {
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   958
    AZERO
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   959
  }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   960
  else{
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   961
    r match {
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   962
      case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   963
        case AZERO => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   964
          AZERO
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   965
        case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   966
          prune6(acc, fuse(bs1, r2), ctx)
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   967
        case r1p => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   968
          ASEQ(bs, r1p, r2)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   969
      }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   970
      case AALTS(bs, rs0) => 
530
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
   971
        rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   972
          case Nil => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   973
            AZERO
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   974
          case r :: Nil => 
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
   975
            fuse(bs, r) 
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   976
          case rs0p => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   977
            AALTS(bs, rs0p)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   978
        }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   979
      case r => r
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   980
    }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   981
  }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   982
}
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
   983
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   984
def prune6cc(acc: Set[Rexp], r: Rexp, ctx: List[Rexp]) : Rexp = {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   985
  if (ABIncludedByC(a = r, b = ctx, c = acc, 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   986
                    f = attachCtxcc, subseteqPred = rs1_subseteq_rs2)) 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   987
  {//acc.flatMap(breakIntoTerms
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   988
    ZERO
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   989
  }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   990
  else{
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   991
    r match {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   992
      case SEQ(r1, r2) => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   993
      (prune6cc(acc, r1, r2 :: ctx)) match{
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   994
        case ZERO => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   995
          ZERO
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   996
        case ONE => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   997
          r2
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   998
        case r1p => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
   999
          SEQ(r1p, r2)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1000
      }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1001
      case ALTS(r1, r2) => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1002
        List(r1, r2).map(r => prune6cc(acc, r, ctx)).filter(_ != AZERO) match {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1003
          case Nil => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1004
            ZERO
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1005
          case r :: Nil => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1006
            r 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1007
          case ra :: rb :: Nil => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1008
            ALTS(ra, rb)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1009
        }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1010
      case r => r
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1011
    }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1012
  }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1013
}
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1014
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1015
def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : 
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1016
List[ARexp] = xs match {
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1017
  case Nil => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1018
    Nil
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1019
  case x :: xs => {
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1020
    val erased = erase(x)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1021
    if(acc.contains(erased)){
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1022
      distinctBy6(xs, acc)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1023
    }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1024
    else{
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1025
      val pruned = prune6(acc, x)
533
Chengsong
parents: 532
diff changeset
  1026
      val newTerms = turnIntoTerms(erase(pruned))
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1027
      pruned match {
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1028
        case AZERO => 
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1029
          distinctBy6(xs, acc)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1030
        case xPrime => 
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1031
          xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1032
      }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1033
    }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1034
  }
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1035
}
431
Chengsong
parents:
diff changeset
  1036
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1037
def distinctByacc(xs: List[Rexp], acc: Set[Rexp] = Set()) : Set[Rexp] = xs match {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1038
  case Nil => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1039
    acc
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1040
  case x :: xs => {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1041
    if(acc.contains(x)){
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1042
      distinctByacc(xs, acc)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1043
    }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1044
    else{
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1045
      val pruned = prune6cc(acc, x, Nil)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1046
      val newTerms = turnIntoTerms(pruned)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1047
      pruned match {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1048
        case ZERO => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1049
          distinctByacc(xs, acc)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1050
        case xPrime => 
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1051
          distinctByacc(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1052
      }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1053
    }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1054
  }
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1055
}
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1056
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1057
def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1058
  case SEQ(r1, r2)  => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1059
  case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1060
  case ZERO => Nil
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1061
  case _ => r::Nil
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1062
}
431
Chengsong
parents:
diff changeset
  1063
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1064
def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1065
  //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1066
  case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1067
  case ZERO => Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1068
  case _ => r::Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1069
}
431
Chengsong
parents:
diff changeset
  1070
Chengsong
parents:
diff changeset
  1071
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1072
def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1073
  case (ONE, bs) => (Empty, bs)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1074
  case (CHAR(f), bs) => (Chr(f), bs)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1075
  case (ALTS(r1, r2), Z::bs1) => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1076
      val (v, bs2) = decode_aux(r1, bs1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1077
      (Left(v), bs2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1078
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1079
  case (ALTS(r1, r2), S::bs1) => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1080
      val (v, bs2) = decode_aux(r2, bs1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1081
      (Right(v), bs2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1082
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1083
  case (SEQ(r1, r2), bs) => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1084
    val (v1, bs1) = decode_aux(r1, bs)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1085
    val (v2, bs2) = decode_aux(r2, bs1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1086
    (Sequ(v1, v2), bs2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1087
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1088
  case (STAR(r1), S::bs) => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1089
    val (v, bs1) = decode_aux(r1, bs)
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1090
    //(v)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1091
    val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1092
    (Stars(v::vs), bs2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1093
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1094
  case (STAR(_), Z::bs) => (Stars(Nil), bs)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1095
  case (RECD(x, r1), bs) => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1096
    val (v, bs1) = decode_aux(r1, bs)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1097
    (Rec(x, v), bs1)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1098
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1099
  case (NOT(r), bs) => (Nots(r.toString), bs)
431
Chengsong
parents:
diff changeset
  1100
}
Chengsong
parents:
diff changeset
  1101
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1102
def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1103
  case (v, Nil) => v
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1104
  case _ => throw new Exception("Not decodable")
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1105
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1106
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1107
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1108
431
Chengsong
parents:
diff changeset
  1109
def blexing_simp(r: Rexp, s: String) : Val = {
Chengsong
parents:
diff changeset
  1110
    val bit_code = blex_simp(internalise(r), s.toList)
Chengsong
parents:
diff changeset
  1111
    decode(r, bit_code)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1112
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1113
def simpBlexer(r: Rexp, s: String) : Val = {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1114
  Try(blexing_simp(r, s)).getOrElse(Failure)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1115
}
431
Chengsong
parents:
diff changeset
  1116
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1117
def strong_blexing_simp(r: Rexp, s: String) : Val = {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1118
  decode(r, strong_blex_simp(internalise(r), s.toList))
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1119
}
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1120
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1121
def strong_blexing_simp5(r: Rexp, s: String) : Val = {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1122
  decode(r, strong_blex_simp5(internalise(r), s.toList))
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1123
}
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 strongBlexer(r: Rexp, s: String) : Val = {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1127
  Try(strong_blexing_simp(r, s)).getOrElse(Failure)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1128
}
431
Chengsong
parents:
diff changeset
  1129
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1130
def strongBlexer5(r: Rexp, s: String): Val = {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1131
  Try(strong_blexing_simp5(r, s)).getOrElse(Failure)
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1132
}
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1133
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1134
def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1135
  case Nil => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1136
    if (bnullable(r)) {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1137
      //println(asize(r))
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1138
      val bits = mkepsBC(r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1139
      bits
431
Chengsong
parents:
diff changeset
  1140
    }
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1141
    else 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1142
      throw new Exception("Not matched")
431
Chengsong
parents:
diff changeset
  1143
  }
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1144
  case c::cs => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1145
    val der_res = bder(c,r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1146
    val simp_res = strongBsimp(der_res)  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1147
    strong_blex_simp(simp_res, cs)      
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1148
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1149
}
431
Chengsong
parents:
diff changeset
  1150
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1151
def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1152
  case Nil => {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1153
    if (bnullable(r)) {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1154
      val bits = mkepsBC(r)
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1155
      bits
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1156
    }
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1157
    else 
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1158
      throw new Exception("Not matched")
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1159
  }
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1160
  case c::cs => {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1161
    val der_res = bder(c,r)
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1162
    val simp_res = strongBsimp5(der_res)  
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1163
    strong_blex_simp5(simp_res, cs)      
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1164
  }
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1165
}
431
Chengsong
parents:
diff changeset
  1166
Chengsong
parents:
diff changeset
  1167
Chengsong
parents:
diff changeset
  1168
  def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
Chengsong
parents:
diff changeset
  1169
    case Nil => r
435
Chengsong
parents: 432
diff changeset
  1170
    case c::s => 
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1171
      //println(erase(r))
435
Chengsong
parents: 432
diff changeset
  1172
      bders_simp(s, bsimp(bder(c, r)))
431
Chengsong
parents:
diff changeset
  1173
  }
Chengsong
parents:
diff changeset
  1174
  
494
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1175
  def bdersStrong5(s: List[Char], r: ARexp) : ARexp = s match {
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1176
    case Nil => r
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1177
    case c::s => bdersStrong5(s, strongBsimp5(bder(c, r)))
c730d018ebfa blexer2
Chengsong
parents: 493
diff changeset
  1178
  }
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1179
  def bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1180
    case Nil => r
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1181
    case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1182
  }
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1183
  def bdersStrong7(s: List[Char], r: ARexp) : ARexp = s match {
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1184
    case Nil => r
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1185
    case c::s => bdersStrong7(s, strongBsimp7(bder(c, r)))
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1186
  }
431
Chengsong
parents:
diff changeset
  1187
  def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
Chengsong
parents:
diff changeset
  1188
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1189
  def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
431
Chengsong
parents:
diff changeset
  1190
    case Nil => r 
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1191
    case c::s => bdersStrong(s, strongBsimp(bder(c, r)))
431
Chengsong
parents:
diff changeset
  1192
  }
Chengsong
parents:
diff changeset
  1193
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1194
  def bdersStrongRexp(s: String, r: Rexp) : ARexp = bdersStrong(s.toList, internalise(r))
431
Chengsong
parents:
diff changeset
  1195
Chengsong
parents:
diff changeset
  1196
  def erase(r:ARexp): Rexp = r match{
Chengsong
parents:
diff changeset
  1197
    case AZERO => ZERO
Chengsong
parents:
diff changeset
  1198
    case AONE(_) => ONE
Chengsong
parents:
diff changeset
  1199
    case ACHAR(bs, c) => CHAR(c)
Chengsong
parents:
diff changeset
  1200
    case AALTS(bs, Nil) => ZERO
Chengsong
parents:
diff changeset
  1201
    case AALTS(bs, a::Nil) => erase(a)
Chengsong
parents:
diff changeset
  1202
    case AALTS(bs, a::as) => ALTS(erase(a), erase(AALTS(bs, as)))
Chengsong
parents:
diff changeset
  1203
    case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
Chengsong
parents:
diff changeset
  1204
    case ASTAR(cs, r)=> STAR(erase(r))
Chengsong
parents:
diff changeset
  1205
    case ANOT(bs, r) => NOT(erase(r))
Chengsong
parents:
diff changeset
  1206
    case AANYCHAR(bs) => ANYCHAR
Chengsong
parents:
diff changeset
  1207
  }
Chengsong
parents:
diff changeset
  1208
Chengsong
parents:
diff changeset
  1209
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1210
  def allCharSeq(r: Rexp) : Boolean = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1211
    case CHAR(c) => true
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1212
    case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1213
    case _ => false
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1214
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1215
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1216
  def flattenSeq(r: Rexp) : String = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1217
    case CHAR(c) => c.toString
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1218
    case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1219
    case _ => throw new Error("flatten unflattenable rexp")
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1220
  } 
431
Chengsong
parents:
diff changeset
  1221
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1222
  def shortRexpOutput(r: Rexp) : String = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1223
      case CHAR(c) => c.toString
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1224
      case ONE => "1"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1225
      case ZERO => "0"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1226
      case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1227
      case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1228
      case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1229
      case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1230
      case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1231
      //case RTOP => "RTOP"
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1232
    }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1233
431
Chengsong
parents:
diff changeset
  1234
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1235
  def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1236
      case Nil => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1237
        if (bnullable(r)) {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1238
          val bits = mkepsBC(r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1239
          bits
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1240
        }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1241
        else 
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1242
          throw new Exception("Not matched")
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1243
      }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1244
      case c::cs => {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1245
        val der_res = bder(c,r)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1246
        val simp_res = bsimp(der_res)  
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1247
        blex_simp(simp_res, cs)      
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1248
      }
431
Chengsong
parents:
diff changeset
  1249
  }
Chengsong
parents:
diff changeset
  1250
Chengsong
parents:
diff changeset
  1251
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1252
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1253
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1254
    def size(r: Rexp) : Int = r match {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1255
      case ZERO => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1256
      case ONE => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1257
      case CHAR(_) => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1258
      case ANYCHAR => 1
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1259
      case NOT(r0) => 1 + size(r0)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1260
      case SEQ(r1, r2) => 1 + size(r1) + size(r2)
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1261
      case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1262
      case STAR(r) => 1 + size(r)
431
Chengsong
parents:
diff changeset
  1263
    }
Chengsong
parents:
diff changeset
  1264
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1265
    def asize(a: ARexp) = size(erase(a))
431
Chengsong
parents:
diff changeset
  1266
Chengsong
parents:
diff changeset
  1267
//pder related
Chengsong
parents:
diff changeset
  1268
type Mon = (Char, Rexp)
Chengsong
parents:
diff changeset
  1269
type Lin = Set[Mon]
Chengsong
parents:
diff changeset
  1270
Chengsong
parents:
diff changeset
  1271
def dot_prod(rs: Set[Rexp], r: Rexp): Set[Rexp] = r match {
Chengsong
parents:
diff changeset
  1272
    case ZERO => Set()
Chengsong
parents:
diff changeset
  1273
    case ONE => rs
Chengsong
parents:
diff changeset
  1274
    case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
Chengsong
parents:
diff changeset
  1275
  }
Chengsong
parents:
diff changeset
  1276
  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
  1277
    case ZERO => Set()
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1278
    // case ONE => l
526
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1279
    case t => l.map( m => m._2 match 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1280
      {
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1281
        case ZERO => m 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1282
        case ONE => (m._1, t) 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1283
        case p => (m._1, SEQ(p, t)) 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1284
      }  
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1285
    
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1286
    )
431
Chengsong
parents:
diff changeset
  1287
  }
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1288
  def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1289
    case ZERO => Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1290
    case ONE => l
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1291
    case t => l.map(m => m._2 match
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1292
      {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1293
        case ZERO => m
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1294
        case ONE => (m._1, t)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1295
        case p => (m._1, SEQ(p, t))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1296
      }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1297
    )
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1298
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1299
  }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1300
  def lfList(r: Rexp) : List[Mon] = r match {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1301
    case ZERO => Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1302
    case ONE => Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1303
    case CHAR(f) => {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1304
      (f, ONE) :: Nil
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1305
    }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1306
    case ALTS(r1, r2) => {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1307
      lfList(r1) ++ lfList(r2)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1308
    }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1309
    case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1310
    case SEQ(r1, r2) => {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1311
      if(nullable(r1))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1312
        cir_prodList(lfList(r1), r2) ++ lfList(r2)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1313
      else
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1314
        cir_prodList(lfList(r1), r2)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1315
    }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1316
  }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1317
  def lfprint(ls: Lin) = ls.foreach(m =>{
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1318
    println(m._1)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1319
    rprint(m._2)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1320
    })
431
Chengsong
parents:
diff changeset
  1321
  def lf(r: Rexp): Lin = r match {
Chengsong
parents:
diff changeset
  1322
    case ZERO => Set()
Chengsong
parents:
diff changeset
  1323
    case ONE => Set()
Chengsong
parents:
diff changeset
  1324
    case CHAR(f) => {
Chengsong
parents:
diff changeset
  1325
      //val Some(c) = alphabet.find(f) 
Chengsong
parents:
diff changeset
  1326
      Set((f, ONE))
Chengsong
parents:
diff changeset
  1327
    }
Chengsong
parents:
diff changeset
  1328
    case ALTS(r1, r2) => {
Chengsong
parents:
diff changeset
  1329
      lf(r1 ) ++ lf(r2)
Chengsong
parents:
diff changeset
  1330
    }
Chengsong
parents:
diff changeset
  1331
    case STAR(r1) => cir_prod(lf(r1), STAR(r1)) //may try infix notation later......
Chengsong
parents:
diff changeset
  1332
    case SEQ(r1, r2) =>{
Chengsong
parents:
diff changeset
  1333
      if (nullable(r1))
Chengsong
parents:
diff changeset
  1334
        cir_prod(lf(r1), r2) ++ lf(r2)
Chengsong
parents:
diff changeset
  1335
      else
Chengsong
parents:
diff changeset
  1336
        cir_prod(lf(r1), r2) 
Chengsong
parents:
diff changeset
  1337
    }
Chengsong
parents:
diff changeset
  1338
  }
Chengsong
parents:
diff changeset
  1339
  def lfs(r: Set[Rexp]): Lin = {
Chengsong
parents:
diff changeset
  1340
    r.foldLeft(Set[Mon]())((acc, r) => acc ++ lf(r))
Chengsong
parents:
diff changeset
  1341
  }
Chengsong
parents:
diff changeset
  1342
Chengsong
parents:
diff changeset
  1343
  def pder(x: Char, t: Rexp): Set[Rexp] = {
Chengsong
parents:
diff changeset
  1344
    val lft = lf(t)
Chengsong
parents:
diff changeset
  1345
    (lft.filter(mon => if(mon._1 == x) true else false)).map(mon => mon._2)
Chengsong
parents:
diff changeset
  1346
  }
Chengsong
parents:
diff changeset
  1347
  def pders_single(s: List[Char], t: Rexp) : Set[Rexp] = s match {
Chengsong
parents:
diff changeset
  1348
    case x::xs => pders(xs, pder(x, t))
Chengsong
parents:
diff changeset
  1349
    case Nil => Set(t)
Chengsong
parents:
diff changeset
  1350
  }
Chengsong
parents:
diff changeset
  1351
  def pders(s: List[Char], ts: Set[Rexp]) : Set[Rexp] = s match {
Chengsong
parents:
diff changeset
  1352
    case x::xs => pders(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
Chengsong
parents:
diff changeset
  1353
    case Nil => ts 
Chengsong
parents:
diff changeset
  1354
  }
526
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1355
  def pderss(ss: List[List[Char]], t: Rexp): Set[Rexp] = 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1356
    ss.foldLeft( Set[Rexp]() )( (acc, s) => pders_single(s, t) ++ acc )
431
Chengsong
parents:
diff changeset
  1357
  def pdera(t: Rexp): Set[Rexp] = lf(t).map(mon => mon._2)
Chengsong
parents:
diff changeset
  1358
  //all implementation of partial derivatives that involve set union are potentially buggy
Chengsong
parents:
diff changeset
  1359
  //because they don't include the original regular term before they are pdered.
Chengsong
parents:
diff changeset
  1360
  //now only pderas is fixed.
526
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1361
  def pderas(t: Set[Rexp], d: Int): Set[Rexp] = 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1362
    if(d > 0) 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1363
      pderas(lfs(t).map(mon => mon._2), d - 1) ++ t 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1364
    else 
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1365
      lfs(t).map(mon => mon._2) ++ t//repeated application of pderas over the newest set of pders.
431
Chengsong
parents:
diff changeset
  1366
  def pderUNIV(r: Rexp) : Set[Rexp] = pderas(Set(r), awidth(r) + 1)
Chengsong
parents:
diff changeset
  1367
  def awidth(r: Rexp) : Int = r match {
Chengsong
parents:
diff changeset
  1368
    case CHAR(c) => 1
Chengsong
parents:
diff changeset
  1369
    case SEQ(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents:
diff changeset
  1370
    case ALTS(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents:
diff changeset
  1371
    case ONE => 0
Chengsong
parents:
diff changeset
  1372
    case ZERO => 0
Chengsong
parents:
diff changeset
  1373
    case STAR(r) => awidth(r)
Chengsong
parents:
diff changeset
  1374
  }
Chengsong
parents:
diff changeset
  1375
  //def sigma_lf(l: Set[Mon]) : Rexp = ALTS(l.map(mon => SEQ(CHAR(mon._1),mon._2)).toList)
Chengsong
parents:
diff changeset
  1376
  //def sigma(rs: Set[Rexp]) : Rexp = ALTS(rs.toList)
Chengsong
parents:
diff changeset
  1377
  def o(r: Rexp) = if (nullable(r)) ONE else ZERO
Chengsong
parents:
diff changeset
  1378
  //def nlf(t: Rexp) : Rexp = ALTS(List( o(t), sigma_lf(lf(t)) ))
Chengsong
parents:
diff changeset
  1379
  def pdp(x: Char, r: Rexp) : Set[Rexp] = r match {
Chengsong
parents:
diff changeset
  1380
    case ZERO => Set[Rexp]()
Chengsong
parents:
diff changeset
  1381
    case ONE => Set[Rexp]()
Chengsong
parents:
diff changeset
  1382
    case CHAR(f) => if(x == f) Set(ONE) else Set[Rexp]()
Chengsong
parents:
diff changeset
  1383
    case ALTS(r1, r2) => pdp(x, r1) ++ pdp(x, r2)
Chengsong
parents:
diff changeset
  1384
    case STAR(r1) => pdp(x, r).map(a => SEQ(a, STAR(r1)))
Chengsong
parents:
diff changeset
  1385
    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
  1386
  }
Chengsong
parents:
diff changeset
  1387
  def pdps(s: List[Char], ts: Set[Rexp]): Set[Rexp] = s match {
Chengsong
parents:
diff changeset
  1388
    case x::xs => pdps(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
Chengsong
parents:
diff changeset
  1389
    case Nil => ts   
Chengsong
parents:
diff changeset
  1390
  }
Chengsong
parents:
diff changeset
  1391
  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
  1392
Chengsong
parents:
diff changeset
  1393
Chengsong
parents:
diff changeset
  1394
Chengsong
parents:
diff changeset
  1395
def starPrint(r: Rexp) : Unit = r match {
Chengsong
parents:
diff changeset
  1396
        
Chengsong
parents:
diff changeset
  1397
          case SEQ(head, rstar) =>
Chengsong
parents:
diff changeset
  1398
            println(shortRexpOutput(head) ++ "~STARREG")
Chengsong
parents:
diff changeset
  1399
          case STAR(rstar) =>
Chengsong
parents:
diff changeset
  1400
            println("STARREG")
Chengsong
parents:
diff changeset
  1401
          case ALTS(r1, r2) =>  
Chengsong
parents:
diff changeset
  1402
            println("(")
Chengsong
parents:
diff changeset
  1403
            starPrint(r1)
Chengsong
parents:
diff changeset
  1404
            println("+")
Chengsong
parents:
diff changeset
  1405
            starPrint(r2)
Chengsong
parents:
diff changeset
  1406
            println(")")
Chengsong
parents:
diff changeset
  1407
          case ZERO => println("0")
Chengsong
parents:
diff changeset
  1408
      }
Chengsong
parents:
diff changeset
  1409
Chengsong
parents:
diff changeset
  1410
// @arg(doc = "small tests")
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1411
def n_astar_list(d: Int) : Rexp = {
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1412
  if(d == 0) STAR("a") 
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1413
  else ALTS(STAR("a" * d), n_astar_list(d - 1))
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1414
}
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1415
def n_astar_alts(d: Int) : Rexp = d match {
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1416
  case 0 => n_astar_list(0)
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1417
  case d => STAR(n_astar_list(d))
533
Chengsong
parents: 532
diff changeset
  1418
  }
Chengsong
parents: 532
diff changeset
  1419
def n_astar_alts2(d: Int) : Rexp = d match {
Chengsong
parents: 532
diff changeset
  1420
  case 0 => n_astar_list(0)
Chengsong
parents: 532
diff changeset
  1421
  case d => STAR(STAR(n_astar_list(d)))
Chengsong
parents: 532
diff changeset
  1422
  }
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1423
def n_astar_aux(d: Int) = {
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1424
  if(d == 0) n_astar_alts(0)
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1425
  else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1426
}
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1427
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1428
def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d))
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1429
//val STARREG = n_astar(3)
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1430
// ( STAR("a") | 
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1431
//                  ("a" | "aa").% | 
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1432
//                 ( "a" | "aa" | "aaa").% 
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1433
//                 ).%
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1434
                //( "a" | "aa" | "aaa" | "aaaa").% |
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1435
                //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% 
431
Chengsong
parents:
diff changeset
  1436
(((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
Chengsong
parents:
diff changeset
  1437
Chengsong
parents:
diff changeset
  1438
// @main
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1439
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1440
def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1441
  (a, b) => b * a /
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1442
  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
  1443
}
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1444
431
Chengsong
parents:
diff changeset
  1445
def small() = {
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1446
  //val pderSTAR = pderUNIV(STARREG)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1447
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1448
  //val refSize = pderSTAR.map(size(_)).sum
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1449
  for(n <- 5 to 5){
533
Chengsong
parents: 532
diff changeset
  1450
    val STARREG = n_astar_alts2(n)
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1451
    val iMax = (lcm((1 to n).toList))
533
Chengsong
parents: 532
diff changeset
  1452
    for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1453
      val prog0 = "a" * i
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1454
      //println(s"test: $prog0")
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1455
      print(i)
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1456
      print(" ")
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1457
      // print(i)
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1458
      // print(" ")
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1459
      println(asize(bders_simp(prog0.toList, internalise(STARREG))))
533
Chengsong
parents: 532
diff changeset
  1460
      // println(asize(bdersStrong7(prog0.toList, internalise(STARREG))))
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1461
    }
539
Chengsong
parents: 536
diff changeset
  1462
    
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1463
  }
431
Chengsong
parents:
diff changeset
  1464
}
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1465
// small()
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1466
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1467
def aaa_star() = {
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1468
  val r = STAR(("a" | "aa"))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1469
  for(i <- 0 to 20) {
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1470
    val prog = "a" * i
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1471
    print(i+" ")
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1472
    println(asize(bders_simp(prog.toList, internalise(r))))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1473
    //println(size(ders_simp(prog.toList, r)))
536
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1474
  }
aff7bf93b9c7 comments addressed all
Chengsong
parents: 533
diff changeset
  1475
}
539
Chengsong
parents: 536
diff changeset
  1476
// aaa_star()
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
539
Chengsong
parents: 536
diff changeset
  1480
  for(i <- 0 to 20) {
Chengsong
parents: 536
diff changeset
  1481
    val s = "a" * i 
Chengsong
parents: 536
diff changeset
  1482
    val t1 = System.nanoTime
Chengsong
parents: 536
diff changeset
  1483
    matcher(s, r)
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(" ")
Chengsong
parents: 536
diff changeset
  1487
    // print(duration)
Chengsong
parents: 536
diff changeset
  1488
    // print(" ")
Chengsong
parents: 536
diff changeset
  1489
    print(asize(bders_simp(s.toList, internalise(r))))
Chengsong
parents: 536
diff changeset
  1490
    //print(size(ders_simp(s.toList, r)))
Chengsong
parents: 536
diff changeset
  1491
    println()
Chengsong
parents: 536
diff changeset
  1492
  }
Chengsong
parents: 536
diff changeset
  1493
  // for(i <- 1 to 40000000 by 500000) {
Chengsong
parents: 536
diff changeset
  1494
  //   val s = "a" * i
Chengsong
parents: 536
diff changeset
  1495
  //   val t1 = System.nanoTime
Chengsong
parents: 536
diff changeset
  1496
  //   val derssimp_result = ders_simp(s.toList, r)
Chengsong
parents: 536
diff changeset
  1497
  //   val duration = (System.nanoTime - t1) / 1e9d
Chengsong
parents: 536
diff changeset
  1498
  //   print(i)
Chengsong
parents: 536
diff changeset
  1499
  //   print(" ")
Chengsong
parents: 536
diff changeset
  1500
  //   print(duration)
Chengsong
parents: 536
diff changeset
  1501
  //   println()
Chengsong
parents: 536
diff changeset
  1502
  // }
Chengsong
parents: 536
diff changeset
  1503
  
Chengsong
parents: 536
diff changeset
  1504
}
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1505
// naive_matcher()
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1506
//single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1507
//  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1508
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1509
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1510
//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
  1511
def generator_test() {
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1512
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1513
  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
  1514
  // 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
  1515
    val ss = Set("ab")//stringsFromRexp(r)
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1516
    val boolList = ss.map(s => {
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1517
      //val bdStrong = bdersStrong(s.toList, internalise(r))
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1518
      val bdStrong6 = bdersStrong6(s.toList, internalise(r))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1519
      val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
533
Chengsong
parents: 532
diff changeset
  1520
      val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
Chengsong
parents: 532
diff changeset
  1521
      val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1522
      (rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList)) ||
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1523
      bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1524
      rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken))//|| bdStrong6Set.size <= pdersSetBroken.size
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1525
      
493
Chengsong
parents: 492
diff changeset
  1526
    })
500
Chengsong
parents: 494
diff changeset
  1527
    //!boolList.exists(b => b == false)
493
Chengsong
parents: 492
diff changeset
  1528
    !boolList.exists(b => b == false)
492
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1529
  }
61eff2abb0b6 problem with erase
Chengsong
parents: 435
diff changeset
  1530
}
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1531
// small()
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1532
// generator_test()
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1533
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1534
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1535
  
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1536
  //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1537
          //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1538
          //  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
  1539
//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
  1540
//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
  1541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1542
//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
  1543
//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
  1544
//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
  1545
//circular double-nullable STAR(SEQ((STAR("b") | "a" | "b"), ("b" | ONE)))
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1546
def counterexample_check() {
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1547
  val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1548
    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
  1549
    //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1550
  val s = "ab"
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1551
  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1552
  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
533
Chengsong
parents: 532
diff changeset
  1553
  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
  1554
  val apdersSet = pdersSet.map(internalise)
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1555
  println("original regex ")
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1556
  rprint(r)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1557
  println("after strong bsimp")
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1558
  aprint(bdStrong5)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1559
  println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   ")
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1560
  rsprint(bdStrong5Set)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1561
  println("after pderUNIV")
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1562
  rsprint(pdersSet.toList)
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1563
  println("pderUNIV distinctBy6")
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1564
  //asprint(distinctBy6(apdersSet.toList))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1565
  rsprint((pdersSet.toList).flatMap(turnIntoTerms))
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1566
  // rsprint(turnIntoTerms(pdersSet.toList(3)))
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1567
  // println("NO 3 not into terms")
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1568
  // rprint((pdersSet.toList()))
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1569
  // println("after pderUNIV broken")
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1570
  // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1571
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1572
}
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1573
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1574
// counterexample_check()
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1575
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1576
def lf_display() {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1577
  val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1578
    ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1579
    //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1580
  val s = "ab"
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1581
  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1582
  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1583
  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
  1584
  val apdersSet = pdersSet.map(internalise)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1585
  lfprint(lf(r))
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
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1589
lf_display()
541
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1590
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1591
def breakable(r: Rexp) : Boolean = r match {
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1592
  case SEQ(ALTS(_, _), _) => true
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1593
  case SEQ(r1, r2) => breakable(r1)
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1594
  case _ => false
5bf9f94c02e1 some comments implemented
Chengsong
parents: 539
diff changeset
  1595
}
532
cc54ce075db5 restructured
Chengsong
parents: 530
diff changeset
  1596
526
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1597
def linform_test() {
530
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
  1598
  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
  1599
  val r_linforms = lf(r)
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1600
  println(r_linforms.size)
530
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
  1601
  val pderuniv = pderUNIV(r)
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
  1602
  println(pderuniv.size)
526
cb702fb4227f updated
Chengsong
parents: 518
diff changeset
  1603
}
530
823d9b19d21c all comments addressed
Chengsong
parents: 526
diff changeset
  1604
// linform_test()
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1605
// 1
518
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1606
def newStrong_test() {
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1607
  val r2 = (CHAR('b') | ONE)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1608
  val r0 = CHAR('d')
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1609
  val r1 = (ONE | CHAR('c'))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1610
  val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1611
  println(s"original regex is: ")
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1612
  rprint(expRexp)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1613
  val expSimp5 = strongBsimp5(internalise(expRexp))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1614
  val expSimp6 = strongBsimp6(internalise(expRexp))
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1615
  aprint(expSimp5)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1616
  aprint(expSimp6)
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1617
}
ff7945a988a3 more to thesis
Chengsong
parents: 516
diff changeset
  1618
// newStrong_test()
516
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1619
// SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1620
// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1621
// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
6fecb7fe8cd0 blexer2: modified for plotting
Chengsong
parents: 514
diff changeset
  1622
// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
493
Chengsong
parents: 492
diff changeset
  1623
Chengsong
parents: 492
diff changeset
  1624
Chengsong
parents: 492
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))
543
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1626
// 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
  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
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1632
def bders_bderssimp() {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1633
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1634
  test(single(SEQ(ALTS(ONE,CHAR('c')),
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1635
  SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 1) { (r: Rexp) => 
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1636
  // 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
  1637
    val ss = Set("aa")//stringsFromRexp(r)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1638
    val boolList = ss.map(s => {
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1639
      //val bdStrong = bdersStrong(s.toList, internalise(r))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1640
      val bds = bsimp(bders(s.toList, internalise(r)))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1641
      val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1642
      //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1643
      //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1644
      //rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1645
      //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1646
      //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1647
      rprint(r)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1648
      println(bds)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1649
      println(bdssimp)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1650
      bds == bdssimp
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1651
    })
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1652
    //!boolList.exists(b => b == false)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1653
    !boolList.exists(b => b == false)
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1654
  }
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1655
}
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1656
//  bders_bderssimp()
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1657
  
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1658
b2bea5968b89 thesis_thys
Chengsong
parents: 541
diff changeset
  1659