Skip to content

Commit a1d7676

Browse files
marvinbornermarvinborner
committed
Initiator and better dup
1 parent df56924 commit a1d7676

7 files changed

Lines changed: 110 additions & 42 deletions

File tree

‎lib/language/ic/ruler.effekt‎

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ def redexes(program: Program): Unit / emit[Redex] =
2828
with val ctorA = for { program() }
2929
with val ctorB = for { program() }
3030
if (ctorA.term::pp is Left(Neg(_)) and ctorB.term::pp is Right(Pos(_)))
31-
if (ctorA.pp.name == ctorB.pp.name)
31+
if (ctorA.canInteract && ctorB.canInteract && ctorA.pp.name == ctorB.pp.name)
3232
do emit(Redex(ctorA, ctorB))
3333

3434
def apply(port: SuperPort, substitutions: Ref[Map[SuperPort, SuperPort]]): SuperPort =
@@ -77,8 +77,8 @@ def interact(redex: Redex): Unit / { Rewrite, fresh } = redex match {
7777
case Redex(Duplicator(Neg(k1), ks, l), Abstractor(Pos(x), Neg(b), Pos(k2))) and k1 == k2 => {
7878
with on[OutOfBounds].panic() // can not happen
7979
val n = ks.size
80-
val xs = n.list::build { i => s"${do fresh().show}" }
81-
val bs = n.list::build { i => s"${do fresh().show}" }
80+
val xs = n.list::build { i => do fresh().show }
81+
val bs = n.list::build { i => do fresh().show }
8282
do construct(Superposer(Pos(x), xs.map { xi => Neg(xi) }, l))
8383
do construct(Duplicator(Neg(b), bs.map { bi => Pos(bi) }, l))
8484
0.each(n) { i =>
@@ -92,8 +92,8 @@ def interact(redex: Redex): Unit / { Rewrite, fresh } = redex match {
9292
case Redex(Applicator(Neg(f1), Neg(a), Pos(k)), Superposer(Pos(f2), fs, l)) and f1 == f2 => {
9393
with on[OutOfBounds].panic() // can not happen
9494
val n = fs.size
95-
val ks = n.list::build { i => s"${do fresh().show}" }
96-
val as = n.list::build { i => s"${do fresh().show}" }
95+
val ks = n.list::build { i => do fresh().show }
96+
val as = n.list::build { i => do fresh().show }
9797
do construct(Superposer(Pos(k), ks.map { ki => Neg(ki) }, l))
9898
do construct(Duplicator(Neg(a), as.map { ai => Pos(ai) }, l))
9999
0.each(n) { i =>
@@ -133,28 +133,26 @@ def interact(redex: Redex): Unit / { Rewrite, fresh } = redex match {
133133
with on[OutOfBounds].panic() // can not happen
134134
val n = out.size
135135
val m = ins.size
136+
val fresh = max(n, m).list::build { _ => do fresh().show }
136137
0.each(m) { i => // duplicators
137-
val outM = n.list::build { j =>
138-
Pos(s"${do fresh().show}")
139-
}
138+
val outM = n.list::build { j => Pos(s"${fresh.get(i)}_${j.show}") }
140139
do construct(Duplicator(ins.get(i), outM, l1))
141140
}
142141
0.each(n) { i => // superposers
143-
val insN = m.list::build { j =>
144-
Neg(s"${do fresh().show}")
145-
}
142+
val insN = m.list::build { j => Neg(s"${fresh.get(j)}_${i.show}") }
146143
do construct(Superposer(out.get(i), insN, l2))
147144
}
148145
}
149146

150147
case _ => {
151-
// inspect(redex)
148+
inspect(redex)
152149
panic("invalid redex")
153150
}
154151
}
155152

156153
def step_(program: Program, redex: Redex): Unit / { emit[Constructor], fresh } = {
157154
val annihilated = ref[Set[Constructor]](emptyGeneric())
155+
val constructed = ref[Set[Constructor]](emptyGeneric())
158156
val substitutions = ref[Map[SuperPort, SuperPort]](emptyGeneric())
159157

160158
try {
@@ -188,18 +186,21 @@ def choose(mode: StepMode, redexes: RedexBag): Redex / fail = mode match {
188186
// TODO: emit new redexes directly during interactions (wires get reconnected, check if same port)
189187
def step(program: Program, mode: StepMode, redexes: RedexBag): Unit / { emit[Constructor], emit[Redex], fresh, fail } = {
190188
val redex = choose(mode, redexes)
191-
// println("\nREDEX: " ++ redex.left.show ++ " - " ++ redex.right.show)
192189
val program: Program = collect { program.step_(redex) }
193190

194191
// println(list::collect[Constructor] { program() }.show { ctor => ctor.show })
195192

196-
// val posPorts = collect[Constructor] { program() }.flatMap { ctor => ctor.ports }.filter { p => p.isPos }
197-
// val negPorts = collect[Constructor] { program() }.flatMap { ctor => ctor.ports }.filter { p => p.isNeg }
198-
// if (posPorts.size != negPorts.size + 1)
199-
// println(s"\n!!! Pos ${posPorts.size.show} != Neg ${negPorts.size.show}: " ++ posPorts.show { p => p.name } ++ " vs " ++ negPorts.show { p => p.name })
200-
201-
program.redexes() // TODO: this could be an expensive call, we should not do it at every step.
202-
program()
193+
// only for debugging
194+
val posPorts = collect[Constructor] { program() }.flatMap { ctor => ctor.ports }.filter { p => p.isPos }.map { p => p.name }.set::fromListGeneric
195+
val negPorts = collect[Constructor] { program() }.flatMap { ctor => ctor.ports }.filter { p => p.isNeg }.map { p => p.name }.set::fromListGeneric
196+
if (posPorts.difference(negPorts).size != 0) {
197+
println("\n!!! FATAL " ++ posPorts.toList.show ++ " vs " ++ negPorts.toList.show)
198+
println("\nREDEX: " ++ redex.left.show ++ " - " ++ redex.right.show)
199+
println(posPorts.difference(negPorts).toList.show)
200+
} else {
201+
program.redexes() // TODO: this could be an expensive call, we should not do it at every step.
202+
program()
203+
}
203204
}
204205

205206
def normalize(program: Program, redexes: RedexBag, max: Int): (Program, Int) = {
@@ -214,4 +215,4 @@ def normalize(program: Program, redexes: RedexBag, max: Int): (Program, Int) = {
214215
collect { state.first.step(NonDeterministic(), state.second) } }
215216
if (count > max) do fail()
216217
(state.first, count)
217-
}
218+
}

‎lib/language/ic/term.effekt‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ def map(port: Neg) { f: Port => Port }: Neg = Neg(port.name.f)
4444
// def negate(port: Port) = port.map { pol => pol.negate }
4545

4646
type Constructor {
47+
Initiator(k: Neg);
4748
Abstractor(x: Pos, b: Neg, k: Pos);
4849
Applicator(f: Neg, a: Neg, k: Pos);
4950
Duplicator(o: Neg, ins: List[Pos], label: Int);
@@ -54,20 +55,27 @@ type Constructor {
5455
// def delta(pp: Port, aux: List[Port], label: Int): A
5556
// }
5657

58+
def canInteract(ctor: Constructor) = ctor match{
59+
case Initiator(k) => false
60+
case _ => true
61+
}
62+
5763
type Program = => Unit / emit[Constructor] at {}
5864
def empty(): Program = box {}
5965

6066
record Redex(left: Constructor, right: Constructor) // pp: (-, +)
6167
type RedexBag = => Unit / emit[Redex] at {}
6268

6369
def pp(ctor: Constructor): SuperPort = ctor match {
70+
case Initiator(k) => k.super
6471
case Abstractor(x, b, k) => k.super
6572
case Applicator(f, a, k) => f.super
6673
case Duplicator(o, ins, label) => o.super
6774
case Superposer(i, out, label) => i.super
6875
}
6976

7077
def aux(ctor: Constructor): List[SuperPort] = ctor match {
78+
case Initiator(k) => []
7179
case Abstractor(x, b, k) => [x.super, b.super]
7280
case Applicator(f, a, k) => [a.super, k.super]
7381
case Duplicator(o, ins, label) => ins.map { i => i.super }
@@ -77,6 +85,7 @@ def aux(ctor: Constructor): List[SuperPort] = ctor match {
7785
def ports(ctor: Constructor): List[SuperPort] = Cons(ctor.pp, ctor.aux)
7886

7987
def map(ctor: Constructor) { func: SuperPort => Port }: Constructor = ctor match {
88+
case Initiator(k) => Initiator(Neg(k.super.func))
8089
case Abstractor(x, b, k) => Abstractor(Pos(x.super.func), Neg(b.super.func), Pos(k.super.func))
8190
case Applicator(f, a, k) => Applicator(Neg(f.super.func), Neg(a.super.func), Pos(k.super.func))
8291
case Duplicator(i, out, label) => Duplicator(Neg(i.super.func), out.map { s => Pos(s.super.func) }, label)
@@ -91,6 +100,7 @@ def map(ctor: Constructor) { func: SuperPort => Port }: Constructor = ctor match
91100
// }
92101

93102
def kind(ctor: Constructor): Kind = ctor match {
103+
case Initiator(k) => LightTriangle()
94104
case Abstractor(x, b, k) => LightTriangle()
95105
case Applicator(f, a, k) => LightTriangle()
96106
case Duplicator(o, ins, label) => DarkTriangle()
@@ -109,6 +119,7 @@ def show(ctor: Constructor) = {
109119
def pretty(many: List[Pos]) = many.map { p => p.show() }.join(", ")
110120
def pretty(many: List[Neg]) = many.map { p => p.show() }.join(", ")
111121
ctor match {
122+
case Initiator(k) => s"ι(${k.show})"
112123
case Abstractor(x, b, k) => s"λ(${x.show}, ${b.show}, ${k.show})"
113124
case Applicator(f, a, k) => s"@(${f.show}, ${a.show}, ${k.show})"
114125
case Duplicator(o, ins, label) => s"δ(${o.show}, ${ins.pretty})(${label.show})"

‎lib/language/lc/netter.effekt‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,4 +70,5 @@ def net!(): Unit / { Exception[WrongFormat], read[Term], emit[Constructor] } = {
7070

7171
if (context.bindings.size > 0)
7272
wrongFormat("term is open: " ++ context.bindings.keys.join(", "))
73-
}
73+
do emit(Initiator(Neg(context.out)))
74+
}

‎lib/utils.effekt‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,12 @@ def collapse[A, B, R](port: Either[A, B]) { left: A => R } { right: B => R }: R
99
case Right(b) => right(b)
1010
}
1111

12+
// println without the ln: only for jsNode, of course
13+
extern def print(s: String) at io: Unit =
14+
jsNode "process.stdout.write(${s})"
15+
jsWeb "console.log(${s})"
16+
default { println(s) }
17+
1218
def size[A] { s: => Unit / emit[A] }: Int = {
1319
var size = 0
1420
try s()
@@ -26,6 +32,12 @@ def choose[A] { stream: () => Unit / emit[A] }: A / fail =
2632
else resume(())
2733
}
2834

35+
def init[A](l: List[A]): List[A] / Exception[MissingValue] = l match {
36+
case Nil() => do raise(MissingValue(), "Trying to get the beginning of an empty list")
37+
case Cons(a, Nil()) => Nil()
38+
case Cons(a, as) => Cons(a, as.init)
39+
}
40+
2941
def exhaustively[R](init: R) { program: () => R / fail }: R =
3042
var res: R = init
3143
try {
@@ -37,3 +49,15 @@ def exhaustively[R](init: R) { program: () => R / fail }: R =
3749
} with fail {
3850
res
3951
}
52+
53+
def assertNotThrown[E](ex: on[E]) { body: => Unit / Exception[E] }: Unit / Assertion =
54+
ex.default { do assert(false, "Unexpected Exception") } {body}
55+
56+
def assertNoThrow[E] { body: => Unit / Exception[E] }: Unit / Assertion =
57+
on[E].default{ do assert(false, "Unexpected Exception") } {body}
58+
59+
def assertThrown[E](ex: on[E]) { body: => Unit / Exception[E] }: Unit / Assertion =
60+
do assert(ex.default { true } { body(); false }, "Expected Exception, but exited normally")
61+
62+
def assertThrows[E] { body: => Unit / Exception[E] }: Unit / Assertion =
63+
do assert(on[E].default { true } { body(); false }, "Expected Exception, but exited normally")

‎test/lc.effekt‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ def tests() = suite("└ lc tests") {
2020
compile!()
2121
}
2222
assertEqual(ctors, [
23-
Abstractor(Pos("xSym1"), Neg("xSym1"), Pos("kAbs2"))]) // (x => x)_k
23+
Abstractor(Pos("xSym1"), Neg("xSym1"), Pos("kAbs2")), // (x => x)_k
24+
Initiator(Neg("kAbs2"))])
2425
}
2526

2627
test("lc compilation: identity annihilation") {
@@ -30,9 +31,10 @@ def tests() = suite("└ lc tests") {
3031
compile!()
3132
}
3233
assertEqual(ctors, [
33-
Abstractor(Pos("xSym1"), Neg("xSym1"), Pos("kAbs2")), // (x => x1)_k
34-
Abstractor(Pos("ySym3"), Neg("ySym3"), Pos("kAbs4")), // (y => y1)_k5
35-
Applicator(Neg("kAbs2"), Neg("kAbs4"), Pos("kApp5"))]) // (k2 k5)_k7
34+
Abstractor(Pos("xSym1"), Neg("xSym1"), Pos("kAbs2")), // (x => x1)_k
35+
Abstractor(Pos("ySym3"), Neg("ySym3"), Pos("kAbs4")), // (y => y1)_k5
36+
Applicator(Neg("kAbs2"), Neg("kAbs4"), Pos("kApp5")), // (k2 k5)_k7
37+
Initiator(Neg("kApp5"))])
3638
}
3739

3840
// test("lc compilation: omega") {
@@ -93,4 +95,4 @@ def tests() = suite("└ lc tests") {
9395
// compile!()
9496
// }
9597
// }
96-
}
98+
}

‎test/net.effekt‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ def tests() = suite("└ net tests") {
3939
}
4040
net!()
4141
}
42-
assertEqual(net.agents.clean, [("kAbs2", 0, [2, 3], LightTriangle())])
43-
assertEqual(net.wires, [Wire(2, 3)])
42+
assertEqual(net.agents.clean, [("kAbs2", 0, [2, 3], LightTriangle()), ("kAbs2", 1, Nil(), LightTriangle())])
43+
assertEqual(net.wires, [Wire(2, 3), Wire(0, 1)])
4444
}
4545

4646
test("netting: working stream splitting") {
@@ -54,9 +54,9 @@ def tests() = suite("└ net tests") {
5454
}
5555

5656
val agents: List[Agent] = collect { agents { net() } }
57-
assertEqual(agents.clean, [("kAbs2", 0, [2, 3], LightTriangle())])
57+
assertEqual(agents.clean, [("kAbs2", 0, [2, 3], LightTriangle()), ("kAbs2", 1, Nil(), LightTriangle())])
5858

5959
val wires: List[Wire] = collect { wires { net() } }
60-
assertEqual(wires, [Wire(2, 3)])
60+
assertEqual(wires, [Wire(2, 3), Wire(0, 1)])
6161
}
62-
}
62+
}

‎test/ruler.effekt‎

Lines changed: 39 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ def assertEquivalent(bs: List[Constructor], as: List[Constructor]): Unit / { For
3838
case (Superposer(Pos(i1), out1, label1), Superposer(Pos(i2), out2, label2)) =>
3939
assertEqual(out1.size, out2.size)
4040
assertEqual(label1, label2)
41+
case (Initiator(Neg(k1)), Initiator(Neg(k2))) => ()
4142
case (_, _) => assertEqual(as, bs) // will fail, but we'll see why
4243
}
4344
assertEqual(as.size, bs.size)
@@ -60,7 +61,8 @@ def tests() = suite("└ ruler tests") {
6061
val (normalized, steps) = normalize(program, redexes, 10)
6162
assertEqual(steps, 1)
6263
assertEquivalent(list::collect[Constructor] { normalized() }, [
63-
Abstractor(Pos("xSym3"), Neg("xSym3"), Pos("xSym1"))
64+
Abstractor(Pos("xSym3"), Neg("xSym3"), Pos("xSym1")),
65+
Initiator(Neg("xSym1"))
6466
])
6567
}
6668

@@ -75,7 +77,8 @@ def tests() = suite("└ ruler tests") {
7577
val (normalized, steps) = normalize(program, redexes, 10)
7678
assertEqual(steps, 4)
7779
assertEquivalent(list::collect[Constructor] { normalized() }, [
78-
Abstractor(Pos("xSym6_1_1"), Neg("xSym6_1_1"), Pos("xSym6_0_0"))
80+
Abstractor(Pos("xSym6_1_1"), Neg("xSym6_1_1"), Pos("xSym6_0_0")),
81+
Initiator(Neg("xSym6_0_0"))
7982
])
8083
}
8184

@@ -90,7 +93,8 @@ def tests() = suite("└ ruler tests") {
9093
val (normalized, steps) = normalize(program, redexes, 10)
9194
assertEqual(steps, 5)
9295
assertEquivalent(list::collect[Constructor] { normalized() }, [
93-
Abstractor(Pos("xSym9_1_1"), Neg("xSym9_1_1"), Pos("xSym9_0_0"))
96+
Abstractor(Pos("xSym9_1_1"), Neg("xSym9_1_1"), Pos("xSym9_0_0")),
97+
Initiator(Neg("xSym9_0_0"))
9498
])
9599
}
96100

@@ -105,7 +109,8 @@ def tests() = suite("└ ruler tests") {
105109
val (normalized, steps) = normalize(program, redexes, 20)
106110
assertEqual(steps, 11)
107111
assertEquivalent(list::collect[Constructor] { normalized() }, [
108-
Abstractor(Pos("xSym20_8_8"), Neg("xSym20_8_8"), Pos("xSym20_7_7"))
112+
Abstractor(Pos("xSym20_8_8"), Neg("xSym20_8_8"), Pos("xSym20_7_7")),
113+
Initiator(Neg("xSym20_7_7"))
109114
])
110115
}
111116

@@ -120,7 +125,8 @@ def tests() = suite("└ ruler tests") {
120125
val (normalized, steps) = normalize(program, redexes, 20)
121126
assertEqual(steps, 9)
122127
assertEquivalent(list::collect[Constructor] { normalized() }, [
123-
Abstractor(Pos("xSym9_1_1"), Neg("xSym9_1_1"), Pos("kAbs6"))
128+
Abstractor(Pos("xSym9_1_1"), Neg("xSym9_1_1"), Pos("kAbs6")),
129+
Initiator(Neg("kAbs6"))
124130
])
125131
}
126132

@@ -137,7 +143,8 @@ def tests() = suite("└ ruler tests") {
137143
assertEquivalent(list::collect[Constructor] { normalized() }, [ // x => y => (x y)
138144
Applicator(Neg("xSym17_5_5"), Neg("ySym18_17_5"), Pos("kApp19_19_1")), // (x y)
139145
Abstractor(Pos("ySym18_17_5"), Neg("kApp19_19_1"), Pos("kAbs20_6_0")), // y =>
140-
Abstractor(Pos("xSym17_5_5"), Neg("kAbs20_6_0"), Pos("kAbs14")) // x =>
146+
Abstractor(Pos("xSym17_5_5"), Neg("kAbs20_6_0"), Pos("kAbs14")), // x =>
147+
Initiator(Neg("kAbs14"))
141148
])
142149
}
143150

@@ -156,7 +163,8 @@ def tests() = suite("└ ruler tests") {
156163
Duplicator(Neg("yEra11_5_1"), Nil(), 1),
157164
Abstractor(Pos("yEra11_4_0"), Neg("xSym9_0_0"), Pos("kAbs10_2_0")), // y11_4 =>
158165
Abstractor(Pos("yEra11_5_1"), Neg("xSym9_1_1"), Pos("xSym9_0_0")), // y11_5 =>
159-
Abstractor(Pos("xSym9_1_1"), Neg("kAbs10_2_0"), Pos("kAbs6")) // x9 =>
166+
Abstractor(Pos("xSym9_1_1"), Neg("kAbs10_2_0"), Pos("kAbs6")), // x9 =>
167+
Initiator(Neg("kAbs6"))
160168
])
161169
}
162170

@@ -171,7 +179,8 @@ def tests() = suite("└ ruler tests") {
171179
val (normalized, steps) = normalize(program, redexes, 20)
172180
assertEqual(steps, 11)
173181
assertEquivalent(list::collect[Constructor] { normalized() }, [
174-
Abstractor(Pos("ySym1"), Neg("ySym1"), Pos("kAbs2"))
182+
Abstractor(Pos("ySym1"), Neg("ySym1"), Pos("kAbs2")),
183+
Initiator(Neg("kAbs2"))
175184
])
176185
}
177186

@@ -188,7 +197,8 @@ def tests() = suite("└ ruler tests") {
188197
assertEquivalent(list::collect[Constructor] { normalized() }, [
189198
Duplicator(Neg("zSym5"), Nil(), 1),
190199
Duplicator(Neg("zDup9"), [Pos("zSym2"), Pos("zSym5")], 0),
191-
Abstractor(Pos("zDup9"), Neg("zSym2"), Pos("kAbs8"))
200+
Abstractor(Pos("zDup9"), Neg("zSym2"), Pos("kAbs8")),
201+
Initiator(Neg("kAbs8"))
192202
])
193203
}
194204

@@ -207,7 +217,26 @@ def tests() = suite("└ ruler tests") {
207217
assertEquivalent(list::collect[Constructor] { normalized() }, [
208218
Duplicator(Neg("zDup29"), [Pos("zSym22"), Pos("zSym25")], 2),
209219
Abstractor(Pos("zDup29"), Neg("zSym22"), Pos("kAbs28")),
210-
Duplicator(Neg("zSym25"), [], 2)
220+
Duplicator(Neg("zSym25"), [], 2),
221+
Initiator(Neg("kAbs28"))
222+
])
223+
}
224+
225+
test("normalization: iota iota iota iota") {
226+
with confluence
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, 63)
235+
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"))
211240
])
212241
}
213242
}

0 commit comments

Comments
 (0)