Skip to content

Commit 9078a64

Browse files
marvinbornermarvinborner
committed
Better testing infrastructure
1 parent 20a08f7 commit 9078a64

2 files changed

Lines changed: 66 additions & 121 deletions

File tree

‎lib/language/ic/term.effekt‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,15 @@ def show(ctor: Constructor) = {
8282
def show(ctors: List[Constructor]) =
8383
"[" ++ ctors.map { ctor => ctor.show() }.join(", ") ++ "]"
8484

85+
def sameKind(ctor1: Constructor, ctor2: Constructor) = (ctor1, ctor2) match {
86+
case (Initiator(k1), Initiator(k2)) => true
87+
case (Abstractor(x1, b1, k1), Abstractor(x2, b2, k2)) => true
88+
case (Applicator(f1, a1, k1), Applicator(f2, a2, k2)) => true
89+
case (Duplicator(o1, ins1, label1), Duplicator(o2, ins2, label2)) => label1 == label2
90+
case (Superposer(i1, out1, label1), Superposer(i2, out2, label2)) => label1 == label2
91+
case _ => false
92+
}
93+
8594
def infixEq(ctor1: Constructor, ctor2: Constructor) = (ctor1, ctor2) match {
8695
case (Initiator(k1), Initiator(k2)) => k1 == k2
8796
case (Abstractor(x1, b1, k1), Abstractor(x2, b2, k2)) => x1 == x2 && b1 == b2 && k1 == k2

‎test/ruler.effekt‎

Lines changed: 57 additions & 121 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import test
22
import tty
33
import set
4+
import map
45

56
import lib/utils
67
import lib/net/net
@@ -14,34 +15,58 @@ def confluence(n: Int) { test: => Unit / Assertion }: Unit / Assertion = {
1415
0.each(n) { i =>
1516
try test()
1617
with Assertion {
17-
def assert(condition, msg) = do assert(condition, s"${msg} (run number ${i.show})")
18+
def assert(condition, msg) = resume(do assert(condition, s"${msg} (run number ${i.show})"))
1819
}
1920
}
2021
test()
2122
}
2223

23-
// for now mostly heuristics
24+
/// equivalence after renaming
2425
def assertEquivalent(bs: List[Constructor], as: List[Constructor]): Unit / { Formatted, Assertion } = {
25-
// TODO: ordering?
26-
// TODO: map for actual alpha equivalence
26+
// TODO: do not require same ordering
27+
28+
with on[MissingValue].default { assertTrue(false, s"constructor mismatch:\n${bs.show}\n vs\n${as.show}") }
29+
30+
var counter = 0
31+
var aMap: Map[String, String] = emptyGeneric()
32+
var bMap: Map[String, String] = emptyGeneric()
33+
as.zip(bs).foreach { case (a, b) =>
34+
assertTrue(a.sameKind(b), s"expected same constructor kind in\n${b.show}\n vs\n${a.show}")
35+
a.ports.zip(b.ports).foreach { case (pa, pb) =>
36+
if (aMap.contains(pa.name) || bMap.contains(pb.name)) {
37+
// these accesses should potentially fail
38+
val aName = aMap.get(pa.name).value
39+
val bName = bMap.get(pb.name).value
40+
assertEqual(aName, bName, s"expected same name, but got ${aName} and ${bName} in\n${b.show}\n vs\n${a.show}")
41+
assertEqual(pa.isPos, pb.isPos, s"expected same polarity in\n${b.show}\n vs \n${a.show}")
42+
} else {
43+
aMap = aMap.put(pa.name, counter.show)
44+
bMap = bMap.put(pb.name, counter.show)
45+
}
46+
}
47+
}
48+
assertEqual(as.size, bs.size)
2749

50+
// TODO: this check should be redundant now
2851
val aPorts = fromListGeneric(as.flatMap { ctor => ctor.ports.map { p => p.name } })
2952
val bPorts = fromListGeneric(bs.flatMap { ctor => ctor.ports.map { p => p.name } })
30-
assertEqual(aPorts.size, bPorts.size, s"Expected ${aPorts.size.show} unique variables, but got ${bPorts.size.show}:\n" ++ aPorts.toList.show ++ " vs " ++ bPorts.toList.show ++ "\nin " ++ as.show ++ "\nvs " ++ bs.show)
31-
32-
as.zip(bs).foreach {
33-
case (Abstractor(Pos(x1), Neg(b1), Pos(k1)), Abstractor(Pos(x2), Neg(b2), Pos(k2))) => ()
34-
case (Applicator(Neg(f1), Neg(a1), Pos(k1)), Applicator(Neg(f2), Neg(a2), Pos(k2))) => ()
35-
case (Duplicator(Neg(o1), ins1, label1), Duplicator(Neg(o2), ins2, label2)) =>
36-
assertEqual(ins1.size, ins2.size)
37-
assertEqual(label1, label2)
38-
case (Superposer(Pos(i1), out1, label1), Superposer(Pos(i2), out2, label2)) =>
39-
assertEqual(out1.size, out2.size)
40-
assertEqual(label1, label2)
41-
case (Initiator(Neg(k1)), Initiator(Neg(k2))) => ()
42-
case (_, _) => assertEqual(as, bs) { (a, b) => a == b } { c => c.show } // will fail, but we'll see why
53+
assertEqual(aPorts.size, bPorts.size, s"Expected ${aPorts.size.show} unique variables, but got ${bPorts.size.show}:\n${aPorts.toList.show} vs ${bPorts.toList.show}\nin ${as.show}\nvs ${bs.show}")
54+
}
55+
56+
record Confluence(value: Int)
57+
record Steps(value: Int)
58+
59+
def normalizeWith(term: String, conf: Confluence, steps: Steps, normalized: List[Constructor]) = {
60+
with confluence(conf.value)
61+
val program: Program = collect {
62+
with assertNoThrow[WrongFormat]
63+
with source[Char] { term.each }
64+
compile!()
4365
}
44-
assertEqual(as.size, bs.size)
66+
val redexes = box { program.redexes() }
67+
val (_normalized, _steps) = normalize(program, redexes, steps.value + 10)
68+
assertEqual(_steps, steps.value)
69+
assertEquivalent(list::collect[Constructor] { _normalized() }, normalized)
4570
}
4671

4772
def tests() = suite("└ ruler tests") {
@@ -67,80 +92,36 @@ def tests() = suite("└ ruler tests") {
6792
}
6893

6994
test("normalization: identity duplication") {
70-
with confluence(5)
71-
val program: Program = collect {
72-
with assertNoThrow[WrongFormat]
73-
with source[Char] { "(x=>(x x) x=>x)".each }
74-
compile!()
75-
}
76-
val redexes = box { program.redexes() }
77-
val (normalized, steps) = normalize(program, redexes, 10)
78-
assertEqual(steps, 4)
79-
assertEquivalent(list::collect[Constructor] { normalized() }, [
95+
"(x=>(x x) x=>x)".normalizeWith(Confluence(5), Steps(4), [
8096
Abstractor(Pos("xSym6_1_1".ref), Neg("xSym6_1_1".ref), Pos("xSym6_0_0".ref)),
8197
Initiator(Neg("xSym6_0_0".ref))
8298
])
8399
}
84100

85101
test("normalization: more complex identity annihilation") {
86-
with confluence(50)
87-
val program: Program = collect {
88-
with assertNoThrow[WrongFormat]
89-
with source[Char] { "(x=>x x=>(x x) x=>x)".each }
90-
compile!()
91-
}
92-
val redexes = box { program.redexes() }
93-
val (normalized, steps) = normalize(program, redexes, 10)
94-
assertEqual(steps, 5)
95-
assertEquivalent(list::collect[Constructor] { normalized() }, [
102+
"(x=>x x=>(x x) x=>x)".normalizeWith(Confluence(50), Steps(5), [
96103
Abstractor(Pos("xSym9_1_1".ref), Neg("xSym9_1_1".ref), Pos("xSym9_0_0".ref)),
97104
Initiator(Neg("xSym9_0_0".ref))
98105
])
99106
}
100107

101-
test("normalization: multi-arity identity annihilation") {
102-
with confluence(50)
103-
val program: Program = collect {
104-
with assertNoThrow[WrongFormat]
105-
with source[Char] { "(x=>(x x x x x x x x x) x=>x)".each }
106-
compile!()
107-
}
108-
val redexes = box { program.redexes() }
109-
val (normalized, steps) = normalize(program, redexes, 20)
110-
assertEqual(steps, 11)
111-
assertEquivalent(list::collect[Constructor] { normalized() }, [
112-
Abstractor(Pos("xSym20_8_8".ref), Neg("xSym20_8_8".ref), Pos("xSym20_7_7".ref)),
113-
Initiator(Neg("xSym20_7_7".ref))
108+
test("normalization: multi-dup identity annihilation") {
109+
"(x=>(x x x x x x x x x) x=>x)".normalizeWith(Confluence(50), Steps(11), [
110+
Abstractor(Pos("xSym9_1_1".ref), Neg("xSym9_1_1".ref), Pos("xSym9_0_0".ref)),
111+
Initiator(Neg("xSym9_0_0".ref))
114112
])
115113
}
116114

117115
test("normalization: church identity annihilation") {
118-
with confluence(50)
119-
val program: Program = collect {
120-
with assertNoThrow[WrongFormat]
121-
with source[Char] { "(s=>z=>(s (s (s (s (s (s z)))))) x=>x)".each }
122-
compile!()
123-
}
124-
val redexes = box { program.redexes() }
125-
val (normalized, steps) = normalize(program, redexes, 20)
126-
assertEqual(steps, 9)
127-
assertEquivalent(list::collect[Constructor] { normalized() }, [
116+
"(s=>z=>(s (s (s (s (s (s z)))))) x=>x)".normalizeWith(Confluence(50), Steps(9), [
128117
Abstractor(Pos("xSym9_1_1".ref), Neg("xSym9_1_1".ref), Pos("kAbs6".ref)),
129118
Initiator(Neg("kAbs6".ref))
130119
])
131120
}
132121

122+
// this broke once! but only because of different ordering, so TODO: better equivalence check
133123
test("normalization: church i* annihilation") {
134-
with confluence(50)
135-
val program: Program = collect {
136-
with assertNoThrow[WrongFormat]
137-
with source[Char] { "(s=>z=>(s (s (s (s (s (s z)))))) x=>y=>(x y))".each }
138-
compile!()
139-
}
140-
val redexes = box { program.redexes() }
141-
val (normalized, steps) = normalize(program, redexes, 20)
142-
assertEqual(steps, 17)
143-
assertEquivalent(list::collect[Constructor] { normalized() }, [ // x => y => (x y)
124+
"(s=>z=>(s (s (s (s (s (s z)))))) x=>y=>(x y))".normalizeWith(Confluence(50), Steps(17), [
144125
Applicator(Neg("xSym17_5_5".ref), Neg("ySym18_17_5".ref), Pos("kApp19_19_1".ref)), // (x y)
145126
Abstractor(Pos("ySym18_17_5".ref), Neg("kApp19_19_1".ref), Pos("kAbs20_6_0".ref)), // y =>
146127
Abstractor(Pos("xSym17_5_5".ref), Neg("kAbs20_6_0".ref), Pos("kAbs14".ref)), // x =>
@@ -149,16 +130,7 @@ def tests() = suite("└ ruler tests") {
149130
}
150131

151132
test("normalization: church bruijnification") {
152-
with confluence(50)
153-
val program: Program = collect {
154-
with assertNoThrow[WrongFormat]
155-
with source[Char] { "(s=>z=>(s (s z)) x=>y=>x)".each }
156-
compile!()
157-
}
158-
val redexes = box { program.redexes() }
159-
val (normalized, steps) = normalize(program, redexes, 20)
160-
assertEqual(steps, 7)
161-
assertEquivalent(list::collect[Constructor] { normalized() }, [ // x9_4 => y11_4 => y11_5 => x9_4
133+
"(s=>z=>(s (s z)) x=>y=>x)".normalizeWith(Confluence(50), Steps(7), [
162134
Duplicator(Neg("yEra11_4_0".ref), Nil(), 1),
163135
Duplicator(Neg("yEra11_5_1".ref), Nil(), 1),
164136
Abstractor(Pos("yEra11_4_0".ref), Neg("xSym9_0_0".ref), Pos("kAbs10_2_0".ref)), // y11_4 =>
@@ -169,32 +141,14 @@ def tests() = suite("└ ruler tests") {
169141
}
170142

171143
test("normalization: erasing church") {
172-
with confluence(50)
173-
val program: Program = collect {
174-
with assertNoThrow[WrongFormat]
175-
with source[Char] { "(x=>y=>y s=>z=>(s (s (s z))))".each }
176-
compile!()
177-
}
178-
val redexes = box { program.redexes() }
179-
val (normalized, steps) = normalize(program, redexes, 20)
180-
assertEqual(steps, 11)
181-
assertEquivalent(list::collect[Constructor] { normalized() }, [
144+
"(x=>y=>y s=>z=>(s (s (s z))))".normalizeWith(Confluence(50), Steps(11), [
182145
Abstractor(Pos("ySym1".ref), Neg("ySym1".ref), Pos("kAbs2".ref)),
183146
Initiator(Neg("kAbs2".ref))
184147
])
185148
}
186149

187150
test("normalization: s k k") {
188-
with confluence(50)
189-
val program: Program = collect {
190-
with assertNoThrow[WrongFormat]
191-
with source[Char] { "(x=>y=>z=>(x z (y z)) x=>y=>x x=>y=>x)".each }
192-
compile!()
193-
}
194-
val redexes = box { program.redexes() }
195-
val (normalized, steps) = normalize(program, redexes, 10)
196-
assertEqual(steps, 7)
197-
assertEquivalent(list::collect[Constructor] { normalized() }, [
151+
"(x=>y=>z=>(x z (y z)) x=>y=>x x=>y=>x)".normalizeWith(Confluence(50), Steps(7), [
198152
Duplicator(Neg("zSym5".ref), Nil(), 1),
199153
Duplicator(Neg("zDup9".ref), [Pos("zSym2".ref), Pos("zSym5".ref)], 0),
200154
Abstractor(Pos("zDup9".ref), Neg("zSym2".ref), Pos("kAbs8".ref)),
@@ -205,16 +159,7 @@ def tests() = suite("└ ruler tests") {
205159
val iota = "s=>(s x=>y=>z=>(x z (y z)) x=>y=>x)"
206160

207161
test("normalization: iota iota") {
208-
with confluence(50)
209-
val program: Program = collect {
210-
with assertNoThrow[WrongFormat]
211-
with source[Char] { s"(${iota} ${iota})".each }
212-
compile!()
213-
}
214-
val redexes = box { program.redexes() }
215-
val (normalized, steps) = normalize(program, redexes, 20)
216-
assertEqual(steps, 19)
217-
assertEquivalent(list::collect[Constructor] { normalized() }, [
162+
s"(${iota} ${iota})".normalizeWith(Confluence(50), Steps(19), [
218163
Duplicator(Neg("zDup29".ref), [Pos("zSym22".ref), Pos("zSym25".ref)], 2),
219164
Abstractor(Pos("zDup29".ref), Neg("zSym22".ref), Pos("kAbs28".ref)),
220165
Duplicator(Neg("zSym25".ref), [], 2),
@@ -223,16 +168,7 @@ def tests() = suite("└ ruler tests") {
223168
}
224169

225170
test("normalization: iota iota iota iota") {
226-
with confluence(50)
227-
val program: Program = collect {
228-
with assertNoThrow[WrongFormat]
229-
with source[Char] { s"(${iota} (${iota} (${iota} ${iota})))".each }
230-
compile!()
231-
}
232-
val redexes = box { program.redexes() }
233-
val (normalized, steps) = normalize(program, redexes, 70)
234-
assertEqual(steps, 67)
235-
assertEquivalent(list::collect[Constructor] { normalized() }, [
171+
s"(${iota} (${iota} (${iota} ${iota})))".normalizeWith(Confluence(50), Steps(67), [
236172
Duplicator(Neg("38".ref), Nil(), 1),
237173
Abstractor(Pos("38".ref), Neg("34".ref), Pos("36".ref)), // y => x
238174
Abstractor(Pos("34".ref), Neg("36".ref), Pos("32_0".ref)), // x =>

0 commit comments

Comments
 (0)