git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Erasure.hs
517 lines 22 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Erasure (performUsageAnalysis, mkFieldName) where
5import Idris.AbsSyntax
6import Idris.ASTUtils
7import Idris.Core.CaseTree
8import Idris.Core.TT
9import Idris.Core.Evaluate
10import Idris.Primitives
11import Idris.Error
13import Debug.Trace
14import System.IO.Unsafe
16import Control.Category
17import Prelude hiding (id, (.))
19import Control.Arrow
20import Control.Applicative
21import Control.Monad.State
22import Data.Maybe
23import Data.List
24import qualified Data.Set as S
25import qualified Data.IntSet as IS
26import qualified Data.Map as M
27import qualified Data.IntMap as IM
28import Data.Set (Set)
29import Data.IntSet (IntSet)
30import Data.Map (Map)
31import Data.IntMap (IntMap)
32import Data.Text (pack)
33import qualified Data.Text as T
35-- UseMap maps names to the set of used (reachable) argument positions.
36type UseMap = Map Name (IntMap (Set Reason))
38data Arg = Arg Int | Result deriving (Eq, Ord)
40instance Show Arg where
41 show (Arg i) = show i
42 show Result = "*"
44type Node = (Name, Arg)
45type Deps = Map Cond DepSet
46type Reason = (Name, Int) -- function name, argument index
48-- Nodes along with sets of reasons for every one.
49type DepSet = Map Node (Set Reason)
51-- "Condition" is the conjunction
52-- of elementary assumptions along the path from the root.
53-- Elementary assumption (f, i) means that "function f uses the argument i".
54type Cond = Set Node
56-- Variables carry certain information with them.
57data VarInfo = VI
58 { viDeps :: DepSet -- dependencies drawn in by the variable
59 , viFunArg :: Maybe Int -- which function argument this variable came from (defined only for patvars)
60 , viMethod :: Maybe Name -- name of the metamethod represented by the var, if any
61 }
62 deriving Show
64type Vars = Map Name VarInfo
66-- Perform usage analysis, write the relevant information in the internal
67-- structures, returning the list of reachable names.
68performUsageAnalysis :: [Name] -> Idris [Name]
69performUsageAnalysis startNames = do
70 ctx <- tt_ctxt <$> getIState
71 case startNames of
72 [] -> return [] -- no main -> not compiling -> reachability irrelevant
73 main -> do
74 ci <- idris_classes <$> getIState
75 cg <- idris_callgraph <$> getIState
76 opt <- idris_optimisation <$> getIState
77 used <- idris_erasureUsed <$> getIState
78 externs <- idris_externs <$> getIState
80 -- Build the dependency graph.
81 let depMap = buildDepMap ci used (S.toList externs) ctx main
83 -- Search for reachable nodes in the graph.
84 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
85 usage = M.toList minUse
87 -- Print some debug info.
88 logLvl 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)
89 logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
90 logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage
91 logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
93 -- Check that everything reachable is accessible.
94 checkEnabled <- (WarnReach `elem`) . opt_cmdline . idris_options <$> getIState
95 when checkEnabled $
96 mapM_ (checkAccessibility opt) usage
98 -- Check that no postulates are reachable.
99 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState
100 when (not . S.null $ reachablePostulates)
101 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])
103 -- Store the usage info in the internal state.
104 mapM_ storeUsage usage
106 return $ S.toList reachableNames
107 where
108 indent = (" " ++)
110 fmtItem :: (Cond, DepSet) -> String
111 fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)
113 fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
114 fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ fmtIxs is)
116 fmtIxs :: IntMap (Set Reason) -> String
117 fmtIxs = intercalate ", " . map fmtArg . IM.toList
118 where
119 fmtArg (i, rs)
120 | S.null rs = show i
121 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)
123 storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
124 storeUsage (n, args) = fputState (cg_usedpos . ist_callgraph n) flat
125 where
126 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
128 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
129 checkAccessibility opt (n, reachable)
130 | Just (Optimise inaccessible dt) <- lookupCtxtExact n opt
131 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
132 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
134 | otherwise = return ()
135 where
136 fmt n [] = show n ++ " (no more information available)"
137 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]
138 warn = logLvl 0
140-- Find the minimal consistent usage by forward chaining.
141minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
142minimalUsage = second gather . forwardChain
143 where
144 gather :: DepSet -> (Set Name, UseMap)
145 gather = foldr ins (S.empty, M.empty) . M.toList
146 where
147 ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
148 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
149 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
151forwardChain :: Deps -> (Deps, DepSet)
152forwardChain deps
153 | Just trivials <- M.lookup S.empty deps
154 = (M.unionWith S.union trivials)
155 `second` forwardChain (remove trivials . M.delete S.empty $ deps)
156 | otherwise = (deps, M.empty)
157 where
158 -- Remove the given nodes from the Deps entirely,
159 -- possibly creating new empty Conds.
160 remove :: DepSet -> Deps -> Deps
161 remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)
163-- Build the dependency graph,
164-- starting the depth-first search from a list of Names.
165buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->
166 Context -> [Name] -> Deps
167buildDepMap ci used externs ctx startNames
168 = addPostulates used $ dfs S.empty M.empty startNames
169 where
170 -- mark the result of Main.main as used with the empty assumption
171 addPostulates :: [(Name, Int)] -> Deps -> Deps
172 addPostulates used deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps (postulates used)
173 where
174 -- mini-DSL for postulates
175 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])
176 it n is = [(sUN n, Arg i) | i <- is]
177 mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
179 -- believe_me is special because it does not use all its arguments
180 specialPrims = S.fromList [sUN "prim__believe_me"]
181 usedNames = allNames deps S.\\ specialPrims
182 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]
184 postulates used =
185 [ [] ==> concat
186 -- Main.main ( + export lists) and run__IO, are always evaluated
187 -- but they elude analysis since they come from the seed term.
188 [(map (\n -> (n, Result)) startNames)
189 ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]
190 ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]
192 -- Explicit usage declarations from a %used pragma
193 , map (\(n, i) -> (n, Arg i)) used
195 -- MkIO is read by run__IO,
196 -- but this cannot be observed in the source code of programs.
197 , it "MkIO" [2]
198 , it "prim__IO" [1]
200 -- Foreign calls are built with pairs, but mkForeign doesn't
201 -- have an implementation so analysis won't see them
202 , [(pairCon, Arg 2),
203 (pairCon, Arg 3)] -- Used in foreign calls
205 -- these have been discovered as builtins but are not listed
206 -- among Idris.Primitives.primitives
207 --, mn "__MkPair" [2,3]
208 , it "prim_fork" [0]
209 , it "unsafePerformPrimIO" [1]
211 -- believe_me is a primitive but it only uses its third argument
212 -- it is special-cased in usedNames above
213 , it "prim__believe_me" [2]
215 -- in general, all other primitives use all their arguments
216 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
218 -- %externs are assumed to use all their arguments
219 , [(n, Arg i) | (n,arity) <- externs, i <- [0..arity-1]]
221 -- mkForeign* functions are special-cased below
222 ]
223 ]
225 -- perform depth-first search
226 -- to discover all the names used in the program
227 -- and call getDeps for every name
228 dfs :: Set Name -> Deps -> [Name] -> Deps
229 dfs visited deps [] = deps
230 dfs visited deps (n : ns)
231 | n `S.member` visited = dfs visited deps ns
232 | otherwise = dfs (S.insert n visited) (M.unionWith (M.unionWith S.union) deps' deps) (next ++ ns)
233 where
234 next = [n | n <- S.toList depn, n `S.notMember` visited]
235 depn = S.delete n $ allNames deps'
236 deps' = getDeps n
238 -- extract all names that a function depends on
239 -- from the Deps of the function
240 allNames :: Deps -> Set Name
241 allNames = S.unions . map names . M.toList
242 where
243 names (cs, ns) = S.map fst cs `S.union` S.map fst (M.keysSet ns)
245 -- get Deps for a Name
246 getDeps :: Name -> Deps
247 getDeps (SN (WhereN i (SN (InstanceCtorN classN)) (MN i' field)))
248 = M.empty -- these deps are created when applying instance ctors
249 getDeps n = case lookupDefExact n ctx of
250 Just def -> getDepsDef n def
251 Nothing -> error $ "erasure checker: unknown reference: " ++ show n
253 getDepsDef :: Name -> Def -> Deps
254 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
255 getDepsDef fn (TyDecl ty t) = M.empty
256 getDepsDef fn (Operator ty n' f) = M.empty -- TODO: what's this?
257 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
258 = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
259 where
260 -- we must eta-expand the definition with fresh variables
261 -- to capture these dependencies as well
262 etaIdx = [length vars .. length tys - 1]
263 etaVars = [eta i | i <- etaIdx]
264 etaMap = M.fromList [varPair (eta i) i | i <- etaIdx]
265 eta i = MN i (pack "eta")
267 -- the variables that arose as function arguments only depend on (n, i)
268 varMap = M.fromList [varPair v i | (v,i) <- zip vars [0..]]
270 varPair n argNo = (n, VI
271 { viDeps = M.singleton (fn, Arg argNo) S.empty
272 , viFunArg = Just argNo
273 , viMethod = Nothing
274 })
276 (vars, sc) = cases_runtime cdefs
277 -- we use cases_runtime in order to have case-blocks
278 -- resolved to top-level functions before our analysis
280 etaExpand :: [Name] -> Term -> Term
281 etaExpand [] t = t
282 etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))
284 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
285 getDepsSC fn es vs ImpossibleCase = M.empty
286 getDepsSC fn es vs (UnmatchedCase msg) = M.empty
288 -- for the purposes of erasure, we can disregard the projection
289 getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step
290 getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case Shared n alts) -- base
292 -- other ProjCase's are not supported
293 getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)
295 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
296 getDepsSC fn es vs (Case sh n alts)
297 -- we case-split on this variable, which marks it as used
298 -- (unless there is exactly one case branch)
299 -- hence we add a new dependency, whose only precondition is
300 -- that the result of this function is used at all
301 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree
302 where
303 addTagDep = case alts of
304 [_] -> id -- single branch, tag not used
305 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)
306 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
308 getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt -> Deps
309 getDepsAlt fn es vs var (FnCase n ns sc) = M.empty -- can't use FnCase at runtime
310 getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc
311 getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc
312 getDepsAlt fn es vs var (SucCase n sc)
313 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
315 -- data constructors
316 getDepsAlt fn es vs var (ConCase n cnt ns sc)
317 = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
318 where
319 -- Here we insert dependencies that arose from pattern matching on a constructor.
320 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
321 vs' = M.fromList [(v, VI
322 { viDeps = M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) (viDeps var)
323 , viFunArg = viFunArg var
324 , viMethod = meth j
325 })
326 | (v, j) <- zip ns [0..]]
328 -- this is safe because it's certainly a patvar
329 varIdx = fromJust (viFunArg var)
331 -- generate metamethod names, "n" is the instance ctor
332 meth :: Int -> Maybe Name
333 meth | SN (InstanceCtorN className) <- n = \j -> Just (mkFieldName n j)
334 | otherwise = \j -> Nothing
336 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
337 getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps
339 -- named variables introduce dependencies as described in `vs'
340 getDepsTerm vs bs cd (P _ n _)
341 -- de bruijns (lambda-bound, let-bound vars)
342 | Just deps <- lookup n bs
343 = deps cd
345 -- ctor-bound/arg-bound variables
346 | Just var <- M.lookup n vs
347 = M.singleton cd (viDeps var)
349 -- sanity check: machine-generated names shouldn't occur at top-level
350 | MN _ _ <- n
351 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
353 -- assumed to be a global reference
354 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
356 -- dependencies of de bruijn variables are described in `bs'
357 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd
359 getDepsTerm vs bs cd (Bind n bdr body)
360 -- here we just push IM.empty on the de bruijn stack
361 -- the args will be marked as used at the usage site
362 | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body
363 | Pi _ ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body
365 -- let-bound variables can get partially evaluated
366 -- it is sufficient just to plug the Cond in when the bound names are used
367 | Let ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body
368 | NLet ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body
369 where
370 var t cd = getDepsTerm vs bs cd t
372 -- applications may add items to Cond
373 getDepsTerm vs bs cd app@(App _ _)
374 | (fun, args) <- unApply app = case fun of
375 -- instance constructors -> create metamethod deps
376 P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _
377 -> conditionalDeps ctorName args -- regular data ctor stuff
378 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff
380 -- ordinary constructors
381 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
382 P (DCon _ _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used
384 -- mkForeign* calls must be special-cased because they are variadic
385 -- All arguments must be marked as used, except for the first one,
386 -- which is the (Foreign a) spec that defines the type
387 -- and is not needed at runtime.
388 P _ (UN n) _
389 | n `elem` map T.pack ["mkForeignPrim"]
390 -> unconditionalDeps args -- (drop 1 args)
392 -- a bound variable might draw in additional dependencies,
393 -- think: f x = x 0 <-- here, `x' _is_ used
394 P _ n _
395 -- debruijn-bound name
396 | Just deps <- lookup n bs
397 -> deps cd `union` unconditionalDeps args
399 -- local name that refers to a method
400 | Just var <- M.lookup n vs
401 , Just meth <- viMethod var
402 -> viDeps var `ins` conditionalDeps meth args -- use the method instead
404 -- local name
405 | Just var <- M.lookup n vs
406 -- unconditional use
407 -> viDeps var `ins` unconditionalDeps args
409 -- global name
410 | otherwise
411 -- depends on whether the referred thing uses its argument
412 -> conditionalDeps n args
414 -- TODO: could we somehow infer how bound variables use their arguments?
415 V i -> snd (bs !! i) cd `union` unconditionalDeps args
417 -- we interpret applied lambdas as lets in order to reuse code here
418 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
420 -- and we interpret applied lets as lambdas
421 Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')
422 Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')
424 Proj t i
425 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t
427 Erased -> M.empty
429 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
430 where
431 union = M.unionWith $ M.unionWith S.union
432 ins = M.insertWith (M.unionWith S.union) cd
434 unconditionalDeps :: [Term] -> Deps
435 unconditionalDeps = unionMap (getDepsTerm vs bs cd)
437 conditionalDeps :: Name -> [Term] -> Deps
438 conditionalDeps n
439 = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices
440 where
441 indices = map Just [0 .. getArity n - 1] ++ repeat Nothing
442 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
443 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
445 methodDeps :: Name -> (Int, Term) -> Deps
446 methodDeps ctorName (methNo, t)
447 = getDepsTerm (vars `M.union` vs) (bruijns ++ bs) cond body
448 where
449 vars = M.fromList [(v, VI
450 { viDeps = deps i
451 , viFunArg = Just i
452 , viMethod = Nothing
453 }) | (v, i) <- zip args [0..]]
454 deps i = M.singleton (metameth, Arg i) S.empty
455 bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]
456 cond = S.singleton (metameth, Result)
457 metameth = mkFieldName ctorName methNo
458 (args, body) = unfoldLams t
460 -- projections
461 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n
462 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
464 -- the easy cases
465 getDepsTerm vs bs cd (Constant _) = M.empty
466 getDepsTerm vs bs cd (TType _) = M.empty
467 getDepsTerm vs bs cd (UType _) = M.empty
468 getDepsTerm vs bs cd Erased = M.empty
469 getDepsTerm vs bs cd Impossible = M.empty
471 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t
473 -- Get the number of arguments that might be considered for erasure.
474 getArity :: Name -> Int
475 getArity (SN (WhereN i' ctorName (MN i field)))
476 | Just (TyDecl (DCon _ _ _) ty) <- lookupDefExact ctorName ctx
477 = let argTys = map snd $ getArgTys ty
478 in if i <= length argTys
479 then length $ getArgTys (argTys !! i)
480 else error $ "invalid field number " ++ show i ++ " for " ++ show ctorName
482 | otherwise = error $ "unknown instance constructor: " ++ show ctorName
484 getArity n = case lookupDefExact n ctx of
485 Just (CaseOp ci ty tys def tot cdefs) -> length tys
486 Just (TyDecl (DCon tag arity _) _) -> arity
487 Just (TyDecl (Ref) ty) -> length $ getArgTys ty
488 Just (Operator ty arity op) -> arity
489 Just df -> error $ "Erasure/getArity: unrecognised entity '"
490 ++ show n ++ "' with definition: " ++ show df
491 Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n
493 -- convert applications of lambdas to lets
494 -- Note that this transformation preserves de bruijn numbering
495 lamToLet :: [Term] -> Term -> Term
496 lamToLet xs (App f x) = lamToLet (x:xs) f
497 lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)
498 lamToLet (x:xs) t = App (lamToLet xs t) x
499 lamToLet [] t = t
501 -- split "\x_i -> T(x_i)" into [x_i] and T
502 unfoldLams :: Term -> ([Name], Term)
503 unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')
504 unfoldLams t = ([], t)
506 union :: Deps -> Deps -> Deps
507 union = M.unionWith (M.unionWith S.union)
509 unions :: [Deps] -> Deps
510 unions = M.unionsWith (M.unionWith S.union)
512 unionMap :: (a -> Deps) -> [a] -> Deps
513 unionMap f = M.unionsWith (M.unionWith S.union) . map f
515-- Make a field name out of a data constructor name and field number.
516mkFieldName :: Name -> Int -> Name
517mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")