@@ -8,6 +8,7 @@ module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
88import Idris.Core.TT
99
1010import Control.Monad.State
11+import Control.Monad.Reader
1112import Data.Maybe
1213import Data.List hiding (partition)
1314import qualified Data.List(partition)
@@ -213,7 +214,11 @@ isUsed sc n = used sc where
213214 usedA (SucCase _ sc) = used sc
214215 usedA (DefaultCase sc) = used sc
215216
216−type CaseBuilder a = State CS a
217+type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found
218+type CaseBuilder a = ReaderT ErasureInfo (State CS) a
219+
220+runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
221+runCaseBuilder ei bld = runState $ runReaderT bld ei
217222
218223data Phase = CompileTime | RunTime
219224 deriving (Show, Eq)
@@ -244,7 +249,8 @@ simpleCase tc cover reflect phase fc inacc argtys cs
244249 let numargs = length (fst (head pats))
245250 ns = take numargs args
246251 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
247− (tree, st) = runState
252+ (tree, st) = runCaseBuilder
253+ undefined -- TODO
248254 (match ns' ps' (defaultCase cover))
249255 ([], numargs, [])
250256 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in