Skip to content

Eager Constraint Solving in Polymorphic Flow Analysis #621

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
flandia wants to merge 7 commits into
base: hkmc2
Choose a base branch
from
+1,732 −1,174
Open

Eager Constraint Solving in Polymorphic Flow Analysis #621

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
897c029
Restructure Flow Analysis
flandia Oct 31, 2026
88264a5
Eager Constraint Solving
flandia Nov 2, 2026
e364e01
Flow Analysis Optimization
flandia Nov 6, 2026
1a96c15
Simplify `EffectAnalysis.summarize`
flandia Nov 6, 2026
6fa1532
Test solved scheme flows through shared mutable bindings
codex Nov 7, 2026
1eb5fe3
Merge upstream hkmc2 into eager-analysis
codex Nov 10, 2026
40ae24c
Resolve Anto's comments
flandia Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions hkmc2/shared/src/main/scala/hkmc2/codegen/EtaExpansion.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ class EtaExpansionSolver(val constraintSolver: FlowConstraintSolver, tl: TraceLo
EtaTargets(a.paramCount, a.requiredParamCount, a.hasRestParam, a.prodFuns ++ b.prodFuns)
go(S(mergedRes))
else Nil
case UnknownProd | UnsafeEta | NoProd => Nil
case UnknownProd | UnsafeEta => Nil
case _: Ctor => Nil
end go

Expand All @@ -107,7 +107,7 @@ class EtaExpansionSolver(val constraintSolver: FlowConstraintSolver, tl: TraceLo
case _ => false
then go(N)
else Nil
case UnknownProd | UnsafeEta | NoProd => Nil
case UnknownProd | UnsafeEta => Nil
case _: Ctor => Nil
end funResShape

Expand Down
4 changes: 2 additions & 2 deletions hkmc2/shared/src/main/scala/hkmc2/codegen/PolyInstantiationRewrite.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,8 @@ abstract class PolyInstantiationRewrite(val constraintSolver: FlowConstraintSolv
val res = LinkedHashMap.empty[InstantiationId, Map[TermSymbol, (BlockMemberSymbol, TermSymbol)]]
def funSymsToBeCopiedAt(path: InstantiationId): Iterator[TermSymbol] =
collector.synthesizedInstIdToFunSym.get(path) match
case S(entry) => collector.funToSccGroups(entry).iterator.filterNot(_ is entry)
case N => collector.funToSccGroups(path.last.getReferredFun.get).iterator
case S(entry) => collector.funToScc(entry).iterator.filterNot(_ is entry)
case N => collector.funToScc(path.last.getReferredFun.get).iterator
for
instId <- solvers.iterator.flatMap(_.polyInstIds)
path <- instId.inits
Expand Down
8 changes: 3 additions & 5 deletions hkmc2/shared/src/main/scala/hkmc2/codegen/flowAnalysis/EffectAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,9 @@ enum EffectSummary:

object EffectAnalysis:

def summarize(effectVar: StratVar | NoProd): EffectSummary =
effectVar match
case NoProd => EffectSummary.Pure
case effectVar: StratVar =>
if effectVar.lowerBounds.forall(_.isInstanceOf[StratVar])
def summarize(effectVar: EffectVar): EffectSummary =
effectVar.fold(EffectSummary.Pure): v =>
if v.lowerBounds.isEmpty
then EffectSummary.Pure
else EffectSummary.UnsafeEta

Expand Down
1,344 changes: 832 additions & 512 deletions hkmc2/shared/src/main/scala/hkmc2/codegen/flowAnalysis/FlowAnalysis.scala
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions hkmc2/shared/src/test/mlscript/dead-param-elim/basic.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -316,8 +316,8 @@ private fun f(a) = g(a)
private fun g(x) = 3
f(1)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > f²⁵#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > g²#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > f²⁵#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 3

Expand All @@ -328,7 +328,7 @@ f(1)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > g²#0 @ f²⁵.g³ -> eliminable: {0}
//│ dead-param-elim > g²#0 @ f²⁶.g³ -> eliminable: {0}
//│ dead-param-elim > f²⁷#0 @ f²⁶ -> eliminable: {0}
//│ dead-param-elim > f²⁷#0 @ f²⁵ -> eliminable: {0}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 3

Expand Down
8 changes: 4 additions & 4 deletions hkmc2/shared/src/test/mlscript/dead-param-elim/clash.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,8 @@ private fun choose(x)(y) = if false then x else y
private fun m() = choose(f)(g)(1)(2)
m()
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > g⁰#1 @ <root> -> eliminable: {0}
//│ dead-param-elim > f⁰#1 @ <root> -> eliminable: {0}
//│ dead-param-elim > g⁰#1 @ <root> -> eliminable: {0}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 1

Expand All @@ -81,8 +81,8 @@ private fun choose(x)(y) = if false then x else y
private fun m() = choose(f)(g)(1, 2)
m()
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {1}
//│ dead-param-elim > f⁰#0 @ <root> -> eliminable: {1}
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {1}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 1

Expand All @@ -108,8 +108,8 @@ private fun f(a, b, ...rest) = rest
private fun g(a, b, c, ...rest) = rest
(if false then f else g)(1,2,3,4,5)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > f⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = [4, 5]

Expand All @@ -119,8 +119,8 @@ private fun f(a, b, ...rest) = rest
private fun g(a, b, c, ...rest) = rest
(if true then f else g)(1,2,3,4,5)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > f⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {0, 1}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = [3, 4, 5]

Expand Down
2 changes: 1 addition & 1 deletion hkmc2/shared/src/test/mlscript/dead-param-elim/dead-ref.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ private fun f(a) =
private fun g(a) = 2
f(unsafe.undefined)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > f⁰#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > g⁰#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > f⁰#0 @ <root> -> eliminable: {0}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ ——————————————| Optimized IR |——————————————————————————————————————————————————————————————————————
//│ @private
Expand Down
4 changes: 2 additions & 2 deletions hkmc2/shared/src/test/mlscript/dead-param-elim/lambda.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,10 +110,10 @@ private fun main(f1, f2) =
private fun main1() = main((a) => 0, (a) => a + 1)
main1()
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > apply⁰#0 @ main1⁰.main⁰.apply¹ -> eliminable: {1}
//│ dead-param-elim > lambda⁰#0 @ main1⁰ -> eliminable: {0}
//│ dead-param-elim > apply⁰#0 @ main1¹.main⁰.apply¹ -> eliminable: {1}
//│ dead-param-elim > apply⁰#0 @ main1⁰.main⁰.apply¹ -> eliminable: {1}
//│ dead-param-elim > lambda⁰#0 @ main1¹ -> eliminable: {0}
//│ dead-param-elim > apply⁰#0 @ main1¹.main⁰.apply¹ -> eliminable: {1}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 1

Expand Down
8 changes: 4 additions & 4 deletions hkmc2/shared/src/test/mlscript/dead-param-elim/recursive.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,10 +161,10 @@ fun ping(n, unused) = if n == 0 then 0 else pong(n - 1, unused)
fun pong(n, unused) = if n == 0 then 0 else ping(n - 1, unused)
ping(5, 99)
//│ dead-param-elim > >>> dead-param-elim results >>>
//│ dead-param-elim > ping⁴#0 @ pong⁴ -> eliminable: {1}
//│ dead-param-elim > pong⁵#0 @ ping⁵ -> eliminable: {1}
//│ dead-param-elim > ping⁴#0 @ ping⁶ -> eliminable: {1}
//│ dead-param-elim > pong⁵#0 @ ping⁶ -> eliminable: {1}
//│ dead-param-elim > ping⁴#0 @ ping⁵ -> eliminable: {1}
//│ dead-param-elim > pong⁴#0 @ ping⁵ -> eliminable: {1}
//│ dead-param-elim > pong⁴#0 @ ping⁶ -> eliminable: {1}
//│ dead-param-elim > ping⁴#0 @ pong⁵ -> eliminable: {1}
//│ dead-param-elim > <<< dead-param-elim results <<<
//│ = 0

Expand Down
8 changes: 4 additions & 4 deletions hkmc2/shared/src/test/mlscript/deforest/append.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,22 +65,22 @@ appendThree of
//│ deforest > match: xs⁰
//│ deforest > fields: xs⁰.h¹
//│ deforest > fields: xs⁰.t⁰
//│ deforest > Nil⁰ ->
//│ deforest > match: xs⁰
//│ deforest > Cons⁰(h², tmp¹) ->
//│ deforest > match: xs⁰
//│ deforest > fields: xs⁰.h¹
//│ deforest > fields: xs⁰.t⁰
//│ deforest > Nil⁰ ->
//│ deforest > match: xs⁰
//│ deforest > Cons⁰(h⁰, tmp⁰) ->
//│ deforest > match: xs⁰
//│ deforest > fields: xs⁰.h¹
//│ deforest > fields: xs⁰.t⁰
//│ deforest > Nil⁰ ->
//│ deforest > match: xs⁰
//│ deforest > Cons⁰(h², tmp¹) ->
//│ deforest > match: xs⁰
//│ deforest > fields: xs⁰.h¹
//│ deforest > fields: xs⁰.t⁰
//│ deforest > Nil⁰ ->
//│ deforest > match: xs⁰
//│ deforest > <<< fusing <<<
//│ = Cons(1, Cons(2, Cons(3, Cons(4, Cons(5, Cons(6, Nil))))))

Expand Down
10 changes: 5 additions & 5 deletions hkmc2/shared/src/test/mlscript/deforest/basic.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,9 +175,6 @@ fun c(x, d) = if x is
X(a) then c(X(a), d)
() => c(X(3), 2)
//│ deforest > >>> fusing >>>
//│ deforest > X⁰(a²) ->
//│ deforest > match: x⁴
//│ deforest > fields: x⁴.a⁰
//│ deforest > X⁰(3) ->
//│ deforest > match: x⁴
//│ deforest > fields: x⁴.a⁰
Expand All @@ -187,6 +184,9 @@ fun c(x, d) = if x is
//│ deforest > X⁰(3) ->
//│ deforest > match: x⁴
//│ deforest > fields: x⁴.a⁰
//│ deforest > X⁰(a²) ->
//│ deforest > match: x⁴
//│ deforest > fields: x⁴.a⁰
//│ deforest > <<< fusing <<<
//│ = fun lambda$lambda

Expand Down Expand Up @@ -301,10 +301,10 @@ fun f(x) = if x is
A(x) then 2
f(A(2)) + f(A(3))
//│ deforest > >>> fusing >>>
//│ deforest > A⁰(3) ->
//│ deforest > A⁰(2) ->
//│ deforest > match: x¹⁰
//│ deforest > fields: x¹⁰.x⁸
//│ deforest > A⁰(2) ->
//│ deforest > A⁰(3) ->
//│ deforest > match: x¹⁰
//│ deforest > fields: x¹⁰.x⁸
//│ deforest > <<< fusing <<<
Expand Down
4 changes: 2 additions & 2 deletions hkmc2/shared/src/test/mlscript/deforest/cyclic.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,11 @@ fun f(x) = if x is
else 0
f(Nil)
//│ deforest > >>> fusing >>>
//│ deforest > Nil⁰ ->
//│ deforest > match: x⁰
//│ deforest > A⁰(2) ->
//│ deforest > match: x⁰
//│ deforest > fields: x⁰.x¹
//│ deforest > Nil⁰ ->
//│ deforest > match: x⁰
//│ deforest > <<< fusing <<<
//│ = 0

Expand Down
16 changes: 8 additions & 8 deletions hkmc2/shared/src/test/mlscript/deforest/eta-expansion/basic.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,9 +69,9 @@ g(f(p()))
//│ deforest > fields: y⁰.b⁰
//│ deforest > <<< fusing <<<
//│ eta-expansion > >>> eta-expansion targets shapes >>>
//│ eta-expansion > f$f⁰#0 @ <root>: [1, 2]
//│ eta-expansion > p$p⁰#0 @ <root>: [0, 2, 2]
//│ eta-expansion > f$x_X⁰#0 @ <root>: [1, 2, 2]
//│ eta-expansion > p$p⁰#0 @ <root>: [0, 2, 2]
//│ eta-expansion > f$f⁰#0 @ <root>: [1, 2]
//│ eta-expansion > <<< eta-expansion targets shapes <<<
//│ = O

Expand Down Expand Up @@ -111,18 +111,18 @@ fun main(x) =
c(p(2))
main(3)
//│ deforest > >>> fusing >>>
//│ deforest > X⁰(tmp³) ->
//│ deforest > match: x⁵
//│ deforest > fields: x⁵.a⁰
//│ deforest > Y⁰(tmp⁴) ->
//│ deforest > Y⁰(tmp³) ->
//│ deforest > match: arg$X$0$¹
//│ deforest > fields: arg$X$0$¹.b⁰
//│ deforest > X⁰(tmp³) ->
//│ deforest > X⁰(tmp⁴) ->
//│ deforest > match: x⁵
//│ deforest > fields: x⁵.a⁰
//│ deforest > Y⁰(tmp⁴) ->
//│ deforest > Y⁰(tmp³) ->
//│ deforest > match: arg$X$0$¹
//│ deforest > fields: arg$X$0$¹.b⁰
//│ deforest > X⁰(tmp⁴) ->
//│ deforest > match: x⁵
//│ deforest > fields: x⁵.a⁰
//│ deforest > <<< fusing <<<
//│ eta-expansion > >>> eta-expansion targets shapes >>>
//│ eta-expansion > main_p$p⁰#0 @ <root>: [2, 3]
Expand Down
2 changes: 1 addition & 1 deletion hkmc2/shared/src/test/mlscript/deforest/eta-expansion/recursive.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,8 @@ len(flatten(id((1 :: 2 :: Nil) :: (3 :: Nil) :: Nil)))
//│ deforest > fields: ls¹.t⁰
//│ deforest > <<< fusing <<<
//│ eta-expansion > >>> eta-expansion targets shapes >>>
//│ eta-expansion > flatten_append$append⁰#0 @ <root>: [2, 5]
//│ eta-expansion > flatten$flatten⁰#0 @ <root>: [1, 5]
//│ eta-expansion > flatten_append$append⁰#0 @ <root>: [2, 5]
//│ eta-expansion > <<< eta-expansion targets shapes <<<
//│ ——————————————| Optimized IR |——————————————————————————————————————————————————————————————————————
//│ let tmp, tmp1, tmp2, tmp3, tmp4, flatten$flatten, flatten_append$append$worker, flatten$flatten$worker;
Expand Down
6 changes: 3 additions & 3 deletions hkmc2/shared/src/test/mlscript/deforest/fusibility.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,12 +97,12 @@ affine_branched(AA(0), AA(1), (y) => if y is AA(x) then x + 2)
//│ deforest > cap_ub_(term:lambda,0)_for_lambda⁰
//│ deforest > <<< non-affine syms <<<
//│ deforest > >>> fusing >>>
//│ deforest > AA⁰(1) ->
//│ deforest > match: y⁰
//│ deforest > fields: y⁰.x⁰
//│ deforest > AA⁰(0) ->
//│ deforest > match: x²
//│ deforest > fields: x².x⁰
//│ deforest > AA⁰(1) ->
//│ deforest > match: y⁰
//│ deforest > fields: y⁰.x⁰
//│ deforest > <<< fusing <<<
//│ = 3

Expand Down
Loading
Loading