{-|
Module      : Idris.Erasure
Description : Utilities to erase stuff not necessary for runtime.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}

module Idris.Erasure (performUsageAnalysis, mkFieldName) where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Error
import Idris.Options
import Idris.Primitives

import Prelude hiding (id, (.))

import Control.Arrow
import Control.Category
import Control.Monad
import Control.Monad.State
import Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS
import Data.List
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as S
import Data.Text (pack)
import qualified Data.Text as T

-- | UseMap maps names to the set of used (reachable) argument
-- positions.
type UseMap = Map Name (IntMap (Set Reason))

data Arg = Arg Int | Result deriving (Arg -> Arg -> Bool
(Arg -> Arg -> Bool) -> (Arg -> Arg -> Bool) -> Eq Arg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Arg -> Arg -> Bool
== :: Arg -> Arg -> Bool
$c/= :: Arg -> Arg -> Bool
/= :: Arg -> Arg -> Bool
Eq, Eq Arg
Eq Arg =>
(Arg -> Arg -> Ordering)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Arg)
-> (Arg -> Arg -> Arg)
-> Ord Arg
Arg -> Arg -> Bool
Arg -> Arg -> Ordering
Arg -> Arg -> Arg
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Arg -> Arg -> Ordering
compare :: Arg -> Arg -> Ordering
$c< :: Arg -> Arg -> Bool
< :: Arg -> Arg -> Bool
$c<= :: Arg -> Arg -> Bool
<= :: Arg -> Arg -> Bool
$c> :: Arg -> Arg -> Bool
> :: Arg -> Arg -> Bool
$c>= :: Arg -> Arg -> Bool
>= :: Arg -> Arg -> Bool
$cmax :: Arg -> Arg -> Arg
max :: Arg -> Arg -> Arg
$cmin :: Arg -> Arg -> Arg
min :: Arg -> Arg -> Arg
Ord)

instance Show Arg where
    show :: Arg -> String
show (Arg Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i
    show Arg
Result  = String
"*"

type Node = (Name, Arg)
type Deps = Map Cond DepSet
type Reason = (Name, Int)  -- function name, argument index

-- | Nodes along with sets of reasons for every one.
type DepSet = Map Node (Set Reason)

-- | "Condition" is the conjunction of elementary assumptions along
-- the path from the root.  Elementary assumption (f, i) means that
-- "function f uses the argument i".
type Cond = Set Node

-- | Variables carry certain information with them.
data VarInfo = VI
    { VarInfo -> DepSet
viDeps   :: DepSet      -- ^ dependencies drawn in by the variable
    , VarInfo -> Maybe Int
viFunArg :: Maybe Int   -- ^ which function argument this variable came from (defined only for patvars)
    , VarInfo -> Maybe Name
viMethod :: Maybe Name  -- ^ name of the metamethod represented by the var, if any
    }
    deriving Int -> VarInfo -> ShowS
[VarInfo] -> ShowS
VarInfo -> String
(Int -> VarInfo -> ShowS)
-> (VarInfo -> String) -> ([VarInfo] -> ShowS) -> Show VarInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VarInfo -> ShowS
showsPrec :: Int -> VarInfo -> ShowS
$cshow :: VarInfo -> String
show :: VarInfo -> String
$cshowList :: [VarInfo] -> ShowS
showList :: [VarInfo] -> ShowS
Show

type Vars = Map Name VarInfo

-- | Perform usage analysis, write the relevant information in the
-- internal structures, returning the list of reachable names.
performUsageAnalysis :: [Name] -> Idris [Name]
performUsageAnalysis :: [Name] -> Idris [Name]
performUsageAnalysis [Name]
startNames = do
    Context
ctx <- IState -> Context
tt_ctxt (IState -> Context)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
    case [Name]
startNames of
      [] -> [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- no main -> not compiling -> reachability irrelevant
      [Name]
main  -> do
        Ctxt InterfaceInfo
ci  <- IState -> Ctxt InterfaceInfo
idris_interfaces (IState -> Ctxt InterfaceInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt InterfaceInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        Ctxt CGInfo
cg  <- IState -> Ctxt CGInfo
idris_callgraph (IState -> Ctxt CGInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt CGInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        Ctxt OptInfo
opt <- IState -> Ctxt OptInfo
idris_optimisation (IState -> Ctxt OptInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt OptInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        [Reason]
used <- IState -> [Reason]
idris_erasureUsed (IState -> [Reason])
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) [Reason]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        Set Reason
externs <- IState -> Set Reason
idris_externs (IState -> Set Reason)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Set Reason)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState

        -- Build the dependency graph.
        let depMap :: Deps
depMap = Ctxt InterfaceInfo
-> [Reason] -> [Reason] -> Context -> [Name] -> Deps
buildDepMap Ctxt InterfaceInfo
ci [Reason]
used (Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
externs) Context
ctx [Name]
main

        -- Search for reachable nodes in the graph.
        let (Deps
residDeps, (Set Name
reachableNames, UseMap
minUse)) = Deps -> (Deps, (Set Name, UseMap))
minimalUsage Deps
depMap
            usage :: [(Name, IntMap (Set Reason))]
usage = UseMap -> [(Name, IntMap (Set Reason))]
forall k a. Map k a -> [(k, a)]
M.toList UseMap
minUse

        -- Print some debug info.
        Int -> String -> Idris ()
logErasure Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Original deps:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (((Cond, DepSet) -> String) -> [(Cond, DepSet)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> String
fmtItem ([(Cond, DepSet)] -> [String])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList (Deps -> [String]) -> Deps -> [String]
forall a b. (a -> b) -> a -> b
$ Deps
depMap)
        Int -> String -> Idris ()
logErasure Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Reachable names:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
indent ShowS -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> String
forall a. Show a => a -> String
show) ([Name] -> [String])
-> (Set Name -> [Name]) -> Set Name -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [String]) -> Set Name -> [String]
forall a b. (a -> b) -> a -> b
$ Set Name
reachableNames)
        Int -> String -> Idris ()
logErasure Int
4 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Minimal usage:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, IntMap (Set Reason))] -> String
fmtUseMap [(Name, IntMap (Set Reason))]
usage
        Int -> String -> Idris ()
