git.iko.soy/Idris-dev
on master help sign in
findUsed stub written.
437322cMatus Tejiscak
src/Idris/Erasure.hs+66−33
compare with master
unifiedsplit
@@ -5,21 +5,54 @@ module Idris.Erasure
5 ) where
5 ) where
6
6
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8−
9import Idris.Core.CaseTree
8import Idris.Core.CaseTree
10import Idris.Core.TT
9import Idris.Core.TT
10+import Idris.Core.Evaluate
11
11
12import Control.Applicative
12import Control.Applicative
13import Control.Monad.State
13import Control.Monad.State
14import Data.Maybe
14import Data.Maybe
15import Data.List
15import 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
17
49
18findUnusedArgs :: [Name] -> Idris ()
50findUnusedArgs :: [Name] -> Idris ()
19findUnusedArgs names = do
51findUnusedArgs names = do
20 cg <- idris_callgraph <$> getIState
52 cg <- idris_callgraph <$> getIState
21 mapM_ (process cg) names
53 mapM_ (process cg) names
22 where
54 where
55+ process :: Ctxt CGInfo -> Name -> Idris ()
23 process cg n = case lookupCtxt n cg of
56 process cg n = case lookupCtxt n cg of
24 [x] -> do
57 [x] -> do
25 let unused = traceUnused cg n x
58 let unused = traceUnused cg n x
@@ -27,38 +60,38 @@ findUnusedArgs names = do
27 addToCG n $ x{ unusedpos = unused }
60 addToCG n $ x{ unusedpos = unused }
28 _ -> return ()
61 _ -> return ()
29
62
30−traceUnused :: Ctxt CGInfo -> Name -> CGInfo -> [Int]
63+ traceUnused :: Ctxt CGInfo -> Name -> CGInfo -> [Int]
31−traceUnused cg n (CGInfo args calls _ usedns _)
64+ traceUnused cg n (CGInfo args calls _ usedns _)
32− = findIndices (not . (`elem` fused)) args
65+ = findIndices (not . (`elem` fused)) args
33− where
66+ where
34− fargs = concatMap (getFargpos calls) (zip args [0..])
67+ fargs = concatMap (getFargpos calls) (zip args [0..])
35− recused = [n | (n, i, (g,j)) <- fargs, used cg [(n,i)] g j]
68+ recused = [n | (n, i, (g,j)) <- fargs, used cg [(n,i)] g j]
36− fused = nub $ usedns ++ recused
69+ fused = nub $ usedns ++ recused
37−
70+
38−used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
71+ used :: Ctxt CGInfo -> [(Name, Int)] -> Name -> Int -> Bool
39−used cg path g j
72+ used cg path g j
40− | (g, j) `elem` path = False -- cycle, never used on the way
73+ | (g, j) `elem` path = False -- cycle, never used on the way
41
74
42− | [CGInfo args calls _ usedns _] <- lookupCtxt g cg
75+ | [CGInfo args calls _ usedns _] <- lookupCtxt g cg
43− , j < length args -- not overapplied
76+ , j < length args -- not overapplied
44− = let directuse = args!!j `elem` usedns
77+ = let directuse = args!!j `elem` usedns
45− garg = getFargpos calls (args!!j, j)
78+ garg = getFargpos calls (args!!j, j)
46− recused = map getUsed garg
79+ recused = map getUsed garg
47− in directuse || null recused || or recused
80+ in directuse || null recused || or recused
48− -- used on any route from here, or not used recursively
81+ -- used on any route from here, or not used recursively
49
82
50− | otherwise = True
83+ | otherwise = True
51− where
84+ where
52− getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
85+ getUsed (argn, j, (g', j')) = used cg ((g,j):path) g' j'
53
86
54−getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
87+ getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
55−getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
88+ getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
56− where
89+ where
57− getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
90+ getCallArgpos :: Name -> Int -> (Name, [[Name]]) -> [(Name, Int, (Name, Int))]
58− getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
91+ getCallArgpos n i (g, args) = mapMaybe (getOne g) (zip [0..] args)
59−
92+
60− getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
93+ getOne :: Name -> (Int, [Name]) -> Maybe (Name, Int, (Name, Int))
61− getOne g (j, xs)
94+ getOne g (j, xs)
62− | n `elem` xs = Just (n, i, (g, j))
95+ | n `elem` xs = Just (n, i, (g, j))
63− | otherwise = Nothing
96+ | otherwise = Nothing
64
97