module Agda.TypeChecking.Free.Old
( 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 ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>) )
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as Set
data FreeVars = FV
{ stronglyRigidVars :: VarSet
, unguardedVars :: VarSet
, weaklyRigidVars :: VarSet
, flexibleVars :: VarSet
, irrelevantVars :: VarSet
} deriving (Eq, Show)
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]
data Occurrence
= NoOccurrence
| Irrelevantly
| StronglyRigid
| Unguarded
| WeaklyRigid
| Flexible
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
| 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 }
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) (Set.union fv1 fv2) (Set.union iv1 iv2)
unions :: [FreeVars] -> FreeVars
unions = foldr union empty
empty :: FreeVars
empty = FV Set.empty Set.empty Set.empty Set.empty Set.empty
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) (Set.delete n fv) (Set.delete n iv)
subtractFV :: Nat -> FreeVars -> FreeVars
subtractFV n (FV sv gv rv fv iv) = FV (Set.subtract n sv) (Set.subtract n gv) (Set.subtract n rv) (Set.subtract n fv) (Set.subtract n iv)
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 Semigroup FreeT where
(<>) = liftA2 mappend
instance Monoid FreeT where
mempty = pure mempty
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 = bind' 1
bind' :: Nat -> FreeT -> FreeT
bind' n = local $ \ e -> e { fcContext = n + 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
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
SizeUniv -> mempty
PiSort s1 s2 -> weakly <$> freeVars' (s1, s2)
UnivSort s -> weakly <$> freeVars' s
MetaS x es -> flexible <$> freeVars' es
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
_ -> 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 Clause where
freeVars' cl = bind' (size $ clauseTel cl) $ freeVars' $ clauseBody cl
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