{-# LANGUAGE PatternGuards #-}
module Idris.Erasure (performUsageAnalysis, mkFieldName) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Error
import Idris.Options
import Idris.Primitives
import Prelude hiding (id, (.))
import Control.Arrow
import Control.Category
import Control.Monad
import Control.Monad.State
import Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS
import Data.List
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as S
import Data.Text (pack)
import qualified Data.Text as T
type UseMap = Map Name (IntMap (Set Reason))
data Arg = Arg Int | Result deriving (Arg -> Arg -> Bool
(Arg -> Arg -> Bool) -> (Arg -> Arg -> Bool) -> Eq Arg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Arg -> Arg -> Bool
== :: Arg -> Arg -> Bool
$c/= :: Arg -> Arg -> Bool
/= :: Arg -> Arg -> Bool
Eq, Eq Arg
Eq Arg =>
(Arg -> Arg -> Ordering)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Arg)
-> (Arg -> Arg -> Arg)
-> Ord Arg
Arg -> Arg -> Bool
Arg -> Arg -> Ordering
Arg -> Arg -> Arg
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Arg -> Arg -> Ordering
compare :: Arg -> Arg -> Ordering
$c< :: Arg -> Arg -> Bool
< :: Arg -> Arg -> Bool
$c<= :: Arg -> Arg -> Bool
<= :: Arg -> Arg -> Bool
$c> :: Arg -> Arg -> Bool
> :: Arg -> Arg -> Bool
$c>= :: Arg -> Arg -> Bool
>= :: Arg -> Arg -> Bool
$cmax :: Arg -> Arg -> Arg
max :: Arg -> Arg -> Arg
$cmin :: Arg -> Arg -> Arg
min :: Arg -> Arg -> Arg
Ord)
instance Show Arg where
show :: Arg -> String
show (Arg Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i
show Arg
Result = String
"*"
type Node = (Name, Arg)
type Deps = Map Cond DepSet
type Reason = (Name, Int)
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
(Int -> VarInfo -> ShowS)
-> (VarInfo -> String) -> ([VarInfo] -> ShowS) -> Show VarInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VarInfo -> ShowS
showsPrec :: Int -> VarInfo -> ShowS
$cshow :: VarInfo -> String
show :: VarInfo -> String
$cshowList :: [VarInfo] -> ShowS
showList :: [VarInfo] -> ShowS
Show
type Vars = Map Name VarInfo
performUsageAnalysis :: [Name] -> Idris [Name]
performUsageAnalysis :: [Name] -> Idris [Name]
performUsageAnalysis [Name]
startNames = do
Context
ctx <- IState -> Context
tt_ctxt (IState -> Context)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
case [Name]
startNames of
[] -> [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
[Name]
main -> do
Ctxt InterfaceInfo
ci <- IState -> Ctxt InterfaceInfo
idris_interfaces (IState -> Ctxt InterfaceInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt InterfaceInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Ctxt CGInfo
cg <- IState -> Ctxt CGInfo
idris_callgraph (IState -> Ctxt CGInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt CGInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Ctxt OptInfo
opt <- IState -> Ctxt OptInfo
idris_optimisation (IState -> Ctxt OptInfo)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Ctxt OptInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
[Reason]
used <- IState -> [Reason]
idris_erasureUsed (IState -> [Reason])
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) [Reason]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Set Reason
externs <- IState -> Set Reason
idris_externs (IState -> Set Reason)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Set Reason)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
let depMap :: Deps
depMap = Ctxt InterfaceInfo
-> [Reason] -> [Reason] -> Context -> [Name] -> Deps
buildDepMap Ctxt InterfaceInfo
ci [Reason]
used (Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
externs) Context
ctx [Name]
main
let (Deps
residDeps, (Set Name
reachableNames, UseMap
minUse)) = Deps -> (Deps, (Set Name, UseMap))
minimalUsage Deps
depMap
usage :: [(Name, IntMap (Set Reason))]
usage = UseMap -> [(Name, IntMap (Set Reason))]
forall k a. Map k a -> [(k, a)]
M.toList UseMap
minUse
Int -> String -> Idris ()
logErasure Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Original deps:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (((Cond, DepSet) -> String) -> [(Cond, DepSet)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> String
fmtItem ([(Cond, DepSet)] -> [String])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList (Deps -> [String]) -> Deps -> [String]
forall a b. (a -> b) -> a -> b
$ Deps
depMap)
Int -> String -> Idris ()
logErasure Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Reachable names:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
indent ShowS -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> String
forall a. Show a => a -> String
show) ([Name] -> [String])
-> (Set Name -> [Name]) -> Set Name -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [String]) -> Set Name -> [String]
forall a b. (a -> b) -> a -> b
$ Set Name
reachableNames)
Int -> String -> Idris ()
logErasure Int
4 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Minimal usage:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, IntMap (Set Reason))] -> String
fmtUseMap [(Name, IntMap (Set Reason))]
usage
Int -> String -> Idris ()
logErasure Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Residual deps:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (((Cond, DepSet) -> String) -> [(Cond, DepSet)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> String
fmtItem ([(Cond, DepSet)] -> [String])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList (Deps -> [String]) -> Deps -> [String]
forall a b. (a -> b) -> a -> b
$ Deps
residDeps)
Bool
checkEnabled <- (Opt
WarnReach Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Opt] -> Bool) -> (IState -> [Opt]) -> IState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IOption -> [Opt]
opt_cmdline (IOption -> [Opt]) -> (IState -> IOption) -> IState -> [Opt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> IOption
idris_options (IState -> Bool)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkEnabled (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
((Name, IntMap (Set Reason)) -> Idris ())
-> [(Name, IntMap (Set Reason))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility Ctxt OptInfo
opt) [(Name, IntMap (Set Reason))]
usage
Set Name
reachablePostulates <- Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set Name
reachableNames (Set Name -> Set Name)
-> (IState -> Set Name) -> IState -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Set Name
idris_postulates (IState -> Set Name)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Set Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> (Set Name -> Bool) -> Set Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Set Name -> Bool
forall a. Set a -> Bool
S.null (Set Name -> Bool) -> Set Name -> Bool
forall a b. (a -> b) -> a -> b
$ Set Name
reachablePostulates)
(Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
forall a. String -> Idris a
ifail (String
"reachable postulates:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n | Name
n <- Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
reachablePostulates])
((Name, IntMap (Set Reason)) -> Idris ())
-> [(Name, IntMap (Set Reason))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, IntMap (Set Reason)) -> Idris ()
storeUsage [(Name, IntMap (Set Reason))]
usage
[Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Idris [Name]) -> [Name] -> Idris [Name]
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
reachableNames
where
indent :: ShowS
indent = (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++)
fmtItem :: (Cond, DepSet) -> String
fmtItem :: (Cond, DepSet) -> String
fmtItem (Cond
cond, DepSet
deps) = ShowS
indent ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Node] -> String
forall a. Show a => a -> String
show (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
cond) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Node, Set Reason)] -> String
forall a. Show a => a -> String
show (DepSet -> [(Node, Set Reason)]
forall k a. Map k a -> [(k, a)]
M.toList DepSet
deps)
fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
fmtUseMap = [String] -> String
unlines ([String] -> String)
-> ([(Name, IntMap (Set Reason))] -> [String])
-> [(Name, IntMap (Set Reason))]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, IntMap (Set Reason)) -> String)
-> [(Name, IntMap (Set Reason))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,IntMap (Set Reason)
is) -> ShowS
indent ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IntMap (Set Reason) -> String
fmtIxs IntMap (Set Reason)
is)
fmtIxs :: IntMap (Set Reason) -> String
fmtIxs :: IntMap (Set Reason) -> String
fmtIxs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String)
-> (IntMap (Set Reason) -> [String])
-> IntMap (Set Reason)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Int, Set Reason) -> String) -> [(Int, Set Reason)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Set Reason) -> String
forall {a} {a}. (Show a, Show a) => (a, Set a) -> String
fmtArg ([(Int, Set Reason)] -> [String])
-> (IntMap (Set Reason) -> [(Int, Set Reason)])
-> IntMap (Set Reason)
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IntMap (Set Reason) -> [(Int, Set Reason)]
forall a. IntMap a -> [(Int, a)]
IM.toList
where
fmtArg :: (a, Set a) -> String
fmtArg (a
i, Set a
rs)
| Set a -> Bool
forall a. Set a -> Bool
S.null Set a
rs = a -> String
forall a. Show a => a -> String
show a
i
| Bool
otherwise = a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show ([a] -> [String]) -> [a] -> [String]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
rs)
storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
storeUsage (Name
n, IntMap (Set Reason)
args) = Field IState [(Int, [Reason])] -> [(Int, [Reason])] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field CGInfo [(Int, [Reason])]
cg_usedpos Field CGInfo [(Int, [Reason])]
-> Field IState CGInfo -> Field IState [(Int, [Reason])]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n) [(Int, [Reason])]
flat
where
flat :: [(Int, [Reason])]
flat = [(Int
i, Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Set Reason
rs) <- IntMap (Set Reason) -> [(Int, Set Reason)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap (Set Reason)
args]
checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility Ctxt OptInfo
opt (Name
n, IntMap (Set Reason)
reachable)
| Just (Optimise [(Int, Name)]
inaccessible Bool
dt [Int]
force) <- Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n Ctxt OptInfo
opt
, eargs :: [String]
eargs@(String
_:[String]
_) <- [Name -> [Reason] -> String
forall {a} {a} {a}.
(Show a, Show a, Show a) =>
a -> [(a, a)] -> String
fmt Name
n (Set Reason -> [Reason]
forall a. Set a -> [a]
S.toList Set Reason
rs) | (Int
i,Name
n) <- [(Int, Name)]
inaccessible, Set Reason
rs <- Maybe (Set Reason) -> [Set Reason]
forall a. Maybe a -> [a]
maybeToList (Maybe (Set Reason) -> [Set Reason])
-> Maybe (Set Reason) -> [Set Reason]
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Set Reason) -> Maybe (Set Reason)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Set Reason)
reachable]
= String -> Idris ()
warn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": inaccessible arguments reachable:\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n " [String]
eargs
| Bool
otherwise = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
fmt :: a -> [(a, a)] -> String
fmt a
n [] = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (no more information available)"
fmt a
n [(a, a)]
rs = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [a -> String
forall a. Show a => a -> String
show a
rn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arg# " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ri | (a
rn,a
ri) <- [(a, a)]
rs]
warn :: String -> Idris ()
warn = Int -> String -> Idris ()
logErasure Int
0
type Constraint = (Cond, DepSet)
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage Deps
deps
= IntMap (Cond, DepSet) -> Deps
fromNumbered (IntMap (Cond, DepSet) -> Deps)
-> (DepSet -> (Set Name, UseMap))
-> (IntMap (Cond, DepSet), DepSet)
-> (Deps, (Set Name, UseMap))
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** DepSet -> (Set Name, UseMap)
gather
((IntMap (Cond, DepSet), DepSet) -> (Deps, (Set Name, UseMap)))
-> (IntMap (Cond, DepSet), DepSet) -> (Deps, (Set Name, UseMap))
forall a b. (a -> b) -> a -> b
$ Map Node IntSet
-> DepSet
-> DepSet
-> IntMap (Cond, DepSet)
-> (IntMap (Cond, DepSet), DepSet)
forwardChain (IntMap (Cond, DepSet) -> Map Node IntSet
index IntMap (Cond, DepSet)
numbered) DepSet
seedDeps DepSet
seedDeps IntMap (Cond, DepSet)
numbered
where
numbered :: IntMap (Cond, DepSet)
numbered = Deps -> IntMap (Cond, DepSet)
toNumbered Deps
deps
seedDeps :: DepSet
seedDeps :: DepSet
seedDeps = (Set Reason -> Set Reason -> Set Reason) -> [DepSet] -> DepSet
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union [DepSet
ds | (Cond
cond, DepSet
ds) <- IntMap (Cond, DepSet) -> [(Cond, DepSet)]
forall a. IntMap a -> [a]
IM.elems IntMap (Cond, DepSet)
numbered, Cond -> Bool
forall a. Set a -> Bool
S.null Cond
cond]
toNumbered :: Deps -> IntMap Constraint
toNumbered :: Deps -> IntMap (Cond, DepSet)
toNumbered = [(Int, (Cond, DepSet))] -> IntMap (Cond, DepSet)
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, (Cond, DepSet))] -> IntMap (Cond, DepSet))
-> (Deps -> [(Int, (Cond, DepSet))])
-> Deps
-> IntMap (Cond, DepSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Int] -> [(Cond, DepSet)] -> [(Int, (Cond, DepSet))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([(Cond, DepSet)] -> [(Int, (Cond, DepSet))])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [(Int, (Cond, DepSet))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList
fromNumbered :: IntMap Constraint -> Deps
fromNumbered :: IntMap (Cond, DepSet) -> Deps
fromNumbered = ((Cond, DepSet) -> Deps -> Deps)
-> Deps -> IntMap (Cond, DepSet) -> Deps
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IM.foldr (Cond, DepSet) -> Deps -> Deps
forall {k} {k} {a}.
(Ord k, Ord k, Ord a) =>
(k, Map k (Set a))
-> Map k (Map k (Set a)) -> Map k (Map k (Set a))
addConstraint Deps
forall k a. Map k a
M.empty
where
addConstraint :: (k, Map k (Set a))
-> Map k (Map k (Set a)) -> Map k (Map k (Set a))
addConstraint (k
ns, Map k (Set a)
vs) = (Map k (Set a) -> Map k (Set a) -> Map k (Set a))
-> k
-> Map k (Set a)
-> Map k (Map k (Set a))
-> Map k (Map k (Set a))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set a -> Set a -> Set a)
-> Map k (Set a) -> Map k (Set a) -> Map k (Set a)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.union) k
ns Map k (Set a)
vs
index :: IntMap Constraint -> Map Node IntSet
index :: IntMap (Cond, DepSet) -> Map Node IntSet
index = (Int -> (Cond, DepSet) -> Map Node IntSet -> Map Node IntSet)
-> Map Node IntSet -> IntMap (Cond, DepSet) -> Map Node IntSet
forall a b. (Int -> a -> b -> b) -> b -> IntMap a -> b
IM.foldrWithKey (
\Int
i (Cond
ns, DepSet
_ds) Map Node IntSet
ix -> (Node -> Map Node IntSet -> Map Node IntSet)
-> Map Node IntSet -> [Node] -> Map Node IntSet
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (
\Node
n Map Node IntSet
ix' -> (IntSet -> IntSet -> IntSet)
-> Node -> IntSet -> Map Node IntSet -> Map Node IntSet
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith IntSet -> IntSet -> IntSet
IS.union Node
n (Int -> IntSet
IS.singleton Int
i) Map Node IntSet
ix'
) Map Node IntSet
ix (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
ns)
) Map Node IntSet
forall k a. Map k a
M.empty
gather :: DepSet -> (Set Name, UseMap)
gather :: DepSet -> (Set Name, UseMap)
gather = ((Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap))
-> (Set Name, UseMap) -> [(Node, Set Reason)] -> (Set Name, UseMap)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins (Set Name
forall a. Set a
S.empty, UseMap
forall k a. Map k a
M.empty) ([(Node, Set Reason)] -> (Set Name, UseMap))
-> (DepSet -> [(Node, Set Reason)]) -> DepSet -> (Set Name, UseMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. DepSet -> [(Node, Set Reason)]
forall k a. Map k a -> [(k, a)]
M.toList
where
ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins ((Name
n, Arg
Result), Set Reason
rs) (Set Name
ns, UseMap
umap) = (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
n Set Name
ns, UseMap
umap)
ins ((Name
n, Arg Int
i ), Set Reason
rs) (Set Name
ns, UseMap
umap) = (Set Name
ns, (IntMap (Set Reason) -> IntMap (Set Reason) -> IntMap (Set Reason))
-> Name -> IntMap (Set Reason) -> UseMap -> UseMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> IntMap (Set Reason)
-> IntMap (Set Reason)
-> IntMap (Set Reason)
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Name
n (Int -> Set Reason -> IntMap (Set Reason)
forall a. Int -> a -> IntMap a
IM.singleton Int
i Set Reason
rs) UseMap
umap)
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
| DepSet -> Bool
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
((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union DepSet
solution DepSet
currentlyNew)
DepSet
currentlyNew
IntMap (Cond, DepSet)
constrs'
where
affectedIxs :: IntSet
affectedIxs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions [
IntSet -> Node -> Map Node IntSet -> IntSet
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault IntSet
IS.empty Node
n Map Node IntSet
index
| Node
n <- DepSet -> [Node]
forall k a. Map k a -> [k]
M.keys DepSet
previouslyNew
]
(DepSet
currentlyNew, IntMap (Cond, DepSet)
constrs')
= (Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet)))
-> (DepSet, IntMap (Cond, DepSet))
-> IntSet
-> (DepSet, IntMap (Cond, DepSet))
forall b. (Int -> b -> b) -> b -> IntSet -> b
IS.foldr
(Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
reduceConstraint (Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet)))
-> Cond
-> Int
-> (DepSet, IntMap (Cond, DepSet))
-> (DepSet, IntMap (Cond, DepSet))
forall a b. (a -> b) -> a -> b
$ DepSet -> Cond
forall k a. Map k a -> Set k
M.keysSet DepSet
previouslyNew)
(DepSet
forall k a. Map k a
M.empty, IntMap (Cond, DepSet)
constrs)
IntSet
affectedIxs
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) <- Int -> IntMap (Cond, DepSet) -> Maybe (Cond, DepSet)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Cond, DepSet)
constrs
= case Cond
cond Cond -> Cond -> Cond
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Cond
previouslyNew of
Cond
cond'
| Cond -> Bool
forall a. Set a -> Bool
S.null Cond
cond'
-> ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union DepSet
news DepSet
deps, Int -> IntMap (Cond, DepSet) -> IntMap (Cond, DepSet)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap (Cond, DepSet)
constrs)
| Cond -> Int
forall a. Set a -> Int
S.size Cond
cond' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Cond -> Int
forall a. Set a -> Int
S.size Cond
cond
-> (DepSet
news, Int
-> (Cond, DepSet) -> IntMap (Cond, DepSet) -> IntMap (Cond, DepSet)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (Cond
cond', DepSet
deps) IntMap (Cond, DepSet)
constrs)
| 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 (Deps -> Deps) -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ Set Name -> Deps -> [Name] -> Deps
dfs Set Name
forall a. Set a
S.empty Deps
forall k a. Map k a
M.empty [Name]
startNames
where
addPostulates :: [(Name, Int)] -> Deps -> Deps
addPostulates :: [Reason] -> Deps -> Deps
addPostulates [Reason]
used Deps
deps = ((Cond, DepSet) -> Deps -> Deps)
-> Deps -> [(Cond, DepSet)] -> Deps
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Cond
ds, DepSet
rs) -> (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
ds DepSet
rs) Deps
deps ([Reason] -> [(Cond, DepSet)]
forall {a} {a}. Ord a => [Reason] -> [(Set a, Map Node (Set a))]
postulates [Reason]
used)
where
==> :: [a] -> [k] -> (Set a, Map k (Set a))
(==>) [a]
ds [k]
rs = ([a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList [a]
ds, [(k, Set a)] -> Map k (Set a)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(k
r, Set a
forall a. Set a
S.empty) | k
r <- [k]
rs])
it :: String -> [Int] -> [Node]
it String
n [Int]
is = [(String -> Name
sUN String
n, Int -> Arg
Arg Int
i) | Int
i <- [Int]
is]
specialPrims :: Set Name
specialPrims = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList [String -> Name
sUN String
"prim__believe_me"]
usedNames :: Set Name
usedNames = Deps -> Set Name
allNames Deps
deps Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set Name
specialPrims
usedPrims :: [Reason]
usedPrims = [(Prim -> Name
p_name Prim
p, Prim -> Int
p_arity Prim
p) | Prim
p <- [Prim]
primitives, Prim -> Name
p_name Prim
p Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Name
usedNames]
postulates :: [Reason] -> [(Set a, Map Node (Set a))]
postulates [Reason]
used =
[ [] [a] -> [Node] -> (Set a, Map Node (Set a))
forall {a} {k} {a}.
(Ord a, Ord k) =>
[a] -> [k] -> (Set a, Map k (Set a))
==> [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[((Name -> Node) -> [Name] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Arg
Result)) [Name]
startNames)
,[(String -> Name
sUN String
"run__IO", Arg
Result), (String -> Name
sUN String
"run__IO", Int -> Arg
Arg Int
1)]
,[(String -> Name
sUN String
"call__IO", Arg
Result), (String -> Name
sUN String
"call__IO", Int -> Arg
Arg Int
2)]
, (Reason -> Node) -> [Reason] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Int
i) -> (Name
n, Int -> Arg
Arg Int
i)) [Reason]
used
, 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
arityInt -> Int -> Int
forall 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
arityInt -> Int -> Int
forall 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 Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Name
visited = Set Name -> Deps -> [Name] -> Deps
dfs Set Name
visited Deps
deps [Name]
ns
| Bool
otherwise = Set Name -> Deps -> [Name] -> Deps
dfs (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
n Set Name
visited) ((DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Deps
deps' Deps
deps) ([Name]
next [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
ns)
where
next :: [Name]
next = [Name
n | Name
n <- Set Name -> [Name]
forall a. Set a -> [a]
S.toList Set Name
depn, Name
n Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Name
visited]
depn :: Set Name
depn = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.delete Name
n (Set Name -> Set Name) -> Set Name -> Set Name
forall a b. (a -> b) -> a -> b
$ Deps -> Set Name
allNames Deps
deps'
deps' :: Deps
deps' = Name -> Deps
getDeps Name
n
allNames :: Deps -> Set Name
allNames :: Deps -> Set Name
allNames = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Name] -> Set Name)
-> (Deps -> [Set Name]) -> Deps -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Cond, DepSet) -> Set Name) -> [(Cond, DepSet)] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map (Cond, DepSet) -> Set Name
forall {a} {b} {b} {a}.
Ord a =>
(Set (a, b), Map (a, b) a) -> Set a
names ([(Cond, DepSet)] -> [Set Name])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [Set Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Deps -> [(Cond, DepSet)]
forall k a. Map k a -> [(k, a)]
M.toList
where
names :: (Set (a, b), Map (a, b) a) -> Set a
names (Set (a, b)
cs, Map (a, b) a
ns) = ((a, b) -> a) -> Set (a, b) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, b) -> a
forall a b. (a, b) -> a
fst Set (a, b)
cs Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` ((a, b) -> a) -> Set (a, b) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, b) -> a
forall a b. (a, b) -> a
fst (Map (a, b) a -> Set (a, b)
forall k a. Map k a -> Set k
M.keysSet Map (a, b) a
ns)
getDeps :: Name -> Deps
getDeps :: Name -> Deps
getDeps (SN (WhereN Int
i (SN (ImplementationCtorN Name
interfaceN)) (MN Int
i' Text
field)))
= Deps
forall k a. Map k a
M.empty
getDeps Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
Just Def
def -> Name -> Def -> Deps
getDepsDef Name
n Def
def
Maybe Def
Nothing -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"erasure checker: unknown reference: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
getDepsDef :: Name -> Def -> Deps
getDepsDef :: Name -> Def -> Deps
getDepsDef Name
fn (Function TT Name
ty TT Name
t) = String -> Deps
forall a. HasCallStack => String -> a
error String
"a function encountered"
getDepsDef Name
fn (TyDecl NameType
ty TT Name
t) = Deps
forall k a. Map k a
M.empty
getDepsDef Name
fn (Operator TT Name
ty Int
n' [Value] -> Maybe Value
f) = Deps
forall k a. Map k a
M.empty
getDepsDef Name
fn (CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
tys [Either (TT Name) (TT Name, TT Name)]
def [([Name], TT Name, TT Name)]
tot CaseDefs
cdefs)
= Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
etaVars (Vars
etaMap Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
varMap) SC' (TT Name)
sc
where
etaIdx :: [Int]
etaIdx = [[Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
vars .. [(TT Name, Bool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(TT Name, Bool)]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
etaVars :: [Name]
etaVars = [Int -> Name
eta Int
i | Int
i <- [Int]
etaIdx]
etaMap :: Vars
etaMap = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [Name -> Int -> (Name, VarInfo)
forall {a}. a -> Int -> (a, VarInfo)
varPair (Int -> Name
eta Int
i) Int
i | Int
i <- [Int]
etaIdx]
eta :: Int -> Name
eta Int
i = Int -> Text -> Name
MN Int
i (String -> Text
pack String
"eta")
varMap :: Vars
varMap = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [Name -> Int -> (Name, VarInfo)
forall {a}. a -> Int -> (a, VarInfo)
varPair Name
v Int
i | (Name
v,Int
i) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars [Int
0..]]
varPair :: a -> Int -> (a, VarInfo)
varPair a
n Int
argNo = (a
n, VI
{ viDeps :: DepSet
viDeps = Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
fn, Int -> Arg
Arg Int
argNo) Set Reason
forall a. Set a
S.empty
, viFunArg :: Maybe Int
viFunArg = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
argNo
, viMethod :: Maybe Name
viMethod = Maybe Name
forall a. Maybe a
Nothing
})
([Name]
vars, SC' (TT Name)
sc) = CaseDefs -> ([Name], SC' (TT Name))
cases_runtime CaseDefs
cdefs
etaExpand :: [Name] -> Term -> Term
etaExpand :: [Name] -> TT Name -> TT Name
etaExpand [] TT Name
t = TT Name
t
etaExpand (Name
n : [Name]
ns) TT Name
t = [Name] -> TT Name -> TT Name
etaExpand [Name]
ns (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete TT Name
t (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n TT Name
forall n. TT n
Erased))
getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
getDepsSC :: Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC' (TT Name)
ImpossibleCase = Deps
forall k a. Map k a
M.empty
getDepsSC Name
fn [Name]
es Vars
vs (UnmatchedCase String
msg) = Deps
forall k a. Map k a
M.empty
getDepsSC Name
fn [Name]
es Vars
vs (ProjCase (Proj TT Name
t Int
i) [CaseAlt' (TT Name)]
alts) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (TT Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)
getDepsSC Name
fn [Name]
es Vars
vs (ProjCase (P NameType
_ Name
n TT Name
_) [CaseAlt' (TT Name)]
alts) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (CaseType -> Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
Shared Name
n [CaseAlt' (TT Name)]
alts)
getDepsSC Name
fn [Name]
es Vars
vs (ProjCase TT Name
t [CaseAlt' (TT Name)]
alts) = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"ProjCase not supported:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC' (TT Name) -> String
forall a. Show a => a -> String
show (TT Name -> [CaseAlt' (TT Name)] -> SC' (TT Name)
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)
getDepsSC Name
fn [Name]
es Vars
vs (STerm TT Name
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [] (Node -> Cond
forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) ([Name] -> TT Name -> TT Name
etaExpand [Name]
es TT Name
t)
getDepsSC Name
fn [Name]
es Vars
vs (Case CaseType
sh Name
n [CaseAlt' (TT Name)]
alts)
= Deps -> Deps
addTagDep (Deps -> Deps) -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ (CaseAlt' (TT Name) -> Deps) -> [CaseAlt' (TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> [Name] -> Vars -> VarInfo -> CaseAlt' (TT Name) -> Deps
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
casedVar) [CaseAlt' (TT Name)]
alts
where
addTagDep :: Deps -> Deps
addTagDep = case [CaseAlt' (TT Name)]
alts of
[CaseAlt' (TT Name)
_] -> Deps -> Deps
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
[CaseAlt' (TT Name)]
_ -> (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) (Node -> Cond
forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) (VarInfo -> DepSet
viDeps VarInfo
casedVar)
casedVar :: VarInfo
casedVar = VarInfo -> Maybe VarInfo -> VarInfo
forall a. a -> Maybe a -> a
fromMaybe (String -> VarInfo
forall a. HasCallStack => String -> a
error (String -> VarInfo) -> String -> VarInfo
forall a b. (a -> b) -> a -> b
$ String
"nonpatvar in case: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n) (Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs)
getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt -> Deps
getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt' (TT Name) -> Deps
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (FnCase Name
n [Name]
ns SC' (TT Name)
sc) = Deps
forall k a. Map k a
M.empty
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (ConstCase Const
c SC' (TT Name)
sc) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC' (TT Name)
sc
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (DefaultCase SC' (TT Name)
sc) = Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC' (TT Name)
sc
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (SucCase Name
n SC' (TT Name)
sc)
= Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es (Name -> VarInfo -> Vars -> Vars
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
n VarInfo
var Vars
vs) SC' (TT Name)
sc
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
var (ConCase Name
n Int
cnt [Name]
ns SC' (TT Name)
sc)
= Name -> [Name] -> Vars -> SC' (TT Name) -> Deps
getDepsSC Name
fn [Name]
es (Vars
vs' Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) SC' (TT Name)
sc
where
vs' :: Vars
vs' = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
{ viDeps :: DepSet
viDeps = (Set Reason -> Set Reason -> Set Reason)
-> Node -> Set Reason -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union (Name
n, Int -> Arg
Arg Int
j) (Reason -> Set Reason
forall a. a -> Set a
S.singleton (Name
fn, Int
varIdx)) (VarInfo -> DepSet
viDeps VarInfo
var)
, viFunArg :: Maybe Int
viFunArg = VarInfo -> Maybe Int
viFunArg VarInfo
var
, viMethod :: Maybe Name
viMethod = Int -> Maybe Name
meth Int
j
})
| (Name
v, Int
j) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Int
0..]]
varIdx :: Int
varIdx = Maybe Int -> Int
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 -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Int -> Name
mkFieldName Name
n Int
j)
| Bool
otherwise = \Int
j -> Maybe Name
forall a. Maybe a
Nothing
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 <- Name -> [(Name, Cond -> Deps)] -> Maybe (Cond -> Deps)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Cond -> Deps)]
bs
= Cond -> Deps
deps Cond
cd
| Just VarInfo
var <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
= Cond -> DepSet -> Deps
forall k a. k -> a -> Map k a
M.singleton Cond
cd (VarInfo -> DepSet
viDeps VarInfo
var)
| MN Int
_ Text
_ <- Name
n
= String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"erasure analysis: variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" unbound in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node] -> String
forall a. Show a => a -> String
show (Cond -> [Node]
forall a. Set a -> [a]
S.toList Cond
cd)
| Bool
otherwise = Cond -> DepSet -> Deps
forall k a. k -> a -> Map k a
M.singleton Cond
cd (Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set Reason
forall a. Set a
S.empty)
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (V Int
i) = (Name, Cond -> Deps) -> Cond -> Deps
forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs [(Name, Cond -> Deps)] -> Int -> (Name, Cond -> Deps)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Cond
cd
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Bind Name
n Binder (TT Name)
bdr TT Name
body)
| Lam RigCount
_ TT Name
ty <- Binder (TT Name)
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
| Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
ty TT Name
_ <- Binder (TT Name)
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
| Let RigCount
rig TT Name
ty TT Name
t <- Binder (TT Name)
bdr = TT Name -> Cond -> Deps
var TT Name
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
| NLet TT Name
ty TT Name
t <- Binder (TT Name)
bdr = TT Name -> Cond -> Deps
var TT Name
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs ((Name
n, Deps -> Cond -> Deps
forall a b. a -> b -> a
const Deps
forall k a. Map k a
M.empty) (Name, Cond -> Deps)
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. a -> [a] -> [a]
: [(Name, Cond -> Deps)]
bs) Cond
cd TT Name
body
where
var :: TT Name -> Cond -> Deps
var TT Name
t Cond
cd = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd app :: TT Name
app@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (TT Name
fun, [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
app = case TT Name
fun of
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` ((Int, TT Name) -> Deps) -> [(Int, TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Int, TT Name) -> Deps
methodDeps Name
ctorName) ([Int] -> [TT Name] -> [(Int, TT Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [TT Name]
args)
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"mkForeignPrim"
-> [TT Name] -> Deps
unconditionalDeps ([TT Name] -> Deps) -> [TT Name] -> Deps
forall a b. (a -> b) -> a -> b
$ Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop Int
4 [TT Name]
args
P NameType
_ Name
n TT Name
_
| Just Cond -> Deps
deps <- Name -> [(Name, Cond -> Deps)] -> Maybe (Cond -> Deps)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Cond -> Deps)]
bs
-> Cond -> Deps
deps Cond
cd Deps -> Deps -> Deps
`union` [TT Name] -> Deps
unconditionalDeps [TT Name]
args
| Just VarInfo
var <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
, Just Name
meth <- VarInfo -> Maybe Name
viMethod VarInfo
var
-> VarInfo -> DepSet
viDeps VarInfo
var DepSet -> Deps -> Deps
`ins` Name -> [TT Name] -> Deps
conditionalDeps Name
meth [TT Name]
args
| Just VarInfo
var <- Name -> Vars -> Maybe VarInfo
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 -> (Name, Cond -> Deps) -> Cond -> Deps
forall a b. (a, b) -> b
snd ([(Name, Cond -> Deps)]
bs [(Name, Cond -> Deps)] -> Int -> (Name, Cond -> Deps)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Cond
cd Deps -> Deps -> Deps
`union` [TT Name] -> Deps
unconditionalDeps [TT Name]
args
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 (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
t) TT Name
t')
Bind Name
n (NLet TT Name
ty TT Name
t') TT Name
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
t) TT Name
t')
Proj TT Name
t Int
i
-> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot[0] analyse projection !" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t
TT Name
Erased -> Deps
forall k a. Map k a
M.empty
TT Name
_ -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot analyse application of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
fun String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [TT Name] -> String
forall a. Show a => a -> String
show [TT Name]
args
where
union :: Deps -> Deps -> Deps
union = (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps)
-> (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ (Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union
ins :: DepSet -> Deps -> Deps
ins = (DepSet -> DepSet -> DepSet) -> Cond -> DepSet -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
cd
unconditionalDeps :: [Term] -> Deps
unconditionalDeps :: [TT Name] -> Deps
unconditionalDeps = (TT Name -> Deps) -> [TT Name] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd)
conditionalDeps :: Name -> [Term] -> Deps
conditionalDeps :: Name -> [TT Name] -> Deps
conditionalDeps Name
n
= DepSet -> Deps -> Deps
ins (Node -> Set Reason -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set Reason
forall a. Set a
S.empty) (Deps -> Deps) -> ([TT Name] -> Deps) -> [TT Name] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Maybe Int, TT Name) -> Deps) -> [(Maybe Int, TT Name)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Maybe Int, TT Name) -> Deps
getDepsArgs Name
n) ([(Maybe Int, TT Name)] -> Deps)
-> ([TT Name] -> [(Maybe Int, TT Name)]) -> [TT Name] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Maybe Int] -> [TT Name] -> [(Maybe Int, TT Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Int]
indices
where
indices :: [Maybe Int]
indices = (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int
0 .. Name -> Int
getArity Name
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ Maybe Int -> [Maybe Int]
forall a. a -> [a]
repeat Maybe Int
forall a. Maybe a
Nothing
getDepsArgs :: Name -> (Maybe Int, TT Name) -> Deps
getDepsArgs Name
n (Just Int
i, TT Name
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> TT Name -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs (Node -> Cond -> Cond
forall a. Ord a => a -> Set a -> Set a
S.insert (Name
n, Int -> Arg
Arg Int
i) Cond
cd) TT Name
t
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 Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) ([(Name, Cond -> Deps)]
forall {k} {a}. [(Name, k -> Map k (Map Node (Set a)))]
bruijns [(Name, Cond -> Deps)]
-> [(Name, Cond -> Deps)] -> [(Name, Cond -> Deps)]
forall a. [a] -> [a] -> [a]
++ [(Name, Cond -> Deps)]
bs) Cond
cond TT Name
body
where
vars :: Vars
vars = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI
{ viDeps :: DepSet
viDeps = Int -> DepSet
forall {a}. Int -> Map Node (Set a)
deps Int
i
, viFunArg :: Maybe Int
viFunArg = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
, viMethod :: Maybe Name
viMethod = Maybe Name
forall a. Maybe a
Nothing
}) | (Name
v, Int
i) <- [Name] -> [Int] -> [Reason]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [Int
0..]]
deps :: Int -> Map Node (Set a)
deps Int
i = Node -> Set a -> Map Node (Set a)
forall k a. k -> a -> Map k a
M.singleton (Name
metameth, Int -> Arg
Arg Int
i) Set a
forall a. Set a
S.empty
bruijns :: [(Name, k -> Map k (Map Node (Set a)))]
bruijns = [(Name, k -> Map k (Map Node (Set a)))]
-> [(Name, k -> Map k (Map Node (Set a)))]
forall a. [a] -> [a]
reverse [(Name
n, \k
cd -> k -> Map Node (Set a) -> Map k (Map Node (Set a))
forall k a. k -> a -> Map k a
M.singleton k
cd (Int -> Map Node (Set a)
forall {a}. Int -> Map Node (Set a)
deps Int
i)) | (Int
i, Name
n) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
args]
cond :: Cond
cond = Node -> Cond
forall a. a -> Set a
S.singleton (Name
metameth, Arg
Result)
metameth :: Name
metameth = Name -> Int -> Name
mkFieldName Name
ctorName Int
methNo
([Name]
args, TT Name
body) = TT Name -> ([Name], TT Name)
unfoldLams TT Name
t
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) = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot[1] analyse projection !" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t
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
_) = Deps
forall k a. Map k a
M.empty
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (TType UExp
_) = Deps
forall k a. Map k a
M.empty
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (UType Universe
_) = Deps
forall k a. Map k a
M.empty
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
Erased = Deps
forall k a. Map k a
M.empty
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
Impossible = Deps
forall k a. Map k a
M.empty
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd TT Name
t = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ String
"cannot get deps of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
t
getArity :: Name -> Int
getArity :: Name -> Int
getArity (SN (WhereN Int
i' Name
ctorName (MN Int
i Text
field)))
| Just (TyDecl (DCon Int
_ Int
_ Bool
_) TT Name
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
ctorName Context
ctx
= let argTys :: [TT Name]
argTys = ((Name, TT Name) -> TT Name) -> [(Name, TT Name)] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd ([(Name, TT Name)] -> [TT Name]) -> [(Name, TT Name)] -> [TT Name]
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ty
in if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [TT Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT Name]
argTys
then [(Name, TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, TT Name)] -> Int) -> [(Name, TT Name)] -> Int
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys ([TT Name]
argTys [TT Name] -> Int -> TT Name
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
else String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"invalid field number " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ctorName
| Bool
otherwise = String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"unknown implementation constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ctorName
getArity Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
Just (CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
tys [Either (TT Name) (TT Name, TT Name)]
def [([Name], TT Name, TT Name)]
tot CaseDefs
cdefs) -> [(TT Name, Bool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(TT Name, Bool)]
tys
Just (TyDecl (DCon Int
tag Int
arity Bool
_) TT Name
_) -> Int
arity
Just (TyDecl (NameType
Ref) TT Name
ty) -> [(Name, TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, TT Name)] -> Int) -> [(Name, TT Name)] -> Int
forall a b. (a -> b) -> a -> b
$ TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ty
Just (Operator TT Name
ty Int
arity [Value] -> Maybe Value
op) -> Int
arity
Just Def
df -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: unrecognised entity '"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' with definition: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Def -> String
forall a. Show a => a -> String
show Def
df
Maybe Def
Nothing -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"Erasure/getArity: definition not found for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
lamToLet :: Term -> Term
lamToLet :: TT Name -> TT Name
lamToLet TT Name
tm = Int -> [TT Name] -> TT Name -> TT Name
lamToLet' Int
0 [TT Name]
args TT Name
f
where
(TT Name
f, [TT Name]
args) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm
lamToLet' :: Int -> [Term] -> Term -> Term
lamToLet' :: Int -> [TT Name] -> TT Name -> TT Name
lamToLet' Int
wk (TT Name
v:[TT Name]
vs) (Bind Name
n (Lam RigCount
rig TT Name
ty) TT Name
tm) = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig TT Name
ty (Int -> TT Name -> TT Name
forall n. Int -> TT n -> TT n
weakenTm Int
wk TT Name
v)) (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ Int -> [TT Name] -> TT Name -> TT Name
lamToLet' (Int
wkInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [TT Name]
vs TT Name
tm
lamToLet' Int
wk [TT Name]
vs TT Name
tm = TT Name -> [TT Name] -> TT Name
forall n. TT n -> [TT n] -> TT n
mkApp TT Name
tm ([TT Name] -> TT Name) -> [TT Name] -> TT Name
forall a b. (a -> b) -> a -> b
$ (TT Name -> TT Name) -> [TT Name] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TT Name -> TT Name
forall n. Int -> TT n -> TT n
weakenTm Int
wk) [TT Name]
vs
unfoldLams :: Term -> ([Name], Term)
unfoldLams :: TT Name -> ([Name], TT Name)
unfoldLams (Bind Name
n (Lam RigCount
_ TT Name
ty) TT Name
t) = let ([Name]
ns,TT Name
t') = TT Name -> ([Name], TT Name)
unfoldLams TT Name
t in (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns, TT Name
t')
unfoldLams TT Name
t = ([], TT Name
t)
union :: Deps -> Deps -> Deps
union :: Deps -> Deps -> Deps
union = (DepSet -> DepSet -> DepSet) -> Deps -> Deps -> Deps
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union)
unionMap :: (a -> Deps) -> [a] -> Deps
unionMap :: forall a. (a -> Deps) -> [a] -> Deps
unionMap a -> Deps
f = (DepSet -> DepSet -> DepSet) -> [Deps] -> Deps
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith ((Set Reason -> Set Reason -> Set Reason)
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set Reason -> Set Reason -> Set Reason
forall a. Ord a => Set a -> Set a -> Set a
S.union) ([Deps] -> Deps) -> ([a] -> [Deps]) -> [a] -> Deps
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Deps) -> [a] -> [Deps]
forall a b. (a -> b) -> [a] -> [b]
map a -> Deps
f
mkFieldName :: Name -> Int -> Name
mkFieldName :: Name -> Int -> Name
mkFieldName Name
ctorName Int
fieldNo = SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
fieldNo Name
ctorName (Name -> SpecialName) -> Name -> SpecialName
forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
fieldNo String
"field")