module Types where

import Data.HashSet as HashSet
import Data.Hashable (Hashable, hashWithSalt, hash)
-- 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
type Literal = ELiteral -- change as you like
type EClause = [ELiteral]
type Clause = HashSet Literal -- change as you like
type EConjForm = [EClause]
type ConjForm = [Clause] -- change as you like

type Key = Int
type EKeyClause = (Key, EClause)
type KeyClause = (Key, Clause) -- change as you like
type EKeyConjForm = [EKeyClause]
type KeyConjForm = [KeyClause] -- change as you like

data EResolve = Resolve EName Key Key
  deriving (Eq, Show)
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)
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

toEName :: Name -> EName
toEName = id

toName :: EName -> Name
toName = id

toELiteral :: Literal -> ELiteral
toELiteral = id

toLiteral :: ELiteral -> Literal
toLiteral = id

toEClause :: Clause -> EClause
toEClause = HashSet.toList

toClause :: EClause -> Clause
toClause = HashSet.fromList

toEConjForm :: ConjForm -> EConjForm
toEConjForm = Prelude.map toEClause

toConjForm :: EConjForm -> ConjForm
toConjForm = Prelude.map toClause

toEKeyClause :: KeyClause -> EKeyClause
toEKeyClause (key, cl) = (key, toEClause cl)

toKeyClause :: EKeyClause -> KeyClause
toKeyClause (key, cl) = (key, toClause cl)

toEKeyConjForm :: KeyConjForm -> EKeyConjForm
toEKeyConjForm = Prelude.map toEKeyClause

toKeyConjForm :: EKeyConjForm -> KeyConjForm
toKeyConjForm = Prelude.map toKeyClause

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


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

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

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 Hashable ELiteral where
  hashWithSalt s (Literal Pos val) = 7361 * hash val + s
  hashWithSalt s (Literal Neg val) = hash val + s