-- | Free variable check that reduces the subject to make certain variables not
--   free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
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

-- | A variable can either not occur (`NotFree`) or it does occur
--   (`MaybeFree`).  In the latter case, the occurrence may disappear
--   depending on the instantiation of some set of metas.
data IsFree
  = MaybeFree MetaSet
  | NotFree
  deriving (IsFree -> IsFree -> Bool
(IsFree -> IsFree -> Bool)
-> (IsFree -> IsFree -> Bool) -> Eq IsFree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFree -> IsFree -> Bool
$c/= :: IsFree -> IsFree -> Bool
== :: IsFree -> IsFree -> Bool
$c== :: IsFree -> IsFree -> Bool
Eq, Int -> IsFree -> ShowS
[IsFree] -> ShowS
IsFree -> String
(Int -> IsFree -> ShowS)
-> (IsFree -> String) -> ([IsFree] -> ShowS) -> Show IsFree
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsFree] -> ShowS
$cshowList :: [IsFree] -> ShowS
show :: IsFree -> String
$cshow :: IsFree -> String
showsPrec :: Int -> IsFree -> ShowS
$cshowsPrec :: Int -> IsFree -> ShowS
Show)

-- | Try to enforce a set of variables not occurring in a given
--   type. Returns a possibly reduced version of the type and for each
--   of the given variables whether it is either not free, or
--   maybe free depending on some metavariables.
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m)
             => IntSet -> a -> m (IntMap IsFree, a)
forceNotFree :: IntSet -> a -> m (IntMap IsFree, a)
forceNotFree IntSet
xs a
a = do
  -- Initially, all variables are marked as `NotFree`. This is changed
  -- to `MaybeFree` when we find an occurrence.
  let mxs :: IntMap IsFree
mxs = (Int -> IsFree) -> IntSet -> IntMap IsFree
forall a. (Int -> a) -> IntSet -> IntMap a
IntMap.fromSet (IsFree -> Int -> IsFree
forall a b. a -> b -> a
const IsFree
NotFree) IntSet
xs
  (a
a, IntMap IsFree
mxs) <- StateT (IntMap IsFree) m a -> IntMap IsFree -> m (a, IntMap IsFree)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ReaderT MetaSet (StateT (IntMap IsFree) m) a
-> MetaSet -> StateT (IntMap IsFree) m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR (a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a)
-> a -> ReaderT MetaSet (StateT (IntMap IsFree) m) a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ a
a) MetaSet
forall a. Monoid a => a
mempty) IntMap IsFree
mxs
  (IntMap IsFree, a) -> m (IntMap IsFree, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap IsFree
mxs, a
a)

type MonadFreeRed m =
  ( MonadReader MetaSet m
  , MonadState (IntMap IsFree) m
  , MonadReduce m
  )

class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a where
  -- Reduce the argument if necessary, to make as many as possible of
  -- the variables in the state not free. Updates the state, marking
  -- the variables that couldn't be make not free as `MaybeFree`. By
  -- updating the state as soon as a variable can not be reduced away,
  -- we avoid trying to get rid of it in other places.
  forceNotFree' :: (MonadFreeRed m) => a -> m a

-- Return the set of variables for which there is still hope that they
-- may not occur.
varsToForceNotFree :: (MonadFreeRed m) => m IntSet
varsToForceNotFree :: m IntSet
varsToForceNotFree = IntMap IsFree -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (IntMap IsFree -> IntSet)
-> (IntMap IsFree -> IntMap IsFree) -> IntMap IsFree -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IsFree -> Bool) -> IntMap IsFree -> IntMap IsFree
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (IsFree -> IsFree -> Bool
forall a. Eq a => a -> a -> Bool
== IsFree
NotFree)) (IntMap IsFree -> IntSet) -> m (IntMap IsFree) -> m IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (IntMap IsFree)
forall s (m :: * -> *). MonadState s m => m s
get

-- Reduce the argument if there are offending free variables. Doesn't call the
-- continuation when no reduction is required.
reduceIfFreeVars :: (Reduce a, ForceNotFree a, MonadFreeRed m)
                 => (a -> m a) -> a -> m a
reduceIfFreeVars :: (a -> m a) -> a -> m a
reduceIfFreeVars a -> m a
k a
a = do
  IntSet
xs <- m IntSet
forall (m :: * -> *). MonadFreeRed m => m IntSet
varsToForceNotFree
  let fvs :: IntSet
fvs     = a -> IntSet
forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
a
      notfree :: Bool
