@@ -157,168 +157,12 @@ findUsed ctx cg ns = dfs M.empty ns
157157 getDepsTerm vs bs cd Impossible = IM.empty
158158 getDepsTerm vs bs cd (TType _) = IM.empty
159159
160−{-
161−data TT n = P NameType n (TT n) -- ^ named references
162− | V !Int -- ^ a resolved de Bruijn-indexed variable
163− | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
164− | App !(TT n) (TT n) -- ^ function, function type, arg
165− | Constant Const -- ^ constant
166− | Proj (TT n) !Int -- ^ argument projection; runtime only
167− -- (-1) is a special case for 'subtract one from BI'
168− | Erased -- ^ an erased term
169− | Impossible -- ^ special case for totality checking
170− | TType UExp -- ^ the type of types at some level
171−
172−-- | All binding forms are represented in a unform fashion.
173−data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
174− | Pi { binderTy :: !b }
175− | Let { binderTy :: !b,
176− binderVal :: b {-^ value for bound variable-}}
177− | NLet { binderTy :: !b,
178− binderVal :: b }
179− | Hole { binderTy :: !b}
180− | GHole { envlen :: Int,
181− binderTy :: !b}
182− | Guess { binderTy :: !b,
183− binderVal :: b }
184− | PVar { binderTy :: !b }
185− | PVTy { binderTy :: !b }
186−-}
187−
188160 unions :: [Deps] -> Deps
189161 unions = IM.unionsWith S.union
190162
191163 unionMap :: (a -> Deps) -> [a] -> Deps
192164 unionMap f = unions . map f
193165
194−{-
195−buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
196−buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
197− where
198− union :: [DepGraph] -> DepGraph
199− union = M.unionsWith $ M.unionWith S.union
200−
201− unionMap :: (a -> DepGraph) -> [a] -> DepGraph
202− unionMap f = union . map f
203−
204− getDef :: Context -> Name -> Def
205− getDef ctx n = case lookupDef n ctx of
206− [def] -> def
207− [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
208− _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
209−
210− findDepsDef :: Ctxt CGInfo -> Name -> Def -> DepGraph
211− findDepsDef cg fn (Function ty t ) = M.empty
212− findDepsDef cg fn (TyDecl ty t ) = M.empty
213− findDepsDef cg fn (Operator ty n f) = M.empty
214− -- ^- non-pattern-matching definitions don't contribute to dependencies
215−
216− findDepsDef cg fn (CaseOp ci ty tys def tot cdefs)
217− -- the fst component is the list of pattern variables, which we don't use
218− = findDepsSC cg fn M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
219−
220− findDepsSC :: Ctxt CGInfo -> Name -> PatvarMap -> SC -> DepGraph
221− findDepsSC cg fn vars ImpossibleCase = M.empty
222− findDepsSC cg fn vars (UnmatchedCase msg) = M.empty
223− findDepsSC cg fn vars (Case n alts) = unionMap (findDepsAlt cg fn vars) alts
224− findDepsSC cg fn vars (ProjCase t alt ) = findDepsAlt cg fn vars alt
225− findDepsSC cg fn vars (STerm t) = findDepsTerm cg vars (fn, Retval) t
226−
227− findDepsAlt :: Ctxt CGInfo -> Name -> PatvarMap -> CaseAlt -> DepGraph
228− findDepsAlt cg fn vars (FnCase n ns sc) = findDepsSC cg fn vars sc -- TODO: what's this?
229− findDepsAlt cg fn vars (ConstCase c sc) = findDepsSC cg fn vars sc
230− findDepsAlt cg fn vars (SucCase n sc) = findDepsSC cg fn (M.insert n (error "put S here") vars) sc -- TODO
231− findDepsAlt cg fn vars (DefaultCase sc) = findDepsSC cg fn vars sc
232− findDepsAlt cg fn vars (ConCase n cnt ns sc) = findDepsSC cg fn (ns `u` vars) sc
233− where
234− -- constructor name `n' is passed implicitly
235− u :: [Name] -> PatvarMap -> PatvarMap
236− vs `u` pmap = M.fromList [(var, S.singleton (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
237−
238− -- where do we introduce the dependency
239− -- f x = x
240− -- (f, Result) -> (f, 0) ?
241−
242− findDepsTerm :: Ctxt CGInfo -> PatvarMap -> (Name, Arg) -> Term -> DepGraph
243− findDepsTerm cg vars (tn,ta) (P _ n _) = tn ~> ta ~> case M.lookup n vars of
244− Just vs -> vs -- an existing patvar
245− Nothing -> S.singleton (n, Retval) -- must be the return value of something from the context
246− findDepsTerm cg vars (tn,ta) (Bind n (Let t v) body) = union
247− [ findDepsTerm cg vars (tn,ta) (instantiate v body)
248− , findDepsTerm cg vars (tn,ta) t
249− ]
250− findDepsTerm cg vars (tn,ta) (Bind n b body) = union
251− [ findDepsTerm cg (M.delete n vars) (tn,ta) body
252− , findDepsTerm cg vars (tn,ta) (binderTy b)
253− ]
254−
255− infixr 3 ~>
256− (~>) :: (Ord a) => a -> b -> Map a b
257− (~>) = M.singleton
258−
259−findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
260−findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
261− where
262− unionMap :: (a -> UseMap) -> [a] -> UseMap
263− unionMap f = M.unionsWith IS.union . map f
264−
265− getDef :: Context -> Name -> Def
266− getDef ctx n = case lookupDef n ctx of
267− [def] -> def
268− [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
269− _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
270−
271− findUsedDef :: Ctxt CGInfo -> Def -> UseMap
272− findUsedDef cg (Function ty t ) = M.empty
273− findUsedDef cg (TyDecl ty t ) = M.empty
274− findUsedDef cg (Operator ty n f) = M.empty
275− -- ^- non-pattern-matching definitions don't contribute to usage of data
276−
277− findUsedDef cg (CaseOp ci ty def tot cdefs)
278− -- the fst component is the list of pattern variables, which we don't use
279− = findUsedSC cg M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
280−
281− findUsedSC :: Ctxt CGInfo -> PatvarMap -> SC -> UseMap
282− findUsedSC cg vars ImpossibleCase = M.empty
283− findUsedSC cg vars (UnmatchedCase msg) = M.empty
284− findUsedSC cg vars (Case n alts) = unionMap (findUsedAlt cg vars) alts
285− findUsedSC cg vars (ProjCase t alt) = findUsedAlt cg vars alt
286− findUsedSC cg vars (STerm t) = unionMap lookUp . S.toList $ findUsedTerm cg t
287− where
288− lookUp :: Name -> UseMap
289− lookUp n = case M.lookup n vars of
290− Just (cn, i) -> M.singleton cn (IS.singleton i)
291− Nothing -> M.empty
292−
293− findUsedAlt :: Ctxt CGInfo -> PatvarMap -> CaseAlt -> UseMap
294− findUsedAlt cg vars (FnCase n ns sc) = findUsedSC cg vars sc -- TODO: what's this?
295− findUsedAlt cg vars (ConstCase c sc) = findUsedSC cg vars sc
296− findUsedAlt cg vars (SucCase n sc) = findUsedSC cg (M.insert n (error "put S here") vars) sc -- TODO
297− findUsedAlt cg vars (DefaultCase sc) = findUsedSC cg vars sc
298− findUsedAlt cg vars (ConCase n cnt ns sc) = findUsedSC cg (ns `u` vars) sc
299− where
300− u :: [Name] -> PatvarMap -> PatvarMap
301− vs `u` pmap = M.fromList [(var, (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
302−
303− -- Find used pattern variables in the given term.
304− findUsedTerm :: Ctxt CGInfo -> Term -> Set Name
305− findUsedTerm cg (P _ n _) = S.singleton n
306− findUsedTerm cg (Bind n (Let t v) body) = S.unions
307− [ findUsedTerm cg v
308− , S.delete n $ findUsedTerm cg body
309− , findUsedTerm cg t ]
310− findUsedTerm cg (Bind n b t) = S.unions
311− [ findUsedTerm cg (binderTy b)
312− , S.delete n $ findUsedTerm cg t ]
313− findUsedTerm cg (Proj t i) = findUsedTerm cg t
314− findUsedTerm cg t@(App _ _) | (P _ n _, args) <- unApply t
315− = let unused = case lookupCtxt n cg of
316− [cgi] -> unusedpos cgi
317− _ -> []
318− in S.unions [findUsedTerm cg arg | (i,arg) <- zip [0..] args, i `notElem` unused]
319− findUsedTerm cg _ = S.empty
320−-}
321−
322166findUnusedArgs :: [Name] -> Idris ()
323167findUnusedArgs names = do
324168 cg <- idris_callgraph <$> getIState