module Types where
import Data.List
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map

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

type EName = String
type Name = Int -- change as you like
--type Name = EName -- change as you like
data Polarity = Pos | Neg
  deriving Eq
data ELiteral = Literal Polarity EName
  deriving Eq
--type Literal = ELiteral
type Literal = Int 
--  deriving Eq-- change as you like
type EClause = [ELiteral]
--type Clause = [Literal]
type Clause = Set.Set Literal -- change as you like
type EConjForm = [EClause]
type ConjForm = Map.Map Int Clause-- change as you like
--type ConjForm = [Clause]

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

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

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
toEName = show

toName :: EName -> Name
--toName = id
toName = read

toELiteral :: Literal -> ELiteral
--toELiteral = id
toELiteral a = if a <= 0 then Literal Neg (toEName (-a)) else Literal Pos (toEName a)

toLiteral :: ELiteral -> Literal
--toLiteral = id
toLiteral (Literal Pos a) = (toName a)
toLiteral (Literal Neg a) = -(toName a)

toEClause :: Clause -> EClause
--toEClause = id
toEClause = map toELiteral . Set.toList

toClause :: EClause -> Clause
--toClause = id
toClause = Set.fromList . map toLiteral

toEConjForm :: ConjForm -> EConjForm
--toEConjForm = id
toEConjForm = map (toEClause . snd) . Map.toAscList

toConjForm :: EConjForm -> ConjForm
--toConjForm = id
toConjForm xs = Map.fromAscList $ (zip [0..length xs - 1] . map toClause) xs

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

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

toEKeyConjForm :: KeyConjForm -> EKeyConjForm
--toEKeyConjForm = id
toEKeyConjForm = map toEKeyClause . Map.toAscList

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

toEResolve :: Resolve -> EResolve
--toEResolve = id
toEResolve (R n k1 k2)= (Resolve (toEName n) k1 k2)

toResolve :: EResolve -> Resolve
--toResolve = id
toResolve (Resolve n k1 k2) = (R (toName n) k1 k2) 

toEValuation :: Valuation -> EValuation
--toEValuation = id
toEValuation = map toEName . Set.toList

toValuation :: EValuation -> Valuation
toValuation = Set.fromList . map toName

toEProof :: Proof -> EProof
--toEProof = id
toEProof (Ref x) = (Refutation (map toEResolve x)) 
toEProof (M x) = (Model (toEValuation x)) 

toProof :: EProof -> Proof
--toProof = id
toProof (Refutation x) = (Ref (map toResolve x))
toProof (Model x) = (M (toValuation x))