{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeSynonymInstances #-}
-- |A monad to manage the knowledge base.
module Chiou.Monad
    ( SkolemCount(..)
    , State(..)
    , FolModule
    , ProverT
    , zeroKB
    , runProverT
    ) where

import Control.Monad.State (MonadState, StateT, evalStateT, get, put)
import Chiou.NormalForm (ImplicativeNormalForm)

newtype SkolemCount = SkolemCount {unSkolemCount :: Int} deriving (Eq, Ord, Show)

instance Num SkolemCount where
    SkolemCount a + SkolemCount b = SkolemCount (a + b)
    SkolemCount a * SkolemCount b = SkolemCount (a * b)
    abs (SkolemCount a) = SkolemCount (abs a)
    signum (SkolemCount a) = SkolemCount (signum a)
    fromInteger = SkolemCount . fromInteger

instance Enum SkolemCount where
    toEnum = SkolemCount
    fromEnum = unSkolemCount

data State v p f
    = State { knowledgeBase ::[(ImplicativeNormalForm v p f, SkolemCount)]
            , skolemCount :: SkolemCount
            , modules :: [FolModule] }

zeroKB :: State v p f
zeroKB = State { knowledgeBase = []
               , skolemCount = 0
               , modules = [("user", SkolemCount 0)] }

type FolModule = (String, SkolemCount)

-- |A monad for running the knowledge base.
type ProverT v p f = StateT (State v p f)

runProverT :: Monad m => StateT (State v p f) m a -> m a
runProverT action = evalStateT action zeroKB

class MonadState (State v p f) m => Skolem v p f m where
    skolem :: m Int

instance Monad m => Skolem v p f (ProverT v p f m) where
    skolem =
        get >>= \ st ->
        put (st {skolemCount = skolemCount st + 1}) >>
        return (unSkolemCount (skolemCount st))