logErasure Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Residual deps:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (((Cond, DepSet) -> String) -> [(Cond, DepSet)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> String
fmtItem ([(Cond, DepSet)] -> [String])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList (Deps -> [String]) -> Deps -> [String]
forall a b. (a -> b) -> a -> b
$ Deps
residDeps)

        -- Check that everything reachable is accessible.
        Bool
checkEnabled <- (Opt
WarnReach Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Opt] -> Bool) -> (IState -> [Opt]) -> IState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IOption -> [Opt]
opt_cmdline (IOption -> [Opt]) -> (IState -> IOption) -> IState -> [Opt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> IOption
idris_options (IState -> Bool)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkEnabled (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
            ((Name, IntMap (Set Reason)) -> Idris ())
-> [(Name, IntMap (Set Reason))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility Ctxt OptInfo
opt) [(Name, IntMap (Set Reason))]
usage

        -- Check that no postulates are reachable.
        Set Name
reachablePostulates <- Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set Name
reachableNames (Set Name -> Set Name)
-> (IState -> Set Name) -> IState -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Set Name
idris_postulates (IState -> Set Name)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Set Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> (Set Name -> Bool) -> Set Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Set Name -> Bool
forall a. Set a -> Bool
S.null (Set Name -> Bool) -> Set Name -> Bool
forall a b. (a -> b) -> a -> b
$ Set Name
reachablePostulates)
            (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
forall a. String -> Idris a
ifail (String
"reachable postulates:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n | Name
n <- Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
reachablePostulates])

        -- Store the usage info in the internal state.
        ((Name, IntMap (Set Reason)) -> Idris ())
-> [(Name, IntMap (Set Reason))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, IntMap (Set Reason)) -> Idris ()
storeUsage [(Name, IntMap (Set Reason))]
usage

        [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Idris [Name]) -> [Name] -> Idris [Name]
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
reachableNames
  where
    indent :: ShowS
indent = (String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++)

    fmtItem :: (Cond, DepSet) -> String
    fmtItem :: (Cond, DepSet) -> String
fmtItem (Cond
cond, DepSet
deps) = ShowS
indent ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Node] -> String
forall a. Show a => a -> String
show (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
cond) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Node, Set Reason)] -> String
forall a. Show a => a -> String
show (DepSet -> [(Node, Set Reason)]
forall k a. Map k a -> [(k, a)]
M.toList DepSet
deps)

    fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
    fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
fmtUseMap = [String] -> String
unlines ([String] -> String)
-> ([(Name, IntMap (Set Reason))] -> [String])
-> [(Name, IntMap (Set Reason))]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, IntMap (Set Reason)) -> String)
-> [(Name, IntMap (Set Reason))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,IntMap (Set Reason)
is) -> ShowS
indent ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IntMap (Set Reason) -> String
fmtIxs IntMap (Set Reason)
is)

    fmtIxs :: IntMap (Set Reason) -> String
    fmtIxs :: IntMap (Set Reason) -> String
fmtIxs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String)
-> (IntMap (Set Reason) -> [String])
-> IntMap (Set Reason)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Int, Set Reason) -> String) -> [(Int, Set Reason)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Set Reason) -> String
forall {a} {a}. (Show a, Show a) => (a, Set a) -> String
fmtArg ([(Int, Set Reason)] -> [String])
-> (IntMap (Set Reason) -> [(Int, Set Reason)])
-> IntMap (Set Reason)
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IntMap (Set Reason) -> [(Int, Set Reason)]
forall a. IntMap a -> [(Int, a)]
IM.toList
      where
        fmtArg :: (a, Set a) -> String
fmtArg (a
i, Set a
rs)
            | Set a -> Bool
forall a. Set a -> Bool
S.null Set a
rs = a -> String
forall a. Show a => a -> String
show a
i
            | Bool
otherwise = a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show ([a] -> [String]) -> [a] -> [String]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
rs)

    storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
    storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
storeUsage (Name
n, IntMap (Set Reason)
args) = Field IState [(Int, [Reason])] -> [(Int, [Reason])] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field CGInfo [(Int, [Reason])]
cg_usedpos Field CGInfo [(Int, [Reason])]
-> Field IState CGInfo -> Field IState [(Int, [Reason])]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n) [(Int, [Reason])]
flat
      where
        flat :: [(Int, [Reason])]
flat = [(Int
i, Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Set Reason
rs) <- IntMap (Set Reason) -> [(Int, Set Reason)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap (Set Reason)
args]

    checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
    checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility Ctxt OptInfo
opt (Name
n, IntMap (Set Reason)
reachable)
        | Just (Optimise [(Int, Name)]
inaccessible Bool
dt [Int]
force) <- Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n Ctxt OptInfo
opt
        , eargs :: [String]
eargs@(String
_:[String]
_) <- [Name -> [Reason] -> String
forall {a} {a} {a}.
(Show a, Show a, Show a) =>
a -> [(a, a)] -> String
fmt Name
n (Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Name
n) <- [(Int, Name)]
inaccessible, Set Reason
rs <- Maybe (Set Reason) -> [Set Reason]
forall a. Maybe a -> [a]
maybeToList (Maybe (Set Reason) -> [Set Reason])
-> Maybe (Set Reason) -> [Set Reason]
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Set Reason) -> Maybe (Set Reason)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Set Reason)
reachable]
        = String -> Idris ()
warn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": inaccessible arguments reachable:\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " [String]
eargs

        | Bool
otherwise = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      where
        fmt :: a -> [(a, a)] -> String
fmt a
n [] = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (no more information available)"
        fmt a
n [(a, a)]
rs = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [a -> String
forall a. Show a => a -> String
show a
rn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arg# " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ri | (a
rn,a
ri) <- [(a, a)]
rs]
        warn :: String -> Idris ()
warn = Int -> String -> Idris ()
logErasure Int
0

type Constraint = (Cond, DepSet)

-- | Find the minimal consistent usage by forward chaining.
--
-- We use a cleverer implementation that:
-- 1. First transforms Deps into a collection of numbered constraints
-- 2. For each node, we remember the numbers of constraints
--    that contain that node among their preconditions.
-- 3. When performing forward chaining, we perform unit propagation
--    only on the relevant constraints, not all constraints.
--
-- Typical numbers from the current version of Blodwen:
-- * 56 iterations until fixpoint
-- * out of 20k constraints total, 5-1000 are relevant per iteration
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage Deps
deps
    = IntMap (Cond, DepSet) -> Deps
fromNumbered (IntMap (Cond, DepSet) -> Deps)
-> (DepSet -> (Set Name, UseMap))
-> (IntMap (Cond, DepSet), DepSet)
-> (Deps, (Set Name, UseMap))
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** DepSet -> (Set Name, UseMap)
gather
    ((IntMap (Cond, DepSet), DepSet) -> (Deps, (Set Name, UseMap)))
-> (IntMap (Cond, DepSet), DepSet) -> (Deps, (Set Name, UseMap))
forall a b. (a -> b) -> a -> b
$ Map Node IntSet
-> DepSet
-> DepSet
-> IntMap (Cond, DepSet)
-> (IntMap (Cond, DepSet), DepSet)
forwardChain (IntMap (Cond, DepSet) -> Map Node IntSet
index IntMap (Cond, DepSet)
numbered) DepSet
seedDeps DepSet
seedDeps IntMap (Cond, DepSet)
numbered
  where
    numbered :: IntMap (Cond, DepSet)
numbered = Deps -> IntMap (Cond, DepSet)
toNumbered Deps
deps

    -- The initial solution. Consists of nodes that are
    -- reachable immediately, without any preconditions.
    seedDeps :: DepSet
    seedDeps :: DepSet
