module Types where

import qualified Data.Set as S
import qualified Data.IntMap.Strict as IM
import Data.Bifunctor

import Text.ParserCombinators.ReadP
    ( char, munch1, option, readP_to_S )
import Data.Char ( isDigit )

-- type definitions
-- don't change the unmarked types

type EName = String
type Name = EName -- change as you like
data Polarity = Pos | Neg
  deriving (Eq)
data ELiteral = Literal Polarity EName
  deriving (Eq)
newtype Literal = SLiteral { unLiteral :: Int }
  deriving (Eq)
-- type Literal = ELiteral -- change as you like
type EClause = [ELiteral]
type Clause = S.Set Literal -- change as you like
type EConjForm = [EClause]
type ConjForm = S.Set Clause -- change as you like

type Key = Int
type EKeyClause = (Key, EClause)
type KeyClause = (Key, Clause) -- change as you like
type EKeyConjForm = [EKeyClause]
data KeyConjForm = KeyConjForm
  { kcfClauses :: S.Set Clause -- change as you like
  , kcfKeymap :: IM.IntMap Clause
  } deriving (Eq, Show)

data EResolve = Resolve EName Key Key
  deriving (Eq, Show, Read)
type Resolve = EResolve -- change as you like
type EValuation = [EName]
type Valuation = EValuation -- change as you like
data EProof = Refutation [EResolve] | Model EValuation
  deriving (Eq, Show, Read)
type Proof = EProof -- change as you like

type SelClauseStrategy = KeyConjForm -> Maybe KeyClause  -- change as you like

-- adapt the following if you changed the internal data types above

instance Show Polarity where
  show Pos = ""
  show Neg = "~"

instance Show ELiteral where
  show (Literal p a) = show p ++ a

instance Show Literal where
  show (SLiteral l)
    | l >= 0 = show l
    | otherwise = "~" ++ show (abs l)

instance Read ELiteral where
  readsPrec _ = readP_to_S $ do
    pol <- option Pos (Neg <$ char '~')
    name <- munch1 isDigit
    pure $ Literal pol name

instance Ord Polarity where
  Neg <= Pos = False
  _ <= _ = True

instance Ord ELiteral where
  (Literal p a) <= (Literal p' a') = a < a' || a == a' && p <= p'


instance Ord Literal where
  (SLiteral l1) <= (SLiteral l2) = abs l1 < abs l2 || abs l1 == abs l2 && not (signum l1 <= signum l2)


toEName :: Name -> EName
toEName = id

toName :: EName -> Name
toName = id

toELiteral :: Literal -> ELiteral
toELiteral (SLiteral i)
  | i >= 0    = Literal Pos (show i)
  | otherwise = Literal Neg (show $ abs i)

toLiteral :: ELiteral -> Literal
toLiteral (Literal Pos n) = SLiteral $        (read n :: Int)
toLiteral (Literal Neg n) = SLiteral $ negate (read n :: Int)

toEClause :: Clause -> EClause
toEClause = fmap toELiteral . S.toList

toClause :: EClause -> Clause
toClause = S.fromList . fmap toLiteral

toEConjForm :: ConjForm -> EConjForm
toEConjForm = fmap toEClause . S.toList

toConjForm :: EConjForm -> ConjForm
toConjForm = S.fromList . fmap toClause

toEKeyClause :: KeyClause -> EKeyClause
toEKeyClause (k, c) = (k, fmap toELiteral (S.toList c))

toKeyClause :: EKeyClause -> KeyClause
toKeyClause (k, c) = (k, S.fromList (fmap toLiteral c))

toEKeyConjForm :: KeyConjForm -> EKeyConjForm
toEKeyConjForm (KeyConjForm kcs kmap) = fmap toEKeyClause $ IM.toList kmap

toKeyConjForm :: EKeyConjForm -> KeyConjForm
toKeyConjForm ekcf = KeyConjForm (S.fromList . fmap (\(k, c) -> toClause c) $ ekcf) (IM.fromList $ fmap (second toClause) ekcf)

toEResolve :: Resolve -> EResolve
toEResolve = id

toResolve :: EResolve -> Resolve
toResolve = id

toEValuation :: Valuation -> EValuation
toEValuation = id

toValuation :: EValuation -> Valuation
toValuation = id

toEProof :: Proof -> EProof
toEProof = id

toProof :: EProof -> Proof
toProof = id