module Types where

import Data.Set

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

type EName = String

type Name = Int -- change as you like

data Polarity = Pos | Neg
  deriving (Eq)

data ELiteral = Literal Polarity EName
  deriving (Eq)

data Literal = Lit Polarity Int -- change as you like
  deriving (Eq)

instance Ord Literal where
  (Lit p n) <= (Lit q m) = n < m || (n == m && (p == q || q == Pos))
  (Lit p n) < (Lit q m) = n < m || (n == m && p == Neg && q == Pos)

type EClause = [ELiteral]

type Clause = Set Literal -- change as you like

type EConjForm = [EClause]

type ConjForm = [Clause] -- change as you like

type Key = Int

type EKeyClause = (Key, EClause)

data KeyClause = Kc Key Clause -- change as you like

getClause :: KeyClause -> Clause
getClause (Kc _ c) = c

instance Eq KeyClause where
  (Kc _ c) == (Kc _ d) = c == d

instance Ord KeyClause where
  (Kc _ c) <= (Kc _ d) = size c <= size d
  (Kc _ c) < (Kc _ d) = size c < size d

type EKeyConjForm = [EKeyClause]

type KeyConjForm = [KeyClause] -- change as you like

data EResolve = Resolve EName Key Key
  deriving (Eq, Show)

data Resolve = Res Name Key Key -- change as you like
  deriving (Eq, Show)

type EValuation = [EName]

type Valuation = [Name] -- change as you like

data EProof = Refutation [EResolve] | Model EValuation
  deriving (Eq, Show)

data Proof = Ref [Resolve] | Mod Valuation -- change as you like
  deriving (Eq, Show)

type SelClauseStrategy = Set KeyClause -> (KeyClause, Set KeyClause) -- change as you like

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

toEName :: Name -> EName
toEName = show

toName :: EName -> Name
toName = read

toELiteral :: Literal -> ELiteral
toELiteral (Lit p n) = Literal p (toEName n)

toLiteral :: ELiteral -> Literal
toLiteral (Literal p n) = Lit p (toName n)

toEClause :: Clause -> EClause
toEClause = Prelude.map toELiteral . elems

toClause :: EClause -> Clause
toClause = fromList . Prelude.map toLiteral

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

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

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

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

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

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

toEResolve :: Resolve -> EResolve
toEResolve (Res n k l) = Resolve (toEName n) k l

toResolve :: EResolve -> Resolve
toResolve (Resolve n k l) = Res (toName n) k l

toEValuation :: Valuation -> EValuation
toEValuation = Prelude.map toEName

toValuation :: EValuation -> Valuation
toValuation = Prelude.map toName

toEProof :: Proof -> EProof
toEProof (Ref rs) = Refutation (Prelude.map toEResolve rs)
toEProof (Mod val) = Model (Prelude.map toEName val)

toProof :: EProof -> Proof
toProof (Refutation rs) = Ref (Prelude.map toResolve rs)
toProof (Model val) = Mod (Prelude.map toName val)