seedDeps = (Set Reason -> Set Reason -> Set Reason) -> [DepSet] -> DepSet
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union [DepSet
ds | (Cond
cond, DepSet
ds) <- IntMap (Cond, DepSet) -> [(Cond, DepSet)]
forall a. IntMap a -> [a]
IM.elems IntMap (Cond, DepSet)
numbered, Cond -> Bool
forall a. Set a -> Bool
S.null Cond
cond]

    toNumbered :: Deps -> IntMap Constraint
    toNumbered :: Deps -> IntMap (Cond, DepSet)
toNumbered = [(Int, (Cond, DepSet))] -> IntMap (Cond, DepSet)
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, (Cond, DepSet))] -> IntMap (Cond, DepSet))
-> (Deps -> [(Int, (Cond, DepSet))])
-> Deps
-> IntMap (Cond, DepSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Int] -> [(Cond, DepSet)] -> [(Int, (Cond, DepSet))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([(Cond, DepSet)] -> [(Int, (Cond, DepSet))])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [(Int, (Cond, DepSet))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList

    fromNumbered :: IntMap Constraint -> Deps
    fromNumbered :: IntMap (Cond, DepSet) -> Deps
fromNumbered = ((Cond, DepSet) -> Deps -> Deps)
-> Deps -> IntMap (Cond, DepSet) -> Deps
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IM.foldr (Cond, DepSet) -> Deps -> Deps
forall {k} {k} {a}.
(Ord k, Ord k, Ord a) =>
(k, Map k (Set a))
-> Map k (Map k (Set a)) -> Map k (Map k (Set a))
addConstraint Deps
forall k a. Map k a
M.empty
      where
        addConstraint :: (k, Map k (Set a))
-> Map k (Map k (Set a)) -> Map k (Map k (Set a))
addConstraint (k
ns, Map k (Set a)
vs) = (Map k (Set a) -> Map k (Set a) -> Map k (Set a))
-> k
-> Map k (Set a)
-> Map k (Map k (Set a))
-> Map k (Map k (Set a))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set a -> Set a -> Set a)
-> Map k (Set a) -> Map k (Set a) -> Map k (Set a)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.union) k
ns Map k (Set a)
vs

    -- Build an index that maps every node to the set of constraints
    -- where the node appears among the preconditions.
    index :: IntMap Constraint -> Map Node IntSet
    index :: IntMap (Cond, DepSet) -> Map Node IntSet
index = (Int -> (Cond, DepSet) -> Map Node IntSet -> Map Node IntSet)
-> Map Node IntSet -> IntMap (Cond, DepSet) -> Map Node IntSet
forall a b. (Int -> a -> b -> b) -> b -> IntMap a -> b
IM.foldrWithKey (
            -- for each clause (i. ns --> _ds)
            \Int
i (Cond
ns, DepSet
_ds) Map Node IntSet
ix -> (Node -> Map Node IntSet -> Map Node IntSet)
-> Map Node IntSet -> [Node] -> Map Node IntSet
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (
                -- for each node `n` in `ns`
                \Node
n Map Node IntSet
ix' -> (IntSet -> IntSet -> IntSet)
-> Node -> IntSet -> Map Node IntSet -> Map Node IntSet
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith IntSet -> IntSet -> IntSet
IS.union Node
n (Int -> IntSet
IS.singleton Int
i) Map Node IntSet
ix'
              ) Map Node IntSet
ix (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
ns)
        ) Map Node IntSet
forall k a. Map k a
M.empty

    -- Convert a solution of constraints into:
    -- 1. the list of names used in the program
    -- 2. the list of arguments used, together with their reasons
    gather :: DepSet -> (Set Name, UseMap)
    gather :: DepSet -> (Set Name, UseMap)
gather = ((Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap))
-> (Set Name, UseMap) -> [(Node, Set Reason)] -> (Set Name, UseMap)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins (Set Name
forall a. Set a
S.empty, UseMap
forall k a. Map k a
M.empty) ([(Node, Set Reason)] -> (Set Name, UseMap))
-> (DepSet -> [(Node, Set Reason)]) -> DepSet -> (Set Name, UseMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. DepSet -> [(Node, Set Reason)]
forall k a. Map k a -> [(k, a)]
M.toList
       where
        ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
        ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins ((Name
n, Arg
Result), Set Reason
rs) (Set Name
ns, UseMap
umap) = (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
n Set Name
ns, UseMap
umap)
        ins ((Name
n, Arg Int
i ), Set Reason
rs) (Set Name
ns, UseMap
umap) = (Set Name
ns, (IntMap (Set Reason) -> IntMap (Set Reason) -> IntMap (Set Reason))
-> Name -> IntMap (Set Reason) -> UseMap -> UseMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> IntMap (Set Reason)
-> IntMap (Set Reason)
-> IntMap (Set Reason)
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Name
n (Int -> Set Reason -> IntMap (Set Reason)
forall a. Int -> a -> IntMap a
IM.singleton Int
i Set Reason
rs) UseMap
umap)

-- | In each iteration, we find the set of nodes immediately reachable
-- from the current set of constraints, and then reduce the set of constraints
-- based on that knowledge.
--
-- In the implementation, this is phase-shifted. We first reduce the set
-- of constraints, given the newly reachable nodes from the previous iteration,
-- and then compute the set of currently reachable nodes.
-- Then we decide whether to iterate further.
forwardChain
    :: Map Node IntSet   -- ^ node index
    -> DepSet            -- ^ all reachable nodes found so far
    -> DepSet            -- ^ nodes reached in the previous iteration
    -> IntMap Constraint -- ^ numbered constraints
    -> (IntMap Constraint, DepSet)
forwardChain :: Map Node IntSet
-> DepSet
-> DepSet
-> IntMap (Cond, DepSet)
-> (IntMap (Cond, DepSet), DepSet)
forwardChain Map Node IntSet
index DepSet
solution DepSet
previouslyNew IntMap (Cond, DepSet)
constrs
    -- no newly reachable nodes, fixed point has been reached
    | DepSet -> Bool
forall k a. Map k a -> Bool
M.null DepSet
currentlyNew
    = (IntMap (Cond, DepSet)
constrs, DepSet
solution)

    -- some newly reachable nodes, iterate more
    | Bool
otherwise
    = Map Node IntSet
-> DepSet
-> DepSet
-> IntMap (Cond, DepSet)
-> (IntMap (Cond, DepSet), DepSet)
forwardChain Map Node IntSet
index
        ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union DepSet
solution DepSet
currentlyNew)
        DepSet
currentlyNew
        IntMap (Cond, DepSet)
constrs'
  where
    -- which constraints could give new results,
    -- given that `previouslyNew` has been derived in the last iteration
    affectedIxs :: IntSet
