@@ -84,9 +84,9 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
8484
8585 getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
8686 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
8888 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)
9090 getDepsAlt vs pv (ConCase n cnt ns sc)
9191 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
9292 where
@@ -95,22 +95,38 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
9595
9696 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
9797 getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
98+
99+ -- named variables introduce dependencies as described in `vs'
98100 getDepsTerm vs bs cd (P _ n _)
99101 | Just var <- M.lookup n vs = var cd
100102 | otherwise = IM.empty
103+
104+ -- dependencies of de bruijn variables are described in `bs'
101105 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
103− getDepsTerm vs bs cd (Bind n (Pi ty) t) = error "stray bind" -- the args will be marked as used on the usage site
104− getDepsTerm vs bs cd (Bind n (Let ty v) t) =
105− getDepsTerm (M.insert n (\cd -> getDepsTerm vs bs cd v) vs) 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?
106+
107+ getDepsTerm vs bs cd (Bind n bdr t)
108+ -- here we just push IM.empty on the de bruijn stack
109+ -- the args will be marked as used at the usage site
110+ | Lam ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
111+ | Pi ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
112+
113+ -- let-bound variables can get partially evaluated
114+ -- it is sufficient just to plug the Cond in when the bound names are used
115+ | Let ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
116+ | NLet ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
117+ where
118+ var v cd = getDepsTerm vs bs cd v
119+
120+ -- applications may add items to Cond
108121 getDepsTerm vs bs cd app@(App _ _)
109122 | (fun, args) <- unApply app = case fun of
110− P Bound n _ -> ?
111− -- named references depend on whether the referred thing uses the argument
112− P Ref n _ -> called n args
123+ -- these depend on whether the referred thing uses the argument
124+ P Ref n _ -> called n args
113125 P (DCon _ _) n _ -> called n args
126+
127+ -- these do not
128+ P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
129+ P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
114130 where
115131 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
116132