@@ -5,21 +5,54 @@ module Idris.Erasure
55 ) where
66
77import Idris.AbsSyntax
8−
98import Idris.Core.CaseTree
109import Idris.Core.TT
10+import Idris.Core.Evaluate
1111
1212import Control.Applicative
1313import Control.Monad.State
1414import Data.Maybe
1515import Data.List
16−import qualified Data.Set as S
16+import qualified Data.IntSet as S
17+import qualified Data.Map as M
18+import Data.IntSet (IntSet)
19+import Data.Map (Map)
20+
21+findUsed :: Context -> Ctxt CGInfo -> [Name] -> Map Name IntSet
22+findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
23+ where
24+ union :: [Map Name IntSet] -> Map Name IntSet
25+ union = M.unionsWith S.union
26+
27+ getDef :: Context -> Name -> Def
28+ getDef ctx n = case lookupDef n ctx of
29+ [def] -> def
30+ [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
31+ _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
32+
33+ findUsedDef :: Ctxt CGInfo -> Def -> Map Name IntSet
34+ findUsedDef cg (Function ty t ) = M.empty
35+ findUsedDef cg (TyDecl ty t ) = M.empty
36+ findUsedDef cg (Operator ty n f) = M.empty
37+ -- ^- non-pattern-matching definitions don't contribute to usage of data
38+
39+ findUsedDef cg (CaseOp ci ty def tot cdefs)
40+ -- the fst component is the list of pattern variables, which we don't use
41+ = findUsedSC cg M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
42+
43+ findUsedSC :: Ctxt CGInfo -> Map Name (Name, Int) -> SC -> Map Name IntSet
44+ findUsedSC cg vars ImpossibleCase = M.empty
45+ findUsedSC cg vars (UnmatchedCase msg) = M.empty
46+ findUsedSC cg vars (Case n alts) = undefined
47+ findUsedSC cg vars (ProjCase t alts) = undefined
48+ findUsedSC cg vars (STerm t) = undefined
1749
1850findUnusedArgs :: [Name] -> Idris ()
1951findUnusedArgs names = do
2052 cg <- idris_callgraph <$> getIState
2153 mapM_ (process cg) names
2254 where
55+ process :: Ctxt CGInfo -> Name -> Idris ()
2356 process cg n = case lookupCtxt n cg of
2457 [x] -> do
2558 let unused = traceUnused cg n x
@@ -27,38 +60,38 @@ findUnusedArgs names = do
2760 addToCG n $ x{ unusedpos = unused }
2861 _ -> return ()
2962
30−traceUnused :: Ctxt CGInfo -> Name -> CGInfo -> [Int]
31−traceUnused cg n (CGInfo args calls _ usedns _)
32− = findIndices (not . (`elem` fused)) args
33− where
34− fargs = concatMap (getFargpos calls) (zip args [0..])
35− recused = [n | (n, i, (g,j)) <- fargs, used cg [(n,i)] g j]
36− fused = nub $ usedns ++ recused
37−
38−used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
39−used cg path g j
40− | (g, j) `elem` path = False -- cycle, never used on the way
63+ traceUnused :: Ctxt CGInfo -> Name -> CGInfo -> [Int]
64+ traceUnused cg n (CGInfo args calls _ usedns _)
65+ = findIndices (not . (`elem` fused)) args
66+ where
67+ fargs = concatMap (getFargpos calls) (zip args [0..])
68+ recused = [n | (n, i, (g,j)) <- fargs, used cg [(n,i)] g j]
69+ fused = nub $ usedns ++ recused
70+
71+ used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
72+ used cg path g j
73+ | (g, j) `elem` path = False -- cycle, never used on the way
4174
42− | [CGInfo args calls _ usedns _] <- lookupCtxt g cg
43− , j < length args -- not overapplied
44− = let directuse = args!!j `elem` usedns
45− garg = getFargpos calls (args!!j, j)
46− recused = map getUsed garg
47− in directuse || null recused || or recused
48− -- used on any route from here, or not used recursively
75+ | [CGInfo args calls _ usedns _] <- lookupCtxt g cg
76+ , j < length args -- not overapplied
77+ = let directuse = args!!j `elem` usedns
78+ garg = getFargpos calls (args!!j, j)
79+ recused = map getUsed garg
80+ in directuse || null recused || or recused
81+ -- used on any route from here, or not used recursively
4982
50− | otherwise = True
51− where
52− getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
83+ | otherwise = True
84+ where
85+ getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
5386
54−getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
55−getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
56− where
57− getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
58− getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
59−
60− getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
61− getOne g (j, xs)
62− | n `elem` xs = Just (n, i, (g, j))
63− | otherwise = Nothing
87+ getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
88+ getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
89+ where
90+ getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
91+ getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
92+
93+ getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
94+ getOne g (j, xs)
95+ | n `elem` xs = Just (n, i, (g, j))
96+ | otherwise = Nothing
6497