affectedIxs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions [
        IntSet -> Node -> Map Node IntSet -> IntSet
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault IntSet
IS.empty Node
n Map Node IntSet
index
        | Node
n <- DepSet -> [Node]
forall k a. Map k a -> [k]
M.keys DepSet
previouslyNew
      ]

    -- traverse all (potentially) affected constraints, building:
    -- 1. a set of newly reached nodes
    -- 2. updated set of constraints where the previously
    --    reached nodes have been removed
    (DepSet
currentlyNew, IntMap (Cond, DepSet)
constrs')
        = (Int
 -> (DepSet, IntMap (Cond, DepSet))
 -> (DepSet, IntMap (Cond, DepSet)))
-> (DepSet, IntMap (Cond, DepSet))
-> IntSet
-> (DepSet, IntMap (Cond, DepSet))
forall b. (Int -> b -> b) -> b -> IntSet -> b
IS.foldr
            (Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
reduceConstraint (Cond
 -> Int
 -> (DepSet, IntMap (Cond, DepSet))
 -> (DepSet, IntMap (Cond, DepSet)))
-> Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
forall a b. (a -> b) -> a -> b
$ DepSet -> Cond
forall k a. Map k a -> Set k
M.keysSet DepSet
previouslyNew)
            (DepSet
forall k a. Map k a
M.empty, IntMap (Cond, DepSet)
constrs)
            IntSet
affectedIxs

    -- Update the pair (newly reached nodes, numbered constraint set)
    -- by reducing the constraint with the given number.
    reduceConstraint
        :: Set Node  -- ^ nodes reached in the previous iteration
        -> Int       -- ^ constraint number
        -> (DepSet, IntMap (Cond, DepSet))
        -> (DepSet, IntMap (Cond, DepSet))
    reduceConstraint :: Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
reduceConstraint Cond
previouslyNew Int
i (DepSet
news, IntMap (Cond, DepSet)
constrs)
        | Just (Cond
cond, DepSet
deps) <- Int -> IntMap (Cond, DepSet) -> Maybe (Cond, DepSet)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Cond, DepSet)
constrs
        = case Cond
cond Cond -> Cond -> Cond
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Cond
previouslyNew of
            Cond
cond'
                -- This constraint's set of preconditions has shrunk
                -- to the empty set. We can add its RHS to the set of newly
                -- reached nodes, and remove the constraint altogether.
                | Cond -> Bool
forall a. Set a -> Bool
S.null Cond
cond'
                -> ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union DepSet
news DepSet
deps, Int -> IntMap (Cond, DepSet) -> IntMap (Cond, DepSet)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap (Cond, DepSet)
constrs)

                -- This constraint's set of preconditions has shrunk
                -- so we need to overwrite the numbered slot
                -- with the updated constraint.
                | Cond -> Int
forall a. Set a -> Int
S.size Cond
cond' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Cond -> Int
forall a. Set a -> Int
S.size Cond
cond
                -> (DepSet
news, Int
-> (Cond, DepSet) -> IntMap (Cond, DepSet) -> IntMap (Cond, DepSet)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (Cond
cond', DepSet
deps) IntMap (Cond, DepSet)
constrs)

                -- This constraint's set of preconditions hasn't changed
                -- so we do not do anything about it.
                | Bool
otherwise
                -> (DepSet
news, IntMap (Cond, DepSet)
constrs)

        -- Constraint number present in index but not found
        -- among the constraints. This happens more and more frequently
        -- as we delete constraints from the set.
        | Bool
otherwise = (DepSet
news, IntMap (Cond, DepSet)
constrs)

-- | Build the dependency graph, starting the depth-first search from
-- a list of Names.
buildDepMap :: Ctxt InterfaceInfo -> [(Name, Int)] -> [(Name, Int)] ->
               Context -> [Name] -> Deps
buildDepMap :: Ctxt InterfaceInfo
-> [Reason] -> [Reason] -> Context -> [Name] -> Deps
buildDepMap Ctxt InterfaceInfo
ci [Reason]
used [Reason]
externs Context
ctx [Name]
startNames
    = [Reason] -> Deps -> Deps
addPostulates [Reason]
used (Deps -> Deps) -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ Set Name -> Deps -> [Name] -> Deps
dfs Set Name
forall a. Set a
S.empty Deps
forall k a. Map k a
M.empty [Name]
startNames
  where
    -- mark the result of Main.main as used with the empty assumption
    addPostulates :: [(Name, Int)] -> Deps -> Deps
    addPostulates :: [Reason] -> Deps -> Deps
addPostulates [Reason]
used Deps
deps = ((Cond, DepSet) -> Deps -> Deps)
-> Deps -> [(Cond, DepSet)] -> Deps
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Cond
ds, DepSet
rs) -> (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
ds DepSet
rs) Deps
deps ([Reason] -> [(Cond, DepSet)]
forall {a} {a}. Ord a => [Reason] -> [(Set a, Map Node (Set a))]
postulates [Reason]
used)
      where
        -- mini-DSL for postulates
        ==> :: [a] -> [k] -> (Set a, Map k (Set a))
(==>) [a]
ds [k]
rs = ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
ds, [(k, Set a)] -> Map k (Set a)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(k
r, Set a
forall a. Set a
S.empty) | k
r <- [k]
rs])
        it :: String -> [Int] -> [Node]
it String
n [Int]
is = [(String -> Name
sUN String
n, Int -> Arg
Arg Int
i) | Int
i <- [Int]
is]

        -- believe_me is special because it does not use all its arguments
        specialPrims :: Set Name
specialPrims = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList [String -> Name
sUN String
"prim__believe_me"]
        usedNames :: Set Name
usedNames = Deps -> Set Name
allNames Deps
deps Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set Name
specialPrims
        usedPrims :: [Reason]
usedPrims = [(Prim -> Name
p_name Prim
p, Prim -> Int
p_arity Prim
p) | Prim
p <- [Prim]
primitives, Prim -> Name
p_name Prim
p Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Name
usedNames]

        postulates :: [Reason] -> [(Set a, Map Node (Set a))]
postulates [Reason]
used =
            [ [] [a] -> [Node] -> (Set a, Map Node (Set a))
forall {a} {k} {a}.
(Ord a, Ord k) =>
[a] -> [k] -> (Set a, Map k (Set a))
==> [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                -- Main.main ( + export lists) and run__IO, are always evaluated
                -- but they elude analysis since they come from the seed term.
                [((Name -> Node) -> [Name] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Arg
Result)) [Name]
startNames)
                ,[(String -> Name
sUN String
"run__IO", Arg
Result), (String -> Name
sUN String
"run__IO", Int -> Arg
Arg Int
1)]
                ,[(String -> Name
sUN String
"call__IO", Arg
Result), (String -> Name
sUN String
"call__IO", Int -> Arg
Arg Int
2)]

                -- Explicit usage declarations from a %used pragma
                , (Reason -> Node) -> [Reason] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Int
i) -> (Name
n, Int -> Arg
Arg Int
i)) [Reason]
used

                -- MkIO is read by run__IO,
                -- but this cannot be observed in the source code of programs.
                , String -> [Int] -> [Node]
