{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.TypeChecking.Free
( FreeVars(..)
, VarCounts(..)
, Free
, IsVarSet(..)
, IgnoreSorts(..)
, runFree , rigidVars, relevantVars, allVars
, allFreeVars, allFreeVarsWithOcc
, allRelevantVars, allRelevantVarsIgnoring
, freeIn, freeInIgnoringSorts, isBinderUsed
, relevantIn, relevantInIgnoringSortAnn
, Occurrence(..)
, VarOcc(..)
, occurrence
, closed
, freeVars
, freeVars'
) where
import Prelude hiding (null)
import Control.Monad.Reader
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>), Any(..), All(..) )
import Data.IntSet (IntSet)
import qualified Data.IntSet as Set
import Data.IntMap (IntMap)
import qualified Data.IntMap as Map
import Data.Set (Set)
import Data.Proxy
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
import Agda.Syntax.Internal
import Agda.TypeChecking.Free.Lazy
( Free(..) , FreeEnv(..), initFreeEnv
, VarOcc(..), topVarOcc, TheVarMap, theVarMap, IgnoreSorts(..), Variable, SingleVar
, MetaSet, IsVarSet(..), runFreeM
)
import qualified Agda.TypeChecking.Free.Lazy as Free
import Agda.Utils.Null
import Agda.Utils.Singleton
type VarSet = IntSet
data FreeVars = FV
{ stronglyRigidVars :: VarSet
, unguardedVars :: VarSet
, weaklyRigidVars :: VarSet
, flexibleVars :: IntMap MetaSet
, irrelevantVars :: VarSet
} deriving (Eq, Show)
mapSRV, mapUGV, mapWRV, mapIRV
:: (VarSet -> VarSet) -> FreeVars -> FreeVars
mapSRV f fv = fv { stronglyRigidVars = f $ stronglyRigidVars fv }
mapUGV f fv = fv { unguardedVars = f $ unguardedVars fv }
mapWRV f fv = fv { weaklyRigidVars = f $ weaklyRigidVars fv }
mapIRV f fv = fv { irrelevantVars = f $ irrelevantVars fv }
mapFXV :: (IntMap MetaSet -> IntMap MetaSet) -> FreeVars -> FreeVars
mapFXV f fv = fv { flexibleVars = f $ flexibleVars fv }
rigidVars :: FreeVars -> VarSet
rigidVars fv = Set.unions
[ stronglyRigidVars fv
, unguardedVars fv
, weaklyRigidVars fv
]
relevantVars :: FreeVars -> VarSet
relevantVars fv = Set.unions [rigidVars fv, Map.keysSet (flexibleVars fv)]
allVars :: FreeVars -> VarSet
allVars fv = Set.unions [relevantVars fv, irrelevantVars fv]
data Occurrence
= NoOccurrence
| Irrelevantly
| StronglyRigid
| Unguarded
| WeaklyRigid
| Flexible MetaSet
deriving (Eq,Show)
occurrence :: Free a => Nat -> a -> Occurrence
occurrence x v = occurrenceFV x $ freeVars v
occurrenceFV :: Nat -> FreeVars -> Occurrence
occurrenceFV x fv
| x `Set.member` stronglyRigidVars fv = StronglyRigid
| x `Set.member` unguardedVars fv = Unguarded
| x `Set.member` weaklyRigidVars fv = WeaklyRigid
| Just ms <- Map.lookup x (flexibleVars fv) = Flexible ms
| x `Set.member` irrelevantVars fv = Irrelevantly
| otherwise = NoOccurrence
flexible :: MetaSet -> FreeVars -> FreeVars
flexible ms fv =
fv { stronglyRigidVars = Set.empty
, unguardedVars = Set.empty
, weaklyRigidVars = Set.empty
, flexibleVars = Map.unionsWith mappend
[ Map.fromSet (const ms) (rigidVars fv)
, fmap (mappend ms) (flexibleVars fv) ]
}
weakly :: FreeVars -> FreeVars
weakly fv = fv
{ stronglyRigidVars = Set.empty
, unguardedVars = Set.empty
, weaklyRigidVars = rigidVars fv
}
strongly :: FreeVars -> FreeVars
strongly fv = fv
{ stronglyRigidVars = stronglyRigidVars fv `Set.union` unguardedVars fv
, unguardedVars = Set.empty
}
underConstructor :: ConHead -> FreeVars -> FreeVars
underConstructor (ConHead c i fs) =
case (i,fs) of
(CoInductive, _) -> weakly
(Inductive, []) -> strongly
(Inductive, (_:_)) -> id
irrelevantly :: FreeVars -> FreeVars
irrelevantly fv = empty { irrelevantVars = allVars fv }
union :: FreeVars -> FreeVars -> FreeVars
union (FV sv1 gv1 rv1 fv1 iv1) (FV sv2 gv2 rv2 fv2 iv2) =
FV (Set.union sv1 sv2) (Set.union gv1 gv2) (Set.union rv1 rv2) (Map.unionWith mappend fv1 fv2) (Set.union iv1 iv2)
unions :: [FreeVars] -> FreeVars
unions = foldr union empty
instance Null FreeVars where
empty = FV Set.empty Set.empty Set.empty Map.empty Set.empty
null (FV a b c d e) = null a && null b && null c && null d && null e
instance Semigroup FreeVars where
(<>) = union
instance Monoid FreeVars where
mempty = empty
mappend = (<>)
mconcat = unions
delete :: Nat -> FreeVars -> FreeVars
delete n (FV sv gv rv fv iv) = FV (Set.delete n sv) (Set.delete n gv) (Set.delete n rv) (Map.delete n fv) (Set.delete n iv)
instance Singleton Variable FreeVars where
singleton i = mapUGV (Set.insert i) mempty
instance IsVarSet FreeVars where
withVarOcc (VarOcc o r) = goOcc o . goRel r
where
goOcc o = case o of
Free.Flexible ms -> flexible ms
Free.WeaklyRigid -> weakly
Free.Unguarded -> id
Free.StronglyRigid -> strongly
goRel r = case r of
Relevant -> id
NonStrict -> id
Irrelevant -> irrelevantly
instance IsVarSet VarSet where withVarOcc _ = id
instance IsVarSet [Int] where withVarOcc _ = id
instance IsVarSet Any where withVarOcc _ = id
instance IsVarSet All where withVarOcc _ = id
newtype VarCounts = VarCounts { varCounts :: IntMap Int }
instance Semigroup VarCounts where
VarCounts fv1 <> VarCounts fv2 = VarCounts (Map.unionWith (+) fv1 fv2)
instance Monoid VarCounts where
mempty = VarCounts Map.empty
mappend = (<>)
instance IsVarSet VarCounts where withVarOcc _ = id
instance Singleton Variable VarCounts where
singleton i = VarCounts $ Map.singleton i 1
bench :: a -> a
bench = Bench.billToPure [ Bench.Typing , Bench.Free ]
{-# SPECIALIZE freeVars :: Free a => a -> FreeVars #-}
freeVars :: (IsVarSet c, Singleton Variable c, Free a) => a -> c
freeVars = freeVarsIgnore IgnoreNot
{-# SPECIALIZE freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars #-}
freeVarsIgnore :: (IsVarSet c, Singleton Variable c, Free a) =>
IgnoreSorts -> a -> c
freeVarsIgnore = runFree singleton
{-# SPECIALIZE runFree :: Free a => SingleVar Any -> IgnoreSorts -> a -> Any #-}
{-# SPECIALIZE runFree :: Free a => SingleVar FreeVars -> IgnoreSorts -> a -> FreeVars #-}
{-# SPECIALIZE runFree :: SingleVar Any -> IgnoreSorts -> Term -> Any #-}
{-# SPECIALIZE runFree :: SingleVar FreeVars -> IgnoreSorts -> Term -> FreeVars #-}
runFree :: (IsVarSet c, Free a) => SingleVar c -> IgnoreSorts -> a -> c
runFree single i t =
runFreeM single i (freeVars' t)
freeIn' :: Free a => IgnoreSorts -> Nat -> a -> Bool
freeIn' ig x t = getAny $ runFree (Any . (x ==)) ig t
{-# SPECIALIZE freeIn :: Nat -> Term -> Bool #-}
freeIn :: Free a => Nat -> a -> Bool
freeIn = freeIn' IgnoreNot
freeInIgnoringSorts :: Free a => Nat -> a -> Bool
freeInIgnoringSorts = freeIn' IgnoreAll
freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool
freeInIgnoringSortAnn = freeIn' IgnoreInAnnotations
newtype RelevantIn a = RelevantIn {getRelevantIn :: a}
deriving (Semigroup, Monoid)
instance IsVarSet a => IsVarSet (RelevantIn a) where
withVarOcc o x
| isIrrelevant (varRelevance o) = mempty
| otherwise = RelevantIn $ withVarOcc o $ getRelevantIn x
relevantIn' :: Free a => IgnoreSorts -> Nat -> a -> Bool
relevantIn' ig x t = getAny . getRelevantIn $ runFree (RelevantIn . Any . (x ==)) ig t
relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
relevantInIgnoringSortAnn = relevantIn' IgnoreInAnnotations
relevantIn :: Free a => Nat -> a -> Bool
relevantIn = relevantIn' IgnoreAll
isBinderUsed :: Free a => Abs a -> Bool
isBinderUsed NoAbs{} = False
isBinderUsed (Abs _ x) = 0 `freeIn` x
closed :: Free a => a -> Bool
closed t = getAll $ runFree (const $ All False) IgnoreNot t
allFreeVars :: Free a => a -> VarSet
allFreeVars = runFree Set.singleton IgnoreNot
allFreeVarsWithOcc :: Free a => a -> TheVarMap
allFreeVarsWithOcc = theVarMap . runFree (singleton . (,topVarOcc)) IgnoreNot
allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> VarSet
allRelevantVarsIgnoring ig = getRelevantIn . runFree (RelevantIn . Set.singleton) ig
allRelevantVars :: Free a => a -> VarSet
allRelevantVars = allRelevantVarsIgnoring IgnoreNot