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.

Sign up for GitHub

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

Jump to bottom

Unify in-scope name types #2635

Merged
merged 4 commits into from
Jul 6, 2023
Merged

Unify in-scope name types #2635

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
937358e
Unify in-scope name types
thpani Jul 6, 2023
6e5478c
Update changelog
thpani Jul 6, 2023
0d10230
Merge branch 'main' into th/builder-name-unify
thpani Jul 6, 2023
afa6555
Merge branch 'main' into th/builder-name-unify
apalache-bot Jul 6, 2023
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
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/2635-unify-name-expr.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Fix a typing issue when translating Quint name expressions, see #2635
23 changes: 15 additions & 8 deletions tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ package at.forsyte.apalache.tla.typecomp.subbuilder
import at.forsyte.apalache.tla.lir._
import at.forsyte.apalache.tla.typecomp._
import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeLiteralAndNameBuilder
import at.forsyte.apalache.tla.types.{Substitution, TypeUnifier, TypeVarPool}
import scalaz.Scalaz._
import scalaz._

Expand Down Expand Up @@ -58,16 +59,22 @@ trait LiteralAndNameBuilder {
def name(exprName: String, t: TlaType1): TBuilderInstruction = State[TBuilderContext, TlaEx] { mi =>
val scope = mi.freeNameScope

// If already in scope, type must be the same
scope.get(exprName).foreach { tt =>
if (tt != t)
throw new TBuilderScopeException(
s"Name $exprName with type $t constructed in scope where expected type is $tt."
)
// If already in scope, type must be unifiable
val unifT = scope.get(exprName).map { tt =>
val unifOpt = new TypeUnifier(new TypeVarPool()).unify(Substitution.empty, tt, t)
unifOpt match {
case Some((_, unifiedOperT)) => unifiedOperT
case None =>
throw new TBuilderScopeException(
s"Name $exprName with type $t constructed in scope where expected type is $tt."
)
}
}
// If not in scope, just use `t`
val finalT = unifT.getOrElse(t)

val ret = unsafeBuilder.name(exprName, t)
(mi.copy(freeNameScope = scope + (exprName -> t), usedNames = mi.usedNames + exprName), ret)
val ret = unsafeBuilder.name(exprName, finalT)
(mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret)
}

/** Attempt to infer the type from the scope. Fails if exprName is not in scope. */
Expand Down