scala/comp1.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 13:18:07 +0000
changeset 296 3fee65a40838
parent 271 4457185b22ef
permissions -rw-r--r--
updated to Isabelle 2018
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 comp1 {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     3
// Abacus to TM translation
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     4
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
import lib._
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
import turing._
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
import abacus._
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
     8
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
     9
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
// TMs used in the translation
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    12
val TMInc = TM((WOc, 1), (R, 2), (WOc, 3), (R, 2), (WOc, 3), (R, 4), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    13
               (L, 7), (WBk, 5), (R, 6), (WBk, 5), (WOc, 3), (R, 6),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    14
               (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (WBk, 9))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    16
val TMDec = TM((WOc, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    17
               (R, 5), (WBk, 4), (R, 6), (WBk, 5), (L, 7), (L, 8),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    18
               (L, 11), (WBk, 7), (WOc, 8), (R, 9), (L, 10), (R, 9),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    19
               (R, 5), (WBk, 10), (L, 12), (L, 11), (R, 13), (L, 11),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    20
               (R, 17), (WBk, 13), (L, 15), (L, 14), (R, 16), (L, 14),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    21
               (R, 0), (WBk, 16))
193
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
val TMGoto = TM((Nop, 1), (Nop, 1))
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    24
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    25
val TMMopup_aux = TM((R, 2), (R, 1), (L, 5), (WBk, 3), (R, 4), (WBk, 3),
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    26
                     (R, 2), (WBk, 3), (L, 5), (L, 6), (R, 0), (L, 6))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
def TMFindnth(n: Int) : TM = n match {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
  case 0 => TM(Nil)
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    30
  case n => TMFindnth(n - 1) ++ TM((WOc, 2 * n - 1), (R, 2 * n), (R, 2 * n + 1), (R, 2 * n))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
def TMMopup(n: Int) = {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
  def TMMopup1(n: Int) : TM = n match {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
    case 0 => TM(Nil)
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    36
    case n => TMMopup1(n - 1) ++ TM((R, 2 * n + 1), (WBk, 2 * n), (R, 2 * n - 1), (WOc, 2 * n))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
  }
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    38
  TMMopup1(n) ++ TMMopup_aux.shift(2 * n)
193
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
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    42
// start address of the instructions
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    43
@tailrec
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    44
def layout(p: AProg, sum: Int, out: List[Int]) : List[Int] = p match {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    45
    case Nil => out.reverse
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    46
    case Inc(n)::p => layout(p, 2 * n + 9 + sum, 2 * n + 9 + sum::out) 
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    47
    case Dec(n, _)::p => layout(p, 2 * n + 16 + sum, 2 * n + 16 + sum::out)  
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    48
    case Goto(n)::p => layout(p, 1 + sum, 1 + sum::out) 
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    49
 }
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    50
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    51
def address(layout: List[Int], n: Int) = {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    52
  //println("calculating layout of " + n)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    53
  layout(n) + 1
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    54
}
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
def compile_Inc(s: Int, n: Int) = 
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  TMFindnth(n).shift(s - 1) ++ TMInc.shift(2 * n).shift(s - 1)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
def compile_Dec(s: Int, n: Int, e: Int) = 
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
  TMFindnth(n).shift(s - 1) ++ TMDec.shift(2 * n).shift(s - 1).adjust(e)
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 compile_Goto(s: Int) = TMGoto.shift(s - 1)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    64
@tailrec
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    65
def compile_abc(lay: List[Int], p: AProg, cnt: Int, out: List[TM]): List[TM] = {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    66
  if (cnt % 1000 == 0) println("compile counter of instructions " + cnt);
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    67
p match {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    68
  case Nil => out.reverse
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    69
  case Inc(n)::p => compile_abc(lay, p, cnt + 1, compile_Inc(address(lay, cnt), n)::out)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    70
  case Dec(n, e)::p => compile_abc(lay, p, cnt + 1, compile_Dec(address(lay, cnt), n, address(lay, e))::out)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    71
  case Goto(e)::p => compile_abc(lay, p, cnt + 1, compile_Goto(address(lay, e))::out)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    72
}
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
// component TMs for each instruction
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    76
def TMs(p: AProg) = {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    77
  val lay = layout(p, 0, Nil) 
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    78
  println("layout calculated")
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    79
  println("number of states (38667456): " + lay.last)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    80
  compile_abc(lay, p, 0, Nil)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    81
}
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    83
def toTM(p: AProg) = {
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    84
  println("start TM compilation")
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    85
  TMs(p).reduceLeft(_ ++ _)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
    86
}
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
    
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89