from dataclasses import dataclass, field, MISSING
from fractions import Fraction
from typing import NamedTuple, Tuple, Union, Optional, Text, MutableMapping, Sequence, Set, \
    MutableSet, Generator, Iterable, Collection

from abc import ABCMeta, abstractmethod


class ChartException(Exception, metaclass=ABCMeta):
    @property
    @abstractmethod
    def msgs(self) -> Sequence['ChartMessage']:
        pass

    @abstractmethod
    def to_json(self):
        pass


class ChartMessage(ChartException):
    @property
    def msgs(self) -> Sequence['ChartMessage']:
        return (self,)

    def __init__(self, kind, message, target=None):
        self.kind, self.message = kind, message
        self.target = target.id if hasattr(target, 'id') else target

    def to_json(self):
        json = {'kind': self.kind, 'message': self.message}
        if self.target is not None: json['target'] = self.target
        return json


class ChartMessages(ChartException):
    @property
    def msgs(self) -> Sequence['ChartMessage']:
        return self._msgs

    def __init__(self, *exceptions: ChartException):
        self._msgs = [msg for exception in exceptions for msg in exception.msgs]

    def to_json(self):
        return list(map(ChartException.to_json, self.msgs))


class Error(ChartMessage):
    def __init__(self, message, target=None):
        super().__init__('error', message, target)


class Alert(ChartMessage):
    def __init__(self, message, target=None):
        super().__init__('alert', message, target)


class Warning(ChartMessage):
    def __init__(self, message, target=None):
        super().__init__('warning', message, target)

from enum import Enum


class Kind(Enum):
    INTEGER = 'integer', lambda x: x == 0
    SUBRANGE = '‥', lambda x: x == 2
    BOOLEAN = 'bool', lambda x: x == 0
    FRACTION = 'fraction', lambda x: x == 2
    PRODUCT = '×', lambda x: x >= 2
    FUNCTION = '→', lambda x: x == 2
    SET = 'set', lambda x: x == 1

    def __new__(cls, name, arity):
        kind = object.__new__(cls)
        kind._value_ = name
        kind.arity = arity
        return kind

    def __str__(self):
        return self.value


@dataclass
class Type:
    kind: Kind
    args: Tuple[Union['Type', 'Expression'], ...]

    def __init__(self, kind: Union[Text, Kind], *args: Union['Type', 'Expression']):
        self.kind = kind if isinstance(kind, Kind) else Kind(kind)
        self.args = args
        assert self.kind.arity(len(args))

    def __str__(self):
        if self.kind in (Kind.SUBRANGE, Kind.FUNCTION):
            return '%s %s %s' % (self.args[0], self.kind, self.args[1])
        elif self.kind == Kind.PRODUCT:
            return ' × '.join(
                ('[%s]' if arg.kind in {Kind.PRODUCT, Kind.FUNCTION} else '%s') % arg for arg in self.args)
        elif self.kind == Kind.SET:
            return 'set ' + ('[%s]' if self.args[0].kind in {Kind.PRODUCT, Kind.FUNCTION} else '%s') % self.args[0]
        else:
            return str(self.kind)  # integer, boolean, fraction


assert str(Type('→', Type('×', Type('‥', 3, 9), Type('bool')), Type('set', Type('‥', 0, 9)))) == \
       '3 ‥ 9 × bool → set 0 ‥ 9'
assert str(Type('→', Type('integer'), Type('×', Type('bool'), Type('integer')))) == 'integer → bool × integer'
assert str(Type('×', Type('→', Type('integer'), Type('bool')), Type('integer'))) == '[integer → bool] × integer'
assert str(Type('×', Type('integer'), Type('→', Type('bool'), Type('integer')))) == 'integer × [bool → integer]'

Event = Text
Cost = Tuple['Expression', Optional[Text]]

INHERIT_NAME_FROM_ID = object()


