thys2/blexer1.sc
author Chengsong
Sat, 05 Feb 2022 15:30:01 +0000
changeset 412 48876e1092f1
parent 409 f71df68776bb
child 414 1234e6bd4fd1
permissions -rw-r--r--
newDB
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     1
// A simple lexer inspired by work of Sulzmann & Lu
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     2
//==================================================
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     3
//
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     4
// Call the test cases with 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     5
//
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     6
//   amm lexer.sc small
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     7
//   amm lexer.sc fib
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     8
//   amm lexer.sc loops
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
     9
//   amm lexer.sc email
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    10
//
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    11
//   amm lexer.sc all
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    12
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    13
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    14
// regular expressions including records
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    15
abstract class Rexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    16
case object ZERO extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    17
case object ONE extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    18
case object ANYCHAR extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    19
case class CHAR(c: Char) extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    20
case class ALTS(r1: Rexp, r2: Rexp) extends Rexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    21
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    22
case class STAR(r: Rexp) extends Rexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    23
case class RECD(x: String, r: Rexp) extends Rexp  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    24
case class NTIMES(n: Int, r: Rexp) extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    25
case class OPTIONAL(r: Rexp) extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    26
case class NOT(r: Rexp) extends Rexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    27
                // records for extracting strings or tokens
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    28
  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    29
