Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Support for GADTs #195

Closed
wants to merge 95 commits into from
Closed
Show file tree
Hide file tree
Changes from 79 commits
Commits
Show all changes
95 commits
Select commit Hold shift + click to select a range
c4aa6d1
WIP Start implementing branch-local reasoning
LPTK Oct 3, 2023
261f9e0
refactor
Meowcolm024 Oct 5, 2023
816ea20
naive type member lookup
Meowcolm024 Oct 5, 2023
e7025e2
WIP type member partially works
Meowcolm024 Oct 16, 2023
6b2334e
WIP fixed name mangling ing TypeHelpers
Meowcolm024 Oct 17, 2023
5f18602
WIP refactor
Meowcolm024 Oct 17, 2023
b7e1bc7
TODO wildcard type and refinement
Meowcolm024 Oct 20, 2023
55eaa2a
added `as` keyword
Meowcolm024 Oct 25, 2023
270a859
WIP wildcard types
Meowcolm024 Oct 25, 2023
e201914
WIP
Meowcolm024 Nov 1, 2023
9566694
WIP
Meowcolm024 Nov 1, 2023
957b966
WIP added :GADTs flag
Meowcolm024 Nov 1, 2023
88b1af4
added GADT examples
Meowcolm024 Nov 3, 2023
ce83f9b
WIP update examples
Meowcolm024 Nov 3, 2023
cdf0f04
added some GADT examples
Meowcolm024 Nov 3, 2023
37a9de7
updated some examples and added some notes
Meowcolm024 Nov 3, 2023
570f3d7
WIP update tests
Meowcolm024 Nov 10, 2023
cb89a08
WIP
Meowcolm024 Nov 10, 2023
5150f53
Add an interesting test
LPTK Nov 10, 2023
28a831c
WIP move cache to ctx
Meowcolm024 Nov 17, 2023
aecd07e
Merge branch 'local-gadt' of github.com:Meowcolm024/mlscript into loc…
Meowcolm024 Nov 17, 2023
1e5b030
annot to trigger GADTs
Meowcolm024 Nov 28, 2023
1e87c13
clean up tests
Meowcolm024 Nov 28, 2023
3293b58
Merge remote-tracking branch 'hkust-taco/new-definition-typing' into …
Meowcolm024 Nov 28, 2023
a30e27d
clean up
Meowcolm024 Nov 28, 2023
a6c5451
fix lift
Meowcolm024 Nov 28, 2023
fa04070
add keyword "as" for asc
Meowcolm024 Dec 22, 2023
ecfde50
Merge remote-tracking branch 'hkust-taco/new-definition-typing' into …
Meowcolm024 Dec 27, 2023
13a0e85
cleanup
Meowcolm024 Dec 27, 2023
9f5d9b9
add more test cases
Meowcolm024 Dec 27, 2023
53e1352
Merge branch 'new-definition-typing' into local-gadt
Meowcolm024 Jan 3, 2024
ac25d4e
small test case change
Meowcolm024 Jan 3, 2024
6bfad52
add variance in type members decl
Meowcolm024 Jan 4, 2024
3104598
Merge branch 'new-definition-typing' into local-gadt
Meowcolm024 Jan 4, 2024
6c5975d
added more tests
Meowcolm024 Jan 4, 2024
fbd709f
added some multi param type tests
Meowcolm024 Jan 4, 2024
b77b47b
Merge remote-tracking branch 'origin/new-definition-typing' into loca…
Meowcolm024 Jan 15, 2024
e7b2c4c
wip
Meowcolm024 Jan 16, 2024
9c5e2c5
wip
Meowcolm024 Jan 17, 2024
2f193c8
WIP Prepare the grounds for SimpleTypeOrWildcard
LPTK Feb 2, 2024
f52774b
Fix bug in extrusion (extruded assigned TV level) and hack around pro…
LPTK Feb 2, 2024
1bb4b2d
wip
Meowcolm024 Feb 2, 2024
a017daa
Merge remote-tracking branch 'lptk/local-gadt-wip' into local-gadt-wip
Meowcolm024 Feb 2, 2024
61e8319
wip
Meowcolm024 Feb 2, 2024
e0c09ca
WIP wildcard
Meowcolm024 Feb 5, 2024
7868b3d
add more tests
Meowcolm024 Feb 5, 2024
2a633d2
wip: fixed some tests
Meowcolm024 Feb 6, 2024
17e8491
Add current type projection unsoundness example
LPTK Feb 3, 2024
f0b84c0
Push ascriptions inside branches for better type checking
LPTK Feb 7, 2024
9b73514
fixed parens
Meowcolm024 Feb 7, 2024
4f72058
wip err msg
Meowcolm024 Feb 7, 2024
80476ef
Minor: remove TODO
LPTK Feb 7, 2024
bb437ea
Fix freak condition in freshening
LPTK Feb 7, 2024
e4bff8c
Merge branch 'mlscript' into local-gadt (one test now fails)
LPTK Feb 7, 2024
dce34e4
Make test green; not sure why it now fails
LPTK Feb 7, 2024
462804a
wip various fixed
Meowcolm024 Feb 8, 2024
c6491bd
WIP correct polarity/variance treatment of WildcardArg
Meowcolm024 Feb 8, 2024
db7f38a
WIP Move towards a correct handling of WildcardArg
LPTK Feb 8, 2024
8ee5a84
Add alias GADT use case
LPTK Feb 13, 2024
4b129aa
various small fixes
Meowcolm024 Feb 14, 2024
79e3f0f
change typing of type member alias
Meowcolm024 Feb 14, 2024
8defef6
implement parser for type argument bounds
Meowcolm024 Feb 14, 2024
05b68c0
small format fix
Meowcolm024 Feb 16, 2024
73d970a
WIP added test case similar to the zip one
Meowcolm024 Feb 17, 2024
f8784ac
wip change tag checking in <:< for LhsNf
Meowcolm024 Feb 26, 2024
0f9e788
wip: self type sig issue
Meowcolm024 Feb 26, 2024
7a0353f
WIP early finish some dnfs
Meowcolm024 Feb 28, 2024
cf228b0
wip change extr type args
Meowcolm024 Feb 29, 2024
4f24921
add prov for wildcard
Meowcolm024 Mar 1, 2024
6e6b9a1
WIP refactor wildcard
Meowcolm024 Mar 4, 2024
a7e3b94
WIP fix various crashes
Meowcolm024 Mar 4, 2024
625fafe
WIP fix standalone wildcard typing
Meowcolm024 Mar 4, 2024
3c05aee
wip expand alias issue
Meowcolm024 Mar 4, 2024
e13bff7
wip fix pol
Meowcolm024 Mar 5, 2024
71d9232
wip fix alias ty arg extursion
Meowcolm024 Mar 5, 2024
0b766ce
wip early finish dnf solving for other tags
Meowcolm024 Mar 5, 2024
e667617
wip fix extr for alias and updated some tests
Meowcolm024 Mar 5, 2024
2b27281
small fix
Meowcolm024 Mar 6, 2024
2bc5cf8
simple level indexed extrusion cache
Meowcolm024 Mar 6, 2024
d268965
WIP replace incorrect use of mapTargs and avoid level-mismatched cons…
LPTK Mar 15, 2024
031f611
WW
LPTK Mar 15, 2024
95f4cb7
WWW
LPTK Mar 15, 2024
60c4b74
WWW
LPTK Mar 15, 2024
ab4b456
WWW
LPTK Mar 15, 2024
27c2354
WWW
LPTK Mar 15, 2024
ab2fe6b
WW
LPTK Mar 15, 2024
03044b8
WW fix extruded compare
LPTK Mar 15, 2024
2f636e5
W simplify YC's mess
LPTK Mar 15, 2024
7b89780
WWW trial
LPTK Mar 15, 2024
95a3620
W
LPTK Mar 16, 2024
54ba6ad
W
LPTK Mar 18, 2024
db2fb45
Minor
LPTK Apr 2, 2024
e24d01e
Merge remote-tracking branch 'origin/mlscript' into local-gadt
Meowcolm024 Apr 9, 2024
064f004
add some test cases
Meowcolm024 Apr 12, 2024
9ef9425
fix some test cases
Meowcolm024 Apr 23, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -741,7 +741,7 @@ class ClassLifter(logDebugMsg: Boolean = false) {
val nTerms = termList.map(liftTerm(_)(using emptyCtx, nCache, globFuncs, nOuter)).unzip
clsList.foreach(x => liftTypeDef(x)(using nCache, globFuncs, nOuter))
retSeq = retSeq.appended(NuTypeDef(
kind, nName, nTps.map((None, _)), S(Tup(nParams)), None, None, nPars._1,
kind, nName, nTps.map((TypeParamInfo(None, false, N, N), _)), S(Tup(nParams)), None, None, nPars._1,
None, None, TypingUnit(nFuncs._1 ++ nTerms._1))(None, None))
}

