@@ -28,37 +28,23 @@ import Data.IntMap (IntMap)
2828-- UseMap maps names to the set of used (reachable) argument positions.
2929type UseMap = Map Name IntSet
3030
31−-- A dependency, potential edge in the dep graph.
32−-- Every dependency belongs to a certain Idris function.
33−-- For the effect to take place, the condition must be true.
34−data Dep = Dep
35− -- Effect
36− { depArg :: Int -- | This argument of the function should be marked as used.
37− , depCtors :: Set (Name, Int) -- | These ctor fields should be marked as used.
38− , depTags :: Set Name -- | Tags of these ADTs should be marked as used.
39−
40− -- Condition
41− , depGuards :: Set (Name, Int) -- | All these arguments must be marked as used.
42− }
43− deriving (Eq, Ord, Show)
44−
45−-- DepMap maps function names to their sets of dependencies.
46−type DepMap = Map Name (Set Dep)
31+type Deps = IntMap (Set (Name, Int))
32+type DepMap = Map Name Deps
4733
48−findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
34+findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
4935findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
5036 where
51− getDeps :: Name -> Set Dep
37+ getDeps :: Name -> Deps
5238 getDeps n = case lookupDef n ctx of
5339 [def] -> getDepsDef def
5440 [] -> error $ "erasure checker: unknown name: " ++ show n
5541 _ -> error $ "erasure checker: ambiguous name: " ++ show n
5642
57− getDepsDef :: Def -> Set Dep
58− getDepsDef (Function ty t) = S.empty
59− getDepsDef (TyDecl ty t) = S.empty
60− getDepsDef (Operator ty n f) = S.empty
61− getDepsDef (CaseOp ci ty tys def tot cdefs) = S.empty
43+ getDepsDef :: Def -> Deps
44+ getDepsDef (Function ty t) = IM.empty
45+ getDepsDef (TyDecl ty t) = IM.empty
46+ getDepsDef (Operator ty n f) = IM.empty
47+ getDepsDef (CaseOp ci ty tys def tot cdefs) = IM.empty
6248
6349{-
6450buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph