grammar aussagenlogik;

// Standardtokens:
NUMBER: [0-9];
ZERO: ~[a-zA-Z0-9][0]; // negatives Look-Behind nötig, um konfliktierendes Lexing zu vermeiden
ONE: ~[a-zA-Z0-9][1];  // ""
WHITESPACE: [ \r\n\t]+ -> skip;
LBRACE: '(';
RBRACE: ')';
LCURLYBRACE: '{';
RCURLYBRACE: '}';
TEXT: [a-zA-Z0-9\\_];

// Symbole (erlaube mehrere Varianten)
SYMB_NOT:  ('!'|'~'|'not');
SYMB_AND:  ('&'+|'^'|'and');
SYMB_OR:   ('|'+|'v'|'or');
SYMB_IFF:  ([<][-]+[>]|[<][=]+[>]|'iff');
SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);

// Rules
start: open <EOF> | closed <EOF>;

closed: atomic | not | LBRACE open RBRACE;
open: and2 | and | or2 | or | implies | iff;

// Schemata für atomische Ausdrücke
atomic: taut | contradiction | atom | generic;
taut:  (ONE|'true');
contradiction: (ZERO|'false');
atom: 'A' NUMBER+;
// als 'generische' Formeln schreibe bspw. {F}, {G}, usw.
generic: LCURLYBRACE TEXT+ RCURLYBRACE | LCURLYBRACE TEXT* ( generic TEXT* )+ RCURLYBRACE;
// FIXME: liest Zahlen schlecht ein

// Schema für Negation: ¬ F
not:                symb=SYMB_NOT  closed;
// Schemata für Konjunktion: F1 ⋀ F2 bzw. F1 ⋀ F2 ⋀ ... ⋀ Fn
and2:      closed   symb=SYMB_AND  closed;
and:     ( closed ( symb=SYMB_AND  closed )+ );
// Schemata für Disjunktion: F1 ⋁ F2 bzw. F1 ⋁ F2 ⋁ ... ⋁ Fn
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;