{-# 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
(Arg -> Arg -> Bool) -> (Arg -> Arg -> Bool) -> Eq Arg
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
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
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
$cp1Ord :: Eq Arg
Ord)
instance Show Arg where
show :: Arg -> String
show (Arg i :: Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i
show Result = "*"
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
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 startNames :: [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 (m :: * -> *) a. Monad m => a -> m a
return []
main :: [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
[(Name, Int)]
used <- IState -> [(Name, Int)]
idris_erasureUsed (IState -> [(Name, Int)])
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) [(Name, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
Set (Name, Int)
externs <- IState -> Set (Name, Int)
idris_externs (IState -> Set (Name, Int))
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) (Set (Name, Int))
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
-> [(Name, Int)] -> [(Name, Int)] -> Context -> [Name] -> Deps
buildDepMap Ctxt InterfaceInfo
ci [(Name, Int)]
used (Set (Name, Int) -> [(Name, Int)]
forall a. Set a -> [a]
S.toList Set (Name, Int)
externs) Context
ctx [Name]
main
let (residDeps :: Deps
residDeps, (reachableNames :: Set Name
reachableNames, minUse :: UseMap
minUse)) = Deps -> (Deps, (Set Name, UseMap))
minimalUsage Deps
depMap
usage :: [(Name, IntMap (Set (Name, Int)))]
usage = UseMap -> [(Name, IntMap (Set (Name, Int)))]
forall k a. Map k a -> [(k, a)]
M.toList UseMap
minUse
Int -> String -> Idris ()
logErasure 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 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 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 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 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 4 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Minimal usage:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, IntMap (Set (Name, Int)))] -> String
fmtUseMap [(Name, IntMap (Set (Name, Int)))]
usage
Int -> String -> Idris ()
logErasure 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Opt] -> Bool) -> (IState -> [Opt]) -> IState -> Bool
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 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 (Name, Int))) -> Idris ())
-> [(Name, IntMap (Set (Name, Int)))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ctxt OptInfo -> (Name, IntMap (Set (Name, Int))) -> Idris ()
checkAccessibility Ctxt OptInfo
opt) [(Name, IntMap (Set (Name, Int)))]
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 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 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 ("reachable postulates:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [" " 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 (Name, Int))) -> Idris ())
-> [(Name, IntMap (Set (Name, Int)))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, IntMap (Set (Name, Int))) -> Idris ()
storeUsage [(Name, IntMap (Set (Name, Int)))]
usage
[Name] -> Idris [Name]
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 -> ShowS
forall a. [a] -> [a] -> [a]
++)
fmtItem :: (Cond, DepSet) -> String
fmtItem :: (Cond, DepSet) -> String
fmtItem (cond :: Cond
cond, deps :: 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Node, Set (Name, Int))] -> String
forall a. Show a => a -> String
show (DepSet -> [(Node, Set (Name, Int))]
forall k a. Map k a -> [(k, a)]
M.toList DepSet
deps)
fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
fmtUseMap :: [(Name, IntMap (Set (Name, Int)))] -> String
fmtUseMap = [String] -> String
unlines ([String] -> String)
-> ([(Name, IntMap (Set (Name, Int)))] -> [String])
-> [(Name, IntMap (Set (Name, Int)))]
-> String
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 (Name, Int))) -> String)
-> [(Name, IntMap (Set (Name, Int)))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n,is :: IntMap (Set (Name, Int))
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ IntMap (Set (Name, Int)) -> String
fmtIxs IntMap (Set (Name, Int))
is)
fmtIxs :: IntMap (Set Reason) -> String
fmtIxs :: IntMap (Set (Name, Int)) -> String
fmtIxs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([String] -> String)
-> (IntMap (Set (Name, Int)) -> [String])
-> IntMap (Set (Name, Int))
-> String
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Int, Set (Name, Int)) -> String)
-> [(Int, Set (Name, Int))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Set (Name, Int)) -> String
forall a a. (Show a, Show a) => (a, Set a) -> String
fmtArg ([(Int, Set (Name, Int))] -> [String])
-> (IntMap (Set (Name, Int)) -> [(Int, Set (Name, Int))])
-> IntMap (Set (Name, Int))
-> [String]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IntMap (Set (Name, Int)) -> [(Int, Set (Name, Int))]
forall a. IntMap a -> [(Int, a)]
IM.toList
where
fmtArg :: (a, Set a) -> String
fmtArg (i :: a
i, rs :: 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]
++ " from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((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 (Name, Int))) -> Idris ()
storeUsage (n :: Name
n, args :: IntMap (Set (Name, Int))
args) = Field IState [(Int, [(Name, Int)])]
-> [(Int, [(Name, Int)])] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
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, [(Name, Int)])]
flat
where
flat :: [(Int, [(Name, Int)])]
flat = [(Int
i, Set (Name, Int) -> [(Name, Int)]
forall a. Set a -> [a]
S.toList Set (Name, Int)
rs) | (i :: Int
i,rs :: Set (Name, Int)
rs) <- IntMap (Set (Name, Int)) -> [(Int, Set (Name, Int))]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap (Set (Name, Int))
args]
checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set (Name, Int))) -> Idris ()
checkAccessibility opt :: Ctxt OptInfo
opt (n :: Name
n, reachable :: IntMap (Set (Name, Int))
reachable)
| Just (Optimise inaccessible :: [(Int, Name)]
inaccessible dt :: Bool
dt force :: [Int]
force) <- Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n Ctxt OptInfo
opt
, eargs :: [String]
eargs@(_:_) <- [Name -> [(Name, Int)] -> String
forall a a a. (Show a, Show a, Show a) => a -> [(a, a)] -> String
fmt Name
n (Set (Name, Int) -> [(Name, Int)]
forall a. Set a -> [a]
S.toList Set (Name, Int)
rs) | (i :: Int
i,n :: Name
n) <- [(Int, Name)]
inaccessible, Set (Name, Int)
rs <- Maybe (Set (Name, Int)) -> [Set (Name, Int)]
forall a. Maybe a -> [a]
maybeToList (Maybe (Set (Name, Int)) -> [Set (Name, Int)])
-> Maybe (Set (Name, Int)) -> [Set (Name, Int)]
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Set (Name, Int)) -> Maybe (Set (Name, Int))
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (Set (Name, Int))
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]
++ ": inaccessible arguments reachable:\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n " [String]
eargs
| Bool
otherwise = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
fmt :: a -> [(a, a)] -> String
fmt n :: a
n [] = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (no more information available)"
fmt n :: a
n rs :: [(a, a)]
rs = a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [a -> String
forall a. Show a => a -> String
show a
rn String -> ShowS
forall a. [a] -> [a] -> [a]
++ " arg# " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ri | (rn :: a
rn,ri :: a
ri) <- [(a, a)]
rs]
warn :: String -> Idris ()
warn = Int -> String -> Idris ()
logErasure 0
type Constraint = (Cond, DepSet)
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
minimalUsage deps :: Deps
deps
= IntMap (Cond, DepSet) -> Deps
fromNumbered (IntMap (Cond, DepSet) -> Deps)
-> (DepSet -> (Set Name, UseMap))
-> (IntMap (Cond, DepSet), DepSet)
-> (Deps, (Set Name, UseMap))
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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> [DepSet] -> DepSet
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union [DepSet
ds | (cond :: Cond
cond, ds :: 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 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 [0..] ([(Cond, DepSet)] -> [(Int, (Cond, DepSet))])
-> (Deps -> [(Cond, DepSet)]) -> Deps -> [(Int, (Cond, DepSet))]
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 (ns :: k
ns, vs :: 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 (
\i :: Int
i (ns :: Cond
ns, _ds :: DepSet
_ds) ix :: Map Node IntSet
ix -> (Node -> Map Node IntSet -> Map Node IntSet)
-> Map Node IntSet -> [Node] -> Map Node IntSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (
\n :: Node
n ix' :: 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 (Name, Int))
-> (Set Name, UseMap) -> (Set Name, UseMap))
-> (Set Name, UseMap)
-> [(Node, Set (Name, Int))]
-> (Set Name, UseMap)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Node, Set (Name, Int)) -> (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 (Name, Int))] -> (Set Name, UseMap))
-> (DepSet -> [(Node, Set (Name, Int))])
-> DepSet
-> (Set Name, UseMap)
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 (Name, Int))]
forall k a. Map k a -> [(k, a)]
M.toList
where
ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins :: (Node, Set (Name, Int)) -> (Set Name, UseMap) -> (Set Name, UseMap)
ins ((n :: Name
n, Result), rs :: Set (Name, Int)
rs) (ns :: Set Name
ns, umap :: 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 ((n :: Name
n, Arg i :: Int
i ), rs :: Set (Name, Int)
rs) (ns :: Set Name
ns, umap :: UseMap
umap) = (Set Name
ns, (IntMap (Set (Name, Int))
-> IntMap (Set (Name, Int)) -> IntMap (Set (Name, Int)))
-> Name -> IntMap (Set (Name, Int)) -> UseMap -> UseMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> IntMap (Set (Name, Int))
-> IntMap (Set (Name, Int))
-> IntMap (Set (Name, Int))
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union) Name
n (Int -> Set (Name, Int) -> IntMap (Set (Name, Int))
forall a. Int -> a -> IntMap a
IM.singleton Int
i Set (Name, Int)
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 index :: Map Node IntSet
index solution :: DepSet
solution previouslyNew :: DepSet
previouslyNew constrs :: 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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
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
]
(currentlyNew :: DepSet
currentlyNew, constrs' :: 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 previouslyNew :: Cond
previouslyNew i :: Int
i (news :: DepSet
news, constrs :: IntMap (Cond, DepSet)
constrs)
| Just (cond :: Cond
cond, deps :: 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'
| Cond -> Bool
forall a. Set a -> Bool
S.null Cond
cond'
-> ((Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
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
-> [(Name, Int)] -> [(Name, Int)] -> Context -> [Name] -> Deps
buildDepMap ci :: Ctxt InterfaceInfo
ci used :: [(Name, Int)]
used externs :: [(Name, Int)]
externs ctx :: Context
ctx startNames :: [Name]
startNames
= [(Name, Int)] -> Deps -> Deps
addPostulates [(Name, Int)]
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 :: [(Name, Int)] -> Deps -> Deps
addPostulates used :: [(Name, Int)]
used deps :: Deps
deps = ((Cond, DepSet) -> Deps -> Deps)
-> Deps -> [(Cond, DepSet)] -> Deps
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(ds :: Cond
ds, rs :: 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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
ds DepSet
rs) Deps
deps ([(Name, Int)] -> [(Cond, DepSet)]
forall a a. Ord a => [(Name, Int)] -> [(Set a, Map Node (Set a))]
postulates [(Name, Int)]
used)
where
==> :: [a] -> [k] -> (Set a, Map k (Set a))
(==>) ds :: [a]
ds rs :: [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 n :: String
n is :: [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 "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 :: [(Name, Int)]
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 :: [(Name, Int)] -> [(Set a, Map Node (Set a))]
postulates used :: [(Name, Int)]
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 (\n :: Name
n -> (Name
n, Arg
Result)) [Name]
startNames)
,[(String -> Name
sUN "run__IO", Arg
Result), (String -> Name
sUN "run__IO", Int -> Arg
Arg 1)]
,[(String -> Name
sUN "call__IO", Arg
Result), (String -> Name
sUN "call__IO", Int -> Arg
Arg 2)]
, ((Name, Int) -> Node) -> [(Name, Int)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, i :: Int
i) -> (Name
n, Int -> Arg
Arg Int
i)) [(Name, Int)]
used
, String -> [Int] -> [Node]
it "MkIO" [2]
, String -> [Int] -> [Node]
it "prim__IO" [1]
, [(Name
pairCon, Int -> Arg
Arg 2),
(Name
pairCon, Int -> Arg
Arg 3)]
, String -> [Int] -> [Node]
it "prim_fork" [0]
, String -> [Int] -> [Node]
it "unsafePerformPrimIO" [1]
, String -> [Int] -> [Node]
it "prim__believe_me" [2]
, [(Name
n, Int -> Arg
Arg Int
i) | (n :: Name
n,arity :: Int
arity) <- [(Name, Int)]
usedPrims, Int
i <- [0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]]
, [(Name
n, Int -> Arg
Arg Int
i) | (n :: Name
n,arity :: Int
arity) <- [(Name, Int)]
externs, Int
i <- [0..Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]]
]
]
dfs :: Set Name -> Deps -> [Name] -> Deps
dfs :: Set Name -> Deps -> [Name] -> Deps
dfs visited :: Set Name
visited deps :: Deps
deps [] = Deps
deps
dfs visited :: Set Name
visited deps :: Deps
deps (n :: Name
n : ns :: [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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
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 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 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 (cs :: Set (a, b)
cs, ns :: 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 i :: Int
i (SN (ImplementationCtorN interfaceN :: Name
interfaceN)) (MN i' :: Int
i' field :: Text
field)))
= Deps
forall k a. Map k a
M.empty
getDeps n :: Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
Just def :: Def
def -> Name -> Def -> Deps
getDepsDef Name
n Def
def
Nothing -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "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 fn :: Name
fn (Function ty :: Type
ty t :: Type
t) = String -> Deps
forall a. HasCallStack => String -> a
error "a function encountered"
getDepsDef fn :: Name
fn (TyDecl ty :: NameType
ty t :: Type
t) = Deps
forall k a. Map k a
M.empty
getDepsDef fn :: Name
fn (Operator ty :: Type
ty n' :: Int
n' f :: [Value] -> Maybe Value
f) = Deps
forall k a. Map k a
M.empty
getDepsDef fn :: Name
fn (CaseOp ci :: CaseInfo
ci ty :: Type
ty tys :: [(Type, Bool)]
tys def :: [Either Type (Type, Type)]
def tot :: [([Name], Type, Type)]
tot cdefs :: CaseDefs
cdefs)
= Name -> [Name] -> Vars -> SC -> 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
sc
where
etaIdx :: [Int]
etaIdx = [[Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
vars .. [(Type, Bool)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, Bool)]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 i :: Int
i = Int -> Text -> Name
MN Int
i (String -> Text
pack "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 | (v :: Name
v,i :: Int
i) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars [0..]]
varPair :: a -> Int -> (a, VarInfo)
varPair n :: a
n argNo :: Int
argNo = (a
n, VI :: DepSet -> Maybe Int -> Maybe Name -> VarInfo
VI
{ viDeps :: DepSet
viDeps = Node -> Set (Name, Int) -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
fn, Int -> Arg
Arg Int
argNo) Set (Name, Int)
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
})
(vars :: [Name]
vars, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cdefs
etaExpand :: [Name] -> Term -> Term
etaExpand :: [Name] -> Type -> Type
etaExpand [] t :: Type
t = Type
t
etaExpand (n :: Name
n : ns :: [Name]
ns) t :: Type
t = [Name] -> Type -> Type
etaExpand [Name]
ns (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Type
t (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
forall n. TT n
Erased))
getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs ImpossibleCase = Deps
forall k a. Map k a
M.empty
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (UnmatchedCase msg :: String
msg) = Deps
forall k a. Map k a
M.empty
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (ProjCase (Proj t :: Type
t i :: Int
i) alts :: [CaseAlt' Type]
alts) = Name -> [Name] -> Vars -> SC -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (Type -> [CaseAlt' Type] -> SC
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase Type
t [CaseAlt' Type]
alts)
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (ProjCase (P _ n :: Name
n _) alts :: [CaseAlt' Type]
alts) = Name -> [Name] -> Vars -> SC -> Deps
getDepsSC Name
fn [Name]
es Vars
vs (CaseType -> Name -> [CaseAlt' Type] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
Shared Name
n [CaseAlt' Type]
alts)
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (ProjCase t :: Type
t alts :: [CaseAlt' Type]
alts) = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "ProjCase not supported:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show (Type -> [CaseAlt' Type] -> SC
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase Type
t [CaseAlt' Type]
alts)
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (STerm t :: Type
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [] (Node -> Cond
forall a. a -> Set a
S.singleton (Name
fn, Arg
Result)) ([Name] -> Type -> Type
etaExpand [Name]
es Type
t)
getDepsSC fn :: Name
fn es :: [Name]
es vs :: Vars
vs (Case sh :: CaseType
sh n :: Name
n alts :: [CaseAlt' Type]
alts)
= Deps -> Deps
addTagDep (Deps -> Deps) -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ (CaseAlt' Type -> Deps) -> [CaseAlt' Type] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> [Name] -> Vars -> VarInfo -> CaseAlt' Type -> Deps
getDepsAlt Name
fn [Name]
es Vars
vs VarInfo
casedVar) [CaseAlt' Type]
alts
where
addTagDep :: Deps -> Deps
addTagDep = case [CaseAlt' Type]
alts of
[_] -> Deps -> Deps
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
_ -> (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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
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
$ "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' Type -> Deps
getDepsAlt fn :: Name
fn es :: [Name]
es vs :: Vars
vs var :: VarInfo
var (FnCase n :: Name
n ns :: [Name]
ns sc :: SC
sc) = Deps
forall k a. Map k a
M.empty
getDepsAlt fn :: Name
fn es :: [Name]
es vs :: Vars
vs var :: VarInfo
var (ConstCase c :: Const
c sc :: SC
sc) = Name -> [Name] -> Vars -> SC -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC
sc
getDepsAlt fn :: Name
fn es :: [Name]
es vs :: Vars
vs var :: VarInfo
var (DefaultCase sc :: SC
sc) = Name -> [Name] -> Vars -> SC -> Deps
getDepsSC Name
fn [Name]
es Vars
vs SC
sc
getDepsAlt fn :: Name
fn es :: [Name]
es vs :: Vars
vs var :: VarInfo
var (SucCase n :: Name
n sc :: SC
sc)
= Name -> [Name] -> Vars -> SC -> 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
sc
getDepsAlt fn :: Name
fn es :: [Name]
es vs :: Vars
vs var :: VarInfo
var (ConCase n :: Name
n cnt :: Int
cnt ns :: [Name]
ns sc :: SC
sc)
= Name -> [Name] -> Vars -> SC -> 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
sc
where
vs' :: Vars
vs' = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI :: DepSet -> Maybe Int -> Maybe Name -> VarInfo
VI
{ viDeps :: DepSet
viDeps = (Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> Node -> Set (Name, Int) -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union (Name
n, Int -> Arg
Arg Int
j) ((Name, Int) -> Set (Name, Int)
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
})
| (v :: Name
v, j :: Int
j) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [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 interfaceName :: Name
interfaceName) <- Name
n = \j :: Int
j -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Int -> Name
mkFieldName Name
n Int
j)
| Bool
otherwise = \j :: Int
j -> Maybe Name
forall a. Maybe a
Nothing
getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps
getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (P _ n :: Name
n _)
| Just deps :: 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 var :: 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 _ _ <- Name
n
= String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "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]
++ " 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 (Name, Int) -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set (Name, Int)
forall a. Set a
S.empty)
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (V i :: 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. [a] -> Int -> a
!! Int
i) Cond
cd
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (Bind n :: Name
n bdr :: Binder Type
bdr body :: Type
body)
| Lam _ ty :: Type
ty <- Binder Type
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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 Type
body
| Pi _ _ ty :: Type
ty _ <- Binder Type
bdr = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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 Type
body
| Let rig :: RigCount
rig ty :: Type
ty t :: Type
t <- Binder Type
bdr = Type -> Cond -> Deps
var Type
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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 Type
body
| NLet ty :: Type
ty t :: Type
t <- Binder Type
bdr = Type -> Cond -> Deps
var Type
t Cond
cd Deps -> Deps -> Deps
`union` Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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 Type
body
where
var :: Type -> Cond -> Deps
var t :: Type
t cd :: Cond
cd = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd Type
t
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd app :: Type
app@(App _ _ _)
| (fun :: Type
fun, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
app = case Type
fun of
P (DCon _ _ _) ctorName :: Name
ctorName@(SN (ImplementationCtorN interfaceName :: Name
interfaceName)) _
-> Name -> [Type] -> Deps
conditionalDeps Name
ctorName [Type]
args
Deps -> Deps -> Deps
`union` ((Int, Type) -> Deps) -> [(Int, Type)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Int, Type) -> Deps
methodDeps Name
ctorName) ([Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Type]
args)
P (TCon _ _) n :: Name
n _ -> [Type] -> Deps
unconditionalDeps [Type]
args
P (DCon _ _ _) n :: Name
n _ -> Name -> [Type] -> Deps
conditionalDeps Name
n [Type]
args
P _ (UN n :: Text
n) _
| Text
n Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "mkForeignPrim"
-> [Type] -> Deps
unconditionalDeps ([Type] -> Deps) -> [Type] -> Deps
forall a b. (a -> b) -> a -> b
$ Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop 4 [Type]
args
P _ n :: Name
n _
| Just deps :: 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` [Type] -> Deps
unconditionalDeps [Type]
args
| Just var :: VarInfo
var <- Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs
, Just meth :: Name
meth <- VarInfo -> Maybe Name
viMethod VarInfo
var
-> VarInfo -> DepSet
viDeps VarInfo
var DepSet -> Deps -> Deps
`ins` Name -> [Type] -> Deps
conditionalDeps Name
meth [Type]
args
| Just var :: 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` [Type] -> Deps
unconditionalDeps [Type]
args
| Bool
otherwise
-> Name -> [Type] -> Deps
conditionalDeps Name
n [Type]
args
V i :: 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. [a] -> Int -> a
!! Int
i) Cond
cd Deps -> Deps -> Deps
`union` [Type] -> Deps
unconditionalDeps [Type]
args
Bind n :: Name
n (Lam _ ty :: Type
ty) t :: Type
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (Type -> Type
lamToLet Type
app)
Bind n :: Name
n (Let _ ty :: Type
ty t' :: Type
t') t :: Type
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Type
ty) Type
t) Type
t')
Bind n :: Name
n (NLet ty :: Type
ty t' :: Type
t') t :: Type
t -> Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Type
ty) Type
t) Type
t')
Proj t :: Type
t i :: Int
i
-> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "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]
++ " of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t
Erased -> Deps
forall k a. Map k a
M.empty
_ -> String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "cannot analyse application of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
fun String -> ShowS
forall a. [a] -> [a] -> [a]
++ " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
forall a. Show a => a -> String
show [Type]
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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union) Cond
cd
unconditionalDeps :: [Term] -> Deps
unconditionalDeps :: [Type] -> Deps
unconditionalDeps = (Type -> Deps) -> [Type] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd)
conditionalDeps :: Name -> [Term] -> Deps
conditionalDeps :: Name -> [Type] -> Deps
conditionalDeps n :: Name
n
= DepSet -> Deps -> Deps
ins (Node -> Set (Name, Int) -> DepSet
forall k a. k -> a -> Map k a
M.singleton (Name
n, Arg
Result) Set (Name, Int)
forall a. Set a
S.empty) (Deps -> Deps) -> ([Type] -> Deps) -> [Type] -> Deps
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Maybe Int, Type) -> Deps) -> [(Maybe Int, Type)] -> Deps
forall a. (a -> Deps) -> [a] -> Deps
unionMap (Name -> (Maybe Int, Type) -> Deps
getDepsArgs Name
n) ([(Maybe Int, Type)] -> Deps)
-> ([Type] -> [(Maybe Int, Type)]) -> [Type] -> Deps
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Maybe Int] -> [Type] -> [(Maybe Int, Type)]
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 [0 .. Name -> Int
getArity Name
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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, Type) -> Deps
getDepsArgs n :: Name
n (Just i :: Int
i, t :: Type
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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) Type
t
getDepsArgs n :: Name
n (Nothing, t :: Type
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd Type
t
methodDeps :: Name -> (Int, Term) -> Deps
methodDeps :: Name -> (Int, Type) -> Deps
methodDeps ctorName :: Name
ctorName (methNo :: Int
methNo, t :: Type
t)
= Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> 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 Type
body
where
vars :: Vars
vars = [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI :: DepSet -> Maybe Int -> Maybe Name -> VarInfo
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
}) | (v :: Name
v, i :: Int
i) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [0..]]
deps :: Int -> Map Node (Set a)
deps i :: 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, \cd :: 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)) | (i :: Int
i, n :: Name
n) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [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
(args :: [Name]
args, body :: Type
body) = Type -> ([Name], Type)
unfoldLams Type
t
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (Proj t :: Type
t (-1)) = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd Type
t
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (Proj t :: Type
t i :: Int
i) = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "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]
++ " of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (Inferred t :: Type
t) = Vars -> [(Name, Cond -> Deps)] -> Cond -> Type -> Deps
getDepsTerm Vars
vs [(Name, Cond -> Deps)]
bs Cond
cd Type
t
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (Constant _) = Deps
forall k a. Map k a
M.empty
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (TType _) = Deps
forall k a. Map k a
M.empty
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd (UType _) = Deps
forall k a. Map k a
M.empty
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd Erased = Deps
forall k a. Map k a
M.empty
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd Impossible = Deps
forall k a. Map k a
M.empty
getDepsTerm vs :: Vars
vs bs :: [(Name, Cond -> Deps)]
bs cd :: Cond
cd t :: Type
t = String -> Deps
forall a. HasCallStack => String -> a
error (String -> Deps) -> String -> Deps
forall a b. (a -> b) -> a -> b
$ "cannot get deps of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t
getArity :: Name -> Int
getArity :: Name -> Int
getArity (SN (WhereN i' :: Int
i' ctorName :: Name
ctorName (MN i :: Int
i field :: Text
field)))
| Just (TyDecl (DCon _ _ _) ty :: Type
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
ctorName Context
ctx
= let argTys :: [Type]
argTys = ((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd ([(Name, Type)] -> [Type]) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
ty
in if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
argTys
then [(Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, Type)] -> Int) -> [(Name, Type)] -> Int
forall a b. (a -> b) -> a -> b
$ Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys ([Type]
argTys [Type] -> Int -> Type
forall a. [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
$ "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]
++ " 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
$ "unknown implementation constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ctorName
getArity n :: Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctx of
Just (CaseOp ci :: CaseInfo
ci ty :: Type
ty tys :: [(Type, Bool)]
tys def :: [Either Type (Type, Type)]
def tot :: [([Name], Type, Type)]
tot cdefs :: CaseDefs
cdefs) -> [(Type, Bool)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, Bool)]
tys
Just (TyDecl (DCon tag :: Int
tag arity :: Int
arity _) _) -> Int
arity
Just (TyDecl (NameType
Ref) ty :: Type
ty) -> [(Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, Type)] -> Int) -> [(Name, Type)] -> Int
forall a b. (a -> b) -> a -> b
$ Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
ty
Just (Operator ty :: Type
ty arity :: Int
arity op :: [Value] -> Maybe Value
op) -> Int
arity
Just df :: Def
df -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ "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]
++ "' with definition: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Def -> String
forall a. Show a => a -> String
show Def
df
Nothing -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ "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 :: Type -> Type
lamToLet tm :: Type
tm = [Type] -> Type -> Type
lamToLet' [Type]
args Type
f
where
(f :: Type
f, args :: [Type]
args) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
tm
lamToLet' :: [Term] -> Term -> Term
lamToLet' :: [Type] -> Type -> Type
lamToLet' (v :: Type
v:vs :: [Type]
vs) (Bind n :: Name
n (Lam rig :: RigCount
rig ty :: Type
ty) tm :: Type
tm) = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Type -> Binder Type
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Type
ty Type
v) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> Type
lamToLet' [Type]
vs Type
tm
lamToLet' [] tm :: Type
tm = Type
tm
lamToLet' vs :: [Type]
vs tm :: Type
tm = String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$
"Erasure.hs:lamToLet': unexpected input: "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "vs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
forall a. Show a => a -> String
show [Type]
vs String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", tm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tm
unfoldLams :: Term -> ([Name], Term)
unfoldLams :: Type -> ([Name], Type)
unfoldLams (Bind n :: Name
n (Lam _ ty :: Type
ty) t :: Type
t) = let (ns :: [Name]
ns,t' :: Type
t') = Type -> ([Name], Type)
unfoldLams Type
t in (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns, Type
t')
unfoldLams t :: Type
t = ([], Type
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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union)
unionMap :: (a -> Deps) -> [a] -> Deps
unionMap :: (a -> Deps) -> [a] -> Deps
unionMap f :: 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 (Name, Int) -> Set (Name, Int) -> Set (Name, Int))
-> DepSet -> DepSet -> DepSet
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Set (Name, Int) -> Set (Name, Int) -> Set (Name, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union) ([Deps] -> Deps) -> ([a] -> [Deps]) -> [a] -> Deps
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 ctorName :: Name
ctorName fieldNo :: 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 "field")