module Agda.Termination.RecCheck
( recursive
, anyDefs
)
where
import Control.Monad (forM, forM_)
import Data.Graph
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Defs
import Agda.TypeChecking.Monad
import Agda.Utils.List (hasElem)
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Impossible
type NamesPerClause = IntMap (Set QName)
recursive :: [QName] -> TCM [[QName]]
recursive :: [QName] -> TCM [[QName]]
recursive [QName]
names = do
([IntMap (Set QName)]
perClauses, [Set QName]
nss) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((QName -> Bool) -> QName -> TCM (IntMap (Set QName), Set QName)
recDef ([QName]
names forall a. Ord a => [a] -> a -> Bool
`hasElem`)) [QName]
names
let graph :: [(QName, QName, [QName])]
graph = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ QName
x Set QName
ns -> (QName
x, QName
x, forall a. Set a -> [a]
Set.toList Set QName
ns)) [QName]
names [Set QName]
nss
let sccs :: [SCC QName]
sccs = forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [(QName, QName, [QName])]
graph
let nonRec :: [QName]
nonRec = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case{ AcyclicSCC QName
x -> forall a. a -> Maybe a
Just QName
x ; SCC QName
_ -> forall a. Maybe a
Nothing}) [SCC QName]
sccs
let recs :: [[QName]]
recs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case{ CyclicSCC [QName]
xs -> forall a. a -> Maybe a
Just [QName]
xs; SCC QName
_ -> forall a. Maybe a
Nothing}) [SCC QName]
sccs
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Key -> [Char] -> m ()
reportSLn [Char]
"rec.graph" Key
60 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show [(QName, QName, [QName])]
graph
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCMT IO ()
markNonRecursive [QName]
nonRec
let clMap :: Map QName (IntMap (Set QName))
clMap = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [QName]
names [IntMap (Set QName)]
perClauses
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[QName]]
recs forall a b. (a -> b) -> a -> b
$ \ [QName]
scc -> do
let overlap :: Set QName -> Bool
overlap Set QName
s = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
s) [QName]
scc
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
scc forall a b. (a -> b) -> a -> b
$ \ QName
x -> do
let perClause :: IntMap (Set QName)
perClause = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ QName
x Map QName (IntMap (Set QName))
clMap
let recClause :: Key -> Bool
recClause Key
i = Set QName -> Bool
overlap forall a b. (a -> b) -> a -> b
$ forall a. a -> Key -> IntMap a -> a
IntMap.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Key
i IntMap (Set QName)
perClause
(Key -> Bool) -> QName -> TCMT IO ()
markRecursive Key -> Bool
recClause QName
x
forall (m :: * -> *) a. Monad m => a -> m a
return [[QName]]
recs
markNonRecursive :: QName -> TCM ()
markNonRecursive :: QName -> TCMT IO ()
markNonRecursive QName
q = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
def :: Defn
def@Function{} -> Defn
def
{ funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True
, funClauses :: [Clause]
funClauses = forall a b. (a -> b) -> [a] -> [b]
map (\ Clause
cl -> Clause
cl { clauseRecursive :: Maybe Bool
clauseRecursive = forall a. a -> Maybe a
Just Bool
False }) forall a b. (a -> b) -> a -> b
$ Defn -> [Clause]
funClauses Defn
def
}
Defn
def -> Defn
def
markRecursive
:: (Int -> Bool)
-> QName -> TCM ()
markRecursive :: (Key -> Bool) -> QName -> TCMT IO ()
markRecursive Key -> Bool
f QName
q = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
def :: Defn
def@Function{} -> Defn
def
{ funClauses :: [Clause]
funClauses = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Key
i Clause
cl -> Clause
cl { clauseRecursive :: Maybe Bool
clauseRecursive = forall a. a -> Maybe a
Just (Key -> Bool
f Key
i) }) [Key
0..] forall a b. (a -> b) -> a -> b
$ Defn -> [Clause]
funClauses Defn
def
}
Defn
def -> Defn
def
recDef :: (QName -> Bool) -> QName -> TCM (NamesPerClause, Set QName)
recDef :: (QName -> Bool) -> QName -> TCM (IntMap (Set QName), Set QName)
recDef QName -> Bool
include QName
name = do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
Set QName
ns1 <- forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs QName -> Bool
include (Definition -> Type
defType Definition
def)
(IntMap (Set QName)
perClause, Set QName
ns2) <- case Definition -> Defn
theDef Definition
def of
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls } -> do
[(Key, Set QName)]
perClause <- do
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Key
0..] [Clause]
cls) forall a b. (a -> b) -> a -> b
$ \ (Key
i, Clause
cl) ->
(Key
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs QName -> Bool
include Clause
cl
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [(Key, a)] -> IntMap a
IntMap.fromList [(Key, Set QName)]
perClause, forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Key, Set QName)]
perClause)
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty)
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Key -> a -> m ()
reportS [Char]
"rec.graph" Key
20
[ [Char]
"recDef " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
name
, [Char]
" names in the type: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
ns1
, [Char]
" names in the def: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Set QName
ns2
]
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap (Set QName)
perClause, Set QName
ns1 forall a. Monoid a => a -> a -> a
`mappend` Set QName
ns2)
anyDefs :: GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs :: forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
anyDefs QName -> Bool
include a
a = do
MetaStore
st <- forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
let lookup :: MetaId -> Maybe Term
lookup (MetaId Key
x) = (MetaVariable -> MetaInstantiation
mvInstantiation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
x MetaStore
st) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
InstV [Arg [Char]]
_ Term
v -> forall a. a -> Maybe a
Just Term
v
MetaInstantiation
Open -> forall a. Maybe a
Nothing
MetaInstantiation
OpenInstance -> forall a. Maybe a
Nothing
BlockedConst{} -> forall a. Maybe a
Nothing
PostponedTypeCheckingProblem{} -> forall a. Maybe a
Nothing
emb :: QName -> Set QName
emb QName
d = if QName -> Bool
include QName
d then forall a. a -> Set a
Set.singleton QName
d else forall a. Set a
Set.empty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b.
(GetDefs a, Monoid b) =>
(MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' MetaId -> Maybe Term
lookup QName -> Set QName
emb a
a