@@ -19,6 +19,7 @@ import IRTS.Inliner
1919
2020import Idris.AbsSyntax
2121import Idris.AbsSyntaxTree
22+import Idris.ASTUtils
2223import Idris.Erasure
2324import Idris.Error
2425
@@ -28,6 +29,9 @@ import Idris.Core.TT
2829import Idris.Core.Evaluate
2930import Idris.Core.CaseTree
3031
32+import Control.Category
33+import Prelude hiding (id, (.))
34+
3135import Control.Applicative
3236import Control.Monad.State
3337import Data.Maybe
@@ -172,10 +176,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
172176 (args, sc) = cases_runtime cd
173177
174178mkLDecl n (TyDecl (DCon tag arity) _) =
175− LConstructor n tag . erasedArity . lookup n <$> getIState
176− where
177− lookup n = lookupCtxtExact n . idris_callgraph
178− erasedArity = maybe 0 (length . usedpos)
179+ LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
179180
180181mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
181182mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -262,14 +263,13 @@ irTerm vs env tm@(App f a) = case unApply tm of
262263 ])
263264
264265 (P (DCon t arity) n _, args) -> do
265− ist <- getIState
266− let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267− used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268− args' = [a | (i,a) <- zip [0..] args, i `elem` used]
266+ detag <- fgetState (opt_detaggable . ist_optimisation n)
267+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
269268
270269 when (length args > arity) $
271270 ifail ("oversaturated data ctor: " ++ show tm)
272271
272+ let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
273273 if length args' == 1 && detag -- detaggable
274274 then irTerm vs env (head args') -- newtype
275275 else irCon vs env (length used) n args'
@@ -473,8 +473,8 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
473473irSC vs (Case n [alt]) = do
474474 replacement <- case alt of
475475 ConCase cn a ns sc -> do
476− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
477− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
476+ detag <- fgetState (opt_detaggable . ist_optimisation n)
477+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
478478 if detag && length used == 1
479479 then return . Just $ substSC (ns !! head used) n sc
480480 else return Nothing
@@ -505,13 +505,10 @@ irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
505505
506506-- this leaves out all unused arguments of the constructor
507507irAlt vs _ (ConCase n t args sc) = do
508− used <- getUsed . lookup n <$> getIState
508+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
509509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
510510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
511511 where
512− lookup n = lookupCtxtExact n . idris_callgraph
513− getUsed = maybe [] (map fst . usedpos)
514−
515512 methodVars = case n of
516513 SN (InstanceCtorN className)
517514 -> M.fromList [(v, VI