module Types where

import Data.HashSet (HashSet, fromList, toList)
import Data.Hashable (Hashable, hashWithSalt)

-- 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 = HashSet Clause -- change as you like

instance Hashable Polarity where
    hashWithSalt salt pol = hashWithSalt salt (pol == Pos)

instance Hashable ELiteral where
    hashWithSalt salt (Literal pol name) = hashWithSalt salt (pol, name)


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

instance Eq KeyClause where
    (KeyClause _ clause1) == (KeyClause _ clause2) =
        clause1 == clause2

instance Hashable KeyClause where
    hashWithSalt salt (KeyClause _ clause) =
        hashWithSalt salt clause


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

instance Hashable EResolve where
    hashWithSalt salt (Resolve name key1 key2) =
        hashWithSalt salt (name, (key1, key2))

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 = toList

toClause :: EClause -> Clause
toClause = fromList

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

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

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

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

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

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

toEResolve :: Resolve -> EResolve
toEResolve = id

toResolve :: EResolve -> Resolve
toResolve = id

toEValuation :: Valuation -> EValuation
toEValuation = toList

toValuation :: EValuation -> Valuation
toValuation = fromList

-- data Proof = Ref [Resolve] | Mod Valuation

toEProof :: Proof -> EProof
toEProof (Ref steps) = Refutation steps
toEProof (Mod val)   = Model (toEValuation val)

toProof :: EProof -> Proof
toProof (Refutation steps)  = Ref steps
toProof (Model eval) = Mod (toValuation eval)