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