exps/both.scala
author Christian Urban <urbanc@in.tum.de>
Wed, 20 Feb 2019 00:00:30 +0000
changeset 312 8b0b414e71b0
parent 311 8b8db9558ecf
child 314 20a57552d722
permissions -rw-r--r--
added size bounds for partial derivatives
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
import scala.language.implicitConversions    
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
import scala.language.reflectiveCalls
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
import scala.annotation.tailrec   
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
import scala.util.Try
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
def escape(raw: String) : String = {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
  import scala.reflect.runtime.universe._
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  Literal(Constant(raw)).toString
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
def esc2(r: (String, String)) = (escape(r._1), escape(r._2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
  case Nil => Nil
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
  case (x::xs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
    val res = f(x)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
    if (acc.contains(res)) distinctBy(xs, f, acc)  
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
    else x::distinctBy(xs, f, res::acc)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
} 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
abstract class Bit
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
case object Z extends Bit
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
case object S extends Bit
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
case class C(c: Char) extends Bit
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
type Bits = List[Bit]
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
// usual regular expressions
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
abstract class Rexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
case object ZERO extends Rexp
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
case object ONE extends Rexp
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    34
case class PRED(f: Char => Boolean, s: String = "_") extends Rexp 
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
case class ALTS(rs: List[Rexp]) extends Rexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
case class STAR(r: Rexp) extends Rexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
case class RECD(x: String, r: Rexp) extends Rexp
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
// abbreviations
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    42
def CHAR(c: Char) = PRED(_ == c, c.toString)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
def ALT(r1: Rexp, r2: Rexp) = ALTS(List(r1, r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
def PLUS(r: Rexp) = SEQ(r, STAR(r))
312
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
    45
val ANYCHAR = PRED(_ => true, ".")
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
// annotated regular expressions
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
abstract class ARexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
case object AZERO extends ARexp
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
case class AONE(bs: Bits) extends ARexp
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    51
case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
case class ASTAR(bs: Bits, r: ARexp) extends ARexp 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
// abbreviations
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
def AALT(bs: Bits, r1: ARexp, r2: ARexp) = AALTS(bs, List(r1, r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
// values
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
abstract class Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
case object Empty extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
case class Chr(c: Char) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
case class Sequ(v1: Val, v2: Val) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
case class Left(v: Val) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
case class Right(v: Val) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
case class Stars(vs: List[Val]) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
case class Rec(x: String, v: Val) extends Val
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
   
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
// some convenience for typing in regular expressions
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
def charlist2rexp(s : List[Char]): Rexp = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
  case Nil => ONE
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
  case c::Nil => CHAR(c)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
  case c::s => SEQ(CHAR(c), charlist2rexp(s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
implicit def string2rexp(s : String) : Rexp = charlist2rexp(s.toList)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
implicit def RexpOps(r: Rexp) = new {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
  def | (s: Rexp) = ALT(r, s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
  def % = STAR(r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
  def ~ (s: Rexp) = SEQ(r, s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
implicit def stringOps(s: String) = new {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
  def | (r: Rexp) = ALT(s, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
  def | (r: String) = ALT(s, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
  def % = STAR(s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
  def ~ (r: Rexp) = SEQ(s, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
  def ~ (r: String) = SEQ(s, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
  def $ (r: Rexp) = RECD(s, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
    95
// string of a regular expressions - for testing purposes
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    96
def string(r: Rexp): String = r match {
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    97
  case ZERO => "0"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    98
  case ONE => "1"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
    99
  case PRED(_, s) => s
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   100
  case ALTS(rs) => rs.map(string).mkString("[", "|", "]")
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   101
  case SEQ(r1, r2) => s"(${string(r1)} ~ ${string(r2)})"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   102
  case STAR(r) => s"{${string(r)}}*"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   103
  case RECD(x, r) => s"(${x}! ${string(r)})"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   104
}
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   105
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   106
// string of an annotated regular expressions - for testing purposes
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   107
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   108
def astring(a: ARexp): String = a match {
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   109
  case AZERO => "0"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   110
  case AONE(_) => "1"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   111
  case APRED(_, _, s) => s
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   112
  case AALTS(_, rs) => rs.map(astring).mkString("[", "|", "]")
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   113
  case ASEQ(_, r1, r2) => s"(${astring(r1)} ~ ${astring(r2)})"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   114
  case ASTAR(_, r) => s"{${astring(r)}}*"
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   115
}
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   116
 
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   117
306
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   118
//--------------------------------------------------------------
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
// START OF NON-BITCODE PART
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
//
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
// nullable function: tests whether the regular 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
// expression can recognise the empty string
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
def nullable (r: Rexp) : Boolean = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
  case ZERO => false
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
  case ONE => true
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   127
  case PRED(_, _) => false
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
  case ALTS(rs) => rs.exists(nullable)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
  case SEQ(r1, r2) => nullable(r1) && nullable(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
  case STAR(_) => true
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
  case RECD(_, r) => nullable(r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
// derivative of a regular expression w.r.t. a character
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
def der (c: Char, r: Rexp) : Rexp = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
  case ZERO => ZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
  case ONE => ZERO
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   138
  case PRED(f, _) => if (f(c)) ONE else ZERO
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
  case ALTS(List(r1, r2)) => ALTS(List(der(c, r1), der(c, r2)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
  case SEQ(r1, r2) => 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
    if (nullable(r1)) ALTS(List(SEQ(der(c, r1), r2), der(c, r2)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
    else SEQ(der(c, r1), r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
  case STAR(r) => SEQ(der(c, r), STAR(r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
  case RECD(_, r1) => der(c, r1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
def flatten(v: Val) : String = v match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
  case Empty => ""
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
  case Chr(c) => c.toString
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
  case Left(v) => flatten(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
  case Right(v) => flatten(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
  case Sequ(v1, v2) => flatten(v1) + flatten(v2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
  case Stars(vs) => vs.map(flatten).mkString
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
  case Rec(_, v) => flatten(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
// extracts an environment from a value
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
def env(v: Val) : List[(String, String)] = v match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
  case Empty => Nil
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
  case Chr(c) => Nil
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
  case Left(v) => env(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
  case Right(v) => env(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
  case Sequ(v1, v2) => env(v1) ::: env(v2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
  case Stars(vs) => vs.flatMap(env)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
  case Rec(x, v) => (x, flatten(v))::env(v)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
// injection part
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
def mkeps(r: Rexp) : Val = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
  case ONE => Empty
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
  case ALTS(List(r1, r2)) => 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
    if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
  case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
  case STAR(r) => Stars(Nil)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
  case RECD(x, r) => Rec(x, mkeps(r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
  case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
  case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
  case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
  case (ALTS(List(r1, r2)), Left(v1)) => Left(inj(r1, c, v1))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
  case (ALTS(List(r1, r2)), Right(v2)) => Right(inj(r2, c, v2))
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   187
  case (PRED(_, _), Empty) => Chr(c) 
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
  case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
// lexing without simplification
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
def lex(r: Rexp, s: List[Char]) : Val = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
  case Nil => if (nullable(r)) mkeps(r) else throw new Exception("Not matched")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
  case c::cs => inj(r, c, lex(der(c, r), cs))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
def lexing(r: Rexp, s: String) : Val = lex(r, s.toList)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
//println(lexing(("ab" | "ab") ~ ("b" | ONE), "ab"))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
// some "rectification" functions for simplification
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
def F_ID(v: Val): Val = v
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
def F_LEFT(f: Val => Val) = (v:Val) => Left(f(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
def F_ALT(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
  case Right(v) => Right(f2(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
  case Left(v) => Left(f1(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
def F_SEQ(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
  case Sequ(v1, v2) => Sequ(f1(v1), f2(v2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
def F_SEQ_Empty1(f1: Val => Val, f2: Val => Val) = 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
  (v:Val) => Sequ(f1(Empty), f2(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
def F_SEQ_Empty2(f1: Val => Val, f2: Val => Val) = 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
  (v:Val) => Sequ(f1(v), f2(Empty))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
def F_RECD(f: Val => Val) = (v:Val) => v match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
  case Rec(x, v) => Rec(x, f(v))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
def F_ERROR(v: Val): Val = throw new Exception("error")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
// simplification of regular expressions returning also an
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
// rectification function; no simplification under STAR 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
def simp(r: Rexp): (Rexp, Val => Val) = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
  case ALTS(List(r1, r2)) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
    val (r1s, f1s) = simp(r1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
    val (r2s, f2s) = simp(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
    (r1s, r2s) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
      case (ZERO, _) => (r2s, F_RIGHT(f2s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
      case (_, ZERO) => (r1s, F_LEFT(f1s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
      case _ => if (r1s == r2s) (r1s, F_LEFT(f1s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
                else (ALTS(List(r1s, r2s)), F_ALT(f1s, f2s)) 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
    }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
  case SEQ(r1, r2) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
    val (r1s, f1s) = simp(r1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
    val (r2s, f2s) = simp(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
    (r1s, r2s) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
      case (ZERO, _) => (ZERO, F_ERROR)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
      case (_, ZERO) => (ZERO, F_ERROR)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
      case (ONE, _) => (r2s, F_SEQ_Empty1(f1s, f2s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
      case (_, ONE) => (r1s, F_SEQ_Empty2(f1s, f2s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
      case _ => (SEQ(r1s,r2s), F_SEQ(f1s, f2s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
    }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
  case RECD(x, r1) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
    val (r1s, f1s) = simp(r1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
    (RECD(x, r1s), F_RECD(f1s))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
  case r => (r, F_ID)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   252
def ders_simp(s: List[Char], r: Rexp) : Rexp = s match {
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   253
  case Nil => r
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   254
  case c::s => ders_simp(s, simp(der(c, r))._1)
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   255
}
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   256
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   257
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
def lex_simp(r: Rexp, s: List[Char]) : Val = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
  case Nil => if (nullable(r)) mkeps(r) else throw new Exception("Not matched")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
  case c::cs => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
    val (r_simp, f_simp) = simp(der(c, r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
    inj(r, c, f_simp(lex_simp(r_simp, cs)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
306
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   268
//println(lexing_simp(("a" | "ab") ~ ("b" | ""), "ab"))
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   269
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   270
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   271
def tokenise_simp(r: Rexp, s: String) = 
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   272
  env(lexing_simp(r, s)).map(esc2)
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   273
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   274
//--------------------------------------------------------------------
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   275
// Partial Derivatives
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
306
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   278
def pder(c: Char, r: Rexp): Set[Rexp] = r match {
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   279
  case ZERO => Set()
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   280
  case ONE => Set()
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   281
  case PRED(f, _) => if (f(c)) Set(ONE) else Set()
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   282
  case ALTS(rs) => rs.toSet.flatMap(pder(c, _))
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   283
  case SEQ(r1, r2) =>
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   284
    (for (pr1 <- pder(c, r1)) yield SEQ(pr1, r2)) ++
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   285
    (if (nullable(r1)) pder(c, r2) else Set())
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   286
  case STAR(r1) =>
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   287
    for (pr1 <- pder(c, r1)) yield SEQ(pr1, STAR(r1))
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   288
  case RECD(_, r1) => pder(c, r1)
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   289
}
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   290
306
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   291
def pders(cs: List[Char], r: Rexp): Set[Rexp] = cs match {
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   292
  case Nil => Set(r)
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   293
  case c::cs => pder(c, r).flatMap(pders(cs, _))
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   294
}
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   295
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   296
def pders_simp(cs: List[Char], r: Rexp): Set[Rexp] = cs match {
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   297
  case Nil => Set(r)
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   298
  case c::cs => pder(c, r).flatMap(pders_simp(cs, _)).map(simp(_)._1)
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   299
}
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   300
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   301
def psize(rs: Set[Rexp])  = 
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   302
  rs.map(size).sum
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   303
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   304
//--------------------------------------------------------------------
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
// BITCODED PART
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
def fuse(bs: Bits, r: ARexp) : ARexp = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
  case AZERO => AZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
  case AONE(cs) => AONE(bs ++ cs)
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   311
  case APRED(cs, f, s) => APRED(bs ++ cs, f, s)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
  case AALTS(cs, rs) => AALTS(bs ++ cs, rs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
  case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
  case ASTAR(cs, r) => ASTAR(bs ++ cs, r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
// translation into ARexps
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
def internalise(r: Rexp) : ARexp = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
  case ZERO => AZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
  case ONE => AONE(Nil)
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   321
  case PRED(f, s) => APRED(Nil, f, s)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
  case ALTS(List(r1, r2)) => 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
    AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
  case ALTS(r1::rs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
     val AALTS(Nil, rs2) = internalise(ALTS(rs))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
     AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
  case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
  case STAR(r) => ASTAR(Nil, internalise(r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
  case RECD(x, r) => internalise(r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
internalise(("a" | "ab") ~ ("b" | ""))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
// decoding of values from bit sequences
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
  case (ONE, bs) => (Empty, bs)
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   338
  case (PRED(f, _), C(c)::bs) => (Chr(c), bs)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
  case (ALTS(r::Nil), bs) => decode_aux(r, bs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
  case (ALTS(rs), bs) => bs match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
    case Z::bs1 => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
      val (v, bs2) = decode_aux(rs.head, bs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
      (Left(v), bs2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
    }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
    case S::bs1 => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
      val (v, bs2) = decode_aux(ALTS(rs.tail), bs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
      (Right(v), bs2)			
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
    }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
  case (SEQ(r1, r2), bs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
    val (v1, bs1) = decode_aux(r1, bs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
    val (v2, bs2) = decode_aux(r2, bs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
    (Sequ(v1, v2), bs2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
  case (STAR(r1), S::bs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
    val (v, bs1) = decode_aux(r1, bs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
    val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
    (Stars(v::vs), bs2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
  case (STAR(_), Z::bs) => (Stars(Nil), bs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
  case (RECD(x, r1), bs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
    val (v, bs1) = decode_aux(r1, bs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
    (Rec(x, v), bs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   367
def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   368
  case (v, Nil) => v
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
  case _ => throw new Exception("Not decodable")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
//erase function: extracts a Rexp from Arexp
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
def erase(r: ARexp) : Rexp = r match{
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
  case AZERO => ZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
  case AONE(_) => ONE
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   377
  case APRED(bs, f, s) => PRED(f, s)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
  case AALTS(bs, rs) => ALTS(rs.map(erase(_)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
  case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
  case ASTAR(cs, r)=> STAR(erase(r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
// bnullable function: tests whether the aregular 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
// expression can recognise the empty string
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
def bnullable (r: ARexp) : Boolean = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
  case AZERO => false
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   388
  case AONE(_) => true
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   389
  case APRED(_,_,_) => false
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
  case AALTS(_, rs) => rs.exists(bnullable)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   391
  case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
  case ASTAR(_, _) => true
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
def bmkeps(r: ARexp) : Bits = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
  case AONE(bs) => bs
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
  case AALTS(bs, rs) => {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
    val n = rs.indexWhere(bnullable)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
    bs ++ bmkeps(rs(n))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
  case ASEQ(bs, r1, r2) => bs ++ bmkeps(r1) ++ bmkeps(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
  case ASTAR(bs, r) => bs ++ List(Z)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
// derivative of a regular expression w.r.t. a character
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
def bder(c: Char, r: ARexp) : ARexp = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
  case AZERO => AZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
  case AONE(_) => AZERO
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   409
  case APRED(bs, f, _) => if (f(c)) AONE(bs:::List(C(c))) else AZERO
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
  case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
  case ASEQ(bs, r1, r2) => 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
    if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(bmkeps(r1), bder(c, r2)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
    else ASEQ(bs, bder(c, r1), r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
  case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
// derivative w.r.t. a string (iterates bder)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
@tailrec
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
def bders (s: List[Char], r: ARexp) : ARexp = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
  case Nil => r
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
  case c::s => bders(s, bder(c, r))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   425
def flats(rs: List[ARexp]): List[ARexp] = rs match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   426
    case Nil => Nil
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
    case AZERO :: rs1 => flats(rs1)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   428
    case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
    case r1 :: rs2 => r1 :: flats(rs2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   431
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
def bsimp(r: ARexp): ARexp = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   433
  case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   434
      case (AZERO, _) => AZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   435
      case (_, AZERO) => AZERO
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
      case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
      case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   438
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   439
  case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp)), erase) match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   440
    case Nil => AZERO
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   441
    case r :: Nil => fuse(bs1, r)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   442
    case rs => AALTS(bs1, rs)  
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   443
  }
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   444
  //case ASTAR(bs1, r1) => ASTAR(bs1, bsimp(r1))
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   445
  case r => r
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   446
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   447
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   448
def bders_simp (s: List[Char], r: ARexp) : ARexp = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
  case Nil => r
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
  case c::s => bders_simp(s, bsimp(bder(c, r)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   453
def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   454
  case Nil => if (bnullable(r)) bmkeps(r)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
	      else throw new Exception("Not matched")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   456
  case c::cs => blex_simp(bsimp(bder(c, r)), cs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   457
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   458
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   460
def blexing_simp(r: Rexp, s: String) : Val = 
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   461
 decode(r, blex_simp(internalise(r), s.toList))
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   462
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   463
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   464
def btokenise_simp(r: Rexp, s: String) = 
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   465
  env(blexing_simp(r, s)).map(esc2)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   466
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   467
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   469
// INCLUDING SIMPLIFICATION UNDER STARS
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   470
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   471
def bsimp_full(r: ARexp): ARexp = r match {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   472
  case ASEQ(bs1, r1, r2) => (bsimp_full(r1), bsimp_full(r2)) match {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   473
      case (AZERO, _) => AZERO
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   474
      case (_, AZERO) => AZERO
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   475
      case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   476
      case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   477
  }
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   478
  case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp_full)), erase) match {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   479
    case Nil => AZERO
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   480
    case r :: Nil => fuse(bs1, r)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   481
    case rs => AALTS(bs1, rs)  
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   482
  }
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   483
  case ASTAR(bs1, r1) => ASTAR(bs1, bsimp_full(r1))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   484
  case r => r
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   485
}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   486
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   487
def bders_simp_full(s: List[Char], r: ARexp) : ARexp = s match {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   488
  case Nil => r
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   489
  case c::s => bders_simp_full(s, bsimp_full(bder(c, r)))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   490
}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   491
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   492
def blex_simp_full(r: ARexp, s: List[Char]) : Bits = s match {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   493
  case Nil => if (bnullable(r)) bmkeps(r)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   494
	      else throw new Exception("Not matched")
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   495
  case c::cs => blex_simp_full(bsimp_full(bder(c, r)), cs)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   496
}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   497
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   498
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   499
def blexing_simp_full(r: Rexp, s: String) : Val = 
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   500
 decode(r, blex_simp_full(internalise(r), s.toList))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   501
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   502
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   503
def btokenise_simp_full(r: Rexp, s: String) = env(blexing_simp_full(r, s)).map(esc2)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   504
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   505
// bders2 for strings in the ALTS case
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   506
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   507
def bders2_simp(s: List[Char], a: ARexp) : ARexp = {
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   508
  //println(s"s = ${s.length}   a = ${asize(a)}")
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   509
  //Console.readLine
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   510
  (s, a) match {
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   511
  case (Nil, r) => r
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   512
  case (s, AZERO) => AZERO
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   513
  case (s, AONE(_)) => AZERO
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   514
  case (s, APRED(bs, f, _)) => 
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   515
    if (f(s.head) && s.tail == Nil) AONE(bs:::List(C(s.head))) else AZERO
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   516
  case (s, AALTS(bs, rs)) => bsimp(AALTS(bs, rs.map(bders2_simp(s, _)))) 
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   517
  case (c::s, r) => bders2_simp(s, bsimp(bder(c, r)))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   518
}}
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   519
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   520
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   521
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   522
def blexing2_simp(r: Rexp, s: String) : Val = {
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   523
  val bder = bders2_simp(s.toList, internalise(r))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   524
  if (bnullable(bder)) decode(r, bmkeps(bder)) else 
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   525
  throw new Exception("Not matched")
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   526
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   527
}
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   528
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   529
def btokenise2_simp(r: Rexp, s: String) = 
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   530
  env(blexing2_simp(r, s)).map(esc2)
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   531
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   532
312
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   533
// Parser for regexes
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   534
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   535
case class Parser(s: String) {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   536
  var i = 0
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   537
  
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   538
  def peek() = s(i)
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   539
  def eat(c: Char) = 
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   540
    if (c == s(i)) i = i + 1 else throw new Exception("Expected " + c + " got " + s(i))
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   541
  def next() = { i = i + 1; s(i - 1) }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   542
  def more() = s.length - i > 0
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   543
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   544
  def Regex() : Rexp = {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   545
    val t = Term();
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   546
    if (more() && peek() == '|') {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   547
      eat ('|') ; 
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   548
      ALT(t, Regex()) 
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   549
    } 
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   550
    else t
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   551
  }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   552
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   553
  def Term() : Rexp = {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   554
    var f : Rexp = 
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   555
      if (more() && peek() != ')' && peek() != '|') Factor() else ONE;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   556
    while (more() && peek() != ')' && peek() != '|') {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   557
      f = SEQ(f, Factor()) ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   558
    }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   559
    f
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   560
  }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   561
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   562
  def Factor() : Rexp = {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   563
    var b = Base();
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   564
    while (more() && peek() == '*') {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   565
      eat('*') ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   566
      b = STAR(b) ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   567
    }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   568
    while (more() && peek() == '?') {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   569
      eat('?') ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   570
      b = ALT(b, ONE) ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   571
    }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   572
    while (more() && peek() == '+') {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   573
      eat('+') ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   574
      b = SEQ(b, STAR(b)) ;
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   575
    }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   576
    b
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   577
  }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   578
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   579
  def Base() : Rexp = {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   580
    peek() match {
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   581
      case '(' => { eat('(') ; val r = Regex(); eat(')') ; r }   // if groups should be groups RECD("",r) }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   582
      case '.' => { eat('.'); ANYCHAR }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   583
      case _ => CHAR(next())
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   584
    }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   585
  }
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   586
}
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   587
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   588
// two simple examples for the regex parser
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   589
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   590
println("two simple examples for the regex parser")
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   591
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   592
println(string(Parser("a|(bc)*").Regex()))
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   593
println(string(Parser("(a|b)*(babab(a|b)*bab|bba(a|b)*bab)(a|b)*").Regex()))
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   594
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   595
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   596
8b0b414e71b0 added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents: 311
diff changeset
   597
System.exit(0)
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   598
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   599
//   Testing
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   600
//============
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   601
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   602
def time[T](code: => T) = {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   603
  val start = System.nanoTime()
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   604
  val result = code
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   605
  val end = System.nanoTime()
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   606
  ((end - start)/1.0e9).toString
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   607
  //result
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   608
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   609
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   610
def timeR[T](code: => T) = {
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   611
  val start = System.nanoTime()
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   612
  for (i <- 1 to 10) code
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   613
  val result = code
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   614
  val end = System.nanoTime()
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   615
  (result, (end - start))
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   616
}
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   617
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   618
//size: of a Aregx for testing purposes 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   619
def size(r: Rexp) : Int = r match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   620
  case ZERO => 1
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   621
  case ONE => 1
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   622
  case PRED(_,_) => 1
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   623
  case SEQ(r1, r2) => 1 + size(r1) + size(r2)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   624
  case ALTS(rs) => 1 + rs.map(size).sum
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   625
  case STAR(r) => 1 + size(r)
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   626
  case RECD(_, r) => size(r)
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   628
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   629
def asize(a: ARexp) = size(erase(a))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   630
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   631
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   632
// Lexing Rules for a Small While Language
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   633
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   634
//symbols
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   635
val SYM = PRED("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".contains(_), "SYM")
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   636
//digits
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   637
val DIGIT = PRED("0123456789".contains(_), "NUM")
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   638
//identifiers
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   639
val ID = SYM ~ (SYM | DIGIT).% 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   640
//numbers
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   641
val NUM = STAR(DIGIT)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   642
//keywords
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   643
val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   644
//semicolons
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   645
val SEMI: Rexp = ";"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   646
//operators
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   647
val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   648
//whitespaces
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   649
val WHITESPACE = PLUS(" " | "\n" | "\t")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   650
//parentheses
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   651
val RPAREN: Rexp = ")"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   652
val LPAREN: Rexp = "("
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   653
val BEGIN: Rexp = "{"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   654
val END: Rexp = "}"
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   655
//strings...but probably needs not
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   656
val STRING: Rexp = "\"" ~ SYM.% ~ "\""
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   657
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   658
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   659
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   660
val WHILE_REGS = (("k" $ KEYWORD) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   661
                  ("i" $ ID) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   662
                  ("o" $ OP) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   663
                  ("n" $ NUM) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   664
                  ("s" $ SEMI) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   665
                  ("str" $ STRING) |
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   666
                  ("p" $ (LPAREN | RPAREN)) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   667
                  ("b" $ (BEGIN | END)) | 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   668
                  ("w" $ WHITESPACE)).%
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   669
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   670
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   671
// Some Small Tests
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   672
//==================
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   673
307
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   674
println("Small tests")
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   675
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   676
val re1 = STAR("a" | "aa")
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   677
println(astring(bders_simp("".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   678
println(astring(bders_simp("a".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   679
println(astring(bders_simp("aa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   680
println(astring(bders_simp("aaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   681
println(astring(bders_simp("aaaaaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   682
println(astring(bders_simp("aaaaaaaaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   683
println(astring(bders_simp("aaaaaaaaaaaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   684
println(astring(bders_simp("aaaaaaaaaaaaaaaaaaaaaaaaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   685
println(astring(bders_simp("aaaaaabaaaabbbbbaaaaaaaaaaaaaaa".toList, internalise(re1))))
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   686
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   687
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   688
for (i <- 0 to 100 by 5) {
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   689
  //print("Old: " + time(tokenise_simp(re1, "a" * i)))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   690
  print(" Bit: " + time(btokenise_simp(re1, "a" * i)))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   691
  print(" Bit full simp: " + time(btokenise_simp_full(re1, "a" * i)))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   692
  println(" Bit2: " + time(btokenise2_simp(re1, "a" * i)))
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   693
}
307
ee1caac29bb2 updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   694
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   695
Console.readLine
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   696
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   697
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   698
// Bigger Tests
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   699
//==============
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   700
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   701
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   702
println("Big tests")
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   703
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   704
val fib_prog = """
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   705
write "Fib";
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   706
read n;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   707
minus1 := 0;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   708
minus2 := 1;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   709
while n > 0 do {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   710
  temp := minus2;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   711
  minus2 := minus1 + minus2;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   712
  minus1 := temp;
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   713
  n := n - 1
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   714
};
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   715
write "Result";
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   716
write minus2
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   717
"""
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   718
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   719
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   720
println("fib prog tests :")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   721
println(tokenise_simp(WHILE_REGS, fib_prog))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   722
println(btokenise_simp(WHILE_REGS, fib_prog))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   723
println("equal? " + (tokenise_simp(WHILE_REGS, fib_prog) == btokenise_simp(WHILE_REGS, fib_prog)))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   724
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   725
for (i <- 1 to 20) {
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   726
  print("Old: " + time(tokenise_simp(WHILE_REGS, fib_prog * i)))
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   727
  print(" Bit: " + time(btokenise_simp(WHILE_REGS, fib_prog * i)))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   728
  println(" Bit full simp: " + time(btokenise_simp_full(WHILE_REGS, fib_prog * i)))
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   729
  //println(" Bit2: " + time(btokenise2_simp(WHILE_REGS, fib_prog * i)))
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   730
}
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   731
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   732
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   733
println("Original " + size(WHILE_REGS))
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   734
println("Size Bit  " + asize(bders_simp((fib_prog * 1).toList, internalise(WHILE_REGS))))
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   735
println("Size Bitf " + asize(bders_simp_full((fib_prog * 1).toList, internalise(WHILE_REGS))))
311
8b8db9558ecf updated
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
   736
println("Size Bit2 " + asize(bders2_simp((fib_prog * 1).toList, internalise(WHILE_REGS))))
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   737
println("Size Old  " + size(ders_simp((fib_prog * 1).toList, WHILE_REGS)))
306
6756b026c5fe added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents: 305
diff changeset
   738
println("Size Pder " + psize(pders_simp((fib_prog * 1).toList, WHILE_REGS)))
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   739
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   740
System.exit(0)
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   741
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   742
println("Internal sizes test OK or strange")
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   743
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   744
def perc(p1: Double, p2: Double) : String =
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   745
  f"${(((p1 - p2) / p2) * 100.0) }%5.0f" + "%"
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   746
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   747
def ders_test(n: Int, s: List[Char], r: Rexp, a: ARexp) : (Rexp, ARexp) = s match {
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   748
  case Nil => (r, a)
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   749
  case c::s => {
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   750
    // derivative 
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   751
    val (rd1, tr1) = timeR(der(c, r))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   752
    val (ad1, ta1) = timeR(bder(c, a))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   753
    val trs1 = f"${tr1}%.5f"
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   754
    val tas1 = f"${ta1}%.5f"
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   755
    if (tr1 < ta1) println(s"Time strange der  (step) ${n} ${perc(ta1, tr1)} sizes  der ${size(rd1)} ${asize(ad1)}")
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   756
    //simplification
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   757
    val (rd, tr) = timeR(simp(rd1)._1)
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   758
    val (ad, ta) = timeR(bsimp(ad1))
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   759
    val trs = f"${tr}%.5f"
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   760
    val tas = f"${ta}%.5f"
300
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   761
    //full simplification
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   762
    val (adf, taf) = timeR(bsimp_full(ad1))
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   763
    if (tr < ta) println(s"Time strange simp (step) ${n} ${perc(ta, tr)} sizes simp ${size(rd)} ${asize(ad)}")
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   764
    if (n == 1749 || n == 1734) {
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   765
      println{s"Aregex before bder (size: ${asize(a)})\n ${string(erase(a))}"}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   766
      println{s"Aregex after bder (size: ${asize(ad1)})\n ${string(erase(ad1))}"}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   767
      println{s"Aregex after bsimp (size: ${asize(ad)})\n ${string(erase(ad))}"}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   768
      println{s"Aregex after bsimp_full (size: ${asize(adf)})\n ${string(erase(adf))}"}
b7987014fed8 updated
Christian Urban <urbanc@in.tum.de>
parents: 299
diff changeset
   769
    }
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   770
    ders_test(n + 1, s, rd, ad)
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   771
  }
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   772
}
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   773
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   774
val prg = (fib_prog * 10).toList
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   775
ders_test(0, prg, WHILE_REGS, internalise(WHILE_REGS))
298
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   776
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   777
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   778
//testing the two lexings produce the same value
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   779
//enumerates strings of length n over alphabet cs
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   780
def strs(n: Int, cs: String) : Set[String] = {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   781
  if (n == 0) Set("")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   782
  else {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   783
    val ss = strs(n - 1, cs)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   784
    ss ++
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   785
    (for (s <- ss; c <- cs.toList) yield c + s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   786
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   787
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   788
def enum(n: Int, s: String) : Stream[Rexp] = n match {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   789
  case 0 => ZERO #:: ONE #:: s.toStream.map(CHAR)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   790
  case n => {  
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   791
    val rs = enum(n - 1, s)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   792
    rs #:::
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   793
    (for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) #:::
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   794
    (for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) #:::
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   795
    (for (r1 <- rs) yield STAR(r1))
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   796
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   797
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   798
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   799
//tests blexing and lexing
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   800
def tests(ss: Set[String])(r: Rexp) = {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   801
  //println(s"Testing ${r}")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   802
  for (s <- ss.par) yield {
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   803
    val res1 = Try(Some(lexing_simp(r, s))).getOrElse(None)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   804
    val res2 = Try(Some(blexing_simp(r, s))).getOrElse(None)
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   805
    if (res1 != res2) 
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   806
      { println(s"Disagree on ${r} and ${s}")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   807
	println(s"   ${res1} !=  ${res2}")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   808
	Some((r, s)) } else None
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   809
  }
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   810
}
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   811
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   812
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   813
println("Partial searching: ")
db329a4d2bc0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   814
enum(2, "abc").map(tests(strs(3, "abc"))).toSet
299
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   815
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   816
cae7eab03018 added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents: 298
diff changeset
   817
305
6e2cef17a9b3 updated
Christian Urban <urbanc@in.tum.de>
parents: 300
diff changeset
   818