@dataclass()
class State:
    id: Text
    parent: 'Optional[State]' = None
    children: 'MutableSet[State]' = field(default_factory=set, init=False)
    name: Optional[Text] = INHERIT_NAME_FROM_ID
    const: 'MutableMapping[Text, ConstNumberExpression]' = field(default_factory=dict)
    var: MutableMapping[Text, Type] = field(default_factory=dict)
    inv: 'Optional[Expression]' = None
    ev: MutableSet[Event] = field(default_factory=set)
    cost: MutableMapping[Text, Cost] = field(default_factory=dict)
    init: Set['Conditional'] = field(default_factory=set)
    unique_name: Optional[Text] = None
    unique_vars: Optional[MutableMapping[Text, Text]] = None  # unique_name -> declared name

    def __post_init__(self):
        if self.name is INHERIT_NAME_FROM_ID:
            self.name = self.id

        if self.parent is not None:
            self.parent.children.add(self)

    def __str__(self):
        return 'State(id=' + str(self.id) + \
               (', parent=' + str(self.parent.id) if self.parent else '') + \
               ', children=' + str(self.children) + \
               ', name=' + str(self.name) + \
               ', const=' + str(self.const) + \
               ', var=' + str({v: str(self.var[v]) for v in self.var}) + \
               (', inv=' + str(self.inv) if self.inv else '') + \
               ', ev=' + str(self.ev) + \
               ', cost=' + str({c: (str(self.cost[c][0]), str(self.cost[c][1])) for c in self.cost}) + \
               ', init=' + str(self.init) + \
               (', unique_name=' + str(self.unique_name) if self.unique_name is not None else '') + ')'

    def __repr__(self):
        return 'State(id=' + str(self.id) + ', ...)'

    def __hash__(self):
        return hash(self.id)

    def print_hierarchy(self, prefer_unique=False, indent=2, depth=0) -> Text:
        if prefer_unique and self.unique_vars:
            variables = map(lambda ud: (ud[0], self.var[ud[1]]), self.unique_vars.items())
        else:
            variables = self.var.items()
        variables_msg = ', '.join('%s:%s' % (name, typ) for name, typ in variables)
        if len(variables_msg) > 0:
            variables_msg = '|' + variables_msg

        msg = depth * indent * ' ' + ((prefer_unique and self.unique_name) or self.name or '_') + variables_msg
        for child in self.children:
            msg += '\n' + child.print_hierarchy(prefer_unique=prefer_unique, indent=indent, depth=depth + 1)
        return msg

    def siblings(self, reflexive=False) -> Generator['State', None, None]:
        if self.parent is None:
            return
        for s in self.parent.children:
            if reflexive or s.id != self.id:
                yield s

class Transition:
    def __init__(self, id: Text, source: State, event: Union[Event, 'Timing'], guard: 'Expression',
                 cost: MutableMapping[Text, Cost], body: 'Statement', alt: 'Set[Alternative]'):
        self.id, self.source, self.event, self.guard, self.cost, self.body, self.alt = \
            id, source, event, guard, cost, body, alt

    def __str__(self):
        return 'Transition(source=' + repr(self.source) + \
               ' event=' + str(self.event) + \
               (' guard=' + str(self.guard) if self.guard else '') + \
               ' cost=' + str(self.cost) + \
               ' body=' + str(self.body) + \
               ' alt=' + str([[str(alt.prob), str(alt.body), [[str(cond.guard), str(cond.body), repr(cond.target)]
                                                              for cond in alt.cond]] for alt in self.alt]) + ')'

    def __repr__(self):
        return 'Transition(id=' + str(self.id) + ', ...)'


class Alternative(NamedTuple):
    prob: Fraction
    body: 'Statement'
    cond: 'Set[Conditional]'


class Conditional(NamedTuple):
    guard: 'Expression'
    body: 'Statement'
    target: 'State'


def cond_always(target: 'State'):
    return Conditional(True, skip, target)

