{-|
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 n :: Name
n (P Bound _ _) = Bool
False
occurs n :: Name
n (P _ n' :: Name
n' _) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
occurs n :: Name
n (Bind _ b :: Binder Term
b sc :: Term
sc) = Name -> Binder Term -> Bool
occursBinder Name
n Binder Term
b Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
sc
occurs n :: Name
n (App _ t1 :: Term
t1 t2 :: Term
t2) = Name -> Term -> Bool
occurs Name
n Term
t1 Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
t2
occurs n :: Name
n (Proj t :: Term
t _) = Name -> Term -> Bool
occurs Name
n Term
t
occurs n :: Name
n _ = Bool
False

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

occursBinder :: Name -> Binder Term -> Bool
occursBinder :: Name -> Binder Term -> Bool
occursBinder n :: Name
n (Let rc :: RigCount
rc ty :: Term
ty val :: Term
val) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
val
occursBinder n :: Name
n (NLet ty :: Term
ty val :: Term
val) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
val
occursBinder n :: Name
n b :: 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 rc :: RigCount
rc ty :: Term
ty val :: Term
val) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
val
namesBinder (NLet ty :: Term
ty val :: Term
val) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
val
namesBinder b :: 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 n :: Name
n (Case _ _ alts :: [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 n :: Name
n (ProjCase t :: Term
t alts :: [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 n :: Name
n (STerm t :: Term
t) = Name -> Term -> Bool
occurs Name
n Term
t
occursSC n :: Name
n _ = Bool
False

namesSC :: SC -> [Name]
namesSC :: SC -> [Name]
namesSC (Case _ _ alts :: [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 t :: Term
t alts :: [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 t :: Term
t) = Term -> [Name]
names Term
t
namesSC _ = []

occursCaseAlt :: Name -> CaseAlt -> Bool
occursCaseAlt :: Name -> CaseAlt' Term -> Bool
occursCaseAlt n :: Name
n (ConCase n' :: Name
n' _ _ sc :: 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 n :: Name
n (FnCase n' :: Name
n' _ sc :: 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 n :: Name
n (ConstCase _ sc :: SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt n :: Name
n (SucCase _ sc :: SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc
occursCaseAlt n :: Name
n (DefaultCase sc :: SC
sc) = Name -> SC -> Bool
occursSC Name
n SC
sc

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

occursDef :: Name -> Def -> Bool
occursDef :: Name -> Def -> Bool
occursDef n :: Name
n (Function ty :: Term
ty tm :: Term
tm) = Name -> Term -> Bool
occurs Name
n Term
ty Bool -> Bool -> Bool
|| Name -> Term -> Bool
occurs Name
n Term
tm
occursDef n :: Name
n (TyDecl _ ty :: Term
ty) = Name -> Term -> Bool
occurs Name
n Term
ty
occursDef n :: Name
n (Operator ty :: Term
ty _ _) = Name -> Term -> Bool
occurs Name
n Term
ty
occursDef n :: Name
n (CaseOp _ ty :: Term
ty _ _ _ defs :: 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 ty :: Term
ty tm :: Term
tm) = Term -> [Name]
names Term
ty [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
names Term
tm
namesDef (TyDecl _ ty :: Term
ty) = Term -> [Name]
names Term
ty
namesDef (Operator ty :: Term
ty _ _) = Term -> [Name]
names Term
ty
namesDef (CaseOp _ ty :: Term
ty _ _ _ defs :: 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 n :: 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 (\(n' :: Name
n', def :: 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 (m :: * -> *) a. Monad m => a -> m a
return [Name]
defs

whoCalls :: Name -> Idris [(Name, [Name])]
whoCalls :: Name -> Idris [(Name, [Name])]
whoCalls n :: 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 nm :: Name
nm = do [Name]
ns <- Name -> Idris [Name]
findOccurs Name
nm
                                 (Name, [Name]) -> StateT IState (ExceptT Err IO) (Name, [Name])
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)
mapM Name -> StateT IState (ExceptT Err IO) (Name, [Name])
find [Name]
names

callsWho :: Name -> Idris [(Name, [Name])]
callsWho :: Name -> Idris [(Name, [Name])]
callsWho n :: 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 (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 (\ (n :: Name
n, def :: 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