scala/turing.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 12:51:24 +0000
changeset 294 6836da75b3ac
parent 210 5e2e576fac7c
permissions -rw-r--r--
updated to Isabelle 2016-1
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: 192
diff changeset
     1
package object turing {
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
     2
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
     3
import scala.annotation.tailrec
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
     4
import lib._
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
     5
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     6
// tape cells
192
3c1107984b41 introduced sealed classes
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
     7
sealed abstract class Cell {
188
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
     8
  def * (n: Int) : List[Cell] = n match {
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
     9
    case 0 => Nil
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    10
    case n => this :: this * (n - 1)
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    11
  }
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    12
}
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
case object Bk extends Cell { override def toString = "0" }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
case object Oc extends Cell { override def toString = "1" }
d2c85556d290 added scala file
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
// actions
192
3c1107984b41 introduced sealed classes
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    17
sealed abstract class Action
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
case object WBk extends Action
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
case object WOc extends Action
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
case object R extends Action
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
case object L extends Action
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
case object Nop extends Action
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
type State = Int
188
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    25
type Inst = (Action, State)
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    26
type Prog = List[Inst]
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    28
// tapes
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
case class Tape(l: List[Cell], r: List[Cell]) {
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
    30
  
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
  def update(a: Action) = a match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
    case WBk => Tape(l, Bk::tl(r))
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
    case WOc => Tape(l, Oc::tl(r))
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
    case L => if (l == Nil) Tape(Nil, Bk::r) else Tape (tl(l), hd(l)::r)
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
    case R => if (r == Nil) Tape(Bk::l, Nil) else Tape(hd(r)::l, tl(r))
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
    case Nop => Tape(l, r)
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
  }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
  def read = r match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
    case Nil => Bk
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
    case x::_ => x
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
  }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
    44
  override def toString = join(l.reverse) + ">" + join(r)
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
}
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    47
// standard tapes
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
    48
object Tape {
209
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    49
  def apply(ns: List[Int]) : Tape = 
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    50
   Tape(Nil, ns.map(n => Oc * (n + 1)).reduceLeft(_ ::: List(Bk) ::: _))
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    51
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    52
  def apply(ns: Int*) : Tape = apply(ns.toList)
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    53
    
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
    54
}
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 192
diff changeset
    55
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
// configurations
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
case class Config(s: State, tp: Tape) {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
  def is_final = s == 0
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
  override def toString = tp.toString
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
}
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
183
4cf023ee2f4c updated exponent program
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 182
diff changeset
    63
// Turing machines
177
1c2e639d4e54 added abacus programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 176
diff changeset
    64
case class TM(p: Prog) {
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
    65
209
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
    66
  // composition
188
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    67
  def ++ (that: TM) = TM(this.p ::: that.p)
210
5e2e576fac7c tuned abacus to turing compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 209
diff changeset
    68
  def :+ (that: TM) = this.adjust ++ that.shift(this.p.length / 2)
188
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    69
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
    70
  def shift(n: Int) =
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
    71
    TM(p.map{case (a, s) => (a, if (s == 0) 0 else s + n)})
189
5974111de158 parts of the Abacus translation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 188
diff changeset
    72
  def adjust(n: Int) : TM =
5974111de158 parts of the Abacus translation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 188
diff changeset
    73
    TM(p.map{case (a, s) => (a, if (s == 0) n else s)})
5974111de158 parts of the Abacus translation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 188
diff changeset
    74
  def adjust : TM = adjust(p.length / 2 + 1)
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
  
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
  def fetch(s: State, a: Cell) = (s, a) match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
    case (0, _) => (Nop, 0)
188
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    78
    case (s, Bk) => nth_of(p, 2 * (s - 1)) match {
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    79
      case None => (Nop, 0)
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    80
      case Some(i) => i
8939cc9b14f9 tuned Scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 183
diff changeset
    81
    }
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
    case (s, Oc) => nth_of(p, 2 * (s - 1) + 1) match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
      case None => (Nop, 0)
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
      case Some(i) => i
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
    }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
  } 
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
  def step(cf: Config) : Config = fetch (cf.s, cf.tp.read) match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
    case (a, s_next) => Config(s_next, cf.tp.update(a))
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
  }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
  def steps(cf: Config, n: Int) : Config = n match {
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
    case 0 => cf
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
    case n => steps(step(cf), n - 1)
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
  } 
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
191
98370b96c1c5 compilation from Abacus to Turing in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 189
diff changeset
    97
  @tailrec
98370b96c1c5 compilation from Abacus to Turing in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 189
diff changeset
    98
  final def run(cf: Config) : Config = {
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
    if (cf.is_final) cf else run(step(cf))
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
  }
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
 
177
1c2e639d4e54 added abacus programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 176
diff changeset
   102
  def run(tp: Tape) : Tape = run(Config(1, tp)).tp
176
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
}
d2c85556d290 added scala file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
   105
// some syntactical convenience
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
   106
object TM {
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
   107
  def apply(is: Inst*) : TM = TM(is.toList)
178
8248f8adf17d added some TM machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 177
diff changeset
   108
}
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
   109
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
   110
}