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