@@ -92,19 +92,23 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
9292 cctx.nest(v -> nc) givenIn :
9393 v.state.upperBounds ::= nc
9494 v.state.lowerBounds.foreach(lb => constrainImpl(lb, nc))
95+ v.state.disjsub.foreach: d =>
96+ Type .disjoint(d.disjoint(v), bd.toBasic.simp.toBasic)(Set .empty)(using c = mutable.Map .empty)
97+ .foreach(_.foreach(k => DisjSub (d.disjoint ++ k, d.dss, d.cs).commit()))
9598 else
9699 log(s " New bound: ${v.showDbg} :> ${bd.showDbg}" )
97100 cctx.nest(bd -> v) givenIn :
98101 v.state.lowerBounds ::= bd
99102 v.state.upperBounds.foreach(ub => constrainImpl(bd, ub))
100- v.state.disjsub.foreach: (d) =>
101- Type .disjoint(d.disjoint(v),bd.toBasic.simp) match
102- case N =>
103+ v.state.disjsub.foreach: d =>
104+ Type .disjoint(d.disjoint(v), bd.toBasic.simp.toBasic)( Set .empty)( using c = mutable. Map .empty) match
105+ case N =>
103106 d.remove(v)
104107 if d.disjoint.isEmpty then
105108 d.dss.foreach(_.commit())
106- d.cs.foreach((a,b)=> constrainImpl(a,b))
107- case S (k)=> d.disjoint++= k
109+ d.cs.foreach((a, b) => constrainImpl(a, b))
110+ case S (k) =>
111+ k.foreach(k => DisjSub (d.disjoint ++ k, d.dss, d.cs).commit())
108112 case Conj (i, u, Nil ) => (conj.i, conj.u) match
109113 case (_, Union (N , Nil )) =>
110114 // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil))
@@ -120,32 +124,38 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
120124 // raise(ErrorReport(msg"Cannot constrain ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil))
121125 cctx.err
122126 else
123- val k = args2.flatMap(x=> Type .disjoint(x,x))
127+ val k = args2.flatMap: x =>
128+ val u = x.toBasic.simp.toBasic
129+ Type .disjoint(u, u)(Set .empty)(using c = mutable.Map .empty)
124130 if k.isEmpty then
125131 args1.zip(args2).foreach {
126132 case (a1, a2) => constrainImpl(a2, a1)
127133 }
128134 constrainImpl(ret1, ret2)
129135 constrainImpl(eff1, eff2)
130- else if ! k.contains(Nil )then
131- DisjSub (mutable.Map .from(k.flatten),Nil ,(ret1,ret2):: (eff1,eff2):: args2.zip(args1)).commit()
136+ else
137+ val cs = (ret1, ret2) :: (eff1, eff2) :: args2.zip(args1)
138+ k.reduce((x, y) => y.flatMap(y => x.map(_ ++ y))).foreach: k =>
139+ DisjSub (mutable.Map .from(k), Nil , cs).commit()
132140 case (Inter (S (fs: Ls [FunType ])), Union (S (FunType (args2, ret2, eff2)), Nil )) =>
133- val f = fs.filter(_.args.length=== args2.length)
134- val args = f.map(_.args).transpose
135- val k = args2.flatMap(x=> Type .disjoint(x,x))
136- if ! k.contains(Nil )then
141+ val f = fs.filter(_.args.length === args2.length)
142+ val args = f.map(_.args).transpose
143+ val k = args2.flatMap: x =>
144+ val u = x.toBasic.simp.toBasic
145+ Type .disjoint(u, u)(Set .empty)(using c = mutable.Map .empty)
146+ if ! k.contains(Nil ) then
137147 // assume distinguished by the first arg
138148 constrainImpl(args2.head,args.head.foldLeft(Bot : Type )(_|_))
139- args.head.iterator.zip(f).foreach: (a,b) =>
140- val s = args2.zip(b.args).tail
141- Type .disjoint(args2.head.toBasic.simp,a.toBasic.simp) match
149+ args.head.iterator.zip(f).foreach: (a, b) =>
150+ val s = args2.zip(b.args).tail
151+ Type .disjoint(args2.head.toBasic.simp.toBasic ,a.toBasic.simp.toBasic)( Set .empty)( using c = mutable. Map .empty) match
142152 case N =>
143- s.foreach((x,y) => constrainImpl(x,y))
144- constrainImpl(b.ret,ret2)
145- constrainImpl(b.eff,eff2)
153+ s.foreach((x, y) => constrainImpl(x, y))
154+ constrainImpl(b.ret, ret2)
155+ constrainImpl(b.eff, eff2)
146156 case S (k) =>
147- val ds = DisjSub (mutable. Map .from(k), Nil ,( b.ret,ret2):: (b.eff,eff2):: s)
148- ds. commit()
157+ val cs = ( b.ret,ret2) :: (b.eff,eff2) :: s
158+ k.foreach(k => DisjSub (mutable. Map .from(k), Nil , cs). commit() )
149159 case _ =>
150160 // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil))
151161 cctx.err
0 commit comments