class TimingKind(Enum):
    BETWEEN = 'between', lambda t0, t1: t0 is not None or t1 is not None
    EXPONENTIAL = 'exp', lambda t0, t1: t0 is not None and t1 is None
    UNIFORM = 'unif', lambda t0, t1: t0 is not None and t1 is not None

    def __new__(cls, name, validate_args):
        kind = object.__new__(cls)
        kind._value_ = name
        kind.validate_args = validate_args
        return kind

    def __str__(self):
        return self.value


@dataclass
class Timing:
    kind: TimingKind
    t0: Optional['ConstNumberExpression'] = None
    t1: Optional['ConstNumberExpression'] = None

    def __init__(self, kind: Union[Text, TimingKind], t0: Optional['ConstNumberExpression'] = None,
                 t1: Optional['ConstNumberExpression'] = None):
        self.kind = kind if isinstance(kind, TimingKind) else TimingKind(kind)
        self.t0, self.t1 = Fraction(t0) if t0 is not None else None, Fraction(t1) if t1 is not None else None
        assert self.kind.validate_args(t0, t1)

    def __str__(self):
        if self.kind == TimingKind.BETWEEN:
            if self.t0 == self.t1:
                return str(self.t0)
            elif self.t0 is None:
                return '‥' + str(self.t1)
            elif self.t1 is None:
                return '‥' + str(self.t0)
            else:
                return str(self.t0) + '‥' + str(self.t1)
        elif self.kind == TimingKind.EXPONENTIAL:
            return 'exp(%s)' % self.t0
        elif self.kind == TimingKind.UNIFORM:
            return 'unif(%s, %s)' % (self.t0, self.t1)

PrefixOp = {'⊖', '¬', '#', 'in', 'min', 'max', 'all', 'any', 'some', '∑', '∏', 'set'}
NonAssocCommOp = {',', '-', '/', 'div', 'mod', '⇒', '⇐', '≡', '≢', '=', '≠', '≤', '≥', '<', '>',
                  '∈', '∉', '⊆', '⊇', '⊂', '⊃', '\\', '‥'}
AssocCommmOp = {'+', '×', '∧', '∨', '∩', '∪', '{}'}


# additionally tertiary '?', set comprehension `set`

class Application(NamedTuple):
    fn: Text
    arg: Union['Expression', Sequence['Expression']]

    def __eq__(self, other):
        return isinstance(other, Application) and self.fn == other.fn and \
               ((self.fn in AssocCommmOp and all(
                   self.arg.count(a) == other.arg.count(a) for a in self.arg)) or self.arg == other.arg)

    def __str__(self):
        if self.fn in PrefixOp:
            return ('-' if self.fn == '⊖' else self.fn) + ' ' + str(self.arg)
        elif self.fn == '{}':
            return '{' + ', '.join(nstr(a) for a in self.arg) + '}'
        elif self.fn == ',':
            return ', '.join(nstr(a) for a in self.arg)
        elif self.fn in NonAssocCommOp | AssocCommmOp:
            return '(' + (' ' + self.fn + ' ').join(str(a) for a in self.arg) + ')'
        elif self.fn == '?':
            return '(' + nstr(self.arg[0]) + ' ? ' + nstr(self.arg[1]) + ' : ' + nstr(self.arg[2]) + ')'
        else:
            return self.fn + str(self.arg)


class Abstraction(NamedTuple):
    var: Text
    range: Optional[Type]
    cond: Optional['Expression']
    body: 'Expression'

    def __str__(self):
        return '(' + self.var + (' ∈ ' + str(self.range) if self.range else '') + \
               ('' if self.cond is True else ', ' + nstr(self.cond)) + ' • ' + nstr(self.body) + ')'


Expression = Union[bool, int, Fraction, Text, Application, Abstraction]
ConstNumberExpression = Union[int, Fraction]