notfree = IntSet -> Bool
IntSet.null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
xs IntSet
fvs
  if | Bool
notfree   -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
     | Bool
otherwise -> a -> m a
k (a -> m a) -> (a -> a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ (a -> m a) -> m a -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> m a
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce a
a

-- Careful not to define forceNotFree' = forceNotFreeR since that would loop.
forceNotFreeR :: (Reduce a, ForceNotFree a, MonadFreeRed m)
              => a -> m a
forceNotFreeR :: a -> m a
forceNotFreeR = (a -> m a) -> a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree'

instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where
  -- Precomputed free variables are stored in the Arg so reduceIf outside the
  -- traverse.
  forceNotFree' :: Arg a -> m (Arg a)
forceNotFree' = (Arg a -> m (Arg a)) -> Arg a -> m (Arg a)
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars ((a -> m a) -> Arg a -> m (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree')

instance (Reduce a, ForceNotFree a) => ForceNotFree (Dom a) where
  forceNotFree' :: Dom a -> m (Dom a)
forceNotFree' = (a -> m a) -> Dom a -> m (Dom a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR

instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where
  -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here.
  forceNotFree' :: Abs a -> m (Abs a)
forceNotFree' a :: Abs a
a@NoAbs{} = (a -> m a) -> Abs a -> m (Abs a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR Abs a
a
  forceNotFree' a :: Abs a
a@Abs{} =
    -- Shift variables up when going under the abstraction and back down when
    -- coming out of it. Since we never add new indices to the state
    -- there's no danger of getting negative indices.
    (Abs a -> m (Abs a)) -> Abs a -> m (Abs a)
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars (m () -> (() -> m ()) -> m (Abs a) -> m (Abs a)
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ ((IntMap IsFree -> IntMap IsFree) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntMap IsFree -> IntMap IsFree) -> m ())
-> (IntMap IsFree -> IntMap IsFree) -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> IntMap IsFree -> IntMap IsFree
forall a. (Int -> Int) -> IntMap a -> IntMap a
IntMap.mapKeys Int -> Int
forall a. Enum a => a -> a
succ) (\ ()
_ -> (IntMap IsFree -> IntMap IsFree) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntMap IsFree -> IntMap IsFree) -> m ())
-> (IntMap IsFree -> IntMap IsFree) -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> IntMap IsFree -> IntMap IsFree
forall a. (Int -> Int) -> IntMap a -> IntMap a
IntMap.mapKeys Int -> Int
forall a. Enum a => a -> a
pred) (m (Abs a) -> m (Abs a))
-> (Abs a -> m (Abs a)) -> Abs a -> m (Abs a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      (a -> m a) -> Abs a -> m (Abs a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree') Abs a
a

instance ForceNotFree a => ForceNotFree [a] where
  forceNotFree' :: [a] -> m [a]
forceNotFree' = (a -> m a) -> [a] -> m [a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree'

instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where
  -- There's an Arg inside Elim' which stores precomputed free vars, so let's
  -- not skip over that.
  forceNotFree' :: Elim' a -> m (Elim' a)
forceNotFree' (Apply Arg a
arg)    = Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a) -> m (Arg a) -> m (Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg a -> m (Arg a)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Arg a
arg
  forceNotFree' e :: Elim' a
e@Proj{}       = Elim' a -> m (Elim' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Elim' a
e
  forceNotFree' (IApply a
x a
y a
r) = a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (a -> a -> a -> Elim' a) -> m a -> m (a -> a -> Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
x m (a -> a -> Elim' a) -> m a -> m (a -> Elim' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
y m (a -> Elim' a) -> m a -> m (Elim' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m a
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
r

instance ForceNotFree Type where
  forceNotFree' :: Type -> m Type
forceNotFree' (El Sort' Term
s Term
t) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Term
t

instance ForceNotFree Term where
  forceNotFree' :: Term -> m Term
forceNotFree' Term
t = case Term
t of
    Var Int
x Elims
es   -> do
      MetaSet
metas <- m MetaSet
forall r (m :: * -> *). MonadReader r m => m r
ask
      (IntMap IsFree -> IntMap IsFree) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntMap IsFree -> IntMap IsFree) -> m ())
-> (IntMap IsFree -> IntMap IsFree) -> m ()
forall a b. (a -> b) -> a -> b
$ (IsFree -> IsFree) -> Int -> IntMap IsFree -> IntMap IsFree
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (IsFree -> IsFree -> IsFree
forall a b. a -> b -> a
const (IsFree -> IsFree -> IsFree) -> IsFree -> IsFree -> IsFree
forall a b. (a -> b) -> a -> b
$ MetaSet -> IsFree
MaybeFree MetaSet
metas) Int
x
      Int -> Elims -> Term
Var Int
x (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Def QName
f Elims
es   -> QName -> Elims -> Term
Def QName
f    (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Con ConHead
c ConInfo
h Elims
es -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
h  (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    MetaV MetaId
x Elims
es -> (MetaSet -> MetaSet) -> m Term -> m Term
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
x) (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$
                  MetaId -> Elims -> Term
MetaV MetaId
x  (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Lam ArgInfo
h Abs Term
b    -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h    (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> m (Abs Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs Term
b
    Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
Pi       (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs Type
b  -- Dom and Abs do reduceIf so not needed here
    Sort Sort' Term
s     -> Sort' Term -> Term
Sort     (Sort' Term -> Term) -> m (Sort' Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s
    Level Level
l    -> Level -> Term
Level    (Level -> Term) -> m Level -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    DontCare Term
t -> Term -> Term
DontCare (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR Term
t  -- Reduction stops at DontCare so reduceIf
    Lit{}      -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    Dummy{}    -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

instance ForceNotFree Level where
  forceNotFree' :: Level -> m Level
forceNotFree' (Max Integer
m [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m [PlusLevel' Term]
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' [PlusLevel' Term]
as

instance ForceNotFree PlusLevel where
  forceNotFree' :: PlusLevel' Term -> m (PlusLevel' Term)
forceNotFree' (Plus Integer
k LevelAtom' Term
a) = Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
k (LevelAtom' Term -> PlusLevel' Term)
-> m (LevelAtom' Term) -> m (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LevelAtom' Term -> m (LevelAtom' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' LevelAtom' Term
a

instance ForceNotFree LevelAtom where
  forceNotFree' :: LevelAtom' Term -> m (LevelAtom' Term)
forceNotFree' LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
x Elims
es   -> (MetaSet -> MetaSet) -> m (LevelAtom' Term) -> m (LevelAtom' Term)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
x) (m (LevelAtom' Term) -> m (LevelAtom' Term))
-> m (LevelAtom' Term) -> m (LevelAtom' Term)
forall a b. (a -> b) -> a -> b
$
                        MetaId -> Elims -> LevelAtom' Term
forall t. MetaId -> [Elim' t] -> LevelAtom' t
MetaLevel MetaId
x    (Elims -> LevelAtom' Term) -> m Elims -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    BlockedLevel MetaId
x Term
t -> MetaId -> Term -> LevelAtom' Term
forall t. MetaId -> t -> LevelAtom' t
BlockedLevel MetaId
x (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Term
t
    NeutralLevel NotBlocked
b Term
t -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
b (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Term
t
    UnreducedLevel Term
t -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR Term
t  -- Already reduce in the cases above

instance ForceNotFree Sort where
  -- Reduce for sorts already goes under all sort constructors, so we can get
  -- away without forceNotFreeR here.
  forceNotFree' :: Sort' Term -> m (Sort' Term)
forceNotFree' Sort' Term
s = case Sort' Term
s of
    Type Level
l     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Type     (Level -> Sort' Term) -> m Level -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    Prop Level
l     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Prop     (Level -> Sort' Term) -> m Level -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    PiSort Dom Type
a Abs (Sort' Term)
b -> Dom Type -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort   (Dom Type -> Abs (Sort' Term) -> Sort' Term)
-> m (Dom Type) -> m (Abs (Sort' Term) -> Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Dom Type
a m (Abs (Sort' Term) -> Sort' Term)
-> m (Abs (Sort' Term)) -> m (Sort' Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs (Sort' Term) -> m (Abs (Sort' Term))
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs (Sort' Term)
b
    FunSort Sort' Term
a Sort' Term
b -> Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort' Term -> Sort' Term -> Sort' Term)
-> m (Sort' Term) -> m (Sort' Term -> Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
a m (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
b
    UnivSort Sort' Term
s -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s
    MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  (Elims -> Sort' Term) -> m Elims -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    DefS QName
d Elims
es  -> QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d   (Elims -> Sort' Term) -> m Elims -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Sort' Term
Inf        -> Sort' Term -> m (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    Sort' Term
SizeUniv   -> Sort' Term -> m (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    DummyS{}   -> Sort' Term -> m (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s