scala/ex.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 12:51:24 +0000
changeset 294 6836da75b3ac
parent 271 4457185b22ef
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:
diff changeset
     1
import lib._
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
import turing._
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
import abacus._
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
     4
import recs._
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
     5
import comp1._
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
     6
import comp2._
239
ac3309722536 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
     7
222
d682591c63e1 better printing of register programs in Scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 221
diff changeset
     8
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
// Turing machine examples
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    10
val TMCopy = TM((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    11
                (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    12
                (R, 7), (WBk, 6), (R, 7), (R, 8), (WOc, 9), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    13
                (R, 8), (L, 10), (L, 9), (L, 10), (L, 5), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    14
                (L, 0), (R, 12), (WOc, 13), (L, 14), (R, 12), 
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    15
                (R, 12), (L, 15), (WBk, 14), (R, 0), (L, 15))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
    17
/*
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
println("TMCopy:    " + (TMCopy.run(Tape(3))))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
println("TMfindnth: " + (TMFindnth(3).run(Tape(1,2,3,4,5))))
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    20
println("TMMopup:   " + (TMMopup(3).run(Tape(1,2,3,4,5))))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
210
5e2e576fac7c tuned abacus to turing compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 209
diff changeset
    22
println("TMCopyMop: " + ((TMCopy :+ TMMopup(0))))
5e2e576fac7c tuned abacus to turing compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 209
diff changeset
    23
println("TMCopyMop: " + ((TMCopy :+ TMMopup(1)).run(Tape(3))))
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
    24
*/
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
// Abacus machine examples
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
def Copy(in: Int, out: Int, jump: Int) = 
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    28
  Abacus(Dec(in, jump), Inc(out), Goto(0)) 
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
def Plus(m: Int, n: Int, tmp: Int, jump: Int) =
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    31
  Abacus(Dec(m, 4), Inc(n), Inc(tmp), Goto(0), Dec(tmp, jump), Inc(m), Goto(4))
193
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 Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = 
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    34
  Abacus(Dec(in1, jump)) ++ Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0)
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
def Expo(in1: Int, in2: Int, out: Int, tmp1: Int, tmp2: Int, jump: Int) = {
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    37
  Abacus(Inc(out), Dec(in1, jump)) ++ 
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
  Mult(out, in2, tmp2, tmp1, -1).shift(2, -1).adjust(-1, 10) ++
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    39
  Copy(tmp2, out, -1).shift(10, -1).adjust(-1, 1)
193
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
194
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    42
println("Copy 3:     " + (Copy(0, 1, -1).run(Map(0 -> 3, 1 -> 0))))
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    43
println("Plus 3 + 4: " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0))))
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    44
println("Mult 3 * 5: " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0))))
fc2a5e9fbb97 updated Scala files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    45
println("Expo 3 ^ 4: " + (Expo(0, 1, 2, 3, 4, -1).run(Map(0 -> 4, 1 -> 3, 2 -> 0, 3 -> 0, 4 -> 0))))
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
    47
/*
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
// Abacus-to-TM translation examples
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
println("Compiled Copy 3:     " + toTM(Copy(0, 1, Int.MaxValue).p).run(Tape(3,0,0)))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
println("Compiled Plus 3 + 4: " + toTM(Plus(0, 1, 2, Int.MaxValue).p).run(Tape(3,4,0,0)))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
println("Compiled Mult 3 * 5: " + toTM(Mult(0, 1, 2, 3, Int.MaxValue).p).run(Tape(3,5,0,0)))
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
println("Compiled Expo 3 ^ 4: " + toTM(Expo(0, 1, 2, 3, 4, 10000).p).run(Tape(3,4,0,0,0)))
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
    53
*/
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
    54
 
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    55
// Recursive function examples 
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    56
println("Const 8:   " + Const(8).eval(67))
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    57
println("Add 3 4:   " + Add.eval(3, 4))
201
09befdf4fc99 syntactic convenience for recursive functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 200
diff changeset
    58
