diff --git a/code/.gitignore b/code/.gitignore index eb7228e..4a71f7f 100644 --- a/code/.gitignore +++ b/code/.gitignore @@ -10,3 +10,4 @@ !/aussagenlogik !/utests !/**/*.py +!/*/*.lark diff --git a/code/aussagenlogik/grammar.lark b/code/aussagenlogik/grammar.lark new file mode 100644 index 0000000..6f29415 --- /dev/null +++ b/code/aussagenlogik/grammar.lark @@ -0,0 +1,37 @@ +%import common.WS +%import common.NUMBER +%import common.WORD + +%ignore WS + +// Schemata für Ausdrücke +// 'open' = äußerste Klammern fehlen, wenn nötig. +// 'closed' = sonst +?expr: open | closed +?closed: atomic | not | "(" open ")" +?open: and | and_long | or | or_long | impl + +// Schemata für atomische Ausdrücke +?atomic: false | true | atom | generic +?false: /0|false/ -> kontr +?true: /1|true/ -> taut +?atom: /A[0-9]+/ -> atom +// als 'generischen' Formeln schreibe bspw. {F}, {G}, {F1}, usw. +?generic: "{" /((?!({|})).)+/ "}" -> beliebig + +// Symbole (erlaube mehrere Varianten) +?symb_not: /!|~|not/ -> symb +?symb_and: /&+|\^|and/ -> symb +?symb_or: /\|+|v|or/ -> symb +?symb_impl: /->|=>/ -> symb + +// Schema für Negation: ¬ F +?not: symb_not closed -> neg +// Schemata für Konjunktion: F1 ⋀ F2 bzw. F1 ⋀ F2 ⋀ ... ⋀ Fn +?and: closed symb_and closed -> konj +?and_long: [ closed ( symb_and closed )+ ] -> konj_lang +// Schemata für Disjunktion: F1 ⋁ F2 bzw. F1 ⋁ F2 ⋁ ... ⋁ Fn +?or: closed symb_or closed -> disj +?or_long: [ closed ( symb_or closed )+ ] -> disj_lang +// Schema für Implikation: F1 ⟶ F2 +?impl: closed symb_impl closed -> impl diff --git a/code/aussagenlogik/schema.py b/code/aussagenlogik/schema.py index da4b829..778890b 100644 --- a/code/aussagenlogik/schema.py +++ b/code/aussagenlogik/schema.py @@ -18,42 +18,9 @@ from typing import Union; # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ## lexer -lexerAussagenlogik = Lark( - ''' - %import common.WS - %import common.NUMBER - %import common.WORD - %ignore WS - - ?start: expr | open - - ?expr: atomic | not | closed - ?open: and | and_long | or | or_long | impl - ?closed: "(" open ")" - - // atomische Ausdrücke - ?atomic: false | true | atom | generic - ?false: "0" -> kontr - ?true: "1" -> taut - ?atom: /A[0-9]+/ -> atom - ?generic: "{" /((?!({|})).)+/ "}" -> beliebig - - // Symbole - ?symb_not: /!/ -> symb - ?symb_and: /&+/ -> symb - ?symb_or: /\\|+/ -> symb - ?symb_impl: /->|=>/ -> symb - - // Junktoren - ?not: symb_not expr -> neg - ?and: expr symb_and expr -> konj - ?and_long: [ expr ( symb_and expr )+ ] -> konj_lang - ?or: expr symb_or expr -> disj - ?or_long: [ expr ( symb_or expr )+ ] -> disj_lang - ?impl: expr symb_impl expr -> impl - ''', - regex=True -); +with open('aussagenlogik/grammar.lark', 'r') as fp: + grammar = ''.join(fp.readlines()); + lexerAussagenlogik = Lark(grammar, start='expr', regex=True); # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ # KLASSE: Syntaxbaum @@ -87,14 +54,15 @@ class SyntaxBaum(object): signature = ' '.join(signature_parts); self.expr = signature.format(*self.children); if self.kind in [ 'konj', 'konj_lang', 'disj', 'disj_lang', 'impl' ]: - self.expr = '( {} )'.format(self.expr); + self.expr = ('(' if self.expr.startswith('(') else '( ') + self.expr; + self.expr += (')' if self.expr.endswith(')') else ' )'); return; def __str__(self): return self.expr; def pretty(self): - return self.tree.pretty(); + return self.tree.pretty(indent_str='- '); # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ # METHODE: string -> Syntaxbaum