master > master: allgemeine Aufräumung

code/aussagenlogik/syntaxbaum.py

@@ -6,7 +6,7 @@
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 from __future__ import annotations;
-from lark import Tree;
+from lark import Tree as larkTree;
 from typing import Generator;
 from typing import List;
 
@@ -21,37 +21,31 @@ from typing import List;
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 class SyntaxBaum(object):
-    expr: str;
     kind: str;
+    expr: str;
+    valence: int;
     children: List[SyntaxBaum];
-    tree: Tree;
 
-    def __init__(self, fml: Tree):
+    def __init__(self, fml: larkTree):
         self.kind = fml.data;
-        if len(fml.children) == 1 and isinstance(fml.children[0], str):
-            self.expr = fml.children[0];
-            self.children = [];
-            self.tree = Tree(self.kind, fml.children);
-        else:
-            self.children = [ SyntaxBaum(child) for child in fml.children if isinstance(child, Tree) and child.data != 'symb' ];
-            self.tree = Tree(self.kind, [child.tree for child in self.children]);
-            signature_parts = [];
-            i = 0;
-            for subfml in fml.children:
-                if isinstance(subfml, str):
-                    signature_parts.append(subfml);
-                elif subfml.data == 'symb':
-                    symb = str(subfml.children[0]);
-                    signature_parts.append(symb);
-                else:
-                    signature_parts.append('{{{}}}'.format(i));
-                    i += 1;
-            signature = ' '.join(signature_parts);
-            self.expr = signature.format(*self.children);
-            if self.kind in [ 'konj', 'konj_lang', 'disj', 'disj_lang', 'impl' ]:
-                lbrace = '(' if self.expr.startswith('(') else '( ';
-                rbrace = ')' if self.expr.endswith(')') else ' )';
-                self.expr = lbrace + self.expr + rbrace;
+        self.children = [];
+        self.valence = 0;
+        expr_parts = []
+        for child in fml.children:
+            if isinstance(child, str):
+                expr_parts.append(child);
+            ## subfml is instance larkTree:
+            elif child.data == 'symb':
+                symb = str(child.children[0]);
+                expr_parts.append(symb);
+            else:
+                subtree = SyntaxBaum(child);
+                self.children.append(subtree);
+                self.valence += 1;
+                expr_parts.append(subtree.expr);
+        self.expr = ' '.join(expr_parts);
+        if self.valence > 1:
+            self.expr = '(' + self.expr + ')';
         return;
 
     def __str__(self):
@@ -65,5 +59,58 @@ class SyntaxBaum(object):
     def child(self) -> SyntaxBaum:
         return self.children[0];
 
-    def pretty(self):
-        return self.tree.pretty(indent_str='- ');
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    # METHOD: Pretty
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+    def pretty(self, preindent: str = '', tab: str = '  ', prepend: str = '', depth: int = 0) -> str:
+        indent = preindent + tab*depth;
+        if self.valence == 0 and self.kind in [ 'atom', 'generic' ]:
+            return indent + prepend + self.kind + ' ' + self.expr;
+        return '\n'.join(
+            [indent + prepend + self.kind] \
+            + [subtree.pretty(preindent, tab, '|__ ', depth+1) for subtree in self.children]
+        );
+
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    # METHODS: Erkennung von Formeltypen
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+    def isIrreducible(self) -> bool:
+        return self.valence == 0;
+
+    def isAtom(self) -> bool:
+        return self.kind == 'atom';
+
+    def isLiteral(self) -> bool:
+        return self.isAtom() or (self.isNegation() and self.child.isAtom());
+
+    def isGeneric(self) -> bool:
+        return self.kind == 'generic';
+
+    def isTautologySymbol(self) -> bool:
+        return self.kind == 'taut';
+
+    def isContradictionSymbol(self) -> bool:
+        return self.kind == 'contradiction';
+
+    def isConnective(self) -> bool:
+        return self.valence > 0;
+
+    def isNegation(self) -> bool:
+        return self.kind == 'not';
+
+    def isConjunction2(self) -> bool:
+        return self.kind == 'and2';
+
+    def isConjunction(self) -> bool:
+        return self.kind in ['and', 'and2'];
+
+    def isDisjunction2(self) -> bool:
+        return self.kind == 'or2';
+
+    def isDisjunction(self) -> bool:
+        return self.kind in ['or', 'or2'];
+
+    def isImplication(self) -> bool:
+        return self.kind == 'implies';