-
-
Notifications
You must be signed in to change notification settings - Fork 40
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
Type unification for rows, new records, and variants #1646
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1646 +/- ##
============================================
+ Coverage 74.96% 75.15% +0.19%
============================================
Files 358 358
Lines 11612 11654 +42
Branches 541 569 +28
============================================
+ Hits 8705 8759 +54
+ Misses 2907 2895 -12
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I feel this is a little harder to follow than it should be. I had to look back at some previous PR to remember the relation between RecRow
and Row
. I still believe that introducing a different kind than TlaType1
would make this relation clearer in the code. I'm fine with keeping things like this for now, but I would like to try an approach with kinds on TNT and then, if it's clearer, we can copy it to apalache or something like that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
👍
val maxUsedVar = Math.max(genericType.usedNames.foldLeft(0)(Math.max), targetType.usedNames.foldLeft(0)(Math.max)) | ||
new TypeUnifier(new TypeVarPool(maxUsedVar + 1)).unify(Substitution.empty, genericType, targetType) match { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Huh, was there a case where type-var name IDs were causing problems?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes. We had it a month or two ago.
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeUnifier.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeUnifier.scala
Outdated
Show resolved
Hide resolved
// the base case | ||
(lvar, rvar) match { | ||
case (None, None) => | ||
if (rfields.nonEmpty) None else Some(RowT1()) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As an aside, I really don't like how object RowT1
methods are all apply
, because it makes it hard to track what is actually being constructed, since RowT1(), RowT1(_), RowT1(_,_)
are all different methods that return a RowT1
.
if ( | ||
compute(lvar.getOrElse(RowT1()), RowT1(rfields, Some(tailVar))).isEmpty | ||
|| compute(rvar.getOrElse(RowT1()), RowT1(lfields, Some(tailVar))).isEmpty | ||
) { | ||
None | ||
} else { | ||
// apply the computed substitution to obtain the whole row | ||
asRow(Some(Substitution(solution).sub(RowT1(lfields, lvar))._1)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The fact that compute
mutates solution
internally makes this really hard to understand. I'd at least appreciate a comment on that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, if you don't need the substitution, it does unify things. But since we need the resulting substitution, compute
mutates the substitution pretty much everywhere.
Co-authored-by: Kukovec <jure.kukovec@gmail.com>
Closes #1622. This PR implements type unification for rows as part of the meta-issue #401. Unification for new records and variants is very simple: It delegates to row unification. The idea is described in ADR014. However, our unification is much simpler. We do not need kinds, scoped labels, etc.
This version does not require different options of a variant type to have compatible fields, as discussed in Section 5.4. Postponing this decision until implementing the rewriting rules in the model checker. Perhaps, we do not need this requirement.
make fmt-fix
(or had formatting run automatically on all files edited)