@@ -84,9 +84,9 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
85 getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
85 getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
86 getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
86 getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
87− getDepsAlt vs pv (ConstCase c sc) = error "a ConstCase encountered"
87+ getDepsAlt vs pv (ConstCase c sc) = IM.empty
88 getDepsAlt vs pv (SucCase n sc) = error "a SucCase encountered"
88 getDepsAlt vs pv (SucCase n sc) = error "a SucCase encountered"
89− getDepsAlt vs pv (DefaultCase sc) = error "a DefaultCase encountered"
89+ getDepsAlt vs pv (DefaultCase sc) = error $ "a DefaultCase encountered: " ++ show (DefaultCase sc)
90 getDepsAlt vs pv (ConCase n cnt ns sc)
90 getDepsAlt vs pv (ConCase n cnt ns sc)
91 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
91 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
@@ -95,22 +95,38 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
96 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
96 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
97 getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
97 getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
99+ -- named variables introduce dependencies as described in `vs'
98 getDepsTerm vs bs cd (P _ n _)
100 getDepsTerm vs bs cd (P _ n _)
99 | Just var <- M.lookup n vs = var cd
101 | Just var <- M.lookup n vs = var cd
100 | otherwise = IM.empty
102 | otherwise = IM.empty
104+ -- dependencies of de bruijn variables are described in `bs'
101 getDepsTerm vs bs cd (V i) = (bs !! i) cd
105 getDepsTerm vs bs cd (V i) = (bs !! i) cd
102− getDepsTerm vs bs cd (Bind n (Lam ty) t) = error "stray lambda" -- probably just push S.empty on the DeBruijn stack
107+ getDepsTerm vs bs cd (Bind n bdr t)
108+ -- here we just push IM.empty on the de bruijn stack
103− getDepsTerm vs bs cd (Bind n (Pi ty) t) = error "stray bind" -- the args will be marked as used on the usage site
109+ -- the args will be marked as used at the usage site
104− getDepsTerm vs bs cd (Bind n (Let ty v) t) =
110+ | Lam ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
111+ | Pi ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
113+ -- let-bound variables can get partially evaluated
114+ -- it is sufficient just to plug the Cond in when the bound names are used
105− getDepsTerm (M.insert n (\cd -> getDepsTerm vs bs cd v) vs) bs cd t
115+ | Let ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
106− getDepsTerm vs bs cd (Bind n (NLet ty v) t) =
107− getDepsTerm (M.insert n (\cd -> getDepsTerm vs bs cd v) vs) bs cd t -- TODO: what's this?
116+ | NLet ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
118+ var v cd = getDepsTerm vs bs cd v
120+ -- applications may add items to Cond
108 getDepsTerm vs bs cd app@(App _ _)
121 getDepsTerm vs bs cd app@(App _ _)
109 | (fun, args) <- unApply app = case fun of
122 | (fun, args) <- unApply app = case fun of
111− -- named references depend on whether the referred thing uses the argument
123+ -- these depend on whether the referred thing uses the argument
112− P Ref n _ -> called n args
124+ P Ref n _ -> called n args
113 P (DCon _ _) n _ -> called n args
125 P (DCon _ _) n _ -> called n args
128+ P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
129+ P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
115 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
131 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)