270
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1 |
package object recs {
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
//Recursive Functions
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
abstract class Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
def eval(ns: List[Int]) : Int
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
def eval(ns: Int*) : Int = eval(ns.toList)
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
//syntactic convenience for composition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
def o(r: Rec) = Cn(r.arity, this, List(r))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))
|
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>
diff
changeset
|
13 |
def o(r: Rec, f: Rec, g: Rec, h: Rec) = Cn(r.arity, this, List(r, f, g, h))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
def arity : Int
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
case object Z extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
override def eval(ns: List[Int]) = ns match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
case n::Nil => 0
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
case _ => throw new IllegalArgumentException("Z args: " + ns)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
override def arity = 1
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
case object S extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
override def eval(ns: List[Int]) = ns match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
case n::Nil => n + 1
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
case _ => throw new IllegalArgumentException("S args: " + ns)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
override def arity = 1
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
case class Id(n: Int, m: Int) extends Rec {
|
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>
diff
changeset
|
34 |
require(m < n, println("Id m < n:" + m + " " + n))
|
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>
diff
changeset
|
35 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
override def eval(ns: List[Int]) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
if (ns.length == n && m < n) ns(m)
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
override def arity = n
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
|
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>
diff
changeset
|
44 |
require(f.arity == gs.length,
|
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>
diff
changeset
|
45 |
println("CN " + f + " " + gs.mkString(",") + "\n" +
|
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>
diff
changeset
|
46 |
"f.arity gs.length:" + f.arity + " " + gs.length))
|
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>
diff
changeset
|
47 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
override def eval(ns: List[Int]) =
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
val msg = List("Cn f: " + f,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
"n: " + n,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
"f arity: " + f.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
"ns-args: " + ns,
|
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>
diff
changeset
|
55 |
"gs arities: " + gs.map(_.arity).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>
diff
changeset
|
56 |
"gs: " + gs.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>
diff
changeset
|
57 |
"ns.length == n " + (ns.length == n).toString,
|
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>
diff
changeset
|
58 |
"gs.forall(_.arity == n) " + (gs.forall(_.arity == n)).toString,
|
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>
diff
changeset
|
59 |
"f.arity == gs.length " + (f.arity == gs.length).toString
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
throw new IllegalArgumentException(msg.mkString("\n"))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
override def arity = n
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
// syntactic convenience
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
object Cn {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
case class Pr(n: Int, f: Rec, g: Rec) extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
override def eval(ns: List[Int]) =
|
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
if (ns.length == n + 1) {
|
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>
diff
changeset
|
76 |
if (ns.head == 0) f.eval(ns.tail)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
else {
|
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>
diff
changeset
|
78 |
val r = Pr(n, f, g).eval(ns.head - 1 :: ns.tail)
|
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>
diff
changeset
|
79 |
g.eval(ns.head - 1 :: r :: ns.tail)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
}
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
val msg = List("Pr f: " + f,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
"g: " + g,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
"n: " + n,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
"f arity: " + f.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
"g arity: " + g.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
"ns-args: " + ns)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
throw new IllegalArgumentException(msg.mkString("\n"))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
override def arity = n + 1
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
// syntactic convenience
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
object Pr {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
case class Mn(n: Int, f: Rec) extends Rec {
|
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
def evaln(ns: List[Int], n: Int) : Int =
|
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>
diff
changeset
|
103 |
if (f.eval(n :: ns) == 0) n else evaln(ns, n + 1)
|
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
override def eval(ns: List[Int]) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
if (ns.length == n) evaln(ns, 0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
else throw new IllegalArgumentException("Mn: args")
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
override def arity = n
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
|
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>
diff
changeset
|
112 |
object Mn {
|
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>
diff
changeset
|
113 |
def apply(f: Rec) : Rec = Mn(f.arity - 1, f)
|
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>
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>
diff
changeset
|
115 |
|
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>
diff
changeset
|
116 |
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
// Recursive Function examples
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
def Const(n: Int) : Rec = n match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
case 0 => Z
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
case n => S o Const(n - 1)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
}
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
|
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>
diff
changeset
|
125 |
def Swap(f: Rec) = f o (Id(2, 1), Id(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>
diff
changeset
|
126 |
val Add = Pr(Id(1, 0), S o Id(3, 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>
diff
changeset
|
127 |
val Mult = Pr(Z, Add o (Id(3, 1), Id(3, 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>
diff
changeset
|
128 |
val Power = Swap(Pr(Const(1), Mult o (Id(3, 1), Id(3, 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>
diff
changeset
|
129 |
val Fact = (Pr (Const(1), Mult o (S o Id(3, 0), Id(3, 1)))) o (Id(1, 0), Id(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>
diff
changeset
|
130 |
val Pred = Pr(Z, Id(3, 0)) o (Id(1, 0), Id(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>
diff
changeset
|
131 |
val Minus = Swap(Pr(Id(1, 0), Pred o Id(3, 1)))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
val Not = Minus o (Const(1), Id(1, 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>
diff
changeset
|
135 |
val Eq = Minus o (Const(1) o Id(2, 0), Add o (Minus, Swap(Minus)))
|
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>
diff
changeset
|
136 |
val Noteq = Not o Eq
|
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>
diff
changeset
|
137 |
val Conj = Sign o Mult
|
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>
diff
changeset
|
138 |
val Disj = Sign o Add
|
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>
diff
changeset
|
139 |
val Imp = Disj o (Not o Id(2, 0), Id(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>
diff
changeset
|
140 |
val Ifz = Pr(Id(2, 0), Id(4, 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>
diff
changeset
|
141 |
val If = Ifz o (Not o Id(3, 0), Id(3, 1), Id (3, 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>
diff
changeset
|
142 |
|
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>
diff
changeset
|
143 |
val Less = Sign o (Swap(Minus))
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
val Le = Disj o (Less, Eq)
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
|
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>
diff
changeset
|
146 |
def Sigma1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(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>
diff
changeset
|
147 |
Add o (Id(3, 1), f o (S o Id(3, 0), Id(3, 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>
diff
changeset
|
148 |
def Sigma2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(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>
diff
changeset
|
149 |
Add o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 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>
diff
changeset
|
150 |
|
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>
diff
changeset
|
151 |
def Accum1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(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>
diff
changeset
|
152 |
Mult o (Id(3, 1), f o (S o Id(3, 0), Id(3, 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>
diff
changeset
|
153 |
def Accum2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(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>
diff
changeset
|
154 |
Mult o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 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>
diff
changeset
|
155 |
def Accum3(f: Rec) = Pr(f o (Z o (Id(3, 0)), Id(3, 0), Id(3, 1), Id(3, 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>
diff
changeset
|
156 |
Mult o (Id(5, 1), f o (S o Id(5, 0), Id(5, 2), Id(5, 3), Id(5, 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>
diff
changeset
|
157 |
|
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>
diff
changeset
|
158 |
def All1(f: Rec) = Sign o (Accum1(f))
|
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>
diff
changeset
|
159 |
def All2(f: Rec) = Sign o (Accum2(f))
|
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>
diff
changeset
|
160 |
def All3(f: Rec) = Sign o (Accum3(f))
|
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>
diff
changeset
|
161 |
|
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>
diff
changeset
|
162 |
def All1_less(f: Rec) = {
|
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>
diff
changeset
|
163 |
val cond1 = Eq o (Id(3, 0), Id(3, 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>
diff
changeset
|
164 |
val cond2 = f o (Id(3, 0), Id(3, 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>
diff
changeset
|
165 |
All2(Disj o (cond1, cond2)) o (Id(2, 0), Id(2, 0), Id(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>
diff
changeset
|
166 |
}
|
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>
diff
changeset
|
167 |
|
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>
diff
changeset
|
168 |
def All2_less(f: Rec) = {
|
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>
diff
changeset
|
169 |
val cond1 = Eq o (Id(4, 0), Id(4, 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>
diff
changeset
|
170 |
val cond2 = f o (Id(4, 0), Id(4, 2), Id(4, 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>
diff
changeset
|
171 |
All3(Disj o (cond1, cond2)) o (Id(3, 0), Id(3, 0), Id(3, 1), Id(3, 2))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
|
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>
diff
changeset
|
174 |
def Ex1(f: Rec) = Sign o (Sigma1(f))
|
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>
diff
changeset
|
175 |
def Ex2(f: Rec) = Sign o (Sigma2(f))
|
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>
diff
changeset
|
176 |
|
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>
diff
changeset
|
177 |
val Quo = {
|
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>
diff
changeset
|
178 |
val lhs = S o (Id(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>
diff
changeset
|
179 |
val rhs = Mult o (Id(3, 2), S o (Id(3, 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>
diff
changeset
|
180 |
val cond = Eq o (lhs, rhs)
|
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>
diff
changeset
|
181 |
val if_stmt = If o (cond, S o (Id(3, 1)), Id(3, 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>
diff
changeset
|
182 |
Pr(Z, if_stmt)
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
|
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>
diff
changeset
|
185 |
def Iter(f: Rec) = Pr(Id(1, 0), f o (Id(3, 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>
diff
changeset
|
186 |
|
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>
diff
changeset
|
187 |
def Max1(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(3, 0)), Id(3, 2)), S o (Id(3, 0)), Id(3, 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>
diff
changeset
|
188 |
def Max2(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(4, 0)), Id(4, 2), Id(4, 3)), S o (Id(4, 0)), Id(4, 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>
diff
changeset
|
189 |
|
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>
diff
changeset
|
190 |
val Triangle = Quo o (Mult o (Id(1, 0), S), Const(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>
diff
changeset
|
191 |
|
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>
diff
changeset
|
192 |
val MaxTriangle = {
|
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>
diff
changeset
|
193 |
val cond = Not o (Le o (Triangle o (Id(2, 0)), Id(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>
diff
changeset
|
194 |
Max1(cond) o (Id(1, 0), Id(1, 0))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
|
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>
diff
changeset
|
197 |
val MaxTriangle2 = {
|
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>
diff
changeset
|
198 |
Pred o Mn(Le o (Triangle o (Id(2, 0)), Id(2, 1)))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
|
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>
diff
changeset
|
201 |
case object MaxTriangleFast extends Rec {
|
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>
diff
changeset
|
202 |
def triangle(n: Int) : Int = (n * (n + 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>
diff
changeset
|
203 |
|
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>
diff
changeset
|
204 |
def search(m: Int, n: Int) : Int = {
|
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>
diff
changeset
|
205 |
if (triangle(n) > m) n - 1 else search(m, n + 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>
diff
changeset
|
206 |
}
|
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>
diff
changeset
|
207 |
|
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>
diff
changeset
|
208 |
override def eval(ns: List[Int]) = ns match {
|
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>
diff
changeset
|
209 |
case n::Nil => search(n, 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>
diff
changeset
|
210 |
case _ => throw new IllegalArgumentException("MT args: " + ns)
|
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>
diff
changeset
|
211 |
}
|
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>
diff
changeset
|
212 |
|
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>
diff
changeset
|
213 |
override def arity = 1
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
|
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>
diff
changeset
|
216 |
case object TriangleFast extends Rec {
|
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>
diff
changeset
|
217 |
def triangle(n: Int) : Int = (n * (n + 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>
diff
changeset
|
218 |
|
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>
diff
changeset
|
219 |
override def eval(ns: List[Int]) = ns match {
|
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>
diff
changeset
|
220 |
case n::Nil => triangle(n)
|
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>
diff
changeset
|
221 |
case _ => throw new IllegalArgumentException("Tr args: " + ns)
|
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>
diff
changeset
|
222 |
}
|
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>
diff
changeset
|
223 |
|
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>
diff
changeset
|
224 |
override def arity = 1
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
|
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>
diff
changeset
|
227 |
//(0 until 200).map(MaxTriangleFast.eval(_))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
|
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>
diff
changeset
|
230 |
val Penc = Add o (TriangleFast o (Add o (Id(2, 0), Id(2, 1))), Id(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>
diff
changeset
|
231 |
val Pdec1 = Minus o (Id(1, 0), Triangle o (MaxTriangle o (Id(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>
diff
changeset
|
232 |
val Pdec2 = Minus o (MaxTriangle o (Id(1, 0)), Pdec1 o (Id(1, 0)))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
|
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>
diff
changeset
|
234 |
def Lenc(fs: List[Rec]) : Rec = fs match {
|
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>
diff
changeset
|
235 |
case Nil => Z
|
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>
diff
changeset
|
236 |
case f::fs => Penc o (S o (f), Lenc(fs))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
|
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>
diff
changeset
|
239 |
val Ldec = Pred o (Pdec1 o (Swap (Iter(Pdec2))))
|
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>
diff
changeset
|
240 |
|
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>
diff
changeset
|
241 |
val Within = Less o (Z o (Id(2, 0)), Swap (Iter(Pdec2)))
|
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>
diff
changeset
|
242 |
val Enclen = (Max1(Not o (Within o (Id(2, 1), Pred o (Id(2, 0)))))) o (Id(1, 0), Id(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>
diff
changeset
|
243 |
|
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>
diff
changeset
|
244 |
|
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>
diff
changeset
|
245 |
val Read = Ldec o (Id(1, 0), Const(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>
diff
changeset
|
246 |
val Write = Penc o (S o (Id(2, 0)), Pdec2 o (Id(2, 1)))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
|
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>
diff
changeset
|
248 |
val Newleft = {
|
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>
diff
changeset
|
249 |
val cond0 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
250 |
val cond1 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
251 |
val cond2 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
252 |
val cond3 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
253 |
val case3 = Penc o (S o (Read o (Id(3, 1))), Id(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>
diff
changeset
|
254 |
If o (cond0,
|
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>
diff
changeset
|
255 |
Id(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>
diff
changeset
|
256 |
If o (cond1,
|
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>
diff
changeset
|
257 |
Id(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>
diff
changeset
|
258 |
If o (cond2,
|
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>
diff
changeset
|
259 |
Pdec2 o (Id(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>
diff
changeset
|
260 |
If o (cond3, case3, Id(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>
diff
changeset
|
261 |
}
|
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>
diff
changeset
|
262 |
|
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>
diff
changeset
|
263 |
val Newright = {
|
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>
diff
changeset
|
264 |
val cond0 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
265 |
val cond1 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
266 |
val cond2 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
267 |
val cond3 = Eq o (Id(3, 2), Const(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>
diff
changeset
|
268 |
val case2 = Penc o (S o (Read o (Id(3, 0))), Id(3, 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>
diff
changeset
|
269 |
If o (cond0,
|
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>
diff
changeset
|
270 |
Write o (Const(0), Id(3, 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>
diff
changeset
|
271 |
If o (cond1,
|
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>
diff
changeset
|
272 |
Write o (Const(1), Id(3, 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>
diff
changeset
|
273 |
If o (cond2,
|
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>
diff
changeset
|
274 |
case2,
|
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>
diff
changeset
|
275 |
If o (cond3, Pdec2 o (Id(3, 1)), Id(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>
diff
changeset
|
276 |
}
|
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>
diff
changeset
|
277 |
|
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>
diff
changeset
|
278 |
val Actn = Swap (Pr(Pdec1 o (Pdec1 o (Id(1, 0))), Pdec1 o (Pdec2 o (Id(3, 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>
diff
changeset
|
279 |
|
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>
diff
changeset
|
280 |
val Action = {
|
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>
diff
changeset
|
281 |
val cond1 = Noteq o (Id(3, 1), Z)
|
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>
diff
changeset
|
282 |
val cond2 = Within o (Id(3, 0), Pred o (Id(3, 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>
diff
changeset
|
283 |
val if_branch = Actn o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 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>
diff
changeset
|
284 |
If o (Conj o (cond1, cond2), if_branch, Const(4))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
|
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>
diff
changeset
|
287 |
val Newstat = Swap (Pr (Pdec2 o (Pdec1 o (Id(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>
diff
changeset
|
288 |
Pdec2 o (Pdec2 o (Id(3, 2)))))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
|
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>
diff
changeset
|
290 |
val Newstate = {
|
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>
diff
changeset
|
291 |
val cond = Noteq o (Id(3, 1), Z)
|
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>
diff
changeset
|
292 |
val if_branch = Newstat o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 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>
diff
changeset
|
293 |
If o (cond, if_branch, Z)
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
|
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>
diff
changeset
|
296 |
val Conf = Lenc (List(Id(3, 0), Id(3, 1), Id(3, 2)))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
|
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>
diff
changeset
|
298 |
val State = Ldec o (Id(1, 0), Z)
|
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>
diff
changeset
|
299 |
|
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>
diff
changeset
|
300 |
val Left = Ldec o (Id(1, 0), Const(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>
diff
changeset
|
301 |
|
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>
diff
changeset
|
302 |
val Right = Ldec o (Id(1, 0), Const(2))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
303 |
|
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>
diff
changeset
|
304 |
val Step = {
|
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>
diff
changeset
|
305 |
val left = Left o (Id(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>
diff
changeset
|
306 |
val right = Right o (Id(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>
diff
changeset
|
307 |
val state = State o (Id(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>
diff
changeset
|
308 |
val read = Read o (right)
|
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>
diff
changeset
|
309 |
val action = Action o (Id(2, 1), state, read)
|
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>
diff
changeset
|
310 |
val newstate = Newstate o (Id(2, 1), state, read)
|
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>
diff
changeset
|
311 |
val newleft = Newleft o (left, right, action)
|
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>
diff
changeset
|
312 |
val newright = Newright o (left, right, action)
|
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>
diff
changeset
|
313 |
Conf o (newstate, newleft, newright)
|
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>
diff
changeset
|
314 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
|
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>
diff
changeset
|
316 |
val Steps = Pr (Id(2, 0), Step o (Id(4, 1), Id(4, 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>
diff
changeset
|
317 |
|
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>
diff
changeset
|
318 |
val Stknum = Minus o (Sigma1(Ldec o (Id(2, 1), Id(2, 0))) o (Enclen o (Id(1, 0)), Id(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>
diff
changeset
|
319 |
Ldec o (Id(1, 0), Enclen o (Id(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>
diff
changeset
|
320 |
|
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>
diff
changeset
|
321 |
val Right_std = {
|
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>
diff
changeset
|
322 |
val bound = Enclen o (Id(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>
diff
changeset
|
323 |
val cond1 = Le o (Const(1) o (Id(2, 0)), Id(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>
diff
changeset
|
324 |
val cond2 = All1_less (Eq o (Ldec o (Id(2, 1), Id(2, 0)), Const(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>
diff
changeset
|
325 |
val bound2 = Minus o (Enclen o (Id(2, 1)), Id(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>
diff
changeset
|
326 |
val cond3 =
|
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>
diff
changeset
|
327 |
(All2_less (Eq o (Ldec o (Id(3, 2), Add o (Id(3, 1), Id(3, 0))), Z))) o (bound2, Id(2, 0), Id(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>
diff
changeset
|
328 |
Ex1(Conj o (Conj o (cond1, cond2), cond3)) o (bound, Id(1, 0))
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
|
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>
diff
changeset
|
331 |
val Left_std = {
|
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>
diff
changeset
|
332 |
val cond = Eq o (Ldec o (Id(2, 1), Id(2, 0)), Z)
|
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>
diff
changeset
|
333 |
(All1_less(cond)) o (Enclen o (Id(1, 0)), Id(1, 0))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
}
|
238
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
|
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>
diff
changeset
|
336 |
val Std = Conj o (Left_std o (Left o (Id(1, 0))), Right_std o (Right o (Id(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>
diff
changeset
|
337 |
|
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>
diff
changeset
|
338 |
val Final = Eq o (State o (Id(1, 0)), Z)
|
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>
diff
changeset
|
339 |
|
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>
diff
changeset
|
340 |
val Stop = {
|
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>
diff
changeset
|
341 |
val stps = Steps o (Id(3, 2), Id(3, 1), Id(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>
diff
changeset
|
342 |
Conj o (Final o (stps), Std o (stps))
|
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>
diff
changeset
|
343 |
}
|
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>
diff
changeset
|
344 |
|
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>
diff
changeset
|
345 |
val Halt = Mn (Not o (Stop o (Id(3, 1), Id(3, 2), Id(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>
diff
changeset
|
346 |
|
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>
diff
changeset
|
347 |
val UF = Pred o (Stknum o (Right o (Steps o (Halt o (Id(2, 0), Id(2, 1)), Id(2, 1), Id(2, 0)))))
|
238
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
}
|