#!/usr/bin/env python3
# -*- coding: utf-8 -*-
#
# This file is part of ltlf2dfa.
#
# ltlf2dfa is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# ltlf2dfa is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
#

"""This module contains the implementation of Linear Temporal Logic on finite traces."""

import re
from abc import ABC, abstractmethod
from typing import Any, List, Optional

from ltlf2dfa.base import (
    AtomicFormula,
    AtomSymbol,
    BinaryOperator,
    Formula,
    UnaryOperator,
)
from ltlf2dfa.helpers import new_var
from ltlf2dfa.ltlf2dfa import to_dfa
from ltlf2dfa.pl import PLAtomic
from ltlf2dfa.symbols import OpSymbol, Symbols


class LTLfFormula(Formula, ABC):
    """A class for the LTLf formula."""

    def to_nnf(self) -> "LTLfFormula":
        """Convert an LTLf formula in NNF."""
        return self

    @abstractmethod
    def negate(self) -> "LTLfFormula":
        """Negate the formula."""

    def __repr__(self):
        """Get the representation."""
        return self.__str__()

    def to_mona(self, v: Optional[Any] = None) -> str:
        """
        Tranform the LTLf formula into its encoding in MONA.

        :return: a string.
        """
        raise NotImplementedError()

    def to_ldlf(self):
        """
        Tranform the formula into an equivalent LDLf formula.

        :return: an LDLf formula.
        """

    def to_dfa(self, mona_dfa_out: bool = False) -> str:
        """
        Translate into a DFA.

        :param mona_dfa_out: flag for DFA output in MONA syntax.
        """
        return to_dfa(self, mona_dfa_out)


class LTLfUnaryOperator(UnaryOperator[LTLfFormula], LTLfFormula, ABC):
    """A unary operator for LTLf."""


class LTLfBinaryOperator(BinaryOperator[LTLfFormula], LTLfFormula, ABC):
    """A binary operator for LTLf."""


class LTLfAtomic(AtomicFormula, LTLfFormula):
    """Class for LTLf atomic formulas."""

    name_regex = re.compile(r"[a-z][a-z0-9_]*")

    def negate(self):
        """Negate the formula."""
        return LTLfNot(self)

    def find_labels(self) -> List[AtomSymbol]:
        """Find the labels."""
        return PLAtomic(self.s).find_labels()

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf atomic formula."""
        if v != "0":
            return f"({v} in {self.s.upper()})"
        return PLAtomic(self.s).to_mona()

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfDiamond(RegExpPropositional(PLAtomic(self.s)), LDLfLogicalTrue())


class LTLfTrue(LTLfAtomic):
    """Class for the LTLf True formula."""

    def __init__(self):
        """Initialize the formula."""
        super().__init__(Symbols.TRUE.value)

    def negate(self):
        """Negate the formula."""
        return LTLfFalse()

    def find_labels(self) -> List[AtomSymbol]:
        """Find the labels."""
        return []

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding for False."""
        return Symbols.TRUE.value

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfDiamond(RegExpPropositional(PLTrue()), LDLfLogicalTrue())


