{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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
  , reallyFree
  , IsFree(..)
  ) where

import Prelude hiding (null)

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 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
import Agda.Utils.Null

-- | 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
$c== :: IsFree -> IsFree -> Bool
== :: IsFree -> IsFree -> Bool
$c/= :: IsFree -> IsFree -> Bool
/= :: 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
$cshowsPrec :: Int -> IsFree -> ShowS
showsPrec :: Int -> IsFree -> ShowS
$cshow :: IsFree -> String
show :: IsFree -> String
$cshowList :: [IsFree] -> ShowS
showList :: [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 :: forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap IsFree
mxs, a
a)

-- | Checks if the given term contains any free variables that are in
--   the given set of variables, possibly reducing the term in the
--   process.  Returns `Right Nothing` if there are such variables,
--   `Right (Just v')` if there are none (where v' is the possibly
--   reduced version of the given term) or `Left b` if the problem is
--   blocked on a meta.
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a)
           => IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree :: forall (m :: * -> *) a.
(MonadReduce m, Reduce a, ForceNotFree a) =>
IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree IntSet
xs a
v = do
  (IntMap IsFree
mxs , a
v') <- IntSet -> a -> m (IntMap IsFree, a)
forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree IntSet
xs a
v
  case (IsFree -> IsFree -> IsFree) -> IsFree -> IntMap IsFree -> IsFree
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IntMap.foldr IsFree -> IsFree -> IsFree
pickFree IsFree
NotFree IntMap IsFree
mxs of
    MaybeFree MetaSet
ms
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms   -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right Maybe a
forall a. Maybe a
Nothing
      | Bool
otherwise -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Either Blocked_ (Maybe a)
forall a b. a -> Either a b
Left (Blocked_ -> Either Blocked_ (Maybe a))
-> Blocked_ -> Either Blocked_ (Maybe a)
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
      where blocker :: Blocker
blocker = MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
    IsFree
NotFree -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right (a -> Maybe a
forall a. a -> Maybe a
Just a
v')

  where
    -- Check if any of the variables occur freely.
    -- Prefer occurrences that do not depend on any metas.
    pickFree :: IsFree -> IsFree -> IsFree
    pickFree :: IsFree -> IsFree -> IsFree
pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
f2
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms1  = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) f2 :: IsFree
f2@(MaybeFree MetaSet
ms2)
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms2  = IsFree
f2
      | Bool
otherwise = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
NotFree = IsFree
f1
    pickFree IsFree
NotFree IsFree
f2 = IsFree
f2

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

class (PrecomputeFreeVars a, Subst 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 :: forall (m :: * -> *). MonadFreeRed m => m IntSet
varsToForceNotFree = (IntMap IsFree -> IntSet) -> m IntSet
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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)))

-- 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 :: forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(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 -> IntSet -> Bool
IntSet.disjoint IntSet
xs IntSet
fvs
  if Bool
notfree
    then a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    else 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 :: forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
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
forall (m :: * -> *). 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' :: forall (m :: * -> *). MonadFreeRed m => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forall (m :: * -> *). MonadFreeRed m => a -> m a
forceNotFree')

instance (Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term 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' :: forall (m :: * -> *). MonadFreeRed m => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forall (m :: * -> *). MonadFreeRed m => a -> m a
forceNotFree') Abs a
a

instance ForceNotFree a => ForceNotFree [a] where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m a
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forall (m :: * -> *). 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' :: forall (m :: * -> *). MonadFreeRed m => 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
forall (m :: * -> *). MonadFreeRed m => Arg a -> m (Arg a)
forceNotFree' Arg a
arg
  forceNotFree' e :: Elim' a
e@Proj{}       = Elim' a -> m (Elim' a)
forall a. a -> m 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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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' :: forall (m :: * -> *). MonadFreeRed m => 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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
forceNotFree' Sort' Term
s m (Term -> Type) -> m Term -> m Type
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *). MonadFreeRed m => Term -> m Term
forceNotFree' Term
t

instance ForceNotFree Term where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Term -> m Term
forceNotFree' = \case
    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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
forceNotFree' Elims
es
    MetaV MetaId
x Elims
es -> (MetaSet -> MetaSet) -> m Term -> m Term
forall a. (MetaSet -> MetaSet) -> m a -> m a
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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
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
forall (m :: * -> *). MonadFreeRed m => Abs Term -> m (Abs Term)
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
forall (m :: * -> *). MonadFreeRed m => Dom Type -> m (Dom Type)
forceNotFree' Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *). MonadFreeRed m => Abs Type -> m (Abs Type)
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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
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
forall (m :: * -> *). MonadFreeRed m => Level -> m Level
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
    t :: Term
t@Lit{}    -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    t :: Term
t@Dummy{}  -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

instance ForceNotFree Level where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => 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
forall (m :: * -> *).
MonadFreeRed m =>
[PlusLevel' Term] -> m [PlusLevel' Term]
forceNotFree' [PlusLevel' Term]
as

instance ForceNotFree PlusLevel where
  forceNotFree' :: forall (m :: * -> *).
MonadFreeRed m =>
PlusLevel' Term -> m (PlusLevel' Term)
forceNotFree' (Plus Integer
k Term
a) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
k (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' 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
forall (m :: * -> *). MonadFreeRed m => Term -> m Term
forceNotFree' Term
a

instance ForceNotFree Sort where
  -- Reduce for sorts already goes under all sort constructors, so we can get
  -- away without forceNotFreeR here.
  forceNotFree' :: forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
forceNotFree' = \case
    Univ Univ
u Level
l     -> Univ -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (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
forall (m :: * -> *). MonadFreeRed m => Level -> m Level
forceNotFree' Level
l
    PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c -> Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term)
-> m (Dom' Term Term)
-> m (Sort' Term -> Abs (Sort' Term) -> Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term -> m (Dom' Term Term)
forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forall (m :: * -> *).
MonadFreeRed m =>
Dom' Term Term -> m (Dom' Term Term)
forceNotFree' Dom' Term Term
a m (Sort' Term -> Abs (Sort' Term) -> Sort' Term)
-> m (Sort' Term) -> m (Abs (Sort' Term) -> Sort' Term)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
forceNotFree' Sort' Term
b m (Abs (Sort' Term) -> Sort' Term)
-> m (Abs (Sort' Term)) -> m (Sort' Term)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
MonadFreeRed m =>
Abs (Sort' Term) -> m (Abs (Sort' Term))
forceNotFree' Abs (Sort' Term)
c
    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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
forceNotFree' Sort' Term
a m (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
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
forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
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
forall (m :: * -> *). MonadFreeRed m => Elims -> m Elims
forceNotFree' Elims
es
    s :: Sort' Term
s@(Inf Univ
_ Integer
_)-> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
SizeUniv -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
LockUniv -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
LevelUniv -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
IntervalUniv -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@DummyS{} -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s