From 30dcf598361861c5883b3bf901719e954a2b08ad Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 18 Apr 2026 12:59:02 +0100 Subject: [PATCH 1/3] Added Antlr and a simplified grammar The simplified grammar should allow for consts and variables, field accesses, as well as common boolean operations. It also allows for the use of old() for ghost refinements (pre modified value) and the result keyword. --- latte/pom.xml | 17 ++++++++ latte/src/main/antlr4/RJ.g4 | 81 +++++++++++++++++++++++++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 latte/src/main/antlr4/RJ.g4 diff --git a/latte/pom.xml b/latte/pom.xml index 4ccd60e..43a511f 100644 --- a/latte/pom.xml +++ b/latte/pom.xml @@ -96,6 +96,11 @@ ${version.spoon} + + org.antlr + antlr4-runtime + 4.7.1 + @@ -137,6 +142,18 @@ maven-project-info-reports-plugin 3.0.0 + + org.antlr + antlr4-maven-plugin + 4.7.1 + + + + antlr4 + + + + diff --git a/latte/src/main/antlr4/RJ.g4 b/latte/src/main/antlr4/RJ.g4 new file mode 100644 index 0000000..3085cbe --- /dev/null +++ b/latte/src/main/antlr4/RJ.g4 @@ -0,0 +1,81 @@ +grammar RJ; + +prog: expression EOF; + +expression: logicalOrExpression; + +logicalOrExpression + : logicalAndExpression (OR logicalAndExpression)* + ; + +logicalAndExpression + : equalityExpression (AND equalityExpression)* + ; + +equalityExpression + : relationalExpression ((EQ | NEQ) relationalExpression)? + ; + +relationalExpression + : additiveExpression ((LT | GT | LE | GE) additiveExpression)? + ; + +additiveExpression + : unaryExpression ((PLUS | MINUS) unaryExpression)* + ; + +unaryExpression + : (NOT | MINUS) unaryExpression + | primary + ; + +primary + : literal + | RESULT + | oldExpression + | fieldAccess + | ID + | LPAREN expression RPAREN + ; + +oldExpression + : OLD LPAREN fieldAccess RPAREN + ; + +fieldAccess + : ID DOT ID + ; + +literal + : BOOL + | STRING + | INT + | REAL + ; + +OLD: 'old'; +RESULT: 'result'; + +AND: '&&'; +OR: '||'; +EQ: '=='; +LE: '<='; +LT: '<'; +GE: '>='; +GT: '>'; +PLUS: '+'; +MINUS: '-'; +NEQ: '!='; +NOT: '!'; + +LPAREN: '('; +RPAREN: ')'; +DOT: '.'; + +BOOL: 'true' | 'false'; +ID: '#'* [a-zA-Z_][a-zA-Z0-9_#]*; +STRING: '"' (~["])* '"'; +INT: [0-9]+ ('_' [0-9]+)*; +REAL: ([0-9]+ '.' [0-9]+) | ('.' [0-9]+); + +WS: [ \t\n\r]+ -> channel(HIDDEN); From d5f9cb66a961093797acd6278cd28b5e7b094c7d Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 18 Apr 2026 19:05:18 +0100 Subject: [PATCH 2/3] Shortened grammar names, updated Antlr Grammar is now shorter instead of full 'expression' names. Updated Antlr due to issue with directories. Updated IDE settings to update build configuration when sources are generated. --- .vscode/settings.json | 5 +---- latte/pom.xml | 6 ++---- latte/src/main/antlr4/RJ.g4 | 30 +++++++++++++++--------------- 3 files changed, 18 insertions(+), 23 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index b266fd8..9bd06c2 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,7 +1,4 @@ { - "java.configuration.updateBuildConfiguration": "interactive", - "cSpell.words": [ - "symb" - ], + "java.configuration.updateBuildConfiguration": "automatic", "java.debug.settings.onBuildFailureProceed": true } \ No newline at end of file diff --git a/latte/pom.xml b/latte/pom.xml index 43a511f..a623f2a 100644 --- a/latte/pom.xml +++ b/latte/pom.xml @@ -99,12 +99,11 @@ org.antlr antlr4-runtime - 4.7.1 + 4.13.2 - maven-clean-plugin @@ -145,7 +144,7 @@ org.antlr antlr4-maven-plugin - 4.7.1 + 4.13.2 @@ -155,6 +154,5 @@ - diff --git a/latte/src/main/antlr4/RJ.g4 b/latte/src/main/antlr4/RJ.g4 index 3085cbe..094dd9f 100644 --- a/latte/src/main/antlr4/RJ.g4 +++ b/latte/src/main/antlr4/RJ.g4 @@ -2,43 +2,43 @@ grammar RJ; prog: expression EOF; -expression: logicalOrExpression; +expression: logicalOrExp; -logicalOrExpression - : logicalAndExpression (OR logicalAndExpression)* +logicalOrExp + : logicalAndExp (OR logicalAndExp)* ; -logicalAndExpression - : equalityExpression (AND equalityExpression)* +logicalAndExp + : equalityExp (AND equalityExp)* ; -equalityExpression - : relationalExpression ((EQ | NEQ) relationalExpression)? +equalityExp + : relationalExp ((EQ | NEQ) relationalExp)? ; -relationalExpression - : additiveExpression ((LT | GT | LE | GE) additiveExpression)? +relationalExp + : additiveExp ((LT | GT | LE | GE) additiveExp)? ; -additiveExpression - : unaryExpression ((PLUS | MINUS) unaryExpression)* +additiveExp + : unaryExp ((PLUS | MINUS) unaryExp)* ; -unaryExpression - : (NOT | MINUS) unaryExpression +unaryExp + : (NOT | MINUS) unaryExp | primary ; primary : literal | RESULT - | oldExpression + | oldExp | fieldAccess | ID | LPAREN expression RPAREN ; -oldExpression +oldExp : OLD LPAREN fieldAccess RPAREN ; From 961af526bbf6d86885a18d89df838ae01b8418bf Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 18 Apr 2026 21:33:18 +0100 Subject: [PATCH 3/3] Moved grammar to nested folder --- latte/src/main/antlr4/{ => rj/grammar}/RJ.g4 | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename latte/src/main/antlr4/{ => rj/grammar}/RJ.g4 (100%) diff --git a/latte/src/main/antlr4/RJ.g4 b/latte/src/main/antlr4/rj/grammar/RJ.g4 similarity index 100% rename from latte/src/main/antlr4/RJ.g4 rename to latte/src/main/antlr4/rj/grammar/RJ.g4