{-# LANGUAGE NoMonomorphismRestriction #-}

module MProver.Monad where

import MProver.Syntax

import Control.Monad.Reader
import Control.Monad.Error
import Control.Monad.Identity

import Unbound.LocallyNameless

import Data.Map (Map)
import qualified Data.Map as Map

type MPT m       = ErrorT String (ReaderT Environment (FreshMT m))
type ExprEnv     = Map (Name Expr) ((Maybe Ty),(Maybe Expr))
type ProofEnv    = Map (Name Proof) Formula
type DTEnv       = Map String (Bind [Name Ty] [ConstrDecl])
type CEnv        = Map String (Bind [Name Ty] ConstrDecl,String)
type Environment = (ExprEnv,ProofEnv,DTEnv,CEnv)

askEE :: (Monad m) => MPT m ExprEnv
askEE = do
          (ee,_,_,_) <- ask
          return ee

askPE :: (Monad m) => MPT m ProofEnv
askPE = do
          (_,pe,_,_) <- ask
          return pe

askDTE :: (Monad m) => MPT m DTEnv
askDTE = do
           (_,_,dte,_) <- ask
           return dte

askCE :: (Monad m) => MPT m CEnv
askCE = do
          (_,_,_,ce) <- ask
          return ce

localEE :: (Monad m) => (ExprEnv -> ExprEnv) -> MPT m a -> MPT m a
localEE f = local (\(ee,pe,dte,ce) -> (f ee,pe,dte,ce))

localPE :: (Monad m) => (ProofEnv -> ProofEnv) -> MPT m a -> MPT m a
localPE f = local (\(ee,pe,dte,ce) -> (ee,f pe,dte,ce))

localDTE :: (Monad m) => (DTEnv -> DTEnv) -> MPT m a -> MPT m a
localDTE f = local (\(ee,pe,dte,ce) -> (ee,pe,f dte,ce))

localCE :: (Monad m) => (CEnv -> CEnv) -> MPT m a -> MPT m a
localCE f = local (\(ee,pe,dte,ce) -> (ee,pe,dte,f ce))

unbindEnv = Map.delete
bindEnv = Map.insert