{-# 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
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)
type DepSet = Map Node (Set Reason)
type Cond = Set Node
data VarInfo = VI
{ VarInfo -> DepSet
viDeps :: DepSet
, VarInfo -> Maybe Int
viFunArg :: Maybe Int
, VarInfo -> Maybe Name
viMethod :: Maybe Name
}
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
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 []
[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
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
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
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)
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
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])
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)
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
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
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 (
\Int
i (Cond
ns, DepSet
_ds) Map Node IntSet
ix -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (
\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
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)
forwardChain
:: Map Node IntSet
-> DepSet
-> DepSet
-> IntMap Constraint
-> (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
| forall k a. Map k a -> Bool
M.null DepSet
currentlyNew
= (IntMap (Cond, DepSet)
constrs, DepSet
solution)
| 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
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
]
(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
reduceConstraint
:: Set Node
-> Int
-> (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'
| 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)
| 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)
| Bool
otherwise
-> (DepSet
news, IntMap (Cond, DepSet)
constrs)
| Bool
otherwise = (DepSet
news, IntMap (Cond, DepSet)
constrs)
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
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
==> :: [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]
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
[(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)]
, forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Int
i) -> (Name
n, Int -> Arg
Arg Int
i)) [Reason]
used
, String -> [Int] -> [Node]
it String
"MkIO" [Int
2]
, String -> [Int] -> [Node]
it String
"prim__IO" [Int
1]
, [(Name
pairCon, Int -> Arg
Arg Int
2),
(Name
pairCon, Int -> Arg
Arg Int
3)]
, String -> [Int] -> [Node]
it String
"prim_fork" [Int
0]
, String -> [Int] -> [Node]
it String
"unsafePerformPrimIO" [Int
1]
, String -> [Int] -> [Node]
it String
"prim__believe_me" [Int
2]
, [(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]]
, [(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]]
]
]
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
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)
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
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"
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
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
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")
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
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
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)
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)
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)
= 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
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
[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
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
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
where
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..]]
varIdx :: Int
varIdx = forall a. HasCallStack => Maybe a -> a
fromJust (VarInfo -> Maybe Int
viFunArg VarInfo
var)
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
getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps
getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (P NameType
_ Name
n TT 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
| 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)
| 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)
| 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)
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)
| 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 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
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
P (DCon Int
_ Int
_ Bool
_) ctorName :: Name
ctorName@(SN (ImplementationCtorN Name
interfaceName)) TT Name
_
-> Name -> [TT Name] -> Deps
conditionalDeps Name
ctorName [TT Name]
args
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)
P (TCon Int
_ Int
_) Name
n TT Name
_ -> [TT Name] -> Deps
unconditionalDeps [TT Name]
args
P (DCon Int
_ Int
_ Bool
_) Name
n TT Name
_ -> Name -> [TT Name] -> Deps
conditionalDeps Name
n [TT Name]
args
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
P NameType
_ Name
n TT 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
| 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
| Just VarInfo
var <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
-> VarInfo -> DepSet
viDeps VarInfo
var DepSet -> Deps -> Deps
`ins` [TT Name] -> Deps
unconditionalDeps [TT Name]
args
| Bool
otherwise
-> Name -> [TT Name] -> Deps
conditionalDeps Name
n [TT Name]
args
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
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)
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
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
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
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
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
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
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
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
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
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
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")