module Types where

import Data.List
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Set (Set)
import qualified Data.Set as 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
-- My Literal consists only of a name (= Int).
-- Pos/Neg are indicated by the sign of the name.
type Literal = Name -- change as you like
type EClause = [ELiteral]
type Clause = IntSet -- change as you like
type EConjForm = [EClause]
-- Use the index of the clause as key in order to be able to convert between
-- ConjForm and EConjForm.
type ConjForm = IntMap Clause -- change as you like

type Key = Int
type EKeyClause = (Key, EClause)
data KeyClause = KeyClause Key Clause -- change as you like
    deriving Show
instance Eq KeyClause where
    (==) (KeyClause _ c) (KeyClause _ c') = c == c'
instance Ord KeyClause where
    compare (KeyClause _ c) (KeyClause _ c') = compare c c'
type EKeyConjForm = [EKeyClause]
-- Map the clauses to their size (= number of literals).
-- Add the size of the clause to the KeyClause.
data SizeKeyClause = SizeKeyClause Int KeyClause
    deriving Show
instance Eq SizeKeyClause where
    (==) (SizeKeyClause s kc) (SizeKeyClause s' kc') = s == s' && kc == kc'
instance Ord SizeKeyClause where
    compare (SizeKeyClause s kc) (SizeKeyClause s' kc')
      | sdiff /= EQ = sdiff
      | otherwise  = compare kc kc'
        where sdiff = compare s s'
type KeyConjForm = Set SizeKeyClause -- change as you like

data EResolve = Resolve EName Key Key
  deriving (Eq, Show)
data MyResolve = MyResolve Name Key Key -- change as you like
    deriving (Eq, Ord, Show)
type Resolve = MyResolve
type EValuation = [EName]
type Valuation = IntSet -- change as you like
data EProof = Refutation [EResolve] | Model EValuation
  deriving (Eq, Show)
-- We need an IntMap for MyResolve in order to be able to remember the order
-- of the resolution steps!
data MyProof = MyRefutation [MyResolve] | MyModel Valuation -- change as you like
  deriving (Eq, Show)
type Proof = MyProof

type SelClauseStrategy = KeyConjForm -> (KeyClause, KeyConjForm)  -- 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 l | l < 0 = Literal Neg (toEName (abs l))
toELiteral l = Literal Pos (toEName l)

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

toEClause :: Clause -> EClause
toEClause = map toELiteral . IntSet.toList

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

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

toConjForm :: EConjForm -> ConjForm
toConjForm ecf = IntMap.fromAscList $ zip [0..length ecf] $ map toClause ecf

-- Our KeyClause is sorted by the size of the clauses, not by the "key"
-- (= index of the clauses)...
toEKeyClause :: KeyClause -> EKeyClause
toEKeyClause (KeyClause key clause) = (key, toEClause clause)

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

toEKeyConjForm :: KeyConjForm -> EKeyConjForm
toEKeyConjForm = sortOn fst . map (toEKeyClause . getKeyClause) . Set.toList
    where getKeyClause (SizeKeyClause _ kc) = kc

toKeyConjForm :: EKeyConjForm -> KeyConjForm
toKeyConjForm = Set.fromList . map (add_size . toKeyClause)
    where add_size (KeyClause key clause) = SizeKeyClause (IntSet.size clause) (KeyClause key clause)

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

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

toEValuation :: Valuation -> EValuation
toEValuation = map toEName . IntSet.toList

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

toEProof :: Proof -> EProof
toEProof (MyRefutation list) = Refutation (map toEResolve list)
toEProof (MyModel val) = Model (toEValuation val)

-- TODO: order of zip arguments?
toProof :: EProof -> Proof
toProof (Refutation list) = MyRefutation (map toResolve list)
toProof (Model val) = MyModel (toValuation val)

-- Some other conversion functions.

conjForm2KeyConjForm :: ConjForm -> KeyConjForm
conjForm2KeyConjForm = Set.fromList
                       . map (\(key, clause) -> SizeKeyClause (IntSet.size clause) (KeyClause key clause))
                       . IntMap.toList

keyConjForm2ConjForm :: KeyConjForm -> ConjForm
keyConjForm2ConjForm = IntMap.fromList . map getKeyClause . Set.toList
    where getKeyClause (SizeKeyClause _ (KeyClause key clause)) = (key, clause)