it String
"MkIO"         [Int
2]
                , String -> [Int] -> [Node]
it String
"prim__IO"     [Int
1]

                -- Foreign calls are built with pairs, but mkForeign doesn't
                -- have an implementation so analysis won't see them
                , [(Name
pairCon, Int -> Arg
Arg Int
2),
                   (Name
pairCon, Int -> Arg
Arg Int
3)] -- Used in foreign calls

                -- these have been discovered as builtins but are not listed
                -- among Idris.Primitives.primitives
                --, mn "__MkPair"     [2,3]
                , String -> [Int] -> [Node]
it String
"prim_fork"    [Int
0]
                , String -> [Int] -> [Node]
it String
"unsafePerformPrimIO"  [Int
1]

                -- believe_me is a primitive but it only uses its third argument
                -- it is special-cased in usedNames above
                , String -> [Int] -> [Node]
it String
"prim__believe_me" [Int
2]

                -- in general, all other primitives use all their arguments
                , [(Name
n, Int -> Arg
Arg Int
i) | (Name
n,Int
arity) <- [Reason]
usedPrims, Int
i <- [Int
0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]

                -- %externs are assumed to use all their arguments
                , [(Name
n, Int -> Arg
Arg Int
i) | (Name
n,Int
arity) <- [Reason]
externs, Int
i <- [Int
0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]

                -- mkForeign* functions are special-cased below
                ]
            ]

    -- perform depth-first search
    -- to discover all the names used in the program
    -- and call getDeps for every name
    dfs :: Set Name -> Deps -> [Name] -> Deps
    dfs :: Set Name -> Deps -> [Name] -> Deps
dfs Set Name
visited Deps
deps [] = Deps
deps
    dfs Set Name
visited Deps
deps (Name
n : [Name]
ns)
        | Name
n Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Name
visited = Set Name -> Deps -> [Name] -> Deps
dfs Set Name
visited Deps
deps [Name]
ns
        | Bool
