From 79bfcf57bb9ca42abb6ff4ca929634d146bb0a6a Mon Sep 17 00:00:00 2001
From: raj_mathe <raj.dahya@math.uni-leipzig.de>
Date: Sat, 15 May 2021 00:05:03 +0200
Subject: [PATCH] master > master: codego - iff

---
 codego/aussagenlogik/formulae/formulae_basic.go       |  1 +
 .../aussagenlogik/formulae/formulae_construction.go   |  9 +++++++++
 codego/aussagenlogik/recursion/recursion_eval.go      |  2 ++
 codego/aussagenlogik/schema/schema.go                 |  5 +++++
 codego/grammars/aussagenlogik.g4                      | 11 +++++++----
 5 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/codego/aussagenlogik/formulae/formulae_basic.go b/codego/aussagenlogik/formulae/formulae_basic.go
index 55315e6..c85249b 100644
--- a/codego/aussagenlogik/formulae/formulae_basic.go
+++ b/codego/aussagenlogik/formulae/formulae_basic.go
@@ -145,3 +145,4 @@ func (fml Formula) IsConjunction() bool         { return fml.kind == "and" || fm
 func (fml Formula) IsDisjunction2() bool        { return fml.kind == "or2" }
 func (fml Formula) IsDisjunction() bool         { return fml.kind == "or" || fml.kind == "or2" }
 func (fml Formula) IsImplication() bool         { return fml.kind == "implies" }
+func (fml Formula) IsDoubleImplication() bool   { return fml.kind == "iff" }
diff --git a/codego/aussagenlogik/formulae/formulae_construction.go b/codego/aussagenlogik/formulae/formulae_construction.go
index 1074d32..bf4e817 100644
--- a/codego/aussagenlogik/formulae/formulae_construction.go
+++ b/codego/aussagenlogik/formulae/formulae_construction.go
@@ -115,3 +115,12 @@ func Implies(fml1 Formula, fml2 Formula) Formula {
 		subformulae: [](*Formula){&fml1, &fml2},
 	}
 }
+
+func DoubleImplication(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "iff",
+		expr:        "(" + fml1.expr + " <-> " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
diff --git a/codego/aussagenlogik/recursion/recursion_eval.go b/codego/aussagenlogik/recursion/recursion_eval.go
index bccdf18..4ab21fb 100644
--- a/codego/aussagenlogik/recursion/recursion_eval.go
+++ b/codego/aussagenlogik/recursion/recursion_eval.go
@@ -31,6 +31,8 @@ func Eval(fml formulae.Formula, I []string) int {
 				return utils.MaxList(prevValues)
 			} else if fml.IsImplication() {
 				return utils.BoolToInt(prevValues[0] <= prevValues[1])
+			} else if fml.IsDoubleImplication() {
+				return utils.BoolToInt(prevValues[0] == prevValues[1])
 			} else {
 				panic("Could not evaluate expression!")
 			}
diff --git a/codego/aussagenlogik/schema/schema.go b/codego/aussagenlogik/schema/schema.go
index 782b620..78de0d3 100644
--- a/codego/aussagenlogik/schema/schema.go
+++ b/codego/aussagenlogik/schema/schema.go
@@ -139,6 +139,11 @@ func (ant antlrTree) toFormula() formulae.Formula {
 		if nChildren == 3 {
 			return formulae.Implies(subants[0].toFormula(), subants[2].toFormula())
 		}
+	case "iff":
+		// NOTE: expr = expr <=> expr
+		if nChildren == 3 {
+			return formulae.DoubleImplication(subants[0].toFormula(), subants[2].toFormula())
+		}
 	case "and", "or":
 		// NOTE: expr = expr op expr op ... op expr
 		var n int = int((len(subants) + 1) / 2)
diff --git a/codego/grammars/aussagenlogik.g4 b/codego/grammars/aussagenlogik.g4
index a37334a..3e43365 100644
--- a/codego/grammars/aussagenlogik.g4
+++ b/codego/grammars/aussagenlogik.g4
@@ -12,13 +12,14 @@ RCURLYBRACE: '}';
 SYMB_NOT:  ('!'|'~'|'not');
 SYMB_AND:  ('&'+|'^'|'and');
 SYMB_OR:   ('|'+|'v'|'or');
-SYMB_IMPL: ('->'|'=>');
+SYMB_IFF:  ([<][-]+[>]|[<][=]+[>]|'iff');
+SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);
 
 // Rules
 start: open <EOF> | closed <EOF>;
 
 closed: atomic | not | LBRACE open RBRACE;
-open: and2 | and | or2 | or | implies;
+open: and2 | and | or2 | or | implies | iff;
 
 // Schemata für atomische Ausdrücke
 atomic: taut | contradiction | atom; //| generic;
@@ -26,8 +27,8 @@ taut:  ('1'|'true');
 contradiction: ('0'|'false');
 atom: 'A0' | 'A1' | 'A' NUMBER; // muss A0, A1 wegen falsum/verum extra auflisten
 // // als 'generische' Formeln schreibe bspw. {F}, {G}, {F1}, usw.
-// // generic: LCURLYBRACE (.*?) RCURLYBRACE;
-// FIXME: dieses Schema führt zu Konflikten
+// generic: LCURLYBRACE (~[{])+ RCURLYBRACE;
+// // FIXME: dieses Schema führt zu Konflikten
 
 // Schema für Negation: ¬ F
 not:                symb=SYMB_NOT  closed;
@@ -39,3 +40,5 @@ or2:       closed   symb=SYMB_OR   closed;
 or:      ( closed ( symb=SYMB_OR   closed )+ );
 // Schema für Implikation: F1 ⟶ F2
 implies:   closed   symb=SYMB_IMPL closed;
+// Schema für Implikation: F1 ⟷ F2
+iff:       closed   symb=SYMB_IFF  closed;