module Agda.TypeChecking.Free.Reduce (forceNotFree) where
import Control.Monad.State
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.Precompute
import Agda.Utils.Monad
forceNotFree :: IntSet -> Type -> TCM (IntSet, Type)
forceNotFree xs a = do
(a, xs) <- runStateT (forceNotFreeR $ precomputeFreeVars_ a) xs
return (xs, a)
class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a where
forceNotFree' :: a -> StateT IntSet TCM a
reduceIfFreeVars :: (Reduce a, ForceNotFree a) => (a -> StateT IntSet TCM a) -> a -> StateT IntSet TCM a
reduceIfFreeVars k a = do
xs <- get
let fvs = precomputedFreeVars a
notfree = IntSet.null $ IntSet.intersection xs fvs
if | notfree -> return a
| otherwise -> k . precomputeFreeVars_ =<< lift (reduce a)
forceNotFreeR :: (Reduce a, ForceNotFree a) => a -> StateT IntSet TCM 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 $ IntSet.map succ) (\ _ -> modify $ IntSet.map 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
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 -> Var x <$ modify (IntSet.delete x) <*> forceNotFree' es
Def f es -> Def f <$> forceNotFree' es
Con c h es -> Con c h <$> forceNotFree' es
MetaV x es -> 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
instance ForceNotFree Level where
forceNotFree' (Max as) = Max <$> forceNotFree' as
instance ForceNotFree PlusLevel where
forceNotFree' l = case l of
ClosedLevel{} -> return l
Plus k a -> Plus k <$> forceNotFree' a
instance ForceNotFree LevelAtom where
forceNotFree' l = case l of
MetaLevel x es -> 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 -> return Prop
PiSort a b -> PiSort <$> forceNotFree' a <*> forceNotFree' b
UnivSort s -> UnivSort <$> forceNotFree' s
MetaS x es -> MetaS x <$> forceNotFree' es
Inf -> return s
SizeUniv -> return s