1
module Agda.Compiler.Alonzo.PatternMonad where
2
import Agda.Syntax.Internal
3
import Agda.TypeChecking.Monad.Base
5
import Control.Monad.State
6
import Control.Monad.Error
8
import qualified Data.Map
11
import Language.Haskell.Syntax
12
import Agda.TypeChecking.Monad
13
import Agda.Utils.Permutation
14
import Agda.Utils.Size
16
type Defs = Map QName Definition
25
initPState :: Clause -> Defs -> PState
26
initPState c@(Clause{ clausePerm = perm }) d = PSt
28
, vars = permute perm [0..]
34
type PM a = StateT PState TCM a
45
getPclause :: PM Clause
46
getPclause = gets clause
48
putPlst :: [HsPat] -> PM()
49
putPlst newlst = modify $ \s -> s { lst = newlst }
51
putPcnt :: Int -> PM()
52
putPcnt newcnt = modify $ \s -> s { cnt = newcnt }
55
incPcnt = modify $ \s -> s { cnt = 1 + cnt s }
60
putPlst $ lst++[HsPWildCard]
68
putPlst $ lst++[HsPVar(HsIdent ("v" ++ show v))]