@@ -58,23 +58,26 @@ performUsageAnalysis = do
5858 [] -> return [] -- no main -> not compiling -> reachability irrelevant
5959 _ -> do
6060 ci <- idris_classes <$> getIState
61+ cg <- idris_callgraph <$> getIState
62+ opt <- idris_optimisation <$> getIState
6163
6264 -- Build the dependency graph.
6365 let depMap = buildDepMap ci ctx mainName
6466
6567 -- Search for reachable nodes in the graph.
6668 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
69+ usage = M.toList minUse
6770
6871 -- Print some debug info.
6972 logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
70− logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap minUse
73+ logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage
7174 logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
7275
73− -- Check that everything reachable is accessible
74− checkAccessibility minUse
76+ -- Check that everything reachable is accessible.
77+ mapM_ (checkAccessibility opt) usage
7578
7679 -- Store the usage info in the internal state.
77− mapM_ storeUsage . M.toList $ minUse
80+ mapM_ (storeUsage cg) usage
7881
7982 return $ S.toList reachableNames
8083 where
@@ -84,18 +87,25 @@ performUsageAnalysis = do
8487 fmtItem :: (Cond, Set Node) -> String
8588 fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (S.toList deps)
8689
87− fmtUseMap :: UseMap -> String
88− fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IS.toList is)) . M.toList
90+ fmtUseMap :: [(Name, IntSet)] -> String
91+ fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IS.toList is))
8992
90− storeUsage :: (Name, IntSet) -> Idris ()
91− storeUsage (n, args) = do
92− cg <- idris_callgraph <$> getIState
93− case lookupCtxt n cg of
94− [x] -> addToCG n x{ usedpos = IS.toList args } -- functions
95− _ -> addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
93+ storeUsage :: Ctxt CGInfo -> (Name, IntSet) -> Idris ()
94+ storeUsage cg (n, args)
95+ | [x] <- lookupCtxt n cg
96+ = addToCG n x{ usedpos = IS.toList args } -- functions
9697
97−checkAccessibility :: UseMap -> Idris ()
98−checkAccessibility umap = return ()
98+ | otherwise
99+ = addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
100+
101+ checkAccessibility :: Ctxt OptInfo -> (Name, IntSet) -> Idris ()
102+ checkAccessibility opt (n, reachable)
103+ | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt
104+ = let collision = IS.fromList inaccessible `IS.intersection` reachable
105+ in unless (IS.null collision)
106+ . fail $ "Erasure checker: inaccessible arguments reachable: " ++ show (IS.toList collision)
107+
108+ | otherwise = return ()
99109
100110-- Find the minimal consistent usage by forward chaining.
101111minimalUsage :: Deps -> (Deps, (Set Name, UseMap))