println("Mult 3 4:  " + recs.Mult.eval(3, 4))
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    59
println("Power 2 3: " + Power.eval(2, 3))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    60
println("Fact 5:    " + Fact.eval(5))
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    61
println("Pred 9:    " + Pred.eval(9))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    62
println("Pred 0:    " + Pred.eval(0))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    63
println("Minus 6 2: " + Minus.eval(6, 2))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    64
println("Minus 6 8: " + Minus.eval(6, 8))
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    65
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    66
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    67
println("Sign 8:    " + Sign.eval(8))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    68
println("Sign 0:    " + Sign.eval(0))
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    69
println("Not 0:     " + Not.eval(0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    70
println("Not 6:     " + Not.eval(6))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    71
println("Eq 4 4:    " + Eq.eval(4, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    72
println("Eq 4 6:    " + Eq.eval(4, 6))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    73
println("Eq 6 4:    " + Eq.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    74
println("NotEq 4 4: " + Noteq.eval(4, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    75
println("NotEq 4 6: " + Noteq.eval(4, 6))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    76
println("NotEq 6 4: " + Noteq.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    77
println("Conj 0 6:  " + Conj.eval(0, 6))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    78
println("Conj 6 4:  " + Conj.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    79
println("Conj 0 0:  " + Conj.eval(0, 0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    80
println("Disj 0 6:  " + Disj.eval(0, 6))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    81
println("Disj 6 4:  " + Disj.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    82
println("Disj 0 0:  " + Disj.eval(0, 0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    83
println("Imp  6 1:  " + Imp.eval(6, 1))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    84
println("Imp  6 4:  " + Imp.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    85
println("Imp  1 0:  " + Imp.eval(1, 0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    86
println("Ifz  0 1 2:" + Ifz.eval(0, 1, 2))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    87
println("Ifz  1 1 2:" + Ifz.eval(1, 1, 2))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    88
println("If   0 1 2:" + If.eval(0, 1, 2))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    89
println("If   1 1 2:" + If.eval(1, 1, 2))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    90
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    91
200
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    92
println("Less 4 4:  " + Less.eval(4, 4))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    93
println("Less 4 6:  " + Less.eval(4, 6))
8dde2e46c69d added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    94
println("Less 6 4:  " + Less.eval(6, 4))
239
ac3309722536 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    95
println("Le 4 4:    " + recs.Le.eval(4, 4))
ac3309722536 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    96
println("Le 4 6:    " + recs.Le.eval(4, 6))
ac3309722536 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    97
println("Le 6 4:    " + recs.Le.eval(6, 4))
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    98
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    99
println("Sigma1 Add 2 3 -> 12: " + Sigma1(Add).eval(2, 3))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   100
println("Accum1 Add 2 3 -> 60:  " + Accum1(Add).eval(2,3))
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   101
println("Accum1 Mult 2 3 -> 0:  " + Accum1(recs.Mult).eval(2,3))
269
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   102
println("Accum1 (Id(2, 1)) 2 3 -> 27:  " + Accum1(Id(2, 1)).eval(2,3))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   103
println("Accum2 (Id(3, 1)) 2 3 3 -> 27:  " + Accum2(Id(3, 1)).eval(2,3,3))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   104
println("Accum3 (Id(4, 1)) 2 3 3 3 -> 27:  " + Accum3(Id(4, 1)).eval(2,3,3,3))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   105
println("All1 Add 2 0 -> 0:  " + All1(Add).eval(2,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   106
println("All1 Add 2 1 -> 1:  " + All1(Add).eval(2,1))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   107
println("All1_less Add 3 0 -> 0:  " + All1_less(Add).eval(2,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   108
println("All1_less Add 3 1 -> 1:  " + All1_less(Add).eval(2,1))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   109
println("All2_less (Id 3 1) 2 3 0 -> 1:  " + All2_less(Id(3, 1)).eval(2,3,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   110
println("All2_less (Id 3 0) 2 3 0 -> 0:  " + All2_less(Id(3, 0)).eval(2,3,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   111
println("Ex1 Add 2 0 -> 1:       " + Ex1(Add).eval(2,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   112
println("Ex2 Id(3,1) 2 1 0 -> 1: " + Ex2(Id(3, 1)).eval(2,1,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   113
println("Ex2 Id(3,2) 2 1 0 -> 0: " + Ex2(Id(3, 2)).eval(2,1,0))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   114
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   115
println("Quo 6 4 -> 1:   " + Quo.eval(6, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   116
println("Quo 13 4 -> 3:  " + Quo.eval(13, 4))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   117
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   118
println("Triangle 0 - 5: " + (0 until 5).map(Triangle.eval(_)).mkString(","))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   119
println("MaxTriangle 10 -> 4 " + MaxTriangle.eval(10))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   120
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   121
println("Penc 1 2 -> 7: " + Penc.eval(1, 2))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   122
println("Pdec1 7 -> 1:  " + Pdec1.eval(7))
fa40fd8abb54 implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
   123
println("Pdec2 7 -> 2:  " + Pdec2.eval(7))
270
ccec33db31d4 some tests are commented out
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   124
println("Enclen 0 .. 10: " + (0 until 10).map(Enclen.eval(_)))
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   125
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   126
println("Size of UF -> 140843: " + UF.size)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   127
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   128
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   129
// compilation of rec to abacus tests
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   130
def test_comp2(f: Rec, ns: Int*) = {
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   131
  val (abc_f, _) = compile_rec(f)
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   132
  val abc_map = (0 until ns.length).zip(ns).toMap[Int, Int]
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   133
  //val start = System.nanoTime()
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   134
  //val res = (abc_f.run(abc_map))(arity)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   135
  //val end = System.nanoTime()
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   136
  //val time = (end - start)/1.0e9
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   137
  //("Result: " + res + "  length: " + abc_f.p.length + " time: " + "%.5f".format(time))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   138
  ("Length: " + abc_f.p.length)
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   139
}
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   140
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   141
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   142
println("S(3)          " + test_comp2(S, 3))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   143
println("Const(1)      " + test_comp2(Const(1), 0))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   144
println("Const(10)     " + test_comp2(Const(10), 0))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   145
println("Add(69, 30)   " + test_comp2(Add, 69, 30))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   146
println("Mult(13, 9)   " + test_comp2(recs.Mult, 13, 9))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   147
println("Power(3, 4)   " + test_comp2(Power, 3, 4))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   148
println("Minus(30, 4)  " + test_comp2(Minus, 30, 4))
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   149
println("Fact(5)       " + test_comp2(Fact, 5))
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   150
//println("UF(0)         " + test_comp2(UF, 0))
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 194
diff changeset
   151
209
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
   152
def test_comp1(f: Rec, ns: Int*) = {
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   153
  val (abc_f, _) = compile_rec(f)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   154
  println("Abacus Length: " + abc_f.p.length)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   155
  val tm = toTM(abc_f.p) :+ TMMopup(f.arity)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   156
  //val start = System.nanoTime()
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   157
  //val res = tm.run(Tape(ns.toList))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   158
  //val end = System.nanoTime()
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   159
  //val time = (end - start)/1.0e9
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   160
  //("length: " + tm.p.length + " tape: " + arity + " time: " + "%.5f".format(time) + "\nResult: " + res)
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   161
  ("Length: " + abc_f.p.length + " " + tm.p.length)
209
b16dfc467b67 finished compliations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 208
diff changeset
   162
}
205
c7975ab7c52e corrected scala compiler from recs to abacus
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 201
diff changeset
   163
271
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   164
//println("")
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   165
//println("S(3)          " + test_comp1(S, 3))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   166
//println("Const(10)     " + test_comp1(Const(10), 0))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   167
//println("Add(6, 3)     " + test_comp1(Add, 6, 3))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   168
//println("Mult(4, 5)    " + test_comp1(recs.Mult, 4, 5))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   169
//println("Fact(4)       " + test_comp1(Fact, 4))
4457185b22ef added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   170
println("UF(0)         " + test_comp1(UF, 0))
208
3267acc1f97f added examples for the rec to abacus compilation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
   171