{-|
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.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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Arg -> Arg -> Bool
$c/= :: Arg -> Arg -> Bool
== :: Arg -> Arg -> Bool
$c== :: Arg -> Arg -> Bool
Eq, Eq 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
min :: Arg -> Arg -> Arg
$cmin :: Arg -> Arg -> Arg
max :: Arg -> Arg -> Arg
$cmax :: Arg -> Arg -> Arg
>= :: Arg -> Arg -> Bool
$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
compare :: Arg -> Arg -> Ordering
$ccompare :: Arg -> Arg -> Ordering
Ord)

instance Show Arg where
    show :: Arg -> String
show (Arg Int
i) = 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarInfo] -> ShowS
$cshowList :: [VarInfo] -> ShowS
show :: VarInfo -> String
$cshow :: VarInfo -> String
showsPrec :: Int -> VarInfo -> ShowS
$cshowsPrec :: Int -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
    case [Name]
startNames of
      [] -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        Ctxt CGInfo
cg  <- IState -> Ctxt CGInfo
idris_callgraph forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        Ctxt OptInfo
opt <- IState -> Ctxt OptInfo
idris_optimisation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        [Reason]
used <- IState -> [Reason]
idris_erasureUsed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        Set Reason
externs <- IState -> Set Reason
idris_externs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState

        -- Build the dependency graph.
        let depMap :: Deps
depMap = Ctxt InterfaceInfo
-> [Reason] -> [Reason] -> Context -> [Name] -> Deps
buildDepMap Ctxt InterfaceInfo
ci [Reason]
used (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 = forall k a. Map k a -> [(k, a)]
M.toList UseMap
minUse

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

        -- Check that everything reachable is accessible.
        Bool
checkEnabled <- (Opt
WarnReach forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkEnabled forall a b. (a -> b) -> a -> b
$
            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 <- forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set Name
reachableNames 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. Set a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ Set Name
reachablePostulates)
            forall a b. (a -> b) -> a -> b
$ forall a. String -> Idris a
ifail (String
"reachable postulates:\n" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n | Name
n <- forall a. Set a -> [a]
S.toList Set Name
reachablePostulates])

        -- Store the usage info in the internal state.
        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

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

    fmtItem :: (Cond, DepSet) -> String
    fmtItem :: (Cond, DepSet) -> String
fmtItem (Cond
cond, DepSet
deps) = ShowS
indent forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall a. Set a -> [a]
S.toList Cond
cond) forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,IntMap (Set Reason)
is) -> ShowS
indent forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" -> " 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 = forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (Show a, Show a) => (a, Set a) -> String
fmtArg forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. IntMap a -> [(Int, a)]
IM.toList
      where
        fmtArg :: (a, Set a) -> String
fmtArg (a
i, Set a
rs)
            | forall a. Set a -> Bool
S.null Set a
rs = forall a. Show a => a -> String
show a
i
            | Bool
otherwise = forall a. Show a => a -> String
show a
i forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ 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) = forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field CGInfo [(Int, [Reason])]
cg_usedpos 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, forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Set Reason
rs) <- 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) <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n Ctxt OptInfo
opt
        , eargs :: [String]
eargs@(String
_:[String]
_) <- [forall {a} {a} {a}.
(Show a, Show a, Show a) =>
a -> [(a, a)] -> String
fmt Name
n (forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Name
n) <- [(Int, Name)]
inaccessible, Set Reason
rs <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Set Reason)
reachable]
        = String -> Idris ()
warn forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
": inaccessible arguments reachable:\n  " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " [String]
eargs

        | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      where
        fmt :: a -> [(a, a)] -> String
fmt a
n [] = forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" (no more information available)"
        fmt a
