module Agda.Compiler.Alonzo.PatternMonad where
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base

import Control.Monad.State
import Control.Monad.Error

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

import Language.Haskell.Syntax
import Agda.TypeChecking.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size

type Defs =  Map QName Definition
data PState = PSt
  { cnt :: Int
  , vars :: [Int]
  , lst :: [HsPat]
  , clause :: Clause
  , defs :: Defs
  }

initPState :: Clause -> Defs -> PState
initPState c@(Clause{ clausePerm = perm }) d = PSt
  { cnt = 0
  , vars = permute perm [0..]
  , lst = []
  , clause = c
  , defs = d
  }

type PM a = StateT PState TCM a

getPDefs :: PM Defs
getPDefs = gets defs

getPcnt :: PM Int
getPcnt = gets cnt

getPlst :: PM [HsPat]
getPlst = gets lst

getPclause :: PM Clause
getPclause = gets clause

putPlst :: [HsPat] -> PM()
putPlst newlst = modify $ \s -> s { lst = newlst }

putPcnt :: Int -> PM()
putPcnt newcnt = modify $ \s -> s { cnt = newcnt }

incPcnt :: PM()
incPcnt = modify $ \s -> s { cnt = 1 + cnt s }

addWildcard :: PM()
addWildcard = do
        lst <- getPlst
        putPlst $ lst++[HsPWildCard]

addVar :: PM()
addVar = do
        lst <- getPlst
        s <- get
        let v : vs = vars s
        put $ s { vars = vs }
        putPlst $ lst++[HsPVar(HsIdent ("v" ++ show v))]