# HG changeset patch # User Christian Urban # Date 1361193987 0 # Node ID 8f443f2ed1f65ffeee5c71347933f73221064bf8 # Parent 650e7a7a389b171e5bfad585d61b679c28eaf0a1 added abacus machines diff -r 650e7a7a389b -r 8f443f2ed1f6 thys/Abacus.thy --- a/thys/Abacus.thy Mon Feb 18 00:18:56 2013 +0000 +++ b/thys/Abacus.thy Mon Feb 18 13:26:27 2013 +0000 @@ -38,7 +38,7 @@ fun mult :: "nat \ nat \ nat \ nat \ nat \ abc_prog" where - "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1" + "mult m1 m2 n p e = [Dec m1 e]@ plus m2 n p 1" fun expo :: "nat \ nat \ nat \ nat \ nat \ abc_prog" where diff -r 650e7a7a389b -r 8f443f2ed1f6 turing.scala --- a/turing.scala Mon Feb 18 00:18:56 2013 +0000 +++ b/turing.scala Mon Feb 18 13:26:27 2013 +0000 @@ -149,13 +149,30 @@ case class Dec(n: Int, l: Int) extends AInst case class Goto(l: Int) extends AInst +def ashift(ai: AInst, offset: Int, jump: Int) = ai match { + case Inc(n) => Inc(n) + case Dec(n, l) => if (l == jump) Dec(n, l) else Dec(n, l + offset) + case Goto(l) => if (l == jump) Goto(l) else Goto(l + offset) +} + +def aadjust(ai: AInst, old_jump: Int, jump: Int) = ai match { + case Inc(n) => Inc(n) + case Dec(n, l) => if (l == old_jump) Dec(n, jump) else Dec(n, l) + case Goto(l) => if (l == old_jump) Goto(jump) else Goto(l) +} + + + type AProg = List[AInst] type Regs = Map[Int, Int] case class AConfig(s: Int, regs: Regs) case class Abacus(p: AProg) { - + + def shift(offset: Int, jump: Int) = Abacus(p.map(ashift(_, offset, jump))) + def adjust(old_jump: Int, jump: Int) = Abacus(p.map(aadjust(_, old_jump, jump))) + def step(cf: AConfig) : AConfig = (nth_of(p, cf.s), cf.s) match { case (None, _) => cf case (Some(Inc(n)), s) => AConfig(s + 1, cf.regs + (n -> (dget(cf.regs, n) + 1))) @@ -181,15 +198,32 @@ } // examples -class Copy(in: Int, out: Int) extends +def Copy(in: Int, out: Int) = Abacus(List(Dec(in, -1), Inc(out), Goto(0))) -class Plus(in1: Int, in2: Int, out: Int) extends - Abacus(List(Dec(in1, 4), Inc(in2), Inc(out), - Goto(0), Dec(out, -1), Inc(in1), Goto(4))) +def Plus(m: Int, n: Int, tmp: Int, jump: Int) = + Abacus(List(Dec(m, 4), Inc(n), Inc(tmp), + Goto(0), Dec(tmp, jump), Inc(m), Goto(4))) + +def Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = { + val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0) + Abacus(Dec(in1, jump) :: tm.p) +} + +def Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = { + val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0) + Abacus(Dec(in1, jump) :: tm.p) +} + +def Expo(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = { + val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0) + Abacus(Dec(in1, jump) :: tm.p) +} -println("Ab: " + (new Plus(0, 1, 2)).run(Map(0 -> 3, 1 -> 4))) +println("Copy: " + (Copy(0, 1).run(Map(0 -> 3, 1 -> 0)))) +println("Plus: " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0)))) +println("Mult: " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0)))) @@ -231,7 +265,7 @@ else throw new IllegalArgumentException("Cn: args") } case class Mn(n: Int, f: Rec) extends Rec { - override def eval(ns: List[Int]) = + override def eval(ns: List[Int]) = 0 }