@@ -8,6 +8,7 @@ module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
8import Idris.Core.TT
8import Idris.Core.TT
10import Control.Monad.State
10import Control.Monad.State
11+import Control.Monad.Reader
11import Data.Maybe
12import Data.Maybe
12import Data.List hiding (partition)
13import Data.List hiding (partition)
13import qualified Data.List(partition)
14import qualified Data.List(partition)
@@ -213,7 +214,11 @@ isUsed sc n = used sc where
213 usedA (SucCase _ sc) = used sc
214 usedA (SucCase _ sc) = used sc
214 usedA (DefaultCase sc) = used sc
215 usedA (DefaultCase sc) = used sc
217+type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found
216−type CaseBuilder a = State CS a
218+type CaseBuilder a = ReaderT ErasureInfo (State CS) a
220+runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
221+runCaseBuilder ei bld = runState $ runReaderT bld ei
218data Phase = CompileTime | RunTime
223data Phase = CompileTime | RunTime
219 deriving (Show, Eq)
224 deriving (Show, Eq)
@@ -244,7 +249,8 @@ simpleCase tc cover reflect phase fc inacc argtys cs
244 let numargs = length (fst (head pats))
249 let numargs = length (fst (head pats))
245 ns = take numargs args
250 ns = take numargs args
246 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
251 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
247− (tree, st) = runState
252+ (tree, st) = runCaseBuilder
248 (match ns' ps' (defaultCase cover))
254 (match ns' ps' (defaultCase cover))
249 ([], numargs, [])
255 ([], numargs, [])
250 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
256 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in