Skip to content

Commit

Permalink
address some things noticed in review
Browse files Browse the repository at this point in the history
  • Loading branch information
@johnynek
johnynek committed Nov 22, 2023
1 parent 30c99c3 commit b28b023
Show file tree
Hide file tree
Showing 9 changed files with 106 additions and 111 deletions.
20 changes: 9 additions & 11 deletions cli/src/main/protobuf/bosatsu/TypedAst.proto
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,19 @@ message TypeVar {
int32 varName = 1;
}

message VarKind {
int32 varName = 1;
Kind kind = 2;
}

message TypeForAll {
repeated int32 varNames = 1;
repeated Kind kinds = 2;
int32 typeValue = 3;
repeated VarKind varKinds = 1;
int32 typeValue = 2;
}

message TypeExists {
repeated int32 varNames = 1;
repeated Kind kinds = 2;
int32 typeValue = 3;
repeated VarKind varKinds = 1;
int32 typeValue = 2;
}

// represents left[right] type application
Expand Down Expand Up @@ -160,11 +163,6 @@ enum RecursionKind {
IsRec = 1;
}

message VarKind {
int32 varName = 1;
Kind kind = 2;
}

message GenericExpr {
repeated VarKind forAlls = 1;
repeated VarKind exists = 2;
Expand Down
57 changes: 26 additions & 31 deletions cli/src/main/scala/org/bykn/bosatsu/TypedExprToProto.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,10 @@ object ProtoConverter {
def str(i: Int): Try[String] =
ds.tryString(i - 1, s"invalid string idx: $i in $p")

def varKindFromProto(vk: proto.VarKind) =
(str(vk.varName), kindFromProto(vk.kind))
.mapN { (n, k) => (Type.Var.Bound(n), k) }

p.value match {
case Value.Empty => Failure(new Exception(s"empty type found in $p"))
case Value.TypeConst(tc) =>
Expand All @@ -251,25 +255,17 @@ object ProtoConverter {
}
case Value.TypeVar(tv) =>
str(tv.varName).map { n => Type.TyVar(Type.Var.Bound(n)) }
case Value.TypeForAll(TypeForAll(args, kinds, in, _)) =>
if (args.length != kinds.length)
Failure(new Exception(s"args and kinds len mismatch: $p"))
else
for {
inT <- tpe(in)
args <- args.toList.traverse(str(_).map(Type.Var.Bound(_)))
kinds <- kinds.traverse { k => kindFromProto(Some(k)) }
} yield Type.forAll(args.zip(kinds), inT)

case Value.TypeExists(TypeExists(args, kinds, in, _)) =>
if (args.length != kinds.length)
Failure(new Exception(s"args and kinds len mismatch: $p"))
else
for {
inT <- tpe(in)
args <- args.toList.traverse(str(_).map(Type.Var.Bound(_)))
kinds <- kinds.traverse { k => kindFromProto(Some(k)) }
} yield Type.exists(args.zip(kinds), inT)
case Value.TypeForAll(TypeForAll(varKinds, in, _)) =>
for {
inT <- tpe(in)
args <- varKinds.toList.traverse(varKindFromProto)
} yield Type.forAll(args, inT)

case Value.TypeExists(TypeExists(varKinds, in, _)) =>
for {
inT <- tpe(in)
args <- varKinds.toList.traverse(varKindFromProto)
} yield Type.exists(args, inT)

case Value.TypeApply(TypeApply(left, right, _)) =>
(tpe(left), tpe(right)).mapN(Type.TyApply(_, _))
Expand Down Expand Up @@ -521,26 +517,24 @@ object ProtoConverter {
val foralls = q.forallList
val exs = q.existList
val in = q.in
(foralls.traverse { case (b, _) => getId(b.name) },
exs.traverse { case (b, _) => getId(b.name) },
(foralls.traverse { case (b, k) => varKindToProto(b, k) },
exs.traverse { case (b, k) => varKindToProto(b, k) },
typeToProto(in))
.flatMapN { (faids, exids, idx) =>
val ft0 =
if (exs.nonEmpty) {
val eks = exs.map { case (_, k) => kindToProto(k) }
val withEx = Type.exists(exs, in)
getTypeId(withEx,
proto.Type(
Value.TypeExists(TypeExists(exids, eks, idx))))
Value.TypeExists(TypeExists(exids, idx))))
}
else tabPure(idx)

ft0.flatMap { t0 =>
if (foralls.nonEmpty) {
val fks = foralls.map { case (_, k) => kindToProto(k) }
getTypeId(p,
proto.Type(
Value.TypeForAll(TypeForAll(faids, fks, t0))))
Value.TypeForAll(TypeForAll(faids, t0))))
}
else tabPure(t0)
}
Expand Down Expand Up @@ -689,6 +683,11 @@ object ProtoConverter {
}
}

def varKindToProto(v: Type.Var.Bound, k: Kind): Tab[proto.VarKind] =
getId(v.name).map { id =>
proto.VarKind(id, Some(kindToProto(k)))
}

def typedExprToProto(te: TypedExpr[Any]): Tab[Int] =
StateT.get[Try, SerState]
.map(_.expressions.indexOf(te))
Expand All @@ -699,14 +698,10 @@ object ProtoConverter {
te match {
case g@Generic(quant, expr) =>
val fas = quant.forallList.traverse { case (v, k) =>
getId(v.name).map { id =>
proto.VarKind(id, Some(kindToProto(k)))
}
varKindToProto(v, k)
}
val exs = quant.existList.traverse { case (v, k) =>
getId(v.name).map { id =>
proto.VarKind(id, Some(kindToProto(k)))
}
varKindToProto(v, k)
}
(fas, exs, typedExprToProto(expr))
.flatMapN { (fas, exs, exid) =>
Expand Down
4 changes: 2 additions & 2 deletions core/src/main/scala/org/bykn/bosatsu/TypeParser.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,12 +36,12 @@ abstract class TypeParser[A] {
lowerIdent ~ kindP.?
}

val univLike: P[(NonEmptyList[(String, Option[Kind])], A) => A] =
val quantified: P[(NonEmptyList[(String, Option[Kind])], A) => A] =
keySpace("forall").as(universal(_, _)) |
keySpace("exists").as(existential(_, _))

val lambda: P[MaybeTupleOrParens[A]] =
(univLike, univItem.nonEmptyListOfWs(maybeSpacesAndLines) ~ (maybeSpacesAndLines *> P.char('.') *> maybeSpacesAndLines *> recurse))
(quantified, univItem.nonEmptyListOfWs(maybeSpacesAndLines) ~ (maybeSpacesAndLines *> P.char('.') *> maybeSpacesAndLines *> recurse))
.mapN { case (fn, (args, e)) => MaybeTupleOrParens.Bare(fn(args, e)) }

val tupleOrParens: P[MaybeTupleOrParens[A]] =
Expand Down
19 changes: 5 additions & 14 deletions core/src/main/scala/org/bykn/bosatsu/TypedExpr.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ object TypedExpr {
case _ => None
}

private[this] var emptyBound: SortedSet[Type.Var.Bound] =
private[this] val emptyBound: SortedSet[Type.Var.Bound] =
SortedSet.empty

implicit class InvariantTypedExpr[A](val self: TypedExpr[A]) extends AnyVal {
Expand Down Expand Up @@ -458,9 +458,7 @@ object TypedExpr {
.mapN { (typeArgs, r) =>
val forAlls = typeArgs.collect { case (nk, false) => nk }
val exists = typeArgs.collect { case (nk, true) => nk }
val q = quantVars(forallList = forAlls, existList = exists, r)
//println(s"forAlls = $forAlls exists = $exists ${r.repr} quantVars = ${q.repr}")
q
quantVars(forallList = forAlls, existList = exists, r)
}
}

Expand All @@ -470,7 +468,6 @@ object TypedExpr {
for {
envTypeVars <- getMetaTyVars(envList)
localMetas = metas.diff(envTypeVars)
//_ = println(s"localMetas = $localMetas in ${te.repr}")
q <- quantify0(localMetas.toList, te)
} yield q
}
Expand All @@ -479,6 +476,7 @@ object TypedExpr {
// this is lazy because we only evaluate it if there is an existential skolem
lazy val envList = env.toList
lazy val envExistSkols = Type.freeTyVars(envList)
.iterator
.collect {
case ex @ Skolem(_, _, true, _) => ex
}
Expand Down Expand Up @@ -510,12 +508,6 @@ object TypedExpr {

getMetaTyVars(te1.allTypes.toList)
.flatMap(quantifyMetas(envList, _, te1))
/*
.map { res =>
println(s"quantifyFree, teSkols=${teSkols} ${te.repr} => ${te1.repr} => ${res.repr}")
res
}
*/
}

/*
Expand All @@ -530,7 +522,6 @@ object TypedExpr {
def deepQuantify(env: Set[Type], te: TypedExpr[A]): F[TypedExpr[A]] =
quantifyFree(env, te).flatMap {
case Generic(quant, in) =>
//assert(te != in, s"${te.repr} quantifyFree => ${in.repr}")
deepQuantify(env + te.getType, in).map { in1 =>
quantVars(quant.forallList, quant.existList, in1)
}
Expand Down Expand Up @@ -603,10 +594,10 @@ object TypedExpr {
deepQuantify(env1, arg).map(Match(_, branches, tag))
case Generic(quants, expr) =>
finish(expr).map(quantVars(quants.forallList, quants.existList, _))
// $COVERAGE-OFF$
case unreach =>
// $COVERAGE-OFF$
sys.error(s"Match quantification yielded neither Generic nor Match: $unreach")
// $COVERAGE-ON$
// $COVERAGE-ON$
}

noArg.flatMap(finish)
Expand Down
Loading

0 comments on commit b28b023

Please sign in to comment.