{-|
Module      : Idris.WhoCalls
Description : Find function callers and callees.

License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.WhoCalls (whoCalls, callsWho) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT

import Data.List (nub)

occurs :: Name -> Term -> Bool
occurs :: Name -> Term -> Bool
occurs Name
n (P NameType
Bound Name
_ Term
_) = Bool
False
occurs Name
n (P NameType
_ Name
n' Term
_) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
occurs Name
n (Bind Name
_ Binder Term
b Term
sc) = Name -> Binder Term -> Bool
occursBinder Name
n Binder Term
b Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
sc
occurs Name
n (App AppStatus Name
_ Term
t1 Term
t2) = Name -> Term -> Bool
occurs Name
n Term
t1 Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
t2
occurs Name
n (Proj Term
t Int
_) = Name -> Term -> Bool
occurs Name
n Term
t
occurs Name
n Term
_ = Bool
False

names :: Term -> [Name]
names :: Term -> [Name]
names (P NameType
Bound Name
_ Term
_) = []
names (P NameType
_ Name
n Term
_) = [Name
n]
names (Bind Name
_ Binder Term
b Term
sc) = Binder Term -> [Name]
namesBinder Binder Term
b [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
sc
names (App AppStatus Name
_ Term
t1 Term
t2) = Term -> [Name]
names Term
t1 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
t2
names (Proj Term
t Int
_) = Term -> [Name]
names Term
t
names Term
_ = []

occursBinder :: Name -> Binder Term -> Bool
occursBinder :: Name -> Binder Term -> Bool
occursBinder Name
n (Let RigCount
rc Term
ty Term
val) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
val
occursBinder Name
n (NLet Term
ty Term
val) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
val
occursBinder Name
n Binder Term
b = Name -> Term -> Bool
occurs Name
n (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)

namesBinder :: Binder Term -> [Name]
namesBinder :: Binder Term -> [Name]
namesBinder (Let RigCount
rc Term
ty Term
val) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
val
namesBinder (NLet Term
ty Term
val) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
val
namesBinder Binder Term
b = Term -> [Name]
names (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)

occursSC :: Name -> SC -> Bool
occursSC :: Name -> SC -> Bool
occursSC Name
n (Case CaseType
_ Name
_ [CaseAlt' Term]
alts) = (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> CaseAlt' Term -> Bool
occursCaseAlt Name
n) [CaseAlt' Term]
alts
occursSC Name
n (ProjCase Term
t [CaseAlt' Term]
alts) = Name -> Term -> Bool
occurs Name
n Term
t Bool -> Bool -> Bool
|| (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> CaseAlt' Term -> Bool
occursCaseAlt Name
n) [CaseAlt' Term]
alts
occursSC Name
n (STerm Term
t) = Name -> Term -> Bool
occurs Name
n Term
t
occursSC Name
n SC
_ = Bool
False

namesSC :: SC -> [Name]
namesSC :: SC -> [Name]
namesSC (Case CaseType
_ Name
_ [CaseAlt' Term]
alts) = (CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CaseAlt' Term -> [Name]
namesCaseAlt [CaseAlt' Term]
alts
namesSC (ProjCase Term
t [CaseAlt' Term]
alts) = Term -> [Name]
names Term
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CaseAlt' Term -> [Name]
namesCaseAlt [CaseAlt' Term]
alts
namesSC (STerm Term
t) = Term -> [Name]
names Term
t
namesSC SC
_ = []

occursCaseAlt :: Name -> CaseAlt -> Bool
occursCaseAlt :: Name -> CaseAlt' Term -> Bool
occursCaseAlt Name
n (ConCase Name
n' Int
_ [Name]
_ SC
sc) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
|| Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt Name
n (FnCase Name
n' [Name]
_ SC
sc) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
|| Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt Name
n (ConstCase Const
_ SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt Name
n (SucCase Name
_ SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt Name
n (DefaultCase SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc

namesCaseAlt :: CaseAlt -> [Name]
namesCaseAlt :: CaseAlt' Term -> [Name]
namesCaseAlt (ConCase Name
n' Int
_ [Name]
_ SC
sc) = Name
n' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: SC -> [Name]
namesSC SC
sc
namesCaseAlt (FnCase Name
n' [Name]
_ SC
sc) = Name
n' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: SC -> [Name]
namesSC SC
sc
namesCaseAlt (ConstCase Const
_ SC
sc) = SC -> [Name]
namesSC SC
sc
namesCaseAlt (SucCase Name
_ SC
sc) = SC -> [Name]
namesSC SC
sc
namesCaseAlt (DefaultCase SC
sc) = SC -> [Name]
namesSC SC
sc

occursDef :: Name -> Def -> Bool
occursDef :: Name -> Def -> Bool
occursDef Name
n (Function Term
ty Term
tm) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
tm
occursDef Name
n (TyDecl NameType
_ Term
ty) = Name -> Term -> Bool
occurs Name
n Term
ty
occursDef Name
n (Operator Term
ty Int
_ [Value] -> Maybe Value
_) = Name -> Term -> Bool
occurs Name
n Term
ty
occursDef Name
n (CaseOp CaseInfo
_ Term
ty [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
defs) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> SC -> Bool
occursSC Name
n (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
defs))

namesDef :: Def -> [Name]
namesDef :: Def -> [Name]
namesDef (Function Term
ty Term
tm) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
tm
namesDef (TyDecl NameType
_ Term
ty) = Term -> [Name]
names Term
ty
namesDef (Operator Term
ty Int
_ [Value] -> Maybe Value
_) = Term -> [Name]
names Term
ty
namesDef (CaseOp CaseInfo
_ Term
ty [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
defs) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ SC -> [Name]
namesSC (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
defs))

findOccurs :: Name -> Idris [Name]
findOccurs :: Name -> Idris [Name]
findOccurs Name
n = do Context
ctxt <- Idris Context
getContext
                  -- A definition calls a function if the function is in the type or RHS of the definition
                  let defs :: [Name]
defs = (((Name, Def) -> Name) -> [(Name, Def)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Def) -> Name
forall a b. (a, b) -> a
fst ([(Name, Def)] -> [Name])
-> (Context -> [(Name, Def)]) -> Context -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Def) -> Bool) -> [(Name, Def)] -> [(Name, Def)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n', Def
def) -> Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n' Bool -> Bool -> Bool
&& Name -> Def -> Bool
occursDef Name
n Def
def) ([(Name, Def)] -> [(Name, Def)])
-> (Context -> [(Name, Def)]) -> Context -> [(Name, Def)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Name, Def)]
ctxtAlist) Context
ctxt
                  -- A datatype calls its
                  [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name]
defs

whoCalls :: Name -> Idris [(Name, [Name])]
whoCalls :: Name -> Idris [(Name, [Name])]
whoCalls Name
n = do Context
ctxt <- Idris Context
getContext
                let names :: [Name]
names = Name -> Context -> [Name]
lookupNames Name
n Context
ctxt
                    find :: Name -> StateT IState (ExceptT Err IO) (Name, [Name])
find Name
nm = do [Name]
ns <- Name -> Idris [Name]
findOccurs Name
nm
                                 (Name, [Name]) -> StateT IState (ExceptT Err IO) (Name, [Name])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
nm, [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub [Name]
ns)
                (Name -> StateT IState (ExceptT Err IO) (Name, [Name]))
-> [Name] -> Idris [(Name, [Name])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> StateT IState (ExceptT Err IO) (Name, [Name])
find [Name]
names

callsWho :: Name -> Idris [(Name, [Name])]
callsWho :: Name -> Idris [(Name, [Name])]
callsWho Name
n = do Context
ctxt <- Idris Context
getContext
                let defs :: [(Name, Def)]
defs = Name -> Context -> [(Name, Def)]
lookupNameDef Name
n Context
ctxt
                [(Name, [Name])] -> Idris [(Name, [Name])]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, [Name])] -> Idris [(Name, [Name])])
-> [(Name, [Name])] -> Idris [(Name, [Name])]
forall a b. (a -> b) -> a -> b
$ ((Name, Def) -> (Name, [Name]))
-> [(Name, Def)] -> [(Name, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Def
def) -> (Name
n, [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Def -> [Name]
namesDef Def
def)) [(Name, Def)]
defs