Skip to content

Commit

Permalink
can import consts from specs
Browse files Browse the repository at this point in the history
  • Loading branch information
mkurnikov committed Feb 17, 2025
1 parent 03b67df commit 7f8cf6a
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 3 deletions.
3 changes: 0 additions & 3 deletions src/main/kotlin/org/move/lang/core/psi/ext/MvElement.kt
Original file line number Diff line number Diff line change
Expand Up @@ -76,9 +76,6 @@ private fun PsiElement.isMslInner(): Boolean {
return CachedValuesManager.getProjectPsiDependentCache(this) {
var element: PsiElement? = it
while (element != null) {
// use items always non-msl, otherwise import resolution doesn't work correctly
if (element is MvUseSpeck) return@getProjectPsiDependentCache false

// module items
if (element is MvModule
|| element is MvFunction
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -597,4 +597,18 @@ module 0x1::m {
}
}
""")

fun `test no unresolved reference for const in spec`() = checkByText("""
module 0x1::features {
const PERMISSIONED_SIGNER: u64 = 84;
}
module 0x1::m {}
spec 0x1::m {
spec fun is_permissioned_signer(): bool {
use 0x1::features::PERMISSIONED_SIGNER;
PERMISSIONED_SIGNER;
}
}
""")
}
15 changes: 15 additions & 0 deletions src/test/kotlin/org/move/lang/resolve/ResolveVariablesTest.kt
Original file line number Diff line number Diff line change
Expand Up @@ -776,4 +776,19 @@ module 0x1::string_tests {
}
}
""")

fun `test const accessible from spec functions`() = checkByCode("""
module 0x1::features {
const PERMISSIONED_SIGNER: u64 = 84;
//X
}
module 0x1::m {}
spec 0x1::m {
spec fun is_permissioned_signer(): bool {
use 0x1::features::PERMISSIONED_SIGNER;
PERMISSIONED_SIGNER;
//^
}
} """)
}

0 comments on commit 7f8cf6a

Please sign in to comment.