@@ -13,16 +13,24 @@ import Control.Applicative
1313import Control.Monad.State
1414import Data.Maybe
1515import Data.List
16−import qualified Data.IntSet as S
16+import qualified Data.Set as S
17+import qualified Data.IntSet as IS
1718import qualified Data.Map as M
19+import Data.Set (Set)
1820import Data.IntSet (IntSet)
1921import Data.Map (Map)
2022
21−findUsed :: Context -> Ctxt CGInfo -> [Name] -> Map Name IntSet
22−findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
23+-- UseMap maps names to the set of used argument positions.
24+type UseMap = Map Name IntSet
25+
26+-- PatvarMap maps pattern variable names to the corresponding (data-ctor-name, argpos).
27+type PatvarMap = Map Name (Name, Int)
28+
29+findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
30+findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
2331 where
24− union :: [Map Name IntSet] -> Map Name IntSet
25− union = M.unionsWith S.union
32+ unionMap :: (a -> UseMap) -> [a] -> UseMap
33+ unionMap f = M.unionsWith IS.union . map f
2634
2735 getDef :: Context -> Name -> Def
2836 getDef ctx n = case lookupDef n ctx of
@@ -30,7 +38,7 @@ findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
3038 [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
3139 _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
3240
33− findUsedDef :: Ctxt CGInfo -> Def -> Map Name IntSet
41+ findUsedDef :: Ctxt CGInfo -> Def -> UseMap
3442 findUsedDef cg (Function ty t ) = M.empty
3543 findUsedDef cg (TyDecl ty t ) = M.empty
3644 findUsedDef cg (Operator ty n f) = M.empty
@@ -40,12 +48,30 @@ findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
4048 -- the fst component is the list of pattern variables, which we don't use
4149 = findUsedSC cg M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
4250
43− findUsedSC :: Ctxt CGInfo -> Map Name (Name, Int) -> SC -> Map Name IntSet
51+ findUsedSC :: Ctxt CGInfo -> PatvarMap -> SC -> UseMap
4452 findUsedSC cg vars ImpossibleCase = M.empty
4553 findUsedSC cg vars (UnmatchedCase msg) = M.empty
46− findUsedSC cg vars (Case n alts) = undefined
47− findUsedSC cg vars (ProjCase t alt) = undefined
48− findUsedSC cg vars (STerm t) = undefined
54+ findUsedSC cg vars (Case n alts) = unionMap (findUsedAlt cg vars) alts
55+ findUsedSC cg vars (ProjCase t alt) = findUsedAlt cg vars alt
56+ findUsedSC cg vars (STerm t) = unionMap lookUp $ findUsedTerm cg t
57+ where
58+ lookUp :: Name -> UseMap
59+ lookUp n = case M.lookup n vars of
60+ Just (cn, i) -> M.singleton cn (IS.singleton i)
61+ Nothing -> M.empty
62+
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
69+ where
70+ u :: [Name] -> PatvarMap -> PatvarMap
71+ vs `u` pmap = M.fromList [(var, (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
72+
73+ findUsedTerm :: Ctxt CGInfo -> Term -> Set Name
74+ findUsedTerm cg t = undefined
4975
5076findUnusedArgs :: [Name] -> Idris ()
5177findUnusedArgs names = do