{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Free
( VarCounts(..)
, Free
, IsVarSet(..)
, IgnoreSorts(..)
, freeVars, freeVars', filterVarMap, filterVarMapToList
, runFree, rigidVars, stronglyRigidVars, unguardedVars, allVars
, allFreeVars
, allRelevantVars, allRelevantVarsIgnoring
, freeIn, freeInIgnoringSorts, isBinderUsed
, relevantIn, relevantInIgnoringSortAnn
, FlexRig'(..), FlexRig
, LensFlexRig(..), isFlexible, isUnguarded, isStronglyRigid, isWeaklyRigid
, VarOcc'(..), VarOcc
, varOccurrenceIn
, flexRigOccurrenceIn
, closed
, MetaSet
, insertMetaSet, foldrMetaSet
) where
import Prelude hiding (null)
import Data.Monoid ( Monoid, mempty, mappend)
import Data.Semigroup ( Semigroup, (<>), Any(..), All(..) )
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common hiding (Arg, NamedArg)
import Agda.Syntax.Internal
import Agda.TypeChecking.Free.Lazy
import Agda.Utils.Singleton
type VarSet = IntSet
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 (IntMap.unionWith (+) fv1 fv2)
instance Monoid VarCounts where
mempty = VarCounts IntMap.empty
mappend = (<>)
instance IsVarSet () VarCounts where
withVarOcc _ = id
instance Singleton Variable VarCounts where
singleton i = VarCounts $ IntMap.singleton i 1
{-# SPECIALIZE freeVars :: Free a => a -> VarMap #-}
freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c
freeVars = freeVarsIgnore IgnoreNot
freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore = runFree singleton
{-# SPECIALIZE runFree :: Free a => SingleVar Any -> IgnoreSorts -> a -> Any #-}
{-# SPECIALIZE runFree :: SingleVar Any -> IgnoreSorts -> Term -> Any #-}
runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c
runFree single i t =
runFreeM single i (freeVars' t)
where
bench = Bench.billToPure [ Bench.Typing , Bench.Free ]
varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc
varOccurrenceIn = varOccurrenceIn' IgnoreNot
varOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe VarOcc
varOccurrenceIn' ig x t = theSingleVarOcc $ runFree sg ig t
where
sg y = if x == y then oneSingleVarOcc else mempty
newtype SingleVarOcc = SingleVarOcc { theSingleVarOcc :: Maybe VarOcc }
oneSingleVarOcc :: SingleVarOcc
oneSingleVarOcc = SingleVarOcc $ Just $ oneVarOcc
instance Semigroup SingleVarOcc where
SingleVarOcc Nothing <> s = s
s <> SingleVarOcc Nothing = s
SingleVarOcc (Just o) <> SingleVarOcc (Just o') = SingleVarOcc $ Just $ o <> o'
instance Monoid SingleVarOcc where
mempty = SingleVarOcc Nothing
mappend = (<>)
instance IsVarSet MetaSet SingleVarOcc where
withVarOcc o = SingleVarOcc . fmap (composeVarOcc o) . theSingleVarOcc
flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn = flexRigOccurrenceIn' IgnoreNot
flexRigOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn' ig x t = theSingleFlexRig $ runFree sg ig t
where
sg y = if x == y then oneSingleFlexRig else mempty
newtype SingleFlexRig = SingleFlexRig { theSingleFlexRig :: Maybe (FlexRig' ()) }
oneSingleFlexRig :: SingleFlexRig
oneSingleFlexRig = SingleFlexRig $ Just $ oneFlexRig
instance Semigroup SingleFlexRig where
SingleFlexRig Nothing <> s = s
s <> SingleFlexRig Nothing = s
SingleFlexRig (Just o) <> SingleFlexRig (Just o') = SingleFlexRig $ Just $ addFlexRig o o'
instance Monoid SingleFlexRig where
mempty = SingleFlexRig Nothing
mappend = (<>)
instance IsVarSet () SingleFlexRig where
withVarOcc o = SingleFlexRig . fmap (composeFlexRig $ () <$ varFlexRig o) . theSingleFlexRig
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
isBinderUsed :: Free a => Abs a -> Bool
isBinderUsed NoAbs{} = False
isBinderUsed (Abs _ x) = 0 `freeIn` x
newtype RelevantIn c = RelevantIn {getRelevantIn :: c}
deriving (Semigroup, Monoid)
instance IsVarSet a c => IsVarSet a (RelevantIn c) where
withVarOcc o x
| isIrrelevant o = mempty
| otherwise = RelevantIn $ withVarOcc o $ getRelevantIn x
relevantIn' :: Free t => IgnoreSorts -> Nat -> t -> Bool
relevantIn' ig x t = getAny . getRelevantIn $ runFree (RelevantIn . Any . (x ==)) ig t
relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool
relevantInIgnoringSortAnn = relevantIn' IgnoreInAnnotations
relevantIn :: Free t => Nat -> t -> Bool
relevantIn = relevantIn' IgnoreAll
closed :: Free t => t -> Bool
closed t = getAll $ runFree (const $ All False) IgnoreNot t
allFreeVars :: Free t => t -> VarSet
allFreeVars = runFree IntSet.singleton IgnoreNot
allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring ig = getRelevantIn . runFree (RelevantIn . IntSet.singleton) ig
allRelevantVars :: Free t => t -> VarSet
allRelevantVars = allRelevantVarsIgnoring IgnoreNot
filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap f = IntMap.keysSet . IntMap.filter f . theVarMap
filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Variable]
filterVarMapToList f = map fst . filter (f . snd) . IntMap.toList . theVarMap
stronglyRigidVars :: VarMap -> VarSet
stronglyRigidVars = filterVarMap $ \case
VarOcc StronglyRigid _ -> True
_ -> False
unguardedVars :: VarMap -> VarSet
unguardedVars = filterVarMap $ \case
VarOcc Unguarded _ -> True
_ -> False
rigidVars :: VarMap -> VarSet
rigidVars = filterVarMap $ \case
VarOcc o _ -> o `elem` [ WeaklyRigid, Unguarded, StronglyRigid ]
allVars :: VarMap -> VarSet
allVars = IntMap.keysSet . theVarMap