Expand Down
155 changes: 110 additions & 45 deletions shared/src/main/scala/mlscript/ConstraintSolver.scala

Large diffs are not rendered by default.

5 changes: 3 additions & 2 deletions shared/src/main/scala/mlscript/NewLexer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -408,7 +408,7 @@ object NewLexer {
"val",
"var",
// "is",
// "as",
"as",
"of",
// "and",
// "or",
Expand Down Expand Up @@ -442,7 +442,8 @@ object NewLexer {
"undefined",
"abstract",
"constructor",
"virtual"
"virtual",
"restricts",
)

def printToken(tl: TokLoc): Str = tl match {
Expand Down
51 changes: 39 additions & 12 deletions shared/src/main/scala/mlscript/NewParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -646,6 +646,9 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo
case (KEYWORD("super"), l0) :: _ =>
consume
exprCont(Super().withLoc(S(l0)), prec, allowNewlines = false)
case (IDENT("?", true), l0) :: _ =>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do you need a special case for this?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removing it will cause unexpected operator in parsing

consume
exprCont(Var("?").withLoc(S(l0)), prec, allowNewlines = false)
case (IDENT("~", _), l0) :: _ =>
consume
val rest = expr(prec, allowSpace = true)
Expand Down Expand Up @@ -910,7 +913,7 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo
else App(App(v, PlainTup(acc)), PlainTup(rhs))
}, prec, allowNewlines)
}
case (KEYWORD(":"), l0) :: _ if prec <= NewParser.prec(':') =>
case (KEYWORD("as" | ":"), l0) :: _ if prec <= NewParser.prec(':') =>
consume
R(Asc(acc, typ(0)))
case (KEYWORD("where"), l0) :: _ if prec <= 1 =>
Expand Down Expand Up @@ -1108,35 +1111,59 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo
}