class LTLfFalse(LTLfAtomic):
    """Class for the LTLf False formula."""

    def __init__(self):
        """Initialize the formula."""
        super().__init__(Symbols.FALSE.value)

    def negate(self):
        """Negate the formula."""
        return LTLfTrue()

    def find_labels(self) -> List[AtomSymbol]:
        """Find the labels."""
        return []

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding for False."""
        return Symbols.FALSE.value


class LTLfNot(LTLfUnaryOperator):
    """Class for the LTLf not formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.NOT.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        if not isinstance(self.f, AtomicFormula):
            return self.f.negate().to_nnf()
        return self

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.f

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Not formula."""
        return f"~({self.f.to_mona(v)})"

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfNot(self.f.to_ldlf())


class LTLfAnd(LTLfBinaryOperator):
    """Class for the LTLf And formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.AND.value

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return LTLfOr([f.negate() for f in self.formulas])

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf And formula."""
        return f"({' & '.join([f.to_mona(v) for f in self.formulas])})"

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfAnd([f.to_ldlf() for f in self.formulas])


class LTLfOr(LTLfBinaryOperator):
    """Class for the LTLf Or formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.OR.value

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return LTLfAnd([f.negate() for f in self.formulas])

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Or formula."""
        return f"({' | '.join([f.to_mona(v) for f in self.formulas])})"

    # def to_ldlf(self):
    #     """Convert LTLf formula to LDLf."""
    #     return LDLfOr([f.to_ldlf() for f in self.formulas])


class LTLfImplies(LTLfBinaryOperator):
    """Class for the LTLf Implication formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.IMPLIES.value

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        first, second = self.formulas[0:2]
        final_formula = LTLfOr([LTLfNot(first).to_nnf(), second.to_nnf()])
        for subformula in self.formulas[2:]:
            final_formula = LTLfOr(
                [LTLfNot(final_formula).to_nnf(), subformula.to_nnf()]
            )
        return final_formula

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Implication formula."""
        return self.to_nnf().to_mona(v)

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     f1 = (
    #         LTLfImplies(self.formulas[:-1]).to_ldlf()
    #         if len(self.formulas) > 2
    #         else self.formulas[0].to_ldlf()
    #     )
    #     f2 = self.formulas[-1].to_ldlf()
    #     return LDLfOr([LDLfNot(f1), f2])


class LTLfEquivalence(LTLfBinaryOperator):
    """Class for the LTLf Equivalente formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.EQUIVALENCE.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        fs = self.formulas
        pos = LTLfAnd(fs)
        neg = LTLfAnd([LTLfNot(f) for f in fs])
        res = LTLfOr([pos, neg]).to_nnf()
        return res

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Equivalence formula."""
        return self.to_nnf().to_mona(v)

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     f1 = (
    #         LTLfImplies(self.formulas[:-1]).to_ldlf()
    #         if len(self.formulas) > 2
    #         else self.formulas[0].to_ldlf()
    #     )
    #     f2 = self.formulas[-1].to_ldlf()
    #     return LDLfAnd([LDLfOr([LDLfNot(f1), f2]), LDLfOr([f1, LDLfNot(f2)])])


class LTLfNext(LTLfUnaryOperator):
    """Class for the LTLf Next formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.NEXT.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfNext(self.f.to_nnf())

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return LTLfWeakNext(self.f.negate())

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Next formula."""
        ex_var = new_var(v)
        if v != "0":
            return f"(ex1 {ex_var}: {ex_var} in $ & {ex_var}={v}+1 & {self.f.to_mona(ex_var)})"
        return f"(ex1 {ex_var}: {ex_var} in $ & {ex_var}=1 & {self.f.to_mona(ex_var)})"

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfDiamond(
    #         RegExpPropositional(PLTrue()),
    #         LDLfAnd([self.f.to_ldlf(), LDLfNot(LDLfEnd())]),
    #     )


class LTLfWeakNext(LTLfUnaryOperator):
    """Class for the LTLf Weak Next formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.WEAK_NEXT.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfWeakNext(self.f.to_nnf())

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return LTLfNext(self.f.negate())

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf WeakNext formula."""
        ex_var = new_var(v)
        if v != "0":
            return f"(({v} = max($)) | (ex1 {ex_var}: {ex_var} in $ & {ex_var}={v}+1 & {self.f.to_mona(ex_var)}))"
        return f"((0 = max($)) | (ex1 {ex_var}: {ex_var} in $ & {ex_var}=1 & {self.f.to_mona(ex_var)}))"

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfBox(
    #         RegExpPropositional(PLTrue()), LDLfOr([self.f.to_ldlf(), LDLfEnd()])
    #     )


class LTLfUntil(LTLfBinaryOperator):
    """Class for the LTLf Until formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.UNTIL.value

    def to_nnf(self):
        """Transform to NNF."""
        return LTLfUntil([f.to_nnf() for f in self.formulas])

    def negate(self):
        """Negate the formula."""
        return LTLfRelease([f.negate() for f in self.formulas])

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Until formula."""
        ex_var = new_var(v)
        all_var = new_var(ex_var)
        f1 = self.formulas[0].to_mona(v=all_var)
        f2 = (
            LTLfUntil(self.formulas[1:]).to_mona(v=ex_var)
            if len(self.formulas) > 2
            else self.formulas[1].to_mona(v=ex_var)
        )
        return (
            f"(ex1 {ex_var}: {ex_var} in $ & {v}<={ex_var}&{ex_var}<=max($) & {f2} & "
            f"(all1 {all_var}: {all_var} in $ & {v}<={all_var}&{all_var}<{ex_var} => {f1}))"
        )

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     f1 = self.formulas[0].to_ldlf()
    #     f2 = (
    #         LTLfUntil(self.formulas[1:]).to_ldlf()
    #         if len(self.formulas) > 2
    #         else self.formulas[1].to_ldlf()
    #     )
    #     return LDLfDiamond(
    #         RegExpStar(RegExpSequence([RegExpTest(f1), RegExpPropositional(PLTrue())])),
    #         LDLfAnd([f2, LDLfNot(LDLfEnd())]),
    #     )


class LTLfRelease(LTLfBinaryOperator):
    """Class for the LTLf Release formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.RELEASE.value

    def to_nnf(self):
        """Transform to NNF."""
        return LTLfRelease([f.to_nnf() for f in self.formulas])

    def negate(self):
        """Negate the formula."""
        return LTLfUntil([f.negate() for f in self.formulas])

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Release formula."""
        ex_var = new_var(v)
        all_var = new_var(ex_var)
        f1 = self.formulas[0].to_mona(v=ex_var)
        f2 = (
            LTLfRelease(self.formulas[1:]).to_mona(v=all_var)
            if len(self.formulas) > 2
            else self.formulas[1].to_mona(v=all_var)
        )
        return (
            f"((ex1 {ex_var}: {ex_var} in $ & {v}<={ex_var}&{ex_var}<=max($) & {f1} & "
            f"(all1 {all_var}: {all_var} in $ & {v}<={all_var}&{all_var}<={ex_var} => {f2})) | (all1 {all_var}: "
            f"{all_var} in $ & {v}<={all_var}&{all_var}<=max($) => {f2}))"
        )

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     f1 = self.formulas[0].to_ldlf()
    #     f2 = (
    #         LTLfRelease(self.formulas[1:]).to_ldlf()
    #         if len(self.formulas) > 2
    #         else self.formulas[1].to_ldlf()
    #     )
    #     return LDLfBox(
    #         RegExpStar(
    #             RegExpSequence([RegExpTest(LDLfNot(f1)), RegExpPropositional(PLTrue())])
    #         ),
    #         LDLfOr([f2, LDLfEnd()]),
    #     )


class LTLfEventually(LTLfUnaryOperator):
    """Class for the LTLf Eventually formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.EVENTUALLY.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfUntil([LTLfTrue(), self.f])

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Eventually formula."""
        return LTLfUntil([LTLfTrue(), self.f]).to_mona(v)

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfDiamond(
    #         RegExpStar(RegExpPropositional(PLTrue())),
    #         LDLfAnd([self.f.to_ldlf(), LDLfNot(LDLfEnd())]),
    #     )


class LTLfAlways(LTLfUnaryOperator):
    """Class for the LTLf Always formula."""

    @property
    def operator_symbol(self) -> OpSymbol:
        """Get the operator symbol."""
        return Symbols.ALWAYS.value

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfRelease([LTLfFalse(), self.f.to_nnf()])

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Always formula."""
        return LTLfRelease([LTLfFalse(), self.f]).to_mona(v)

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfBox(
    #         RegExpStar(RegExpPropositional(PLTrue())),
    #         LDLfOr([self.f.to_ldlf(), LDLfEnd()]),
    #     )


class LTLfLast(LTLfFormula):
    """Class for the LTLf Last formula."""

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfAnd([LTLfWeakNext(LTLfFalse()), LTLfNot(LTLfEnd())]).to_nnf()

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def find_labels(self) -> List[AtomSymbol]:
        """Find the labels."""
        return []

    def _members(self):
        return (Symbols.LAST.value,)

    def __str__(self):
        """Get the string representation."""
        return Symbols.LAST.value

    def to_mona(self, v="0") -> str:
        """Return the MONA encoding of an LTLf Last formula."""
        return LTLfWeakNext(LTLfFalse()).to_mona(v)

    # def to_ldlf(self):
    #     """Convert the formula to LDLf."""
    #     return LDLfDiamond(RegExpPropositional(PLTrue()), LDLfEnd())


class LTLfEnd(LTLfFormula):
    """Class for the LTLf End formula."""

    def find_labels(self) -> List[AtomSymbol]:
        """Find the labels."""
        return []

    def _members(self):
        return (Symbols.END.value,)

    def to_nnf(self) -> LTLfFormula:
        """Transform to NNF."""
        return LTLfAlways(LTLfFalse()).to_nnf()

    def negate(self) -> LTLfFormula:
        """Negate the formula."""
        return self.to_nnf().negate()

    def __str__(self):
        """Get the string representation."""
        return "_".join(map(str, self._members()))