n [(a, a)]
rs = forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [forall a. Show a => a -> String
show a
rn forall a. [a] -> [a] -> [a]
++ String
" arg# " forall a. [a] -> [a] -> [a]
++ 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 forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** DepSet -> (Set Name, UseMap)
gather
    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 = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith forall a. Ord a => Set a -> Set a -> Set a
S.union [DepSet
ds | (Cond
cond, DepSet
ds) <- forall a. IntMap a -> [a]
IM.elems IntMap (Cond, DepSet)
numbered, forall a. Set a -> Bool
S.null Cond
cond]

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

    fromNumbered :: IntMap Constraint -> Deps
    fromNumbered :: IntMap (Cond, DepSet) -> Deps
fromNumbered = forall a b. (a -> b -> b) -> b -> IntMap a -> b
IM.foldr 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 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) = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith 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 = 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 -> 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' -> 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 (forall a. Set a -> [a]
S.toList Cond
ns)
        ) 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins (forall a. Set a
S.empty, forall k a. Map k a
M.empty) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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) = (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, forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith (forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union) Name
n (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
    | 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
        (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith 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 = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions [
        forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault IntSet
IS.empty Node
n Map Node IntSet
index
        | Node
n <- 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')
        = forall b. (Int -> b -> b) -> b -> IntSet -> b
IS.foldr
            (Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
reduceConstraint forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
M.keysSet DepSet
previouslyNew)
            (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) <- forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Cond, DepSet)
constrs
        = case 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.
                | forall a. Set a -> Bool
S.null Cond
cond'
                -> (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union DepSet
news DepSet
deps, 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.
                | forall a. Set a -> Int
S.size Cond
cond' forall a. Ord a => a -> a -> Bool
< forall a. Set a -> Int
S.size Cond
cond
                -> (DepSet
news, 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 forall a b. (a -> b) -> a -> b
$ Set Name -> Deps -> [Name] -> Deps
dfs forall a. Set a
S.empty 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Cond
ds, DepSet
rs) -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
ds DepSet
rs) Deps
deps (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 = (forall a. Ord a => [a] -> Set a
S.fromList [a]
ds, forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(k
r, 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 = 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 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 forall a. Ord a => a -> Set a -> Bool
`S.member` Set Name
usedNames]

        postulates :: [Reason] -> [(Set a, Map Node (Set a))]
postulates [Reason]
used =
            [ [] forall {a} {k} {a}.
(Ord a, Ord k) =>
[a] -> [k] -> (Set a, Map k (Set a))
==> 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.
                [(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
                , 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
arityforall 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
arityforall 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 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 (forall a. Ord a => a -> Set a -> Set a
S.insert Name
n Set Name
visited) (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union) Deps
deps' Deps
deps) ([Name]
next forall a. [a] -> [a] -> [a]
++ [Name]
ns)
      where
        next :: [Name]
next = [Name
n | Name
n <- forall a. Set a -> [a]
S.toList Set Name
depn, Name
n forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Name
visited]
        depn :: Set Name
depn = forall a. Ord a => a -> Set a -> Set a
S.delete Name
n 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 = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {b} {a}.
Ord a =>
(Set (a, b), Map (a, b) a) -> Set a
names forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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) = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> a
fst Set (a, b)
cs forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> a
fst (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)))
        = 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  -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"erasure checker: unknown reference: " forall a. [a] -> [a] -> [a]
++ 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) = forall a. HasCallStack => String -> a
error String
"a function encountered"  -- TODO
    getDepsDef Name
fn (TyDecl   NameType
ty TT Name
t) = forall k a. Map k a
M.empty
    getDepsDef Name
fn (Operator TT Name
ty Int
n' [Value] -> Maybe Value
f) = 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 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 = [forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
vars .. forall (t :: * -> *) a. Foldable t => t a -> Int
length [(TT Name, Bool)]
tys forall a. Num a => a -> a -> a
- Int
1]
        etaVars :: [Name]
etaVars = [Int -> Name
eta Int
i | Int
i <- [Int]
etaIdx]
        etaMap :: Vars
etaMap = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [forall {a}. a -> Int -> (a, VarInfo)
varPair Name
v Int
i | (Name
v,Int
i) <- 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   = forall k a. k -> a -> Map k a
M.singleton (Name
fn, Int -> Arg
Arg Int
argNo) forall a. Set a
S.empty
            , viFunArg :: Maybe Int
viFunArg = forall a. a -> Maybe a
Just Int
argNo
            , viMethod :: Maybe Name
viMethod = 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 (forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete TT Name
t (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n 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     = forall k a. Map k a
M.empty
    getDepsSC Name
fn [Name]
es Vars
vs (UnmatchedCase String
msg) = 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 (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 (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)   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"ProjCase not supported:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 [] (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 forall a b. (a -> b) -> a -> b
$ 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)
_] -> forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id  -- single branch, tag not used
            [CaseAlt' (TT Name)]
_   -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union) (forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) (VarInfo -> DepSet
viDeps VarInfo
casedVar)
        casedVar :: VarInfo
casedVar  = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"nonpatvar in case: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n) (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) = 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 (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' 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' = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
            { viDeps :: DepSet
viDeps   = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith forall a. Ord a => Set a -> Set a -> Set a
S.union (Name
n, Int -> Arg
Arg Int
j) (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) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Int
0..]]

        -- this is safe because it's certainly a patvar
        varIdx :: Int
varIdx = 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 -> forall a. a -> Maybe a
Just (Name -> Int -> Name
mkFieldName Name
n Int
j)
             | Bool
otherwise = \Int
j -> 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 <- 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 <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
        = 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
        = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"erasure analysis: variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" unbound in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> [a]
S.toList Cond
cd)

        -- assumed to be a global reference
        | Bool
otherwise = forall k a. k -> a -> Map k a
M.singleton Cond
cd (forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) 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) = forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs forall a. [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, forall a b. a -> b -> a
const forall k a. Map k a
M.empty) 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, forall a b. a -> b -> a
const forall k a. Map k a
M.empty) 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, forall a b. a -> b -> a
const forall k a. Map k a
M.empty) 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, forall a b. a -> b -> a
const forall k a. Map k a
M.empty) 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) <- 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` forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Int, TT Name) -> Deps
methodDeps Name
ctorName) (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 forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"mkForeignPrim"
                -> [TT Name] -> Deps
unconditionalDeps forall a b. (a -> b) -> a -> b
$ 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 <- 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  <- 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 <- 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 -> forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs forall a. [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 (forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (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 (forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
t) TT Name
t')

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

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

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

        unconditionalDeps :: [Term] -> Deps
        unconditionalDeps :: [TT Name] -> Deps
unconditionalDeps = 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 (forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) forall a. Set a
S.empty) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Maybe Int, TT Name) -> Deps
getDepsArgs Name
n) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Int]
indices
          where
            indices :: [Maybe Int]
indices = forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Maybe a
Just [Int
0 .. Name -> Int
getArity Name
n forall a. Num a => a -> a -> a
- Int
1] forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat 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 (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 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) (forall {k} {a}. [(Name, k -> Map k (Map Node (Set a)))]
bruijns forall a. [a] -> [a] -> [a]
++ [(Name, Cond -> Deps)]
bs) Cond
cond TT Name
body
          where
            vars :: Vars
vars = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
                { viDeps :: DepSet
viDeps   = forall {a}. Int -> Map Node (Set a)
deps Int
i
                , viFunArg :: Maybe Int
viFunArg = forall a. a -> Maybe a
Just Int
i
                , viMethod :: Maybe Name
viMethod = forall a. Maybe a
Nothing
                }) | (Name
v, Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [Int
0..]]
            deps :: Int -> Map Node (Set a)
deps Int
i   = forall k a. k -> a -> Map k a
M.singleton (Name
metameth, Int -> Arg
Arg Int
i) forall a. Set a
S.empty
            bruijns :: [(Name, k -> Map k (Map Node (Set a)))]
bruijns  = forall a. [a] -> [a]
reverse [(Name
n, \k
cd -> forall k a. k -> a -> Map k a
M.singleton k
cd (forall {a}. Int -> Map Node (Set a)
deps Int
i)) | (Int
i, Name
n) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
args]
            cond :: Cond
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) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"cannot[1] analyse projection !" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" of " forall a. [a] -> [a] -> [a]
++ 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
_) = forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (TType    UExp
_) = forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (UType    Universe
_) = forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd  TT Name
Erased      = forall k a. Map k a
M.empty
    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd  TT Name
Impossible  = forall k a. Map k a
M.empty

    getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"cannot get deps of: " forall a. [a] -> [a] -> [a]
++ 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ty
            in if Int
i forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT Name]
argTys
                then forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall n. TT n -> [(n, TT n)]
getArgTys ([TT Name]
argTys forall a. [a] -> Int -> a
!! Int
i)
                else forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"invalid field number " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
ctorName

        | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"unknown implementation constructor: " forall a. [a] -> [a] -> [a]
++ 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) -> 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)                -> forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ 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 -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: unrecognised entity '"
                             forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"' with definition: "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Def
df
        Maybe Def
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: definition not found for " forall a. [a] -> [a] -> [a]
++ 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) = 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) = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig TT Name
ty (forall n. Int -> TT n -> TT n
weakenTm Int
wk TT Name
v)) forall a b. (a -> b) -> a -> b
$ Int -> [TT Name] -> TT Name -> TT Name
lamToLet' (Int
wkforall a. Num a => a -> a -> a
+Int
1) [TT Name]
vs TT Name
tm
    lamToLet' Int
wk    [TT Name]
vs  TT Name
tm = forall n. TT n -> [TT n] -> TT n
mkApp TT Name
tm forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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
nforall 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 = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith 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 = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Ord a => Set a -> Set a -> Set a
S.union) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
fieldNo String
"field")