module Types where

import Data.Map (Map, toList, fromList)
import Data.HashSet (HashSet, toList, fromList)
import Data.Hashable
import Data.Set (Set, toList, fromDistinctAscList)

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

type EName = String
type Name = EName -- change as you like
data Polarity = Pos | Neg
  deriving (Eq, Enum) --- changed (added enum)
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 = Set 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 = Map Int Clause -- 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

--- for hashing

instance Hashable Polarity where
  hashWithSalt = hashUsing fromEnum 

instance Hashable ELiteral where
  hashWithSalt s (Literal pol n) = s `hashWithSalt` 
                                  pol `hashWithSalt`n


toEName :: Name -> EName
toEName = id

toName :: EName -> Name
toName = id

toELiteral :: Literal -> ELiteral
toELiteral = id

toLiteral :: ELiteral -> Literal
toLiteral = id

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

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

toEConjForm :: ConjForm -> EConjForm
toEConjForm cnf = map toEClause $ Data.Set.toList cnf

toConjForm :: EConjForm -> ConjForm
toConjForm cnf = Data.Set.fromDistinctAscList $ map toClause cnf

toEKeyClause :: KeyClause -> EKeyClause
toEKeyClause (n, c) = (n, toEClause c) 

toKeyClause :: EKeyClause -> KeyClause
toKeyClause (n, c) = (n, toClause c) 

toEKeyConjForm :: KeyConjForm -> EKeyConjForm
toEKeyConjForm kcnf = map toEKeyClause $ Data.Map.toList kcnf

toKeyConjForm :: EKeyConjForm -> KeyConjForm
toKeyConjForm kcnf = Data.Map.fromList $ map toKeyClause kcnf

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