Skip to content

Commit fe0b61c

Browse files
marvinbornermarvinborner
committed
Substitution via union-find
1 parent cc2f375 commit fe0b61c

2 files changed

Lines changed: 74 additions & 60 deletions

File tree

‎lib/language/ic/ruler.effekt‎

Lines changed: 34 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ def freshener[R] { prog: => R / fresh }: R = {
2323
interface Interact {
2424
def annihilate(ctor: Constructor): Unit
2525
def construct(ctor: Constructor): Unit
26-
def substitute(substitution: Substitution): Unit
26+
def rewire(rewiring: Map[String, Substitution]): Unit
2727

2828
def potential(port: PortRef): Unit
2929
def target(from: String): SuperPort
@@ -59,8 +59,10 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
5959
// @(f-, a-, k+) <> λ(x+, b-, f+) ~> [a-/x-][b-/k-]
6060
// beta-reduction: APP-LAM
6161
case Redex(Applicator(Neg(f1), Neg(a), Pos(k)), Abstractor(Pos(x), Neg(b), Pos(f2))) and f1 == f2 => {
62-
do substitute(Substitution(Neg(a).super, do target(Pos(x).show)))
63-
do substitute(Substitution(Neg(b).super, do target(Pos(k).show)))
62+
do rewire([
63+
(Neg(a).show, Substitution(Neg(a).super, do target(Pos(x).show))),
64+
(Neg(b).show, Substitution(Neg(b).super, do target(Pos(k).show)))
65+
].map::fromListGeneric)
6466
do potential(a) // TODO: theoretically, we'd only need to somehow check if Neg(a) is at a principal port
6567
do potential(b)
6668
}
@@ -122,11 +124,11 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
122124
// δ(k-, o1+, ..., on+) <> σ(k+, i1-, ..., im-) ~> [i1-/o1-]...[in-/on-]
123125
// symmetric duplicator annihilation: DUP-SUP
124126
case Redex(Duplicator(Neg(k1), out, l1), Superposer(Pos(k2), ins, l2)) and k1 == k2 and l1 == l2 and out.size == ins.size => {
125-
list::zip(out, ins).foreach { case (o, i) =>
126-
// TODO: pre-substitute
127-
do substitute(Substitution(i.super, do target(o.show)))
127+
val rewiring = out.zip(ins).map { case (o, i) =>
128128
do potential(i.port)
129-
}
129+
(i.show, Substitution(i.super, do target(o.show)))
130+
}.map::fromListGeneric
131+
do rewire(rewiring)
130132
}
131133

132134
// δ(k-, o1+, ..., on+) <> σ(k+, i1-, ..., im-) ~> δ(i1-, o11+, ..., o1n+), .m., δ(im-, om1+, ..., omn+),
@@ -181,13 +183,29 @@ def wiring(program: Program): Map[String, SuperPort] = {
181183
wiring
182184
}
183185

184-
def substitute(substitution: Substitution, wiring: Ref[Map[String, SuperPort]]) = {
185-
val Substitution(from, to) = substitution
186-
println(s"[${from.show}/${to.show}]")
187-
// val x = to.port.get
188-
to.port.set(from.port.get)
189-
// from.port.set(x)
190-
wiring.map { w => w.put(to.show, from).put(from.show, to) }
186+
def unionFind(rewiring: Ref[Map[String, Substitution]], to: SuperPort): SuperPort = {
187+
val substitution = rewiring.get.get(to.show)
188+
substitution match {
189+
case Some(Substitution(from, target)) and target.show != to.show =>
190+
val root = rewiring.unionFind(target)
191+
rewiring.map { w => w.delete(from.show) }
192+
root
193+
case _ =>
194+
to
195+
}
196+
}
197+
198+
def rewire(wiring: Ref[Map[String, SuperPort]], _rewiring: Map[String, Substitution]) = {
199+
val rewiring = ref(_rewiring)
200+
_rewiring.values.foreach { case Substitution(from, _to) => // pre-substitute
201+
val to = rewiring.unionFind(_to)
202+
if (to.show != _to.show)
203+
rewiring.map { w => w.put(from.show, Substitution(from, to)) }
204+
}
205+
rewiring.get.values.foreach { case Substitution(from, to) => // substitute
206+
to.port.set(from.port.get)
207+
wiring.map { w => w.put(to.show, from).put(from.show, to) }
208+
}
191209
}
192210

193211
def step_(program: Program, redex: Redex): List[PortRef] / { emit[Constructor], fresh } = {
@@ -196,25 +214,21 @@ def step_(program: Program, redex: Redex): List[PortRef] / { emit[Constructor],
196214
val potential = ref[List[PortRef]](Nil())
197215
val wiring = ref(program.wiring())
198216

199-
println(program.show)
200-
201217
try {
202218
redex.interact()
203219
do annihilate(redex.left)
204220
do annihilate(redex.right)
205221
} with Interact {
206222
def annihilate(ctor) = resume(annihilated.map { s => s.insert(ctor) })
207223
def construct(ctor) = resume(do emit(ctor))
208-
def substitute(substitution) = resume(substitution.substitute(wiring))
209224
def potential(port) = resume(potential.map { l => Cons(port, l) })
210225
def target(from) = resume(wiring.get.getOrElse(from) { panic(s"invalid target: ${from.show}") })
211226
def wire(from, to) = resume(wiring.map { w => w.put(from.show, to.super).put(to.show, from.super) })
227+
def rewire(rewiring) = resume(wiring.rewire(rewiring))
212228
}
213229

214-
println("\nemitting:")
215230
for { program() } { ctor =>
216231
if (not(annihilated.get.contains(ctor))) {
217-
println(ctor.show)
218232
do emit(ctor)
219233
}
220234
}
@@ -241,7 +255,7 @@ def pop(mode: StepMode, redexes: RedexBag): Redex / { fail, emit[Redex] } = mode
241255
def step(program: Program, mode: StepMode, redexes: RedexBag): Unit / { emit[Constructor], emit[Redex], fresh, fail } = {
242256
//val redex = pop(mode, redexes) // TODO!
243257
val redex = pop(NonDeterministic(), redexes)
244-
println(s"\n=== REDEX: ${redex.show} ===")
258+
// println(s"\n=== REDEX: ${redex.show} ===")
245259
val tup: (List[PortRef], Program) = returning::collect { program.step_(redex) }
246260
val (potential, program) = tup
247261

‎test/ruler.effekt‎

Lines changed: 40 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ import lib/language/ic/term
1010
import lib/language/ic/ruler
1111

1212
// normalize is non-deterministic
13-
def confluence { test: => Unit / Assertion }: Unit / Assertion = {
14-
0.each(50) { i =>
13+
def confluence(n: Int) { test: => Unit / Assertion }: Unit / Assertion = {
14+
0.each(n) { i =>
1515
try test()
1616
with Assertion {
1717
def assert(condition, msg) = do assert(condition, s"${msg} (run number ${i.show})")
@@ -46,7 +46,7 @@ def assertEquivalent(bs: List[Constructor], as: List[Constructor]): Unit / { For
4646

4747
def tests() = suite("└ ruler tests") {
4848
test("normalization: identity application") {
49-
with confluence
49+
with confluence(5)
5050
val program: Program = collect {
5151
with assertNoThrow[WrongFormat]
5252
with source[Char] { "(x=>x x=>x)".each }
@@ -67,7 +67,7 @@ def tests() = suite("└ ruler tests") {
6767
}
6868

6969
test("normalization: identity duplication") {
70-
with confluence
70+
with confluence(5)
7171
val program: Program = collect {
7272
with assertNoThrow[WrongFormat]
7373
with source[Char] { "(x=>(x x) x=>x)".each }
@@ -83,7 +83,7 @@ def tests() = suite("└ ruler tests") {
8383
}
8484

8585
test("normalization: more complex identity annihilation") {
86-
with confluence
86+
with confluence(50)
8787
val program: Program = collect {
8888
with assertNoThrow[WrongFormat]
8989
with source[Char] { "(x=>x x=>(x x) x=>x)".each }
@@ -99,7 +99,7 @@ def tests() = suite("└ ruler tests") {
9999
}
100100

101101
test("normalization: multi-arity identity annihilation") {
102-
with confluence
102+
with confluence(50)
103103
val program: Program = collect {
104104
with assertNoThrow[WrongFormat]
105105
with source[Char] { "(x=>(x x x x x x x x x) x=>x)".each }
@@ -115,7 +115,7 @@ def tests() = suite("└ ruler tests") {
115115
}
116116

117117
test("normalization: church identity annihilation") {
118-
with confluence
118+
with confluence(50)
119119
val program: Program = collect {
120120
with assertNoThrow[WrongFormat]
121121
with source[Char] { "(s=>z=>(s (s (s (s (s (s z)))))) x=>x)".each }
@@ -130,8 +130,8 @@ def tests() = suite("└ ruler tests") {
130130
])
131131
}
132132

133-
/*test("normalization: church i* annihilation") {
134-
with confluence
133+
test("normalization: church i* annihilation") {
134+
with confluence(50)
135135
val program: Program = collect {
136136
with assertNoThrow[WrongFormat]
137137
with source[Char] { "(s=>z=>(s (s (s (s (s (s z)))))) x=>y=>(x y))".each }
@@ -141,15 +141,15 @@ def tests() = suite("└ ruler tests") {
141141
val (normalized, steps) = normalize(program, redexes, 20)
142142
assertEqual(steps, 17)
143143
assertEquivalent(list::collect[Constructor] { normalized() }, [ // x => y => (x y)
144-
Applicator(Neg("xSym17_5_5"), Neg("ySym18_17_5"), Pos("kApp19_19_1")), // (x y)
145-
Abstractor(Pos("ySym18_17_5"), Neg("kApp19_19_1"), Pos("kAbs20_6_0")), // y =>
146-
Abstractor(Pos("xSym17_5_5"), Neg("kAbs20_6_0"), Pos("kAbs14")), // x =>
147-
Initiator(Neg("kAbs14"))
144+
Applicator(Neg("xSym17_5_5".ref), Neg("ySym18_17_5".ref), Pos("kApp19_19_1".ref)), // (x y)
145+
Abstractor(Pos("ySym18_17_5".ref), Neg("kApp19_19_1".ref), Pos("kAbs20_6_0".ref)), // y =>
146+
Abstractor(Pos("xSym17_5_5".ref), Neg("kAbs20_6_0".ref), Pos("kAbs14".ref)), // x =>
147+
Initiator(Neg("kAbs14".ref))
148148
])
149149
}
150150

151151
test("normalization: church bruijnification") {
152-
with confluence
152+
with confluence(50)
153153
val program: Program = collect {
154154
with assertNoThrow[WrongFormat]
155155
with source[Char] { "(s=>z=>(s (s z)) x=>y=>x)".each }
@@ -159,17 +159,17 @@ def tests() = suite("└ ruler tests") {
159159
val (normalized, steps) = normalize(program, redexes, 20)
160160
assertEqual(steps, 7)
161161
assertEquivalent(list::collect[Constructor] { normalized() }, [ // x9_4 => y11_4 => y11_5 => x9_4
162-
Duplicator(Neg("yEra11_4_0"), Nil(), 1),
163-
Duplicator(Neg("yEra11_5_1"), Nil(), 1),
164-
Abstractor(Pos("yEra11_4_0"), Neg("xSym9_0_0"), Pos("kAbs10_2_0")), // y11_4 =>
165-
Abstractor(Pos("yEra11_5_1"), Neg("xSym9_1_1"), Pos("xSym9_0_0")), // y11_5 =>
166-
Abstractor(Pos("xSym9_1_1"), Neg("kAbs10_2_0"), Pos("kAbs6")), // x9 =>
167-
Initiator(Neg("kAbs6"))
162+
Duplicator(Neg("yEra11_4_0".ref), Nil(), 1),
163+
Duplicator(Neg("yEra11_5_1".ref), Nil(), 1),
164+
Abstractor(Pos("yEra11_4_0".ref), Neg("xSym9_0_0".ref), Pos("kAbs10_2_0".ref)), // y11_4 =>
165+
Abstractor(Pos("yEra11_5_1".ref), Neg("xSym9_1_1".ref), Pos("xSym9_0_0".ref)), // y11_5 =>
166+
Abstractor(Pos("xSym9_1_1".ref), Neg("kAbs10_2_0".ref), Pos("kAbs6".ref)), // x9 =>
167+
Initiator(Neg("kAbs6".ref))
168168
])
169169
}
170170

171171
test("normalization: erasing church") {
172-
with confluence
172+
with confluence(50)
173173
val program: Program = collect {
174174
with assertNoThrow[WrongFormat]
175175
with source[Char] { "(x=>y=>y s=>z=>(s (s (s z))))".each }
@@ -179,13 +179,13 @@ def tests() = suite("└ ruler tests") {
179179
val (normalized, steps) = normalize(program, redexes, 20)
180180
assertEqual(steps, 11)
181181
assertEquivalent(list::collect[Constructor] { normalized() }, [
182-
Abstractor(Pos("ySym1"), Neg("ySym1"), Pos("kAbs2")),
183-
Initiator(Neg("kAbs2"))
182+
Abstractor(Pos("ySym1".ref), Neg("ySym1".ref), Pos("kAbs2".ref)),
183+
Initiator(Neg("kAbs2".ref))
184184
])
185185
}
186186

187187
test("normalization: s k k") {
188-
with confluence
188+
with confluence(50)
189189
val program: Program = collect {
190190
with assertNoThrow[WrongFormat]
191191
with source[Char] { "(x=>y=>z=>(x z (y z)) x=>y=>x x=>y=>x)".each }
@@ -195,17 +195,17 @@ def tests() = suite("└ ruler tests") {
195195
val (normalized, steps) = normalize(program, redexes, 10)
196196
assertEqual(steps, 7)
197197
assertEquivalent(list::collect[Constructor] { normalized() }, [
198-
Duplicator(Neg("zSym5"), Nil(), 1),
199-
Duplicator(Neg("zDup9"), [Pos("zSym2"), Pos("zSym5")], 0),
200-
Abstractor(Pos("zDup9"), Neg("zSym2"), Pos("kAbs8")),
201-
Initiator(Neg("kAbs8"))
198+
Duplicator(Neg("zSym5".ref), Nil(), 1),
199+
Duplicator(Neg("zDup9".ref), [Pos("zSym2".ref), Pos("zSym5".ref)], 0),
200+
Abstractor(Pos("zDup9".ref), Neg("zSym2".ref), Pos("kAbs8".ref)),
201+
Initiator(Neg("kAbs8".ref))
202202
])
203203
}
204204

205205
val iota = "s=>(s x=>y=>z=>(x z (y z)) x=>y=>x)"
206206

207207
test("normalization: iota iota") {
208-
with confluence
208+
with confluence(50)
209209
val program: Program = collect {
210210
with assertNoThrow[WrongFormat]
211211
with source[Char] { s"(${iota} ${iota})".each }
@@ -215,28 +215,28 @@ def tests() = suite("└ ruler tests") {
215215
val (normalized, steps) = normalize(program, redexes, 20)
216216
assertEqual(steps, 19)
217217
assertEquivalent(list::collect[Constructor] { normalized() }, [
218-
Duplicator(Neg("zDup29"), [Pos("zSym22"), Pos("zSym25")], 2),
219-
Abstractor(Pos("zDup29"), Neg("zSym22"), Pos("kAbs28")),
220-
Duplicator(Neg("zSym25"), [], 2),
221-
Initiator(Neg("kAbs28"))
218+
Duplicator(Neg("zDup29".ref), [Pos("zSym22".ref), Pos("zSym25".ref)], 2),
219+
Abstractor(Pos("zDup29".ref), Neg("zSym22".ref), Pos("kAbs28".ref)),
220+
Duplicator(Neg("zSym25".ref), [], 2),
221+
Initiator(Neg("kAbs28".ref))
222222
])
223223
}
224224

225225
test("normalization: iota iota iota iota") {
226-
with confluence
226+
with confluence(50)
227227
val program: Program = collect {
228228
with assertNoThrow[WrongFormat]
229229
with source[Char] { s"(${iota} (${iota} (${iota} ${iota})))".each }
230230
compile!()
231231
}
232232
val redexes = box { program.redexes() }
233233
val (normalized, steps) = normalize(program, redexes, 70)
234-
assertEqual(steps, 63)
234+
assertEqual(steps, 67)
235235
assertEquivalent(list::collect[Constructor] { normalized() }, [
236-
Duplicator(Neg("38"), Nil(), 1),
237-
Abstractor(Pos("38"), Neg("34"), Pos("36")), // y => x
238-
Abstractor(Pos("34"), Neg("36"), Pos("32_0")), // x =>
239-
Initiator(Neg("32_0"))
236+
Duplicator(Neg("38".ref), Nil(), 1),
237+
Abstractor(Pos("38".ref), Neg("34".ref), Pos("36".ref)), // y => x
238+
Abstractor(Pos("34".ref), Neg("36".ref), Pos("32_0".ref)), // x =>
239+
Initiator(Neg("32_0".ref))
240240
])
241-
}*/
241+
}
242242
}

0 commit comments

Comments
 (0)