Propositional calculus formula validator

formula_validator.py

import string

af = string.ascii_lowercase  # atomic formulas
bo = ['∧', '∨', '⇒', '⇔']  # binary operators
uo = ['¬']  # unary operators


def formula(str):
    l = len(str)

    if l == 0:  # Empty formula
        return False

    if l == 1 and str in af:  # Atomic formula
        return True

    if str[0] == '(' and str[l - 1] == ')':
        if str[1] in uo:  # (¬(a∧b))
            return formula(str[2:l - 1])  # F((a∧b))

        if l == 5 and str[1] in af and str[2] in bo and str[3] in af:  # (a∧b)
            return True

    depth = 0
    for i in range(1, len(str) - 1):  # for each char
        if str[i] == '(':
            depth += 1

        if str[i] == ')':
            depth -= 1

        if depth == 0 and str[i + 1] in bo:
            return formula(str[1:i + 1]) and formula(str[i + 2:l - 1])  # L & R subtree


if __name__ == '__main__':
    print('(¬(l⇒m))', formula('(¬(l⇒m))'))