def nstr(e: Expression) -> str:
    """no parenthesis string: remove leading ( or [ and trailing ) or ], if present"""
    s = str(e)
    return s[1:-1] if s[0] in ('(', '[') else s

e = Application('+', ('x', Application('×', ('y', 'z'))))
f = Application('+', (Application('×', ('z', 'y')), 'x'))
assert str(e) == '(x + (y × z))'
assert str(f) == '((z × y) + x)'
assert e == f

e, f = Application('{}', ('x', 'y')), Application('{}', ('x', 'z'))
assert str(e) == '{x, y}' and str(f) == '{x, z}'
assert e != f

e, f = Application('-', ('x', 'y')), Application('-', ('y', 'x'))
assert str(e) == '(x - y)' and str(f) == '(y - x)'
assert e != f

e = Application('-', ('x', Application('+', ('x', 'y'))))
f = Application('-', ('x', Application('+', ('y', 'x'))))
assert str(e) == '(x - (x + y))'
assert str(f) == '(x - (y + x))'
assert e == f

def iterate_associative_op(op: Text, *exp: Expression) -> Generator[Expression, None, None]:
    for e in exp:
        if isinstance(e, Application) and e.fn == op:
            yield from iterate_associative_op(op, *e.arg if isinstance(e.arg, Iterable) else e.arg)
        else:
            yield e

def parent_transitive_closure(s: State, reflexive: bool=False, include_root: bool=True) -> Generator[State, None, None]:
    if include_root:
        if reflexive:
            yield s
        while s.parent is not None:
            yield s.parent
            s = s.parent
    else:
        if s.parent is None:
            return
        if reflexive:
            yield s
        s = s.parent # parent is not None from the above if statement
        while s.parent is not None:
            yield s
            s = s.parent

def negative(e: Expression) -> Expression:
    if isinstance(e, (int, Fraction)):
        return -e
    elif isinstance(e, Application) and e.fn == '⊖':
        return e.arg
    else:
        return Application('⊖', e)


assert str(negative(3)) == '-3'
assert str(negative(negative(3))) == '3'
assert str(negative('x')) == '- x'

def negation(e: Expression) -> Expression:
    if isinstance(e, bool):
        return not e
    elif isinstance(e, Application) and e.fn == '¬':
        return e.arg
    else:
        return Application('¬', e)


assert str(negation(True)) == 'False'
assert str(negation(negation('x'))) == 'x'
assert str(negation('x')) == '¬ x'

def summation(e: Abstraction) -> Expression:
    assert e.range is not None and e.range.kind == Kind.SUBRANGE, 'Summation abstraction parameter type must be subrange.'

    if all(isinstance(arg, int) for arg in e.range.args) and e.range.args[0] > e.range.args[1]:
        return 0
    elif e.cond is False:
        return 0
    else:
        return Application('∑', e)


assert str(summation(Abstraction('i', Type('‥', 5, 3), True, 'i'))) == '0'
assert str(summation(Abstraction('i', Type('‥', 'a', 'b'), False, 'i'))) == '0'
assert str(summation(Abstraction('i', Type('‥', 'a', 'b'), True, 'i'))) == '∑ (i ∈ a ‥ b • i)'

def product(e: Abstraction) -> Expression:
    assert e.range is not None and e.range.kind == Kind.SUBRANGE, 'Product abstraction parameter type must be subrange.'

    if all(isinstance(arg, int) for arg in e.range.args) and e.range.args[0] > e.range.args[1]:
        return 1
    elif e.cond is False:
        return 1
    else:
        return Application('∏', e)


assert str(product(Abstraction('i', Type('‥', 5, 3), True, 'i'))) == '1'
assert str(product(Abstraction('i', Type('‥', 'a', 'b'), False, 'i'))) == '1'
assert str(product(Abstraction('i', Type('‥', 'a', 'b'), True, 'i'))) == '∏ (i ∈ a ‥ b • i)'

