scala/abacus.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 12:48:43 +0000
changeset 293 8b55240e12c6
parent 222 d682591c63e1
permissions -rw-r--r--
upodated to Isabelle 2016
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
package object abacus {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 195
diff changeset
     3
import scala.annotation.tailrec
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
import lib._
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     6
// Abacus instructions
222
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
     7
sealed abstract class AInst {
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
     8
  def print : String
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
     9
} 
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    10
case class Inc(n: Int) extends AInst {
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    11
  override def print = "Inc(" + n.toString + ")\n"
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    12
}
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    13
case class Dec(n: Int, l: Int) extends AInst {
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    14
  override def print = "Dec(" + n.toString + "," +  l.toString + ")\n"
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    15
}
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    16
case class Goto(l: Int) extends AInst {
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    17
  override def print = "Goto(" + l.toString + ")\n"
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    18
}
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
type AProg = List[AInst]
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
type Regs = Map[Int, Int]
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    23
// Abacus configurations
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
case class AConfig(s: Int, regs: Regs)  
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    26
// Abacus machines
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
case class Abacus(p: AProg) {
222
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
    28
  def print = p.foldLeft[String]("")(_ + _.print)
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    30
  //simple composition
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    31
  def ++ (that: Abacus) = Abacus(p ::: that.p)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    32
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    33
  def :+ (that: Abacus) = this ++ that.shift(p.length, -1)
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
  def shift(offset: Int, jump: Int) = Abacus(p.map(_ match {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
    case Inc(n) => Inc(n)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
    case Dec(n, l) => if (l == jump) Dec(n, l) else Dec(n, l + offset)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
    case Goto(l) => if (l == jump) Goto(l) else Goto(l + offset)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
  }))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
      
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
  def adjust(old_jump: Int, jump: Int) = Abacus(p.map(_ match {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
    case Inc(n) => Inc(n)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
    case Dec(n, l) => if (l == old_jump) Dec(n, jump) else Dec(n, l)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
    case Goto(l) => if (l == old_jump) Goto(jump) else Goto(l)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
  }))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    47
  def step(cf: AConfig) : AConfig = nth_of(p, cf.s) match {
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    48
    case None => cf
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    49
    case Some(Inc(n)) => AConfig(cf.s + 1, cf.regs + (n -> (dget(cf.regs, n) + 1)))
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    50
    case Some(Dec(n, l)) => {
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
      if (dget(cf.regs, n) == 0) AConfig(l, cf.regs)
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    52
      else AConfig(cf.s + 1, cf.regs + (n -> (dget(cf.regs, n) - 1)))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
    }
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    54
    case Some(Goto(l)) => AConfig(l, cf.regs)
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    55
  } 
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
    56
  
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  def steps(cf: AConfig, n: Int) : AConfig = n match {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
    case 0 => cf
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
    case n => steps(step(cf), n - 1)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
  } 
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
  def steps(regs: Regs, n: Int) : AConfig = steps(AConfig(0, regs), n)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 195
diff changeset
    64
  @tailrec
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 195
diff changeset
    65
  final def run(cf: AConfig) : AConfig = {
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
    if (cf.s >= p.length || cf.s < 0) cf else run(step(cf))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
  }
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
 
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
  def run(regs: Regs): Regs = run(AConfig(0, regs)).regs
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    72
// some syntactical convenience
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    73
object Abacus {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    74
  def apply(is: AInst*) : Abacus = Abacus(is.toList)
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    78
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    79