From f9cf4ade7e88ec48a5408be0e74e4f5200c2906a Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 13 Jan 2025 21:03:01 +0100
Subject: [PATCH] add missing cases and test for neg
---
.../de/tla2b/analysis/PredicateVsExpression.java | 3 ++-
src/main/java/de/tla2bAst/BAstCreator.java | 6 ++++--
.../de/tla2b/typechecking/LogicOperatorsTest.java | 12 ++++++++++++
3 files changed, 18 insertions(+), 3 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index ea0c647..1427941 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -50,7 +50,8 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
case OPCODE_lor: // \/
case OPCODE_equiv: // \equiv
case OPCODE_implies: // =>
- case OPCODE_lnot: // \lnot
+ case OPCODE_neg: // \neg
+ case OPCODE_lnot: // ~ / \lnot
case OPCODE_be: // \E x \in S : P
case OPCODE_bf: // \A x \in S : P
case OPCODE_in: // \in
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 906ef12..5681a7e 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -996,7 +996,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
.map(this::visitExprOrOpArgNodePredicate).collect(Collectors.toList()));
break;
- case OPCODE_lnot: // \lnot
+ case OPCODE_neg: // \neg
+ case OPCODE_lnot: // ~ / \lnot
returnNode = new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
break;
@@ -1144,7 +1145,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
case OPCODE_cl: // $ConjList
case OPCODE_dl: // $DisjList
case OPCODE_lor: // \/
- case OPCODE_lnot: // \lnot
+ case OPCODE_neg: // \neg
+ case OPCODE_lnot: // ~ / \lnot
case OPCODE_in: // \in
case OPCODE_notin: // \notin
case OPCODE_eq: // =
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index 5af94a9..611cecb 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -58,6 +58,18 @@ public class LogicOperatorsTest {
assertEquals("BOOL", t.getConstantType("k3"));
}
+ @Test
+ public void testNeg() throws TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k, k2\n"
+ + "ASSUME k = \\neg k2 \n"
+ + "=================================";
+
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("BOOL", t.getConstantType("k"));
+ assertEquals("BOOL", t.getConstantType("k2"));
+ }
+
@Test(expected = TypeErrorException.class)
public void testLogicOperatorsError() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
--
GitLab