module Agda.TypeChecking.Free.Reduce
( ForceNotFree
, forceNotFree
, IsFree(..)
) where
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute
import Agda.Utils.Monad
data IsFree
= MaybeFree MetaSet
| NotFree
deriving (Eq, Show)
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m)
=> IntSet -> a -> m (IntMap IsFree, a)
forceNotFree xs a = do
let mxs = IntMap.fromSet (const NotFree) xs
(a, mxs) <- runStateT (runReaderT (forceNotFreeR $ precomputeFreeVars_ a) mempty) mxs
return (mxs, a)
type MonadFreeRed m =
( MonadReader MetaSet m
, MonadState (IntMap IsFree) m
, MonadReduce m
)
class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a where
forceNotFree' :: (MonadFreeRed m) => a -> m a
varsToForceNotFree :: (MonadFreeRed m) => m IntSet
varsToForceNotFree = IntMap.keysSet . (IntMap.filter (== NotFree)) <$> get
reduceIfFreeVars :: (Reduce a, ForceNotFree a, MonadFreeRed m)
=> (a -> m a) -> a -> m a
reduceIfFreeVars k a = do
xs <- varsToForceNotFree
let fvs = precomputedFreeVars a
notfree = IntSet.null $ IntSet.intersection xs fvs
if | notfree -> return a
| otherwise -> k . precomputeFreeVars_ =<< reduce a
forceNotFreeR :: (Reduce a, ForceNotFree a, MonadFreeRed m)
=> a -> m a
forceNotFreeR = reduceIfFreeVars forceNotFree'
instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where
forceNotFree' = reduceIfFreeVars (traverse forceNotFree')
instance (Reduce a, ForceNotFree a) => ForceNotFree (Dom a) where
forceNotFree' = traverse forceNotFreeR
instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where
forceNotFree' a@NoAbs{} = traverse forceNotFreeR a
forceNotFree' a@Abs{} =
reduceIfFreeVars (bracket_ (modify $ IntMap.mapKeys succ) (\ _ -> modify $ IntMap.mapKeys pred) .
traverse forceNotFree') a
instance ForceNotFree a => ForceNotFree [a] where
forceNotFree' = traverse forceNotFree'
instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where
forceNotFree' (Apply arg) = Apply <$> forceNotFree' arg
forceNotFree' e@Proj{} = return e
forceNotFree' (IApply x y r) = IApply <$> forceNotFreeR x <*> forceNotFreeR y <*> forceNotFreeR r
instance ForceNotFree Type where
forceNotFree' (El s t) = El <$> forceNotFree' s <*> forceNotFree' t
instance ForceNotFree Term where
forceNotFree' t = case t of
Var x es -> do
metas <- ask
modify $ IntMap.adjust (const $ MaybeFree metas) x
Var x <$> forceNotFree' es
Def f es -> Def f <$> forceNotFree' es
Con c h es -> Con c h <$> forceNotFree' es
MetaV x es -> local (insertMetaSet x) $
MetaV x <$> forceNotFree' es
Lam h b -> Lam h <$> forceNotFree' b
Pi a b -> Pi <$> forceNotFree' a <*> forceNotFree' b
Sort s -> Sort <$> forceNotFree' s
Level l -> Level <$> forceNotFree' l
DontCare t -> DontCare <$> forceNotFreeR t
Lit{} -> return t
Dummy{} -> return t
instance ForceNotFree Level where
forceNotFree' (Max m as) = Max m <$> forceNotFree' as
instance ForceNotFree PlusLevel where
forceNotFree' (Plus k a) = Plus k <$> forceNotFree' a
instance ForceNotFree LevelAtom where
forceNotFree' l = case l of
MetaLevel x es -> local (insertMetaSet x) $
MetaLevel x <$> forceNotFree' es
BlockedLevel x t -> BlockedLevel x <$> forceNotFree' t
NeutralLevel b t -> NeutralLevel b <$> forceNotFree' t
UnreducedLevel t -> UnreducedLevel <$> forceNotFreeR t
instance ForceNotFree Sort where
forceNotFree' s = case s of
Type l -> Type <$> forceNotFree' l
Prop l -> Prop <$> forceNotFree' l
PiSort a b -> PiSort <$> forceNotFree' a <*> forceNotFree' b
UnivSort s -> UnivSort <$> forceNotFree' s
MetaS x es -> MetaS x <$> forceNotFree' es
DefS d es -> DefS d <$> forceNotFree' es
Inf -> return s
SizeUniv -> return s
DummyS{} -> return s