Skip to content

Commit 5cf0d28

Browse files
committed
Proper potential
1 parent fe0b61c commit 5cf0d28

1 file changed

Lines changed: 24 additions & 27 deletions

File tree

lib/language/ic/ruler.effekt

Lines changed: 24 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ interface Interact {
2525
def construct(ctor: Constructor): Unit
2626
def rewire(rewiring: Map[String, Substitution]): Unit
2727

28-
def potential(port: PortRef): Unit
28+
def potential(port: Port): Unit
2929
def target(from: String): SuperPort
3030
def wire(from: Neg, to: Pos): Unit
3131
}
@@ -38,9 +38,8 @@ def redexes(program: Program): Unit / emit[Redex] =
3838
do emit(Redex(ctorA, ctorB))
3939

4040
// TODO: this is horribly inefficient for now, but could be very efficient
41-
def redexes(program: Program, potential: List[PortRef]): Unit / emit[Redex] =
42-
with val ref = potential.foreach
43-
val port = ref.get
41+
def redexes(program: Program, potential: List[Port]): Unit / emit[Redex] =
42+
with val port = potential.foreach
4443
with val ctorA = for { program() }
4544
with val ctorB = for { program() }
4645
if (ctorA.term::pp is Left(Neg(_)) and ctorB.term::pp is Right(Pos(_)))
@@ -63,8 +62,8 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
6362
(Neg(a).show, Substitution(Neg(a).super, do target(Pos(x).show))),
6463
(Neg(b).show, Substitution(Neg(b).super, do target(Pos(k).show)))
6564
].map::fromListGeneric)
66-
do potential(a) // TODO: theoretically, we'd only need to somehow check if Neg(a) is at a principal port
67-
do potential(b)
65+
do potential(a.get) // TODO: theoretically, we'd only need to somehow check if Neg(a) is at a principal port
66+
do potential(b.get)
6867
}
6968

7069
// δ(k-, k1+, ..., kn+) <> λ(x+, b-, k+) ~> σ(x+, x1-, ..., xn-), δ(b-, b1+, ..., bn+),
@@ -80,9 +79,9 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
8079
0.each(n) { i =>
8180
do construct(Abstractor(xsPos.get(i), bsNeg.get(i), ks.get(i)))
8281
}
83-
do potential(x)
84-
do potential(b)
85-
ks.foreach { k => do potential(k.port) }
82+
do potential(x.get)
83+
do potential(b.get)
84+
ks.foreach { k => do potential(k.port.get) }
8685
}
8786

8887
// @(f-, a-, k+) <> σ(f+, f1-, ..., fn-) ~> σ(k+, k1-, ..., kn-), δ(a-, a1+, ..., an+),
@@ -98,17 +97,17 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
9897
0.each(n) { i =>
9998
do construct(Applicator(fs.get(i), asNeg.get(i), ksPos.get(i)))
10099
}
101-
fs.foreach { f => do potential(f.port) }
102-
do potential(a)
103-
do potential(k)
100+
fs.foreach { f => do potential(f.port.get) }
101+
do potential(a.get)
102+
do potential(k.get)
104103
}
105104

106105
// δ(k-) <> σ(k+, i1-, ..., im-) ~> δ(i1-), ..., δ(in-)
107106
// asymmetric eraser annihilation: DUP-SUP
108107
case Redex(Duplicator(Neg(k1), Nil(), l1), Superposer(Pos(k2), ins, l2)) and k1 == k2 => {
109108
ins.foreach { i =>
110109
do construct(Duplicator(i, Nil(), l1))
111-
do potential(i.port)
110+
do potential(i.port.get)
112111
}
113112
}
114113

@@ -117,18 +116,18 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
117116
case Redex(Duplicator(Neg(k1), out, l1), Superposer(Pos(k2), Nil(), l2)) and k1 == k2 => {
118117
out.foreach { o =>
119118
do construct(Superposer(o, Nil(), l2))
120-
do potential(o.port)
119+
do potential(o.port.get)
121120
}
122121
}
123122