// TODO support line-broken param lists; share logic with args/argsOrIf
def typeParams(implicit fe: FoundErr, et: ExpectThen): Ls[(Opt[VarianceInfo], TypeName)] = {
def typeParams(implicit fe: FoundErr, et: ExpectThen): Ls[(TypeParamInfo, TypeName)] = {
val visinfo = yeetSpaces match {
case (KEYWORD("type"), l0) :: _ =>
consume
S(l0)
case _ => N
}
val vinfo = yeetSpaces match {
Meowcolm024 marked this conversation as resolved.
Show resolved Hide resolved
case (KEYWORD("in"), l0) :: (KEYWORD("out"), l1) :: _ =>
consume
S(VarianceInfo.in, l0 ++ l1)
S(VarianceInfo.in -> (l0++l1))
case (KEYWORD("in"), l0) :: _ =>
consume
S(VarianceInfo.contra, l0)
S(VarianceInfo.contra -> l0)
case (KEYWORD("out"), l0) :: _ =>
consume
S(VarianceInfo.co, l0)
case _ => N
S(VarianceInfo.co -> l0)
case _ =>
N
}
yeetSpaces match {
case (IDENT(nme, false), l0) :: _ =>
consume
val tyNme = TypeName(nme).withLoc(S(l0))

@inline def getTypeName(kw: String) = yeetSpaces match {
case (KEYWORD(k), l0) :: _ if k === kw => consume
yeetSpaces match {
case (IDENT(nme, false), l1) :: _ =>
consume; S(TypeName(nme).withLoc(S(l1)))
case _ => err(msg"dangling $kw keyword" -> S(l0) :: Nil); N
}
case _ => N
}
val lb = getTypeName("restricts")
val ub = getTypeName("extends")
// TODO update `TypeParamInfo` to use lb and ub
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO

yeetSpaces match {
case (COMMA, l0) :: _ =>
consume
vinfo.map(_._1) -> tyNme :: typeParams
TypeParamInfo(vinfo.map(_._1), visinfo.isDefined, lb, ub) -> tyNme :: typeParams
case _ =>
vinfo.map(_._1) -> tyNme :: Nil
TypeParamInfo(vinfo.map(_._1), visinfo.isDefined, lb, ub) -> tyNme :: Nil
}
case _ =>
vinfo match {
case S((_, loc)) =>
(visinfo, vinfo) match {
case (S(l1), S(_ -> l2)) =>
err(msg"dangling type member and variance information" -> S(l1 ++ l2) :: Nil)
case (_, S(_ -> loc)) =>
err(msg"dangling variance information" -> S(loc) :: Nil)
case N =>
case (S(loc), _) =>
err(msg"dangling visible type member" -> S(loc) :: Nil)
Meowcolm024 marked this conversation as resolved.
Show resolved Hide resolved
case (N, N) =>
}
Nil
}
Expand Down Expand Up @@ -1203,7 +1230,7 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo
case (NEWLINE, _) :: _ => // TODO: | ...
assert(seqAcc.isEmpty)
acc.reverse
case (IDENT(nme, true), _) :: _ if nme =/= "-" => // TODO: | ...
case (IDENT(nme, true), _) :: _ if nme =/= "-" && nme =/= "?" => // TODO: | ...
assert(seqAcc.isEmpty)
acc.reverse
case _ =>
Expand Down
71 changes: 55 additions & 16 deletions shared/src/main/scala/mlscript/NormalForms.scala
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,13 @@ class NormalForms extends TyperDatatypes { self: Typer =>
mergeSortedMap(trs1, trs2) { (tr1, tr2) =>
assert(tr1.defn === tr2.defn)
assert(tr1.targs.size === tr2.targs.size)
TypeRef(tr1.defn, (tr1.targs lazyZip tr2.targs).map((ta1, ta2) =>
if (pol) TypeBounds.mk(ta1 & ta2, ta1 | ta2) else TypeBounds.mk(ta1 | ta2, ta1 & ta2)
))(noProv)
TypeRef(tr1.defn, (tr1.targs lazyZip tr2.targs).map {
case (l: WildcardArg, r: WildcardArg) =>
if (pol) WildcardArg.mk(l.lb | r.lb, l.ub & r.ub) else WildcardArg.mk(l.lb & r.lb, l.ub | r.ub)
case (l: WildcardArg, r: ST) => if (pol) WildcardArg.mk(l.lb | r, l.ub & r) else WildcardArg.mk(l.lb & r, l.ub | r)
case (l: ST, r: WildcardArg) => if (pol) WildcardArg.mk(l | r.lb, l & r.ub) else WildcardArg.mk(l & r.lb, l | r.ub)
case (l: ST, r: ST) => if (pol) WildcardArg.mk(l | r, l & r) else WildcardArg.mk(l & r, l | r)
})(noProv)
}


Expand Down Expand Up @@ -196,11 +200,25 @@ class NormalForms extends TyperDatatypes { self: Typer =>
val thatTarg = thatTargs.head
thatTargs = thatTargs.tail
vce match {
case S(true) => otherTarg & thatTarg
case S(false) => otherTarg | thatTarg
case N =>
if (pol) TypeBounds.mk(otherTarg | thatTarg, otherTarg & thatTarg)
else TypeBounds.mk(otherTarg & thatTarg, otherTarg | thatTarg)
case S(true) => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) => WildcardArg.mk(l.lb | r.lb, l.ub & r.ub)
case (l: WildcardArg, r: ST) => l.ub & r
case (l: ST, r: WildcardArg) => l & r.ub
case (l: ST, r: ST) => l & r
}
case S(false) => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) => WildcardArg.mk(l.lb & r.lb, l.ub | r.ub)
case (l: WildcardArg, r: ST) => l.lb | r
case (l: ST, r: WildcardArg) => l | r.lb
case (l: ST, r: ST) => l | r
}
case N => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) =>
if (pol) WildcardArg.mk(l.lb | r.lb, l.ub & r.ub) else WildcardArg.mk(l.lb & r.lb, l.ub | r.ub)
case (l: WildcardArg, r: ST) => if (pol) WildcardArg.mk(l.lb | r, l.ub & r) else WildcardArg.mk(l.lb & r, l.ub | r)
case (l: ST, r: WildcardArg) => if (pol) WildcardArg.mk(l | r.lb, l & r.ub) else WildcardArg.mk(l & r.lb, l | r.ub)
case (l: ST, r: ST) => if (pol) WildcardArg.mk(l | r, l & r) else WildcardArg.mk(l & r, l | r)
}
}
}
TypeRef(that.defn, newTargs)(that.prov)
Expand Down Expand Up @@ -241,7 +259,14 @@ class NormalForms extends TyperDatatypes { self: Typer =>
case (LhsTop, _) => false
case (LhsRefined(b1, ts1, rt1, trs1), LhsRefined(b2, ts2, rt2, trs2)) =>
b2.forall(b2 => b1.exists(_ <:< b2)) &&
ts2.forall(ts1) && rt1 <:< rt2 &&
ts2.forall {
case sk: SkolemTag => ts1(sk)
case tt: TraitTag => ts1(tt)
case Extruded(pol, sk) => !pol || ts1.exists { // find ? <: bot
case Extruded(true, _) => true
case _ => false
}
} && rt1 <:< rt2 &&
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This thing looks very fishy. What is going on here? Why don't we use the normal set functions?

trs2.valuesIterator.forall(tr2 => trs1.valuesIterator.exists(_ <:< tr2))
}
def isTop: Bool = isInstanceOf[LhsTop.type]
Expand Down Expand Up @@ -294,11 +319,25 @@ class NormalForms extends TyperDatatypes { self: Typer =>
val thatTarg = thatTargs.head
thatTargs = thatTargs.tail
vce match {
case S(true) => otherTarg | thatTarg
case S(false) => otherTarg & thatTarg
case N =>
if (pol) TypeBounds.mk(otherTarg & thatTarg, otherTarg | thatTarg)
else TypeBounds.mk(otherTarg | thatTarg, otherTarg & thatTarg)
case S(true) => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) => WildcardArg.mk(l.lb & r.lb, l.ub | r.ub)
case (l: WildcardArg, r: ST) => l.lb | r
case (l: ST, r: WildcardArg) => l | r.lb
case (l: ST, r: ST) => l | r
}
case S(false) => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) => WildcardArg.mk(l.lb | r.lb, l.ub & r.ub)
case (l: WildcardArg, r: ST) => l.ub & r
case (l: ST, r: WildcardArg) => l & r.ub
case (l: ST, r: ST) => l & r
}
case N => (otherTarg, thatTarg) match {
case (l: WildcardArg, r: WildcardArg) =>
if (pol) WildcardArg.mk(l.lb & r.lb, l.ub | r.ub) else WildcardArg.mk(l.lb | r.lb, l.ub & r.ub)
case (l: WildcardArg, r: ST) => if (pol) WildcardArg.mk(l.lb & r, l.ub | r) else WildcardArg.mk(l.lb | r, l.ub & r)
case (l: ST, r: WildcardArg) => if (pol) WildcardArg.mk(l & r.lb, l | r.ub) else WildcardArg.mk(l | r.lb, l & r.ub)
case (l: ST, r: ST) => if (pol) WildcardArg.mk(l & r, l | r) else WildcardArg.mk(l | r, l & r)
}
}
}
TypeRef(that.defn, newTargs)(that.prov)
Expand Down Expand Up @@ -760,7 +799,7 @@ class NormalForms extends TyperDatatypes { self: Typer =>
// * TODO later: when proper TypeRef-based simplif. is implemented, can remove this special case
if (preserveTypeRefs && !primitiveTypes.contains(defn.name) || !tr.canExpand) {
of(polymLvl, cons, LhsRefined(tr.mkClsTag, ssEmp, RecordType.empty, SortedMap(defn -> tr)))
} else mk(polymLvl, cons, tr.expandOrCrash, pol)
} else mk(polymLvl, cons, tr.expandOrCrash(pol), pol)
case TypeBounds(lb, ub) => mk(polymLvl, cons, if (pol) ub else lb, pol)
case PolymorphicType(lvl, bod) => mk(lvl, cons, bod, pol)
case ConstrainedType(cs, bod) => mk(polymLvl, cs ::: cons, bod, pol)
Expand Down Expand Up @@ -804,7 +843,7 @@ class NormalForms extends TyperDatatypes { self: Typer =>
case tr @ TypeRef(defn, targs) =>
if (preserveTypeRefs && !primitiveTypes.contains(defn.name) || !tr.canExpand) {
CNF(Disjunct(RhsBases(Nil, N, SortedMap.single(defn -> tr)), ssEmp, LhsTop, ssEmp) :: Nil)
} else mk(polymLvl, cons, tr.expandOrCrash, pol)
} else mk(polymLvl, cons, tr.expandOrCrash(pol), pol)
case TypeBounds(lb, ub) => mk(polymLvl, cons, if (pol) ub else lb, pol)
case PolymorphicType(lvl, bod) => mk(lvl, cons, bod, pol)
case ConstrainedType(cs, bod) => mk(lvl, cs ::: cons, bod, pol)
Expand Down
Loading