module Agda.TypeChecking.Free
( FreeVars(..)
, Free
, IgnoreSorts(..)
, freeVars
, freeVarsIgnore
, allVars
, relevantVars
, rigidVars
, freeIn, isBinderUsed
, freeInIgnoringSorts, freeInIgnoringSortAnn
, relevantIn, relevantInIgnoringSortAnn
, Occurrence(..)
, occurrence
) where
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Data.Foldable (foldMap)
import Data.Monoid
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
import Agda.Syntax.Internal
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as Set
#include "undefined.h"
import Agda.Utils.Impossible
data FreeVars = FV
{ stronglyRigidVars :: VarSet
, unguardedVars :: VarSet
, weaklyRigidVars :: VarSet
, flexibleVars :: VarSet
, irrelevantVars :: VarSet
, unusedVars :: VarSet
}
rigidVars :: FreeVars -> VarSet
rigidVars fv = Set.unions
[ stronglyRigidVars fv
, unguardedVars fv
, weaklyRigidVars fv
]
relevantVars :: FreeVars -> VarSet
relevantVars fv = Set.unions [rigidVars fv, flexibleVars fv]
allVars :: FreeVars -> VarSet
allVars fv = Set.unions [relevantVars fv, irrelevantVars fv, unusedVars fv]
data Occurrence
= NoOccurrence
| Irrelevantly
| StronglyRigid
| Unguarded
| WeaklyRigid
| Flexible
| Unused
deriving (Eq,Show)
occurrence :: Nat -> FreeVars -> Occurrence
occurrence x fv
| x `Set.member` stronglyRigidVars fv = StronglyRigid
| x `Set.member` unguardedVars fv = Unguarded
| x `Set.member` weaklyRigidVars fv = WeaklyRigid
| x `Set.member` flexibleVars fv = Flexible
| x `Set.member` irrelevantVars fv = Irrelevantly
| x `Set.member` unusedVars fv = Unused
| otherwise = NoOccurrence
flexible :: FreeVars -> FreeVars
flexible fv =
fv { stronglyRigidVars = Set.empty
, unguardedVars = Set.empty
, weaklyRigidVars = Set.empty
, flexibleVars = relevantVars 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 }
unused :: FreeVars -> FreeVars
unused fv = empty
{ irrelevantVars = irrelevantVars fv
, unusedVars = Set.unions [ rigidVars fv, flexibleVars fv, unusedVars fv ]
}
union :: FreeVars -> FreeVars -> FreeVars
union (FV sv1 gv1 rv1 fv1 iv1 uv1) (FV sv2 gv2 rv2 fv2 iv2 uv2) =
FV (Set.union sv1 sv2) (Set.union gv1 gv2) (Set.union rv1 rv2) (Set.union fv1 fv2) (Set.union iv1 iv2) (Set.union uv1 uv2)
unions :: [FreeVars] -> FreeVars
unions = foldr union empty
empty :: FreeVars
empty = FV Set.empty Set.empty Set.empty Set.empty Set.empty Set.empty
instance Monoid FreeVars where
mempty = empty
mappend = union
mconcat = unions
delete :: Nat -> FreeVars -> FreeVars
delete n (FV sv gv rv fv iv uv) = FV (Set.delete n sv) (Set.delete n gv) (Set.delete n rv) (Set.delete n fv) (Set.delete n iv) (Set.delete n uv)
subtractFV :: Nat -> FreeVars -> FreeVars
subtractFV n (FV sv gv rv fv iv uv) = FV (Set.subtract n sv) (Set.subtract n gv) (Set.subtract n rv) (Set.subtract n fv) (Set.subtract n iv) (Set.subtract n uv)
singleton :: Nat -> FreeVars
singleton x = empty { unguardedVars = Set.singleton x }
data IgnoreSorts
= IgnoreNot
| IgnoreInAnnotations
| IgnoreAll
deriving (Eq, Show)
data FreeConf = FreeConf
{ fcIgnoreSorts :: !IgnoreSorts
, fcContext :: !Int
}
initFreeConf :: FreeConf
initFreeConf = FreeConf
{ fcIgnoreSorts = IgnoreNot
, fcContext = 0
}
freeVars :: Free a => a -> FreeVars
freeVars t = freeVars' t `runReader` initFreeConf
freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars
freeVarsIgnore i t = freeVars' t `runReader` initFreeConf{ fcIgnoreSorts = i }
type FreeT = Reader FreeConf FreeVars
instance Monoid FreeT where
mempty = pure mempty
mappend = liftA2 mappend
mconcat = mconcat <.> sequence
variable :: Int -> FreeT
variable n = do
m <- (n ) <$> asks fcContext
if m >= 0 then pure $ singleton m else mempty
bind :: FreeT -> FreeT
bind = local $ \ e -> e { fcContext = 1 + fcContext e }
class Free a where
freeVars' :: a -> FreeT
instance Free Term where
freeVars' t = case t of
Var n ts -> variable n `mappend` do weakly <$> freeVars' ts
Lam _ t -> freeVars' t
Lit _ -> mempty
Def _ ts -> weakly <$> freeVars' ts
Con c ts -> underConstructor c <$> freeVars' ts
Pi a b -> freeVars' (a,b)
Sort s -> freeVars' s
Level l -> freeVars' l
MetaV _ ts -> flexible <$> freeVars' ts
DontCare mt -> irrelevantly <$> freeVars' mt
Shared p -> freeVars' (derefPtr p)
ExtLam cs ts -> freeVars' (cs, ts)
instance Free Type where
freeVars' (El s t) =
ifM ((IgnoreNot ==) <$> asks fcIgnoreSorts)
(freeVars' (s, t))
(freeVars' t)
instance Free Sort where
freeVars' s =
ifM ((IgnoreAll ==) <$> asks fcIgnoreSorts) mempty $
case s of
Type a -> freeVars' a
Prop -> mempty
Inf -> mempty
DLub s1 s2 -> weakly <$> freeVars' (s1, s2)
instance Free Level where
freeVars' (Max as) = freeVars' as
instance Free PlusLevel where
freeVars' ClosedLevel{} = mempty
freeVars' (Plus _ l) = freeVars' l
instance Free LevelAtom where
freeVars' l = case l of
MetaLevel _ vs -> flexible <$> freeVars' vs
NeutralLevel v -> freeVars' v
BlockedLevel _ v -> freeVars' v
UnreducedLevel v -> freeVars' v
instance Free a => Free [a] where
freeVars' = foldMap freeVars'
instance Free a => Free (Maybe a) where
freeVars' = foldMap freeVars'
instance (Free a, Free b) => Free (a,b) where
freeVars' (x,y) = freeVars' x `mappend` freeVars' y
instance Free a => Free (Elim' a) where
freeVars' (Apply a) = freeVars' a
freeVars' (Proj{} ) = mempty
instance Free a => Free (Arg a) where
freeVars' a = f <$> freeVars' (unArg a)
where f = case getRelevance a of
Irrelevant -> irrelevantly
UnusedArg -> unused
_ -> id
instance Free a => Free (Dom a) where
freeVars' = freeVars' . unDom
instance Free a => Free (Abs a) where
freeVars' (Abs _ b) = bind $ freeVars' b
freeVars' (NoAbs _ b) = freeVars' b
instance Free a => Free (Tele a) where
freeVars' EmptyTel = mempty
freeVars' (ExtendTel a tel) = freeVars' (a, tel)
instance Free ClauseBody where
freeVars' (Body t) = freeVars' t
freeVars' (Bind b) = freeVars' b
freeVars' NoBody = mempty
instance Free Clause where
freeVars' = freeVars' . clauseBody
freeIn :: Free a => Nat -> a -> Bool
freeIn v t = v `Set.member` allVars (freeVars t)
freeInIgnoringSorts :: Free a => Nat -> a -> Bool
freeInIgnoringSorts v t =
v `Set.member` allVars (freeVarsIgnore IgnoreAll t)
freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool
freeInIgnoringSortAnn v t =
v `Set.member` allVars (freeVarsIgnore IgnoreInAnnotations t)
relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
relevantInIgnoringSortAnn v t =
v `Set.member` relevantVars (freeVarsIgnore IgnoreInAnnotations t)
relevantIn :: Free a => Nat -> a -> Bool
relevantIn v t = v `Set.member` relevantVars (freeVarsIgnore IgnoreAll t)
isBinderUsed :: Free a => Abs a -> Bool
isBinderUsed NoAbs{} = False
isBinderUsed (Abs _ x) = 0 `freeIn` x