From 373aba66ef66d0cf5d119953e5fb843d483c8f85 Mon Sep 17 00:00:00 2001 From: Maksim Kurnikov Date: Tue, 22 Oct 2024 03:18:59 +0200 Subject: [PATCH] correct parsing rules for loop invariants (#214) --- src/main/grammars/MoveParser.bnf | 11 +- .../org/move/ide/MvBreadcrumbsProvider.kt | 1 + .../move/lang/core/psi/ext/MvForLoopExpr.kt | 7 + .../org/move/lang/core/psi/ext/MvItemSpec.kt | 2 +- .../lang/core/types/infer/InferenceContext.kt | 6 +- .../core/types/infer/TypeInferenceWalker.kt | 12 +- .../move/lang/parser/CompleteParsingTest.kt | 2 + .../move/lang/types/ExpressionTypesTest.kt | 9 + .../move/lang/parser/complete/index_expr.txt | 2 +- .../lang/parser/complete/loop_invariants.move | 25 ++ .../lang/parser/complete/loop_invariants.txt | 379 ++++++++++++++++++ .../lang/parser/partial/function_calls.txt | 2 +- .../org/move/lang/parser/specs/scopes.txt | 4 +- 13 files changed, 448 insertions(+), 14 deletions(-) create mode 100644 src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt create mode 100644 src/test/resources/org/move/lang/parser/complete/loop_invariants.move create mode 100644 src/test/resources/org/move/lang/parser/complete/loop_invariants.txt diff --git a/src/main/grammars/MoveParser.bnf b/src/main/grammars/MoveParser.bnf index b0118e842..2ad4087ae 100644 --- a/src/main/grammars/MoveParser.bnf +++ b/src/main/grammars/MoveParser.bnf @@ -868,7 +868,8 @@ LetMslStmt ::= (let post?) Pat TypeAscription? Initializer? ';' } ExprStmt ::= (ExprStmt_expr !('}')) ';' { pin = 1 } -private ExprStmt_expr ::= ItemSpecBlockExpr | Expr +private ExprStmt_expr ::= Expr +//private ExprStmt_expr ::= ItemSpecBlockExpr | Expr { recoverWhile = "ExprStmt_recover" } @@ -973,6 +974,7 @@ private AtomExpr ::= // | RefExpr | LambdaExpr | LitExpr + | SpecBlockExpr | CodeBlockExpr @@ -1182,7 +1184,7 @@ LoopExpr ::= loop AnyBlock { pin = 1 implements = [ "org.move.lang.core.psi.MvLoopLike" ] } -WhileExpr ::= while Condition AnyBlock { +WhileExpr ::= while Condition AnyBlock SpecBlockExpr? { pin = 1 implements = [ "org.move.lang.core.psi.MvLoopLike" ] } @@ -1190,7 +1192,7 @@ ForExpr ::= for ForIterCondition AnyBlock { pin = 1 implements = [ "org.move.lang.core.psi.MvLoopLike" ] } -ForIterCondition ::= '(' PatBinding in Expr ')' { +ForIterCondition ::= '(' PatBinding in Expr SpecBlockExpr? ')' { pin = 1 } @@ -1462,11 +1464,12 @@ Schema ::= Attr* (spec schema) IDENTIFIER TypeParameterList? <> { +SpecBlockExpr ::= spec <> { implements = [ "org.move.lang.core.psi.ScopeMslOnlyElement" ] } +ItemSpecBlockExpr ::= spec <> SpecCodeBlock ::= '{' ItemSpecBlock_items '}' { diff --git a/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt b/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt index 398acb49e..19f589ce5 100644 --- a/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt +++ b/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt @@ -5,6 +5,7 @@ import com.intellij.psi.PsiElement import com.intellij.ui.breadcrumbs.BreadcrumbsProvider import org.move.lang.MoveLanguage import org.move.lang.core.psi.* +import org.move.lang.core.psi.ext.expr class MvBreadcrumbsProvider : BreadcrumbsProvider { diff --git a/src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt b/src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt new file mode 100644 index 000000000..7d09da936 --- /dev/null +++ b/src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt @@ -0,0 +1,7 @@ +package org.move.lang.core.psi.ext + +import org.move.lang.core.psi.MvExpr +import org.move.lang.core.psi.MvForIterCondition + +val MvForIterCondition.expr: MvExpr? get() = exprList.firstOrNull() +val MvForIterCondition.specExpr: MvExpr? get() = exprList.drop(1).firstOrNull() \ No newline at end of file diff --git a/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt b/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt index 1558da81d..494824dc9 100644 --- a/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt +++ b/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt @@ -32,7 +32,7 @@ fun MvModuleItemSpec.specInlineFunctions(): List = .orEmpty() val MvItemSpec.itemSpecBlock: MvSpecCodeBlock? get() = this.childOfType() -val MvItemSpecBlockExpr.specBlock: MvSpecCodeBlock? get() = this.childOfType() +val MvSpecBlockExpr.specBlock: MvSpecCodeBlock? get() = this.childOfType() abstract class MvItemSpecMixin(node: ASTNode): MvElementImpl(node), MvItemSpec { diff --git a/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt b/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt index 9b9649b65..30f68e13b 100644 --- a/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt +++ b/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt @@ -236,10 +236,10 @@ class InferenceContext( when (owner) { is MvFunctionLike -> owner.anyBlock?.let { inference.inferFnBody(it) } is MvItemSpec -> { - owner.itemSpecBlock?.let { inference.inferSpec(it) } + owner.itemSpecBlock?.let { inference.inferSpecBlock(it) } } - is MvModuleItemSpec -> owner.itemSpecBlock?.let { inference.inferSpec(it) } - is MvSchema -> owner.specBlock?.let { inference.inferSpec(it) } + is MvModuleItemSpec -> owner.itemSpecBlock?.let { inference.inferSpecBlock(it) } + is MvSchema -> owner.specBlock?.let { inference.inferSpecBlock(it) } } fallbackUnresolvedTypeVarsIfPossible() diff --git a/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt b/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt index 8d654ec21..a3802e32b 100644 --- a/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt +++ b/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt @@ -79,7 +79,7 @@ class TypeInferenceWalker( } fun inferFnBody(block: AnyBlock): Ty = block.inferBlockCoercableTo(returnTy) - fun inferSpec(block: AnyBlock): Ty = + fun inferSpecBlock(block: AnyBlock): Ty = mslScope { block.inferBlockType(NoExpectation) } private fun AnyBlock.inferBlockCoercableTo(expectedTy: Ty): Ty { @@ -240,7 +240,7 @@ class TypeInferenceWalker( is MvMoveExpr -> expr.expr?.inferType() ?: TyUnknown is MvCopyExpr -> expr.expr?.inferType() ?: TyUnknown - is MvItemSpecBlockExpr -> expr.specBlock?.let { inferSpec(it) } ?: TyUnknown + is MvSpecBlockExpr -> inferSpecBlockExprTy(expr) is MvCastExpr -> { expr.expr.inferType() @@ -640,6 +640,14 @@ class TypeInferenceWalker( return TyUnit } + private fun inferSpecBlockExprTy(specBlockExpr: MvSpecBlockExpr): Ty { + val specBlock = specBlockExpr.specBlock + if (specBlock != null) { + inferSpecBlock(specBlock) + } + return TyUnit + } + /** * Unifies the output type with the expected type early, for more coercions * and forward type information on the input expressions diff --git a/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt b/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt index 490df051d..5f52576b4 100644 --- a/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt +++ b/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt @@ -56,6 +56,8 @@ class CompleteParsingTest: MvParsingTestCase("complete") { fun `test is expr`() = doTest() fun `test dot dot pattern`() = doTest() + fun `test loop invariants`() = doTest() + // feature declaration is required here, as it's a parser-level feature // @ResourceAccessControl() // fun `test access control`() = doTest() diff --git a/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt b/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt index f724673b0..aeb477219 100644 --- a/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt +++ b/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt @@ -2156,4 +2156,13 @@ module 0x1::main { } } """) + + fun `test spec block type`() = testExpr(""" + module 0x1::m { + fun main() { + spec {} + //^ () + } + } + """) } diff --git a/src/test/resources/org/move/lang/parser/complete/index_expr.txt b/src/test/resources/org/move/lang/parser/complete/index_expr.txt index 0f394a25d..ef9c9b335 100644 --- a/src/test/resources/org/move/lang/parser/complete/index_expr.txt +++ b/src/test/resources/org/move/lang/parser/complete/index_expr.txt @@ -536,7 +536,7 @@ FILE PsiElement(;)(';') PsiWhiteSpace('\n ') MvExprStmtImpl(EXPR_STMT) - MvItemSpecBlockExprImpl(ITEM_SPEC_BLOCK_EXPR) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) PsiElement(spec)('spec') PsiWhiteSpace(' ') MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) diff --git a/src/test/resources/org/move/lang/parser/complete/loop_invariants.move b/src/test/resources/org/move/lang/parser/complete/loop_invariants.move new file mode 100644 index 000000000..bf611427d --- /dev/null +++ b/src/test/resources/org/move/lang/parser/complete/loop_invariants.move @@ -0,0 +1,25 @@ +module 0x1::loop_invariants { + fun main() { + while (true) {} spec { assert true }; + while (true) 1 + 1 spec { assert true }; + // loop invariant is written in a spec block inside the loop condition + while ({spec {assert x < 42;}; n < 64}) { + spec { + assert x > 42; + assert 0 < x; + }; + n = n + 1 + }; + + // the following should parse successfully but fail typing + spec {} + 1; + spec {} && spec {}; + &mut spec {}; + (spec {}: ()); + + for (i in 1..10 spec { assert true }) {}; + for (i in 0..1 spec {invariant y > 0;}) { + y = y + 1; + }; + } +} diff --git a/src/test/resources/org/move/lang/parser/complete/loop_invariants.txt b/src/test/resources/org/move/lang/parser/complete/loop_invariants.txt new file mode 100644 index 000000000..86267b393 --- /dev/null +++ b/src/test/resources/org/move/lang/parser/complete/loop_invariants.txt @@ -0,0 +1,379 @@ +FILE + MvModuleImpl(MODULE) + PsiElement(module)('module') + PsiWhiteSpace(' ') + MvAddressRefImpl(ADDRESS_REF) + PsiElement(DIEM_ADDRESS)('0x1') + PsiElement(::)('::') + PsiElement(IDENTIFIER)('loop_invariants') + PsiWhiteSpace(' ') + PsiElement({)('{') + PsiWhiteSpace('\n ') + MvFunctionImpl(FUNCTION) + PsiElement(fun)('fun') + PsiWhiteSpace(' ') + PsiElement(IDENTIFIER)('main') + MvFunctionParameterListImpl(FUNCTION_PARAMETER_LIST) + PsiElement(()('(') + PsiElement())(')') + PsiWhiteSpace(' ') + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvWhileExprImpl(WHILE_EXPR) + PsiElement(while)('while') + PsiWhiteSpace(' ') + MvConditionImpl(CONDITION) + PsiElement(()('(') + MvLitExprImpl(LIT_EXPR) + PsiElement(BOOL_LITERAL)('true') + PsiElement())(')') + PsiWhiteSpace(' ') + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace(' ') + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(BOOL_LITERAL)('true') + PsiWhiteSpace(' ') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvWhileExprImpl(WHILE_EXPR) + PsiElement(while)('while') + PsiWhiteSpace(' ') + MvConditionImpl(CONDITION) + PsiElement(()('(') + MvLitExprImpl(LIT_EXPR) + PsiElement(BOOL_LITERAL)('true') + PsiElement())(')') + PsiWhiteSpace(' ') + MvInlineBlockImpl(INLINE_BLOCK) + MvBinaryExprImpl(BINARY_EXPR[+]) + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(+)('+') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace(' ') + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(BOOL_LITERAL)('true') + PsiWhiteSpace(' ') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + PsiComment(EOL_COMMENT)('// loop invariant is written in a spec block inside the loop condition') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvWhileExprImpl(WHILE_EXPR) + PsiElement(while)('while') + PsiWhiteSpace(' ') + MvConditionImpl(CONDITION) + PsiElement(()('(') + MvCodeBlockExprImpl(CODE_BLOCK_EXPR) + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + MvExprStmtImpl(EXPR_STMT) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + MvSpecExprStmtImpl(SPEC_EXPR_STMT) + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[<]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('x') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(<)('<') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('42') + PsiElement(;)(';') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[<]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('n') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(<)('<') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('64') + PsiElement(})('}') + PsiElement())(')') + PsiWhiteSpace(' ') + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace('\n ') + MvSpecExprStmtImpl(SPEC_EXPR_STMT) + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[>]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('x') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(>)('>') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('42') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvSpecExprStmtImpl(SPEC_EXPR_STMT) + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[<]) + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('0') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(<)('<') + PsiWhiteSpace(' ') + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('x') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvAssignmentExprImpl(ASSIGNMENT_EXPR) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('n') + PsiWhiteSpace(' ') + MvInitializerImpl(INITIALIZER) + PsiElement(=)('=') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[+]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('n') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(+)('+') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiWhiteSpace('\n ') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n\n ') + PsiComment(EOL_COMMENT)('// the following should parse successfully but fail typing') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvBinaryExprImpl(BINARY_EXPR[+]) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(+)('+') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvBinaryExprImpl(BINARY_EXPR[&&]) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(&&)('&&') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvBorrowExprImpl(BORROW_EXPR) + PsiElement(&)('&') + PsiElement(mut)('mut') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvAnnotatedExprImpl(ANNOTATED_EXPR) + PsiElement(()('(') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiElement(:)(':') + PsiWhiteSpace(' ') + MvUnitTypeImpl(UNIT_TYPE) + PsiElement(()('(') + PsiElement())(')') + PsiElement())(')') + PsiElement(;)(';') + PsiWhiteSpace('\n\n ') + MvExprStmtImpl(EXPR_STMT) + MvForExprImpl(FOR_EXPR) + PsiElement(for_kw)('for') + PsiWhiteSpace(' ') + MvForIterConditionImpl(FOR_ITER_CONDITION) + PsiElement(()('(') + MvPatBindingImpl(PAT_BINDING) + PsiElement(IDENTIFIER)('i') + PsiWhiteSpace(' ') + PsiElement(in_kw)('in') + PsiWhiteSpace(' ') + MvRangeExprImpl(RANGE_EXPR) + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiElement(..)('..') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('10') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace(' ') + MvAssertSpecExprImpl(ASSERT_SPEC_EXPR) + PsiElement(assert_kw)('assert') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(BOOL_LITERAL)('true') + PsiWhiteSpace(' ') + PsiElement(})('}') + PsiElement())(')') + PsiWhiteSpace(' ') + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvForExprImpl(FOR_EXPR) + PsiElement(for_kw)('for') + PsiWhiteSpace(' ') + MvForIterConditionImpl(FOR_ITER_CONDITION) + PsiElement(()('(') + MvPatBindingImpl(PAT_BINDING) + PsiElement(IDENTIFIER)('i') + PsiWhiteSpace(' ') + PsiElement(in_kw)('in') + PsiWhiteSpace(' ') + MvRangeExprImpl(RANGE_EXPR) + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('0') + PsiElement(..)('..') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiWhiteSpace(' ') + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) + PsiElement(spec)('spec') + PsiWhiteSpace(' ') + MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) + PsiElement({)('{') + MvSpecExprStmtImpl(SPEC_EXPR_STMT) + MvInvariantSpecExprImpl(INVARIANT_SPEC_EXPR) + PsiElement(invariant_kw)('invariant') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[>]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('y') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(>)('>') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('0') + PsiElement(;)(';') + PsiElement(})('}') + PsiElement())(')') + PsiWhiteSpace(' ') + MvCodeBlockImpl(CODE_BLOCK) + PsiElement({)('{') + PsiWhiteSpace('\n ') + MvExprStmtImpl(EXPR_STMT) + MvAssignmentExprImpl(ASSIGNMENT_EXPR) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('y') + PsiWhiteSpace(' ') + MvInitializerImpl(INITIALIZER) + PsiElement(=)('=') + PsiWhiteSpace(' ') + MvBinaryExprImpl(BINARY_EXPR[+]) + MvPathExprImpl(PATH_EXPR) + MvPathImpl(PATH) + PsiElement(IDENTIFIER)('y') + PsiWhiteSpace(' ') + MvBinaryOpImpl(BINARY_OP) + PsiElement(+)('+') + PsiWhiteSpace(' ') + MvLitExprImpl(LIT_EXPR) + PsiElement(INTEGER_LITERAL)('1') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + PsiElement(})('}') + PsiElement(;)(';') + PsiWhiteSpace('\n ') + PsiElement(})('}') + PsiWhiteSpace('\n') + PsiElement(})('}') \ No newline at end of file diff --git a/src/test/resources/org/move/lang/parser/partial/function_calls.txt b/src/test/resources/org/move/lang/parser/partial/function_calls.txt index a47aca767..adb44d130 100644 --- a/src/test/resources/org/move/lang/parser/partial/function_calls.txt +++ b/src/test/resources/org/move/lang/parser/partial/function_calls.txt @@ -340,7 +340,7 @@ FILE PsiElement())(')') PsiElement(;)(';') PsiWhiteSpace('\n\n ') - MvItemSpecBlockExprImpl(ITEM_SPEC_BLOCK_EXPR) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) PsiElement(spec)('spec') PsiWhiteSpace(' ') MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) diff --git a/src/test/resources/org/move/lang/parser/specs/scopes.txt b/src/test/resources/org/move/lang/parser/specs/scopes.txt index 2fea7cfe2..7157f857f 100644 --- a/src/test/resources/org/move/lang/parser/specs/scopes.txt +++ b/src/test/resources/org/move/lang/parser/specs/scopes.txt @@ -18,7 +18,7 @@ FILE PsiElement({)('{') PsiWhiteSpace('\n ') MvExprStmtImpl(EXPR_STMT) - MvItemSpecBlockExprImpl(ITEM_SPEC_BLOCK_EXPR) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) PsiElement(spec)('spec') PsiWhiteSpace(' ') MvSpecCodeBlockImpl(SPEC_CODE_BLOCK) @@ -26,7 +26,7 @@ FILE PsiElement(})('}') PsiElement(;)(';') PsiWhiteSpace('\n ') - MvItemSpecBlockExprImpl(ITEM_SPEC_BLOCK_EXPR) + MvSpecBlockExprImpl(SPEC_BLOCK_EXPR) PsiElement(spec)('spec') PsiWhiteSpace(' ') MvSpecCodeBlockImpl(SPEC_CODE_BLOCK)