scala/comp1.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 12:48:43 +0000
changeset 293 8b55240e12c6
parent 271 4457185b22ef
permissions -rw-r--r--
upodated to Isabelle 2016

package object comp1 {

// Abacus to TM translation

import lib._
import turing._
import abacus._
import scala.annotation.tailrec

// TMs used in the translation

val TMInc = TM((WOc, 1), (R, 2), (WOc, 3), (R, 2), (WOc, 3), (R, 4), 
               (L, 7), (WBk, 5), (R, 6), (WBk, 5), (WOc, 3), (R, 6),
               (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (WBk, 9))

val TMDec = TM((WOc, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
               (R, 5), (WBk, 4), (R, 6), (WBk, 5), (L, 7), (L, 8),
               (L, 11), (WBk, 7), (WOc, 8), (R, 9), (L, 10), (R, 9),
               (R, 5), (WBk, 10), (L, 12), (L, 11), (R, 13), (L, 11),
               (R, 17), (WBk, 13), (L, 15), (L, 14), (R, 16), (L, 14),
               (R, 0), (WBk, 16))

val TMGoto = TM((Nop, 1), (Nop, 1))

val TMMopup_aux = TM((R, 2), (R, 1), (L, 5), (WBk, 3), (R, 4), (WBk, 3),
                     (R, 2), (WBk, 3), (L, 5), (L, 6), (R, 0), (L, 6))

def TMFindnth(n: Int) : TM = n match {
  case 0 => TM(Nil)
  case n => TMFindnth(n - 1) ++ TM((WOc, 2 * n - 1), (R, 2 * n), (R, 2 * n + 1), (R, 2 * n))
}

def TMMopup(n: Int) = {
  def TMMopup1(n: Int) : TM = n match {
    case 0 => TM(Nil)
    case n => TMMopup1(n - 1) ++ TM((R, 2 * n + 1), (WBk, 2 * n), (R, 2 * n - 1), (WOc, 2 * n))
  }
  TMMopup1(n) ++ TMMopup_aux.shift(2 * n)
}


// start address of the instructions
@tailrec
def layout(p: AProg, sum: Int, out: List[Int]) : List[Int] = p match {
    case Nil => out.reverse
    case Inc(n)::p => layout(p, 2 * n + 9 + sum, 2 * n + 9 + sum::out) 
    case Dec(n, _)::p => layout(p, 2 * n + 16 + sum, 2 * n + 16 + sum::out)  
    case Goto(n)::p => layout(p, 1 + sum, 1 + sum::out) 
 }

def address(layout: List[Int], n: Int) = {
  //println("calculating layout of " + n)
  layout(n) + 1
}

def compile_Inc(s: Int, n: Int) = 
  TMFindnth(n).shift(s - 1) ++ TMInc.shift(2 * n).shift(s - 1)

def compile_Dec(s: Int, n: Int, e: Int) = 
  TMFindnth(n).shift(s - 1) ++ TMDec.shift(2 * n).shift(s - 1).adjust(e)

def compile_Goto(s: Int) = TMGoto.shift(s - 1)

@tailrec
def compile_abc(lay: List[Int], p: AProg, cnt: Int, out: List[TM]): List[TM] = {
  if (cnt % 1000 == 0) println("compile counter of instructions " + cnt);
p match {
  case Nil => out.reverse
  case Inc(n)::p => compile_abc(lay, p, cnt + 1, compile_Inc(address(lay, cnt), n)::out)
  case Dec(n, e)::p => compile_abc(lay, p, cnt + 1, compile_Dec(address(lay, cnt), n, address(lay, e))::out)
  case Goto(e)::p => compile_abc(lay, p, cnt + 1, compile_Goto(address(lay, e))::out)
}
}

// component TMs for each instruction
def TMs(p: AProg) = {
  val lay = layout(p, 0, Nil) 
  println("layout calculated")
  println("number of states (38667456): " + lay.last)
  compile_abc(lay, p, 0, Nil)
}

def toTM(p: AProg) = {
  println("start TM compilation")
  TMs(p).reduceLeft(_ ++ _)
}
    
}