#  CookieJar ADT: Python Abstract Interface (Standard Mutable)
#
# 345678901234567890123456789012345678901234567890123456789012345678901234567890
#

# 2018-10-10: Initial Python version loosely based on Scala version
# 2018-10-12: Corrected/improved statement of model, contracts
# 2022-04-19: Improved comments.

# MODEL: The state of each CookieJar instance 'self' is specified by an
# abstract variable Bag(self). The value of this variable is a mathematical bag
# (multiset) containing the items of type CookieType that are in the cookie jar
# at that point in execution.
#
# INTERFACE INVARIANT:  Bag(self) != UNDEFINED
#
# NOTE: An invariant must apply to all instances of a data type --- those
# passed as explicit or implicit arguments to methods (functions and
# procedures), created by constructors, or returned by mutator and accessor
# functions. It must be made true by the data type (class) constructors and
# each public accessor and mutator methods must preserve it. It is both a
# precondition and a postcondition on all mutator and accessor methods. An
# interface invariant refers only to the model, not to the data structures or
# any concrete implementation.

from typing import Generic, TypeVar
from abc import ABC, abstractmethod

CookieType = TypeVar("CookieType")

# The abstract base class CookieJarABC defines the abstract interface to the
# family of Python Cookie Jar implementations. CookieJarABC has a generic type
# parameter CookieType for the type of the cookies in the CookieJar ADT.


class CookieJarABC(ABC, Generic[CookieType]):

    # The Dale and Walker book defines an operation Create. A Python class
    # implementing this ADT should extend this abstract class and provide an
    # __init__ method (and/or other "constructor" methods) that create an empty
    # cookie jar. That is, they must satisfy the following specification.
    #
    # PRE:   True
    # POST:  Bag(self') == {| |}

    # Mutator method put_in(cookie) adds cookie to the cookie jar.
    # It is called PutIn in the Dale and Walker book.
    #
    # PRE:  True
    # POST: Bag(self') == Bag(self) SUM {| cookie |}

    @abstractmethod
    def put_in(self, cookie: CookieType) -> None:
        pass

    # Mutator method eat(cookie) removes cookie from the cookie jar
    # It is called Eat in the Dale and Walker book.
    #
    # PRE:  has(cookie)
    # POST: Bag(self') == Bag(self) DIFF {| cookie |}

    @abstractmethod
    def eat(self, cookie: CookieType) -> None:
        pass

    # Accessor method is_empty() returns True iff the cookie jar
    # is empty. It is called IsEmpty in the Dale and Walker book.
    #
    # PRE:   True
    # POST:  (Result == (Bag(self) == {| |})) &&
    #        (Bag(self') == Bag(self))

    @abstractmethod
    def is_empty(self) -> bool:
        pass

    # Accessor method has(cookie) returns True iff cookie occurs
    # in the cookie jar. It is called IsIn in the Dale and Walker
    # book.
    #
    # PRE:   True
    # POST:  (Result == (cookie IN Bag(self)))
    #        && (Bag(self') == Bag(self))

    @abstractmethod
    def has(self, cookie: CookieType) -> bool:
        pass

    # Classes that implement CookieJar may want to define "__repr__"
    # (or "__str__") and/or "__eq___" appropriately.