def minimum(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':  # set enumeration
        m, sa, oa = None, [], list(e.arg)  # minimum so far, simplified arguments, original arguments
        while oa:
            ei = oa.pop(0)
            if isinstance(ei, (int, Fraction)):
                if m is None:
                    sa.append(ei); m = ei
                elif m > ei:
                    sa.remove(m); sa.append(ei); m = ei
            elif isinstance(ei, Application) and ei.fn == 'min' and \
                    isinstance(ei.arg, Application) and ei.arg.fn == '{}':
                oa = list(ei.arg.arg) + oa
            elif ei not in sa:
                sa.append(ei)
        assert len(sa) > 0, 'min of empty collection'
        return sa[0] if len(sa) == 1 else Application('min', Application('{}', sa))
    else:
        return Application('min', e)  # other set expression


assert str(minimum(Application('∪', ('x', 'y')))) == 'min (x ∪ y)'

e = Application('{}', (3, 'x', Application('min', Application('{}', ('x', 4)))))
assert str(e) == '{3, x, min {x, 4}}'
assert str(minimum(e)) == 'min {3, x}'

e = Application('{}', (4, 3))
assert str(e) == '{4, 3}'
assert str(minimum(e)) == '3'

try:
    print(minimum(Application('{}', [])))
except Exception as m:
    assert str(m) == 'min of empty collection'

def maximum(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':  # set enumeration
        m, sa, oa = None, [], list(e.arg)  # maximum so far, simplified arguments, original arguments
        while oa:
            ei = oa.pop(0)
            if isinstance(ei, (int, Fraction)):
                if m is None:
                    sa.append(ei); m = ei
                elif m < ei:
                    sa.remove(m); sa.append(ei); m = ei
            elif isinstance(ei, Application) and ei.fn == 'max' and \
                    isinstance(ei.arg, Application) and ei.arg.fn == '{}':
                oa = list(ei.arg.arg) + oa
            elif ei not in sa:
                sa.append(ei)
        assert len(sa) > 0, 'max of empty collection'
        return sa[0] if len(sa) == 1 else Application('max', Application('{}', sa))
    else:
        return Application('max', e)  # other set expression


assert str(maximum(Application('∪', ['x', 'y']))) == 'max (x ∪ y)'

e = Application('{}', [3, 'x', Application('max', Application('{}', ['x', 4]))])
assert str(e) == '{3, x, max {x, 4}}'
assert str(maximum(e)) == 'max {x, 4}'

e = Application('{}', [4, 3])
assert str(e) == '{4, 3}'
assert str(maximum(e)) == '4'

try:
    print(maximum(Application('{}', [])))
except Exception as m:
    assert str(m) == 'max of empty collection'

def universal(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':
        sa = [ei for ei in e.arg if ei is not True]
        if sa == []:
            return True
        elif False in sa:
            return False
        else:
            return Application('all', Application('{}', sa))
    else:
        return Application('all', e)


assert str(universal(Application('{}', []))) == 'True'
assert str(universal(Application('{}', [True]))) == 'True'
assert str(universal(Application('{}', [False]))) == 'False'
assert str(universal(Application('{}', [Application('>', ['x', 3])]))) == 'all {x > 3}'
assert str(universal(Application('∪', ['x', 'y']))) == 'all (x ∪ y)'


#     elif isinstance(e, Quantification): # set comprehension
#        assert e.quantifier == 'set', "argument of 'all' must be set"
#        if all(not substitution(e.cond, e.var, i) or substitution(e.body, e.var, i) \
#               for i in range(e.range[1], e.range[2] + 1)): return True
#        else: return Application('all', [e]) # not all values of the body are true

def existential(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':
        sa = [ei for ei in e.arg if ei is not False]
        if sa == []:
            return False
        elif True in sa:
            return True
        else:
            return Application('any', Application('{}', sa))
    else:
        return Application('any', e)


assert str(existential(Application('{}', [True]))) == 'True'
assert str(existential(Application('{}', [False]))) == 'False'
assert str(existential(Application('{}', [Application('>', ['x', 3])]))) == 'any {x > 3}'
assert str(existential(Application('∪', ['x', 'y']))) == 'any (x ∪ y)'

from random import choice


# TODO move import to beginning, document dependency
# TODO choice in the compiler causes non-deterministic output

def some(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':
        return choice(e.arg)
    else:
        return Application('some', e)


assert str(some(Application('{}', [1, 2]))) in ('1', '2')
assert str(some(Application('∪', ['x', 'y']))) == 'some (x ∪ y)'

def cardinality(e: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':
        return len(e.arg)
    else:
        return Application('#', e)  # other set expression


assert str(cardinality(Application('{}', [3, 5]))) == '2'
assert str(cardinality(Application('∪', ['x', 'y']))) == '# (x ∪ y)'

# TODO add simplifications

def statetest(s: Expression) -> Expression:
    return Application('in', s)


assert str(statetest('S')) == 'in S'

SUP = {'⁰': 0, '¹': 1, '²': 2, '³': 3, '⁴': 4, '⁵': 5, '⁶': 6, '⁷': 7, '⁸': 8, '⁹': 9}


def power(e: Expression, n: Expression) -> Expression:
    if isinstance(e, (int, Fraction)):
        return e ** SUP[n]
    elif n == '⁰':
        return 1
    elif n == '¹':
        return e
    else:
        return Application(n, e)


assert power(3, '²') == 9
assert power(Fraction(1, 2), '¹') == Fraction(1, 2)
assert power('x', '⁰') == 1
assert power('x', '¹') == 'x'

def addition(*el: Expression) -> Expression:
    sc, sa = 0, []  # sum of constants, simplified argument
    for e in iterate_associative_op('+', *el):
        if isinstance(e, (int, Fraction)):
            sc += e
        else:
            sa.append(e)

    return sc if len(sa) == 0 else \
        sa[0] if len(sa) == 1 and sc == 0 else \
            Application('+', sa) if sc == 0 else \
                Application('+', [sc] + sa)


assert str(addition(3, 2)) == '5'
assert str(addition(3, 'x')) == '(3 + x)'
assert str(addition('x', 0)) == 'x'
assert str(addition('x', 'y')) == '(x + y)'
assert str(addition(3, 'x', 2, 'y', 4)) == '(9 + x + y)'
assert str(addition(addition('e', 'f', 2), addition('g', 3, 'h'))) == '(5 + e + f + g + h)'

def subtraction(e: Expression, f: Expression) -> Expression:
    if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)):
        return e - f
    elif f == 0:
        return e
    elif e == 0:
        return negative(f)
    elif isinstance(f, Application) and f.fn == '⊖':
        return addition(e, f.arg)
    else:
        return Application('-', [e, f])


assert str(subtraction(3, 6)) == '-3'
assert str(subtraction('x', negative('y'))) == '(x + y)'
assert str(subtraction('x', 0)) == 'x'
assert str(subtraction(0, 'x')) == '- x'

def multiplication(*el: Expression) -> Expression:
    pc, sa = 1, []  # product of constants, simplified argument
    for e in iterate_associative_op('×', *el):
        if e == 0:
            return 0
        elif isinstance(e, (int, Fraction)):
            pc *= e
        else:
            sa.append(e)
    return pc if len(sa) == 0 else \
        sa[0] if len(sa) == 1 and pc == 1 else \
            Application('×', sa) if pc == 1 else \
                Application('×', [pc] + sa)


assert str(multiplication(3, 2)) == '6'
assert str(multiplication(3, 'x')) == '(3 × x)'
assert str(multiplication('x', 1)) == 'x'
assert str(multiplication('x', 'y')) == '(x × y)'
assert str(multiplication(3, 'x', 2, 'y', 4)) == '(24 × x × y)'
assert str(multiplication(multiplication('e', 'f', 2), multiplication('g', 3, 'h'))) == '(6 × e × f × g × h)'

def fractionaldivision(e: Expression, f: Expression) -> Expression:
    if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)):
        return Fraction(e) / f
    elif e == 0:
        return 0
    elif f == 1:
        return e
    else:
        return Application('/', [e, f])


assert str(fractionaldivision(6, 5)) == '6/5'
assert str(fractionaldivision('x', 'y')) == '(x / y)'
assert str(fractionaldivision(0, 'x')) == '0'
assert str(fractionaldivision('x', 1)) == 'x'

def integerdivision(e: Expression, f: Expression) -> Expression:
    if isinstance(e, int) and isinstance(f, int):
        return e // f
    elif e == 0:
        return 0
    elif f == 1:
        return e
    else:
        return Application('div', [e, f])


assert str(integerdivision(6, 5)) == '1'
assert str(integerdivision('x', 'y')) == '(x div y)'
assert str(integerdivision(0, 'x')) == '0'
assert str(integerdivision('x', 1)) == 'x'

def integermodulo(e: Expression, f: Expression) -> Expression:
    if isinstance(e, int) and isinstance(f, int):
        return e % f
    elif e == 0 or f == 1:
        return 0
    else:
        return Application('mod', [e, f])


assert str(integermodulo(6, 5)) == '1'
assert str(integermodulo('x', 'y')) == '(x mod y)'
assert str(integermodulo(0, 'x')) == '0'
assert str(integermodulo('x', 1)) == '0'

def conjunction(*el: Expression) -> Expression:
    sa = []  # simplified argument
    for e in iterate_associative_op('∧', *el):
        if e is False:
            return False
        elif e is not True and e not in sa:
            sa.append(e)
    return True if len(sa) == 0 else \
        sa[0] if len(sa) == 1 else \
            Application('∧', sa)


assert str(conjunction(True, True)) == 'True'
assert str(conjunction(True, 'e', True, 'f', 'e', True)) == '(e ∧ f)'
assert str(conjunction('e', False)) == 'False'
assert str(conjunction(conjunction('e', 'f', 'g'), conjunction('e', 'h'))) == '(e ∧ f ∧ g ∧ h)'

def disjunction(*el: Expression) -> Expression:
    sa = []  # simplified argument
    for e in iterate_associative_op('∨', *el):
        if e is True:
            return True
        elif e is not False and e not in sa:
            sa.append(e)
    return False if len(sa) == 0 else \
        sa[0] if len(sa) == 1 else \
            Application('∨', sa)


assert str(disjunction(False, 'e', False, 'f', 'e', False)) == '(e ∨ f)'
assert str(disjunction('e', True)) == 'True'
assert str(disjunction(disjunction('e', 'f', 'g'), disjunction('e', 'h'))) == '(e ∨ f ∨ g ∨ h)'

def implication(e: Expression, f: Expression) -> Expression:
    return True if e == f else \
           True if f is True else \
           negation(e) if f is False else \
           f if e is True else \
           True if e is False else \
           Application('⇒', [e, f])


assert str(implication('e', 'e')) == 'True'
assert str(implication('e', True)) == 'True'
assert str(implication('e', False)) == '¬ e'
assert str(implication(True, 'e')) == 'e'
assert str(implication(False, 'e')) == 'True'
assert str(implication('e', 'f')) == '(e ⇒ f)'

def consequence(e: Expression, f: Expression) -> Expression:
    return implication(f, e)

def equivalence(e: Expression, f: Expression) -> Expression:
    return equality(f, e)

def disequivalence(e: Expression, f: Expression) -> Expression:
    return disequality(f, e)

def equality(e: Expression, f: Expression) -> Expression:
    return True if e == f else \
           False if isinstance(e, (int, bool, Fraction)) and isinstance(f, (int, bool, Fraction)) and e != f else \
           e if f is True else \
           f if e is True else \
           negation(e) if f is False else \
           negation(f) if e is False else \
           Application('=', [e, f])


assert str(equality(Application('+', ['x', 'y', 'z']), Application('+', ['y', 'z', 'x']))) == 'True'
assert str(equality(3, 3)) == 'True'
assert str(equality('e', True)) == 'e'
assert str(equality(True, 'e')) == 'e'
assert str(equality('e', False)) == '¬ e'
assert str(equality(False, 'e')) == '¬ e'
assert str(equality('e', 'f')) == '(e = f)'

def disequality(e: Expression, f: Expression) -> Expression:
    return negation(equality(e, f))


assert str(disequality('e', False)) == 'e'

def lessequal(e: Expression, f: Expression) -> Expression:
    return True if e == f else \
           e <= f if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)) else \
           Application('≤', [e, f])