otherwise = Set Name -> Deps -> [Name] -> Deps
dfs (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
n Set Name
visited) ((DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Deps
deps' Deps
deps) ([Name]
next [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
ns)
      where
        next :: [Name]
next = [Name
n | Name
n <- Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
depn, Name
n Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Name
visited]
        depn :: Set Name
depn = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.delete Name
n (Set Name -> Set Name) -> Set Name -> Set Name
forall a b. (a -> b) -> a -> b
$ Deps -> Set Name
allNames Deps
deps'
        deps' :: Deps
deps' = Name -> Deps
getDeps Name
n

    -- extract all names that a function depends on
    -- from the Deps of the function
    allNames :: Deps -> Set Name
    allNames :: Deps -> Set Name
allNames = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Name] -> Set Name)
-> (Deps -> [Set Name]) -> Deps -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Cond, DepSet) -> Set Name) -> [(Cond, DepSet)] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> Set Name
forall {a} {b} {b} {a}.
Ord a =>
(Set (a, b), Map (a, b) a) -> Set a
names ([(Cond, DepSet)] -> [Set Name])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [Set Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList
        where
        names :: (Set (a, b), Map (a, b) a) -> Set a
names (Set (a, b)
cs, Map (a, b) a
ns) = ((a, b) -> a) -> Set (a, b) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, b) -> a
forall a b. (a, b) -> a
fst Set (a, b)
cs Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` ((a, b) -> a) -> Set (a, b) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, b) -> a
forall a b. (a, b) -> a
fst (Map (a, b) a -> Set (a, b)
forall k a. Map k a -> Set k
M.keysSet Map (a, b) a
ns)

    -- get Deps for a Name
    getDeps :: Name -> Deps
    getDeps :: Name -> Deps
getDeps (SN (WhereN Int
i (SN (ImplementationCtorN Name
interfaceN)) (MN Int
i' Text
field)))
        = Deps
forall k a. Map k a
M.empty  -- these deps are created when applying implementation ctors
    getDeps Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
        Just Def
def -> Name -> Def -> Deps
getDepsDef Name
n Def
def
        Maybe Def
Nothing  -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"erasure checker: unknown reference: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n

    getDepsDef :: Name -> Def -> Deps
    getDepsDef :: Name -> Def -> Deps
getDepsDef Name
fn (Function TT Name
ty TT Name
t) = String -> Deps
forall a. HasCallStack => String -> a
error String
"a function encountered"  -- TODO
    getDepsDef Name
fn (TyDecl   NameType
ty TT Name
t) = Deps
forall k a. Map k a
M.empty
    getDepsDef Name
fn (Operator TT Name
ty Int
n' [Value] -> Maybe Value
f) = Deps
forall k a. Map k a
M.empty  -- TODO: what's this?
    getDepsDef Name
fn (CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
tys [Either (TT Name) (TT Name, TT Name)]
def [([Name], TT Name, TT Name)]
tot CaseDefs
cdefs)
        = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
etaVars (Vars
etaMap Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
varMap) SC' (TT Name)
sc
      where
        -- we must eta-expand the definition with fresh variables
        -- to capture these dependencies as well
        etaIdx :: [Int]
etaIdx = [[Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
vars .. [(TT Name, Bool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(TT Name, Bool)]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        etaVars :: [Name]
etaVars = [Int -> Name
eta Int
i | Int
i <- [Int]
etaIdx]
        etaMap :: Vars
etaMap = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [Name -> Int -> (Name, VarInfo)
forall {a}. a -> Int -> (a, VarInfo)
varPair (Int -> Name
eta Int
i) Int
i | Int
i <- [Int]
etaIdx]
        eta :: Int -> Name
eta Int
i = Int -> Text -> Name
MN Int
i (String -> Text
pack String
"eta")

        -- the variables that arose as function arguments only depend on (n, i)
        varMap :: Vars
varMap = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [Name -> Int -> (Name, VarInfo)
forall {a}. a -> Int -> (a, VarInfo)
varPair Name
v Int
i | (Name
v,Int
i) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars [Int
0..]]

        varPair :: a -> Int -> (a, VarInfo)
varPair a
n Int
argNo = (a
n, VI
            { viDeps :: DepSet
viDeps   = Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
fn, Int -> Arg
Arg Int
argNo) Set Reason
forall a. Set a
S.empty
            , viFunArg :: Maybe Int
viFunArg = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
argNo
            , viMethod :: Maybe Name
viMethod = Maybe Name
forall a. Maybe a
Nothing
            })

        ([Name]
vars, SC' (TT Name)
sc) = CaseDefs -> ([Name], SC' (TT Name))
cases_runtime CaseDefs
cdefs
            -- we use cases_runtime in order to have case-blocks
            -- resolved to top-level functions before our analysis

    etaExpand :: [Name] -> Term -> Term
    etaExpand :: [Name] -> TT Name -> TT Name
etaExpand []       TT Name
t = TT Name
t
    etaExpand (Name
n : [Name]
ns) TT Name
t = [Name] -> TT Name -> TT Name
etaExpand [Name]
ns (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete TT Name
t (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n TT Name
forall n. TT n
Erased))

    getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
    getDepsSC :: Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs  SC' (TT Name)
ImpossibleCase     = Deps
forall k a. Map k a
M.empty
    getDepsSC Name
fn [Name]
es Vars
vs (UnmatchedCase String
msg) = Deps
forall k a. Map k a
M.empty

    -- for the purposes of erasure, we can disregard the projection
    getDepsSC Name
fn [Name]
es Vars
vs (ProjCase (Proj TT Name
t Int
i) [CaseAlt' (TT Name)]
alts) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (TT Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)  -- step
    getDepsSC Name
fn [Name]
es Vars
vs (ProjCase (P  NameType
_ Name
n TT Name
_) [CaseAlt' (TT Name)]
alts) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (CaseType -> Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
Shared Name
n [CaseAlt' (TT Name)]
alts)  -- base

    -- other ProjCase's are not supported
    getDepsSC Name
fn [Name]
es Vars
vs (ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)   = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"ProjCase not supported:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC' (TT Name) -> String
forall a. Show a => a -> String
show (TT Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)

    getDepsSC Name
fn [Name]
es Vars
vs (STerm    TT Name
t)        = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [] (Node -> Cond
forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) ([Name] -> TT Name -> TT Name
etaExpand [Name]
es TT Name
t)
    getDepsSC Name
fn [Name]
es Vars
vs (Case CaseType
sh Name
n [CaseAlt' (TT Name)]
alts)
        -- we case-split on this variable, which marks it as used
        -- (unless there is exactly one case branch)
        -- hence we add a new dependency, whose only precondition is
        -- that the result of this function is used at all
        = Deps -> Deps
addTagDep (Deps -> Deps) -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ (CaseAlt' (TT Name) -> Deps) -> [CaseAlt' (TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> [Name] -> Vars -> VarInfo -> CaseAlt' (TT Name) -> Deps
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
casedVar) [CaseAlt' (TT Name)]
alts  -- coming from the whole subtree
      where
        addTagDep :: Deps -> Deps
addTagDep = case [CaseAlt' (TT Name)]
alts of
            [CaseAlt' (TT Name)
_] -> Deps -> Deps
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id  -- single branch, tag not used
            [CaseAlt' (TT Name)]
_   -> (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) (Node -> Cond
forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) (VarInfo -> DepSet
viDeps VarInfo
casedVar)
        casedVar :: VarInfo
casedVar  = VarInfo -> Maybe VarInfo -> VarInfo
forall a. a -> Maybe a -> a
fromMaybe (String -> VarInfo
forall a. HasCallStack => String -> a
error (String -> VarInfo) -> String -> VarInfo
forall a b. (a -> b) -> a -> b
$ String
"nonpatvar in case: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n) (Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs)

    getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt -> Deps
    getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt' (TT Name) -> Deps
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (FnCase Name
n [Name]
ns SC' (TT Name)
sc) = Deps
forall k a. Map k a
M.empty -- can't use FnCase at runtime
    getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (ConstCase Const
c SC' (TT Name)
sc) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC' (TT Name)
sc
    getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (DefaultCase SC' (TT Name)
sc) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC' (TT Name)
sc
    getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (SucCase   Name
n SC' (TT Name)
sc)
        = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es (Name -> VarInfo -> Vars -> Vars
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
n VarInfo
var Vars
vs) SC' (TT Name)
sc -- we're not inserting the S-dependency here because it's special-cased

    -- data constructors
    getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (ConCase Name
n Int
cnt [Name]
ns SC' (TT Name)
sc)
        = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es (Vars
vs' Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) SC' (TT Name)
sc  -- left-biased union
      where
        -- Here we insert dependencies that arose from pattern matching on a constructor.
        -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
        vs' :: Vars
vs' = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
            { viDeps :: DepSet
viDeps   = (Set Reason -> Set Reason -> Set Reason)
-> Node -> Set Reason -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union (Name
n, Int -> Arg
Arg Int
j) (Reason -> Set Reason
forall a. a -> Set a
S.singleton (Name
fn, Int
varIdx)) (VarInfo -> DepSet
viDeps VarInfo
var)
            , viFunArg :: Maybe Int
viFunArg = VarInfo -> Maybe Int
viFunArg VarInfo
var
            , viMethod :: Maybe Name
viMethod = Int -> Maybe Name
meth Int
j
            })
          | (Name
v, Int
j) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Int
0..]]

        -- this is safe because it's certainly a patvar
        varIdx :: Int
varIdx = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (VarInfo -> Maybe Int
viFunArg VarInfo
var)

        -- generate metamethod names, "n" is the implementation ctor
        meth :: Int -> Maybe Name
        meth :: Int -> Maybe Name
meth | SN (ImplementationCtorN Name
interfaceName) <- Name
n = \Int
j -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Int -> Name
mkFieldName Name
n Int
j)
             | Bool
otherwise = \Int
j -> Maybe Name
forall a. Maybe a
Nothing

    -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
    getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps

    -- named variables introduce dependencies as described in `vs'
    getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (P NameType
_ Name
n TT Name
_)
        -- de bruijns (lambda-bound, let-bound vars)
        | Just Cond -> Deps
deps <- Name -> [(Name, Cond -> Deps)] -> Maybe (Cond -> Deps)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Cond -> Deps)]
bs
        = Cond -> Deps
deps Cond
cd

        -- ctor-bound/arg-bound variables
        | Just VarInfo
var <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
        = Cond -> DepSet -> Deps
forall k a. k -> a -> Map k a
M.singleton Cond
cd (VarInfo -> DepSet
viDeps VarInfo
var)

        -- sanity check: machine-generated names shouldn't occur at top-level
        | MN Int
_ Text
_ <- Name
n
        = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"erasure analysis: variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" unbound in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node] -> String
forall a. Show a => a -> String
show (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
cd)

        -- assumed to be a global reference
        | Bool
