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