assert str(lessequal(7, 3)) == 'False'

def greaterequal(e: Expression, f: Expression) -> Expression:
    return True if e == f else \
           e >= f if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)) else \
           Application('≥', [e, f])


assert str(greaterequal(7, 3)) == 'True'

def less(e: Expression, f: Expression) -> Expression:
    return False if e == f else \
           e > f if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)) else \
           Application('<', [e, f])


assert str(less(3, 3)) == 'False'

def greater(e: Expression, f: Expression) -> Expression:
    return False if e == f else \
           e > f if isinstance(e, (int, Fraction)) and isinstance(f, (int, Fraction)) else \
           Application('>', [e, f])


assert str(greater('e', 'f')) == '(e > f)'

def member(e: Expression, f: Expression) -> Expression:
    if isinstance(f, Application) and f.fn == '{}':  # set enumeration
        if any(e == fi for fi in f.arg):
            return True
        elif len(f.arg) == 0:
            return False
        elif isinstance(e, int) and all(isinstance(fi, int) for fi in f.arg):
            return e in f.arg
        else:
            return Application('∈', [e, f])
    else:
        return Application('∈', [e, f])  # other set expression


e = Application('+', ['x', 'y'])
assert str(member(e, Application('{}', ['x', e, 'y']))) == 'True'
assert str(member(e, Application('{}', []))) == 'False'
assert str(member(3, Application('{}', [1, 7]))) == 'False'
assert str(member(e, Application('{}', ['x', 'y']))) == '((x + y) ∈ {x, y})'