124123
// δ(k-, o1+, ..., on+) <> σ(k+, i1-, ..., im-) ~> [i1-/o1-]...[in-/on-]
125124
// symmetric duplicator annihilation: DUP-SUP
126125
case Redex(Duplicator(Neg(k1), out, l1), Superposer(Pos(k2), ins, l2)) and k1 == k2 and l1 == l2 and out.size == ins.size => {
127126
val rewiring = out.zip(ins).map { case (o, i) =>
128-
do potential(i.port)
129127
(i.show, Substitution(i.super, do target(o.show)))
130128
}.map::fromListGeneric
131129
do rewire(rewiring)
130+
ins.foreach { i => do potential(i.port.get) } // REMEMBER: potential must always happen after rewiring
132131
}
133132

134133
// δ(k-, o1+, ..., on+) <> σ(k+, i1-, ..., im-) ~> δ(i1-, o11+, ..., o1n+), .m., δ(im-, om1+, ..., omn+),
@@ -150,8 +149,8 @@ def interact(redex: Redex): Unit / { Interact, fresh } = redex match {
150149
}
151150
}
152151

153-
ins.foreach { i => do potential(i.port) }
154-
out.foreach { o => do potential(o.port) }
152+
ins.foreach { i => do potential(i.port.get) }
153+
out.foreach { o => do potential(o.port.get) }
155154
}
156155

157156
case _ => {
@@ -208,10 +207,10 @@ def rewire(wiring: Ref[Map[String, SuperPort]], _rewiring: Map[String, Substitut
208207
}
209208
}
210209

211-
def step_(program: Program, redex: Redex): List[PortRef] / { emit[Constructor], fresh } = {
210+
def step_(program: Program, redex: Redex): List[Port] / { emit[Constructor], fresh } = {
212211
val annihilated = ref[Set[Constructor]](emptyGeneric())
213212
val constructed = ref[List[Constructor]](Nil())
214-
val potential = ref[List[PortRef]](Nil())
213+
val potential = ref[Set[Port]](emptyGeneric())
215214
val wiring = ref(program.wiring())
216215

217216
try {
@@ -221,7 +220,7 @@ def step_(program: Program, redex: Redex): List[PortRef] / { emit[Constructor],
221220
} with Interact {
222221
def annihilate(ctor) = resume(annihilated.map { s => s.insert(ctor) })
223222
def construct(ctor) = resume(do emit(ctor))
224-
def potential(port) = resume(potential.map { l => Cons(port, l) })
223+
def potential(port) = resume(potential.map { s => s.insert(port) })
225224
def target(from) = resume(wiring.get.getOrElse(from) { panic(s"invalid target: ${from.show}") })
226225
def wire(from, to) = resume(wiring.map { w => w.put(from.show, to.super).put(to.show, from.super) })
227226
def rewire(rewiring) = resume(wiring.rewire(rewiring))
@@ -233,7 +232,7 @@ def step_(program: Program, redex: Redex): List[PortRef] / { emit[Constructor],
233232
}
234233
}
235234

236-
potential.get
235+
potential.get.toList
237236
}
238237

239238
def pop[A] { stream: => Unit / emit[A] }: A / { fail, emit[A] } = {
@@ -253,10 +252,10 @@ def pop(mode: StepMode, redexes: RedexBag): Redex / { fail, emit[Redex] } = mode
253252
}
254253

255254
def step(program: Program, mode: StepMode, redexes: RedexBag): Unit / { emit[Constructor], emit[Redex], fresh, fail } = {
256-
//val redex = pop(mode, redexes) // TODO!
257-
val redex = pop(NonDeterministic(), redexes)
255+
val redex = pop(mode, redexes) // TODO!
256+
// val redex = pop(NonDeterministic(), redexes)
258257
// println(s"\n=== REDEX: ${redex.show} ===")
259-
val tup: (List[PortRef], Program) = returning::collect { program.step_(redex) }
258+
val tup: (List[Port], Program) = returning::collect { program.step_(redex) }
260259
val (potential, program) = tup
261260

262261
// println(list::collect[Constructor] { program() }.show { ctor => ctor.show })
@@ -269,9 +268,7 @@ def step(program: Program, mode: StepMode, redexes: RedexBag): Unit / { emit[Con
269268
// println("\nREDEX: " ++ redex.left.show ++ " - " ++ redex.right.show)
270269
println(posPorts.difference(negPorts).toList.show)
271270
} else {
272-
// println(potential)
273-
//program.redexes(potential)
274-
program.redexes()
271+
program.redexes(potential)
275272
program()
276273
}
277274
}

0 commit comments

Comments
 (0)