@@ -13,16 +13,24 @@ import 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.IntSet as S
16+import qualified Data.Set as S
17+import qualified Data.IntSet as IS
17import qualified Data.Map as M
18import qualified Data.Map as M
18import Data.IntSet (IntSet)
20import Data.IntSet (IntSet)
19import Data.Map (Map)
21import Data.Map (Map)
23+-- UseMap maps names to the set of used argument positions.
24+type UseMap = Map Name IntSet
26+-- PatvarMap maps pattern variable names to the corresponding (data-ctor-name, argpos).
27+type PatvarMap = Map Name (Name, Int)
21−findUsed :: Context -> Ctxt CGInfo -> [Name] -> Map Name IntSet
29+findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
22−findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
30+findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
24− union :: [Map Name IntSet] -> Map Name IntSet
32+ unionMap :: (a -> UseMap) -> [a] -> UseMap
25− union = M.unionsWith S.union
33+ unionMap f = M.unionsWith IS.union . map f
27 getDef :: Context -> Name -> Def
35 getDef :: Context -> Name -> Def
28 getDef ctx n = case lookupDef n ctx of
36 getDef ctx n = case lookupDef n ctx of
@@ -30,7 +38,7 @@ findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
30 [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
38 [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
31 _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
39 _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
33− findUsedDef :: Ctxt CGInfo -> Def -> Map Name IntSet
41+ findUsedDef :: Ctxt CGInfo -> Def -> UseMap
34 findUsedDef cg (Function ty t ) = M.empty
42 findUsedDef cg (Function ty t ) = M.empty
35 findUsedDef cg (TyDecl ty t ) = M.empty
43 findUsedDef cg (TyDecl ty t ) = M.empty
36 findUsedDef cg (Operator ty n f) = M.empty
44 findUsedDef cg (Operator ty n f) = M.empty
@@ -40,12 +48,30 @@ findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
40 -- the fst component is the list of pattern variables, which we don't use
48 -- 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?
49 = findUsedSC cg M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
43− findUsedSC :: Ctxt CGInfo -> Map Name (Name, Int) -> SC -> Map Name IntSet
51+ findUsedSC :: Ctxt CGInfo -> PatvarMap -> SC -> UseMap
44 findUsedSC cg vars ImpossibleCase = M.empty
52 findUsedSC cg vars ImpossibleCase = M.empty
45 findUsedSC cg vars (UnmatchedCase msg) = M.empty
53 findUsedSC cg vars (UnmatchedCase msg) = M.empty
46− findUsedSC cg vars (Case n alts) = undefined
54+ findUsedSC cg vars (Case n alts) = unionMap (findUsedAlt cg vars) alts
47− findUsedSC cg vars (ProjCase t alt) = undefined
55+ findUsedSC cg vars (ProjCase t alt) = findUsedAlt cg vars alt
48− findUsedSC cg vars (STerm t) = undefined
56+ findUsedSC cg vars (STerm t) = unionMap lookUp $ findUsedTerm cg t
58+ lookUp :: Name -> UseMap
59+ lookUp n = case M.lookup n vars of
60+ Just (cn, i) -> M.singleton cn (IS.singleton i)
63+ findUsedAlt :: Ctxt CGInfo -> PatvarMap -> CaseAlt -> UseMap
64+ findUsedAlt cg vars (FnCase n ns sc) = findUsedAlt cg vars sc -- TODO: what's this?
65+ findUsedAlt cg vars (ConstCase c sc) = findUsedAlt cg vars sc
66+ findUsedAlt cg vars (SucCase n sc) = findUsedAlt cg (M.insert n (error "put S here") vars) sc -- TODO
67+ findUsedAlt cg vars (DefaultCase sc) = findUsedAlt cg vars sc
68+ findUsedAlt cg vars (ConCase n cnt ns sc) = findUsedAlt cg (ns `u` vars) sc
70+ u :: [Name] -> PatvarMap -> PatvarMap
71+ vs `u` pmap = M.fromList [(var, (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
73+ findUsedTerm :: Ctxt CGInfo -> Term -> Set Name
74+ findUsedTerm cg t = undefined
50findUnusedArgs :: [Name] -> Idris ()
76findUnusedArgs :: [Name] -> Idris ()
51findUnusedArgs names = do
77findUnusedArgs names = do