{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Free.Lazy where
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Data.Foldable (foldMap)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Monoid ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>) )
import Data.Set (Set)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Singleton
import Agda.Utils.Size
type MetaSet = Set MetaId
data FlexRig
= Flexible MetaSet
| WeaklyRigid
| Unguarded
| StronglyRigid
deriving (Eq, Ord, Show)
composeFlexRig :: FlexRig -> FlexRig -> FlexRig
composeFlexRig o o' =
case (o, o') of
(Flexible ms1, Flexible ms2) -> Flexible $ ms1 `mappend` ms2
(Flexible ms1, _) -> Flexible ms1
(_, Flexible ms2) -> Flexible ms2
(WeaklyRigid, _) -> WeaklyRigid
(_, WeaklyRigid) -> WeaklyRigid
(StronglyRigid, _) -> StronglyRigid
(_, StronglyRigid) -> StronglyRigid
(Unguarded, Unguarded) -> Unguarded
data VarOcc = VarOcc
{ varFlexRig :: FlexRig
, varRelevance :: Relevance
}
deriving (Eq, Show)
maxVarOcc :: VarOcc -> VarOcc -> VarOcc
maxVarOcc (VarOcc o r) (VarOcc o' r') = VarOcc (max o o') (min r r')
topVarOcc :: VarOcc
topVarOcc = VarOcc StronglyRigid Relevant
botVarOcc :: VarOcc
botVarOcc = VarOcc (Flexible mempty) Irrelevant
composeVarOcc :: VarOcc -> VarOcc -> VarOcc
composeVarOcc (VarOcc o r) (VarOcc o' r') = VarOcc (composeFlexRig o o') (max r r')
instance LensRelevance VarOcc where
getRelevance = varRelevance
setRelevance rel (VarOcc x _) = VarOcc x rel
class (Semigroup a, Monoid a) => IsVarSet a where
withVarOcc :: VarOcc -> a -> a
type TheVarMap = IntMap VarOcc
newtype VarMap = VarMap { theVarMap :: TheVarMap }
deriving (Show, Singleton (Variable, VarOcc))
mapVarMap :: (TheVarMap -> TheVarMap) -> VarMap -> VarMap
mapVarMap f = VarMap . f . theVarMap
instance Semigroup VarMap where
VarMap m <> VarMap m' = VarMap $ IntMap.unionWith maxVarOcc m m'
instance Monoid VarMap where
mempty = VarMap IntMap.empty
mappend = (<>)
mconcat = VarMap . IntMap.unionsWith maxVarOcc . map theVarMap
instance IsVarSet VarMap where
withVarOcc o = mapVarMap $ fmap $ composeVarOcc o
data IgnoreSorts
= IgnoreNot
| IgnoreInAnnotations
| IgnoreAll
deriving (Eq, Show)
data FreeEnv c = FreeEnv
{ feIgnoreSorts :: !IgnoreSorts
, feFlexRig :: !FlexRig
, feRelevance :: !Relevance
, feSingleton :: Maybe Variable -> c
}
type Variable = Int
type SingleVar c = Variable -> c
initFreeEnv :: Monoid c => SingleVar c -> FreeEnv c
initFreeEnv sing = FreeEnv
{ feIgnoreSorts = IgnoreNot
, feFlexRig = Unguarded
, feRelevance = Relevant
, feSingleton = maybe mempty sing
}
type FreeM c = Reader (FreeEnv c) c
runFreeM :: IsVarSet c => SingleVar c -> IgnoreSorts -> FreeM c -> c
runFreeM single i m = runReader m $ (initFreeEnv single) { feIgnoreSorts = i }
instance Semigroup c => Semigroup (FreeM c) where
(<>) = liftA2 (<>)
instance (Semigroup c, Monoid c) => Monoid (FreeM c) where
mempty = pure mempty
mappend = (<>)
mconcat = mconcat <.> sequence
variable :: IsVarSet c => Int -> FreeM c
variable n = do
o <- asks feFlexRig
r <- asks feRelevance
s <- asks feSingleton
pure $ withVarOcc (VarOcc o r) (s $ Just n)
subVar :: Int -> Maybe Variable -> Maybe Variable
subVar n x = x >>= \ i -> (i - n) <$ guard (n <= i)
bind :: FreeM a -> FreeM a
bind = bind' 1
bind' :: Nat -> FreeM a -> FreeM a
bind' n = local $ \ e -> e { feSingleton = feSingleton e . subVar n }
go :: FlexRig -> FreeM a -> FreeM a
go o = local $ \ e -> e { feFlexRig = composeFlexRig o $ feFlexRig e }
goRel :: Relevance-> FreeM a -> FreeM a
goRel r = local $ \ e -> e { feRelevance = composeRelevance r $ feRelevance e }
underConstructor :: ConHead -> FreeM a -> FreeM a
underConstructor (ConHead c i fs) =
case (i,fs) of
(CoInductive, _) -> go WeaklyRigid
(Inductive, []) -> go StronglyRigid
(Inductive, (_:_)) -> id
class Free a where
freeVars' :: IsVarSet c => a -> FreeM c
instance Free Term where
freeVars' t = case t of
Var n ts -> variable n `mappend` do go WeaklyRigid $ freeVars' ts
Lam _ t -> freeVars' t
Lit _ -> mempty
Def _ ts -> go WeaklyRigid $ freeVars' ts
Con c _ ts -> underConstructor c $ freeVars' ts
Pi a b -> freeVars' (a,b)
Sort s -> freeVars' s
Level l -> freeVars' l
MetaV m ts -> go (Flexible $ singleton m) $ freeVars' ts
DontCare mt -> goRel Irrelevant $ freeVars' mt
Dummy{} -> mempty
instance Free a => Free (Type' a) where
freeVars' (El s t) =
ifM ((IgnoreNot ==) <$> asks feIgnoreSorts)
(freeVars' (s, t))
(freeVars' t)
instance Free Sort where
freeVars' s =
ifM ((IgnoreAll ==) <$> asks feIgnoreSorts) mempty $
case s of
Type a -> freeVars' a
Prop a -> freeVars' a
Inf -> mempty
SizeUniv -> mempty
PiSort s1 s2 -> go WeaklyRigid $ freeVars' (s1, s2)
UnivSort s -> go WeaklyRigid $ freeVars' s
MetaS x es -> go (Flexible $ singleton x) $ freeVars' es
DefS _ es -> go WeaklyRigid $ freeVars' es
DummyS{} -> mempty
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 m vs -> go (Flexible $ singleton m) $ 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
freeVars' (IApply x y r) = mconcat $ map freeVars' [x,y,r]
instance Free a => Free (Arg a) where
freeVars' a = goRel (getRelevance a) $ freeVars' $ unArg a
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
instance Free EqualityView where
freeVars' (OtherType t) = freeVars' t
freeVars' (EqualityType s _eq l t a b) = freeVars' s `mappend` freeVars' (l ++ [t, a, b])