implemented new UF in scala; made some small adjustments to the definitions in the theory
files
package object comp2 {
// Recusive function to Abacus translation
import lib._
import abacus._
import recs._
def AbacusAdd(m: Int, n: Int, p: Int) =
Abacus(Dec(m, 4), Inc(n), Inc(p), Goto(0), Dec(p, 7), Inc(m), Goto(4))
def MVReg(m: Int, n: Int) = Abacus(Dec(m, 3), Inc(n), Goto(0))
//move the registers ranging from i to i + n to range j to j + n
def MVRegs(i: Int, j: Int, n: Int) : Abacus = n match {
case 0 => Abacus()
case n => MVRegs(i, j, n - 1) :+ MVReg(i + n - 1, j + n - 1)
}
// clears the first n registers
def ClearRegs(n: Int) : Abacus = n match {
case 0 => Abacus()
case n => ClearRegs(n - 1) :+ Abacus(Dec(n - 1, 2), Goto(0))
}
def cn_merge_gs(x: List[(Abacus, Int, Int)], p: Int) : Abacus = x match {
case Nil => Abacus(Nil)
case (gprog, gpara, gn)::gs => gprog :+ MVReg(gpara, p) :+ cn_merge_gs(gs, p + 1)
}
// translation:
// second component is the arity of the recursive function,
// third componen is the maximum of registers used
def compile_rec(f: Rec) : (Abacus, Int, Int) = f match {
case Z => (Abacus(Goto(1)), 1, 2)
case S => (AbacusAdd(0, 1, 2) :+ Abacus(Inc(1)), 1, 3)
case Id(i, j) => (AbacusAdd(j, i, i + 1), i, i + 2)
case Cn(n, f, gs) => {
val cied_gs = gs.map(compile_rec)
val (fprog, fpara, fn) = compile_rec(f)
val pstr = (1 + n :: fn :: (cied_gs.map(_._3))).max
val qstr = pstr + gs.length + 1
(cn_merge_gs(cied_gs, pstr) :+ MVRegs(0, qstr, n) :+
MVRegs(pstr, 0, gs.length) :+ fprog :+
MVReg(fpara, pstr) :+ ClearRegs(gs.length) :+
MVReg(pstr, n) :+ MVRegs(qstr, 0, n), n, qstr + n)
}
case Pr(n, f, g) => {
val (fprog, fpara, fn) = compile_rec(f)
val (gprog, gpara, gn) = compile_rec(g)
val p = List(n + 3, fn, gn).max
val e = gprog.p.length + 7
(MVReg(n, p) :+ fprog :+ MVReg(n, n + 1) :+
((Abacus(Dec(p, e)) :+ gprog :+ Abacus(Inc(n), Dec(n + 1, 3), Goto(1))) ++
Abacus(Dec(n + 2, 0), Inc (n + 1), Goto (gprog.p.length + 4))), n + 1, p + 1)
}
case Mn(n, f) => {
val (fprog, fpara, fn) = compile_rec(f)
val len = fprog.p.length
(fprog ++ Abacus(Dec(n + 1, len + 5), Dec(n + 1, len + 3), Goto(len + 1), Inc(n), Goto(0)),
n, List(n + 1, fn).max)
}
}
}