Skip to content

Commit

Permalink
increase test coverage
Browse files Browse the repository at this point in the history
  • Loading branch information
@johnynek
johnynek committed Dec 22, 2023
1 parent adb68be commit 4fed9c5
Show file tree
Hide file tree
Showing 3 changed files with 138 additions and 108 deletions.
34 changes: 19 additions & 15 deletions core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -695,13 +695,6 @@ object Infer {
} yield coerce.andThen(unskolemizeExists(exSkols))
}

def instSigmaTypedExpr[A](te: TypedExpr[A]): Infer[(TypedExpr.Rho[A], Type.Rho)] =
for {
(exSkols, rho) <- instantiate(te.getType)
ks <- checkedKinds
coerce = TypedExpr.coerceRho(rho, ks)
} yield (coerce.andThen(unskolemizeExists(exSkols))(te), rho)

def unifyFnRho(arity: Int, fnType: Type.Rho, fnRegion: Region, evidenceRegion: Region): Infer[(NonEmptyList[Type], Type)] =
fnType match {
case Type.Fun(arg, res) =>
Expand Down Expand Up @@ -740,9 +733,10 @@ object Infer {
def unifyTyApp(apType: Type.Rho, lKind: Kind, rKind: Kind, apRegion: Region, evidenceRegion: Region): Infer[(Type.Rho, Type)] =
apType match {
case ta @ Type.TyApply(left, right) =>
// this branch only happens when checking ta <:< (rho: lKind[rKind])
// TODO: it seems like we should be checking
// the kinds against lKind and rKind
// this branch only happens when checking ta <:< (rho: lKind[rKind]) or >:> (rho)
// TODO: what validates that ta has compatible kinds with lKind and rKind
// since we could be doing subtyping or supertyping here we would need
// to pass in some directionality
validateKinds(ta, apRegion).as((left, right))
case notApply =>
for {
Expand Down Expand Up @@ -1158,10 +1152,10 @@ object Infer {

validKinds.parProductR {
val remainingFree =
NonEmptyList.fromList(frees.iterator.map { case (_, (k, b)) =>
(b, k)
}
.toList)
NonEmptyList.fromList(
frees.iterator.map { case (_, (k, b)) => (b, k) }
.toList
)

remainingFree match {
case None =>
Expand All @@ -1172,7 +1166,16 @@ object Infer {
.map { argsTE =>
TypedExpr.App(fnTe, argsTE, tpe, tag)
}
case Some(remainingFree) =>

// $COVERAGE-OFF$
//case Some(remainingFree) =>
case Some(_) =>
// Currently we are only returning infOpt as Some when
// there are no remaining free variables due to unit
// tests not passing
sys.error("unreachable")
// $COVERAGE-ON$
/*
// some items are still free
// TODO we could use the args to try to fix these
val freeSub = frees.iterator
Expand All @@ -1187,6 +1190,7 @@ object Infer {
val fn1 = Expr.Annotation(fn, tpe1, fn.tag)
val inner = Expr.App(fn1, args, tag)
checkSigma(inner, tpe)
*/
}
}
case None =>
Expand Down
185 changes: 97 additions & 88 deletions core/src/main/scala/org/bykn/bosatsu/rankn/Type.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,19 @@ object Type {
case q: Quantified => freeTyVars(q :: Nil).isEmpty
}

def hasNoUnboundVars(t: Type): Boolean = {
def loop(t: Type, bound: Set[Var.Bound]): Boolean =
t match {
case TyVar(b: Var.Bound) => bound(b)
case _: Leaf => true
case TyApply(on, arg) => loop(on, bound) && loop(arg, bound)
case q: Quantified =>
loop(q.in, bound ++ q.vars.iterator.map(_._1))
}

loop(t, Set.empty)
}

final def forAll(vars: List[(Var.Bound, Kind)], in: Type): Type =
NonEmptyList.fromList(vars) match {
case None => in
Expand Down Expand Up @@ -477,77 +490,75 @@ object Type {
copy(fixed = fixed ++ keys)
}

// TODO: we could handle `to` being a ForAll as well
// by requiring some of the vars to stay free and correspond
// to free variables in to, but this code doesn't do that yet
def loop(from: Type, to: Type, state: State): Option[State] =
if (from.sameAs(to)) Some(state)
else {
from match {
case TyVar(b: Var.Bound) =>
state.get(b) match {
case Some((kind, opt)) =>
opt match {
case Unknown =>
to match {
case TyVar(toB: Var.Bound) =>
state.rightFrees.get(toB) match {
case Some(toBKind) =>
if (kind === toBKind) {
Some(state.updated(b, (kind, Free(toB))))
}
else None
case None =>
// not free, so treat as any type:
Some(state.updated(b, (kind, Fixed(to))))
}
case _ =>
if (Type.freeBoundTyVars(to :: Nil).isEmpty) {
Some(state.updated(b, (kind, Fixed(to))))
}
else None
}
case Fixed(set) =>
if (set.sameAs(to)) Some(state)
else None
case Free(rightName) =>
to match {
case TyVar(toB) if rightName == toB => Some(state)
case _ => None
}
}
case None =>
// not a variable, we can use, but also not the same as the right
from match {
case TyVar(b: Var.Bound) =>
state.get(b) match {
case Some((kind, opt)) =>
opt match {
case Unknown =>
to match {
case TyVar(toB: Var.Bound) =>
state.rightFrees.get(toB) match {
case Some(toBKind) =>
// TODO we could substitute to a compatible kind if
// we track it and return it correctly
if (kind === toBKind) {
Some(state.updated(b, (kind, Free(toB))))
}
else None
case None => None
// don't set to vars to non-free bound variables
// this shouldn't happen in real inference
}
case _ if hasNoUnboundVars(to) =>
Some(state.updated(b, (kind, Fixed(to))))
case _ => None
}
case Fixed(set) =>
if (set.sameAs(to)) Some(state)
else None
case Free(rightName) =>
to match {
case TyVar(toB) if rightName == toB => Some(state)
case _ => None
}
}
case None =>
// not a variable, we can use, but also not the same as the right
None
}
case TyApply(a, b) =>
to match {
case TyApply(ta, tb) =>
loop(a, ta, state).flatMap { s1 =>
loop(b, tb, s1)
}
case ForAll(rightFrees, rightT) =>
// TODO handle shadowing
if (rightFrees.exists { case (b, _) => state.rightFrees.contains(b) }) {
None
}
case TyApply(a, b) =>
to match {
case TyApply(ta, tb) =>
loop(a, ta, state).flatMap { s1 =>
loop(b, tb, s1)
}
case ForAll(rightFrees, rightT) =>
// TODO handle shadowing
if (rightFrees.exists { case (b, _) => state.rightFrees.contains(b) }) {
None
}
else {
loop(from,
rightT,
state.copy(rightFrees = state.rightFrees ++ rightFrees.iterator))
.map { s1 =>
s1.copy(rightFrees = state.rightFrees)
}
}
case _ => None
}
case ForAll(shadows, from1) =>
val noShadow = state -- shadows.iterator.map(_._1)
loop(from1, to, noShadow).map { s1 =>
s1 ++ shadows.iterator.flatMap { case (v, _) => state.get(v).map(v -> _) }
}
case _ => None
}
}
else {
loop(from,
rightT,
state.copy(rightFrees = state.rightFrees ++ rightFrees.iterator))
.map { s1 =>
s1.copy(rightFrees = state.rightFrees)
}
}
case _ => None
}
case ForAll(shadows, from1) =>
val noShadow = state -- shadows.iterator.map(_._1)
loop(from1, to, noShadow).map { s1 =>
s1 ++ shadows.iterator.flatMap { case (v, _) => state.get(v).map(v -> _) }
}
case _ =>
// We can't use sameAt to compare Var.Bound since we know the variances
// there
if (from.sameAs(to)) Some(state)
else None
}

val initState = State(
Expand Down Expand Up @@ -739,16 +750,23 @@ object Type {

private def predefFn(n: Int) = TyConst(Const.predef(s"Fn$n"))
private val tpes = (1 to MaxSize).map(predefFn)
private val fnMap: Map[TyConst, (TyConst, Int)] =
(1 to MaxSize).iterator.map { idx =>
val tyconst = tpes(idx - 1)
tyconst -> (tyconst, idx)
}
.toMap

object ValidArity {
def unapply(n: Int): Boolean =
(1 <= n) && (n <= MaxSize)
}

def apply(n: Int): Type.TyConst = {
require(ValidArity.unapply(n), s"invalid FnType arity = $n, must be 0 < n <= $MaxSize")
tpes(n - 1)
}
def apply(n: Int): Type.TyConst =
if (ValidArity.unapply(n)) tpes(n - 1)
else {
throw new IllegalArgumentException(s"invalid FnType arity = $n, must be 0 < n <= $MaxSize")
}

def maybeFakeName(n: Int): Type.TyConst =
if (n <= MaxSize) apply(n)
Expand All @@ -757,19 +775,11 @@ object Type {
predefFn(n)
}

def unapply(tpe: Type): Option[(Type.TyConst, Int)] = {
def unapply(tpe: Type): Option[(Type.TyConst, Int)] =
tpe match {
case Type.TyConst(Const.Predef(cons)) if (cons.asString.startsWith("Fn")) =>
var idx = 0
while (idx < MaxSize) {
val thisTpe = tpes(idx)
if (thisTpe == tpe) return Some((thisTpe, idx + 1))
idx = idx + 1
}
None
case tyConst @ Type.TyConst(_) => fnMap.get(tyConst)
case _ => None
}
}

// FnType -> Kind(Kind.Type.contra, Kind.Type.co),
val FnKinds: List[(Type.TyConst, Kind)] = {
Expand Down Expand Up @@ -830,13 +840,12 @@ object Type {
*/
object SimpleUniversal {
def unapply(t: Type): Option[
(NonEmptyList[(Type.Var.Bound, Kind)], NonEmptyList[Type], Type.Rho)
(NonEmptyList[(Type.Var.Bound, Kind)], NonEmptyList[Type], Type)
] =
t match {
case ForAll(univ, Fun(args, resT)) =>
resT match {
case res: Rho => Some((univ, args, res))
case ForAll(univR, res: Rho) =>
case ForAll(univR, res) =>
// we need to relabel univR if it intersects univ
val firstSet = univ.iterator.map(_._1).toSet
val intersects = univR.filter { case (b, _) => firstSet(b) }
Expand All @@ -855,10 +864,10 @@ object Type {
.toMap[Type.Var, Type.Rho]

val bounds = univ.concat(good) ::: rename.map { case ((_, k), b) => (b, k) }
val newRes = Type.substituteRhoVar(res, subMap)
val newRes = Type.substituteVar(res, subMap)
Some((bounds, args, newRes))
}
case _ => None
case res => Some((univ, args, res))
}
case _ => None
}
Expand Down
27 changes: 22 additions & 5 deletions core/src/test/scala/org/bykn/bosatsu/rankn/TypeTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,12 @@ class TypeTest extends AnyFunSuite {
}
}

test("if Type.hasNoUnboundVars then freeBoundTyVars is empty") {
forAll(NTypeGen.genDepth03) { t =>
assert(Type.hasNoUnboundVars(t) == Type.freeBoundTyVars(t :: Nil).isEmpty)
}
}

test("hasNoVars fully recurses") {
def allTypesIn(t: Type): List[Type] =
t match {
Expand Down Expand Up @@ -337,11 +343,15 @@ class TypeTest extends AnyFunSuite {
def check(forall: String, matches: String, subs: List[(String, String)]) = {
val Type.ForAll(fas, t) = parse(forall)
val targ = parse(matches)
val res = Type.instantiate(fas.iterator.toMap, t, targ)
assert(res.isDefined)
subs.foreach { case (k, v) =>
val Type.TyVar(b: Type.Var.Bound) = parse(k)
assert(res.get._2(b)._2 == parse(v))
Type.instantiate(fas.iterator.toMap, t, targ) match {
case Some((frees, subMap)) =>
assert(subMap.size == subs.size)
subs.foreach { case (k, v) =>
val Type.TyVar(b: Type.Var.Bound) = parse(k)
assert(subMap(b)._2 == parse(v))
}
case None =>
fail(s"could not instantitate: $forall to $matches")
}
}

Expand All @@ -367,7 +377,13 @@ class TypeTest extends AnyFunSuite {
check("forall a, b. a -> b", "forall c. c -> Bosatsu/Predef::Int",
List("b" -> "Bosatsu/Predef::Int"))

check("forall a, b. T::Cont[a, b]", "forall a. T::Cont[a, T::Foo]",
List("b" -> "T::Foo"))

noSub("forall a, b. T::Cont[a, b]", "forall a: * -> *. T::Cont[a, T::Foo]")
noSub("forall a. T::Box[a]", "forall a. T::Box[T::Opt[a]]")

check("forall a. T::Foo[a, a]", "forall b. T::Foo[b, b]", Nil)
}

test("Fun(ts, r) and Fun.unapply are inverses") {
Expand Down Expand Up @@ -496,6 +512,7 @@ class TypeTest extends AnyFunSuite {
check("forall a. a -> a", Some("forall a. a -> a"))
check("forall a. a -> Foo::Option[a]", Some("forall a. a -> Foo::Option[a]"))
check("forall a. a -> (forall b. b)", Some("forall a, b. a -> b"))
check("forall a. a -> (forall b. Foo::Option[b])", Some("forall a, b. a -> Foo::Option[b]"))
check("forall a. a -> (forall a. a)", Some("forall a, b. a -> b"))
check("forall a. a -> (forall a, c. a -> c)", Some("forall a, b, c. a -> (b -> c)"))
}
Expand Down

0 comments on commit 4fed9c5

Please sign in to comment.