@@ -19,6 +19,7 @@ import IRTS.Inliner
20import Idris.AbsSyntax
20import Idris.AbsSyntax
21import Idris.AbsSyntaxTree
21import Idris.AbsSyntaxTree
22import Idris.Erasure
23import Idris.Erasure
23import Idris.Error
24import Idris.Error
@@ -28,6 +29,9 @@ import Idris.Core.TT
28import Idris.Core.Evaluate
29import Idris.Core.Evaluate
29import Idris.Core.CaseTree
30import Idris.Core.CaseTree
32+import Control.Category
33+import Prelude hiding (id, (.))
31import Control.Applicative
35import Control.Applicative
32import Control.Monad.State
36import Control.Monad.State
33import Data.Maybe
37import Data.Maybe
@@ -172,10 +176,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
172 (args, sc) = cases_runtime cd
176 (args, sc) = cases_runtime cd
174mkLDecl n (TyDecl (DCon tag arity) _) =
178mkLDecl n (TyDecl (DCon tag arity) _) =
175− LConstructor n tag . erasedArity . lookup n <$> getIState
179+ LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
177− lookup n = lookupCtxtExact n . idris_callgraph
178− erasedArity = maybe 0 (length . usedpos)
180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
181mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
182mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -262,14 +263,13 @@ irTerm vs env tm@(App f a) = case unApply tm of
264 (P (DCon t arity) n _, args) -> do
265 (P (DCon t arity) n _, args) -> do
265− ist <- getIState
266+ detag <- fgetState (opt_detaggable . ist_optimisation n)
266− let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
267− used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268− args' = [a | (i,a) <- zip [0..] args, i `elem` used]
270 when (length args > arity) $
269 when (length args > arity) $
271 ifail ("oversaturated data ctor: " ++ show tm)
270 ifail ("oversaturated data ctor: " ++ show tm)
272+ let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
273 if length args' == 1 && detag -- detaggable
273 if length args' == 1 && detag -- detaggable
274 then irTerm vs env (head args') -- newtype
274 then irTerm vs env (head args') -- newtype
275 else irCon vs env (length used) n args'
275 else irCon vs env (length used) n args'
@@ -473,8 +473,8 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
473irSC vs (Case n [alt]) = do
473irSC vs (Case n [alt]) = do
474 replacement <- case alt of
474 replacement <- case alt of
475 ConCase cn a ns sc -> do
475 ConCase cn a ns sc -> do
476− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
476+ detag <- fgetState (opt_detaggable . ist_optimisation n)
477− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
477+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
478 if detag && length used == 1
478 if detag && length used == 1
479 then return . Just $ substSC (ns !! head used) n sc
479 then return . Just $ substSC (ns !! head used) n sc
480 else return Nothing
480 else return Nothing
@@ -505,13 +505,10 @@ irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
506-- this leaves out all unused arguments of the constructor
506-- this leaves out all unused arguments of the constructor
507irAlt vs _ (ConCase n t args sc) = do
507irAlt vs _ (ConCase n t args sc) = do
508− used <- getUsed . lookup n <$> getIState
508+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
512− lookup n = lookupCtxtExact n . idris_callgraph
513− getUsed = maybe [] (map fst . usedpos)
515 methodVars = case n of
512 methodVars = case n of
516 SN (InstanceCtorN className)
513 SN (InstanceCtorN className)
517 -> M.fromList [(v, VI
514 -> M.fromList [(v, VI