otherwise = Cond -> DepSet -> Deps
forall k a. k -> a -> Map k a
M.singleton Cond
cd (Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set Reason
forall a. Set a
S.empty)

    -- dependencies of de bruijn variables are described in `bs'
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (V Int
i) = (Name, Cond -> Deps) -> Cond -> Deps
forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs [(Name, Cond -> Deps)] -> Int -> (Name, Cond -> Deps)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Cond
cd

    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Bind Name
n Binder (TT Name)
bdr TT Name
body)
        -- here we just push IM.empty on the de bruijn stack
        -- the args will be marked as used at the usage site
        | Lam RigCount
_ TT Name
ty <- Binder (TT Name)
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
        | Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
ty TT Name
_ <- Binder (TT Name)
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body

        -- let-bound variables can get partially evaluated
        -- it is sufficient just to plug the Cond in when the bound names are used
        | Let RigCount
rig TT Name
ty TT Name
t <- Binder (TT Name)
bdr = TT Name -> Cond -> Deps
var TT Name
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
        | NLet TT Name
ty TT Name
t <- Binder (TT Name)
bdr = TT Name -> Cond -> Deps
var TT Name
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
      where
        var :: TT Name -> Cond -> Deps
var TT Name
t Cond
cd = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t

    -- applications may add items to Cond
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd app :: TT Name
app@(App AppStatus Name
_ TT Name
_ TT Name
_)
        | (TT Name
fun, [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
app = case TT Name
fun of
            -- implementation constructors -> create metamethod deps
            P (DCon Int
_ Int
_ Bool
_) ctorName :: Name
ctorName@(SN (ImplementationCtorN Name
interfaceName)) TT Name
_
                -> Name -> [TT Name] -> Deps
conditionalDeps Name
ctorName [TT Name]
args  -- regular data ctor stuff
                    Deps -> Deps -> Deps
`union` ((Int, TT Name) -> Deps) -> [(Int, TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Int, TT Name) -> Deps
methodDeps Name
ctorName) ([Int] -> [TT Name] -> [(Int, TT Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [TT Name]
args)  -- method-specific stuff

            -- ordinary constructors
            P (TCon Int
_ Int
_) Name
n TT Name
_ -> [TT Name] -> Deps
unconditionalDeps [TT Name]
args  -- does not depend on anything
            P (DCon Int
_ Int
_ Bool
_) Name
n TT Name
_ -> Name -> [TT Name] -> Deps
conditionalDeps Name
n [TT Name]
args  -- depends on whether (n,#) is used

            -- mkForeign* calls must be special-cased because they are variadic
            -- All arguments must be marked as used, except for the first four,
            -- which define the call type and are not needed at runtime.
            P NameType
_ (UN Text
n) TT Name
_
                | Text
n Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"mkForeignPrim"
                -> [TT Name] -> Deps
unconditionalDeps ([TT Name] -> Deps) -> [TT Name] -> Deps
forall a b. (a -> b) -> a -> b
$ Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop Int
4 [TT Name]
args

            -- a bound variable might draw in additional dependencies,
            -- think: f x = x 0  <-- here, `x' _is_ used
            P NameType
_ Name
n TT Name
_
                -- debruijn-bound name
                | Just Cond -> Deps
deps <- Name -> [(Name, Cond -> Deps)] -> Maybe (Cond -> Deps)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Cond -> Deps)]
bs
                    -> Cond -> Deps
deps Cond
cd Deps -> Deps -> Deps
`union` [TT Name] -> Deps
unconditionalDeps [TT Name]
args

                -- local name that refers to a method
                | Just VarInfo
var  <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
                , Just Name
meth <- VarInfo -> Maybe Name
viMethod VarInfo
var
                    -> VarInfo -> DepSet
viDeps VarInfo
var DepSet -> Deps -> Deps
`ins` Name -> [TT Name] -> Deps
conditionalDeps Name
meth [TT Name]
args  -- use the method instead

                -- local name
                | Just VarInfo
var <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
                    -- unconditional use
                    -> VarInfo -> DepSet
viDeps VarInfo
var DepSet -> Deps -> Deps
`ins` [TT Name] -> Deps
unconditionalDeps [TT Name]
args

                -- global name
                | Bool
otherwise
                    -- depends on whether the referred thing uses its argument
                    -> Name -> [TT Name] -> Deps
conditionalDeps Name
n [TT Name]
args

            -- TODO: could we somehow infer how bound variables use their arguments?
            V Int
i -> (Name, Cond -> Deps) -> Cond -> Deps
forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs [(Name, Cond -> Deps)] -> Int -> (Name, Cond -> Deps)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Cond
cd Deps -> Deps -> Deps
`union` [TT Name] -> Deps
unconditionalDeps [TT Name]
args

            -- we interpret applied lambdas as lets in order to reuse code here
            Bind Name
n (Lam RigCount
_ TT Name
ty) TT Name
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (TT Name -> TT Name
lamToLet TT Name
app)

            -- and we interpret applied lets as lambdas
            Bind Name
n (Let RigCount
_ TT Name
ty TT Name
t') TT Name
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
t) TT Name
t')
            Bind Name
n (NLet TT Name
ty TT Name
t') TT Name
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
t) TT Name
t')

            Proj TT Name
t Int
i
                -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot[0] analyse projection !" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t

            TT Name
Erased -> Deps
forall k a. Map k a
M.empty

            TT Name
_ -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot analyse application of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
fun String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [TT Name] -> String
forall a. Show a => a -> String
show [TT Name]
args
      where
        union :: Deps -> Deps -> Deps
