module Types where
import Data.List
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
-- type definitions
-- don't change the unmarked types

data Polarity = Pos | Neg
  deriving Eq
type Key = Int

type EName = String
data ELiteral = Literal Polarity EName
  deriving Eq
type EClause = [ELiteral]
type EConjForm = [EClause]
type EKeyClause = (Key, EClause)
type EKeyConjForm = [EKeyClause]
data EResolve = Resolve EName Key Key
  deriving (Eq, Show)
type EValuation = [EName]
data EProof = Refutation [EResolve] | Model EValuation
  deriving (Eq, Show)


-- changed as I liked
type Name = EName
type Literal = ELiteral
--data Literal = Lit Polarity Name
--    deriving Eq
--instance Ord Literal where
--  (Lit p a) <= (Lit p' a') = a < a' || a == a' && p <= p'
--instance Show Literal where
--  show (Lit p a) = show p ++ show a

type Clause = Set.Set Literal
type ConjForm = Set.Set Clause
type KeyClause = (Key, Clause)
type KeyConjForm = Set.Set KeyClause
type Resolve = EResolve
type Valuation = [Name]

type Proof = EProof

type SelClauseStrategy = KeyConjForm -> Maybe KeyClause  -- change as you like

------------------------- Ord -------------------------

instance Ord Polarity where
  Neg <= Pos = False
  _ <= _ = True

instance Ord ELiteral where
  (Literal p a) <= (Literal p' a') = a < a' || a == a' && p <= p'

-- Ordered in the order i, k1, k2
instance Ord EResolve where
    (Resolve i1 k11 k12) <= (Resolve i2 k21 k22)
        | i1 < i2   = True 
        | i1 > i2   = False 
        | k11 < k21 = True 
        | k11 > k21 = False 
        | k12 <= k22    = True 
        | otherwise     = False
------------------------- Show -------------------------

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

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


-- 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
--toELiteral (Lit pol i) = Literal pol (show i)

toLiteral :: ELiteral -> Literal
toLiteral = id
--toLiteral (Literal pol n) = Lit pol (read n)

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

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

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

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

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

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

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

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

toEResolve :: Resolve -> EResolve
toEResolve = id

toResolve :: EResolve -> Resolve
toResolve = id

toEValuation :: Valuation -> EValuation
toEValuation = map toEName

toValuation :: EValuation -> Valuation
toValuation = id
--Refutation [EResolve] | Model EValuation
--Refugee [Resolve] | SuperModel Valuation
toEProof :: Proof -> EProof
toEProof = id

toProof :: EProof -> Proof
toProof = id
{-
conjFormToKeyConjForm :: ConjForm -> KeyConjForm
conjFormToKeyConjForm = zip [0..]
-}

keyConjFormToConjForm :: KeyConjForm -> ConjForm
keyConjFormToConjForm = Set.map snd