From c1b08a82d0b8a741f5b62c5b32e2ca5bd34fe21c Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Tue, 6 Oct 2026 14:13:22 +0800 Subject: [PATCH 1/6] init draft --- .../main/scala/hkmc2/semantics/Symbol.scala | 6 + .../scala/hkmc2/typing/ConstraintSolver.scala | 115 +++++ .../main/scala/hkmc2/typing/NormalForm.scala | 102 +++++ .../scala/hkmc2/typing/TypeTraverser.scala | 35 ++ .../src/main/scala/hkmc2/typing/infctx.scala | 104 +++++ .../src/main/scala/hkmc2/typing/inftype.scala | 199 +++++++++ .../main/scala/hkmc2/typing/logicsub.scala | 401 ++++++++++++++++++ .../test/mlscript/codegen/ConfigDirective.mls | 1 + .../mlscript/ucs/staging/legacy/ElseIf.mls | 288 +++++++++---- .../test/scala/hkmc2/LogicSubDiffMaker.scala | 33 ++ .../src/test/scala/hkmc2/MainDiffMaker.scala | 2 +- 11 files changed, 1195 insertions(+), 91 deletions(-) create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala create mode 100644 hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala create mode 100644 hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala index 3c2c3bc4ec..7c211a5e34 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala @@ -253,6 +253,12 @@ class InstSymbol(val origin: Symbol)(using State) extends LocalSymbol: override def toLoc: Option[Loc] = origin.toLoc def subst(using sub: SymbolSubst): InstSymbol = sub.mapInstSym(this) +class InfVarSymbol(val origin: Symbol | Term, val hint: Str = "")(using State) extends LocalSymbol: + override def nme: Str = origin match + case x: Symbol => x.nme ++ hint + case x: Term => hint + override def toLoc: Option[Loc] = origin.toLoc + def subst(using sub: SymbolSubst): InfVarSymbol = ??? class VarSymbol(val id: Ident, override val erasedType: Opt[ErasedValueType])(using State) extends LocalVarSymbol(id.name) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala new file mode 100644 index 0000000000..da3c7b3fd4 --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala @@ -0,0 +1,115 @@ +package hkmc2 +package typing +package logicsub + +import scala.collection.mutable + +import semantics.* +import Message.MessageContext +import hkmc2.utils.*, shorthands.* +import utils.* +import utils.Scope + +type Cache = mutable.HashSet[(Type, Type)] +type ExtrudeCache = mutable.HashMap[(InfVarSymbol, Bool), InfVar] + +case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])(using Scope): + def err(using Raise, InfCtx) = + raise(ErrorReport( + msg"Type error in ${origin.describe}${exp match + case S(ty) => msg" with expected type ${ty.show}" + case N => msg"" + }" -> origin.toLoc + :: parents.reverse.map(p => + msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N + ) + )) + def nest(sub: (Type, Type)): CCtx = + copy(cache = cache += sub, parents = parents match + case `sub` :: _ => parents + case _ => sub :: parents + ) +object CCtx: + inline def init(origin: Term, exp: Opt[InfType])(using Scope) = + CCtx(mutable.HashSet.empty, Nil, origin, exp) + +class ConstraintSolver(elState: Elaborator.State, tl: TraceLogger)(using Raise): + import tl.{trace, log} + + private def constrainConj(conj: Conj)(using ctx: InfCtx, cctx:CCtx, tl: TL): Unit = trace(s"Constraining ${conj.showDbg}"): + conj match + case Conj(i, u, S(v), w, _, _) => + val rest = Conj(i, u, N, w, Nil,Nil) + val bd = if v.lvl >= rest.lvl then rest else ??? // extrude(rest)(using v.lvl, true, mutable.HashMap.empty) + val nc = (~bd).toDnf // always cache the normal form to avoid unexpected cache misses + log(s"New bound: ${v.showDbg} <: ${nc.showDbg}") + cctx.nest(v.toDnf -> nc) givenIn: + // v.state.upperBounds ::= nc + // v.state.lowerBounds.foreach(lb => constrain(lb, nc)) + ctx.addub(v, nc) + case Conj(i, u, N, S(v), _,_) => + val rest = Conj(i, u, N,N,Nil,Nil) + val bd = if v.lvl >= rest.lvl then rest else ??? // extrude(rest)(using v.lvl, true, mutable.HashMap.empty) + val c = bd.toDnf // always cache the normal form to avoid unexpected cache misses + log(s"New bound: ${v.showDbg} :> ${c.showDbg}") + cctx.nest(c -> v.toDnf) givenIn: + // v.state.lowerBounds ::= c + // v.state.upperBounds.foreach(ub => constrain(c, ub)) + ctx.addlb(c, v) + case Conj(NF.Inter(x :: Nil), NF.Union(Nil), N,N,_,_) => + val da = x.args.iterator.zip(x.out).collect: + case (t, true) => t.posPart + val d = (x.refinement.values ++ da).toList + if d.isEmpty then cctx.err + else ctx.constrain(this, d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.subor(k, ctx.sub(t, Bot)))) + case Conj(NF.Inter(x :: Nil), NF.Union(ClassLikeType(y, yargs, yrefine, in, _) :: Nil), N,N,_,_) => ??? + case Conj(NF.Inter(x :: xs), NF.Union(ClassLikeType(y, yargs, yrefine, in, _) :: Nil), N,N,_,_) => ??? + case Conj(NF.Inter(x :: xs), NF.Union(y :: ys), N,N,_,_) => ??? +// case Conj(Ninter(S(ClassLikeType(c1, a1, r1, _))), Nunion(ClassLikeType(c2, a2, r2, _) :: rest), N, N) => +// case Conj(Ninter(S(c)), Nunion(d :: rest), N, N) => +// if c.sym === d.sym then +// c.args.zip(d.args).foreach: (ta1, ta2) => +// constrainArgs(ta1, ta2) +// // TODO +// else constrainConj(Conj(conj.i, Nunion(rest), N, N)) case _ => + // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil)) + cctx.err + + private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using InfCtx, CCtx, TL): Unit = + constrain(rhs.negPart, lhs.negPart) + constrain(lhs.posPart, rhs.posPart) + + private class SkolemBoundsInliner(using ctx: InfCtx) extends TypeMapper: + val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty + override def apply(pol: Bool)(t: Type) = t.toBasic match + case v @ InfVar(_, s, true) if !cache(s) => + cache += s + apply(pol)(if pol + then ctx.ubs(s).foldLeft[Type](v)(_ & _) + else ctx.lbs(s).foldLeft[Type](v)(_ | _)) + case _: ClassLikeType | _: InfVar => t + case t => super.apply(pol)(t) + private def inlineSkolemBounds(ty: Type)(using InfCtx): Type = + (new SkolemBoundsInliner)(true)(ty) + + private def constrainImpl(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL): Unit = + val p = lhs.toDnf -> rhs.toDnf + if cctx.cache(p) then log(s"Cached!") + else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): + cctx.nest(p) givenIn: + val disj = inlineSkolemBounds(lhs & ~rhs).toDnf + disj.cs.foreach(constrainConj(_)) + + def constrain(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL): Unit = + val (ps, ts) = rhs.disjuncts.partition(_.partialpattern) + if ts.length > 1 then + val p = lhs.toDnf -> rhs + if cctx.cache(p) then log(s"Cached!") + else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): + cctx.nest(p) givenIn: + val u = ps.foldLeft(lhs)((x, y) => x & ~y) + val qs = ts.map(_.discriminator) + constrainImpl(u, qs.reduce(_ | _)) + qs.zip(ts).foreach((q, y) => constrainImpl(q & u, y)) + else + constrainImpl(lhs, rhs) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala new file mode 100644 index 0000000000..1aa2a77dc7 --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala @@ -0,0 +1,102 @@ +package hkmc2 +package typing +package logicsub + +import scala.annotation.tailrec + +import syntax.* +import semantics.* +import Message.MessageContext +import hkmc2.utils.*, shorthands.* +import utils.* +import utils.Scope + +sealed abstract class NormalForm extends TypeExt + +object NF: + final case class Inter(v: Ls[ClassLikeType]) extends NormalForm: + lazy val toBasic = v.foldLeft[Type](Top)(_ & _).toBasic + def merge(other: Inter): Opt[Inter] = + other.v.foldLeft(Opt(v))((r, w) => r.flatMap(w.merge(_))).map(Inter(_)) + + final case class Union(v: Ls[ClassLikeType]) extends NormalForm: + lazy val toBasic = v.foldLeft[Type](Bot)(_ | _).toBasic + def merge(other: Union) = Union(v ++ other.v) + + object Inter: + val empty = Inter(Nil) + object Union: + val empty = Union(Nil) + +final case class Disj(cs: Ls[Conj]) extends NormalForm: + lazy val toBasic = cs.foldLeft[Type](Bot)(_ | _).toBasic + def isBot = cs.isEmpty + +final case class Conj( + i: NF.Inter, u: NF.Union, + v1: Opt[InfVar], v2: Opt[InfVar], + ps: Ls[InfVar], ns: Ls[InfVar] +) extends NormalForm: + lazy val toBasic = (i.toBasic & ~u.toBasic & v1.getOrElse(Top) & v2.fold(Top)(~_)).toBasic + def merge(that: Conj)(using TL): Opt[Conj] = + tl.traceNot[Opt[Conj]](s"merge ${this.showDbg} and ${that.showDbg}", r => s"= ${r.map(_.showDbg)}"): + val Conj(i1, u1, v1, w1, x1, y1) = this + val Conj(i2, u2, v2, w2, x2, y2) = that + val xs = x1 ++ x2 + val ys = y1 ++ y2 + if xs.intersect(ys).nonEmpty then N + else i1.merge(i2) match + case N => N + case S(i) => + val u = u1.merge(u2) + (v1.orElse(v2), w1.orElse(w2)) match + case (S(v), S(w)) if v.sym === w.sym => N + case (v,w) => S(Conj(i, u, v, w, xs, ys)) + +object Conj: + val empty: Conj = Conj(NF.Inter.empty, NF.Union.empty, N, N, Nil, Nil) + def mkVar(v: InfVar, pol: Bool) = + if pol then + Conj(NF.Inter.empty, NF.Union.empty, S(v), N, Nil, Nil) + else Conj(NF.Inter.empty, NF.Union.empty, N, S(v), Nil, Nil) + def mkInter(inter: ClassLikeType) = + Conj(NF.Inter(Ls(inter)), NF.Union.empty, N, N, Nil, Nil) + def mkUnion(union: ClassLikeType) = + Conj(NF.Inter.empty, NF.Union(Ls(union)), N, N, Nil, Nil) +object Disj: + val bot = Disj(Nil) + val top = Disj(Ls(Conj.empty)) + +object NormalForm: + def inter(lhs: Disj, rhs: Disj)(using TL): Disj = + tl.traceNot[Disj](s"inter ${lhs.showDbg} and ${rhs.showDbg}", r => s"= ${r.showDbg}"): + if lhs.isBot || rhs.isBot then Disj.bot + else Disj(lhs.cs.flatMap(lhs => rhs.cs.flatMap(rhs => lhs.merge(rhs) match { + case S(conj) => conj :: Nil + case N => Nil + }))) + + def union(lhs: Disj, rhs: Disj): Disj = Disj(lhs.cs ++ rhs.cs) + + def neg(ty: Type)(using TL): Disj = + tl.traceNot[Disj](s"~Disj ${ty.showDbg} ${ty.getClass} ${ty.toBasic.showDbg}", r => s"= ${r.showDbg}"): + ty match + case u: NF.Union => Disj(Ls(Conj(NF.Inter(Nil), u, N, N, Nil, Nil))) + case v: InfVar => Disj(Ls(Conj.mkVar(v, false))) + case ct: ClassLikeType => Disj(Ls(Conj.mkUnion(ct))) + case _ => dnf(~(ty.toBasic)) + + def dnf(ty: Type)(using TL): Disj = + tl.traceNot[Disj](s"Disj ${ty.showDbg} ${ty.getClass}", r => s"= ${r.showDbg}"): + ty match + case d: Disj => d + case c: Conj => Disj(Ls(c)) + case i: NF.Inter => Disj(Ls(Conj(i, NF.Union.empty, N, N, Nil, Nil))) + case _ => ty.toBasic match + case Top => Disj.top + case Bot => Disj.bot + case v: InfVar => Disj(Ls(Conj.mkVar(v, true))) + case ct: ClassLikeType => Disj(Conj.mkInter(ct) :: Nil) + case Inter(lhs, rhs) => inter(dnf(lhs), dnf(rhs)) + case Union(lhs, rhs) => union(dnf(lhs), dnf(rhs)) + case Neg(ty) => neg(ty) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala new file mode 100644 index 0000000000..1a517a9a3e --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala @@ -0,0 +1,35 @@ +package hkmc2 +package typing +package logicsub + +import hkmc2.utils.*, shorthands.* + +// class TypeTraverser: +// def apply(pol: Bool)(ty: Type): Unit = ty.toBasic match +// case Union(x, y) => +// apply(pol)(x) +// apply(pol)(y) +// case Inter(x, y) => +// apply(pol)(x) +// apply(pol)(y) +// case Neg(ty) => apply(!pol)(ty) +// case ClassLikeType(name, targs, refine) => +// targs.foreach: +// case Wildcard(in, out) => +// apply(!pol)(in) +// apply(pol)(out) +// case ty: Type => +// apply(pol)(ty) +// apply(!pol)(ty) +// refine.values.foreach(apply(pol)) +// case _ => + +class TypeMapper: + def applyArg(pol: Bool)(t: TypeArg): TypeArg = ??? + def apply(pol: Bool)(t: Type): Type = t.toBasic match + case Bot | Top | _: InfVar => t + case Union(x, y) => Union(apply(pol)(x), apply(pol)(y)) + case Inter(x, y) => Inter(apply(pol)(x), apply(pol)(y)) + case Neg(x) => Neg(apply(!pol)(x)) + case ClassLikeType(n, args, refine, i,o) => + ClassLikeType(n, args.map(applyArg(pol)), refine.mapValues(t => apply(pol)(t)), i,o) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala new file mode 100644 index 0000000000..75920279d7 --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala @@ -0,0 +1,104 @@ +package hkmc2 +package typing +package logicsub + +import scala.collection.mutable.{HashSet, HashMap, ListBuffer} +import scala.annotation.tailrec + +import hkmc2.utils.*, shorthands.* +import utils.* + +import Message.MessageContext +import semantics.*, Term.*, ucs.FlatPattern +import Elaborator.Ctx +import syntax.* +import Tree.* +import utils.Scope +import hkmc2.codegen.ErasedType.eraseSign + +final case class DisjOr(p: Type, cs: Ls[K]) +final case class K(x: Type, y: Type | DisjOr) + +class InfVarState: + var lowerBounds: Ls[Type] = Nil + var upperBounds: Ls[Type] = Nil + var disjsub: Ls[DisjOr] = Nil + +final case class InfCtx( + val lvl: Int, + val parent: Option[InfCtx], + val env: HashMap[Symbol, InfType], + val outRegAcc: Type, + val prefix: Ls[Ls[Type->Type]], + val suffix: Ls[K] +)(using + val prim: PrimCtx, + val ctx: Ctx, + val typeNames: HashSet[Str], + val symbolCache: HashMap[Str, TypeSymbol], + val varSt: HashMap[InfVarSymbol, InfVarState] +): + def +=(p: Symbol -> InfType): Unit = env += p + def get(sym: Symbol): Option[InfType] = env.get(sym) `orElse` parent.dlof(_.get(sym))(None) + def getCls(name: Str): TypeSymbol= symbolCache.getOrElseUpdate(name, + ctx.get(name).get.symbol.get.asTpe.get) + def nest: InfCtx = copy(parent = Some(this), env = HashMap.empty) + def nestWithOuter(outer: InfVar): InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer) + def nextLevel: InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty) + + def withTail(x:Ls[K]) = copy(parent = S(this), suffix = x) + // def freshVar(origin: Symbol | Term, hint: Str = ""): InfVar + + def sub(x: Type, y: Type): K = K(x,y) + def subor(x: K, y: K): K = (x,y) match + case (K(a, b: Type), y) => K(a, DisjOr(b, Ls(y))) + case (K(a, DisjOr(b, cs)), y) => K(a, DisjOr(b, cs ++ Ls(y))) + + def constrain(solver: ConstraintSolver, c: K)(using CCtx, TL): Unit= c match + case K(x,y: Type) => solver.constrain(x,y)(using this) + case K(x,DisjOr(y, cs)) => + given InfCtx = withTail(cs) + solver.constrain(x,y) + + def ubs(s: InfVarSymbol): Ls[Type]= varSt(s).upperBounds + def lbs(s: InfVarSymbol): Ls[Type]= varSt(s).lowerBounds + def addub(s: InfVar, ub: Type): Unit= + val v = varSt.getOrElseUpdate(s.sym, new InfVarState) + v.upperBounds = ub :: v.upperBounds + def addlb(lb: Type, s: InfVar): Unit= + val v = varSt.getOrElseUpdate(s.sym, new InfVarState) + v.lowerBounds = lb :: v.lowerBounds + def disjor(p: Type, a: InfVar, cs: Ls[K]): Unit = ??? + +class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx): + val objSym = ctx.get("Object").get.symbol.get.asTpe.get + val intSym = ctx.get("Int").get.symbol.get.asTpe.get + val strSym = ctx.get("Str").get.symbol.get.asTpe.get + val errSym = ctx.get("Error").get.symbol.get.asTpe.get + val fnSym = ctx.get("Function").get.symbol.get.asTpe.get + def litSym(x: syntax.Literal) = LitSymbol(x) + +object InfCtx: + def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL): InfCtx = + val prim = new PrimCtx + InfCtx(1, N, HashMap.empty, Bot, Nil, Nil) + (using prim, ctx, HashSet.empty, HashMap.empty, HashMap.empty) + def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, Nil) + def litTy(lit: Literal)(using ctx: InfCtx) = mkTag(ctx.prim.litSym(lit)) + def objTy(using ctx: InfCtx) = mkTag(ctx.prim.objSym) + def funTy(args: Ls[Type], ret: Type, eff: Type)(using ctx: InfCtx) = + val args = Ls(Bot, Wildcard.out(ret), Wildcard.out(eff)) + val i = Ls(true, false, false) + val o = Ls(false, false, false) + ClassLikeType(ctx.prim.fnSym, args, Nil, i, o) + def asRefinedObj(t: Ls[Type])(using ctx: InfCtx) = + val r = t.zipWithIndex.map: + case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) + ClassLikeType(ctx.prim.objSym, Nil, r, Nil, Nil) + // def arrayTy(elem: Type)(using ctx: InfCtx) = ClassLikeType(ctx.getCls("Array"), Ls(elem), Nil, Nil) + // def tupTy(e: Ls[Type])(using ctx: InfCtx, s: Elaborator.State) = + // val refine = (Tree.Ident("size"): Tree.Ident, litTy(IntLit(e.length))) :: e.zipWithIndex.map: + // case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) + // ClassLikeType(ctx.getCls("Array"), Ls(e.foldLeft[Type](Bot)(_ | _)), refine, Nil) + def refinedObj(r: Ls[Tree.Ident -> Type])(using ctx: InfCtx) = + ClassLikeType(ctx.prim.objSym, Nil, r, Nil, Nil) \ No newline at end of file diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala new file mode 100644 index 0000000000..9e00a6509d --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala @@ -0,0 +1,199 @@ +package hkmc2 +package typing +package logicsub + +import hkmc2.utils.*, shorthands.* +import syntax.* +import semantics.*, semantics.Term.* +import utils.* +import scala.collection.mutable.{Set => MutSet} +import utils.Scope, Scope.scope +import Elaborator.State + + +sealed abstract class InfType: + def lvl: Int + def show(using Scope, InfCtx, Raise): Str + def showDbg: Str + +sealed trait TypeArg: + def lvl: Int + def show(using Scope, InfCtx, Raise): Str + def showDbg: Str + def & (that: TypeArg): TypeArg = (this, that) match + case (Wildcard(in1, out1), Wildcard(in2, out2)) => Wildcard(in1 | in2, out1 & out2) + case (ty: Type, Wildcard(in2, out2)) => Wildcard(ty | in2, ty & out2) + case (Wildcard(in1, out1), ty: Type) => Wildcard(in1 | ty, out1 & ty) + case (ty1: Type, ty2: Type) => ty1 & ty2 + def | (that: TypeArg): TypeArg = (this, that) match + case (Wildcard(in1, out1), Wildcard(in2, out2)) => Wildcard(in1 & in2, out1 | out2) + case (ty: Type, Wildcard(in2, out2)) => Wildcard(ty & in2, ty | out2) + case (Wildcard(in1, out1), ty: Type) => Wildcard(in1 & ty, out1 | ty) + case (ty1: Type, ty2: Type) => ty1 | ty2 + def posPart: Type = this match + case Wildcard(_, out) => out + case ty: Type => ty + def negPart: Type = this match + case Wildcard(in, _) => in + case ty: Type => ty + +case class Wildcard(in: Type, out: Type) extends TypeArg: + lazy val lvl = in.lvl.max(out.lvl) + def show(using Scope, InfCtx, Raise): Str = in match + case `out` => in.show + case Bot => + out match + case Top => "?" + case _ => s"out ${out.show}" + case _ => + out match + case Top => s"in ${in.show}" + case _ => s"in ${in.show} out ${out.show}" + def showDbg: Str = s"in ${in.showDbg} out ${out.showDbg}" + +object Wildcard: + def in(ty: Type) = Wildcard(ty, Top) + def out(ty: Type) = Wildcard(Bot, ty) + def empty = Wildcard(Bot, Top) + +case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: InfType) extends InfType: + lazy val lvl = (body :: tvs).map(_.lvl).max + def show(using Scope, InfCtx, Raise) = showDbg //TODO + def showDbg = ??? + +case class PolyFunType(args: Ls[InfType], ret: InfType, eff: Type) extends InfType: + lazy val lvl = (ret :: eff :: args).iterator.map(_.lvl).max + def show(using Scope, InfCtx, Raise) = + s"(${args.map(_.show).mkString(", ")}) ->{${eff.show}} ${ret.show}" + def showDbg = s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.showDbg}" + +sealed abstract class Type extends InfType with TypeArg: + lazy val lvl = toBasic match + case ClassLikeType(name, targs, refinement, i, o) => + val args = targs.iterator + val refine = refinement.iterator.map(_._2) + (args ++ refine).map(_.lvl).maxOption.getOrElse(0) + case InfVar(lvl, _, _) => lvl + case Top | Bot => 0 + case Union(lhs, rhs) => lhs.lvl.max(rhs.lvl) + case Inter(lhs, rhs) => lhs.lvl.max(rhs.lvl) + case Neg(ty) => ty.lvl + def show(using Scope, InfCtx, Raise) = showDbg //TODO + def showDbg: Str = toBasic match + case ClassLikeType(name, targs, refinement, _,_) => + val cls = if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" + val r = refinement.map { case (l,t) => s"$l: ${t.showDbg}" }.mkString(", ") + cls ++ (if refinement.isEmpty then "" else s" & {$r}") + case v @ InfVar(lvl, sym, isSkolem) => + val name = if sym.hint.isEmpty then s"${sym.nme}" else s"${sym.nme}(${sym.hint})" + if isSkolem then s"${name}${sym.uid}_${lvl}" else s"'${name}${sym.uid}_${lvl}" + case Union(lhs, rhs) => s"${lhs.parenDbg} ∨ ${rhs.parenDbg}" + case Inter(lhs, rhs) => s"${lhs.parenDbg} ∧ ${rhs.parenDbg}" + case Neg(ty) => s"¬${ty.parenDbg}" + case Top => "⊤" + case Bot => "⊥" + + protected[logicsub] def paren(using Scope, InfCtx, Raise): Str = toBasic match + case _: InfVar | _: ClassLikeType | _: Neg | Top | Bot => show + case _ => s"($show)" + + protected[logicsub] def parenDbg: Str = toBasic match + case _: InfVar | _: ClassLikeType | _: Neg | Top | Bot => showDbg + case _ => s"($showDbg)" + + lazy val toBasic: BasicType + lazy val discriminator = Discriminator(true)(this).simp + lazy val partialpattern: Bool = simp match + case _: InfVar => false + case Top | Bot => true + case ClassLikeType(s, args, refine,_,o) => + val p = args.iterator.zip(o).forall: + case (t, true) => t.posPart.partialpattern + case (t, false) => t is Wildcard.empty + p && refine.values.forall(_.partialpattern) + case Union(x,y) => x.partialpattern && y.partialpattern + case Inter(x,y) => x.partialpattern && y.partialpattern + case Neg(x) => x.partialpattern + + lazy val simp: BasicType = (toBasic match + case Union(x,y) => x.simp | y.simp + case Inter(x,y) => x.simp & y.simp + case Neg(Union(x,y)) => Neg(x).simp & Neg(y).simp + case Neg(Inter(x,y)) => Neg(x).simp | Neg(y).simp + case Neg(Neg(x)) => x.simp + case Neg(x) => ~x + case x => x).toBasic + + def disjuncts: Ite[Type] = simp match + case Union(x,y) => x.disjuncts ++ y.disjuncts + case x => Ite(x) + + var _dnf: Disj = null + def toDnf(using TL) = + if _dnf eq null then _dnf = NormalForm.dnf(this) + _dnf + + def |(that: Type): Type = this match + case Top => Top + case Bot => that + case _ => that match + case Top => Top + case Bot => this + case Union(l, r) => this | l | r + case _ => if this === that then this else Union(this, that) + def &(that: Type): Type = this match + case Top => that + case Bot => Bot + case _ => that match + case Top => this + case Bot => Bot + case Inter(l, h) => this & l & h + case _ => if this === that then this else Inter(this, that) + def unary_~ : Type = toBasic match + case Top => Bot + case Bot => Top + case Inter(x,y) => ~x | ~y + case Union(x,y) => ~x & ~y + case Neg(x) => x + case _ => Neg(this) + +abstract class TypeExt extends Type + +sealed abstract class BasicType extends Type: + lazy val toBasic = this +final case class InfVar(vlvl: Int, sym: InfVarSymbol, isSkolem: Bool) extends BasicType +object Bot extends BasicType +object Top extends BasicType +case class Union(lhs: Type, rhs: Type) extends BasicType +case class Inter(lhs: Type, rhs: Type) extends BasicType +case class Neg(t: Type) extends BasicType +case class ClassLikeType( + sym: ClsTag, args: Ls[TypeArg], + refinement: Ls[(Tree.Ident, Type)], + in: Ls[Bool], out: Ls[Bool] +) extends BasicType: + private def merge(u: Ls[TypeArg], r: Ls[Tree.Ident -> Type]) = + val targs = args.lazyZip(u).map(_ & _) + val rmap = mergeMap(refinement, r)(_ & _) + val lbl = (refinement.iterator ++ r.iterator).map(_._1).distinct + val refine = lbl.zip(lbl.map(rmap)).toList + ClassLikeType(sym, targs, refine, in, out) + def merge(cs: Ls[ClassLikeType]): Opt[Ls[ClassLikeType]] = cs match + case Nil => S(Ls(this)) + case x :: _ if x.sym is sym => + S(Ls(cs.foldLeft(this)((x, y) => x.merge(y.args, y.refinement)))) + case _ => N +type ClsTag = LitSymbol | TypeSymbol | ModuleOrObjectSymbol + +object Discriminator extends TypeMapper: + override def apply(pol: Bool)(t: Type) = t.simp match + case _: InfVar => Top + case c @ ClassLikeType(_: LitSymbol, _,_,_,_) => c + case c @ ClassLikeType(s: (TypeSymbol | ModuleOrObjectSymbol), args, refine, i,o) => + // TODO flags in `s.defn.get.tparams` + val a = args.iterator.zip(o).map: + case (t, true) => apply(pol)(t.posPart) // TODO + case _ => Wildcard.empty + ClassLikeType(s, a.toList, refine.mapValues(apply(pol)), i,o) + case t @ Neg(ClassLikeType(_, _, refine, _,_)) => if refine.isEmpty then t else Top + case t => super.apply(pol)(t) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala new file mode 100644 index 0000000000..75f11863bb --- /dev/null +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala @@ -0,0 +1,401 @@ +package hkmc2 +package typing +package logicsub + + +import scala.collection.mutable.{HashSet, HashMap, ListBuffer} +import scala.annotation.tailrec + +import hkmc2.utils.*, shorthands.* +import utils.* + +import Message.MessageContext +import semantics.*, Term.*, ucs.FlatPattern +import Elaborator.Ctx +import syntax.* +import Tree.* +import utils.Scope +import hkmc2.codegen.ErasedType.eraseSign + + +class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): + import tl.{trace, log} + private val builtinOps = Elaborator.binaryOps ++ Elaborator.unaryOps ++ Elaborator.aliasOps.keySet + private val solver = new ConstraintSolver(elState, tl) + + private def error(msg: Ls[Message -> Opt[Loc]], extraInfo: => Opt[Any] = N)(using InfCtx) = + raise(ErrorReport(msg, extraInfo = extraInfo)) + Bot // TODO: error type? + + private def typeNames(using ctx: InfCtx) = ctx.typeNames + private def freshVar(origin: Symbol | Term, hint: Str = "")(using ctx: InfCtx) = + // ctx.freshVar(origin, hint) + InfVar(ctx.lvl, InfVarSymbol(origin, hint), false) + private def freshWildcard(s: Symbol)(using InfCtx) = Wildcard(freshVar(s),freshVar(s)) + + private def freshOuter(sym: Symbol)(using ctx: InfCtx): InfVar = + // ctx.freshOuter(sym) + InfVar(ctx.lvl + 1, new InfVarSymbol(sym), true) + + private def mono(ty: InfType)(using ctx: InfCtx): Opt[Type] = ty match + case x: Type => S(x) + case PolyFunType(args, ret, eff) => + val a = args.map(mono) + val r = mono(ret) + if (r::a).exists(_.isEmpty) then N + else S(InfCtx.funTy(a.flatten, r.get, eff)) + case _ => N + + private def monoOrErr(ty: InfType, sc: Located)(using InfCtx): Type = + mono(ty).getOrElse(error(msg"General type is not allowed here." -> sc.toLoc :: Nil)) + + private def tryMkMono(ty: InfType, sc: Located)(using InfCtx, Scope): Type = ty match + case pt: PolyType => tryMkMono(instantiate(pt), sc) + case ft: PolyFunType => + mono(ft).getOrElse: + error(msg"Expected a monomorphic type or an instantiable type here, but ${ty.show} found" -> sc.toLoc :: Nil) + case ty: Type => ty + + private def typeAndSubstType(ty: Term, pol: Bool) + (using map: Map[LocalSymbol, TypeArg], ctx: InfCtx, cctx: CCtx) + : InfType = + def mono(ty: Term, pol: Bool): Type = monoOrErr(typeAndSubstType(ty, pol), ty) + trace[InfType](s"${ctx.lvl}. Typing type ${ty.showDbg}", r => s"~> ${r.showDbg}"): + ty match + case Ref(sym: LocalSymbol) => + log(s"Type lookup: ${sym.nme} ${sym.uid} ${map.keySet}") + map.get(sym) match + case S(Wildcard(in, out)) => if pol then out else in + case S(ty: Type) => ty + case N => ctx.get(sym) match + case S(ty) => ty + case _ => error(msg"Variable not found: ${sym.nme}" -> ty.toLoc :: Nil) + case Term.TyApp(cls, targs) => + // log(s"Type application: ${cls.nme} with ${targs}") + cls.symbol.flatMap(_.asTpe) match + case S(tpeSym) => + if tpeSym.nme === "Any" then Top // FIXME hygiene + else if tpeSym.nme === "Nothing" then Bot // FIXME hygiene + else + val defn = tpeSym.defn.get + if targs.length != defn.tparams.length then + error(msg"Type arguments do not match class definition" -> ty.toLoc :: Nil) + val ts = defn.tparams.lazyZip(targs).map: (tp, t) => + t match + case Term.WildcardTy(in, out) => Wildcard( + in.fold(Bot)(t => mono(t, !pol)), + out.fold(Top)(t => mono(t, pol)) + ) + case _ => + val ta = mono(t, pol) + tp.vce match + case S(false) => Wildcard.in(ta) + case S(true) => Wildcard.out(ta) + case N => ta + val fs = ts.map(_ => false) // TODO + ClassLikeType(tpeSym, ts, Nil, fs, fs) + case N => error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil) + case FunTy(Term.Tup(params), ret, eff) => + val p = params.map { + case Fld(_, p, _) => typeAndSubstType(p, !pol) + case spd: Spd => lastWords(s"unexpected spread in function type parameters: $spd") + } + val e = eff.fold(Bot): e => + typeAndSubstType(e, pol) match + case t: Type => t + case _ => error(msg"Effect cannot be polymorphic." -> ty.toLoc :: Nil) + PolyFunType(p, typeAndSubstType(ret, pol), e) + case f @ Forall(tvs, outer, body) => + val outsym = outer.getOrElse(TempSymbol(S(f), erasedType = N, "outer")) + val outVar = freshOuter(outsym)(using ctx) + val nestCtx = ctx.nestWithOuter(outVar) + outer.foreach(sym => nestCtx += sym -> outVar) + given InfCtx = nestCtx + genPolyType(tvs, outVar, typeAndSubstType(body, pol)) + case Neg(t) => ~mono(t, !pol) + case CompType(lhs, rhs, pol) => + if pol then mono(lhs, pol) | mono(rhs, pol) else mono(lhs, pol) & mono(rhs, pol) + case UnitVal() => InfCtx.objTy + case _ => ty.symbol.flatMap(_.asTpe) match + case S(cls: (ClassSymbol | TypeAliasSymbol)) => typeAndSubstType(Term.TyApp(ty, Nil)(N), pol) + case _ => error(msg"Invalid type" -> ty.toLoc :: Nil, S(ty)) // TODO + + private def genPolyType(tvs: Ls[QuantVar], outer: InfVar, body: => InfType) + (using ctx: InfCtx, cctx: CCtx) = + val bds = tvs.map: + case qv @ QuantVar(sym, ub, lb) => + val tv = freshVar(sym) + ctx += sym -> tv // TODO: a type var symbol may be better... + tv -> qv + bds.foreach: + case (tv, QuantVar(_, ub, lb)) => + ub.foreach(ub => ctx.addub(tv,typeMonoType(ub))) + lb.foreach(lb => ctx.addlb(typeMonoType(lb), tv)) + val lbty = ctx.lbs(tv.sym).foldLeft[Type](Bot)(_ | _) + val ubty = ctx.ubs(tv.sym).foldLeft[Type](Top)(_ & _) + constrain(lbty, ubty) + PolyType(bds.map(_._1), S(outer), body) + + private def typeType(ty: Term)(using ctx: InfCtx, cctx: CCtx): InfType = + typeAndSubstType(ty, true)(using Map.empty) + private def typeMonoType(ty: Term)(using InfCtx, CCtx) = monoOrErr(typeType(ty), ty) + + def typePurely(t: Term)(using InfCtx, Scope) = + val (ty, eff) = typeCheck(t) + given CCtx = CCtx.init(t, N) + constrain(eff, Bot) + ty + + private def constrain(x: Type, y: Type)(using ctx: InfCtx, cctx: CCtx): Unit = + ctx.constrain(solver, ctx.sub(x,y)) + + private def fundef(sym: Symbol, lam: Term, sig: Opt[Term]) + (using ctx: InfCtx, cctx: CCtx, scope: Scope) = lam match + case Term.Lam(params, body) => sig match + case S(sig) => + val sigTy = typeType(sig) + ctx += sym -> sigTy + ascribe(lam, sigTy) + () + case N => + val outer = freshOuter(new TempSymbol(S(lam), erasedType = N, "outer"))(using ctx) + given InfCtx = ctx.nestWithOuter(outer) + val funTyV = freshVar(sym) + ctx += sym -> funTyV // for recursive functions + val (res, _) = typeCheck(lam) + val funTy = tryMkMono(res, lam) + given CCtx = CCtx.init(lam, N) + constrain(funTy, funTyV) + ctx += sym -> generalize(funTy, S(outer), ctx.lvl + 1) + case _ => + error(msg"Function definition shape not yet supported for ${sym.nme}" -> lam.toLoc :: Nil) + + def instantiate(x: InfType): Type = ??? + def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int): PolyType = ??? + + private def app(lhs: InfType, lhsEff: Type, rhs: Ls[Elem], t: Term) + (using ctx: InfCtx, cctx: CCtx, scope: Scope) + : (InfType, Type) = lhs match + case PolyFunType(params, ret, eff) => + // * if the function type is known, we can directly use it + if params.length != rhs.length + then (error(msg"Incorrect number of arguments" -> t.toLoc :: Nil), Bot) + else + var resEff: Type = lhsEff | eff + rhs.lazyZip(params).foreach: + case (f: Fld, t) => + val (ty, ef) = ascribe(f.term, t) + resEff |= ef + case (spd: Spd, _) => TODO(s"spread arguments: $spd") + (ret, resEff) + case ClassLikeType(s, (params: ClassLikeType) :: ret :: eff :: Nil, _,_,_) + if s === ctx.prim.fnSym && params.sym === ctx.prim.objSym => + app(PolyFunType(params.refinement.values.toList, ret.posPart, eff.posPart), lhsEff, rhs, t) + case ty: PolyType => app(instantiate(ty), lhsEff, rhs, t) + case funTy => + val (argTy, argEff) = rhs.flatMap: + case f: Fld => + val (ty, eff) = typeCheck(f.term) + Left(ty) :: Right(eff) :: Nil + case spd: Spd => TODO(s"spread arguments: $spd") + .partitionMap(x => x) + val effVar = freshVar(TempSymbol(S(t), erasedType = N, "eff")) + val retVar = freshVar(TempSymbol(S(t), erasedType = N, "app")) + constrain(tryMkMono(funTy, t), InfCtx.funTy(argTy.map(tryMkMono(_, t)), retVar, effVar)) + (retVar, argEff.foldLeft[Type](effVar | lhsEff)((res, e) => res | e)) + + + private def selproj(t: Term, cls: Term, field: Tree.Ident)(using InfCtx, CCtx, Scope) + : (InfType, Type) = + val (ty, eff) = typeCheck(t) + cls.symbol.flatMap(_.asCls.flatMap(sym => sym.defn.map(sym -> _))) match + case S(clsSym -> clsDfn) => + val map = HashMap[LocalSymbol, TypeArg]() + val targs = clsDfn.tparams.map { + case TyParam(_, _, targ) => + val ty = freshWildcard(targ) + map += targ -> ty + ty + } + val fs = targs.map(_ => false) // TODO + constrain(tryMkMono(ty, t), ClassLikeType(clsSym, targs, Nil, fs, fs)) + require(clsDfn.paramsOpt.forall(_.restParam.isEmpty)) + (clsDfn.paramsOpt.fold(Nil)(_.params).map { + case Param(_, sym, sign, _) => + if sym.nme === field.name then sign else N + }.filter(_.isDefined)) match + case S(res) :: Nil => (typeAndSubstType(res, pol = true)(using map.toMap), eff) + case _ => (error(msg"${field.name} is not a valid member in class ${clsSym.nme}" -> t.toLoc :: Nil), Bot) + case N => + (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot) + + private def newobj(cls: Term, args: Ls[Term])(using InfCtx, CCtx, Scope) = + cls.symbol.flatMap(_.asCls.flatMap(_.defn)) match + case S(clsDfn: ClassDef.Parameterized) => + require(clsDfn.paramsOpt.forall(_.restParam.isEmpty)) + val argsList = args match + case Nil => Nil + case Term.Tup(elems) :: Nil => elems.map: + case PlainFld(term) => term + case _ => ??? + case _ => ??? + if argsList.length != clsDfn.params.params.length then + (error(msg"The number of parameters is incorrect" -> cls.toLoc :: Nil), Bot) + else + val map = HashMap[LocalSymbol, TypeArg]() + val targs = clsDfn.tparams.map { + case TyParam(_, S(_), targ) => + val ty = freshVar(targ) + map += targ -> ty + ty + case TyParam(_, N, targ) => + // val ty = freshWildcard // FIXME probably not correct + val ty = freshVar(targ) + map += targ -> ty + ty + } + val effBuff = ListBuffer.empty[Type] + require(clsDfn.paramsOpt.forall(_.restParam.isEmpty)) + argsList.iterator.zip(clsDfn.params.params).foreach { + case (arg, Param(sign = S(sign))) => + val (ty, eff) = ascribe(arg, typeAndSubstType(sign, pol = true)(using map.toMap)) + effBuff += eff + case _ => ??? + } + val fs = targs.map(_ => false) // TOOD + (ClassLikeType(clsDfn.sym, targs, Nil, fs, fs), effBuff.foldLeft[Type](Bot)((res, e) => res | e)) + case S(clsDfn: ClassDef.Plain) => ??? // TODO + case N => + (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot) + + def ascribe(lhs: Term, rhs: InfType)(using ctx: InfCtx, scope: Scope): (InfType, Type) = // TODO + trace[(InfType, Type)](s"${ctx.lvl}. Ascribing ${lhs.showDbg} : ${rhs.showDbg}", res => s"! ${res._2.showDbg}"): + given CCtx = CCtx.init(lhs, S(rhs)) + (lhs, rhs) match + case (Term.Lam(PlainParamList(params), body), ft @ PolyFunType(args, ret, eff)) => // * annoted functions + if params.length != args.length then + (error(msg"Cannot type this ${lhs.describe} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot) + else + val nestCtx = ctx.nest + val argsTy = params.zip(args).map: + case (Param(sym = sym), ty) => + nestCtx += sym -> ty + ty + given InfCtx = nestCtx + val (_, effTy) = ascribe(body, ret) + constrain(effTy, eff) + (ft, Bot) + case (Term.Lam(params, body), ft @ ClassLikeType(fn, (args: ClassLikeType)::ret::eff::Nil, _,_,_)) + if fn === ctx.prim.fnSym => + ascribe(lhs, PolyFunType(args.refinement.values.toList, ret.posPart, eff.posPart)) + case (term, pt @ PolyType(_, outer, _)) => // * generalize + val nextCtx = outer match + case S(outer) => ctx.nestWithOuter(outer) + case N => ctx.nextLevel + // given InfCtx = nextCtx + // constrain(ascribe(term, skolemize(pt))._2, Bot) // * never generalize terms with effects + // (pt, Bot) + ??? + // case (Term.IfLike(_, IfLikeForm.ReturningIf, split), ty) => // * propagate + // typeAllSplits(split.getExpandedSplit, S(ty)) + case (Term.Asc(term, ty), rhs) => + ascribe(term, typeType(ty)) + ascribe(term, rhs) + case _ => + val (lhsTy, eff) = typeCheck(lhs) + rhs match + case pf: PolyFunType if mono(pf).isEmpty => + (error(msg"Cannot type non-function term ${lhs.toString} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot) + case _ => + constrain(tryMkMono(lhsTy, lhs), monoOrErr(rhs, lhs)) + (rhs, eff) + + def typeCheck(t: Term)(using ctx: InfCtx, scope: Scope): (InfType, Type) = + trace[(InfType, Type)](s"${ctx.lvl}. Typing ${t.showDbg}", r => s": (${r._1.showDbg}, ${r._2.showDbg})"): + given CCtx = CCtx.init(t, N) + t match + case Term.Error() => (Bot, Bot) // TODO: error type? + case UnitVal() => (InfCtx.objTy, Bot) + case Lit(lit) => (InfCtx.litTy(lit), Bot) + case Ref(sym) => + ctx.get(sym) match + case Some(ty) => (ty, Bot) + case _ => (error(msg"Variable not found: ${sym.nme}" -> t.toLoc :: Nil), Bot) + case t @ Term.App(lhs, Term.Tup(rhs)) => + val (funTy, lhsEff) = typeCheck(lhs) + app(funTy, lhsEff, rhs, t) + case trm @ Term.Sel(t, l) => + val (ty, eff) = typeCheck(t) + val r = freshVar(trm, "") + constrain(tryMkMono(ty, t) , InfCtx.refinedObj(Ls(l -> r))) + (r, eff) + case sel @ Term.SynthSel(Ref(_: TopLevelSymbol), nme) if sel.symbol.isDefined => + typeCheck(Ref(sel.symbol.get)(sel.nme, N)) + case Term.SelProj(term, cls, field) => selproj(term, cls, field) + case Term.Tup(fields) => // TODO tup type + var eff: Type = Bot + val fs = fields.zipWithIndex.map: + case (f: Fld, i) => + val (ty, ef) = typeCheck(f.term) + eff |= ef + (Tree.Ident(i.toString): Tree.Ident, tryMkMono(ty, f)) + case (spd: Spd, _) => TODO(s"spread arguments: $spd") + (InfCtx.refinedObj(fs), eff) + // case Term.IfLike(_, IfLikeForm.ReturningIf, split) => typeAllSplits(split.getExpandedSplit, N) + case Lam(PlainParamList(params), body) => + val nestCtx = ctx.nest + given InfCtx = nestCtx + val tvs = params.map: + case Param(_, sym, sign, _) => + val ty = sign.map(s => typeType(s)(using nestCtx)).getOrElse(freshVar(sym)) + nestCtx += sym -> ty + ty + val (bodyTy, eff) = typeCheck(body) + (PolyFunType(tvs, bodyTy, eff), Bot) + case Blk(stats, res) => + val effBuff = ListBuffer.empty[Type] + def goStats(stats: Ls[Statement]): Unit = stats match + case Nil => () + case (term: Term) :: stats => + effBuff += typeCheck(term)._2 + goStats(stats) + case LetDecl(sym, _) :: DefineVar(sym2, rhs) :: stats => + require(sym2 is sym) + val (rhsTy, eff) = typeCheck(rhs) + effBuff += eff + ctx += sym -> rhsTy + goStats(stats) + case (td @ TermDefinition(k = Fun, params = ps :: Nil, sign = sig, body = S(body))) :: stats => + fundef(td.sym, Term.Lam(ps, body), sig) + goStats(stats) + case (td @ TermDefinition(k = Fun, params = Nil, sign = sig, body = S(body))) :: stats => + fundef(td.sym, body, sig) // * may be a case expressions + goStats(stats) + case (td1 @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: (td2 @ TermDefinition(k = Fun, body = S(body))) :: stats + if td1.sym === td2.sym => goStats(td2 :: stats) // * avoid type check signatures twice + case (td @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: stats => + ctx += td.sym -> typeType(sig) + goStats(stats) + case (clsDef: ClassDef) :: stats => + typeNames.add(clsDef.sym.nme) + // clsDef.ext match + // case S(Term.New(ty, _, N)) => createADTCtor(clsDef, ty) + // case _ => () + goStats(stats) + case (modDef: ModuleOrObjectDef) :: stats => + typeNames.add(modDef.sym.nme) + goStats(stats) + case Import(sym, str, pth) :: stats => + goStats(stats) // TODO: + case stat :: _ => + // TODO(stat) // TODO + goStats(stats) + val (ty, eff) = typeCheck(res) + (ty, effBuff.foldLeft(eff)((res, e) => res | e)) + case Term.New(cls, args, N) => newobj(cls, args) + case Term.Asc(term, ty) => + val res = typeType(ty)(using ctx) + ascribe(term, res) + case Term.Annotated(Annot.Untyped, _) => (Bot, Bot) + case _ => + (error(msg"Term shape not yet supported by InvalML: ${t.toString}" -> t.toLoc :: Nil), Bot) diff --git a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls index 23d42bfd4f..86534e33a8 100644 --- a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls +++ b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls @@ -220,3 +220,4 @@ applyTwice(fst, Pair(1, 2)) allowUnresolvedAccesses: false, useNewResolution: true, typeCheck: None)) +//│ Type: undefined diff --git a/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls b/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls index 99df8ea09e..580a66f480 100644 --- a/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls +++ b/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls @@ -1,4 +1,5 @@ :NewDefs +//│ /!\ Unrecognized command: NewDefs @@ -9,7 +10,11 @@ fun f(x, y) = if x === 0 then true 1 then false else false -//│ fun f: (Eql[0 | 1], Eql[0 | 1]) -> Bool +//│ FAILURE: Unexpected parse error +//│ FAILURE LOCATION: concludeWithImpl (Parser.scala:270) +//│ ╔══[PARSE ERROR] Unexpected 'else' keyword here +//│ ║ l.12: else false +//│ ╙── ^^^^ fun f(x, y) = if x === 0 then true @@ -17,36 +22,26 @@ fun f(x, y) = if x === else if y === 0 then true _ then false -//│ fun f: (Eql[0 | 1], Eql[0]) -> Bool module Tru module Fals -//│ module Tru -//│ module Fals :e fun f(x, y) = if x is Tru and y is Tru then true Fals and y is Fals then false -//│ ╔══[ERROR] when `x` is `Tru` -//│ ║ l.29: Tru and y is Tru then true -//│ ║ ^^^ -//│ ╟── `y` has 1 missing case -//│ ║ l.29: Tru and y is Tru then true -//│ ║ ^ -//│ ╟── it can be module `Fals` -//│ ║ l.30: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ ╔══[ERROR] when `x` is `Fals` -//│ ║ l.30: Fals and y is Fals then false -//│ ║ ^^^^ -//│ ╟── `y` has 1 missing case -//│ ║ l.30: Fals and y is Fals then false -//│ ║ ^ -//│ ╟── it can be module `Tru` -//│ ║ l.29: Tru and y is Tru then true +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.31: Tru and y is Tru then true +//│ ╙── ^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.31: Tru and y is Tru then true //│ ╙── ^^^ -//│ fun f: (Fals | Tru, nothing) -> Bool +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.32: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.32: Fals and y is Fals then false +//│ ╙── ^^^^ // The base case. fun f(x, y) = if x is @@ -54,7 +49,46 @@ fun f(x, y) = if x is Fals and y is Fals then false Tru and y is Fals then true Fals and y is Tru then true -//│ fun f: (Fals | Tru, Fals | Tru) -> Bool +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.48: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.48: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.49: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.49: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.50: Tru and y is Fals then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.50: Tru and y is Fals then true +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.51: Fals and y is Tru then true +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.51: Fals and y is Tru then true +//│ ╙── ^^^ // Replace the `x is Fals` with `_` fun f(x, y) = if x is @@ -63,39 +97,95 @@ fun f(x, y) = if x is _ and y is Tru then true Fals then false -//│ fun f: (Object, Fals | Tru) -> Bool +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.95: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.95: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.96: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.96: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.98: Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.99: Fals then false +//│ ╙── ^^^^ f(Tru, Tru) f(Tru, Fals) f(Fals, Tru) f(Fals, Fals) -//│ Bool -//│ res -//│ = true -//│ res -//│ = false -//│ res -//│ = true -//│ res -//│ = false +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. +//│ ║ l.131: f(Tru, Tru) +//│ ║ ^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. +//│ ║ l.131: f(Tru, Tru) +//│ ║ ^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. +//│ ║ l.132: f(Tru, Fals) +//│ ║ ^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. +//│ ║ l.132: f(Tru, Fals) +//│ ║ ^^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. +//│ ║ l.133: f(Fals, Tru) +//│ ║ ^^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. +//│ ║ l.133: f(Fals, Tru) +//│ ║ ^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. +//│ ║ l.134: f(Fals, Fals) +//│ ║ ^^^^ +//│ ╙── Module argument passed to a non-module parameter. +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: traverse (Resolver.scala:350) +//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. +//│ ║ l.134: f(Fals, Fals) +//│ ║ ^^^^ +//│ ╙── Module argument passed to a non-module parameter. :e fun g(x, y) = if x is true and y is true then true false and y is false then false -//│ ╔══[ERROR] `y` has 1 missing case -//│ ║ l.84: true and y is true then true -//│ ║ ^ -//│ ╟── it can be Boolean value `false` -//│ ║ l.85: false and y is false then false -//│ ╙── ^^^^^ -//│ ╔══[ERROR] `y` has 1 missing case -//│ ║ l.85: false and y is false then false -//│ ║ ^ -//│ ╟── it can be Boolean value `true` -//│ ║ l.84: true and y is true then true -//│ ╙── ^^^^ -//│ fun g: (Bool, nothing) -> Bool +//│ FAILURE: Unexpected lack of compilation or type error // Test with real booleans fun g(x, y) = if x is @@ -104,7 +194,6 @@ fun g(x, y) = if x is _ and y is true then true false then false -//│ fun g: (Object, Bool) -> Bool // Chained UCS terms fun f(x, y) = if x is @@ -113,7 +202,36 @@ fun f(x, y) = if x is else if y is Tru then true Fals then false -//│ fun f: (Object, Fals | Tru) -> Bool +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.200: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.200: Tru and y is Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.201: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.201: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.203: Tru then true +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.204: Fals then false +//│ ╙── ^^^^ :e fun f(x, y) = if x is @@ -122,53 +240,43 @@ fun f(x, y) = if x is else if y is Tru and x is Fals then true Fals and x is Tru then false -//│ ╔══[ERROR] when `y` is `Tru` -//│ ║ l.123: Tru and x is Fals then true -//│ ║ ^^^ -//│ ╟── `x` has 1 missing case -//│ ║ l.123: Tru and x is Fals then true -//│ ║ ^ -//│ ╟── it can be module `Tru` -//│ ║ l.124: Fals and x is Tru then false -//│ ╙── ^^^ -//│ ╔══[ERROR] when `y` is `Fals` -//│ ║ l.124: Fals and x is Tru then false -//│ ║ ^^^^ -//│ ╟── `x` has 1 missing case -//│ ║ l.124: Fals and x is Tru then false -//│ ║ ^ -//│ ╟── it can be module `Fals` -//│ ║ l.123: Tru and x is Fals then true -//│ ╙── ^^^^ -//│ ╔══[ERROR] Type mismatch in `case` expression: -//│ ║ l.123: Tru and x is Fals then true -//│ ║ ^^^^^^^^^^^^^^^^^^^ -//│ ╟── class pattern of type `Tru` is not an instance of type `Fals` -//│ ║ l.120: Tru and y is Tru then true -//│ ║ ^^^ -//│ ╟── but it flows into reference with expected type `Fals` -//│ ║ l.123: Tru and x is Fals then true -//│ ║ ^ -//│ ╟── Note: constraint arises from class pattern: -//│ ║ l.123: Tru and x is Fals then true +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.238: Tru and y is Tru then true +//│ ╙── ^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.238: Tru and y is Tru then true +//│ ╙── ^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.239: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.239: Fals and y is Fals then false +//│ ╙── ^^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.241: Tru and x is Fals then true +//│ ╙── ^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.241: Tru and x is Fals then true //│ ╙── ^^^^ -//│ ╔══[ERROR] Type mismatch in `case` expression: -//│ ║ l.124: Fals and x is Tru then false -//│ ║ ^^^^^^^^^^^^^^^^^^^ -//│ ╟── class pattern of type `Fals` is not an instance of type `Tru` -//│ ║ l.121: Fals and y is Fals then false -//│ ║ ^^^^ -//│ ╟── but it flows into reference with expected type `Tru` -//│ ║ l.124: Fals and x is Tru then false -//│ ║ ^ -//│ ╟── Note: constraint arises from class pattern: -//│ ║ l.124: Fals and x is Tru then false +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.242: Fals and x is Tru then false +//│ ╙── ^^^^ +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.242: Fals and x is Tru then false //│ ╙── ^^^ -//│ fun f: (Fals | Tru, Fals | Tru) -> Bool fun h(x, y, p) = if x and p(x) then 0 y is Tru then 1 Fals then 2 -//│ fun h: forall 'a. ('a & Bool, Fals | Tru, 'a -> Bool) -> (0 | 1 | 2) +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. +//│ ║ l.271: Tru then 1 +//│ ╙── ^^^ +//│ FAILURE: Unexpected compilation error +//│ FAILURE LOCATION: go (Elaborator.scala:2756) +//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. +//│ ║ l.272: Fals then 2 +//│ ╙── ^^^^ diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala new file mode 100644 index 0000000000..89f4c05ade --- /dev/null +++ b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala @@ -0,0 +1,33 @@ +package hkmc2 + +import hkmc2.utils.*, shorthands.* + +import hkmc2.semantics.* +import hkmc2.typing.* +import utils.Scope +import hkmc2.syntax.Keyword.undefined + + +abstract class LogicSubDiffMaker extends WasmDiffMaker: + + lazy val infctx = + given Elaborator.Ctx = curCtx + logicsub.InfCtx.init + + var typer: Opt[logicsub.Typer] = None + + override def processTerm(trm: semantics.Term.Blk, inImport: Bool)(using Config, Raise): Unit = + super.processTerm(trm, inImport) + if summon[Config].language.typeCheck.isDefined then + given Scope = Scope.empty(Scope.Cfg.default) + if typer.isEmpty then + given Elaborator.Ctx = curCtx + typer = S(logicsub.Typer()) + given logicsub.InfCtx = infctx + val ty = typer.get.typePurely(trm) + output(s"Type: ${ty.show}") + ty match + case x: logicsub.InfVar => + output(s" >: ${infctx.lbs(x.sym).foldLeft(logicsub.Bot:logicsub.Type)(_|_).toBasic.show}") + case _ => + diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala index 573bf03e78..89c30aff81 100644 --- a/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala +++ b/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala @@ -9,7 +9,7 @@ import hkmc2.utils.*, shorthands.* abstract class MainDiffMaker (val rootPath: Str, val file: io.Path, val preludeFile: io.Path, val predefFile: io.Path, val relativeName: Str) - extends WasmDiffMaker: + extends LogicSubDiffMaker: // println(s"Running diff test for $relativeName") // * useful to debug nonterminating tests From 5905d7b0964a937b468be6eba8df124d009f72e7 Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Tue, 20 Oct 2026 13:18:43 +0800 Subject: [PATCH 2/6] draft progress --- .../scala/hkmc2/typing/ConstraintSolver.scala | 131 +++++--- .../main/scala/hkmc2/typing/NormalForm.scala | 22 +- .../scala/hkmc2/typing/TypeTraverser.scala | 5 +- .../src/main/scala/hkmc2/typing/infctx.scala | 99 +++--- .../src/main/scala/hkmc2/typing/inftype.scala | 56 +++- .../main/scala/hkmc2/typing/logicsub.scala | 120 ++++++-- .../test/mlscript/codegen/ConfigDirective.mls | 2 +- .../mlscript/ucs/staging/legacy/ElseIf.mls | 288 ++++++------------ .../test/scala/hkmc2/LogicSubDiffMaker.scala | 27 +- 9 files changed, 404 insertions(+), 346 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala index da3c7b3fd4..140cf537de 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala @@ -3,7 +3,7 @@ package typing package logicsub import scala.collection.mutable - +import syntax.* import semantics.* import Message.MessageContext import hkmc2.utils.*, shorthands.* @@ -14,16 +14,16 @@ type Cache = mutable.HashSet[(Type, Type)] type ExtrudeCache = mutable.HashMap[(InfVarSymbol, Bool), InfVar] case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])(using Scope): - def err(using Raise, InfCtx) = - raise(ErrorReport( - msg"Type error in ${origin.describe}${exp match - case S(ty) => msg" with expected type ${ty.show}" - case N => msg"" - }" -> origin.toLoc - :: parents.reverse.map(p => - msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N - ) - )) + def err(using raise: Raise, ctx: InfCtx, tl: TL) = + ctx.err(ErrorReport( + msg"Type error in ${origin.describe}${exp match + case S(ty) => msg" with expected type ${ty.show}" + case N => msg"" + }" -> origin.toLoc + :: parents.reverse.map(p => + msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N + ) + ))(using this) def nest(sub: (Type, Type)): CCtx = copy(cache = cache += sub, parents = parents match case `sub` :: _ => parents @@ -33,53 +33,92 @@ object CCtx: inline def init(origin: Term, exp: Opt[InfType])(using Scope) = CCtx(mutable.HashSet.empty, Nil, origin, exp) -class ConstraintSolver(elState: Elaborator.State, tl: TraceLogger)(using Raise): - import tl.{trace, log} +object ConstraintSolver: + private def log(msg: => Any, noIndent: Bool = false)(using tl: TL) = tl.log(msg, noIndent) - private def constrainConj(conj: Conj)(using ctx: InfCtx, cctx:CCtx, tl: TL): Unit = trace(s"Constraining ${conj.showDbg}"): + private def constrainConj(conj: Conj)(using ctx: InfCtx, cctx:CCtx, tl: TL, raise: Raise): Unit = + tl.trace(s"Constraining ${conj.showDbg}"): conj match - case Conj(i, u, S(v), w, _, _) => - val rest = Conj(i, u, N, w, Nil,Nil) + case Conj(i, u, S(v), w, xs, ys) => + val rest = Conj(i, u, N, w, xs, ys) val bd = if v.lvl >= rest.lvl then rest else ??? // extrude(rest)(using v.lvl, true, mutable.HashMap.empty) val nc = (~bd).toDnf // always cache the normal form to avoid unexpected cache misses log(s"New bound: ${v.showDbg} <: ${nc.showDbg}") cctx.nest(v.toDnf -> nc) givenIn: - // v.state.upperBounds ::= nc - // v.state.lowerBounds.foreach(lb => constrain(lb, nc)) ctx.addub(v, nc) - case Conj(i, u, N, S(v), _,_) => - val rest = Conj(i, u, N,N,Nil,Nil) - val bd = if v.lvl >= rest.lvl then rest else ??? // extrude(rest)(using v.lvl, true, mutable.HashMap.empty) - val c = bd.toDnf // always cache the normal form to avoid unexpected cache misses + case Conj(i, u, N, S(v), xs,ys) => + val rest = Conj(i, u, N,N,xs,ys) + val c = rest.toDnf // always cache the normal form to avoid unexpected cache misses log(s"New bound: ${v.showDbg} :> ${c.showDbg}") cctx.nest(c -> v.toDnf) givenIn: - // v.state.lowerBounds ::= c - // v.state.upperBounds.foreach(ub => constrain(c, ub)) ctx.addlb(c, v) case Conj(NF.Inter(x :: Nil), NF.Union(Nil), N,N,_,_) => - val da = x.args.iterator.zip(x.out).collect: + val da = x.args.iterator.zip(x.congr).collect: case (t, true) => t.posPart val d = (x.refinement.values ++ da).toList if d.isEmpty then cctx.err - else ctx.constrain(this, d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.subor(k, ctx.sub(t, Bot)))) - case Conj(NF.Inter(x :: Nil), NF.Union(ClassLikeType(y, yargs, yrefine, in, _) :: Nil), N,N,_,_) => ??? - case Conj(NF.Inter(x :: xs), NF.Union(ClassLikeType(y, yargs, yrefine, in, _) :: Nil), N,N,_,_) => ??? - case Conj(NF.Inter(x :: xs), NF.Union(y :: ys), N,N,_,_) => ??? -// case Conj(Ninter(S(ClassLikeType(c1, a1, r1, _))), Nunion(ClassLikeType(c2, a2, r2, _) :: rest), N, N) => -// case Conj(Ninter(S(c)), Nunion(d :: rest), N, N) => -// if c.sym === d.sym then -// c.args.zip(d.args).foreach: (ta1, ta2) => -// constrainArgs(ta1, ta2) -// // TODO -// else constrainConj(Conj(conj.i, Nunion(rest), N, N)) case _ => - // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil)) + else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.subor(k, ctx.sub(t, Bot)))) + case Conj(NF.Inter(x :: Nil), NF.Union(y :: Nil), N,N,_,_) => + val da = x.args.iterator.zip(x.congr).collect: + case (t, true) => t.posPart + val d = (x.refinement.values ++ da).toList + val xrm = x.refinement.toMap + val yrm = y.refinement.toMap + val sp = ctx.asSubcls(x,y.sym) + if sp.isEmpty || !yrm.keySet.subsetOf(xrm.keySet) then + if d.isEmpty then cctx.err + else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.subor)) + else + val x = sp.get + val u = x.args.zip(y.args).flatMap(ctx.subArg) + val w = y.refinement.map: + case (a,b) => ctx.sub(xrm(a), b) + val ds = x.refinement.filterNot(f => yrm.contains(f._1)).map: + case (_,t) => ctx.sub(t,Bot) + (u++w).foreach: k => + ctx.constrain((ds ++ Ls(k)).reduce(ctx.subor)) + case Conj(NF.Inter(xs @ (x :: _)), NF.Union(y :: Nil), N,N,_,_) => + if x.sym === y.sym then + val k = x.ov.get + val u = xs.map(_.args(k).negPart.discriminator) + val w = u.reduce[Type](_|_) + val in = y.args(k) + ctx.constrain(ctx.sub(in.negPart, w)) + u.lazyZip(xs).foreach: (p, c) => + val d = ctx.sub(in.negPart, ~p) + val r = y.copy(args = y.args.updated(k, Wildcard(p & in.negPart, in.posPart))) + val s = ctx.sub(c, r) + ctx.constrain(ctx.subor(d, s)) + else cctx.err + case Conj(k @ NF.Inter(x :: _), NF.Union(ys @ (_ :: _)), N,N,ws,zs) => + def h(y: ClassLikeType) = + def f(u: Ls[TypeArg], w: Ls[TypeArg], s: Ls[TypeArg], p:Ls[Bool]) + : Ls[ClassLikeType] = (w,p) match + case (Nil, _) => Nil + case (t::ws, true::ps) => + val a = u ++ (Wildcard.out(~t.posPart)::s) + y.copy(args = a) :: f(s.head::u, ws, s.tail, ps) + case (t::ws, false::ps) => f(s.head::u, ws, s.tail, ps) + case _ => ??? + def g(u: Ls[(Tree.Ident, Type)]) = + val w = y.args.map(_ => Wildcard.empty) + y.refinement.map((a,t) => y.copy(args = w, refinement = (a,~t)::Nil)) + f(Nil, y.args, y.args.map(_ => Wildcard.empty), y.congr) ++ g(y.refinement) + val (ps,t) = ys.partition(_.partialpattern) + val xrs = x.refinement.keys.toSet + val qs = ps.filter(p => ctx.asSubcls(x,p.sym).isDefined && p.refinement.keys.forall(xrs.contains)) + val ks = qs.foldLeft(Ls(k)): (ks, y) => + ks.flatMap(k => h(y).map(c => k.merge(NF.Inter(Ls(c))).get)) + ks.foreach(k => constrainConj(Conj(k, NF.Union(t),N,N,ws,zs))) + case _ => + raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil)) cctx.err - private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using InfCtx, CCtx, TL): Unit = - constrain(rhs.negPart, lhs.negPart) - constrain(lhs.posPart, rhs.posPart) + private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = + ctx.constrain(ctx.sub(rhs.negPart, lhs.negPart)) + ctx.constrain(ctx.sub(lhs.posPart, rhs.posPart)) - private class SkolemBoundsInliner(using ctx: InfCtx) extends TypeMapper: + private class SkolemBoundsInliner(using ctx: InfCtx) extends TypeMap: val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty override def apply(pol: Bool)(t: Type) = t.toBasic match case v @ InfVar(_, s, true) if !cache(s) => @@ -92,20 +131,20 @@ class ConstraintSolver(elState: Elaborator.State, tl: TraceLogger)(using Raise): private def inlineSkolemBounds(ty: Type)(using InfCtx): Type = (new SkolemBoundsInliner)(true)(ty) - private def constrainImpl(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL): Unit = + private def constrainImpl(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = val p = lhs.toDnf -> rhs.toDnf if cctx.cache(p) then log(s"Cached!") - else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): + else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): cctx.nest(p) givenIn: val disj = inlineSkolemBounds(lhs & ~rhs).toDnf disj.cs.foreach(constrainConj(_)) - def constrain(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL): Unit = - val (ps, ts) = rhs.disjuncts.partition(_.partialpattern) + def constrain(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = + val (ps, ts) = rhs.disjuncts.toList.partition(_.partialpattern) if ts.length > 1 then val p = lhs.toDnf -> rhs if cctx.cache(p) then log(s"Cached!") - else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): + else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): cctx.nest(p) givenIn: val u = ps.foldLeft(lhs)((x, y) => x & ~y) val qs = ts.map(_.discriminator) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala index 1aa2a77dc7..0cdcb58683 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala @@ -42,16 +42,14 @@ final case class Conj( tl.traceNot[Opt[Conj]](s"merge ${this.showDbg} and ${that.showDbg}", r => s"= ${r.map(_.showDbg)}"): val Conj(i1, u1, v1, w1, x1, y1) = this val Conj(i2, u2, v2, w2, x2, y2) = that - val xs = x1 ++ x2 - val ys = y1 ++ y2 + val xs = (x1 ++ x2).distinct + val ys = (y1 ++ y2).distinct if xs.intersect(ys).nonEmpty then N - else i1.merge(i2) match - case N => N - case S(i) => - val u = u1.merge(u2) - (v1.orElse(v2), w1.orElse(w2)) match - case (S(v), S(w)) if v.sym === w.sym => N - case (v,w) => S(Conj(i, u, v, w, xs, ys)) + else i1.merge(i2).flatMap: i => + val u = u1.merge(u2) + (v1.orElse(v2), w1.orElse(w2)) match + case (S(v), S(w)) if v.sym === w.sym => N + case (v,w) => S(Conj(i, u, v, w, xs, ys)) object Conj: val empty: Conj = Conj(NF.Inter.empty, NF.Union.empty, N, N, Nil, Nil) @@ -84,7 +82,7 @@ object NormalForm: case u: NF.Union => Disj(Ls(Conj(NF.Inter(Nil), u, N, N, Nil, Nil))) case v: InfVar => Disj(Ls(Conj.mkVar(v, false))) case ct: ClassLikeType => Disj(Ls(Conj.mkUnion(ct))) - case _ => dnf(~(ty.toBasic)) + case _ => (~ty.toBasic).toDnf def dnf(ty: Type)(using TL): Disj = tl.traceNot[Disj](s"Disj ${ty.showDbg} ${ty.getClass}", r => s"= ${r.showDbg}"): @@ -97,6 +95,6 @@ object NormalForm: case Bot => Disj.bot case v: InfVar => Disj(Ls(Conj.mkVar(v, true))) case ct: ClassLikeType => Disj(Conj.mkInter(ct) :: Nil) - case Inter(lhs, rhs) => inter(dnf(lhs), dnf(rhs)) - case Union(lhs, rhs) => union(dnf(lhs), dnf(rhs)) + case Inter(lhs, rhs) => inter(lhs.toDnf, rhs.toDnf) + case Union(lhs, rhs) => union(lhs.toDnf, rhs.toDnf) case Neg(ty) => neg(ty) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala index 1a517a9a3e..8c566e53e8 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala @@ -24,8 +24,9 @@ import hkmc2.utils.*, shorthands.* // refine.values.foreach(apply(pol)) // case _ => -class TypeMapper: - def applyArg(pol: Bool)(t: TypeArg): TypeArg = ??? +class TypeMap: + def applyArg(pol: Bool)(t: TypeArg): TypeArg = + Wildcard(apply(!pol)(t.negPart), apply(pol)(t.posPart)) def apply(pol: Bool)(t: Type): Type = t.toBasic match case Bot | Top | _: InfVar => t case Union(x, y) => Union(apply(pol)(x), apply(pol)(y)) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala index 75920279d7..8670923227 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala @@ -30,75 +30,106 @@ final case class InfCtx( val env: HashMap[Symbol, InfType], val outRegAcc: Type, val prefix: Ls[Ls[Type->Type]], - val suffix: Ls[K] + val suffix: Ls[K], // TODO mutable )(using + val varSt: HashMap[InfVarSymbol, InfVarState], val prim: PrimCtx, val ctx: Ctx, - val typeNames: HashSet[Str], - val symbolCache: HashMap[Str, TypeSymbol], - val varSt: HashMap[InfVarSymbol, InfVarState] + val cfg: Config ): def +=(p: Symbol -> InfType): Unit = env += p def get(sym: Symbol): Option[InfType] = env.get(sym) `orElse` parent.dlof(_.get(sym))(None) - def getCls(name: Str): TypeSymbol= symbolCache.getOrElseUpdate(name, - ctx.get(name).get.symbol.get.asTpe.get) def nest: InfCtx = copy(parent = Some(this), env = HashMap.empty) def nestWithOuter(outer: InfVar): InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer) def nextLevel: InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty) - def withTail(x:Ls[K]) = copy(parent = S(this), suffix = x) + def withSuffix(x:Ls[K]) = copy(parent = S(this), suffix = x ++ suffix) + def dropSuffix = copy(suffix = Nil) // def freshVar(origin: Symbol | Term, hint: Str = ""): InfVar def sub(x: Type, y: Type): K = K(x,y) + def subArg(x: TypeArg, y: TypeArg): Ls[K] = + K(x.posPart,y.posPart) :: K(y.negPart,x.negPart) :: Nil def subor(x: K, y: K): K = (x,y) match case (K(a, b: Type), y) => K(a, DisjOr(b, Ls(y))) case (K(a, DisjOr(b, cs)), y) => K(a, DisjOr(b, cs ++ Ls(y))) - def constrain(solver: ConstraintSolver, c: K)(using CCtx, TL): Unit= c match - case K(x,y: Type) => solver.constrain(x,y)(using this) + def constrain(c: K)(using CCtx, TL, Raise): Unit = c match + case K(x,y: Type) => ConstraintSolver.constrain(x,y)(using this) case K(x,DisjOr(y, cs)) => - given InfCtx = withTail(cs) - solver.constrain(x,y) + given InfCtx = withSuffix(cs) + ConstraintSolver.constrain(x,y) - def ubs(s: InfVarSymbol): Ls[Type]= varSt(s).upperBounds - def lbs(s: InfVarSymbol): Ls[Type]= varSt(s).lowerBounds - def addub(s: InfVar, ub: Type): Unit= - val v = varSt.getOrElseUpdate(s.sym, new InfVarState) - v.upperBounds = ub :: v.upperBounds - def addlb(lb: Type, s: InfVar): Unit= - val v = varSt.getOrElseUpdate(s.sym, new InfVarState) - v.lowerBounds = lb :: v.lowerBounds + def ubs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).upperBounds + def lbs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds + def addub(s: InfVar, ub: Type)(using CCtx, TL, Raise): Unit = + if prefix.isEmpty && suffix.isEmpty then + val v = varSt.getOrElseUpdate(s.sym, new InfVarState) + v.upperBounds = ub :: v.upperBounds + v.lowerBounds.foreach(lb => constrain(sub(lb, ub))) + else ??? + def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise): Unit = + if prefix.isEmpty && suffix.isEmpty then + val v = varSt.getOrElseUpdate(s.sym, new InfVarState) + v.lowerBounds = lb :: v.lowerBounds + v.upperBounds.foreach(ub => constrain(sub(lb, ub))) + else ??? def disjor(p: Type, a: InfVar, cs: Ls[K]): Unit = ??? -class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx): + def err(msg: Diagnostic)(using CCtx, Raise, TL): Unit = + if suffix.isEmpty then raise(msg) + else + val nctx = dropSuffix + suffix.foreach(k => nctx.constrain(k)) + + def asSubcls(x: ClassLikeType, y: ClsTag): Opt[ClassLikeType] = + if x.sym === y then S(x) + else + x.sym match + case lit: LitSymbol => + lit.lit match + case _: IntLit => + if prim.intSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N + case _: StrLit => + if prim.strSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N + case _: BoolLit => + if prim.boolSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N + case _ => N + case _ => N + +class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config): val objSym = ctx.get("Object").get.symbol.get.asTpe.get val intSym = ctx.get("Int").get.symbol.get.asTpe.get val strSym = ctx.get("Str").get.symbol.get.asTpe.get + val boolSym = ctx.get("Bool").get.symbol.get.asTpe.get val errSym = ctx.get("Error").get.symbol.get.asTpe.get val fnSym = ctx.get("Function").get.symbol.get.asTpe.get + val arrSym = ctx.get("Array").get.symbol.get.asTpe.get def litSym(x: syntax.Literal) = LitSymbol(x) object InfCtx: - def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL): InfCtx = - val prim = new PrimCtx - InfCtx(1, N, HashMap.empty, Bot, Nil, Nil) - (using prim, ctx, HashSet.empty, HashMap.empty, HashMap.empty) - def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, Nil) + def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL, cfg: Config): InfCtx = + given PrimCtx = new PrimCtx + InfCtx(1, N, HashMap.empty, Bot, Nil, Nil)(using HashMap.empty) + def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, N) def litTy(lit: Literal)(using ctx: InfCtx) = mkTag(ctx.prim.litSym(lit)) def objTy(using ctx: InfCtx) = mkTag(ctx.prim.objSym) def funTy(args: Ls[Type], ret: Type, eff: Type)(using ctx: InfCtx) = - val args = Ls(Bot, Wildcard.out(ret), Wildcard.out(eff)) + val u = tupTy(args) + val w = Ls(Wildcard.in(u), Wildcard.out(ret), Wildcard.out(eff)) val i = Ls(true, false, false) - val o = Ls(false, false, false) - ClassLikeType(ctx.prim.fnSym, args, Nil, i, o) + ClassLikeType(ctx.prim.fnSym, w, Nil, i, S(0)) def asRefinedObj(t: Ls[Type])(using ctx: InfCtx) = val r = t.zipWithIndex.map: case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) - ClassLikeType(ctx.prim.objSym, Nil, r, Nil, Nil) + ClassLikeType(ctx.prim.objSym, Nil, r, Nil, N) // def arrayTy(elem: Type)(using ctx: InfCtx) = ClassLikeType(ctx.getCls("Array"), Ls(elem), Nil, Nil) - // def tupTy(e: Ls[Type])(using ctx: InfCtx, s: Elaborator.State) = - // val refine = (Tree.Ident("size"): Tree.Ident, litTy(IntLit(e.length))) :: e.zipWithIndex.map: - // case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) - // ClassLikeType(ctx.getCls("Array"), Ls(e.foldLeft[Type](Bot)(_ | _)), refine, Nil) + def tupTy(e: Ls[Type])(using ctx: InfCtx) = + // val refine = (Tree.Ident("size"): Tree.Ident, litTy(IntLit(e.length))) :: e.zipWithIndex.map: + // case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) + // ClassLikeType(ctx.prim.arrSym, Ls(e.foldLeft[Type](Bot)(_ | _)), refine, Ls(true), N) + val refine = e.zipWithIndex.map: + case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) + ClassLikeType(ctx.prim.arrSym, Nil, refine, Nil, N) def refinedObj(r: Ls[Tree.Ident -> Type])(using ctx: InfCtx) = - ClassLikeType(ctx.prim.objSym, Nil, r, Nil, Nil) \ No newline at end of file + ClassLikeType(ctx.prim.objSym, Nil, r, Nil, N) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala index 9e00a6509d..782c433612 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala @@ -56,7 +56,7 @@ object Wildcard: def out(ty: Type) = Wildcard(Bot, ty) def empty = Wildcard(Bot, Top) -case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: InfType) extends InfType: +case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], xbds: Ls[K], body: InfType) extends InfType: lazy val lvl = (body :: tvs).map(_.lvl).max def show(using Scope, InfCtx, Raise) = showDbg //TODO def showDbg = ??? @@ -69,7 +69,7 @@ case class PolyFunType(args: Ls[InfType], ret: InfType, eff: Type) extends InfTy sealed abstract class Type extends InfType with TypeArg: lazy val lvl = toBasic match - case ClassLikeType(name, targs, refinement, i, o) => + case ClassLikeType(name, targs, refinement, _,_) => val args = targs.iterator val refine = refinement.iterator.map(_._2) (args ++ refine).map(_.lvl).maxOption.getOrElse(0) @@ -78,11 +78,30 @@ sealed abstract class Type extends InfType with TypeArg: case Union(lhs, rhs) => lhs.lvl.max(rhs.lvl) case Inter(lhs, rhs) => lhs.lvl.max(rhs.lvl) case Neg(ty) => ty.lvl - def show(using Scope, InfCtx, Raise) = showDbg //TODO + def show(using Scope, InfCtx, Raise) = toBasic match + case ClassLikeType(f, args, _,_,_) if f === summon[InfCtx].prim.fnSym => + val fargs :: ret :: eff :: Nil = args.runtimeChecked + val ClassLikeType(_,_,r,_,_) = fargs.negPart.runtimeChecked + val a = s"[${r.values.map(_.show).mkString(", ")}]" + if eff === Bot then + s"$a -> ${ret.show}" + else + s"$a ->{${eff.show}} ${ret.show}" + case ClassLikeType(name, targs, refinement, _,_) => + val cls = if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]" + val r = refinement.map { case (l,t) => s"${l.name}: ${t.showDbg}" }.mkString(", ") + cls ++ (if refinement.isEmpty then "" else s" & {$r}") + case v @ InfVar(lvl, sym, isSkolem) => + val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.sym.hint)) + if isSkolem then name else s"'${name}" + case Union(lhs, rhs) => s"${lhs.paren} ∨ ${rhs.paren}" + case Inter(lhs, rhs) => s"${lhs.paren} ∧ ${rhs.paren}" + case Neg(ty) => s"¬${ty.paren}" + case _ => showDbg def showDbg: Str = toBasic match case ClassLikeType(name, targs, refinement, _,_) => val cls = if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]" - val r = refinement.map { case (l,t) => s"$l: ${t.showDbg}" }.mkString(", ") + val r = refinement.map { case (l,t) => s"${l.name}: ${t.showDbg}" }.mkString(", ") cls ++ (if refinement.isEmpty then "" else s" & {$r}") case v @ InfVar(lvl, sym, isSkolem) => val name = if sym.hint.isEmpty then s"${sym.nme}" else s"${sym.nme}(${sym.hint})" @@ -106,9 +125,9 @@ sealed abstract class Type extends InfType with TypeArg: lazy val partialpattern: Bool = simp match case _: InfVar => false case Top | Bot => true - case ClassLikeType(s, args, refine,_,o) => - val p = args.iterator.zip(o).forall: - case (t, true) => t.posPart.partialpattern + case ClassLikeType(s, args, refine,congr,_) => + val p = args.iterator.zip(congr).forall: + case (t, true) => t.negPart === Bot && t.posPart.partialpattern case (t, false) => t is Wildcard.empty p && refine.values.forall(_.partialpattern) case Union(x,y) => x.partialpattern && y.partialpattern @@ -127,6 +146,9 @@ sealed abstract class Type extends InfType with TypeArg: def disjuncts: Ite[Type] = simp match case Union(x,y) => x.disjuncts ++ y.disjuncts case x => Ite(x) + def conjuncts: Ite[Type] = simp match + case Inter(x,y) => x.conjuncts ++ y.conjuncts + case x => Ite(x) var _dnf: Disj = null def toDnf(using TL) = @@ -170,30 +192,32 @@ case class Neg(t: Type) extends BasicType case class ClassLikeType( sym: ClsTag, args: Ls[TypeArg], refinement: Ls[(Tree.Ident, Type)], - in: Ls[Bool], out: Ls[Bool] + congr: Ls[Bool], ov: Opt[Int] ) extends BasicType: private def merge(u: Ls[TypeArg], r: Ls[Tree.Ident -> Type]) = val targs = args.lazyZip(u).map(_ & _) val rmap = mergeMap(refinement, r)(_ & _) - val lbl = (refinement.iterator ++ r.iterator).map(_._1).distinct + val lbl = (refinement.iterator ++ r.iterator).map(_._1).distinct.toList val refine = lbl.zip(lbl.map(rmap)).toList - ClassLikeType(sym, targs, refine, in, out) + ClassLikeType(sym, targs, refine, congr, ov) def merge(cs: Ls[ClassLikeType]): Opt[Ls[ClassLikeType]] = cs match case Nil => S(Ls(this)) + case x :: xs if x.sym === sym && x.ov.isDefined => + S(this :: x :: xs) case x :: _ if x.sym is sym => S(Ls(cs.foldLeft(this)((x, y) => x.merge(y.args, y.refinement)))) - case _ => N + case _ => N type ClsTag = LitSymbol | TypeSymbol | ModuleOrObjectSymbol -object Discriminator extends TypeMapper: +object Discriminator extends TypeMap: override def apply(pol: Bool)(t: Type) = t.simp match case _: InfVar => Top case c @ ClassLikeType(_: LitSymbol, _,_,_,_) => c - case c @ ClassLikeType(s: (TypeSymbol | ModuleOrObjectSymbol), args, refine, i,o) => + case c @ ClassLikeType(s: (TypeSymbol | ModuleOrObjectSymbol), args, refine,congr,ov) => // TODO flags in `s.defn.get.tparams` - val a = args.iterator.zip(o).map: - case (t, true) => apply(pol)(t.posPart) // TODO + val a = args.iterator.zip(congr).map: + case (t, true) => Wildcard.out(apply(pol)(t.posPart)) // TODO case _ => Wildcard.empty - ClassLikeType(s, a.toList, refine.mapValues(apply(pol)), i,o) + ClassLikeType(s, a.toList, refine.mapValues(apply(pol)), congr,ov) case t @ Neg(ClassLikeType(_, _, refine, _,_)) => if refine.isEmpty then t else Top case t => super.apply(pol)(t) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala index 75f11863bb..8b06dc8c6a 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala @@ -21,21 +21,25 @@ import hkmc2.codegen.ErasedType.eraseSign class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): import tl.{trace, log} private val builtinOps = Elaborator.binaryOps ++ Elaborator.unaryOps ++ Elaborator.aliasOps.keySet - private val solver = new ConstraintSolver(elState, tl) private def error(msg: Ls[Message -> Opt[Loc]], extraInfo: => Opt[Any] = N)(using InfCtx) = raise(ErrorReport(msg, extraInfo = extraInfo)) Bot // TODO: error type? - private def typeNames(using ctx: InfCtx) = ctx.typeNames private def freshVar(origin: Symbol | Term, hint: Str = "")(using ctx: InfCtx) = // ctx.freshVar(origin, hint) InfVar(ctx.lvl, InfVarSymbol(origin, hint), false) private def freshWildcard(s: Symbol)(using InfCtx) = Wildcard(freshVar(s),freshVar(s)) - private def freshOuter(sym: Symbol)(using ctx: InfCtx): InfVar = // ctx.freshOuter(sym) - InfVar(ctx.lvl + 1, new InfVarSymbol(sym), true) + InfVar(ctx.lvl + 1, InfVarSymbol(sym), true) + private def freshEnv(sym: Symbol)(using ctx: InfCtx): InfVar = + val s = InfVarSymbol(sym) + val state = new InfVarState + ctx.varSt += s -> state + state.upperBounds = ctx.outRegAcc :: Nil + state.lowerBounds = ctx.outRegAcc :: Nil + InfVar(ctx.lvl, s, false) private def mono(ty: InfType)(using ctx: InfCtx): Opt[Type] = ty match case x: Type => S(x) @@ -49,7 +53,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): private def monoOrErr(ty: InfType, sc: Located)(using InfCtx): Type = mono(ty).getOrElse(error(msg"General type is not allowed here." -> sc.toLoc :: Nil)) - private def tryMkMono(ty: InfType, sc: Located)(using InfCtx, Scope): Type = ty match + private def tryMkMono(ty: InfType, sc: Located)(using InfCtx, CCtx, Scope): Type = ty match case pt: PolyType => tryMkMono(instantiate(pt), sc) case ft: PolyFunType => mono(ft).getOrElse: @@ -93,7 +97,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case S(true) => Wildcard.out(ta) case N => ta val fs = ts.map(_ => false) // TODO - ClassLikeType(tpeSym, ts, Nil, fs, fs) + ClassLikeType(tpeSym, ts, Nil, fs, N) case N => error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil) case FunTy(Term.Tup(params), ret, eff) => val p = params.map { @@ -116,6 +120,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case CompType(lhs, rhs, pol) => if pol then mono(lhs, pol) | mono(rhs, pol) else mono(lhs, pol) & mono(rhs, pol) case UnitVal() => InfCtx.objTy + case Lit(x) => InfCtx.litTy(x) case _ => ty.symbol.flatMap(_.asTpe) match case S(cls: (ClassSymbol | TypeAliasSymbol)) => typeAndSubstType(Term.TyApp(ty, Nil)(N), pol) case _ => error(msg"Invalid type" -> ty.toLoc :: Nil, S(ty)) // TODO @@ -134,7 +139,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): val lbty = ctx.lbs(tv.sym).foldLeft[Type](Bot)(_ | _) val ubty = ctx.ubs(tv.sym).foldLeft[Type](Top)(_ & _) constrain(lbty, ubty) - PolyType(bds.map(_._1), S(outer), body) + PolyType(bds.map(_._1), S(outer), Nil, body) private def typeType(ty: Term)(using ctx: InfCtx, cctx: CCtx): InfType = typeAndSubstType(ty, true)(using Map.empty) @@ -147,7 +152,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ty private def constrain(x: Type, y: Type)(using ctx: InfCtx, cctx: CCtx): Unit = - ctx.constrain(solver, ctx.sub(x,y)) + ctx.constrain(ctx.sub(x,y)) private def fundef(sym: Symbol, lam: Term, sig: Opt[Term]) (using ctx: InfCtx, cctx: CCtx, scope: Scope) = lam match @@ -164,14 +169,73 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ctx += sym -> funTyV // for recursive functions val (res, _) = typeCheck(lam) val funTy = tryMkMono(res, lam) - given CCtx = CCtx.init(lam, N) - constrain(funTy, funTyV) - ctx += sym -> generalize(funTy, S(outer), ctx.lvl + 1) + { + given CCtx = CCtx.init(lam, N) + constrain(funTy, funTyV) + ctx += sym -> generalize(funTy, S(outer), ctx.lvl + 1) + } case _ => error(msg"Function definition shape not yet supported for ${sym.nme}" -> lam.toLoc :: Nil) - def instantiate(x: InfType): Type = ??? - def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int): PolyType = ??? + + private class Subst(map: Map[InfVarSymbol, InfVar]) extends TypeMap: + override def apply(pol: Bool)(t: Type) = t.toBasic match + case v @ InfVar(_, s, _) => map.get(s).getOrElse(v) + case t => super.apply(pol)(t) + + private def substMono(map: Map[InfVarSymbol, InfVar])(x: Type): Type = + Subst(map)(true)(x) + + private def substMono(map: Map[InfVarSymbol, InfVar])(x: K): K = x match + case K(x, y: Type) => K(substMono(map)(x), substMono(map)(y)) + case K(x, DisjOr(p, cs)) => K(substMono(map)(x), DisjOr(substMono(map)(p), cs.map(substMono(map)))) + + private def subst(map: Map[InfVarSymbol, InfVar])(x: InfType): InfType = + x match + case _: PolyType => ??? + case PolyFunType(args, ret, eff) => + PolyFunType(args.map(subst(map)), subst(map)(ret), substMono(map)(eff)) + case x: Type => substMono(map)(x) + + private def instantiate(x: PolyType)(using ctx: InfCtx, cctx: CCtx) = + val PolyType(tvs, outer, xbds, body) = x + val env = freshEnv(new TempSymbol(N, erasedType = N, "env")) + val map = (outer.map(_.sym -> env).toList ++ tvs.map(v => + val nv = InfVar(ctx.lvl, InfVarSymbol(InstSymbol(v.sym), v.sym.hint), false) + tl.log(s"instantiate ${v.showDbg} ~> ${nv.showDbg}") + v.sym -> nv + )).toMap + tvs.foreach: v => + ctx.varSt.get(v.sym).foreach: st => + val ns = new InfVarState + ctx.varSt += map(v.sym).sym -> ns + ns.upperBounds = st.upperBounds.map(substMono(map)) + ns.lowerBounds = st.lowerBounds.map(substMono(map)) + ns.disjsub = st.disjsub.map(d => DisjOr(substMono(map)(d.p), d.cs.map(substMono(map)))) + // TODO bound scheme + xbds.foreach(k => ctx.constrain(substMono(map)(k))) + subst(map)(body) + + private def skolemize(x: PolyType)(using ctx: InfCtx, cctx: CCtx) = + val PolyType(tvs, outer, xbds, body) = x + // * Note that by this point, the state is supposed to be frozen/treated as immutable + // * `outer` is already skolemized when it is declared + val map = tvs.map(v => + val sk = InfVar(ctx.lvl, InfVarSymbol(InstSymbol(v.sym), v.sym.hint), true) + tl.log(s"skolemize ${v.showDbg} ~> ${sk.showDbg}") + v.sym -> sk + ).toMap + tvs.foreach: v => + ctx.varSt.get(v.sym).foreach: st => + val ns = new InfVarState + ctx.varSt += map(v.sym).sym -> ns + ns.upperBounds = st.upperBounds.map(substMono(map)) + ns.lowerBounds = st.lowerBounds.map(substMono(map)) + ns.disjsub = st.disjsub.map(d => DisjOr(substMono(map)(d.p), d.cs.map(substMono(map)))) + // xbds.foreach(k => ctx.constrain(substMono(map)(k))) + subst(map)(body) + + private def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int): PolyType = ??? private def app(lhs: InfType, lhsEff: Type, rhs: Ls[Elem], t: Term) (using ctx: InfCtx, cctx: CCtx, scope: Scope) @@ -189,7 +253,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case (spd: Spd, _) => TODO(s"spread arguments: $spd") (ret, resEff) case ClassLikeType(s, (params: ClassLikeType) :: ret :: eff :: Nil, _,_,_) - if s === ctx.prim.fnSym && params.sym === ctx.prim.objSym => + if s === ctx.prim.fnSym => // && params.sym === ctx.prim.objSym => app(PolyFunType(params.refinement.values.toList, ret.posPart, eff.posPart), lhsEff, rhs, t) case ty: PolyType => app(instantiate(ty), lhsEff, rhs, t) case funTy => @@ -218,7 +282,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ty } val fs = targs.map(_ => false) // TODO - constrain(tryMkMono(ty, t), ClassLikeType(clsSym, targs, Nil, fs, fs)) + constrain(tryMkMono(ty, t), ClassLikeType(clsSym, targs, Nil, fs, N)) require(clsDfn.paramsOpt.forall(_.restParam.isEmpty)) (clsDfn.paramsOpt.fold(Nil)(_.params).map { case Param(_, sym, sign, _) => @@ -263,7 +327,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case _ => ??? } val fs = targs.map(_ => false) // TOOD - (ClassLikeType(clsDfn.sym, targs, Nil, fs, fs), effBuff.foldLeft[Type](Bot)((res, e) => res | e)) + (ClassLikeType(clsDfn.sym, targs, Nil, fs, N), effBuff.foldLeft[Type](Bot)((res, e) => res | e)) case S(clsDfn: ClassDef.Plain) => ??? // TODO case N => (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot) @@ -288,19 +352,26 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case (Term.Lam(params, body), ft @ ClassLikeType(fn, (args: ClassLikeType)::ret::eff::Nil, _,_,_)) if fn === ctx.prim.fnSym => ascribe(lhs, PolyFunType(args.refinement.values.toList, ret.posPart, eff.posPart)) - case (term, pt @ PolyType(_, outer, _)) => // * generalize + case (term, pt @ PolyType(_, outer, _, _)) => // * generalize val nextCtx = outer match case S(outer) => ctx.nestWithOuter(outer) case N => ctx.nextLevel - // given InfCtx = nextCtx - // constrain(ascribe(term, skolemize(pt))._2, Bot) // * never generalize terms with effects - // (pt, Bot) - ??? + given InfCtx = nextCtx + constrain(ascribe(term, skolemize(pt))._2, Bot) // * never generalize terms with effects + (pt, Bot) // case (Term.IfLike(_, IfLikeForm.ReturningIf, split), ty) => // * propagate // typeAllSplits(split.getExpandedSplit, S(ty)) case (Term.Asc(term, ty), rhs) => ascribe(term, typeType(ty)) ascribe(term, rhs) + case (lhs, rhs: Type) => rhs.conjuncts.toList match + case rhs :: Nil => + val (lhsTy, eff) = typeCheck(lhs) + constrain(tryMkMono(lhsTy, lhs), monoOrErr(rhs, lhs)) + (rhs, eff) + case cs => + val e = cs.map(c => ascribe(lhs, c)._2).reduce(_|_) + (rhs, e) case _ => val (lhsTy, eff) = typeCheck(lhs) rhs match @@ -377,18 +448,19 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ctx += td.sym -> typeType(sig) goStats(stats) case (clsDef: ClassDef) :: stats => - typeNames.add(clsDef.sym.nme) + // typeNames.add(clsDef.sym.nme) // clsDef.ext match // case S(Term.New(ty, _, N)) => createADTCtor(clsDef, ty) // case _ => () goStats(stats) case (modDef: ModuleOrObjectDef) :: stats => - typeNames.add(modDef.sym.nme) + // typeNames.add(modDef.sym.nme) goStats(stats) case Import(sym, str, pth) :: stats => goStats(stats) // TODO: + case (_: SetConfig) :: _ => case stat :: _ => - // TODO(stat) // TODO + TODO(stat) goStats(stats) val (ty, eff) = typeCheck(res) (ty, effBuff.foldLeft(eff)((res, e) => res | e)) diff --git a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls index 9b1c740083..89e8cd5faf 100644 --- a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls +++ b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls @@ -217,9 +217,9 @@ applyTwice(fst, Pair(1, 2)) allowUnresolvedAccesses: true, useNewResolution: false, typeCheck: Some(TypeChecking())) +//│ Type: undefined #config(language: Language( allowUnresolvedAccesses: false, useNewResolution: true, typeCheck: None)) -//│ Type: undefined diff --git a/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls b/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls index 580a66f480..99df8ea09e 100644 --- a/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls +++ b/hkmc2/shared/src/test/mlscript/ucs/staging/legacy/ElseIf.mls @@ -1,5 +1,4 @@ :NewDefs -//│ /!\ Unrecognized command: NewDefs @@ -10,11 +9,7 @@ fun f(x, y) = if x === 0 then true 1 then false else false -//│ FAILURE: Unexpected parse error -//│ FAILURE LOCATION: concludeWithImpl (Parser.scala:270) -//│ ╔══[PARSE ERROR] Unexpected 'else' keyword here -//│ ║ l.12: else false -//│ ╙── ^^^^ +//│ fun f: (Eql[0 | 1], Eql[0 | 1]) -> Bool fun f(x, y) = if x === 0 then true @@ -22,26 +17,36 @@ fun f(x, y) = if x === else if y === 0 then true _ then false +//│ fun f: (Eql[0 | 1], Eql[0]) -> Bool module Tru module Fals +//│ module Tru +//│ module Fals :e fun f(x, y) = if x is Tru and y is Tru then true Fals and y is Fals then false -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.31: Tru and y is Tru then true -//│ ╙── ^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.31: Tru and y is Tru then true -//│ ╙── ^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.32: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.32: Fals and y is Fals then false +//│ ╔══[ERROR] when `x` is `Tru` +//│ ║ l.29: Tru and y is Tru then true +//│ ║ ^^^ +//│ ╟── `y` has 1 missing case +//│ ║ l.29: Tru and y is Tru then true +//│ ║ ^ +//│ ╟── it can be module `Fals` +//│ ║ l.30: Fals and y is Fals then false //│ ╙── ^^^^ +//│ ╔══[ERROR] when `x` is `Fals` +//│ ║ l.30: Fals and y is Fals then false +//│ ║ ^^^^ +//│ ╟── `y` has 1 missing case +//│ ║ l.30: Fals and y is Fals then false +//│ ║ ^ +//│ ╟── it can be module `Tru` +//│ ║ l.29: Tru and y is Tru then true +//│ ╙── ^^^ +//│ fun f: (Fals | Tru, nothing) -> Bool // The base case. fun f(x, y) = if x is @@ -49,46 +54,7 @@ fun f(x, y) = if x is Fals and y is Fals then false Tru and y is Fals then true Fals and y is Tru then true -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.48: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.48: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.49: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.49: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.50: Tru and y is Fals then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.50: Tru and y is Fals then true -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.51: Fals and y is Tru then true -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.51: Fals and y is Tru then true -//│ ╙── ^^^ +//│ fun f: (Fals | Tru, Fals | Tru) -> Bool // Replace the `x is Fals` with `_` fun f(x, y) = if x is @@ -97,95 +63,39 @@ fun f(x, y) = if x is _ and y is Tru then true Fals then false -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.95: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.95: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.96: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.96: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.98: Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.99: Fals then false -//│ ╙── ^^^^ +//│ fun f: (Object, Fals | Tru) -> Bool f(Tru, Tru) f(Tru, Fals) f(Fals, Tru) f(Fals, Fals) -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. -//│ ║ l.131: f(Tru, Tru) -//│ ║ ^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. -//│ ║ l.131: f(Tru, Tru) -//│ ║ ^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. -//│ ║ l.132: f(Tru, Fals) -//│ ║ ^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. -//│ ║ l.132: f(Tru, Fals) -//│ ║ ^^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. -//│ ║ l.133: f(Fals, Tru) -//│ ║ ^^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Tru. -//│ ║ l.133: f(Fals, Tru) -//│ ║ ^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. -//│ ║ l.134: f(Fals, Fals) -//│ ║ ^^^^ -//│ ╙── Module argument passed to a non-module parameter. -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: traverse (Resolver.scala:350) -//│ ╔══[COMPILATION ERROR] Unexpected moduleful reference of type Fals. -//│ ║ l.134: f(Fals, Fals) -//│ ║ ^^^^ -//│ ╙── Module argument passed to a non-module parameter. +//│ Bool +//│ res +//│ = true +//│ res +//│ = false +//│ res +//│ = true +//│ res +//│ = false :e fun g(x, y) = if x is true and y is true then true false and y is false then false -//│ FAILURE: Unexpected lack of compilation or type error +//│ ╔══[ERROR] `y` has 1 missing case +//│ ║ l.84: true and y is true then true +//│ ║ ^ +//│ ╟── it can be Boolean value `false` +//│ ║ l.85: false and y is false then false +//│ ╙── ^^^^^ +//│ ╔══[ERROR] `y` has 1 missing case +//│ ║ l.85: false and y is false then false +//│ ║ ^ +//│ ╟── it can be Boolean value `true` +//│ ║ l.84: true and y is true then true +//│ ╙── ^^^^ +//│ fun g: (Bool, nothing) -> Bool // Test with real booleans fun g(x, y) = if x is @@ -194,6 +104,7 @@ fun g(x, y) = if x is _ and y is true then true false then false +//│ fun g: (Object, Bool) -> Bool // Chained UCS terms fun f(x, y) = if x is @@ -202,36 +113,7 @@ fun f(x, y) = if x is else if y is Tru then true Fals then false -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.200: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.200: Tru and y is Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.201: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.201: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.203: Tru then true -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.204: Fals then false -//│ ╙── ^^^^ +//│ fun f: (Object, Fals | Tru) -> Bool :e fun f(x, y) = if x is @@ -240,43 +122,53 @@ fun f(x, y) = if x is else if y is Tru and x is Fals then true Fals and x is Tru then false -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.238: Tru and y is Tru then true -//│ ╙── ^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.238: Tru and y is Tru then true -//│ ╙── ^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.239: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.239: Fals and y is Fals then false -//│ ╙── ^^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.241: Tru and x is Fals then true -//│ ╙── ^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.241: Tru and x is Fals then true +//│ ╔══[ERROR] when `y` is `Tru` +//│ ║ l.123: Tru and x is Fals then true +//│ ║ ^^^ +//│ ╟── `x` has 1 missing case +//│ ║ l.123: Tru and x is Fals then true +//│ ║ ^ +//│ ╟── it can be module `Tru` +//│ ║ l.124: Fals and x is Tru then false +//│ ╙── ^^^ +//│ ╔══[ERROR] when `y` is `Fals` +//│ ║ l.124: Fals and x is Tru then false +//│ ║ ^^^^ +//│ ╟── `x` has 1 missing case +//│ ║ l.124: Fals and x is Tru then false +//│ ║ ^ +//│ ╟── it can be module `Fals` +//│ ║ l.123: Tru and x is Fals then true +//│ ╙── ^^^^ +//│ ╔══[ERROR] Type mismatch in `case` expression: +//│ ║ l.123: Tru and x is Fals then true +//│ ║ ^^^^^^^^^^^^^^^^^^^ +//│ ╟── class pattern of type `Tru` is not an instance of type `Fals` +//│ ║ l.120: Tru and y is Tru then true +//│ ║ ^^^ +//│ ╟── but it flows into reference with expected type `Fals` +//│ ║ l.123: Tru and x is Fals then true +//│ ║ ^ +//│ ╟── Note: constraint arises from class pattern: +//│ ║ l.123: Tru and x is Fals then true //│ ╙── ^^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.242: Fals and x is Tru then false -//│ ╙── ^^^^ -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.242: Fals and x is Tru then false +//│ ╔══[ERROR] Type mismatch in `case` expression: +//│ ║ l.124: Fals and x is Tru then false +//│ ║ ^^^^^^^^^^^^^^^^^^^ +//│ ╟── class pattern of type `Fals` is not an instance of type `Tru` +//│ ║ l.121: Fals and y is Fals then false +//│ ║ ^^^^ +//│ ╟── but it flows into reference with expected type `Tru` +//│ ║ l.124: Fals and x is Tru then false +//│ ║ ^ +//│ ╟── Note: constraint arises from class pattern: +//│ ║ l.124: Fals and x is Tru then false //│ ╙── ^^^ +//│ fun f: (Fals | Tru, Fals | Tru) -> Bool fun h(x, y, p) = if x and p(x) then 0 y is Tru then 1 Fals then 2 -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Tru. -//│ ║ l.271: Tru then 1 -//│ ╙── ^^^ -//│ FAILURE: Unexpected compilation error -//│ FAILURE LOCATION: go (Elaborator.scala:2756) -//│ ╔══[COMPILATION ERROR] Pattern name not found: Fals. -//│ ║ l.272: Fals then 2 -//│ ╙── ^^^^ +//│ fun h: forall 'a. ('a & Bool, Fals | Tru, 'a -> Bool) -> (0 | 1 | 2) diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala index 89f4c05ade..f62aecfdc6 100644 --- a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala +++ b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala @@ -5,29 +5,30 @@ import hkmc2.utils.*, shorthands.* import hkmc2.semantics.* import hkmc2.typing.* import utils.Scope -import hkmc2.syntax.Keyword.undefined abstract class LogicSubDiffMaker extends WasmDiffMaker: lazy val infctx = given Elaborator.Ctx = curCtx + given Config = mkConfig logicsub.InfCtx.init var typer: Opt[logicsub.Typer] = None override def processTerm(trm: semantics.Term.Blk, inImport: Bool)(using Config, Raise): Unit = super.processTerm(trm, inImport) - if summon[Config].language.typeCheck.isDefined then - given Scope = Scope.empty(Scope.Cfg.default) - if typer.isEmpty then - given Elaborator.Ctx = curCtx - typer = S(logicsub.Typer()) - given logicsub.InfCtx = infctx - val ty = typer.get.typePurely(trm) - output(s"Type: ${ty.show}") - ty match - case x: logicsub.InfVar => - output(s" >: ${infctx.lbs(x.sym).foldLeft(logicsub.Bot:logicsub.Type)(_|_).toBasic.show}") - case _ => + Config.extractConfigFromStats(trm).givenIn: + if summon[Config].language.typeCheck.isDefined then + given Scope = Scope.empty(Scope.Cfg.default) + if typer.isEmpty then + given Elaborator.Ctx = curCtx + typer = S(logicsub.Typer()) + given logicsub.InfCtx = infctx + val ty = typer.get.typePurely(trm) + output(s"Type: ${ty.show}") + ty match + case x: logicsub.InfVar => + output(s" >: ${infctx.lbs(x.sym).foldLeft(logicsub.Bot:logicsub.Type)(_|_).toBasic.show}") + case _ => From e52d7db86b8dd89d6274f7831d74532cc8f75e64 Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Tue, 20 Oct 2026 13:25:59 +0800 Subject: [PATCH 3/6] minor --- hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala index 8b06dc8c6a..c980af617d 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala @@ -470,4 +470,4 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ascribe(term, res) case Term.Annotated(Annot.Untyped, _) => (Bot, Bot) case _ => - (error(msg"Term shape not yet supported by InvalML: ${t.toString}" -> t.toLoc :: Nil), Bot) + (error(msg"Term shape not yet supported: ${t.toString}" -> t.toLoc :: Nil), Bot) From 1aba78a012468a6412026b7c9f4052d5a0591e70 Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Tue, 20 Oct 2026 13:50:06 +0800 Subject: [PATCH 4/6] add test --- .../src/test/mlscript/logicsub/test.mls | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 hkmc2/shared/src/test/mlscript/logicsub/test.mls diff --git a/hkmc2/shared/src/test/mlscript/logicsub/test.mls b/hkmc2/shared/src/test/mlscript/logicsub/test.mls new file mode 100644 index 0000000000..45ece01d1a --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/test.mls @@ -0,0 +1,29 @@ +#config(language: Language(typeCheck: TypeChecking())) +//│ Type: undefined + +fun f: (1 -> 1) & (("a"|"B") -> ("a"|"B"|"c")) +fun f(x) = x +//│ Type: undefined + +f(1) +//│ Type: 'app +//│ >: 1 + +f("a") +//│ Type: 'app +//│ >: ("c" ∨ "B") ∨ "a" + +fun g: (Int -> Int) & (Str -> Str) +//│ Type: undefined + +// TODO +g(1) +//│ Type: 'app +//│ >: ⊥ + +fun g: (1 -> 1) & (2 -> 2) +//│ Type: undefined + +g(1) +//│ Type: 'app +//│ >: 1 From e28a02ac667ff3cd34f615a78787d46ae1a9ab0b Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Thu, 22 Oct 2026 05:02:34 +0800 Subject: [PATCH 5/6] minor refactor --- .../scala/hkmc2/typing/ConstraintSolver.scala | 71 ++++---- .../src/main/scala/hkmc2/typing/infctx.scala | 165 ++++++++++-------- .../main/scala/hkmc2/typing/logicsub.scala | 26 ++- 3 files changed, 139 insertions(+), 123 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala index 140cf537de..a6b1578a0b 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala @@ -14,16 +14,9 @@ type Cache = mutable.HashSet[(Type, Type)] type ExtrudeCache = mutable.HashMap[(InfVarSymbol, Bool), InfVar] case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])(using Scope): - def err(using raise: Raise, ctx: InfCtx, tl: TL) = - ctx.err(ErrorReport( - msg"Type error in ${origin.describe}${exp match - case S(ty) => msg" with expected type ${ty.show}" - case N => msg"" - }" -> origin.toLoc - :: parents.reverse.map(p => - msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N - ) - ))(using this) + def err(using ctx: KCtx)(using TL, Raise) = + given CCtx = this + ctx.err(parents, origin, exp) def nest(sub: (Type, Type)): CCtx = copy(cache = cache += sub, parents = parents match case `sub` :: _ => parents @@ -36,13 +29,18 @@ object CCtx: object ConstraintSolver: private def log(msg: => Any, noIndent: Bool = false)(using tl: TL) = tl.log(msg, noIndent) - private def constrainConj(conj: Conj)(using ctx: InfCtx, cctx:CCtx, tl: TL, raise: Raise): Unit = + private def constrainConj(conj: Conj)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit = tl.trace(s"Constraining ${conj.showDbg}"): conj match + case Conj(i, u, S(v), S(w), xs, ys) if w.lvl > v.lvl => + val rest = Conj(i, u, S(v), N, xs, ys) + val nc = rest.toDnf // always cache the normal form to avoid unexpected cache misses + log(s"New bound: ${v.showDbg} >: ${nc.showDbg}") + cctx.nest(nc -> w.toDnf) givenIn: + ctx.addlb(nc, w) case Conj(i, u, S(v), w, xs, ys) => val rest = Conj(i, u, N, w, xs, ys) - val bd = if v.lvl >= rest.lvl then rest else ??? // extrude(rest)(using v.lvl, true, mutable.HashMap.empty) - val nc = (~bd).toDnf // always cache the normal form to avoid unexpected cache misses + val nc = (~rest).toDnf // always cache the normal form to avoid unexpected cache misses log(s"New bound: ${v.showDbg} <: ${nc.showDbg}") cctx.nest(v.toDnf -> nc) givenIn: ctx.addub(v, nc) @@ -57,7 +55,7 @@ object ConstraintSolver: case (t, true) => t.posPart val d = (x.refinement.values ++ da).toList if d.isEmpty then cctx.err - else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.subor(k, ctx.sub(t, Bot)))) + else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.or(k, ctx.sub(t, Bot)))) case Conj(NF.Inter(x :: Nil), NF.Union(y :: Nil), N,N,_,_) => val da = x.args.iterator.zip(x.congr).collect: case (t, true) => t.posPart @@ -67,7 +65,7 @@ object ConstraintSolver: val sp = ctx.asSubcls(x,y.sym) if sp.isEmpty || !yrm.keySet.subsetOf(xrm.keySet) then if d.isEmpty then cctx.err - else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.subor)) + else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.or)) else val x = sp.get val u = x.args.zip(y.args).flatMap(ctx.subArg) @@ -76,7 +74,7 @@ object ConstraintSolver: val ds = x.refinement.filterNot(f => yrm.contains(f._1)).map: case (_,t) => ctx.sub(t,Bot) (u++w).foreach: k => - ctx.constrain((ds ++ Ls(k)).reduce(ctx.subor)) + ctx.constrain((ds ++ Ls(k)).reduce(ctx.or)) case Conj(NF.Inter(xs @ (x :: _)), NF.Union(y :: Nil), N,N,_,_) => if x.sym === y.sym then val k = x.ov.get @@ -88,7 +86,7 @@ object ConstraintSolver: val d = ctx.sub(in.negPart, ~p) val r = y.copy(args = y.args.updated(k, Wildcard(p & in.negPart, in.posPart))) val s = ctx.sub(c, r) - ctx.constrain(ctx.subor(d, s)) + ctx.constrain(ctx.or(d, s)) else cctx.err case Conj(k @ NF.Inter(x :: _), NF.Union(ys @ (_ :: _)), N,N,ws,zs) => def h(y: ClassLikeType) = @@ -106,32 +104,31 @@ object ConstraintSolver: f(Nil, y.args, y.args.map(_ => Wildcard.empty), y.congr) ++ g(y.refinement) val (ps,t) = ys.partition(_.partialpattern) val xrs = x.refinement.keys.toSet - val qs = ps.filter(p => ctx.asSubcls(x,p.sym).isDefined && p.refinement.keys.forall(xrs.contains)) + val qs = ps.filter: p => + ctx.asSubcls(x,p.sym).isDefined && p.refinement.keys.forall(xrs.contains) val ks = qs.foldLeft(Ls(k)): (ks, y) => ks.flatMap(k => h(y).map(c => k.merge(NF.Inter(Ls(c))).get)) ks.foreach(k => constrainConj(Conj(k, NF.Union(t),N,N,ws,zs))) case _ => - raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} ∧ ¬⊥" -> N :: Nil)) + raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ⊥" -> N :: Nil)) cctx.err - private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = - ctx.constrain(ctx.sub(rhs.negPart, lhs.negPart)) - ctx.constrain(ctx.sub(lhs.posPart, rhs.posPart)) + // private class SkolemBoundsInliner(using ctx: KCtx) extends TypeMap: + // val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty + // override def apply(pol: Bool)(t: Type) = t.toBasic match + // case v @ InfVar(_, s, true) if !cache(s) => + // cache += s + // apply(pol)(if pol + // then ctx.ubs(s).foldLeft[Type](v)(_ & _) + // else ctx.lbs(s).foldLeft[Type](v)(_ | _)) + // case _: ClassLikeType | _: InfVar => t + // case t => super.apply(pol)(t) + private def inlineSkolemBounds(ty: Type)(using KCtx): Type = ty // TODO + // (new SkolemBoundsInliner)(true)(ty) - private class SkolemBoundsInliner(using ctx: InfCtx) extends TypeMap: - val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty - override def apply(pol: Bool)(t: Type) = t.toBasic match - case v @ InfVar(_, s, true) if !cache(s) => - cache += s - apply(pol)(if pol - then ctx.ubs(s).foldLeft[Type](v)(_ & _) - else ctx.lbs(s).foldLeft[Type](v)(_ | _)) - case _: ClassLikeType | _: InfVar => t - case t => super.apply(pol)(t) - private def inlineSkolemBounds(ty: Type)(using InfCtx): Type = - (new SkolemBoundsInliner)(true)(ty) - - private def constrainImpl(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = + def constrainImpl(lhs: Type, rhs: Type) + (using ctx: KCtx, cctx:CCtx)(using TL, Raise) + : Unit = val p = lhs.toDnf -> rhs.toDnf if cctx.cache(p) then log(s"Cached!") else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"): @@ -139,7 +136,7 @@ object ConstraintSolver: val disj = inlineSkolemBounds(lhs & ~rhs).toDnf disj.cs.foreach(constrainConj(_)) - def constrain(lhs: Type, rhs: Type)(using ctx: InfCtx, cctx: CCtx, tl: TL, raise: Raise): Unit = + def constrain(lhs: Type, rhs: Type)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit = val (ps, ts) = rhs.disjuncts.toList.partition(_.partialpattern) if ts.length > 1 then val p = lhs.toDnf -> rhs diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala index 8670923227..512e579149 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala @@ -14,88 +14,91 @@ import Elaborator.Ctx import syntax.* import Tree.* import utils.Scope -import hkmc2.codegen.ErasedType.eraseSign -final case class DisjOr(p: Type, cs: Ls[K]) -final case class K(x: Type, y: Type | DisjOr) +final case class K(x: Type, y: Type, cs: Opt[Ls[K]]): + def lvl: Int = x.lvl max y.lvl max cs.fold(0)(_.map(_.lvl).max) class InfVarState: var lowerBounds: Ls[Type] = Nil - var upperBounds: Ls[Type] = Nil - var disjsub: Ls[DisjOr] = Nil + var upperBounds: Ls[Type -> Opt[Ls[K]]] = Nil + +trait KCtx(using val prim: PrimCtx): + def sub(x: Type, y: Type): K = K(x,y,N) + def subArg(x: TypeArg, y: TypeArg): Ls[K] = + sub(x.posPart,y.posPart) :: sub(y.negPart,x.negPart) :: Nil + def or(x: K, y: K): K = (x,y) match + case (K(a, b, N), y) => K(a, b, S(Ls(y))) + case (K(a, b, S(cs)), y) => K(a, b, S(cs.map(or(_,y)))) + def constrain(c: K)(using CCtx, TL, Raise): Unit = c match + case K(x,y,N) => ConstraintSolver.constrain(x,y)(using this) + case K(x,y,S(Nil)) => + case K(x,y,S(cs)) => ConstraintSolver.constrain(x,y)(using SuffixCtx(cs, this)) + def asSubcls(x: ClassLikeType, y: ClsTag) = + if x.sym === y then S(x) + else x.sym match + case LitSymbol(_: IntLit) if prim.intSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N)) + case LitSymbol(_: StrLit) if prim.strSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N)) + case LitSymbol(_: BoolLit) if prim.boolSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N)) + case _ => N + + def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise): Unit + def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise): Unit + def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) + (using CCtx, TL, Raise, Scope): Unit final case class InfCtx( - val lvl: Int, - val parent: Option[InfCtx], - val env: HashMap[Symbol, InfType], - val outRegAcc: Type, - val prefix: Ls[Ls[Type->Type]], - val suffix: Ls[K], // TODO mutable + lvl: Int, + parent: Option[InfCtx], + env: HashMap[Symbol, InfType], + outRegAcc: Type, + prefix: Opt[Ls[K]] = N )(using val varSt: HashMap[InfVarSymbol, InfVarState], - val prim: PrimCtx, + val xbds: ListBuffer[K], + prim: PrimCtx, val ctx: Ctx, val cfg: Config -): - def +=(p: Symbol -> InfType): Unit = env += p +) extends KCtx: + def +=(p: Symbol -> InfType) = env += p def get(sym: Symbol): Option[InfType] = env.get(sym) `orElse` parent.dlof(_.get(sym))(None) def nest: InfCtx = copy(parent = Some(this), env = HashMap.empty) - def nestWithOuter(outer: InfVar): InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer) + def nestWithOuter(outer: InfVar): InfCtx = copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer) def nextLevel: InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty) - def withSuffix(x:Ls[K]) = copy(parent = S(this), suffix = x ++ suffix) - def dropSuffix = copy(suffix = Nil) - // def freshVar(origin: Symbol | Term, hint: Str = ""): InfVar - - def sub(x: Type, y: Type): K = K(x,y) - def subArg(x: TypeArg, y: TypeArg): Ls[K] = - K(x.posPart,y.posPart) :: K(y.negPart,x.negPart) :: Nil - def subor(x: K, y: K): K = (x,y) match - case (K(a, b: Type), y) => K(a, DisjOr(b, Ls(y))) - case (K(a, DisjOr(b, cs)), y) => K(a, DisjOr(b, cs ++ Ls(y))) - - def constrain(c: K)(using CCtx, TL, Raise): Unit = c match - case K(x,y: Type) => ConstraintSolver.constrain(x,y)(using this) - case K(x,DisjOr(y, cs)) => - given InfCtx = withSuffix(cs) - ConstraintSolver.constrain(x,y) - - def ubs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).upperBounds - def lbs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds - def addub(s: InfVar, ub: Type)(using CCtx, TL, Raise): Unit = - if prefix.isEmpty && suffix.isEmpty then + def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = + val k = K(s, ub, cs) + if s.lvl < k.lvl then xbds += k + else val v = varSt.getOrElseUpdate(s.sym, new InfVarState) - v.upperBounds = ub :: v.upperBounds + v.upperBounds = ub -> cs :: v.upperBounds v.lowerBounds.foreach(lb => constrain(sub(lb, ub))) - else ??? - def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise): Unit = - if prefix.isEmpty && suffix.isEmpty then - val v = varSt.getOrElseUpdate(s.sym, new InfVarState) - v.lowerBounds = lb :: v.lowerBounds - v.upperBounds.foreach(ub => constrain(sub(lb, ub))) - else ??? - def disjor(p: Type, a: InfVar, cs: Ls[K]): Unit = ??? - - def err(msg: Diagnostic)(using CCtx, Raise, TL): Unit = - if suffix.isEmpty then raise(msg) - else - val nctx = dropSuffix - suffix.foreach(k => nctx.constrain(k)) - - def asSubcls(x: ClassLikeType, y: ClsTag): Opt[ClassLikeType] = - if x.sym === y then S(x) - else - x.sym match - case lit: LitSymbol => - lit.lit match - case _: IntLit => - if prim.intSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N - case _: StrLit => - if prim.strSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N - case _: BoolLit => - if prim.boolSym === y then S(ClassLikeType(y, Nil, Nil, Nil, N)) else N - case _ => N - case _ => N + def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = + val k = K(lb, s, N) + if s.lvl < k.lvl then xbds += k + else + val v = varSt.getOrElseUpdate(s.sym, new InfVarState) + v.lowerBounds = lb :: v.lowerBounds + v.upperBounds.foreach(p => constrain(K(lb, p._1, p._2))) + def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) + (using CCtx, TL, Raise, Scope) = + given InfCtx = this + raise(ErrorReport( + msg"Type error in ${origin.describe}${exp match + case S(ty) => msg" with expected type ${ty.show}" + case N => msg"" + }" -> origin.toLoc + :: parents.reverse.map(p => + msg"because: cannot constrain ${p._1.show} <: ${p._2.show}" -> N + ) + )) + // TODO + def ubs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).upperBounds.map(_._1) + def lbs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds + // def withPrefix(x: Type, y: Type) = ??? + override def constrain(c: K)(using CCtx, TL, Raise) = prefix match + case N => super.constrain(c) + case S(Nil) => + case S(cs) => cs.foreach(k => super.constrain(or(k,c))) class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config): val objSym = ctx.get("Object").get.symbol.get.asTpe.get @@ -110,7 +113,7 @@ class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config): object InfCtx: def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL, cfg: Config): InfCtx = given PrimCtx = new PrimCtx - InfCtx(1, N, HashMap.empty, Bot, Nil, Nil)(using HashMap.empty) + InfCtx(1, N, HashMap.empty, Bot)(using HashMap.empty, ListBuffer.empty) def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, N) def litTy(lit: Literal)(using ctx: InfCtx) = mkTag(ctx.prim.litSym(lit)) def objTy(using ctx: InfCtx) = mkTag(ctx.prim.objSym) @@ -119,11 +122,7 @@ object InfCtx: val w = Ls(Wildcard.in(u), Wildcard.out(ret), Wildcard.out(eff)) val i = Ls(true, false, false) ClassLikeType(ctx.prim.fnSym, w, Nil, i, S(0)) - def asRefinedObj(t: Ls[Type])(using ctx: InfCtx) = - val r = t.zipWithIndex.map: - case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) - ClassLikeType(ctx.prim.objSym, Nil, r, Nil, N) - // def arrayTy(elem: Type)(using ctx: InfCtx) = ClassLikeType(ctx.getCls("Array"), Ls(elem), Nil, Nil) + // def arrayTy(elem: Type)(using ctx: InfCtx) = ClassLikeType(ctx.prim.arrSym, Ls(elem), Nil, Nil) def tupTy(e: Ls[Type])(using ctx: InfCtx) = // val refine = (Tree.Ident("size"): Tree.Ident, litTy(IntLit(e.length))) :: e.zipWithIndex.map: // case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy) @@ -133,3 +132,25 @@ object InfCtx: ClassLikeType(ctx.prim.arrSym, Nil, refine, Nil, N) def refinedObj(r: Ls[Tree.Ident -> Type])(using ctx: InfCtx) = ClassLikeType(ctx.prim.objSym, Nil, r, Nil, N) + +class SuffixCtx(val suffix: Ls[K], val cont: KCtx)(using PrimCtx) extends KCtx: + def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = cs match + case N => cont.addub(s, ub, S(suffix)) + case S(Nil) => + case S(cs) => cont.addub(s, ub, S(cs.flatMap(k => suffix.map(or(k,_))))) + def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = ??? + def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) + (using CCtx, TL, Raise, Scope) = + suffix.foreach(cont.constrain) + +class MkPrefix(using PrimCtx) extends KCtx: + var r = Opt(ListBuffer.empty[K]) + def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = + r.foreach(_ += K(s, ub, cs)) + def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = ??? + def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) + (using CCtx, TL, Raise, Scope) = + r = N + def apply(x: Type, y: Type)(using CCtx, TL, Raise): Opt[Ls[K]] = + constrain(sub(x,y)) + r.map(_.toList) diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala index c980af617d..194360d695 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala @@ -22,26 +22,24 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): import tl.{trace, log} private val builtinOps = Elaborator.binaryOps ++ Elaborator.unaryOps ++ Elaborator.aliasOps.keySet - private def error(msg: Ls[Message -> Opt[Loc]], extraInfo: => Opt[Any] = N)(using InfCtx) = + private def error(msg: Ls[Message -> Opt[Loc]], extraInfo: => Opt[Any] = N) = raise(ErrorReport(msg, extraInfo = extraInfo)) Bot // TODO: error type? private def freshVar(origin: Symbol | Term, hint: Str = "")(using ctx: InfCtx) = - // ctx.freshVar(origin, hint) InfVar(ctx.lvl, InfVarSymbol(origin, hint), false) private def freshWildcard(s: Symbol)(using InfCtx) = Wildcard(freshVar(s),freshVar(s)) private def freshOuter(sym: Symbol)(using ctx: InfCtx): InfVar = - // ctx.freshOuter(sym) InfVar(ctx.lvl + 1, InfVarSymbol(sym), true) private def freshEnv(sym: Symbol)(using ctx: InfCtx): InfVar = val s = InfVarSymbol(sym) val state = new InfVarState ctx.varSt += s -> state - state.upperBounds = ctx.outRegAcc :: Nil + state.upperBounds = ctx.outRegAcc -> N :: Nil state.lowerBounds = ctx.outRegAcc :: Nil InfVar(ctx.lvl, s, false) - private def mono(ty: InfType)(using ctx: InfCtx): Opt[Type] = ty match + private def mono(ty: InfType)(using InfCtx): Opt[Type] = ty match case x: Type => S(x) case PolyFunType(args, ret, eff) => val a = args.map(mono) @@ -134,8 +132,9 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): tv -> qv bds.foreach: case (tv, QuantVar(_, ub, lb)) => - ub.foreach(ub => ctx.addub(tv,typeMonoType(ub))) - lb.foreach(lb => ctx.addlb(typeMonoType(lb), tv)) + val v = ctx.varSt.getOrElseUpdate(tv.sym, new InfVarState) + ub.foreach(ub => v.upperBounds = typeMonoType(ub) -> N :: v.upperBounds) + lb.foreach(lb => v.lowerBounds = typeMonoType(lb) :: v.lowerBounds) val lbty = ctx.lbs(tv.sym).foldLeft[Type](Bot)(_ | _) val ubty = ctx.ubs(tv.sym).foldLeft[Type](Top)(_ & _) constrain(lbty, ubty) @@ -152,7 +151,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ty private def constrain(x: Type, y: Type)(using ctx: InfCtx, cctx: CCtx): Unit = - ctx.constrain(ctx.sub(x,y)) + ctx.constrain(K(x,y,N)) // TODO private def fundef(sym: Symbol, lam: Term, sig: Opt[Term]) (using ctx: InfCtx, cctx: CCtx, scope: Scope) = lam match @@ -187,8 +186,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): Subst(map)(true)(x) private def substMono(map: Map[InfVarSymbol, InfVar])(x: K): K = x match - case K(x, y: Type) => K(substMono(map)(x), substMono(map)(y)) - case K(x, DisjOr(p, cs)) => K(substMono(map)(x), DisjOr(substMono(map)(p), cs.map(substMono(map)))) + case K(x, y, cs) => K(substMono(map)(x), substMono(map)(y), cs.map(_.map(substMono(map)))) private def subst(map: Map[InfVarSymbol, InfVar])(x: InfType): InfType = x match @@ -209,9 +207,9 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ctx.varSt.get(v.sym).foreach: st => val ns = new InfVarState ctx.varSt += map(v.sym).sym -> ns - ns.upperBounds = st.upperBounds.map(substMono(map)) + ns.upperBounds = st.upperBounds.map: d => + substMono(map)(d._1) -> d._2.map(_.map(substMono(map))) ns.lowerBounds = st.lowerBounds.map(substMono(map)) - ns.disjsub = st.disjsub.map(d => DisjOr(substMono(map)(d.p), d.cs.map(substMono(map)))) // TODO bound scheme xbds.foreach(k => ctx.constrain(substMono(map)(k))) subst(map)(body) @@ -229,9 +227,9 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ctx.varSt.get(v.sym).foreach: st => val ns = new InfVarState ctx.varSt += map(v.sym).sym -> ns - ns.upperBounds = st.upperBounds.map(substMono(map)) + ns.upperBounds = st.upperBounds.map: d => + substMono(map)(d._1) -> d._2.map(_.map(substMono(map))) ns.lowerBounds = st.lowerBounds.map(substMono(map)) - ns.disjsub = st.disjsub.map(d => DisjOr(substMono(map)(d.p), d.cs.map(substMono(map)))) // xbds.foreach(k => ctx.constrain(substMono(map)(k))) subst(map)(body) From 7f434f73d830b3209b039681709009cdf9711cb7 Mon Sep 17 00:00:00 2001 From: AU Heung Tung <101095686+auht@users.noreply.github.com> Date: Mon, 26 Oct 2026 12:23:44 +0800 Subject: [PATCH 6/6] init ucs draft and tests --- .../scala/hkmc2/typing/ConstraintSolver.scala | 18 +- .../src/main/scala/hkmc2/typing/infctx.scala | 128 ++++++++--- .../src/main/scala/hkmc2/typing/inftype.scala | 12 +- .../main/scala/hkmc2/typing/logicsub.scala | 49 +++- .../shared/src/test/mlscript/logicsub/Ex.mls | 214 ++++++++++++++++++ .../shared/src/test/mlscript/logicsub/If.mls | 155 +++++++++++++ .../src/test/mlscript/logicsub/test.mls | 9 +- .../test/scala/hkmc2/LogicSubDiffMaker.scala | 1 + 8 files changed, 535 insertions(+), 51 deletions(-) create mode 100644 hkmc2/shared/src/test/mlscript/logicsub/Ex.mls create mode 100644 hkmc2/shared/src/test/mlscript/logicsub/If.mls diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala index a6b1578a0b..a99c0bdec3 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala @@ -55,7 +55,7 @@ object ConstraintSolver: case (t, true) => t.posPart val d = (x.refinement.values ++ da).toList if d.isEmpty then cctx.err - else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.or(k, ctx.sub(t, Bot)))) + else ctx.constrain(d.map(K(_, Bot)).reduce(_.or(_))) case Conj(NF.Inter(x :: Nil), NF.Union(y :: Nil), N,N,_,_) => val da = x.args.iterator.zip(x.congr).collect: case (t, true) => t.posPart @@ -65,28 +65,28 @@ object ConstraintSolver: val sp = ctx.asSubcls(x,y.sym) if sp.isEmpty || !yrm.keySet.subsetOf(xrm.keySet) then if d.isEmpty then cctx.err - else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.or)) + else ctx.constrain(d.map(K(_, Bot)).reduce(_.or(_))) else val x = sp.get val u = x.args.zip(y.args).flatMap(ctx.subArg) val w = y.refinement.map: - case (a,b) => ctx.sub(xrm(a), b) + case (a,b) => K(xrm(a), b) val ds = x.refinement.filterNot(f => yrm.contains(f._1)).map: - case (_,t) => ctx.sub(t,Bot) + case (_,t) => K(t,Bot) (u++w).foreach: k => - ctx.constrain((ds ++ Ls(k)).reduce(ctx.or)) + ctx.constrain((ds ++ Ls(k)).reduce(_.or(_))) case Conj(NF.Inter(xs @ (x :: _)), NF.Union(y :: Nil), N,N,_,_) => if x.sym === y.sym then val k = x.ov.get val u = xs.map(_.args(k).negPart.discriminator) val w = u.reduce[Type](_|_) val in = y.args(k) - ctx.constrain(ctx.sub(in.negPart, w)) + ctx.constrain(K(in.negPart, w)) u.lazyZip(xs).foreach: (p, c) => - val d = ctx.sub(in.negPart, ~p) + val d = K(in.negPart, ~p) val r = y.copy(args = y.args.updated(k, Wildcard(p & in.negPart, in.posPart))) - val s = ctx.sub(c, r) - ctx.constrain(ctx.or(d, s)) + val s = K(c, r) + ctx.constrain(d.or(s)) else cctx.err case Conj(k @ NF.Inter(x :: _), NF.Union(ys @ (_ :: _)), N,N,ws,zs) => def h(y: ClassLikeType) = diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala index 512e579149..e017903b40 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala @@ -14,22 +14,22 @@ import Elaborator.Ctx import syntax.* import Tree.* import utils.Scope +import scala.collection.mutable -final case class K(x: Type, y: Type, cs: Opt[Ls[K]]): +final case class K(x: Type, y: Type, cs: Opt[Ls[K]] = N): def lvl: Int = x.lvl max y.lvl max cs.fold(0)(_.map(_.lvl).max) + def or(k: K): K = cs match + case N => K(x, y, S(Ls(k))) + case S(cs) => K(x, y, S(cs.map(_.or(k)))) class InfVarState: var lowerBounds: Ls[Type] = Nil var upperBounds: Ls[Type -> Opt[Ls[K]]] = Nil trait KCtx(using val prim: PrimCtx): - def sub(x: Type, y: Type): K = K(x,y,N) - def subArg(x: TypeArg, y: TypeArg): Ls[K] = - sub(x.posPart,y.posPart) :: sub(y.negPart,x.negPart) :: Nil - def or(x: K, y: K): K = (x,y) match - case (K(a, b, N), y) => K(a, b, S(Ls(y))) - case (K(a, b, S(cs)), y) => K(a, b, S(cs.map(or(_,y)))) - def constrain(c: K)(using CCtx, TL, Raise): Unit = c match + def subArg(x: TypeArg, y: TypeArg) = + K(x.posPart,y.posPart) :: K(y.negPart,x.negPart) :: Nil + def constrain(c: K)(using CCtx, TL, Raise) = c match case K(x,y,N) => ConstraintSolver.constrain(x,y)(using this) case K(x,y,S(Nil)) => case K(x,y,S(cs)) => ConstraintSolver.constrain(x,y)(using SuffixCtx(cs, this)) @@ -46,24 +46,23 @@ trait KCtx(using val prim: PrimCtx): def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) (using CCtx, TL, Raise, Scope): Unit -final case class InfCtx( - lvl: Int, - parent: Option[InfCtx], - env: HashMap[Symbol, InfType], - outRegAcc: Type, - prefix: Opt[Ls[K]] = N +class InfCtx( + val lvl: Int, + val parent: Option[InfCtx], + val env: HashMap[Symbol, InfType], + val outRegAcc: Type, + val xbds: ListBuffer[K] )(using val varSt: HashMap[InfVarSymbol, InfVarState], - val xbds: ListBuffer[K], prim: PrimCtx, val ctx: Ctx, val cfg: Config ) extends KCtx: def +=(p: Symbol -> InfType) = env += p def get(sym: Symbol): Option[InfType] = env.get(sym) `orElse` parent.dlof(_.get(sym))(None) - def nest: InfCtx = copy(parent = Some(this), env = HashMap.empty) - def nestWithOuter(outer: InfVar): InfCtx = copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer) - def nextLevel: InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty) + def nest = InfCtx(lvl, Some(this), HashMap.empty, outRegAcc, xbds) + def nestWithOuter(outer: InfVar) = InfCtx(lvl + 1, Some(this), HashMap.empty, outRegAcc | outer, ListBuffer.empty) + def nextLevel = InfCtx(lvl + 1, Some(this), HashMap.empty, outRegAcc, ListBuffer.empty) def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = val k = K(s, ub, cs) @@ -71,7 +70,7 @@ final case class InfCtx( else val v = varSt.getOrElseUpdate(s.sym, new InfVarState) v.upperBounds = ub -> cs :: v.upperBounds - v.lowerBounds.foreach(lb => constrain(sub(lb, ub))) + v.lowerBounds.foreach(lb => constrain(K(lb, ub))) def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = val k = K(lb, s, N) if s.lvl < k.lvl then xbds += k @@ -92,13 +91,11 @@ final case class InfCtx( ) )) // TODO - def ubs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).upperBounds.map(_._1) - def lbs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds + def ubs(s: InfVarSymbol) = varSt.getOrElseUpdate(s, new InfVarState).upperBounds.map(_._1) + def lbs(s: InfVarSymbol) = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds // def withPrefix(x: Type, y: Type) = ??? - override def constrain(c: K)(using CCtx, TL, Raise) = prefix match - case N => super.constrain(c) - case S(Nil) => - case S(cs) => cs.foreach(k => super.constrain(or(k,c))) + def thenCtx(env: HashMap[Symbol, InfType], prefix: Ls[K]) = + ThenCtx(lvl, S(this), env, outRegAcc, xbds, prefix) class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config): val objSym = ctx.get("Object").get.symbol.get.asTpe.get @@ -111,9 +108,9 @@ class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config): def litSym(x: syntax.Literal) = LitSymbol(x) object InfCtx: - def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL, cfg: Config): InfCtx = + def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL, cfg: Config) = given PrimCtx = new PrimCtx - InfCtx(1, N, HashMap.empty, Bot)(using HashMap.empty, ListBuffer.empty) + InfCtx(1, N, HashMap.empty, Bot, ListBuffer.empty)(using HashMap.empty) def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, N) def litTy(lit: Literal)(using ctx: InfCtx) = mkTag(ctx.prim.litSym(lit)) def objTy(using ctx: InfCtx) = mkTag(ctx.prim.objSym) @@ -137,7 +134,7 @@ class SuffixCtx(val suffix: Ls[K], val cont: KCtx)(using PrimCtx) extends KCtx: def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = cs match case N => cont.addub(s, ub, S(suffix)) case S(Nil) => - case S(cs) => cont.addub(s, ub, S(cs.flatMap(k => suffix.map(or(k,_))))) + case S(cs) => cont.addub(s, ub, S(cs.flatMap(k => suffix.map(k.or)))) def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = ??? def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) (using CCtx, TL, Raise, Scope) = @@ -151,6 +148,77 @@ class MkPrefix(using PrimCtx) extends KCtx: def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) (using CCtx, TL, Raise, Scope) = r = N - def apply(x: Type, y: Type)(using CCtx, TL, Raise): Opt[Ls[K]] = - constrain(sub(x,y)) + def apply(x: Type, y: Type)(using CCtx, TL, Raise) = + constrain(K(x,y)) r.map(_.toList) + +class ThenCtx( + lvl: Int, parent: Option[InfCtx], + env: HashMap[Symbol, InfType], outRegAcc: Type, + xbds: ListBuffer[K], prefix: Ls[K] +)(using HashMap[InfVarSymbol, InfVarState], PrimCtx, Ctx, Config) +extends InfCtx(lvl, parent, env, outRegAcc, xbds): + override def nest = ThenCtx(lvl, Some(this), HashMap.empty, outRegAcc, xbds, prefix) + override def nestWithOuter(outer: InfVar) = + ThenCtx(lvl + 1, Some(this), HashMap.empty, outRegAcc | outer, ListBuffer.empty, prefix) + override def nextLevel = + ThenCtx(lvl + 1, Some(this), HashMap.empty, outRegAcc, ListBuffer.empty, prefix) + // override def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = + // cont.addub(s,ub,cs) + // override def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = cont.addlb(lb,s) + // override def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType]) + // (using CCtx, TL, Raise, Scope) = cont.err(parents, origin, exp) + override def constrain(c: K)(using CCtx, TL, Raise) = + prefix.foreach(k => parent.get.constrain(k.or(c))) + + +class MatchCtx( + val prefix: Opt[MatchCtx], + val refine: Ls[Ls[Ref -> Type]], + val svt: HashMap[Ref, InfVar -> Type] +): + def end = if prefix.isEmpty then ??? + def pm(s: Ref, t: => Type, cp: FlatPattern.ClassLike) + (using ctx: InfCtx, scope: Scope, st: Elaborator.State) = + val sym = cp.constructor.symbol.get.asCls.get + val params = sym.defn.get.tparams + val patt = ClassLikeType(sym, params.map(_ => Wildcard.empty), Nil, params.map(_ => false), N) // TODO + val (sv, st) = svt.get(s) match + case N => + val vsym = new TempSymbol(S(s), erasedType = N, s.sym.nme) + val v = InfVar(ctx.lvl, InfVarSymbol(vsym), false) + svt += s -> (v , t) + (v, t) + case S(v, t) => (v, t) + val nr = refine.map(s -> patt :: _) + MatchCtx(S(this), nr, svt) + def el = MatchCtx(prefix.get.prefix, pneg, svt) + def thenCtx(using ctx: InfCtx)(using CCtx, TL, Raise): InfCtx = + val c = prefix match + case N => ctx + case S(p) => p.thenCtx + // val ss = refine.flatMap(_.keys).distinct + if refine.contains(Nil) then c + else + val p = refine.map: r => + val m = r.groupMapReduce(_._1)(_._2)(_&_) + val ss = r.keys.distinct.toList + // TODO + val s = ss.map: s => + val (v, t) = svt(s) + c.constrain(K(m(s) & t, v)) + ss.map(s => K(svt(s)._2, ~m(s))).reduceRight(_.or(_)) + c.thenCtx(env, p) + def env: HashMap[Symbol, InfType] = + val ss = refine.flatMap(_.keys).distinct + // if refine.length == 1 + HashMap.from(ss.map(s => s.sym -> svt(s)._1)) + def cond(r: Ls[Ref -> Type]): K = + val m = r.groupMapReduce(_._1)(_._2)(_&_) + r.keys.distinct.map(s => K(svt(s)._2, ~m(s))).reduceRight(_.or(_)) + def pneg: Ls[Ls[Ref -> Type]] = + refine.foldRight(Ls(Nil)): (r, ps) => + ps.flatMap(p => r.map((s, t) => (s, ~t) :: p)) + +object MatchCtx: + def init: MatchCtx = MatchCtx(N, Ls(Nil), HashMap.empty) \ No newline at end of file diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala index 782c433612..62f0e088bc 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala @@ -58,8 +58,16 @@ object Wildcard: case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], xbds: Ls[K], body: InfType) extends InfType: lazy val lvl = (body :: tvs).map(_.lvl).max - def show(using Scope, InfCtx, Raise) = showDbg //TODO - def showDbg = ??? + def show(using Scope, InfCtx, Raise) = + given Scope = scope.nest + val lst = (outer match { + case S(outer) => + val op = outer.show + (if op === "outer" then op else s"outer $op") :: Nil + case N => Nil + }) ++ tvs.map(_.show) + s"[${lst.mkString(", ")}] -> ${body.show}" + def showDbg = s"[${(outer.toList ++ tvs).map(_.showDbg).mkString(", ")}] -> ${body.showDbg}" case class PolyFunType(args: Ls[InfType], ret: InfType, eff: Type) extends InfType: lazy val lvl = (ret :: eff :: args).iterator.map(_.lvl).max diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala index 194360d695..4a4880dd54 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala @@ -15,10 +15,10 @@ import Elaborator.Ctx import syntax.* import Tree.* import utils.Scope -import hkmc2.codegen.ErasedType.eraseSign +import hkmc2.syntax.Keyword.out -class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): +class Typer(using tl: TL)(using Elaborator.State, Raise, codegen.Erasure, Ctx, Config): import tl.{trace, log} private val builtinOps = Elaborator.binaryOps ++ Elaborator.unaryOps ++ Elaborator.aliasOps.keySet @@ -162,7 +162,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): ascribe(lam, sigTy) () case N => - val outer = freshOuter(new TempSymbol(S(lam), erasedType = N, "outer"))(using ctx) + val outer = freshOuter(TempSymbol(S(lam), erasedType = N, "outer"))(using ctx) given InfCtx = ctx.nestWithOuter(outer) val funTyV = freshVar(sym) ctx += sym -> funTyV // for recursive functions @@ -176,7 +176,6 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case _ => error(msg"Function definition shape not yet supported for ${sym.nme}" -> lam.toLoc :: Nil) - private class Subst(map: Map[InfVarSymbol, InfVar]) extends TypeMap: override def apply(pol: Bool)(t: Type) = t.toBasic match case v @ InfVar(_, s, _) => map.get(s).getOrElse(v) @@ -197,7 +196,7 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): private def instantiate(x: PolyType)(using ctx: InfCtx, cctx: CCtx) = val PolyType(tvs, outer, xbds, body) = x - val env = freshEnv(new TempSymbol(N, erasedType = N, "env")) + val env = freshEnv(TempSymbol(N, erasedType = N, "env")) val map = (outer.map(_.sym -> env).toList ++ tvs.map(v => val nv = InfVar(ctx.lvl, InfVarSymbol(InstSymbol(v.sym), v.sym.hint), false) tl.log(s"instantiate ${v.showDbg} ~> ${nv.showDbg}") @@ -233,7 +232,9 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): // xbds.foreach(k => ctx.constrain(substMono(map)(k))) subst(map)(body) - private def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int): PolyType = ??? + private def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int)(using ctx: InfCtx): PolyType = + // TODO + PolyType(Nil, outer, ctx.xbds.toList, ty) private def app(lhs: InfType, lhsEff: Type, rhs: Ls[Elem], t: Term) (using ctx: InfCtx, cctx: CCtx, scope: Scope) @@ -330,6 +331,35 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): case N => (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot) + private def typeSplitImpl(split: Split, sign: InfType, eff: Type, pre: MatchCtx) + (using InfCtx, CCtx, Scope): Unit = split match + case Split.Cons(Branch(s: Ref, cp: FlatPattern.ClassLike, cons), alts) => + val p = pre.pm(s, tryMkMono(typeCheck(s)._1, s), cp) + typeSplitImpl(cons, sign, eff, p) + typeSplitImpl(alts, sign, eff, p.el) + case Split.Cons(Branch(_, p, _), _) => + error(msg"Unsupported pattern" -> p.toLoc :: Nil) + case Split.Else(e) => + given InfCtx = pre.thenCtx + constrain(ascribe(e, sign)._2, eff) + case Split.Let(name, term, tail) => + val nestCtx = pre.thenCtx + nestCtx.givenIn: + val termTy = typeCheck(term) + // val sk = freshSkolem(name) + nestCtx += name -> termTy._1 + typeSplitImpl(tail, sign, eff, pre) + case Split.End => //TODO + case _ => ??? + + private def typeSplit + (split: Split, sign: Opt[InfType])(using InfCtx, CCtx, Scope) + : (InfType, Type) = + val res = sign.getOrElse(freshVar(new TempSymbol(N, erasedType = N, "res"))) + val eff = freshVar(new TempSymbol(N, erasedType = N, "eff")) + typeSplitImpl(split, res, eff, MatchCtx.init) + (res, eff) + def ascribe(lhs: Term, rhs: InfType)(using ctx: InfCtx, scope: Scope): (InfType, Type) = // TODO trace[(InfType, Type)](s"${ctx.lvl}. Ascribing ${lhs.showDbg} : ${rhs.showDbg}", res => s"! ${res._2.showDbg}"): given CCtx = CCtx.init(lhs, S(rhs)) @@ -357,8 +387,8 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): given InfCtx = nextCtx constrain(ascribe(term, skolemize(pt))._2, Bot) // * never generalize terms with effects (pt, Bot) - // case (Term.IfLike(_, IfLikeForm.ReturningIf, split), ty) => // * propagate - // typeAllSplits(split.getExpandedSplit, S(ty)) + case (Term.IfLike(_, IfLikeForm.ReturningIf, split), ty) => // * propagate + typeSplit(split.getExpandedSplit, S(ty)) case (Term.Asc(term, ty), rhs) => ascribe(term, typeType(ty)) ascribe(term, rhs) @@ -410,7 +440,8 @@ class Typer(using elState: Elaborator.State, tl: TL, raise: Raise): (Tree.Ident(i.toString): Tree.Ident, tryMkMono(ty, f)) case (spd: Spd, _) => TODO(s"spread arguments: $spd") (InfCtx.refinedObj(fs), eff) - // case Term.IfLike(_, IfLikeForm.ReturningIf, split) => typeAllSplits(split.getExpandedSplit, N) + case Term.IfLike(_, IfLikeForm.ReturningIf, split) => + typeSplit(split.getExpandedSplit, N) case Lam(PlainParamList(params), body) => val nestCtx = ctx.nest given InfCtx = nestCtx diff --git a/hkmc2/shared/src/test/mlscript/logicsub/Ex.mls b/hkmc2/shared/src/test/mlscript/logicsub/Ex.mls new file mode 100644 index 0000000000..ce79f082bd --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/Ex.mls @@ -0,0 +1,214 @@ +#config(language: Language(typeCheck: TypeChecking())) +//│ Type: undefined + +declare class Str(length: Int, concat: Str -> Str) +declare fun (+): (Int, Int) -> Int +//│ Type: undefined + +fun addImpl(x, y) = if x is + Int then x + y + Str then x.Str#concat(y) +//│ Type: undefined + +fun add: ((Int,Int) -> Int) & ((Str,Str) -> Str) +fun add(x,y) = addImpl(x,y) +//│ Type: undefined + +// FIXME +add(1, 2) +//│ Type: 'app +//│ >: ⊥ + +// add("a", "b") + +fun test(a,b,c,d) = add(a,add(b,add(c,d))) +//│ Type: undefined + +// FIXME +test(0, 1, 2, 3) +//│ Type: 'app +//│ >: ⊥ + +// test("A", "B", "C", "D") + +// Expected type errors: +// test(0, 1, "oops", 3) + +fun selfAdd1(x) = add(x, x) +//│ Type: undefined + +fun intstr: Int | Str +//│ Type: undefined + +// Expected type errors: +// selfAdd1(intstr) + +fun selfAdd2(x) = if x is + Int then add(x, x) + Str then add(x, x) +//│ Type: undefined + +// FIXME +// selfAdd2(intstr) + +fun selfAdd3: (Int -> Int) & (Str -> Str) +fun selfAdd3(x) = selfAdd1(x) +selfAdd3(intstr) +//│ Type: 'app +//│ >: Int ∨ Str + +// fun selfAdd4: (Int | Str) -> (Int | Str) +// fun selfAdd4(x) = selfAdd1(x) + +fun selfAdd5: (Int | Str) -> (Int | Str) +fun selfAdd5(x) = selfAdd3(x) +//│ Type: undefined + +fun cast : ((Int -> Int) & (Str -> Str)) -> (Int | Str) -> (Int | Str) +fun cast(f) = f +//│ Type: undefined + +// cast(selfAdd1) + + + +class + A() + B() +//│ Type: undefined + +// fun useTagged ( x : ([ kind : A , a : Int ] | [ kind : B , b : Str ])) = +// if x.kind is +// A then x.a + 1 +// B then x.b.Str#length + +// fun test (k , a , b) = useTagged ({ kind : k , a : a , b : b }) + +fun test : ((A, Int, Any) -> Int) & ((B, Any, Str) -> Int) +//│ Type: undefined + +test as (A | B, Int, Str) -> Int +//│ Type: (A ∨ B, Int, Str) ->{⊥} Int + + + +class + Tru() + Fls() +//│ Type: undefined + +let + tru = new Tru() + fls = new Fls() +//│ Type: undefined + +fun negImpl(x) = if x is + Tru then fls + Fls then tru +negImpl +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res + +fun negate: (Tru -> Fls) & (Fls -> Tru) +fun negate(x) = negImpl(x) +//│ Type: undefined + +fun bothImpl(x,y) = if + x is Tru and y is Tru then tru + x is Tru and y is Fls then fls + x is Fls and y is Tru then fls + x is Fls and y is Fls then fls +//│ Type: undefined + +fun both: ((Tru, Tru) -> Tru) & ((Tru, Fls) -> Fls) & ((Fls, Tru | Fls) -> Fls) +fun both(x, y) = bothImpl(x,y) +//│ Type: undefined + + +class Ls[A]() +//│ Type: undefined + +fun foldLeft: [A,B] -> (Ls[A], B, (B, A) -> B) -> B +//│ Type: undefined + +// FIXME +// fun all(xs) = foldLeft(xs, tru, both) +// all + +// FIXME +// all as Ls[Tru] -> Tru +// all as Ls[Fls] -> Tru | Fls + +class + Nil() + Cons[A, B](val hd : A, val tl: B) +//│ Type: undefined + +fun all2(x) = if x is + Nil then tru + Cons then both(x.Cons#hd, all2(x.Cons#tl)) +//│ Type: undefined + +let nil = new Nil() +fun cons(x,y) = new Cons(x,y) +//│ Type: undefined + +all2(nil) +//│ Type: 'app +//│ >: ⊥ + +all2(cons(tru, nil)) +//│ Type: 'app +//│ >: ⊥ + +all2(cons(tru, cons(tru, nil))) +//│ Type: 'app +//│ >: ⊥ + +all2(cons(tru, cons(fls, nil))) +//│ Type: 'app +//│ >: ⊥ + +fun test: Tru -> Tru +fun test(x) = all2(cons(tru, cons(x, nil))) +//│ Type: undefined + +fun test: Fls -> Tru | Fls +fun test(x) = all2(cons(tru, cons(x, nil))) +//│ Type: undefined + +fun foldLeft(xs, y, f) = if xs is + Nil then y + Cons then foldLeft(xs.Cons#tl, f(y,xs.Cons#hd), f) +//│ Type: undefined + +fun all3(xs) = foldLeft(xs, tru, both) +//│ Type: undefined + +all3 as Nil -> Tru +//│ Type: (Nil) ->{⊥} Tru + +// FIXME +// all3 as Cons[Tru,Nil] -> Tru +// all3 as Cons[Tru|Fls,Nil] -> Tru | Fls + +fun test: (Tru -> Tru) & (Fls -> Tru | Fls) +fun test(x) = all3(cons(tru, cons(x, nil))) +//│ Type: undefined + + + +class + None() + Some[A](val x: A) +//│ Type: undefined + +let none = new None() +//│ Type: undefined + +fun headOption(x) = if x is + Nil then none + Cons then new Some(x.Cons#hd) +//│ Type: undefined + +headOption +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res diff --git a/hkmc2/shared/src/test/mlscript/logicsub/If.mls b/hkmc2/shared/src/test/mlscript/logicsub/If.mls new file mode 100644 index 0000000000..74f78ffeab --- /dev/null +++ b/hkmc2/shared/src/test/mlscript/logicsub/If.mls @@ -0,0 +1,155 @@ +#config(language: Language(typeCheck: TypeChecking())) +//│ Type: undefined + +declare fun (+): (Int, Int) -> Int +//│ Type: undefined + +fun ib: Int | Bool +fun si: Str | Int +fun sib: Str | Int | Bool +fun rev: Str -> Str +fun neg: Bool -> Bool +//│ Type: undefined + +fun f(x) = if x is + Int then 0 + Bool then x +f +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res + +// FIXME +// f(ib) as (Int | Bool) + +// f(f(ib)) as Int | Bool +// f(f(ib)) + +// FIXME +// :e +f(si) +//│ Type: 'app +//│ >: ⊥ + + +// order-dependent (expected) + +fun f(x, y) = if + x is Int then 1 + y is Str then "" +f(1, "") +//│ Type: 'app +//│ >: ⊥ + +f(1, sib) +//│ Type: 'app +//│ >: ⊥ + +fun f(x, y) = if + y is Str then "" + x is Int then 1 +f(1, "") +//│ Type: 'app +//│ >: ⊥ + +f(1, sib) +//│ Type: 'app +//│ >: ⊥ + +// FIXME +// fun foorec(x, y, r) = if +// x is Int and y is Int then x + y +// x is Str then not(y) +// y is Str then r(y, x, r) + +// fun foo(x, y) = foorec(x, y, foorec) + +// foo(true, "") +// foo(1, 2) +// foo as (Int, Int) -> Int +// foo as (Str, Bool) -> Bool +// (x => foo(x, true)) as Str -> Bool +// (x => foo(x, "")) as Bool -> Bool + +// :e +// foo(1, "") + +fun increv(x) = if x is + Int then x + 1 + else + rev(x) +increv +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res + +fun increv'(x) = if x is + Int then x + 1 + Str then rev(x) +increv' +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res + +// FIXME +// :e +increv(sib) +//│ Type: 'app +//│ >: ⊥ + +// FIXME +// :e +// increv'(sib) + +increv(si) +//│ Type: 'app +//│ >: ⊥ + +// FIXME +// increv'(si) + +fun f(x, y) = if + x is Int and y is Int then 1 + x is Bool then y +//│ Type: undefined + +// literal matching not yet implemented + +// x => if x is +// true then 0 +// false then 0 + +fun f(x) = if + x is Int then x + 2 + x is Str then rev(x) + else + neg(x) +f +//│ Type: [outer] -> ['x] ->{out 'eff} out 'res + +// f(sib) + +fun f(x, y) = if + x is Int then y + y is Str then 1 + x is Str then y + 1 + else + neg(x) +f +//│ Type: [outer] -> ['x, 'y] ->{out 'eff} out 'res + +f(ib, sib) +//│ Type: 'app +//│ >: ⊥ + +// :ns +f(ib, ib) +//│ Type: 'app +//│ >: 1 + +// :todo +// f(ib, ib) + +fun f(x, y) = if + x is Int then 1 + y is Int then neg(x) +f +//│ Type: [outer] -> ['x, 'y] ->{out 'eff} out 'res + +f(ib, 1) +//│ Type: 'app +//│ >: ⊥ diff --git a/hkmc2/shared/src/test/mlscript/logicsub/test.mls b/hkmc2/shared/src/test/mlscript/logicsub/test.mls index 45ece01d1a..a557a2f8b2 100644 --- a/hkmc2/shared/src/test/mlscript/logicsub/test.mls +++ b/hkmc2/shared/src/test/mlscript/logicsub/test.mls @@ -16,7 +16,7 @@ f("a") fun g: (Int -> Int) & (Str -> Str) //│ Type: undefined -// TODO +// FIXME g(1) //│ Type: 'app //│ >: ⊥ @@ -27,3 +27,10 @@ fun g: (1 -> 1) & (2 -> 2) g(1) //│ Type: 'app //│ >: 1 + +fun neg: (true -> false) & (false -> true) +//│ Type: undefined + +// TODO literal pattern +// fun a: (false -> Int) & (true -> Str) +// fun a(x) = if neg(x) then 1 else "" diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala index f62aecfdc6..cf9ffbd788 100644 --- a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala +++ b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala @@ -23,6 +23,7 @@ abstract class LogicSubDiffMaker extends WasmDiffMaker: given Scope = Scope.empty(Scope.Cfg.default) if typer.isEmpty then given Elaborator.Ctx = curCtx + given codegen.Erasure = codegen.Erasure(trm) typer = S(logicsub.Typer()) given logicsub.InfCtx = infctx val ty = typer.get.typePurely(trm)