union = (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps)
-> (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ (Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union
        ins :: DepSet -> Deps -> Deps
ins = (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
cd

        unconditionalDeps :: [Term] -> Deps
        unconditionalDeps :: [TT Name] -> Deps
unconditionalDeps = (TT Name -> Deps) -> [TT Name] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd)

        conditionalDeps :: Name -> [Term] -> Deps
        conditionalDeps :: Name -> [TT Name] -> Deps
conditionalDeps Name
n
            = DepSet -> Deps -> Deps
ins (Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set Reason
forall a. Set a
S.empty) (Deps -> Deps) -> ([TT Name] -> Deps) -> [TT Name] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Maybe Int, TT Name) -> Deps) -> [(Maybe Int, TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Maybe Int, TT Name) -> Deps
getDepsArgs Name
n) ([(Maybe Int, TT Name)] -> Deps)
-> ([TT Name] -> [(Maybe Int, TT Name)]) -> [TT Name] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Maybe Int] -> [TT Name] -> [(Maybe Int, TT Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Int]
indices
          where
            indices :: [Maybe Int]
indices = (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int
0 .. Name -> Int
getArity Name
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ Maybe Int -> [Maybe Int]
forall a. a -> [a]
repeat Maybe Int
forall a. Maybe a
Nothing
            getDepsArgs :: Name -> (Maybe Int, TT Name) -> Deps
getDepsArgs Name
n (Just Int
i,  TT Name
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs (Node -> Cond -> Cond
forall a. Ord a => a -> Set a -> Set a
S.insert (Name
n, Int -> Arg
Arg Int
i) Cond
cd) TT Name
t  -- conditional
            getDepsArgs Name
n (Maybe Int
Nothing, TT Name
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t                        -- unconditional

        methodDeps :: Name -> (Int, Term) -> Deps
        methodDeps :: Name -> (Int, TT Name) -> Deps
methodDeps Name
ctorName (Int
methNo, TT Name
t)
            = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm (Vars
vars Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) ([(Name, Cond -> Deps)]
forall {k} {a}. [(Name, k -> Map k (Map Node (Set a)))]
bruijns [(Name, Cond -> Deps)]
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. [a] -> [a] -> [a]
++ [(Name, Cond -> Deps)]
bs) Cond
cond TT Name
body
          where
            vars :: Vars
vars = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
                { viDeps :: DepSet
viDeps   = Int -> DepSet
forall {a}. Int -> Map Node (Set a)
deps Int
i
                , viFunArg :: Maybe Int
viFunArg = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
                , viMethod :: Maybe Name
viMethod = Maybe Name
forall a. Maybe a
Nothing
                }) | (Name
v, Int
i) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [Int
0..]]
            deps :: Int -> Map Node (Set a)
deps Int
i   = Node -> Set a -> Map Node (Set a)
forall k a. k -> a -> Map k a
M.singleton (Name
metameth, Int -> Arg
Arg Int
i) Set a
forall a. Set a
S.empty
            bruijns :: [(Name, k -> Map k (Map Node (Set a)))]
bruijns  = [(Name, k -> Map k (Map Node (Set a)))]
-> [(Name, k -> Map k (Map Node (Set a)))]
forall a. [a] -> [a]
reverse [(Name
n, \k
cd -> k -> Map Node (Set a) -> Map k (Map Node (Set a))
forall k a. k -> a -> Map k a
M.singleton k
cd (Int -> Map Node (Set a)
forall {a}. Int -> Map Node (Set a)
deps Int
i)) | (Int
i, Name
n) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
args]
            cond :: Cond
cond     = Node -> Cond
forall a. a -> Set a
S.singleton (Name
metameth, Arg
Result)
            metameth :: Name
metameth = Name -> Int -> Name
mkFieldName Name
ctorName Int
methNo
            ([Name]
args, TT Name
body) = TT Name -> ([Name], TT Name)
unfoldLams TT Name
t

    -- projections
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Proj TT Name
t (-1)) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t  -- naturals, (S n) -> n
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Proj TT Name
t Int
i) = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot[1] analyse projection !" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t

    -- inferred term
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Inferred TT Name
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t

    -- the easy cases
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Constant Const
_) = Deps
forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (TType    UExp
_) = Deps
forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (UType    Universe
_) = Deps
forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd  TT Name
Erased      = Deps
forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd  TT Name
Impossible  = Deps
forall k a. Map k a
M.empty

    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot get deps of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t

    -- Get the number of arguments that might be considered for erasure.
    getArity :: Name -> Int
    getArity :: Name -> Int
getArity (SN (WhereN Int
i' Name
ctorName (MN Int
i Text
field)))
        | Just (TyDecl (DCon Int
_ Int
_ Bool
_) TT Name
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
ctorName Context
ctx
        = let argTys :: [TT Name]
argTys = ((Name, TT Name) -> TT Name) -> [(Name, TT Name)] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd ([(Name, TT Name)] -> [TT Name]) -> [(Name, TT Name)] -> [TT Name]
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ty
            in if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [TT Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT Name]
argTys
                then [(Name, TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, TT Name)] -> Int) -> [(Name, TT Name)] -> Int
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys ([TT Name]
argTys [TT Name] -> Int -> TT Name
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
                else String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"invalid field number " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ctorName

        | Bool
otherwise = String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"unknown implementation constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ctorName

    getArity Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
        Just (CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
tys [Either (TT Name) (TT Name, TT Name)]
def [([Name], TT Name, TT Name)]
tot CaseDefs
cdefs) -> [(TT Name, Bool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(TT Name, Bool)]
tys
        Just (TyDecl (DCon Int
tag Int
arity Bool
_) TT Name
_)    -> Int
arity
        Just (TyDecl (NameType
Ref) TT Name
ty)                -> [(Name, TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, TT Name)] -> Int) -> [(Name, TT Name)] -> Int
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ty
        Just (Operator TT Name
ty Int
arity [Value] -> Maybe Value
op)           -> Int
arity
        Just Def
df -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: unrecognised entity '"
                             String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' with definition: "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Def -> String
forall a. Show a => a -> String
show Def
df
        Maybe Def
Nothing -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: definition not found for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n

    -- convert applications of lambdas to lets
    -- note that this transformation preserves de bruijn numbering
    lamToLet :: Term -> Term
    lamToLet :: TT Name -> TT Name
lamToLet TT Name
tm = Int -> [TT Name] -> TT Name -> TT Name
lamToLet' Int
0 [TT Name]
args TT Name
f
      where
        (TT Name
f, [TT Name]
args) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm

    lamToLet' :: Int -> [Term] -> Term -> Term
    lamToLet' :: Int -> [TT Name] -> TT Name -> TT Name
lamToLet' Int
wk (TT Name
v:[TT Name]
vs) (Bind Name
n (Lam RigCount
rig TT Name
ty) TT Name
tm) = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig TT Name
ty (Int -> TT Name -> TT Name
forall n. Int -> TT n -> TT n
weakenTm Int
wk TT Name
v)) (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ Int -> [TT Name] -> TT Name -> TT Name
lamToLet' (Int
wkInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [TT Name]
vs TT Name
tm
    lamToLet' Int
wk    [TT Name]
vs  TT Name
tm = TT Name -> [TT Name] -> TT Name
forall n. TT n -> [TT n] -> TT n
mkApp TT Name
tm ([TT Name] -> TT Name) -> [TT Name] -> TT Name
forall a b. (a -> b) -> a -> b
$ (TT Name -> TT Name) -> [TT Name] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TT Name -> TT Name
forall n. Int -> TT n -> TT n
weakenTm Int
wk) [TT Name]
vs

    -- split "\x_i -> T(x_i)" into [x_i] and T
    unfoldLams :: Term -> ([Name], Term)
    unfoldLams :: TT Name -> ([Name], TT Name)
unfoldLams (Bind Name
n (Lam RigCount
_ TT Name
ty) TT Name
t) = let ([Name]
ns,TT Name
t') = TT Name -> ([Name], TT Name)
unfoldLams TT Name
t in (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns, TT Name
t')
    unfoldLams TT Name
t = ([], TT Name
t)

    union :: Deps -> Deps -> Deps
    union :: Deps -> Deps -> Deps
union = (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union)

    unionMap :: (a -> Deps) -> [a] -> Deps
    unionMap :: forall a. (a -> Deps) -> [a] -> Deps
unionMap a -> Deps
f = (DepSet -> DepSet -> DepSet) -> [Deps] -> Deps
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) ([Deps] -> Deps) -> ([a] -> [Deps]) -> [a] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Deps) -> [a] -> [Deps]
forall a b. (a -> b) -> [a] -> [b]
map a -> Deps
f

-- | Make a field name out of a data constructor name and field number.
mkFieldName :: Name -> Int -> Name
mkFieldName :: Name -> Int -> Name
mkFieldName Name
ctorName Int
fieldNo = SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
fieldNo Name
ctorName (Name -> SpecialName) -> Name -> SpecialName
forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
fieldNo String
"field")