// values  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    30
abstract class Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    31
case object Empty extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    32
case class Chr(c: Char) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    33
case class Sequ(v1: Val, v2: Val) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    34
case class Left(v: Val) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    35
case class Right(v: Val) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    36
case class Stars(vs: List[Val]) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    37
case class Rec(x: String, v: Val) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    38
case class Ntime(vs: List[Val]) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    39
case class Optionall(v: Val) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    40
case class Nots(s: String) extends Val
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    41
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    42
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    43
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    44
abstract class Bit
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    45
case object Z extends Bit
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    46
case object S extends Bit
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    47
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    48
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    49
type Bits = List[Bit]
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    50
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    51
abstract class ARexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    52
case object AZERO extends ARexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    53
case class AONE(bs: Bits) extends ARexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    54
case class ACHAR(bs: Bits, c: Char) extends ARexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    55
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    56
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    57
case class ASTAR(bs: Bits, r: ARexp) extends ARexp 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    58
case class ANOT(bs: Bits, r: ARexp) extends ARexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    59
case class AANYCHAR(bs: Bits) extends ARexp
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    60
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    61
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    62
   
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    63
// some convenience for typing in regular expressions
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    64
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    65
def charlist2rexp(s : List[Char]): Rexp = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    66
  case Nil => ONE
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    67
  case c::Nil => CHAR(c)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    68
  case c::s => SEQ(CHAR(c), charlist2rexp(s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    69
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    70
implicit def string2rexp(s : String) : Rexp = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    71
  charlist2rexp(s.toList)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    72
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    73
implicit def RexpOps(r: Rexp) = new {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    74
  def | (s: Rexp) = ALTS(r, s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    75
  def % = STAR(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    76
  def ~ (s: Rexp) = SEQ(r, s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    77
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    78
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    79
implicit def stringOps(s: String) = new {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    80
  def | (r: Rexp) = ALTS(s, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    81
  def | (r: String) = ALTS(s, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    82
  def % = STAR(s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    83
  def ~ (r: Rexp) = SEQ(s, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    84
  def ~ (r: String) = SEQ(s, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    85
  def $ (r: Rexp) = RECD(s, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    86
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    87
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    88
def nullable(r: Rexp) : Boolean = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    89
  case ZERO => false
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    90
  case ONE => true
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    91
  case CHAR(_) => false
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    92
  case ANYCHAR => false
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    93
  case ALTS(r1, r2) => nullable(r1) || nullable(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    94
  case SEQ(r1, r2) => nullable(r1) && nullable(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    95
  case STAR(_) => true
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    96
  case RECD(_, r1) => nullable(r1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    97
  case NTIMES(n, r) => if (n == 0) true else nullable(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    98
  case OPTIONAL(r) => true
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
    99
  case NOT(r) => !nullable(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   100
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   101
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   102
def der(c: Char, r: Rexp) : Rexp = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   103
  case ZERO => ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   104
  case ONE => ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   105
  case CHAR(d) => if (c == d) ONE else ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   106
  case ANYCHAR => ONE 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   107
  case ALTS(r1, r2) => ALTS(der(c, r1), der(c, r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   108
  case SEQ(r1, r2) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   109
    if (nullable(r1)) ALTS(SEQ(der(c, r1), r2), der(c, r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   110
    else SEQ(der(c, r1), r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   111
  case STAR(r) => SEQ(der(c, r), STAR(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   112
  case RECD(_, r1) => der(c, r1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   113
  case NTIMES(n, r) => if(n > 0) SEQ(der(c, r), NTIMES(n - 1, r)) else ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   114
  case OPTIONAL(r) => der(c, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   115
  case NOT(r) =>  NOT(der(c, r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   116
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   117
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   118
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   119
// extracts a string from a value
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   120
def flatten(v: Val) : String = v match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   121
  case Empty => ""
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   122
  case Chr(c) => c.toString
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   123
  case Left(v) => flatten(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   124
  case Right(v) => flatten(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   125
  case Sequ(v1, v2) => flatten(v1) ++ flatten(v2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   126
  case Stars(vs) => vs.map(flatten).mkString
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   127
  case Ntime(vs) => vs.map(flatten).mkString
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   128
  case Optionall(v) => flatten(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   129
  case Rec(_, v) => flatten(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   130
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   131
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   132
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   133
// extracts an environment from a value;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   134
// used for tokenising a string
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   135
def env(v: Val) : List[(String, String)] = v match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   136
  case Empty => Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   137
  case Chr(c) => Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   138
  case Left(v) => env(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   139
  case Right(v) => env(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   140
  case Sequ(v1, v2) => env(v1) ::: env(v2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   141
  case Stars(vs) => vs.flatMap(env)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   142
  case Ntime(vs) => vs.flatMap(env)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   143
  case Rec(x, v) => (x, flatten(v))::env(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   144
  case Optionall(v) => env(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   145
  case Nots(s) => ("Negative", s) :: Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   146
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   147
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   148
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   149
// The injection and mkeps part of the lexer
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   150
//===========================================
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   151
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   152
def mkeps(r: Rexp) : Val = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   153
  case ONE => Empty
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   154
  case ALTS(r1, r2) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   155
    if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   156
  case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   157
  case STAR(r) => Stars(Nil)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   158
  case RECD(x, r) => Rec(x, mkeps(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   159
  case NTIMES(n, r) => Ntime(List.fill(n)(mkeps(r)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   160
  case OPTIONAL(r) => Optionall(Empty)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   161
  case NOT(rInner) => if(nullable(rInner)) throw new Exception("error")  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   162
                         else Nots("")//Nots(s.reverse.toString)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   163
//   case NOT(ZERO) => Empty
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   164
//   case NOT(CHAR(c)) => Empty
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   165
//   case NOT(SEQ(r1, r2)) => Sequ(mkeps(NOT(r1)), mkeps(NOT(r2)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   166
//   case NOT(ALTS(r1, r2)) => if(!nullable(r1)) Left(mkeps(NOT(r1))) else Right(mkeps(NOT(r2)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   167
//   case NOT(STAR(r)) => Stars(Nil) 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   168
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   169
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   170
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   171
def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   172
  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   173
  case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   174
  case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   175
  case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   176
  case (ALTS(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   177
  case (ALTS(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   178
  case (CHAR(d), Empty) => Chr(c) 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   179
  case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   180
  case (NTIMES(n, r), Sequ(v1, Ntime(vs))) => Ntime(inj(r, c, v1)::vs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   181
  case (OPTIONAL(r), v) => Optionall(inj(r, c, v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   182
  case (NOT(r), Nots(s)) => Nots(c.toString ++ s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   183
  case (ANYCHAR, Empty) => Chr(c)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   184
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   185
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   186
// some "rectification" functions for simplification
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   187
def F_ID(v: Val): Val = v
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   188
def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   189
def F_LEFT(f: Val => Val) = (v:Val) => Left(f(v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   190
def F_ALT(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   191
  case Right(v) => Right(f2(v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   192
  case Left(v) => Left(f1(v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   193
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   194
def F_SEQ(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   195
  case Sequ(v1, v2) => Sequ(f1(v1), f2(v2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   196
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   197
def F_SEQ_Empty1(f1: Val => Val, f2: Val => Val) = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   198
  (v:Val) => Sequ(f1(Empty), f2(v))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   199
def F_SEQ_Empty2(f1: Val => Val, f2: Val => Val) = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   200
  (v:Val) => Sequ(f1(v), f2(Empty))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   201
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   202
def F_ERROR(v: Val): Val = throw new Exception("error")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   203
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   204
// simplification
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   205
def simp(r: Rexp): (Rexp, Val => Val) = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   206
  case ALTS(r1, r2) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   207
    val (r1s, f1s) = simp(r1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   208
    val (r2s, f2s) = simp(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   209
    (r1s, r2s) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   210
      case (ZERO, _) => (r2s, F_RIGHT(f2s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   211
      case (_, ZERO) => (r1s, F_LEFT(f1s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   212
      case _ => if (r1s == r2s) (r1s, F_LEFT(f1s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   213
                else (ALTS (r1s, r2s), F_ALT(f1s, f2s)) 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   214
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   215
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   216
  case SEQ(r1, r2) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   217
    val (r1s, f1s) = simp(r1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   218
    val (r2s, f2s) = simp(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   219
    (r1s, r2s) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   220
      case (ZERO, _) => (ZERO, F_ERROR)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   221
      case (_, ZERO) => (ZERO, F_ERROR)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   222
      case (ONE, _) => (r2s, F_SEQ_Empty1(f1s, f2s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   223
      case (_, ONE) => (r1s, F_SEQ_Empty2(f1s, f2s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   224
      case _ => (SEQ(r1s,r2s), F_SEQ(f1s, f2s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   225
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   226
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   227
  case r => (r, F_ID)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   228
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   229
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   230
// lexing functions including simplification
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   231
def lex_simp(r: Rexp, s: List[Char]) : Val = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   232
  case Nil => if (nullable(r)) mkeps(r) else 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   233
    { throw new Exception(s"lexing error $r not nullable") } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   234
  case c::cs => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   235
    val (r_simp, f_simp) = simp(der(c, r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   236
    inj(r, c, f_simp(lex_simp(r_simp, cs)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   237
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   238
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   239
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   240
def lexing_simp(r: Rexp, s: String) = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   241
  env(lex_simp(r, s.toList))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   242
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   243
// The Lexing Rules for the WHILE Language
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   244
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   245
def PLUS(r: Rexp) = r ~ r.%
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   246
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   247
def Range(s : List[Char]) : Rexp = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   248
  case Nil => ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   249
  case c::Nil => CHAR(c)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   250
  case c::s => ALTS(CHAR(c), Range(s))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   251
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   252
def RANGE(s: String) = Range(s.toList)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   253
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   254
val SYM = RANGE("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz_")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   255
val DIGIT = RANGE("0123456789")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   256
val ID = SYM ~ (SYM | DIGIT).% 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   257
val NUM = PLUS(DIGIT)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   258
val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   259
val SEMI: Rexp = ";"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   260
val OP: Rexp = ":=" | "=" | "-" | "+" | "*" | "!=" | "<" | ">"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   261
val WHITESPACE = PLUS(" " | "\n" | "\t" | "\r")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   262
val RPAREN: Rexp = "{"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   263
val LPAREN: Rexp = "}"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   264
val STRING: Rexp = "\"" ~ SYM.% ~ "\""
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   265
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   266
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   267
//ab \ a --> 1b
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   268
//
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   269
val WHILE_REGS = (("k" $ KEYWORD) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   270
                  ("i" $ ID) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   271
                  ("o" $ OP) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   272
                  ("n" $ NUM) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   273
                  ("s" $ SEMI) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   274
                  ("str" $ STRING) |
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   275
                  ("p" $ (LPAREN | RPAREN)) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   276
                  ("w" $ WHITESPACE)).%
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   277
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   278
val NREGS = NTIMES(5, OPTIONAL(SYM))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   279
val NREGS1 = ("test" $ NREGS)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   280
// Two Simple While Tests
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   281
//========================
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   282
val NOTREG = "hehe" ~ NOT((ANYCHAR.%) ~ "haha" ~ (ANYCHAR.%))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   283
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   284
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   285
  // bnullable function: tests whether the aregular 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   286
  // expression can recognise the empty string
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   287
def bnullable (r: ARexp) : Boolean = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   288
    case AZERO => false
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   289
    case AONE(_) => true
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   290
    case ACHAR(_,_) => false
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   291
    case AALTS(_, rs) => rs.exists(bnullable)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   292
    case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   293
    case ASTAR(_, _) => true
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   294
    case ANOT(_, rn) => !bnullable(rn)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   295
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   296
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   297
def mkepsBC(r: ARexp) : Bits = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   298
    case AONE(bs) => bs
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   299
    case AALTS(bs, rs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   300
      val n = rs.indexWhere(bnullable)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   301
      bs ++ mkepsBC(rs(n))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   302
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   303
    case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   304
    case ASTAR(bs, r) => bs ++ List(Z)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   305
    case ANOT(bs, rn) => bs
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   306
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   307
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   308
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   309
def bder(c: Char, r: ARexp) : ARexp = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   310
    case AZERO => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   311
    case AONE(_) => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   312
    case ACHAR(bs, f) => if (c == f) AONE(bs) else AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   313
    case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   314
    case ASEQ(bs, r1, r2) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   315
      if (bnullable(r1)) AALTS(bs, ASEQ(Nil, bder(c, r1), r2) :: fuse(mkepsBC(r1), bder(c, r2)) :: Nil )
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   316
      else ASEQ(bs, bder(c, r1), r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   317
    case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   318
    case ANOT(bs, rn) => ANOT(bs, bder(c, rn))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   319
    case AANYCHAR(bs) => AONE(bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   320
  } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   321
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   322
def fuse(bs: Bits, r: ARexp) : ARexp = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   323
    case AZERO => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   324
    case AONE(cs) => AONE(bs ++ cs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   325
    case ACHAR(cs, f) => ACHAR(bs ++ cs, f)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   326
    case AALTS(cs, rs) => AALTS(bs ++ cs, rs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   327
    case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   328
    case ASTAR(cs, r) => ASTAR(bs ++ cs, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   329
    case ANOT(cs, r) => ANOT(bs ++ cs, r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   330
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   331
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   332
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   333
def internalise(r: Rexp) : ARexp = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   334
    case ZERO => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   335
    case ONE => AONE(Nil)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   336
    case CHAR(c) => ACHAR(Nil, c)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   337
    //case PRED(f) => APRED(Nil, f)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   338
    case ALTS(r1, r2) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   339
      AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   340
    // case ALTS(r1::rs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   341
    //   val AALTS(Nil, rs2) = internalise(ALTS(rs))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   342
    //   AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   343
    // }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   344
    case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   345
    case STAR(r) => ASTAR(Nil, internalise(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   346
    case RECD(x, r) => internalise(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   347
    case NOT(r) => ANOT(Nil, internalise(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   348
    case ANYCHAR => AANYCHAR(Nil)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   349
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   350
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   351
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   352
def bsimp(r: ARexp): ARexp = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   353
  {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   354
    r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   355
      case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   356
          case (AZERO, _) => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   357
          case (_, AZERO) => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   358
          case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   359
          case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   360
      }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   361
      case AALTS(bs1, rs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   362
            val rs_simp = rs.map(bsimp(_))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   363
            val flat_res = flats(rs_simp)
409
Chengsong
parents: 403
diff changeset
   364
            val dist_res = distinctBy(flat_res, erase)//strongDB(flat_res)//distinctBy(flat_res, erase)
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   365
            dist_res match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   366
              case Nil => AZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   367
              case s :: Nil => fuse(bs1, s)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   368
              case rs => AALTS(bs1, rs)  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   369
            }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   370
          
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   371
      }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   372
      case r => r
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   373
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   374
  }
409
Chengsong
parents: 403
diff changeset
   375
  def strongBsimp(r: ARexp): ARexp =
Chengsong
parents: 403
diff changeset
   376
  {
Chengsong
parents: 403
diff changeset
   377
    r match {
Chengsong
parents: 403
diff changeset
   378
      case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(r2)) match {
Chengsong
parents: 403
diff changeset
   379
          case (AZERO, _) => AZERO
Chengsong
parents: 403
diff changeset
   380
          case (_, AZERO) => AZERO
Chengsong
parents: 403
diff changeset
   381
          case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
Chengsong
parents: 403
diff changeset
   382
          case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
Chengsong
parents: 403
diff changeset
   383
      }
Chengsong
parents: 403
diff changeset
   384
      case AALTS(bs1, rs) => {
Chengsong
parents: 403
diff changeset
   385
            val rs_simp = rs.map(strongBsimp(_))
Chengsong
parents: 403
diff changeset
   386
            val flat_res = flats(rs_simp)
412
Chengsong
parents: 409
diff changeset
   387
            val dist_res = distinctBy2(flat_res)//distinctBy(flat_res, erase)
409
Chengsong
parents: 403
diff changeset
   388
            dist_res match {
Chengsong
parents: 403
diff changeset
   389
              case Nil => AZERO
Chengsong
parents: 403
diff changeset
   390
              case s :: Nil => fuse(bs1, s)
Chengsong
parents: 403
diff changeset
   391
              case rs => AALTS(bs1, rs)  
Chengsong
parents: 403
diff changeset
   392
            }
Chengsong
parents: 403
diff changeset
   393
          
Chengsong
parents: 403
diff changeset
   394
      }
Chengsong
parents: 403
diff changeset
   395
      case r => r
Chengsong
parents: 403
diff changeset
   396
    }
Chengsong
parents: 403
diff changeset
   397
  }
Chengsong
parents: 403
diff changeset
   398
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   399
  def bders (s: List[Char], r: ARexp) : ARexp = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   400
    case Nil => r
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   401
    case c::s => bders(s, bder(c, r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   402
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   404
  def flats(rs: List[ARexp]): List[ARexp] = rs match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   405
      case Nil => Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   406
      case AZERO :: rs1 => flats(rs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   407
      case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   408
      case r1 :: rs2 => r1 :: flats(rs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   409
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   410
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   411
  def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   412
    case Nil => Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   413
    case (x::xs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   414
      val res = f(x)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   415
      if (acc.contains(res)) distinctBy(xs, f, acc)  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   416
      else x::distinctBy(xs, f, res::acc)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   417
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   418
  } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   419
412
Chengsong
parents: 409
diff changeset
   420
  def projectFirstChild(rs: List[ARexp]) : List[ARexp] = rs match {
Chengsong
parents: 409
diff changeset
   421
    case (ASEQ(bs, r1, r2p)::rs1) => r1::projectFirstChild(rs1)
Chengsong
parents: 409
diff changeset
   422
    case Nil => Nil
Chengsong
parents: 409
diff changeset
   423
  }
Chengsong
parents: 409
diff changeset
   424
Chengsong
parents: 409
diff changeset
   425
Chengsong
parents: 409
diff changeset
   426
  def distinctBy2(xs: List[ARexp], acc: List[Rexp] = Nil): List[ARexp] = xs match {
Chengsong
parents: 409
diff changeset
   427
    case Nil => Nil
Chengsong
parents: 409
diff changeset
   428
    case (x::xs) => {
Chengsong
parents: 409
diff changeset
   429
      val res = erase(x)
Chengsong
parents: 409
diff changeset
   430
      if(acc.contains(res))
Chengsong
parents: 409
diff changeset
   431
        distinctBy2(xs, acc)
Chengsong
parents: 409
diff changeset
   432
      else
Chengsong
parents: 409
diff changeset
   433
        x match {
Chengsong
parents: 409
diff changeset
   434
          case ASEQ(bs0, AALTS(bs1, rs), r2) => 
Chengsong
parents: 409
diff changeset
   435
            val newTerms =  distinctBy2(rs.map(r1 => ASEQ(Nil, r1, r2)), acc)
Chengsong
parents: 409
diff changeset
   436
            val rsPrime = projectFirstChild(newTerms)
Chengsong
parents: 409
diff changeset
   437
            newTerms match {
Chengsong
parents: 409
diff changeset
   438
              case Nil => distinctBy2(xs, acc)
Chengsong
parents: 409
diff changeset
   439
              case t::Nil => ASEQ(bs0, fuse(bs1, rsPrime.head), r2)::distinctBy2(xs, erase(t)::acc)
Chengsong
parents: 409
diff changeset
   440
              case ts => ASEQ(bs0, AALTS(bs1, rsPrime), r2)::distinctBy2(xs, newTerms.map(erase(_)):::acc)
Chengsong
parents: 409
diff changeset
   441
            }
Chengsong
parents: 409
diff changeset
   442
          case x => x::distinctBy2(xs, res::acc)
Chengsong
parents: 409
diff changeset
   443
        }
Chengsong
parents: 409
diff changeset
   444
    }
Chengsong
parents: 409
diff changeset
   445
  } 
Chengsong
parents: 409
diff changeset
   446
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   447
  def prettyRexp(r: Rexp) : String = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   448
      case STAR(r0) => s"${prettyRexp(r0)}*"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   449
      case SEQ(CHAR(c), r2) => c.toString ++ prettyRexp(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   450
      case SEQ(r1, r2) => s"${prettyRexp(r1)}~${prettyRexp(r2)}"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   451
      case CHAR(c) => c.toString
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   452
      case ANYCHAR => "."
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   453
    //   case NOT(r0) => s
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   454
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   455
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   456
  def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   457
    case (ONE, bs) => (Empty, bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   458
    case (CHAR(f), bs) => (Chr(f), bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   459
    case (ALTS(r1, r2), Z::bs1) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   460
        val (v, bs2) = decode_aux(r1, bs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   461
        (Left(v), bs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   462
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   463
    case (ALTS(r1, r2), S::bs1) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   464
        val (v, bs2) = decode_aux(r2, bs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   465
        (Right(v), bs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   466
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   467
    case (SEQ(r1, r2), bs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   468
      val (v1, bs1) = decode_aux(r1, bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   469
      val (v2, bs2) = decode_aux(r2, bs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   470
      (Sequ(v1, v2), bs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   471
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   472
    case (STAR(r1), S::bs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   473
      val (v, bs1) = decode_aux(r1, bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   474
      //println(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   475
      val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   476
      (Stars(v::vs), bs2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   477
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   478
    case (STAR(_), Z::bs) => (Stars(Nil), bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   479
    case (RECD(x, r1), bs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   480
      val (v, bs1) = decode_aux(r1, bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   481
      (Rec(x, v), bs1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   482
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   483
    case (NOT(r), bs) => (Nots(prettyRexp(r)), bs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   484
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   485
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   486
  def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   487
    case (v, Nil) => v
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   488
    case _ => throw new Exception("Not decodable")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   489
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   490
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   491
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   492
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   493
def blexSimp(r: Rexp, s: String) : List[Bit] = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   494
    blex_simp(internalise(r), s.toList)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   495
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   496
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   497
def blexing_simp(r: Rexp, s: String) : Val = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   498
    val bit_code = blex_simp(internalise(r), s.toList)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   499
    decode(r, bit_code)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   500
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   501
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   502
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   503
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   504
  def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   505
    case Nil => r
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   506
    case c::s => bders_simp(s, bsimp(bder(c, r)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   507
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   508
  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   509
  def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   510
412
Chengsong
parents: 409
diff changeset
   511
  def bders_simpS(s: List[Char], r: ARexp) : ARexp = s match {
Chengsong
parents: 409
diff changeset
   512
    case Nil => r 
Chengsong
parents: 409
diff changeset
   513
    case c::s => bders_simpS(s, strongBsimp(bder(c, r)))
Chengsong
parents: 409
diff changeset
   514
  }
Chengsong
parents: 409
diff changeset
   515
Chengsong
parents: 409
diff changeset
   516
  def bdersSimpS(s: String, r: Rexp) : ARexp = bders_simpS(s.toList, internalise(r))
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   517
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   518
  def erase(r:ARexp): Rexp = r match{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   519
    case AZERO => ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   520
    case AONE(_) => ONE
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   521
    case ACHAR(bs, c) => CHAR(c)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   522
    case AALTS(bs, Nil) => ZERO
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   523
    case AALTS(bs, a::Nil) => erase(a)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   524
    case AALTS(bs, a::as) => ALTS(erase(a), erase(AALTS(bs, as)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   525
    case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   526
    case ASTAR(cs, r)=> STAR(erase(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   527
    case ANOT(bs, r) => NOT(erase(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   528
    case AANYCHAR(bs) => ANYCHAR
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   529
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   530
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   531
def breakHead(r: ARexp) : List[ARexp] = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   532
    case AALTS(bs, rs) => rs
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   533
    case r => r::Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   534
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   535
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   536
def distinctByWithAcc[B, C](xs: List[B], f: B => C, 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   537
    acc: List[C] = Nil, accB: List[B] = Nil): (List[B], List[C]) = xs match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   538
    case Nil => (accB.reverse, acc)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   539
    case (x::xs) => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   540
      val res = f(x)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   541
      if (acc.contains(res)) distinctByWithAcc(xs, f, acc, accB)  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   542
      else distinctByWithAcc(xs, f, res::acc, x::accB)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   543
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   544
  } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   545
412
Chengsong
parents: 409
diff changeset
   546
//(r1+r2)r + (r2'+r3)r' ~> (r1+r2)r + (r3)r' (erase r = erase r') (erase r2 = erase r2')
Chengsong
parents: 409
diff changeset
   547
//s = s1@s2 \in L R  s1 \in L r2 s2 \in L r
Chengsong
parents: 409
diff changeset
   548
//s = s3@s4  s3 \in L r1 s4 \in L r |s3| < |s1| \nexists s3' s4' s.t. s3'@s4' = s and s3' \in L r1 s4' \in L r
Chengsong
parents: 409
diff changeset
   549
//(r1+r4)r ~> r1r +_usedToBeSeq r4r 
Chengsong
parents: 409
diff changeset
   550
// | ss7:  "erase a01 = erase a02 ∧ (distinctBy as2 erase (set (map erase as1)) = as2p)  ⟹ 
Chengsong
parents: 409
diff changeset
   551
//         (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2) (ASTAR bs02 a02)]@rsc)  s↝
Chengsong
parents: 409
diff changeset
   552
//         (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2p) (ASTAR bs02 a02)]@rsc)"
Chengsong
parents: 409
diff changeset
   553
// | ss8:  "erase a01 = erase a02 ∧ (distinctBy [a2] erase (set (map erase as1)) = [])  ⟹ 
Chengsong
parents: 409
diff changeset
   554
//         (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs a2 (ASTAR bs02 a02)]@rsc) s↝                                                
Chengsong
parents: 409
diff changeset
   555
//         (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@rsc)"
Chengsong
parents: 409
diff changeset
   556
// | ss9:  "erase a01 = erase a02 ∧ (distinctBy as2 erase {erase a1} = as2p)  ⟹ 
Chengsong
parents: 409
diff changeset
   557
//         (rsa@[ASEQ bs a1 (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2) (ASTAR bs02 a02)]@rsc) s↝ 
Chengsong
parents: 409
diff changeset
   558
//         (rsa@[ASEQ bs a1 (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2p) (ASTAR bs02 a02)]@rsc)"
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   559
412
Chengsong
parents: 409
diff changeset
   560
Chengsong
parents: 409
diff changeset
   561
//# of top-level terms
Chengsong
parents: 409
diff changeset
   562
//      r1r2 -> r11r2 + r12 -> r21r2 + r22 + r12' -> 4 terms -> 5 terms -> 6..........
Chengsong
parents: 409
diff changeset
   563
// if string long enough --> #| r1r2 \s s | > unbounded? No ->  #| r1r2 \s s | <  #| pders UNIV r1| + #|pders UNIV r2| <= awidth r1r2
Chengsong
parents: 409
diff changeset
   564
//r* -> r1r* -> r21r* + r22r* -> 4 terms -> 8 terms..............
409
Chengsong
parents: 403
diff changeset
   565
  def strongDB(xs: List[ARexp], 
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   566
                       acc1: List[Rexp] = Nil, 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   567
                       acc2 : List[(List[Rexp], Rexp)] = Nil): List[ARexp] = xs match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   568
    case Nil => Nil
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   569
    case (x::xs) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   570
        if(acc1.contains(erase(x)))
409
Chengsong
parents: 403
diff changeset
   571
            strongDB(xs, acc1, acc2)
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   572
        else{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   573
            x match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   574
                case ASTAR(bs0, r0) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   575
                    val headList : List[ARexp] = List[ARexp](AONE(Nil))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   576
                    val i = acc2.indexWhere(
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   577
                        r2stl => {val (r2s, tl) = r2stl; tl == erase(r0) } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   578
                    )
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   579
                    if(i == -1){ 
409
Chengsong
parents: 403
diff changeset
   580
                        x::strongDB(
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   581
                            xs, erase(x)::acc1, (ONE::Nil, erase(r0))::acc2
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   582
                        )
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   583
                    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   584
                    else{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   585
                        val headListAlready = acc2(i)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   586
                        val (newHeads, oldHeadsUpdated) = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   587
                                distinctByWithAcc(headList, erase, headListAlready._1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   588
                        newHeads match{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   589
                            case newHead::Nil =>
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   590
                                ASTAR(bs0, r0) :: 
409
Chengsong
parents: 403
diff changeset
   591
                                strongDB(xs, erase(x)::acc1, 
412
Chengsong
parents: 409
diff changeset
   592
                                acc2.updated(i, (oldHeadsUpdated, headListAlready._2)) )
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   593
                            case Nil =>
409
Chengsong
parents: 403
diff changeset
   594
                                strongDB(xs, erase(x)::acc1, 
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   595
                                acc2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   596
                        }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   597
                    }                
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   598
                case ASEQ(bs, r1, ASTAR(bs0, r0)) => 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   599
                    val headList = breakHead(r1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   600
                    val i = acc2.indexWhere(
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   601
                        r2stl => {val (r2s, tl) = r2stl; tl == erase(r0) } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   602
                    )
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   603
                    if(i == -1){ 
409
Chengsong
parents: 403
diff changeset
   604
                        x::strongDB(
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   605
                            xs, erase(x)::acc1, (headList.map(erase(_)), erase(r0))::acc2
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   606
                        )
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   607
                    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   608
                    else{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   609
                        val headListAlready = acc2(i)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   610
                        val (newHeads, oldHeadsUpdated) = 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   611
                                distinctByWithAcc(headList, erase, headListAlready._1)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   612
                        newHeads match{
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   613
                            case newHead::Nil =>
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   614
                                ASEQ(bs, newHead, ASTAR(bs0, r0)) :: 
409
Chengsong
parents: 403
diff changeset
   615
                                strongDB(xs, erase(x)::acc1, 
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   616
                                acc2.updated(i, (oldHeadsUpdated, headListAlready._2)) )//TODO: acc2 already contains headListAlready
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   617
                            case Nil =>
409
Chengsong
parents: 403
diff changeset
   618
                                strongDB(xs, erase(x)::acc1, 
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   619
                                acc2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   620
                            case hds => val AALTS(bsp, rsp) = r1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   621
                                ASEQ(bs, AALTS(bsp, hds), ASTAR(bs0, r0)) ::
409
Chengsong
parents: 403
diff changeset
   622
                                strongDB(xs, erase(x)::acc1,
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   623
                                acc2.updated(i, (oldHeadsUpdated, headListAlready._2)))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   624
                        }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   625
                    }
409
Chengsong
parents: 403
diff changeset
   626
                case rPrime => x::strongDB(xs, erase(x)::acc1, acc2)    
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   627
            }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   628
                
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   629
        }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   630
    
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   631
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   632
412
Chengsong
parents: 409
diff changeset
   633
def shortRexpOutput(r: Rexp) : String = r match {
Chengsong
parents: 409
diff changeset
   634
    case CHAR(c) => c.toString
Chengsong
parents: 409
diff changeset
   635
    case ONE => "1"
Chengsong
parents: 409
diff changeset
   636
    case ZERO => "0"
Chengsong
parents: 409
diff changeset
   637
    case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
Chengsong
parents: 409
diff changeset
   638
    case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
Chengsong
parents: 409
diff changeset
   639
    case STAR(r) => "[" ++ shortRexpOutput(r) ++ "]*"
Chengsong
parents: 409
diff changeset
   640
    //case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
Chengsong
parents: 409
diff changeset
   641
    //case RTOP => "RTOP"
Chengsong
parents: 409
diff changeset
   642
  }
Chengsong
parents: 409
diff changeset
   643
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   644
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   645
def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   646
    case Nil => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   647
      if (bnullable(r)) {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   648
        //println(asize(r))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   649
        val bits = mkepsBC(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   650
        bits
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   651
      }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   652
    else throw new Exception("Not matched")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   653
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   654
    case c::cs => {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   655
      val der_res = bder(c,r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   656
      val simp_res = bsimp(der_res)  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   657
      blex_simp(simp_res, cs)      
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   658
    }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   659
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   660
  def size(r: Rexp) : Int = r match {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   661
    case ZERO => 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   662
    case ONE => 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   663
    case CHAR(_) => 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   664
    case ANYCHAR => 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   665
    case NOT(r0) => 1 + size(r0)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   666
    case SEQ(r1, r2) => 1 + size(r1) + size(r2)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   667
    case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   668
    case STAR(r) => 1 + size(r)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   669
  }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   670
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   671
  def asize(a: ARexp) = size(erase(a))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   672
412
Chengsong
parents: 409
diff changeset
   673
//pder related
Chengsong
parents: 409
diff changeset
   674
type Mon = (Char, Rexp)
Chengsong
parents: 409
diff changeset
   675
type Lin = Set[Mon]
Chengsong
parents: 409
diff changeset
   676
Chengsong
parents: 409
diff changeset
   677
def dot_prod(rs: Set[Rexp], r: Rexp): Set[Rexp] = r match {
Chengsong
parents: 409
diff changeset
   678
    case ZERO => Set()
Chengsong
parents: 409
diff changeset
   679
    case ONE => rs
Chengsong
parents: 409
diff changeset
   680
    case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
Chengsong
parents: 409
diff changeset
   681
  }
Chengsong
parents: 409
diff changeset
   682
  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: 409
diff changeset
   683
    case ZERO => Set()
Chengsong
parents: 409
diff changeset
   684
    case ONE => l
Chengsong
parents: 409
diff changeset
   685
    case t => l.map( m => m._2 match {case ZERO => m case ONE => (m._1, t) case p => (m._1, SEQ(p, t)) }  )
Chengsong
parents: 409
diff changeset
   686
  }
Chengsong
parents: 409
diff changeset
   687
  def lf(r: Rexp): Lin = r match {
Chengsong
parents: 409
diff changeset
   688
    case ZERO => Set()
Chengsong
parents: 409
diff changeset
   689
    case ONE => Set()
Chengsong
parents: 409
diff changeset
   690
    case CHAR(f) => {
Chengsong
parents: 409
diff changeset
   691
      //val Some(c) = alphabet.find(f) 
Chengsong
parents: 409
diff changeset
   692
      Set((f, ONE))
Chengsong
parents: 409
diff changeset
   693
    }
Chengsong
parents: 409
diff changeset
   694
    case ALTS(r1, r2) => {
Chengsong
parents: 409
diff changeset
   695
      lf(r1 ) ++ lf(r2)
Chengsong
parents: 409
diff changeset
   696
    }
Chengsong
parents: 409
diff changeset
   697
    case STAR(r1) => cir_prod(lf(r1), STAR(r1)) //may try infix notation later......
Chengsong
parents: 409
diff changeset
   698
    case SEQ(r1, r2) =>{
Chengsong
parents: 409
diff changeset
   699
      if (nullable(r1))
Chengsong
parents: 409
diff changeset
   700
        cir_prod(lf(r1), r2) ++ lf(r2)
Chengsong
parents: 409
diff changeset
   701
      else
Chengsong
parents: 409
diff changeset
   702
        cir_prod(lf(r1), r2) 
Chengsong
parents: 409
diff changeset
   703
    }
Chengsong
parents: 409
diff changeset
   704
  }
Chengsong
parents: 409
diff changeset
   705
  def lfs(r: Set[Rexp]): Lin = {
Chengsong
parents: 409
diff changeset
   706
    r.foldLeft(Set[Mon]())((acc, r) => acc ++ lf(r))
Chengsong
parents: 409
diff changeset
   707
  }
Chengsong
parents: 409
diff changeset
   708
Chengsong
parents: 409
diff changeset
   709
  def pder(x: Char, t: Rexp): Set[Rexp] = {
Chengsong
parents: 409
diff changeset
   710
    val lft = lf(t)
Chengsong
parents: 409
diff changeset
   711
    (lft.filter(mon => if(mon._1 == x) true else false)).map(mon => mon._2)
Chengsong
parents: 409
diff changeset
   712
  }
Chengsong
parents: 409
diff changeset
   713
  def pders_single(s: List[Char], t: Rexp) : Set[Rexp] = s match {
Chengsong
parents: 409
diff changeset
   714
    case x::xs => pders(xs, pder(x, t))
Chengsong
parents: 409
diff changeset
   715
    case Nil => Set(t)
Chengsong
parents: 409
diff changeset
   716
  }
Chengsong
parents: 409
diff changeset
   717
  def pders(s: List[Char], ts: Set[Rexp]) : Set[Rexp] = s match {
Chengsong
parents: 409
diff changeset
   718
    case x::xs => pders(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
Chengsong
parents: 409
diff changeset
   719
    case Nil => ts 
Chengsong
parents: 409
diff changeset
   720
  }
Chengsong
parents: 409
diff changeset
   721
  def pderss(ss: List[List[Char]], t: Rexp): Set[Rexp] = ss.foldLeft( Set[Rexp]() )( (acc, s) => pders_single(s, t) ++ acc )
Chengsong
parents: 409
diff changeset
   722
  def pdera(t: Rexp): Set[Rexp] = lf(t).map(mon => mon._2)
Chengsong
parents: 409
diff changeset
   723
  //all implementation of partial derivatives that involve set union are potentially buggy
Chengsong
parents: 409
diff changeset
   724
  //because they don't include the original regular term before they are pdered.
Chengsong
parents: 409
diff changeset
   725
  //now only pderas is fixed.
Chengsong
parents: 409
diff changeset
   726
  def pderas(t: Set[Rexp], d: Int): Set[Rexp] = if(d > 0) pderas(lfs(t).map(mon => mon._2), d - 1) ++ t else lfs(t).map(mon => mon._2) ++ t//repeated application of pderas over the newest set of pders.
Chengsong
parents: 409
diff changeset
   727
  def pderUNIV(r: Rexp) : Set[Rexp] = pderas(Set(r), awidth(r))
Chengsong
parents: 409
diff changeset
   728
  def awidth(r: Rexp) : Int = r match {
Chengsong
parents: 409
diff changeset
   729
    case CHAR(c) => 1
Chengsong
parents: 409
diff changeset
   730
    case SEQ(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents: 409
diff changeset
   731
    case ALTS(r1, r2) => awidth(r1) + awidth(r2)
Chengsong
parents: 409
diff changeset
   732
    case ONE => 0
Chengsong
parents: 409
diff changeset
   733
    case ZERO => 0
Chengsong
parents: 409
diff changeset
   734
    case STAR(r) => awidth(r)
Chengsong
parents: 409
diff changeset
   735
  }
Chengsong
parents: 409
diff changeset
   736
  //def sigma_lf(l: Set[Mon]) : Rexp = ALTS(l.map(mon => SEQ(CHAR(mon._1),mon._2)).toList)
Chengsong
parents: 409
diff changeset
   737
  //def sigma(rs: Set[Rexp]) : Rexp = ALTS(rs.toList)
Chengsong
parents: 409
diff changeset
   738
  def o(r: Rexp) = if (nullable(r)) ONE else ZERO
Chengsong
parents: 409
diff changeset
   739
  //def nlf(t: Rexp) : Rexp = ALTS(List( o(t), sigma_lf(lf(t)) ))
Chengsong
parents: 409
diff changeset
   740
  def pdp(x: Char, r: Rexp) : Set[Rexp] = r match {
Chengsong
parents: 409
diff changeset
   741
    case ZERO => Set[Rexp]()
Chengsong
parents: 409
diff changeset
   742
    case ONE => Set[Rexp]()
Chengsong
parents: 409
diff changeset
   743
    case CHAR(f) => if(x == f) Set(ONE) else Set[Rexp]()
Chengsong
parents: 409
diff changeset
   744
    case ALTS(r1, r2) => pdp(x, r1) ++ pdp(x, r2)
Chengsong
parents: 409
diff changeset
   745
    case STAR(r1) => pdp(x, r).map(a => SEQ(a, STAR(r1)))
Chengsong
parents: 409
diff changeset
   746
    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: 409
diff changeset
   747
  }
Chengsong
parents: 409
diff changeset
   748
  def pdps(s: List[Char], ts: Set[Rexp]): Set[Rexp] = s match {
Chengsong
parents: 409
diff changeset
   749
    case x::xs => pdps(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
Chengsong
parents: 409
diff changeset
   750
    case Nil => ts   
Chengsong
parents: 409
diff changeset
   751
  }
Chengsong
parents: 409
diff changeset
   752
  def pdpss(ss: List[List[Char]], t: Rexp): Set[Rexp] = ss.foldLeft( Set[Rexp]())((acc, s) => pdps(s, Set(t)) ++ acc)
Chengsong
parents: 409
diff changeset
   753
Chengsong
parents: 409
diff changeset
   754
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   755
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   756
// @arg(doc = "small tests")
412
Chengsong
parents: 409
diff changeset
   757
val STARREG = (((STAR("a") | (STAR("aa")) | STAR(STAR("aaa") | STAR("aaaa")) | STAR("aaaaa") | (STAR("aaaaaa")) | STAR("aaaaaaa") | STAR("aaaaaaaa")).%).%).%
Chengsong
parents: 409
diff changeset
   758
//(STAR("a") | ( STAR("aaa")) | STAR("aaaa") | STAR("aaaaa")).%.%.%
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   759
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   760
@main
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   761
def small() = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   762
412
Chengsong
parents: 409
diff changeset
   763
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   764
//   println(lexing_simp(NOTREG, prog0))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   765
//   val v = lex_simp(NOTREG, prog0.toList)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   766
//   println(v)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   767
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   768
//   val d =  (lex_simp(NOTREG, prog0.toList))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   769
//   println(d)
412
Chengsong
parents: 409
diff changeset
   770
  val pderSTAR = pderUNIV(STARREG)
Chengsong
parents: 409
diff changeset
   771
  val refSize = pderSTAR.map(size(_)).sum
Chengsong
parents: 409
diff changeset
   772
  println(refSize)
Chengsong
parents: 409
diff changeset
   773
  for(i <- 10 to 100){
Chengsong
parents: 409
diff changeset
   774
    val prog0 = "a" * i
Chengsong
parents: 409
diff changeset
   775
    println(s"test: $prog0")
Chengsong
parents: 409
diff changeset
   776
    val bd = bdersSimp(prog0, STARREG)//DB
Chengsong
parents: 409
diff changeset
   777
    val sbd = bdersSimpS(prog0, STARREG)//strongDB
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   778
412
Chengsong
parents: 409
diff changeset
   779
Chengsong
parents: 409
diff changeset
   780
    // println(shortRexpOutput(erase(sbd)))
Chengsong
parents: 409
diff changeset
   781
    // println(shortRexpOutput(erase(bd)))
Chengsong
parents: 409
diff changeset
   782
    println("pdersize, original, strongSimp, simp")
Chengsong
parents: 409
diff changeset
   783
    println(refSize, size(STARREG), asize(sbd), asize(bd))
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   784
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   785
    val vres = blexing_simp( STARREG, prog0)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   786
    println(vres)
412
Chengsong
parents: 409
diff changeset
   787
  }
403
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   788
//   println(vs.length)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   789
//   println(vs)
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   790
   
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   791
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   792
  // val prog1 = """read  n; write n"""  
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   793
  // println(s"test: $prog1")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   794
  // println(lexing_simp(WHILE_REGS, prog1))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   795
}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   796
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   797
// // Bigger Tests
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   798
// //==============
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   799
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   800
// // escapes strings and prints them out as "", "\n" and so on
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   801
// def esc(raw: String): String = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   802
//   import scala.reflect.runtime.universe._
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   803
//   Literal(Constant(raw)).toString
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   804
// }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   805
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   806
// def escape(tks: List[(String, String)]) =
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   807
//   tks.map{ case (s1, s2) => (s1, esc(s2))}
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   808
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   809
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   810
// val prog2 = """
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   811
// write "Fib";
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   812
// read n;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   813
// minus1 := 0;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   814
// minus2 := 1;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   815
// while n > 0 do {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   816
//   temp := minus2;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   817
//   minus2 := minus1 + minus2;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   818
//   minus1 := temp;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   819
//   n := n - 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   820
// };
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   821
// write "Result";
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   822
// write minus2
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   823
// """
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   824
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   825
// @arg(doc = "Fibonacci test")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   826
// @main
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   827
// def fib() = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   828
//   println("lexing fib program")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   829
//   println(escape(lexing_simp(WHILE_REGS, prog2)).mkString("\n"))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   830
// }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   831
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   832
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   833
// val prog3 = """
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   834
// start := 1000;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   835
// x := start;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   836
// y := start;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   837
// z := start;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   838
// while 0 < x do {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   839
//  while 0 < y do {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   840
//   while 0 < z do {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   841
//     z := z - 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   842
//   };
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   843
//   z := start;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   844
//   y := y - 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   845
//  };     
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   846
//  y := start;
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   847
//  x := x - 1
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   848
// }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   849
// """
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   850
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   851
// @arg(doc = "Loops test")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   852
// @main
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   853
// def loops() = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   854
//   println("lexing Loops")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   855
//   println(escape(lexing_simp(WHILE_REGS, prog3)).mkString("\n"))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   856
// }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   857
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   858
// @arg(doc = "Email Test")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   859
// @main
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   860
// def email() = {
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   861
//   val lower = "abcdefghijklmnopqrstuvwxyz"
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   862
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   863
//   val NAME = RECD("name", PLUS(RANGE(lower ++ "_.-")))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   864
//   val DOMAIN = RECD("domain", PLUS(RANGE(lower ++ "-")))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   865
//   val RE = RANGE(lower ++ ".")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   866
//   val TOPLEVEL = RECD("top", (RE ~ RE) |
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   867
//                              (RE ~ RE ~ RE) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   868
//                              (RE ~ RE ~ RE ~ RE) | 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   869
//                              (RE ~ RE ~ RE ~ RE ~ RE) |
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   870
//                              (RE ~ RE ~ RE ~ RE ~ RE ~ RE))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   871
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   872
//   val EMAIL = NAME ~ "@" ~ DOMAIN ~ "." ~ TOPLEVEL
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   873
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   874
//   println(lexing_simp(EMAIL, "christian.urban@kcl.ac.uk"))
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   875
// }
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   876
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   877
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   878
// @arg(doc = "All tests.")
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   879
// @main
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   880
// def all() = { small(); fib() ; loops() ; email() } 
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   881
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   882
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   883
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   884
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   885
// runs with amm2 and amm3
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   886
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   887
6291181fad07 blexer1 for size bound with strongDB
Chengsong
parents:
diff changeset
   888