def notmember(e: Expression, f: Expression) -> Expression:
    return negation(member(e, f))


assert str(notmember('x', Application('{}', ['x', 'y']))) == 'False'

def subsetequal(e: Expression, f: Expression) -> Expression:
    if isinstance(e, Application) and e.fn == '{}':
        if isinstance(f, Application) and f.fn == '{}':  # set enumeration
            if all(any(ei == fi for fi in f.arg) for ei in e.arg):
                return True
            elif all(isinstance(ei, int) for ei in e.arg) and all(isinstance(fi, int) for fi in f.arg):
                return False
            elif len(f.arg) == 0:
                return False
            else:
                return Application('⊆', [e, f])
        elif len(e.arg) == 0:
            return True
        else:
            return Application('⊆', [e, f])
    else:
        return Application('⊆', [e, f])  # other set expression


e = Application('+', ['x', 'y'])
assert str(subsetequal(Application('{}', [e, 'x']), Application('{}', ['x', e, 'y']))) == 'True'
assert str(subsetequal(Application('{}', [3]), Application('{}', [5]))) == 'False'
assert str(subsetequal(Application('{}', ['e']), Application('{}', []))) == 'False'
assert str(subsetequal(Application('{}', [e]), Application('{}', ['y']))) == '({x + y} ⊆ {y})'
assert str(subsetequal(Application('{}', []), 'e')) == 'True'