{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Reduce
 -- Meta instantiation
 ( Instantiate, instantiate', instantiate, instantiateWhen
 -- Recursive meta instantiation
 , InstantiateFull, instantiateFull', instantiateFull
 -- Check for meta (no reduction)
 , IsMeta, isMeta
 -- Reduction and blocking
 , Reduce, reduce', reduceB', reduce, reduceB, reduceWithBlocker, reduceIApply'
 , reduceDefCopy, reduceDefCopyTCM
 , reduceHead
 , slowReduceTerm
 , unfoldCorecursion, unfoldCorecursionE
 , unfoldDefinitionE, unfoldDefinitionStep
 , unfoldInlined
 , appDef', appDefE'
 , abortIfBlocked, ifBlocked, isBlocked, fromBlocked, blockOnError
 -- Simplification
 , Simplify, simplify, simplifyBlocked'
 -- Normalization
 , Normalise, normalise', normalise
 , slowNormaliseArgs
 ) where

import Control.Monad ( (>=>), void )
import Control.Monad.Except

import Data.List ( intercalate )
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Foldable
import Data.Traversable
import Data.HashMap.Strict (HashMap)
import qualified Data.Set as Set

import Agda.Interaction.Options

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Base (Scope)
import Agda.Syntax.Literal

import {-# SOURCE #-} Agda.TypeChecking.Irrelevance (isPropM)
import Agda.TypeChecking.Monad hiding ( enterClosure, constructorForm )
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.EtaContract

import Agda.TypeChecking.Reduce.Monad

import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Match
import {-# SOURCE #-} Agda.TypeChecking.Patterns.Match
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import {-# SOURCE #-} Agda.TypeChecking.Rewriting
import {-# SOURCE #-} Agda.TypeChecking.Reduce.Fast
import {-# SOURCE #-} Agda.TypeChecking.Opacity

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.SmallSet as SmallSet

import Agda.Utils.Impossible

instantiate :: (Instantiate a, MonadReduce m) => a -> m a
instantiate :: forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate = ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate'

instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a
instantiateFull :: forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull = ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM a
forall t. InstantiateFull t => t -> ReduceM t
instantiateFull'

-- | A variant of 'instantiateFull' that only instantiates those
-- meta-variables that satisfy the predicate.

instantiateWhen ::
  (InstantiateFull a, MonadReduce m) =>
  (MetaId -> ReduceM Bool) ->
  a -> m a
instantiateWhen :: forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
(MetaId -> ReduceM Bool) -> a -> m a
instantiateWhen MetaId -> ReduceM Bool
p =
  ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
forall a. (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
localR (\ReduceEnv
env -> ReduceEnv
env { redPred = Just p }) (ReduceM a -> ReduceM a) -> (a -> ReduceM a) -> a -> ReduceM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  a -> ReduceM a
forall t. InstantiateFull t => t -> ReduceM t
instantiateFull'

{-# INLINE reduce #-}
reduce :: (Reduce a, MonadReduce m) => a -> m a
reduce :: forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce = ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM a
forall t. Reduce t => t -> ReduceM t
reduce'

{-# INLINE reduceB #-}
reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a)
reduceB :: forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB = ReduceM (Blocked a) -> m (Blocked a)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Blocked a) -> m (Blocked a))
-> (a -> ReduceM (Blocked a)) -> a -> m (Blocked a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM (Blocked a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'

-- Reduce a term and also produce a blocker signifying when
-- this reduction should be retried.
reduceWithBlocker :: (Reduce a, IsMeta a, MonadReduce m) => a -> m (Blocker, a)
reduceWithBlocker :: forall a (m :: * -> *).
(Reduce a, IsMeta a, MonadReduce m) =>
a -> m (Blocker, a)
reduceWithBlocker a
a = a
-> (Blocker -> a -> m (Blocker, a))
-> (NotBlocked -> a -> m (Blocker, a))
-> m (Blocker, a)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked a
a
  (\Blocker
b a
a' -> (Blocker, a) -> m (Blocker, a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker
b, a
a'))
  (\NotBlocked
_ a
a' -> (Blocker, a) -> m (Blocker, a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker
neverUnblock, a
a'))

{-# INLINE normalise #-}
normalise :: (Normalise a, MonadReduce m) => a -> m a
normalise :: forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise = ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM a
forall t. Normalise t => t -> ReduceM t
normalise'

-- UNUSED
-- -- | Normalise the given term but also preserve blocking tags
-- --   TODO: implement a more efficient version of this.
-- normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t)
-- normaliseB = normalise >=> reduceB

{-# INLINE simplify #-}
simplify :: (Simplify a, MonadReduce m) => a -> m a
simplify :: forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify = ReduceM a -> m a
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM a -> m a) -> (a -> ReduceM a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify'

-- | Meaning no metas left in the instantiation.
isFullyInstantiatedMeta :: MetaId -> TCM Bool
isFullyInstantiatedMeta :: MetaId -> TCM Bool
isFullyInstantiatedMeta MetaId
m = do
  MetaInstantiation
inst <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
  case MetaInstantiation
inst of
    InstV Instantiation
inst -> Term -> Bool
forall a. AllMetas a => a -> Bool
noMetas (Term -> Bool) -> TCMT IO Term -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Instantiation -> Term
instBody Instantiation
inst)
    MetaInstantiation
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

{-# INLINABLE blockAll #-}
-- | Blocking on all blockers.
blockAll :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)
blockAll :: forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAll f (Blocked a)
bs = Blocker -> f a -> Blocked' Term (f a)
forall a t. Blocker -> a -> Blocked' t a
blockedOn Blocker
block (f a -> Blocked' Term (f a)) -> f a -> Blocked' Term (f a)
forall a b. (a -> b) -> a -> b
$ (Blocked a -> a) -> f (Blocked a) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Blocked a -> a
forall t a. Blocked' t a -> a
ignoreBlocking f (Blocked a)
bs
  where block :: Blocker
block = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (Blocked a -> Set Blocker) -> f (Blocked a) -> Set Blocker
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Blocker -> Set Blocker
forall a. a -> Set a
Set.singleton (Blocker -> Set Blocker)
-> (Blocked a -> Blocker) -> Blocked a -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked a -> Blocker
forall {t} {a}. Blocked' t a -> Blocker
blocker) f (Blocked a)
bs
        blocker :: Blocked' t a -> Blocker
blocker NotBlocked{}  = Blocker
alwaysUnblock
        blocker (Blocked Blocker
b a
_) = Blocker
b

{-# INLINABLE blockAny #-}
-- | Blocking on any blockers.
blockAny :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)
blockAny :: forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAny f (Blocked a)
bs = Blocker -> f a -> Blocked' Term (f a)
forall a t. Blocker -> a -> Blocked' t a
blockedOn Blocker
block (f a -> Blocked' Term (f a)) -> f a -> Blocked' Term (f a)
forall a b. (a -> b) -> a -> b
$ (Blocked a -> a) -> f (Blocked a) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Blocked a -> a
forall t a. Blocked' t a -> a
ignoreBlocking f (Blocked a)
bs
  where block :: Blocker
block = case (Blocked a -> [Blocker]) -> f (Blocked a) -> [Blocker]
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Blocked a -> [Blocker]
forall {t} {a}. Blocked' t a -> [Blocker]
blocker f (Blocked a)
bs of
                  [] -> Blocker
alwaysUnblock -- no blockers
                  [Blocker]
bs -> Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList [Blocker]
bs
        blocker :: Blocked' t a -> [Blocker]
blocker NotBlocked{}  = []
        blocker (Blocked Blocker
b a
_) = [Blocker
b]

{-# SPECIALIZE blockOnError :: Blocker -> TCM a -> TCM a #-}
-- | Run the given computation but turn any errors into blocked computations with the given blocker
blockOnError :: MonadError TCErr m => Blocker -> m a -> m a
blockOnError :: forall (m :: * -> *) a. MonadError TCErr m => Blocker -> m a -> m a
blockOnError Blocker
blocker m a
f
  | Blocker
blocker Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock = m a
f
  | Bool
otherwise               = m a
f m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    TypeError{}         -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> TCErr -> m a
forall a b. (a -> b) -> a -> b
$ Blocker -> TCErr
PatternErr Blocker
blocker
    PatternErr Blocker
blocker' -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> TCErr -> m a
forall a b. (a -> b) -> a -> b
$ Blocker -> TCErr
PatternErr (Blocker -> TCErr) -> Blocker -> TCErr
forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnEither Blocker
blocker Blocker
blocker'
    err :: TCErr
err@Exception{}     -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    err :: TCErr
err@IOException{}   -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

-- | Instantiate something.
--   Results in an open meta variable or a non meta.
--   Doesn't do any reduction, and preserves blocking tags (when blocking meta
--   is uninstantiated).
class Instantiate t where
  instantiate' :: t -> ReduceM t

  default instantiate' :: (t ~ f a, Traversable f, Instantiate a) => t -> ReduceM t
  instantiate' = (a -> ReduceM a) -> f a -> ReduceM (f 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) -> f a -> f (f b)
traverse a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate'

instance Instantiate t => Instantiate [t]
instance Instantiate t => Instantiate (Map k t)
instance Instantiate t => Instantiate (Maybe t)
instance Instantiate t => Instantiate (Strict.Maybe t)

instance Instantiate t => Instantiate (Abs t)
instance Instantiate t => Instantiate (Arg t)
instance Instantiate t => Instantiate (Elim' t)
instance Instantiate t => Instantiate (Tele t)
instance Instantiate t => Instantiate (IPBoundary' t)

instance Instantiate () where
    instantiate' :: () -> ReduceM ()
instantiate' () = () -> ReduceM ()
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance (Instantiate a, Instantiate b) => Instantiate (a,b) where
    instantiate' :: (a, b) -> ReduceM (a, b)
instantiate' (a
x,b
y) = (,) (a -> b -> (a, b)) -> ReduceM a -> ReduceM (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate' a
x ReduceM (b -> (a, b)) -> ReduceM b -> ReduceM (a, b)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM b
forall t. Instantiate t => t -> ReduceM t
instantiate' b
y

instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where
    instantiate' :: (a, b, c) -> ReduceM (a, b, c)
instantiate' (a
x,b
y,c
z) = (,,) (a -> b -> c -> (a, b, c))
-> ReduceM a -> ReduceM (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate' a
x ReduceM (b -> c -> (a, b, c))
-> ReduceM b -> ReduceM (c -> (a, b, c))
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM b
forall t. Instantiate t => t -> ReduceM t
instantiate' b
y ReduceM (c -> (a, b, c)) -> ReduceM c -> ReduceM (a, b, c)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> ReduceM c
forall t. Instantiate t => t -> ReduceM t
instantiate' c
z

-- | Run the second computation if the 'redPred' predicate holds for
-- the given meta-variable (or if the predicate is not defined), and
-- otherwise the first computation.

ifPredicateDoesNotHoldFor ::
  MetaId -> ReduceM a -> ReduceM a -> ReduceM a
ifPredicateDoesNotHoldFor :: forall a. MetaId -> ReduceM a -> ReduceM a -> ReduceM a
ifPredicateDoesNotHoldFor MetaId
m ReduceM a
doesNotHold ReduceM a
holds = do
  Maybe (MetaId -> ReduceM Bool)
pred <- ReduceEnv -> Maybe (MetaId -> ReduceM Bool)
redPred (ReduceEnv -> Maybe (MetaId -> ReduceM Bool))
-> ReduceM ReduceEnv -> ReduceM (Maybe (MetaId -> ReduceM Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM ReduceEnv
askR
  case Maybe (MetaId -> ReduceM Bool)
pred of
    Maybe (MetaId -> ReduceM Bool)
Nothing -> ReduceM a
holds
    Just MetaId -> ReduceM Bool
p  -> ReduceM Bool -> ReduceM a -> ReduceM a -> ReduceM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> ReduceM Bool
p MetaId
m) ReduceM a
holds ReduceM a
doesNotHold

instance Instantiate Term where
  instantiate' :: Term -> ReduceM Term
instantiate' t :: Term
t@(MetaV MetaId
x Elims
es) = MetaId -> ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. MetaId -> ReduceM a -> ReduceM a -> ReduceM a
ifPredicateDoesNotHoldFor MetaId
x (Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t) (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ do
    Bool
blocking <- Lens' TCState Bool -> TCState -> Bool
forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstantiateBlocking (TCState -> Bool) -> ReduceM TCState -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState

    Maybe (Either RemoteMetaVariable MetaVariable)
m <- MetaId -> ReduceM (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
x
    case Maybe (Either RemoteMetaVariable MetaVariable)
m of
      Just (Left RemoteMetaVariable
rmv) -> Instantiation -> ReduceM Term
cont (RemoteMetaVariable -> Instantiation
rmvInstantiation RemoteMetaVariable
rmv)

      Just (Right MetaVariable
mv) -> case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
         InstV Instantiation
inst -> Instantiation -> ReduceM Term
cont Instantiation
inst

         MetaInstantiation
_ | Just MetaId
m' <- MetaVariable -> Maybe MetaId
mvTwin MetaVariable
mv, Bool
blocking ->
           Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' (MetaId -> Elims -> Term
MetaV MetaId
m' Elims
es)

         OpenMeta MetaKind
_ -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

         BlockedConst Term
u
           | Bool
blocking  -> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' (Term -> ReduceM Term)
-> (BraveTerm -> Term) -> BraveTerm -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BraveTerm -> Term
unBrave (BraveTerm -> ReduceM Term) -> BraveTerm -> ReduceM Term
forall a b. (a -> b) -> a -> b
$
                          Term -> BraveTerm
BraveTerm Term
u BraveTerm -> Elims -> BraveTerm
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
           | Bool
otherwise -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

         PostponedTypeCheckingProblem Closure TypeCheckingProblem
_ -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

      Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> [Char] -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__
                   ([Char]
"Meta-variable not found: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
x)
    where
    cont :: Instantiation -> ReduceM Term
cont Instantiation
i = Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
inst
      where
      -- A slight complication here is that the meta might be underapplied,
      -- in which case we have to build the lambda abstraction before
      -- applying the substitution, or overapplied in which case we need to
      -- fall back to applyE.
      (Elims
es1, Elims
es2) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt ([Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Instantiation -> [Arg [Char]]
instTel Instantiation
i)) Elims
es
      vs1 :: [Term]
vs1 = [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es1
      rho :: Substitution' Term
rho = [Term]
vs1 [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs1) Substitution' Term
forall a. Substitution' a
idS
            -- really should be .. ++# emptyS but using wkS makes it reduce to idS
            -- when applicable
      -- specification:
      -- inst == foldr mkLam (instBody i) (instTel i) `applyE` es
      inst :: Term
inst =
        Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
rho
          ((Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
mkLam (Instantiation -> Term
instBody Instantiation
i) ([Arg [Char]] -> Term) -> [Arg [Char]] -> Term
forall a b. (a -> b) -> a -> b
$ Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
drop (Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es1) (Instantiation -> [Arg [Char]]
instTel Instantiation
i))
          Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2

  instantiate' (Level Level
l) = Level -> Term
levelTm (Level -> Term) -> ReduceM Level -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReduceM Level
forall t. Instantiate t => t -> ReduceM t
instantiate' Level
l
  instantiate' (Sort Sort
s) = Sort -> Term
Sort (Sort -> Term) -> ReduceM Sort -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
  instantiate' Term
t = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

instance Instantiate t => Instantiate (Type' t) where
  instantiate' :: Type' t -> ReduceM (Type' t)
instantiate' (El Sort
s t
t) = Sort -> t -> Type' t
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> t -> Type' t) -> ReduceM Sort -> ReduceM (t -> Type' t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s ReduceM (t -> Type' t) -> ReduceM t -> ReduceM (Type' t)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> ReduceM t
forall t. Instantiate t => t -> ReduceM t
instantiate' t
t

instance Instantiate Level where
  instantiate' :: Level -> ReduceM Level
instantiate' (Max Integer
m [PlusLevel]
as) = Integer -> [PlusLevel] -> Level
levelMax Integer
m ([PlusLevel] -> Level) -> ReduceM [PlusLevel] -> ReduceM Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel] -> ReduceM [PlusLevel]
forall t. Instantiate t => t -> ReduceM t
instantiate' [PlusLevel]
as

-- Use Traversable instance
instance Instantiate t => Instantiate (PlusLevel' t)

instance Instantiate a => Instantiate (Blocked a) where
  instantiate' :: Blocked a -> ReduceM (Blocked a)
instantiate' v :: Blocked a
v@NotBlocked{} = Blocked a -> ReduceM (Blocked a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked a
v
  instantiate' v :: Blocked a
v@(Blocked Blocker
b a
u) = Blocker -> ReduceM Blocker
forall t. Instantiate t => t -> ReduceM t
instantiate' Blocker
b ReduceM Blocker
-> (Blocker -> ReduceM (Blocked a)) -> ReduceM (Blocked a)
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
    Blocker
b | Blocker
b Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock -> a -> Blocked a
forall a t. a -> Blocked' t a
notBlocked (a -> Blocked a) -> ReduceM a -> ReduceM (Blocked a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate' a
u
      | Bool
otherwise          -> Blocked a -> ReduceM (Blocked a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked a -> ReduceM (Blocked a))
-> Blocked a -> ReduceM (Blocked a)
forall a b. (a -> b) -> a -> b
$ Blocker -> a -> Blocked a
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b a
u

instance Instantiate Blocker where
  instantiate' :: Blocker -> ReduceM Blocker
instantiate' (UnblockOnAll Set Blocker
bs) = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker) -> ReduceM [Blocker] -> ReduceM Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> ReduceM Blocker) -> [Blocker] -> ReduceM [Blocker]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Blocker -> ReduceM Blocker
forall t. Instantiate t => t -> ReduceM t
instantiate' (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs)
  instantiate' (UnblockOnAny Set Blocker
bs) = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker) -> ReduceM [Blocker] -> ReduceM Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> ReduceM Blocker) -> [Blocker] -> ReduceM [Blocker]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Blocker -> ReduceM Blocker
forall t. Instantiate t => t -> ReduceM t
instantiate' (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs)
  instantiate' b :: Blocker
b@(UnblockOnMeta MetaId
x) =
    ReduceM Bool
-> ReduceM Blocker -> ReduceM Blocker -> ReduceM Blocker
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> ReduceM Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
x) (Blocker -> ReduceM Blocker
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock) (Blocker -> ReduceM Blocker
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b)
  instantiate' (UnblockOnProblem ProblemId
pi) =
    ReduceM Bool
-> ReduceM Blocker -> ReduceM Blocker -> ReduceM Blocker
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProblemId -> ReduceM Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pi) (Blocker -> ReduceM Blocker
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock) (Blocker -> ReduceM Blocker
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> ReduceM Blocker) -> Blocker -> ReduceM Blocker
forall a b. (a -> b) -> a -> b
$ ProblemId -> Blocker
UnblockOnProblem ProblemId
pi)
  instantiate' b :: Blocker
b@UnblockOnDef{} = Blocker -> ReduceM Blocker
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b

instance Instantiate Sort where
  instantiate' :: Sort -> ReduceM Sort
instantiate' = \case
    MetaS MetaId
x Elims
es -> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) ReduceM Term -> (Term -> ReduceM Sort) -> ReduceM Sort
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Sort Sort
s'      -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'
      MetaV MetaId
x' Elims
es' -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> ReduceM Sort) -> Sort -> ReduceM Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x' Elims
es'
      Def QName
d Elims
es'    -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> ReduceM Sort) -> Sort -> ReduceM Sort
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es'
      Term
_            -> ReduceM Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Sort
s -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s

instance (Instantiate t, Instantiate e) => Instantiate (Dom' t e) where
    instantiate' :: Dom' t e -> ReduceM (Dom' t e)
instantiate' (Dom ArgInfo
i Maybe NamedName
n Bool
b Maybe t
tac e
x) = ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
i Maybe NamedName
n Bool
b (Maybe t -> e -> Dom' t e)
-> ReduceM (Maybe t) -> ReduceM (e -> Dom' t e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe t -> ReduceM (Maybe t)
forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe t
tac ReduceM (e -> Dom' t e) -> ReduceM e -> ReduceM (Dom' t e)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> e -> ReduceM e
forall t. Instantiate t => t -> ReduceM t
instantiate' e
x

instance Instantiate a => Instantiate (Closure a) where
    instantiate' :: Closure a -> ReduceM (Closure a)
instantiate' Closure a
cl = do
        a
x <- Closure a -> (a -> ReduceM a) -> ReduceM a
forall c a b. LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b
enterClosure Closure a
cl a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate'
        Closure a -> ReduceM (Closure a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure a -> ReduceM (Closure a))
-> Closure a -> ReduceM (Closure a)
forall a b. (a -> b) -> a -> b
$ Closure a
cl { clValue = x }

instance Instantiate Constraint where
  instantiate' :: Constraint -> ReduceM Constraint
instantiate' (ValueCmp Comparison
cmp CompareAs
t Term
u Term
v) = do
    (CompareAs
t,Term
u,Term
v) <- (CompareAs, Term, Term) -> ReduceM (CompareAs, Term, Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' (CompareAs
t,Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp CompareAs
t Term
u Term
v
  instantiate' (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = do
    ((Term
p,Type
t),Term
u,Term
v) <- ((Term, Type), Term, Term) -> ReduceM ((Term, Type), Term, Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' ((Term
p,Type
t),Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v
  instantiate' (ElimCmp [Polarity]
cmp [IsForced]
fs Type
t Term
v Elims
as Elims
bs) =
    [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
cmp [IsForced]
fs (Type -> Term -> Elims -> Elims -> Constraint)
-> ReduceM Type -> ReduceM (Term -> Elims -> Elims -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t ReduceM (Term -> Elims -> Elims -> Constraint)
-> ReduceM Term -> ReduceM (Elims -> Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v ReduceM (Elims -> Elims -> Constraint)
-> ReduceM Elims -> ReduceM (Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Instantiate t => t -> ReduceM t
instantiate' Elims
as ReduceM (Elims -> Constraint)
-> ReduceM Elims -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Instantiate t => t -> ReduceM t
instantiate' Elims
bs
  instantiate' (LevelCmp Comparison
cmp Level
u Level
v)   = (Level -> Level -> Constraint) -> (Level, Level) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) ((Level, Level) -> Constraint)
-> ReduceM (Level, Level) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Level, Level) -> ReduceM (Level, Level)
forall t. Instantiate t => t -> ReduceM t
instantiate' (Level
u,Level
v)
  instantiate' (SortCmp Comparison
cmp Sort
a Sort
b)    = (Sort -> Sort -> Constraint) -> (Sort, Sort) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) ((Sort, Sort) -> Constraint)
-> ReduceM (Sort, Sort) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sort, Sort) -> ReduceM (Sort, Sort)
forall t. Instantiate t => t -> ReduceM t
instantiate' (Sort
a,Sort
b)
  instantiate' (UnBlock MetaId
m)          = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
UnBlock MetaId
m
  instantiate' (FindInstance MetaId
m Maybe [Candidate]
cs)  = MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m (Maybe [Candidate] -> Constraint)
-> ReduceM (Maybe [Candidate]) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Candidate] -> ReduceM [Candidate])
-> Maybe [Candidate] -> ReduceM (Maybe [Candidate])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM [Candidate] -> ReduceM [Candidate]
forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe [Candidate]
cs
  instantiate' (ResolveInstanceHead QName
q) = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ QName -> Constraint
ResolveInstanceHead QName
q
  instantiate' (IsEmpty Range
r Type
t)        = Range -> Type -> Constraint
IsEmpty Range
r (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (CheckSizeLtSat Term
t)   = Term -> Constraint
CheckSizeLtSat (Term -> Constraint) -> ReduceM Term -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
t
  instantiate' c :: Constraint
c@CheckFunDef{}      = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  instantiate' (HasBiggerSort Sort
a)    = Sort -> Constraint
HasBiggerSort (Sort -> Constraint) -> ReduceM Sort -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
a
  instantiate' (HasPTSRule Dom Type
a Abs Sort
b)     = (Dom Type -> Abs Sort -> Constraint)
-> (Dom Type, Abs Sort) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Sort -> Constraint
HasPTSRule ((Dom Type, Abs Sort) -> Constraint)
-> ReduceM (Dom Type, Abs Sort) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom Type, Abs Sort) -> ReduceM (Dom Type, Abs Sort)
forall t. Instantiate t => t -> ReduceM t
instantiate' (Dom Type
a,Abs Sort
b)
  instantiate' (CheckLockedVars Term
a Type
b Arg Term
c Type
d) =
    Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Term -> Type -> Arg Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Type -> Arg Term -> Type -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
a ReduceM (Type -> Arg Term -> Type -> Constraint)
-> ReduceM Type -> ReduceM (Arg Term -> Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
b ReduceM (Arg Term -> Type -> Constraint)
-> ReduceM (Arg Term) -> ReduceM (Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
c ReduceM (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
d
  instantiate' (UnquoteTactic Term
t Term
h Type
g) = Term -> Term -> Type -> Constraint
UnquoteTactic (Term -> Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Term -> Type -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
t ReduceM (Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
h ReduceM (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
g
  instantiate' (CheckDataSort QName
q Sort
s)  = QName -> Sort -> Constraint
CheckDataSort QName
q (Sort -> Constraint) -> ReduceM Sort -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
  instantiate' c :: Constraint
c@CheckMetaInst{}    = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  instantiate' (CheckType Type
t)        = Type -> Constraint
CheckType (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = (Maybe Sort -> Modality -> Term -> Constraint)
-> Modality -> Maybe Sort -> Term -> Constraint
forall a b c. (a -> b -> c) -> b -> a -> c
flip (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc) Modality
mod (Maybe Sort -> Term -> Constraint)
-> ReduceM (Maybe Sort) -> ReduceM (Term -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Sort -> ReduceM (Maybe Sort)
forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe Sort
ms ReduceM (Term -> Constraint) -> ReduceM Term -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
t

instance Instantiate CompareAs where
  instantiate' :: CompareAs -> ReduceM CompareAs
instantiate' (AsTermsOf Type
a) = Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> ReduceM Type -> ReduceM CompareAs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
a
  instantiate' CompareAs
AsSizes       = CompareAs -> ReduceM CompareAs
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
  instantiate' CompareAs
AsTypes       = CompareAs -> ReduceM CompareAs
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsTypes

instance Instantiate Candidate where
  instantiate' :: Candidate -> ReduceM Candidate
instantiate' (Candidate CandidateKind
q Term
u Type
t OverlapMode
ov) = CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
q (Term -> Type -> OverlapMode -> Candidate)
-> ReduceM Term -> ReduceM (Type -> OverlapMode -> Candidate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
u ReduceM (Type -> OverlapMode -> Candidate)
-> ReduceM Type -> ReduceM (OverlapMode -> Candidate)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t ReduceM (OverlapMode -> Candidate)
-> ReduceM OverlapMode -> ReduceM Candidate
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OverlapMode -> ReduceM OverlapMode
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OverlapMode
ov

instance Instantiate EqualityView where
  instantiate' :: EqualityView -> ReduceM EqualityView
instantiate' (OtherType Type
t)            = Type -> EqualityView
OtherType
    (Type -> EqualityView) -> ReduceM Type -> ReduceM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (IdiomType Type
t)            = Type -> EqualityView
IdiomType
    (Type -> EqualityView) -> ReduceM Type -> ReduceM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (EqualityType Sort
s QName
eq [Arg Term]
l Arg Term
t Arg Term
a Arg Term
b) = Sort
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType
    (Sort
 -> QName
 -> [Arg Term]
 -> Arg Term
 -> Arg Term
 -> Arg Term
 -> EqualityView)
-> ReduceM Sort
-> ReduceM
     (QName
      -> [Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
    ReduceM
  (QName
   -> [Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM QName
-> ReduceM
     ([Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> ReduceM QName
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
eq
    ReduceM
  ([Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM [Arg Term]
-> ReduceM (Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Arg Term -> ReduceM (Arg Term))
-> [Arg Term] -> ReduceM [Arg Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Arg Term -> ReduceM (Arg Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' [Arg Term]
l
    ReduceM (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM (Arg Term)
-> ReduceM (Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
t
    ReduceM (Arg Term -> Arg Term -> EqualityView)
-> ReduceM (Arg Term) -> ReduceM (Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
a
    ReduceM (Arg Term -> EqualityView)
-> ReduceM (Arg Term) -> ReduceM EqualityView
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
b

---------------------------------------------------------------------------
-- * Reduction to weak head normal form.
---------------------------------------------------------------------------

-- | Is something (an elimination of) a meta variable?
--   Does not perform any reductions.

class IsMeta a where
  isMeta :: a -> Maybe MetaId

instance IsMeta Term where
  isMeta :: Term -> Maybe MetaId
isMeta (MetaV MetaId
m Elims
_) = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
m
  isMeta Term
_           = Maybe MetaId
forall a. Maybe a
Nothing

instance IsMeta a => IsMeta (Sort' a) where
  isMeta :: Sort' a -> Maybe MetaId
isMeta (MetaS MetaId
m [Elim' a]
_) = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
m
  isMeta Sort' a
_           = Maybe MetaId
forall a. Maybe a
Nothing

instance IsMeta a => IsMeta (Type'' t a) where
  isMeta :: Type'' t a -> Maybe MetaId
isMeta = a -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta (a -> Maybe MetaId)
-> (Type'' t a -> a) -> Type'' t a -> Maybe MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' t a -> a
forall t a. Type'' t a -> a
unEl

instance IsMeta a => IsMeta (Elim' a) where
  isMeta :: Elim' a -> Maybe MetaId
isMeta Proj{}    = Maybe MetaId
forall a. Maybe a
Nothing
  isMeta IApply{}  = Maybe MetaId
forall a. Maybe a
Nothing
  isMeta (Apply Arg a
a) = Arg a -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta Arg a
a

instance IsMeta a => IsMeta (Arg a) where
  isMeta :: Arg a -> Maybe MetaId
isMeta = a -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta (a -> Maybe MetaId) -> (Arg a -> a) -> Arg a -> Maybe MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance IsMeta a => IsMeta (Level' a) where
  isMeta :: Level' a -> Maybe MetaId
isMeta (Max Integer
0 [PlusLevel' a
l]) = PlusLevel' a -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta PlusLevel' a
l
  isMeta Level' a
_           = Maybe MetaId
forall a. Maybe a
Nothing

instance IsMeta a => IsMeta (PlusLevel' a) where
  isMeta :: PlusLevel' a -> Maybe MetaId
isMeta (Plus Integer
0 a
l)  = a -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta a
l
  isMeta PlusLevel' a
_           = Maybe MetaId
forall a. Maybe a
Nothing

instance IsMeta CompareAs where
  isMeta :: CompareAs -> Maybe MetaId
isMeta (AsTermsOf Type
a) = Type -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta Type
a
  isMeta CompareAs
AsSizes       = Maybe MetaId
forall a. Maybe a
Nothing
  isMeta CompareAs
AsTypes       = Maybe MetaId
forall a. Maybe a
Nothing

-- | Case on whether a term is blocked on a meta (or is a meta).
--   That means it can change its shape when the meta is instantiated.
ifBlocked
  :: (Reduce t, IsMeta t, MonadReduce m)
  => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked :: forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked t
t Blocker -> t -> m a
blocked NotBlocked -> t -> m a
unblocked = do
  Blocked t
t <- t -> m (Blocked t)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB t
t
  case Blocked t
t of
    Blocked Blocker
m t
t     -> Blocker -> t -> m a
blocked Blocker
m t
t
    NotBlocked NotBlocked
nb t
t -> case t -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta t
t of -- #4899: MetaS counts as NotBlocked at the moment
      Just MetaId
m    -> Blocker -> t -> m a
blocked (MetaId -> Blocker
unblockOnMeta MetaId
m) t
t
      Maybe MetaId
Nothing   -> NotBlocked -> t -> m a
unblocked NotBlocked
nb t
t

-- | Throw pattern violation if blocked or a meta.
abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t
abortIfBlocked :: forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked t
t = t -> (Blocker -> t -> m t) -> (NotBlocked -> t -> m t) -> m t
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked t
t (m t -> t -> m t
forall a b. a -> b -> a
const (m t -> t -> m t) -> (Blocker -> m t) -> Blocker -> t -> m t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> m t
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation) ((t -> m t) -> NotBlocked -> t -> m t
forall a b. a -> b -> a
const t -> m t
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)

isBlocked
  :: (Reduce t, IsMeta t, MonadReduce m)
  => t -> m (Maybe Blocker)
isBlocked :: forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked t
t = t
-> (Blocker -> t -> m (Maybe Blocker))
-> (NotBlocked -> t -> m (Maybe Blocker))
-> m (Maybe Blocker)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked t
t (\Blocker
m t
_ -> Maybe Blocker -> m (Maybe Blocker)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocker -> m (Maybe Blocker))
-> Maybe Blocker -> m (Maybe Blocker)
forall a b. (a -> b) -> a -> b
$ Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
m) (\NotBlocked
_ t
_ -> Maybe Blocker -> m (Maybe Blocker)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Blocker
forall a. Maybe a
Nothing)

-- | Throw a pattern violation if the argument is @Blocked@,
--   otherwise return the value embedded in the @NotBlocked@.
fromBlocked :: MonadBlock m => Blocked a -> m a
fromBlocked :: forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked (Blocked Blocker
b a
_) = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
b
fromBlocked (NotBlocked NotBlocked
_ a
x) = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

class Reduce t where
  reduce'  :: t -> ReduceM t
  reduceB' :: t -> ReduceM (Blocked t)

  reduce'  t
t = Blocked t -> t
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked t -> t) -> ReduceM (Blocked t) -> ReduceM t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> ReduceM (Blocked t)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' t
t
  reduceB' t
t = t -> Blocked t
forall a t. a -> Blocked' t a
notBlocked (t -> Blocked t) -> ReduceM t -> ReduceM (Blocked t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce' t
t

instance Reduce Type where
    reduce' :: Type -> ReduceM Type
reduce'  (El Sort
s Term
t) = ReduceM Type -> ReduceM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (ReduceM Type -> ReduceM Type) -> ReduceM Type -> ReduceM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> ReduceM Term -> ReduceM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t
    reduceB' :: Type -> ReduceM (Blocked Type)
reduceB' (El Sort
s Term
t) = ReduceM (Blocked Type) -> ReduceM (Blocked Type)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (ReduceM (Blocked Type) -> ReduceM (Blocked Type))
-> ReduceM (Blocked Type) -> ReduceM (Blocked Type)
forall a b. (a -> b) -> a -> b
$ (Term -> Type) -> Blocked' Term Term -> Blocked Type
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s) (Blocked' Term Term -> Blocked Type)
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
t

instance Reduce Sort where
    reduceB' :: Sort -> ReduceM (Blocked Sort)
reduceB' Sort
s = do
      Sort
s <- Sort -> ReduceM Sort
forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
      let done :: ReduceM (Blocked Sort)
done | MetaS MetaId
x Elims
_ <- Sort
s = Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ MetaId -> Sort -> Blocked Sort
forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Sort
s
               | Bool
otherwise      = Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Blocked Sort
forall a t. a -> Blocked' t a
notBlocked Sort
s
      case Sort
s of
        PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> (Sort, Abs Sort) -> ReduceM (Blocked (Sort, Abs Sort))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Sort
s1 , Abs Sort
s2) ReduceM (Blocked (Sort, Abs Sort))
-> (Blocked (Sort, Abs Sort) -> ReduceM (Blocked Sort))
-> ReduceM (Blocked Sort)
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b (Sort
s1',Abs Sort
s2') -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
s1' Abs Sort
s2'
          NotBlocked NotBlocked
_ (Sort
s1',Abs Sort
s2') -> do
            -- Jesper, 2022-10-12: do instantiateFull here because
            -- `piSort'` does checking of free variables, and if we
            -- don't instantiate we might end up blocking on a solved
            -- metavariable.
            Abs Sort
s2' <- Abs Sort -> ReduceM (Abs Sort)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Abs Sort
s2'
            case Dom' Term Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' Dom' Term Term
a Sort
s1' Abs Sort
s2' of
              Left Blocker
b -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
s1' Abs Sort
s2'
              Right Sort
s -> Sort -> ReduceM (Blocked Sort)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        FunSort Sort
s1 Sort
s2 -> (Sort, Sort) -> ReduceM (Blocked (Sort, Sort))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Sort
s1 , Sort
s2) ReduceM (Blocked (Sort, Sort))
-> (Blocked (Sort, Sort) -> ReduceM (Blocked Sort))
-> ReduceM (Blocked Sort)
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b (Sort
s1',Sort
s2') -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
          NotBlocked NotBlocked
_ (Sort
s1',Sort
s2') -> do
            case Sort -> Sort -> Either Blocker Sort
funSort' Sort
s1' Sort
s2' of
              Left Blocker
b -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
              Right Sort
s -> Sort -> ReduceM (Blocked Sort)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        UnivSort Sort
s1 -> Sort -> ReduceM (Blocked Sort)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s1 ReduceM (Blocked Sort)
-> (Blocked Sort -> ReduceM (Blocked Sort))
-> ReduceM (Blocked Sort)
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b Sort
s1' -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s1'
          NotBlocked NotBlocked
_ Sort
s1' -> case Sort -> Either Blocker Sort
univSort' Sort
s1' of
            Left Blocker
b -> Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Blocker -> Sort -> Blocked Sort
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (Sort -> Blocked Sort) -> Sort -> Blocked Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s1'
            Right Sort
s -> Sort -> ReduceM (Blocked Sort)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        Univ Univ
u Level
l   -> Sort -> Blocked Sort
forall a t. a -> Blocked' t a
notBlocked (Sort -> Blocked Sort) -> (Level -> Sort) -> Level -> Blocked Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Blocked Sort) -> ReduceM Level -> ReduceM (Blocked Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReduceM Level
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Level
l
        Inf Univ
_ Integer
_    -> ReduceM (Blocked Sort)
done
        Sort
SizeUniv   -> ReduceM (Blocked Sort)
done
        Sort
LockUniv   -> ReduceM (Blocked Sort)
done
        Sort
LevelUniv  -> do
          Bool
levelUniverseEnabled <- ReduceM Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
          if Bool
levelUniverseEnabled
          then ReduceM (Blocked Sort)
done
          else Blocked Sort -> ReduceM (Blocked Sort)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Sort -> ReduceM (Blocked Sort))
-> Blocked Sort -> ReduceM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Blocked Sort
forall a t. a -> Blocked' t a
notBlocked (Integer -> Sort
mkType Integer
0)
        Sort
IntervalUniv -> ReduceM (Blocked Sort)
done
        MetaS MetaId
x Elims
es -> ReduceM (Blocked Sort)
done
        DefS QName
d Elims
es  -> ReduceM (Blocked Sort)
done -- postulated sorts do not reduce
        DummyS{}   -> ReduceM (Blocked Sort)
done

instance Reduce Elim where
  reduce' :: Elim -> ReduceM Elim
reduce' (Apply Arg Term
v) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> ReduceM (Arg Term) -> ReduceM Elim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
v
  reduce' (Proj ProjOrigin
o QName
f)= Elim -> ReduceM Elim
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elim -> ReduceM Elim) -> Elim -> ReduceM Elim
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f
  reduce' (IApply Term
x Term
y Term
v) = Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply (Term -> Term -> Term -> Elim)
-> ReduceM Term -> ReduceM (Term -> Term -> Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
x ReduceM (Term -> Term -> Elim)
-> ReduceM Term -> ReduceM (Term -> Elim)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
y ReduceM (Term -> Elim) -> ReduceM Term -> ReduceM Elim
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
v

instance Reduce Level where
  reduce' :: Level -> ReduceM Level
reduce'  (Max Integer
m [PlusLevel]
as) = Integer -> [PlusLevel] -> Level
levelMax Integer
m ([PlusLevel] -> Level) -> ReduceM [PlusLevel] -> ReduceM Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PlusLevel -> ReduceM PlusLevel)
-> [PlusLevel] -> ReduceM [PlusLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM PlusLevel -> ReduceM PlusLevel
forall t. Reduce t => t -> ReduceM t
reduce' [PlusLevel]
as
  reduceB' :: Level -> ReduceM (Blocked Level)
reduceB' (Max Integer
m [PlusLevel]
as) = ([PlusLevel] -> Level)
-> Blocked' Term [PlusLevel] -> Blocked Level
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> [PlusLevel] -> Level
levelMax Integer
m) (Blocked' Term [PlusLevel] -> Blocked Level)
-> ([Blocked PlusLevel] -> Blocked' Term [PlusLevel])
-> [Blocked PlusLevel]
-> Blocked Level
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocked PlusLevel] -> Blocked' Term [PlusLevel]
forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAny ([Blocked PlusLevel] -> Blocked Level)
-> ReduceM [Blocked PlusLevel] -> ReduceM (Blocked Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PlusLevel -> ReduceM (Blocked PlusLevel))
-> [PlusLevel] -> ReduceM [Blocked PlusLevel]
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 PlusLevel -> ReduceM (Blocked PlusLevel)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' [PlusLevel]
as

instance Reduce PlusLevel where
  reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel)
reduceB' (Plus Integer
n Term
l) = (Term -> PlusLevel) -> Blocked' Term Term -> Blocked PlusLevel
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Term -> PlusLevel
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) (Blocked' Term Term -> Blocked PlusLevel)
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked PlusLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
l

instance (Subst a, Reduce a) => Reduce (Abs a) where
  reduceB' :: Abs a -> ReduceM (Blocked (Abs a))
reduceB' b :: Abs a
b@(Abs [Char]
x a
_) = (a -> Abs a) -> Blocked' Term a -> Blocked (Abs a)
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
Abs [Char]
x) (Blocked' Term a -> Blocked (Abs a))
-> ReduceM (Blocked' Term a) -> ReduceM (Blocked (Abs a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs a
-> (a -> ReduceM (Blocked' Term a)) -> ReduceM (Blocked' Term a)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
b a -> ReduceM (Blocked' Term a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'
  reduceB' (NoAbs [Char]
x a
v) = (a -> Abs a) -> Blocked' Term a -> Blocked (Abs a)
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x) (Blocked' Term a -> Blocked (Abs a))
-> ReduceM (Blocked' Term a) -> ReduceM (Blocked (Abs a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM (Blocked' Term a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' a
v

-- Lists are never blocked
instance Reduce t => Reduce [t] where
    reduce' :: [t] -> ReduceM [t]
reduce' = (t -> ReduceM t) -> [t] -> ReduceM [t]
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 t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce'

-- Maybes are never blocked
instance Reduce t => Reduce (Maybe t) where
    reduce' :: Maybe t -> ReduceM (Maybe t)
reduce' = (t -> ReduceM t) -> Maybe t -> ReduceM (Maybe t)
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) -> Maybe a -> f (Maybe b)
traverse t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce'

instance Reduce t => Reduce (Arg t) where
    reduce' :: Arg t -> ReduceM (Arg t)
reduce' Arg t
a = case Arg t -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg t
a of
      Relevance
Irrelevant -> Arg t -> ReduceM (Arg t)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Arg t
a             -- Don't reduce' irr. args!?
                                         -- Andreas, 2018-03-03, caused #2989.
      Relevance
_          -> (t -> ReduceM t) -> Arg t -> ReduceM (Arg t)
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 t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce' Arg t
a

    reduceB' :: Arg t -> ReduceM (Blocked (Arg t))
reduceB' Arg t
t = (Blocked' Term t -> Blocked' Term t)
-> Arg (Blocked' Term t) -> Blocked (Arg t)
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 Blocked' Term t -> Blocked' Term t
forall a. a -> a
id (Arg (Blocked' Term t) -> Blocked (Arg t))
-> ReduceM (Arg (Blocked' Term t)) -> ReduceM (Blocked (Arg t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t -> ReduceM (Blocked' Term t))
-> Arg t -> ReduceM (Arg (Blocked' Term t))
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 t -> ReduceM (Blocked' Term t)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg t
t

instance Reduce t => Reduce (Dom t) where
    reduce' :: Dom t -> ReduceM (Dom t)
reduce' = (t -> ReduceM t) -> Dom t -> ReduceM (Dom t)
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 t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce'
    reduceB' :: Dom t -> ReduceM (Blocked (Dom t))
reduceB' Dom t
t = (Blocked' Term t -> Blocked' Term t)
-> Dom' Term (Blocked' Term t) -> Blocked (Dom t)
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 Blocked' Term t -> Blocked' Term t
forall a. a -> a
id (Dom' Term (Blocked' Term t) -> Blocked (Dom t))
-> ReduceM (Dom' Term (Blocked' Term t))
-> ReduceM (Blocked (Dom t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t -> ReduceM (Blocked' Term t))
-> Dom t -> ReduceM (Dom' Term (Blocked' Term t))
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 t -> ReduceM (Blocked' Term t)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Dom t
t

instance (Reduce a, Reduce b) => Reduce (a,b) where
    reduce' :: (a, b) -> ReduceM (a, b)
reduce' (a
x,b
y)  = (,) (a -> b -> (a, b)) -> ReduceM a -> ReduceM (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Reduce t => t -> ReduceM t
reduce' a
x ReduceM (b -> (a, b)) -> ReduceM b -> ReduceM (a, b)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM b
forall t. Reduce t => t -> ReduceM t
reduce' b
y
    reduceB' :: (a, b) -> ReduceM (Blocked (a, b))
reduceB' (a
x,b
y) = do
      Blocked a
x <- a -> ReduceM (Blocked a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' a
x
      Blocked b
y <- b -> ReduceM (Blocked b)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' b
y
      let blk :: Blocked' Term ()
blk = Blocked a -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked a
x Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` Blocked b -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked b
y
          xy :: (a, b)
xy  = (Blocked a -> a
forall t a. Blocked' t a -> a
ignoreBlocking Blocked a
x , Blocked b -> b
forall t a. Blocked' t a -> a
ignoreBlocking Blocked b
y)
      Blocked (a, b) -> ReduceM (Blocked (a, b))
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked (a, b) -> ReduceM (Blocked (a, b)))
-> Blocked (a, b) -> ReduceM (Blocked (a, b))
forall a b. (a -> b) -> a -> b
$ Blocked' Term ()
blk Blocked' Term () -> (a, b) -> Blocked (a, b)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (a, b)
xy

instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where
    reduce' :: (a, b, c) -> ReduceM (a, b, c)
reduce' (a
x,b
y,c
z) = (,,) (a -> b -> c -> (a, b, c))
-> ReduceM a -> ReduceM (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Reduce t => t -> ReduceM t
reduce' a
x ReduceM (b -> c -> (a, b, c))
-> ReduceM b -> ReduceM (c -> (a, b, c))
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM b
forall t. Reduce t => t -> ReduceM t
reduce' b
y ReduceM (c -> (a, b, c)) -> ReduceM c -> ReduceM (a, b, c)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> ReduceM c
forall t. Reduce t => t -> ReduceM t
reduce' c
z
    reduceB' :: (a, b, c) -> ReduceM (Blocked (a, b, c))
reduceB' (a
x,b
y,c
z) = do
      Blocked a
x <- a -> ReduceM (Blocked a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' a
x
      Blocked b
y <- b -> ReduceM (Blocked b)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' b
y
      Blocked c
z <- c -> ReduceM (Blocked c)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' c
z
      let blk :: Blocked' Term ()
blk = Blocked a -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked a
x Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` Blocked b -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked b
y Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` Blocked c -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked c
z
          xyz :: (a, b, c)
xyz = (Blocked a -> a
forall t a. Blocked' t a -> a
ignoreBlocking Blocked a
x , Blocked b -> b
forall t a. Blocked' t a -> a
ignoreBlocking Blocked b
y , Blocked c -> c
forall t a. Blocked' t a -> a
ignoreBlocking Blocked c
z)
      Blocked (a, b, c) -> ReduceM (Blocked (a, b, c))
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked (a, b, c) -> ReduceM (Blocked (a, b, c)))
-> Blocked (a, b, c) -> ReduceM (Blocked (a, b, c))
forall a b. (a -> b) -> a -> b
$ Blocked' Term ()
blk Blocked' Term () -> (a, b, c) -> Blocked (a, b, c)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (a, b, c)
xyz

reduceIApply :: ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
reduceIApply :: ReduceM (Blocked' Term Term)
-> Elims -> ReduceM (Blocked' Term Term)
reduceIApply = (Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> Elims
-> ReduceM (Blocked' Term Term)
reduceIApply' Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'

reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
reduceIApply' :: (Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> Elims
-> ReduceM (Blocked' Term Term)
reduceIApply' Term -> ReduceM (Blocked' Term Term)
red ReduceM (Blocked' Term Term)
d (IApply Term
x Term
y Term
r : Elims
es) = do
  Term -> IntervalView
view <- ReduceM (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Blocked' Term Term
r <- Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
r
  -- We need to propagate the blocking information so that e.g.
  -- we postpone "someNeutralPath ?0 = a" rather than fail.
  case Term -> IntervalView
view (Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term Term
r) of
   IntervalView
IZero -> Term -> ReduceM (Blocked' Term Term)
red (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
x Elims
es)
   IntervalView
IOne  -> Term -> ReduceM (Blocked' Term Term)
red (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
y Elims
es)
   IntervalView
_     -> (Blocked' Term Term -> Blocked' Term Term)
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Blocked' Term Term -> Blocked' Term Term -> Blocked' Term Term
forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Blocked' Term Term
r) ((Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> Elims
-> ReduceM (Blocked' Term Term)
reduceIApply' Term -> ReduceM (Blocked' Term Term)
red ReduceM (Blocked' Term Term)
d Elims
es)
reduceIApply' Term -> ReduceM (Blocked' Term Term)
red ReduceM (Blocked' Term Term)
d (Elim
_ : Elims
es) = (Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> Elims
-> ReduceM (Blocked' Term Term)
reduceIApply' Term -> ReduceM (Blocked' Term Term)
red ReduceM (Blocked' Term Term)
d Elims
es
reduceIApply' Term -> ReduceM (Blocked' Term Term)
_   ReduceM (Blocked' Term Term)
d [] = ReduceM (Blocked' Term Term)
d

instance Reduce DeBruijnPattern where
  reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern)
reduceB' (DotP PatternInfo
o Term
v) = (Term -> DeBruijnPattern)
-> Blocked' Term Term -> Blocked DeBruijnPattern
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o) (Blocked' Term Term -> Blocked DeBruijnPattern)
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
v
  reduceB' DeBruijnPattern
p          = Blocked DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern))
-> Blocked DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Blocked DeBruijnPattern
forall a t. a -> Blocked' t a
notBlocked DeBruijnPattern
p

instance Reduce Term where
  reduceB' :: Term -> ReduceM (Blocked' Term Term)
reduceB' = {-# SCC "reduce'<Term>" #-} Term -> ReduceM (Blocked' Term Term)
maybeFastReduceTerm

shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce = PragmaOptions -> Bool
optFastReduce (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
maybeFastReduceTerm :: Term -> ReduceM (Blocked' Term Term)
maybeFastReduceTerm Term
v = do
  let tryFast :: Bool
tryFast = case Term
v of
                  Def{}   -> Bool
True
                  Con{}   -> Bool
True
                  MetaV{} -> Bool
True
                  Term
_       -> Bool
False
  if Bool -> Bool
not Bool
tryFast then Term -> ReduceM (Blocked' Term Term)
slowReduceTerm Term
v
                 else
    case Term
v of
      MetaV MetaId
x Elims
_ -> ReduceM Bool
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> ReduceM Bool
forall {f :: * -> *}. ReadTCState f => MetaId -> f Bool
isOpen MetaId
x) (Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> Blocked' Term Term
forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Term
v) (Term -> ReduceM (Blocked' Term Term)
maybeFast Term
v)
      Term
_         -> Term -> ReduceM (Blocked' Term Term)
maybeFast Term
v
  where
    isOpen :: MetaId -> f Bool
isOpen MetaId
x = MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> f MetaInstantiation -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
    maybeFast :: Term -> ReduceM (Blocked' Term Term)
maybeFast Term
v = ReduceM Bool
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ReduceM Bool
shouldTryFastReduce (Term -> ReduceM (Blocked' Term Term)
fastReduce Term
v) (Term -> ReduceM (Blocked' Term Term)
slowReduceTerm Term
v)

slowReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm :: Term -> ReduceM (Blocked' Term Term)
slowReduceTerm Term
v = do
    Term
v <- Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
    let done :: ReduceM (Blocked' Term Term)
done | MetaV MetaId
x Elims
_ <- Term
v = Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> Blocked' Term Term
forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Term
v
             | Bool
otherwise      = Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked Term
v
        iapp :: Elims -> ReduceM (Blocked' Term Term)
iapp = ReduceM (Blocked' Term Term)
-> Elims -> ReduceM (Blocked' Term Term)
reduceIApply ReduceM (Blocked' Term Term)
done
    case Term
v of
--    Andreas, 2012-11-05 not reducing meta args does not destroy anything
--    and seems to save 2% sec on the standard library
--      MetaV x args -> notBlocked . MetaV x <$> reduce' args
      MetaV MetaId
x Elims
es -> Elims -> ReduceM (Blocked' Term Term)
iapp Elims
es
      Def QName
f Elims
es   -> (ReduceM (Blocked' Term Term)
 -> Elims -> ReduceM (Blocked' Term Term))
-> Elims
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReduceM (Blocked' Term Term)
-> Elims -> ReduceM (Blocked' Term Term)
reduceIApply Elims
es (ReduceM (Blocked' Term Term) -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (QName -> Elims -> Term
Def QName
f []) QName
f Elims
es
      Con ConHead
c ConInfo
ci Elims
es -> do
          -- Constructors can reduce' when they come from an
          -- instantiated module.
          -- also reduce when they are path constructors
          Blocked' Term Term
v <- (ReduceM (Blocked' Term Term)
 -> Elims -> ReduceM (Blocked' Term Term))
-> Elims
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReduceM (Blocked' Term Term)
-> Elims -> ReduceM (Blocked' Term Term)
reduceIApply Elims
es
                 (ReduceM (Blocked' Term Term) -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) (ConHead -> QName
conName ConHead
c) Elims
es
          (Term -> ReduceM Term)
-> Blocked' Term Term -> ReduceM (Blocked' Term Term)
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) -> Blocked' Term a -> f (Blocked' Term b)
traverse Term -> ReduceM Term
reduceNat Blocked' Term Term
v
      Sort Sort
s   -> ReduceM (Blocked' Term Term)
done
      Level Level
l  -> ReduceM Bool
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
-> ReduceM (Blocked' Term Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.member AllowedReduction
LevelReductions (SmallSet AllowedReduction -> Bool)
-> ReduceM (SmallSet AllowedReduction) -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> SmallSet AllowedReduction)
-> ReduceM (SmallSet AllowedReduction)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions)
                    {- then -} ((Level -> Term) -> Blocked Level -> Blocked' Term Term
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Term
levelTm (Blocked Level -> Blocked' Term Term)
-> ReduceM (Blocked Level) -> ReduceM (Blocked' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReduceM (Blocked Level)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Level
l)
                    {- else -} ReduceM (Blocked' Term Term)
done
      Pi Dom Type
_ Abs Type
_   -> ReduceM (Blocked' Term Term)
done
      Lit Literal
_    -> ReduceM (Blocked' Term Term)
done
      Var Int
_ Elims
es  -> Elims -> ReduceM (Blocked' Term Term)
iapp Elims
es
      Lam ArgInfo
_ Abs Term
_  -> ReduceM (Blocked' Term Term)
done
      DontCare Term
_ -> ReduceM (Blocked' Term Term)
done
      Dummy{}    -> ReduceM (Blocked' Term Term)
done
    where
      -- NOTE: reduceNat can traverse the entire term.
      reduceNat :: Term -> ReduceM Term
reduceNat v :: Term
v@(Con ConHead
c ConInfo
ci []) = do
        Maybe Term
mz  <- BuiltinId -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
        case Term
v of
          Term
_ | Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
mz  -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Literal
LitNat Integer
0
          Term
_                 -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
      reduceNat v :: Term
v@(Con ConHead
c ConInfo
ci [Apply Arg Term
a]) | Arg Term -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Term
a Bool -> Bool -> Bool
&& Arg Term -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant Arg Term
a = do
        Maybe Term
ms  <- BuiltinId -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc
        case Term
v of
          Term
_ | Term -> Maybe Term
forall a. a -> Maybe a
Just (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
ms -> Term -> Term
inc (Term -> Term) -> ReduceM Term -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
          Term
_                         -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          where
            inc :: Term -> Term
inc = \case
              Lit (LitNat Integer
n) -> Literal -> Term
Lit (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Literal
LitNat (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
              Term
w              -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
w]
      reduceNat Term
v = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- Andreas, 2013-03-20 recursive invokations of unfoldCorecursion
-- need also to instantiate metas, see Issue 826.
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE (Proj ProjOrigin
o QName
p)           = Elim -> Blocked Elim
forall a t. a -> Blocked' t a
notBlocked (Elim -> Blocked Elim) -> (QName -> Elim) -> QName -> Blocked Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o (QName -> Blocked Elim) -> ReduceM QName -> ReduceM (Blocked Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
p
unfoldCorecursionE (Apply (Arg ArgInfo
info Term
v)) = (Term -> Elim) -> Blocked' Term Term -> Blocked Elim
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Term -> Arg Term) -> Term -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info) (Blocked' Term Term -> Blocked Elim)
-> ReduceM (Blocked' Term Term) -> ReduceM (Blocked Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  Term -> ReduceM (Blocked' Term Term)
unfoldCorecursion Term
v
unfoldCorecursionE (IApply Term
x Term
y Term
r) = do -- TODO check if this makes sense
   [Blocked' Term Term
x,Blocked' Term Term
y,Blocked' Term Term
r] <- (Term -> ReduceM (Blocked' Term Term))
-> [Term] -> ReduceM [Blocked' Term Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term -> ReduceM (Blocked' Term Term)
unfoldCorecursion [Term
x,Term
y,Term
r]
   Blocked Elim -> ReduceM (Blocked Elim)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Elim -> ReduceM (Blocked Elim))
-> Blocked Elim -> ReduceM (Blocked Elim)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply (Term -> Term -> Term -> Elim)
-> Blocked' Term Term -> Blocked' Term (Term -> Term -> Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked' Term Term
x Blocked' Term (Term -> Term -> Elim)
-> Blocked' Term Term -> Blocked' Term (Term -> Elim)
forall a b.
Blocked' Term (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Blocked' Term Term
y Blocked' Term (Term -> Elim) -> Blocked' Term Term -> Blocked Elim
forall a b.
Blocked' Term (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Blocked' Term Term
r

unfoldCorecursion :: Term -> ReduceM (Blocked Term)
unfoldCorecursion :: Term -> ReduceM (Blocked' Term Term)
unfoldCorecursion Term
v = do
  Term
v <- Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
  case Term
v of
    Def QName
f Elims
es -> (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
unfoldCorecursion (QName -> Elims -> Term
Def QName
f []) QName
f Elims
es
    Term
_ -> Term -> ReduceM (Blocked' Term Term)
slowReduceTerm Term
v

-- | If the first argument is 'True', then a single delayed clause may
-- be unfolded.
unfoldDefinition ::
  (Term -> ReduceM (Blocked Term)) ->
  Term -> QName -> Args -> ReduceM (Blocked Term)
unfoldDefinition :: (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> [Arg Term] -> ReduceM (Blocked' Term Term)
unfoldDefinition Term -> ReduceM (Blocked' Term Term)
keepGoing Term
v QName
f [Arg Term]
args =
  (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
keepGoing Term
v QName
f ((Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)

unfoldDefinitionE ::
  (Term -> ReduceM (Blocked Term)) ->
  Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinitionE :: (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
keepGoing Term
v QName
f Elims
es = do
  Reduced (Blocked' Term Term) Term
r <- Term
-> QName -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
unfoldDefinitionStep Term
v QName
f Elims
es
  case Reduced (Blocked' Term Term) Term
r of
    NoReduction Blocked' Term Term
v    -> Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked' Term Term
v
    YesReduction Simplification
_ Term
v -> Term -> ReduceM (Blocked' Term Term)
keepGoing Term
v

unfoldDefinition' ::
  (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) ->
  Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
unfoldDefinition' :: (Simplification
 -> Term -> ReduceM (Simplification, Blocked' Term Term))
-> Term
-> QName
-> Elims
-> ReduceM (Simplification, Blocked' Term Term)
unfoldDefinition' Simplification
-> Term -> ReduceM (Simplification, Blocked' Term Term)
keepGoing Term
v0 QName
f Elims
es = do
  Reduced (Blocked' Term Term) Term
r <- Term
-> QName -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
unfoldDefinitionStep Term
v0 QName
f Elims
es
  case Reduced (Blocked' Term Term) Term
r of
    NoReduction Blocked' Term Term
v       -> (Simplification, Blocked' Term Term)
-> ReduceM (Simplification, Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification
NoSimplification, Blocked' Term Term
v)
    YesReduction Simplification
simp Term
v -> Simplification
-> Term -> ReduceM (Simplification, Blocked' Term Term)
keepGoing Simplification
simp Term
v

unfoldDefinitionStep :: Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep :: Term
-> QName -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
unfoldDefinitionStep Term
v0 QName
f Elims
es =
  {-# SCC "reduceDef" #-} do
  [Char]
-> Int
-> TCMT IO Doc
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.reduce" Int
90 (TCMT IO Doc
"unfoldDefinitionStep v0" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v0) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ do
  Definition
info <- QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  RewriteRules
rewr <- RewriteRules -> ReduceM RewriteRules
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRules -> m RewriteRules
instantiateRewriteRules (RewriteRules -> ReduceM RewriteRules)
-> ReduceM RewriteRules -> ReduceM RewriteRules
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> ReduceM RewriteRules
forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
f
  SmallSet AllowedReduction
allowed <- (TCEnv -> SmallSet AllowedReduction)
-> ReduceM (SmallSet AllowedReduction)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions
  Either Blocker Bool
prp <- BlockT ReduceM Bool -> ReduceM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT ReduceM Bool -> ReduceM (Either Blocker Bool))
-> BlockT ReduceM Bool -> ReduceM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type -> BlockT ReduceM Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM (Type -> BlockT ReduceM Bool) -> Type -> BlockT ReduceM Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
info
  Bool
defOk <- QName -> ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
shouldReduceDef QName
f
  let def :: Defn
def = Definition -> Defn
theDef Definition
info
      v :: Term
v   = Term
v0 Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
      -- Non-terminating functions
      -- (i.e., those that failed the termination check)
      -- and delayed definitions
      -- are not unfolded unless explicitly permitted.
      dontUnfold :: Bool
dontUnfold = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
        [ Definition -> Bool
defNonterminating Definition
info Bool -> Bool -> Bool
&& AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.notMember AllowedReduction
NonTerminatingReductions SmallSet AllowedReduction
allowed
        , Definition -> Bool
defTerminationUnconfirmed Definition
info Bool -> Bool -> Bool
&& AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.notMember AllowedReduction
UnconfirmedReductions SmallSet AllowedReduction
allowed
        , Either Blocker Bool
prp Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True
        , Definition -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
info
        , Bool -> Bool
not Bool
defOk
        ]
      copatterns :: Bool
copatterns = Definition -> Bool
defCopatternLHS Definition
info
  case Defn
def of
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c} -> do
      let hd :: Elims -> Term
hd = ConHead -> ConInfo -> Elims -> Term
Con (ConHead
c ConHead -> QName -> ConHead
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
f) ConInfo
ConOSystem
      Blocked' Term ()
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
rewrite (NotBlocked -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
forall t. NotBlocked' t
ReallyNotBlocked ()) Elims -> Term
hd RewriteRules
rewr Elims
es
    Primitive{primAbstr :: Defn -> IsAbstract
primAbstr = IsAbstract
ConcreteDef, primName :: Defn -> PrimitiveId
primName = PrimitiveId
x, primClauses :: Defn -> [Clause]
primClauses = [Clause]
cls} -> do
      PrimFun
pf <- PrimFun -> Maybe PrimFun -> PrimFun
forall a. a -> Maybe a -> a
fromMaybe PrimFun
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe PrimFun -> PrimFun)
-> ReduceM (Maybe PrimFun) -> ReduceM PrimFun
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimitiveId -> ReduceM (Maybe PrimFun)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe PrimFun)
getPrimitive' PrimitiveId
x
      if AllowedReduction
FunctionReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
        then PrimitiveId
-> Term
-> QName
-> Elims
-> PrimFun
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> ReduceM (Reduced (Blocked' Term Term) Term)
reducePrimitive PrimitiveId
x Term
v0 QName
f Elims
es PrimFun
pf Bool
dontUnfold
                             [Clause]
cls (Definition -> Maybe CompiledClauses
defCompiled Definition
info) RewriteRules
rewr
        else Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked Term
v
    PrimitiveSort{ primSortSort :: Defn -> Sort
primSortSort = Sort
s } -> Simplification
-> Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {m :: * -> *} {a} {no}.
Monad m =>
Simplification -> a -> m (Reduced no a)
yesReduction Simplification
NoSimplification (Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es

    Defn
_  -> do
      if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
          [ AllowedReduction
RecursiveReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
          , Maybe Projection -> Bool
forall a. Maybe a -> Bool
isJust (Defn -> Maybe Projection
isProjection_ Defn
def) Bool -> Bool -> Bool
&& AllowedReduction
ProjectionReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
              -- Includes projection-like and irrelevant projections.
              -- Note: irrelevant projections lead to @dontUnfold@ and
              -- so are not actually unfolded.
          , Defn -> Bool
isInlineFun Defn
def Bool -> Bool -> Bool
&& AllowedReduction
InlineReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
          , Defn -> Bool
definitelyNonRecursive_ Defn
def Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
            [ Bool
copatterns Bool -> Bool -> Bool
&& AllowedReduction
CopatternReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
            , AllowedReduction
FunctionReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
            ]
          ]
        then
          Term
-> QName
-> [MaybeReduced Elim]
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> ReduceM (Reduced (Blocked' Term Term) Term)
reduceNormalE Term
v0 QName
f ((Elim -> MaybeReduced Elim) -> Elims -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> MaybeReduced Elim
forall a. a -> MaybeReduced a
notReduced Elims
es) Bool
dontUnfold
                       (Definition -> [Clause]
defClauses Definition
info) (Definition -> Maybe CompiledClauses
defCompiled Definition
info) RewriteRules
rewr
        else Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked Term
v  -- Andrea(s), 2014-12-05 OK?

  where
    noReduction :: a -> ReduceM (Reduced a yes)
noReduction    = Reduced a yes -> ReduceM (Reduced a yes)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced a yes -> ReduceM (Reduced a yes))
-> (a -> Reduced a yes) -> a -> ReduceM (Reduced a yes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Reduced a yes
forall no yes. no -> Reduced no yes
NoReduction
    yesReduction :: Simplification -> a -> m (Reduced no a)
yesReduction Simplification
s = Reduced no a -> m (Reduced no a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced no a -> m (Reduced no a))
-> (a -> Reduced no a) -> a -> m (Reduced no a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Simplification -> a -> Reduced no a
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
s
    reducePrimitive :: PrimitiveId
-> Term
-> QName
-> Elims
-> PrimFun
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> ReduceM (Reduced (Blocked' Term Term) Term)
reducePrimitive PrimitiveId
x Term
v0 QName
f Elims
es PrimFun
pf Bool
dontUnfold [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr
      | Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
ar
                  = Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ NotBlocked -> Term -> Blocked' Term Term
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
forall t. NotBlocked' t
Underapplied (Term -> Blocked' Term Term) -> Term -> Blocked' Term Term
forall a b. (a -> b) -> a -> b
$ Term
v0 Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es -- not fully applied
      | Bool
otherwise = {-# SCC "reducePrimitive" #-} do
          let (Elims
es1,Elims
es2) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
ar Elims
es
              args1 :: [Arg Term]
args1     = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Elim -> Maybe (Arg Term)) -> Elims -> Maybe [Arg Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es1
          Reduced MaybeReducedArgs Term
r <- PrimFun
-> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
primFunImplementation PrimFun
pf [Arg Term]
args1 (Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es2)
          case Reduced MaybeReducedArgs Term
r of
            NoReduction MaybeReducedArgs
args1' -> do
              let es1' :: [MaybeReduced Elim]
es1' = (MaybeReduced (Arg Term) -> MaybeReduced Elim)
-> MaybeReducedArgs -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args1'
              if [Clause] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Clause]
cls Bool -> Bool -> Bool
&& RewriteRules -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null RewriteRules
rewr then do
                Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (QName -> Elims -> Term
Def QName
f []) (Elims -> Term) -> Blocked' Term Elims -> Blocked' Term Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
                  [Blocked Elim] -> Blocked' Term Elims
forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAll ([Blocked Elim] -> Blocked' Term Elims)
-> [Blocked Elim] -> Blocked' Term Elims
forall a b. (a -> b) -> a -> b
$ (MaybeReduced Elim -> Blocked Elim)
-> [MaybeReduced Elim] -> [Blocked Elim]
forall a b. (a -> b) -> [a] -> [b]
map MaybeReduced Elim -> Blocked Elim
forall t. IsMeta t => MaybeReduced t -> Blocked t
mredToBlocked [MaybeReduced Elim]
es1' [Blocked Elim] -> [Blocked Elim] -> [Blocked Elim]
forall a. [a] -> [a] -> [a]
++ (Elim -> Blocked Elim) -> Elims -> [Blocked Elim]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> Blocked Elim
forall a t. a -> Blocked' t a
notBlocked Elims
es2
               else
                Term
-> QName
-> [MaybeReduced Elim]
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> ReduceM (Reduced (Blocked' Term Term) Term)
reduceNormalE Term
v0 QName
f ([MaybeReduced Elim]
es1' [MaybeReduced Elim] -> [MaybeReduced Elim] -> [MaybeReduced Elim]
forall a. [a] -> [a] -> [a]
++ (Elim -> MaybeReduced Elim) -> Elims -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> MaybeReduced Elim
forall a. a -> MaybeReduced a
notReduced Elims
es2) Bool
dontUnfold [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr
            YesReduction Simplification
simpl Term
v -> Simplification
-> Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {m :: * -> *} {a} {no}.
Monad m =>
Simplification -> a -> m (Reduced no a)
yesReduction Simplification
simpl (Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2
      where
          ar :: Int
ar  = PrimFun -> Int
primFunArity PrimFun
pf

          mredToBlocked :: IsMeta t => MaybeReduced t -> Blocked t
          mredToBlocked :: forall t. IsMeta t => MaybeReduced t -> Blocked t
mredToBlocked (MaybeRed IsReduced
NotReduced  t
e) = t -> Blocked' Term t
forall a t. a -> Blocked' t a
notBlocked t
e
          mredToBlocked (MaybeRed (Reduced Blocked' Term ()
b) t
e) = t
e t -> Blocked' Term () -> Blocked' Term t
forall a b. a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked' Term ()
b

    reduceNormalE :: Term -> QName -> [MaybeReduced Elim] -> Bool -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> ReduceM (Reduced (Blocked Term) Term)
    reduceNormalE :: Term
-> QName
-> [MaybeReduced Elim]
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> ReduceM (Reduced (Blocked' Term Term) Term)
reduceNormalE Term
v0 QName
f [MaybeReduced Elim]
es Bool
dontUnfold [Clause]
def Maybe CompiledClauses
mcc RewriteRules
rewr = {-# SCC "reduceNormal" #-} do
      [Char]
-> Int
-> TCMT IO Doc
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.reduce" Int
90 (TCMT IO Doc
"reduceNormalE v0 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v0) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ do
      case ([Clause]
def,RewriteRules
rewr) of
        ([Clause], RewriteRules)
_ | Bool
dontUnfold -> [Char]
-> Int
-> [Char]
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"tc.reduce" Int
90 [Char]
"reduceNormalE: don't unfold (non-terminating or delayed)" (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$
                          ReduceM (Reduced (Blocked' Term Term) Term)
defaultResult -- non-terminating or delayed
        ([],[])        -> [Char]
-> Int
-> [Char]
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"tc.reduce" Int
90 [Char]
"reduceNormalE: no clauses or rewrite rules" (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ do
          -- no definition for head
          (Definition -> Blocked' Term ()
defBlocked (Definition -> Blocked' Term ())
-> ReduceM Definition -> ReduceM (Blocked' Term ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f) ReduceM (Blocked' Term ())
-> (Blocked' Term ()
    -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Blocked{}    -> Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Blocker -> Term -> Blocked' Term Term
forall t a. Blocker -> a -> Blocked' t a
Blocked (QName -> Blocker
UnblockOnDef QName
f) Term
vfull
            NotBlocked{} -> ReduceM (Reduced (Blocked' Term Term) Term)
defaultResult
        ([Clause]
cls,RewriteRules
rewr)     -> do
          Reduced (Blocked' Term Term) Term
ev <- QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr [MaybeReduced Elim]
es
          Reduced (Blocked' Term Term) Term -> ReduceM ()
debugReduce Reduced (Blocked' Term Term) Term
ev
          Reduced (Blocked' Term Term) Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Reduced (Blocked' Term Term) Term
ev
      where
      defaultResult :: ReduceM (Reduced (Blocked' Term Term) Term)
defaultResult = Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term)
forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction (Blocked' Term Term -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Blocked' Term Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ NotBlocked -> Term -> Blocked' Term Term
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
forall t. NotBlocked' t
ReallyNotBlocked Term
vfull
      vfull :: Term
vfull         = Term
v0 Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` (MaybeReduced Elim -> Elim) -> [MaybeReduced Elim] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced [MaybeReduced Elim]
es
      debugReduce :: Reduced (Blocked' Term Term) Term -> ReduceM ()
debugReduce Reduced (Blocked' Term Term) Term
ev = [Char] -> Int -> ReduceM () -> ReduceM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.reduce" Int
90 (ReduceM () -> ReduceM ()) -> ReduceM () -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ do
        case Reduced (Blocked' Term Term) Term
ev of
          NoReduction Blocked' Term Term
v -> do
            [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reduce" Int
90 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"*** tried to reduce " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
              , TCMT IO Doc
"    es =  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((MaybeReduced Elim -> TCMT IO Doc)
-> [MaybeReduced Elim] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Elim -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Elim -> TCMT IO Doc)
-> (MaybeReduced Elim -> Elim) -> MaybeReduced Elim -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced) [MaybeReduced Elim]
es)
              -- , "*** tried to reduce " <+> pretty vfull
              , TCMT IO Doc
"    stuck on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term Term
v)
              ]
          YesReduction Simplification
_simpl Term
v -> do
            [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reduce"  Int
90 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"*** reduced definition: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
            [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reduce"  Int
95 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"    result" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v

-- | Specialized version to put in boot file.
reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM = QName -> Elims -> TCM (Reduced () Term)
forall (m :: * -> *).
PureTCM m =>
QName -> Elims -> m (Reduced () Term)
reduceDefCopy

-- | Reduce a non-primitive definition if it is a copy linking to another def.
reduceDefCopy :: forall m. PureTCM m => QName -> Elims -> m (Reduced () Term)
reduceDefCopy :: forall (m :: * -> *).
PureTCM m =>
QName -> Elims -> m (Reduced () Term)
reduceDefCopy QName
f Elims
es = do
  Definition
info <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  case Definition -> Defn
theDef Definition
info of
    Defn
_ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Bool
defCopy Definition
info     -> Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ () -> Reduced () Term
forall no yes. no -> Reduced no yes
NoReduction ()
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c} -> Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced () Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem Elims
es)
    Defn
_                          -> Definition -> QName -> Elims -> m (Reduced () Term)
reduceDef_ Definition
info QName
f Elims
es
  where
    reduceDef_ :: Definition -> QName -> Elims -> m (Reduced () Term)
    reduceDef_ :: Definition -> QName -> Elims -> m (Reduced () Term)
reduceDef_ Definition
info QName
f Elims
es = case Definition -> [Clause]
defClauses Definition
info of
      [Clause
cl] -> do  -- proper copies always have a single clause
        let v0 :: Term
v0 = QName -> Elims -> Term
Def QName
f [] -- TODO: could be Con
            ps :: NAPs
ps    = Clause -> NAPs
namedClausePats Clause
cl
            nargs :: Int
nargs = Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es
            -- appDefE_ cannot handle underapplied functions, so we eta-expand here if that's the
            -- case. We use this function to compute display forms from module applications and in
            -- that case we don't always have saturated applications.
            (Term -> Term
lam, Elims
es') = ([Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs, Elims
newes)
              where
                etaArgs :: NAPs -> [a] -> [Arg [Char]]
etaArgs [] [a]
_ = []
                etaArgs (NamedArg DeBruijnPattern
p : NAPs
ps) []
                  | VarP PatternInfo
_ DBPatVar
x <- NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p = ArgInfo -> [Char] -> Arg [Char]
forall e. ArgInfo -> e -> Arg e
Arg (NamedArg DeBruijnPattern -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg DeBruijnPattern
p) (DBPatVar -> [Char]
dbPatVarName DBPatVar
x) Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
forall a. a -> [a] -> [a]
: NAPs -> [a] -> [Arg [Char]]
etaArgs NAPs
ps []
                  | Bool
otherwise              = []
                etaArgs (NamedArg DeBruijnPattern
_ : NAPs
ps) (a
_ : [a]
es) = NAPs -> [a] -> [Arg [Char]]
etaArgs NAPs
ps [a]
es
                xs :: [Arg [Char]]
xs  = NAPs -> Elims -> [Arg [Char]]
forall {a}. NAPs -> [a] -> [Arg [Char]]
etaArgs NAPs
ps Elims
es
                n :: Int
n   = [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs
                newes :: Elims
newes = Int -> Elims -> Elims
forall a. Subst a => Int -> a -> a
raise Int
n Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [ Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i Term -> Arg [Char] -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char]
x | (Int
i, Arg [Char]
x) <- [Int] -> [Arg [Char]] -> [(Int, Arg [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) [Arg [Char]]
xs ]
        if Definition -> Bool
defNonterminating Definition
info
         then Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ () -> Reduced () Term
forall no yes. no -> Reduced no yes
NoReduction ()
         else do
            Reduced (Blocked' Term Term) Term
ev <- ReduceM (Reduced (Blocked' Term Term) Term)
-> m (Reduced (Blocked' Term Term) Term)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Reduced (Blocked' Term Term) Term)
 -> m (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> m (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE_ QName
f Term
v0 [Clause
cl] Maybe CompiledClauses
forall a. Maybe a
Nothing RewriteRules
forall a. Monoid a => a
mempty ([MaybeReduced Elim]
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ (Elim -> MaybeReduced Elim) -> Elims -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> MaybeReduced Elim
forall a. a -> MaybeReduced a
notReduced Elims
es'
            case Reduced (Blocked' Term Term) Term
ev of
              YesReduction Simplification
simpl Term
t -> Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced () Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl (Term -> Term
lam Term
t)
              NoReduction{}        -> Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ () -> Reduced () Term
forall no yes. no -> Reduced no yes
NoReduction ()
      []    -> Reduced () Term -> m (Reduced () Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced () Term -> m (Reduced () Term))
-> Reduced () Term -> m (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ () -> Reduced () Term
forall no yes. no -> Reduced no yes
NoReduction ()  -- copies of generalizable variables have no clauses (and don't need unfolding)
      Clause
_:Clause
_:[Clause]
_ -> m (Reduced () Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Reduce simple (single clause) definitions.
reduceHead :: PureTCM m => Term -> m (Blocked Term)
reduceHead :: forall (m :: * -> *). PureTCM m => Term -> m (Blocked' Term Term)
reduceHead Term
v = do -- ignoreAbstractMode $ do
  -- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage
  -- see Issue 796

  -- first, possibly rewrite literal v to constructor form
  Term
v <- Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
  [Char]
-> Int
-> TCMT IO Doc
-> m (Blocked' Term Term)
-> m (Blocked' Term Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.inj.reduce" Int
30 (TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"reduceHead" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v) (m (Blocked' Term Term) -> m (Blocked' Term Term))
-> m (Blocked' Term Term) -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ do
  case Term
v of
    Def QName
f Elims
es -> do

      AbstractMode
abstractMode <- TCEnv -> AbstractMode
envAbstractMode (TCEnv -> AbstractMode) -> m TCEnv -> m AbstractMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
      Bool
isAbstract <- Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Bool
forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
hasAccessibleDef QName
f
      [Char]
-> Int
-> [Char]
-> m (Blocked' Term Term)
-> m (Blocked' Term Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"tc.inj.reduce" Int
50 (
        [Char]
"reduceHead: we are in " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ AbstractMode -> [Char]
forall a. Show a => a -> [Char]
show AbstractMode
abstractMode [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"; " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
        [Char]
" is treated " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ if Bool
isAbstract then [Char]
"abstractly" else [Char]
"concretely"
        ) (m (Blocked' Term Term) -> m (Blocked' Term Term))
-> m (Blocked' Term Term) -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ do
      let v0 :: Term
v0  = QName -> Elims -> Term
Def QName
f []
          red :: m (Blocked' Term Term)
red = ReduceM (Blocked' Term Term) -> m (Blocked' Term Term)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Blocked' Term Term) -> m (Blocked' Term Term))
-> ReduceM (Blocked' Term Term) -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE Term -> ReduceM (Blocked' Term Term)
forall (m :: * -> *). PureTCM m => Term -> m (Blocked' Term Term)
reduceHead Term
v0 QName
f Elims
es
      Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      case Defn
def of
        -- Andreas, 2012-11-06 unfold aliases (single clause terminating functions)
        -- see test/succeed/Issue747
        -- We restrict this to terminating functions to not make the
        -- type checker loop here on non-terminating functions.
        -- see test/fail/TerminationInfiniteRecord
        Function{ funClauses :: Defn -> [Clause]
funClauses = [ Clause
_ ], funTerminates :: Defn -> Maybe Bool
funTerminates = Just Bool
True } -> do
          [Char]
-> Int
-> [Char]
-> m (Blocked' Term Term)
-> m (Blocked' Term Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"tc.inj.reduce" Int
50 ([Char]
"reduceHead: head " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is Function") (m (Blocked' Term Term) -> m (Blocked' Term Term))
-> m (Blocked' Term Term) -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ do
          m (Blocked' Term Term)
red
        Datatype{ dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
_ } -> m (Blocked' Term Term)
red
        Record{ recClause :: Defn -> Maybe Clause
recClause = Just Clause
_ }    -> m (Blocked' Term Term)
red
        Defn
_                               -> Blocked' Term Term -> m (Blocked' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> m (Blocked' Term Term))
-> Blocked' Term Term -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked Term
v
    Term
_ -> Blocked' Term Term -> m (Blocked' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> m (Blocked' Term Term))
-> Blocked' Term Term -> m (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked Term
v

-- | Unfold a single inlined function.
unfoldInlined :: PureTCM m => Term -> m Term
unfoldInlined :: forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined Term
v = do
  Bool
inTypes <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eWorkingOnTypes
  case Term
v of
    Term
_ | Bool
inTypes -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v -- Don't inline in types (to avoid unfolding of goals)
    Def QName
f Elims
es -> do
      Definition
info <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      let def :: Defn
def = Definition -> Defn
theDef Definition
info
          irr :: Bool
irr = ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant (ArgInfo -> Bool) -> ArgInfo -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> ArgInfo
defArgInfo Definition
info
      case Defn
def of
        Function{} ->
          [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inline" Int
90 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
            [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
            [ [Char]
"considering to inline " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f
            , [Char]
"irr         = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Bool
irr
            , [Char]
"funInline   = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Defn
def Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funInline)
            , [Char]
"funCompiled = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Defn -> Maybe CompiledClauses
funCompiled Defn
def)
            ]
        Defn
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      case Defn
def of   -- Only for simple definitions with no pattern matching (TODO: maybe copatterns?)
        Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just Done{} }
          | Defn
def Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funInline , Bool -> Bool
not Bool
irr -> do
              [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inline" Int
70 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"asking to inline " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f
              ReduceM Term -> m Term
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM Term -> m Term) -> ReduceM Term -> m Term
forall a b. (a -> b) -> a -> b
$
                Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked' Term Term -> Term)
-> ReduceM (Blocked' Term Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> ReduceM (Blocked' Term Term))
-> Term -> QName -> Elims -> ReduceM (Blocked' Term Term)
unfoldDefinitionE (Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> (Term -> Blocked' Term Term)
-> Term
-> ReduceM (Blocked' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked) (QName -> Elims -> Term
Def QName
f []) QName
f Elims
es
        Defn
_ -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    Term
_ -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | Apply a definition using the compiled clauses, or fall back to
--   ordinary clauses if no compiled clauses exist.
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef_ :: QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDef_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr MaybeReducedArgs
args = QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr ([MaybeReduced Elim]
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ (MaybeReduced (Arg Term) -> MaybeReduced Elim)
-> MaybeReducedArgs -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args

appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE_ :: QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc RewriteRules
rewr [MaybeReduced Elim]
args =
  (TCEnv -> TCEnv)
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a. (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envAppDef = Just f }) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$
  ReduceM (Reduced (Blocked' Term Term) Term)
-> (CompiledClauses -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Maybe CompiledClauses
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Term
-> [Clause]
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE'' Term
v0 [Clause]
cls RewriteRules
rewr [MaybeReduced Elim]
args)
        (\CompiledClauses
cc -> Term
-> CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE Term
v0 CompiledClauses
cc RewriteRules
rewr [MaybeReduced Elim]
args) Maybe CompiledClauses
mcc


-- | Apply a defined function to it's arguments, using the compiled clauses.
--   The original term is the first argument applied to the third.
appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef :: Term
-> CompiledClauses
-> RewriteRules
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDef Term
v CompiledClauses
cc RewriteRules
rewr MaybeReducedArgs
args = Term
-> CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE Term
v CompiledClauses
cc RewriteRules
rewr ([MaybeReduced Elim]
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ (MaybeReduced (Arg Term) -> MaybeReduced Elim)
-> MaybeReducedArgs -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args

appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE :: Term
-> CompiledClauses
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE Term
v CompiledClauses
cc RewriteRules
rewr [MaybeReduced Elim]
es = do
  [Char]
-> Int
-> TCMT IO Doc
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.reduce" Int
90 (TCMT IO Doc
"appDefE v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ do
  Reduced (Blocked' Term Elims) Term
r <- CompiledClauses
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Elims) Term)
matchCompiledE CompiledClauses
cc [MaybeReduced Elim]
es
  case Reduced (Blocked' Term Elims) Term
r of
    YesReduction Simplification
simpl Term
t -> Reduced (Blocked' Term Term) Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked' Term Term) Term
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Reduced (Blocked' Term Term) Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced (Blocked' Term Term) Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl Term
t
    NoReduction Blocked' Term Elims
es'      -> Blocked' Term ()
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
rewrite (Blocked' Term Elims -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked' Term Elims
es') (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v) RewriteRules
rewr (Blocked' Term Elims -> Elims
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term Elims
es')

-- | Apply a defined function to it's arguments, using the original clauses.
appDef' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef' :: QName
-> Term
-> [Clause]
-> RewriteRules
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDef' QName
f Term
v [Clause]
cls RewriteRules
rewr MaybeReducedArgs
args = QName
-> Term
-> [Clause]
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE' QName
f Term
v [Clause]
cls RewriteRules
rewr ([MaybeReduced Elim]
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ (MaybeReduced (Arg Term) -> MaybeReduced Elim)
-> MaybeReducedArgs -> [MaybeReduced Elim]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args

appDefE' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE' :: QName
-> Term
-> [Clause]
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE' QName
f Term
v [Clause]
cls RewriteRules
rewr [MaybeReduced Elim]
es =
  (TCEnv -> TCEnv)
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a. (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envAppDef = Just f }) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$
  Term
-> [Clause]
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE'' Term
v [Clause]
cls RewriteRules
rewr [MaybeReduced Elim]
es

-- | Expects @'envAppDef' = Just f@ in 'TCEnv' to be able to report @'MissingClauses' f@.
appDefE'' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE'' :: Term
-> [Clause]
-> RewriteRules
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDefE'' Term
v [Clause]
cls RewriteRules
rewr [MaybeReduced Elim]
es = [Char]
-> Int
-> TCMT IO Doc
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.reduce" Int
90 (TCMT IO Doc
"appDefE' v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v) (ReduceM (Reduced (Blocked' Term Term) Term)
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ do
  [Clause] -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
goCls [Clause]
cls (Elims -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ (MaybeReduced Elim -> Elim) -> [MaybeReduced Elim] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced [MaybeReduced Elim]
es
  where
    goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term)
    goCls :: [Clause] -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
goCls [Clause]
cl Elims
es = do
      case [Clause]
cl of
        -- Andreas, 2013-10-26  In case of an incomplete match,
        -- we just do not reduce.  This allows adding single function
        -- clauses after they have been type-checked, to type-check
        -- the remaining clauses (see Issue 907).
        -- Andrea(s), 2014-12-05:  We return 'MissingClauses' here, since this
        -- is the most conservative reason.
        [] -> do
          QName
f <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> ReduceM (Maybe QName) -> ReduceM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Maybe QName) -> ReduceM (Maybe QName)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe QName
envAppDef
          Blocked' Term ()
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
rewrite (NotBlocked -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked
forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v) RewriteRules
rewr Elims
es
        Clause
cl : [Clause]
cls -> do
          let pats :: NAPs
pats = Clause -> NAPs
namedClausePats Clause
cl
              body :: Maybe Term
body = Clause -> Maybe Term
clauseBody Clause
cl
              npats :: Int
npats = NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
pats
              nvars :: Int
nvars = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl
          -- if clause is underapplied, skip to next clause
          if Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
npats then [Clause] -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
goCls [Clause]
cls Elims
es else do
            let (Elims
es0, Elims
es1) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
npats Elims
es
            (Match Term
m, Elims
es0) <- NAPs -> Elims -> ReduceM (Match Term, Elims)
forall (m :: * -> *).
MonadMatch m =>
NAPs -> Elims -> m (Match Term, Elims)
matchCopatterns NAPs
pats Elims
es0
            let es :: Elims
es = Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1
            case Match Term
m of
              Match Term
No               -> [Clause] -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
goCls [Clause]
cls Elims
es
              -- Szumi, 2024-03-29, issue #7181:
              -- If a lazy match is stuck and all non-lazy matches are conclusive,
              -- then reduction should not be stuck on the current clause and it
              -- should be fine to continue matching on the next clause.
              -- This assumes it's impossible for a lazy match to be stuck if
              -- all non-lazy matches succeed.
              DontKnow OnlyLazy
OnlyLazy Blocked' Term ()
_ -> [Clause] -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
goCls [Clause]
cls Elims
es
              DontKnow OnlyLazy
NonLazy  Blocked' Term ()
b -> Blocked' Term ()
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
rewrite Blocked' Term ()
b (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v) RewriteRules
rewr Elims
es
              Yes Simplification
simpl IntMap (Arg Term)
vs -- vs is the subst. for the variables bound in body
                | Just Term
w <- Maybe Term
body -> do -- clause has body?
                    -- TODO: let matchPatterns also return the reduced forms
                    -- of the original arguments!
                    -- Andreas, 2013-05-19 isn't this done now?
                    let sigma :: Substitution' Term
sigma = Impossible -> Int -> IntMap (Arg Term) -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution Impossible
HasCallStack => Impossible
impossible Int
nvars IntMap (Arg Term)
vs
                    Reduced (Blocked' Term Term) Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked' Term Term) Term
 -> ReduceM (Reduced (Blocked' Term Term) Term))
-> Reduced (Blocked' Term Term) Term
-> ReduceM (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced (Blocked' Term Term) Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl (Term -> Reduced (Blocked' Term Term) Term)
-> Term -> Reduced (Blocked' Term Term) Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sigma Term
w Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1
                | Bool
otherwise     -> Blocked' Term ()
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
rewrite (NotBlocked -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
forall t. NotBlocked' t
AbsurdMatch ()) (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v) RewriteRules
rewr Elims
es

instance Reduce a => Reduce (Closure a) where
    reduce' :: Closure a -> ReduceM (Closure a)
reduce' Closure a
cl = do
        a
x <- Closure a -> (a -> ReduceM a) -> ReduceM a
forall c a b. LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b
enterClosure Closure a
cl a -> ReduceM a
forall t. Reduce t => t -> ReduceM t
reduce'
        Closure a -> ReduceM (Closure a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure a -> ReduceM (Closure a))
-> Closure a -> ReduceM (Closure a)
forall a b. (a -> b) -> a -> b
$ Closure a
cl { clValue = x }
{-# SPECIALIZE reduce' :: Closure Constraint -> ReduceM (Closure Constraint) #-}

instance Reduce Telescope where
  reduce' :: Telescope -> ReduceM Telescope
reduce' Telescope
EmptyTel          = Telescope -> ReduceM Telescope
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
forall a. Tele a
EmptyTel
  reduce' (ExtendTel Dom Type
a Abs Telescope
tel) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Dom Type -> Abs Telescope -> Telescope)
-> ReduceM (Dom Type) -> ReduceM (Abs Telescope -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> ReduceM (Dom Type)
forall t. Reduce t => t -> ReduceM t
reduce' Dom Type
a ReduceM (Abs Telescope -> Telescope)
-> ReduceM (Abs Telescope) -> ReduceM Telescope
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Telescope -> ReduceM (Abs Telescope)
forall t. Reduce t => t -> ReduceM t
reduce' Abs Telescope
tel

instance Reduce Constraint where
  reduce' :: Constraint -> ReduceM Constraint
reduce' (ValueCmp Comparison
cmp CompareAs
t Term
u Term
v) = do
    (CompareAs
t,Term
u,Term
v) <- (CompareAs, Term, Term) -> ReduceM (CompareAs, Term, Term)
forall t. Reduce t => t -> ReduceM t
reduce' (CompareAs
t,Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp CompareAs
t Term
u Term
v
  reduce' (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = do
    ((Term
p,Type
t),Term
u,Term
v) <- ((Term, Type), Term, Term) -> ReduceM ((Term, Type), Term, Term)
forall t. Reduce t => t -> ReduceM t
reduce' ((Term
p,Type
t),Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v
  reduce' (ElimCmp [Polarity]
cmp [IsForced]
fs Type
t Term
v Elims
as Elims
bs) =
    [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
cmp [IsForced]
fs (Type -> Term -> Elims -> Elims -> Constraint)
-> ReduceM Type -> ReduceM (Term -> Elims -> Elims -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t ReduceM (Term -> Elims -> Elims -> Constraint)
-> ReduceM Term -> ReduceM (Elims -> Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
v ReduceM (Elims -> Elims -> Constraint)
-> ReduceM Elims -> ReduceM (Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Reduce t => t -> ReduceM t
reduce' Elims
as ReduceM (Elims -> Constraint)
-> ReduceM Elims -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Reduce t => t -> ReduceM t
reduce' Elims
bs
  reduce' (LevelCmp Comparison
cmp Level
u Level
v)    = (Level -> Level -> Constraint) -> (Level, Level) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) ((Level, Level) -> Constraint)
-> ReduceM (Level, Level) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Level, Level) -> ReduceM (Level, Level)
forall t. Reduce t => t -> ReduceM t
reduce' (Level
u,Level
v)
  reduce' (SortCmp Comparison
cmp Sort
a Sort
b)     = (Sort -> Sort -> Constraint) -> (Sort, Sort) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) ((Sort, Sort) -> Constraint)
-> ReduceM (Sort, Sort) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sort, Sort) -> ReduceM (Sort, Sort)
forall t. Reduce t => t -> ReduceM t
reduce' (Sort
a,Sort
b)
  reduce' (UnBlock MetaId
m)           = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
UnBlock MetaId
m
  reduce' (FindInstance MetaId
m Maybe [Candidate]
cs)   = MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m (Maybe [Candidate] -> Constraint)
-> ReduceM (Maybe [Candidate]) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Candidate] -> ReduceM [Candidate])
-> Maybe [Candidate] -> ReduceM (Maybe [Candidate])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM [Candidate] -> ReduceM [Candidate]
forall t. Reduce t => t -> ReduceM t
reduce' Maybe [Candidate]
cs
  reduce' (ResolveInstanceHead QName
q) = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ QName -> Constraint
ResolveInstanceHead QName
q
  reduce' (IsEmpty Range
r Type
t)         = Range -> Type -> Constraint
IsEmpty Range
r (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (CheckSizeLtSat Term
t)    = Term -> Constraint
CheckSizeLtSat (Term -> Constraint) -> ReduceM Term -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t
  reduce' c :: Constraint
c@CheckFunDef{}       = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  reduce' (HasBiggerSort Sort
a)     = Sort -> Constraint
HasBiggerSort (Sort -> Constraint) -> ReduceM Sort -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Reduce t => t -> ReduceM t
reduce' Sort
a
  reduce' (HasPTSRule Dom Type
a Abs Sort
b)      = (Dom Type -> Abs Sort -> Constraint)
-> (Dom Type, Abs Sort) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Sort -> Constraint
HasPTSRule ((Dom Type, Abs Sort) -> Constraint)
-> ReduceM (Dom Type, Abs Sort) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom Type, Abs Sort) -> ReduceM (Dom Type, Abs Sort)
forall t. Reduce t => t -> ReduceM t
reduce' (Dom Type
a,Abs Sort
b)
  reduce' (UnquoteTactic Term
t Term
h Type
g) = Term -> Term -> Type -> Constraint
UnquoteTactic (Term -> Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Term -> Type -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t ReduceM (Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
h ReduceM (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
g
  reduce' (CheckLockedVars Term
a Type
b Arg Term
c Type
d) =
    Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Term -> Type -> Arg Term -> Type -> Constraint)
-> ReduceM Term -> ReduceM (Type -> Arg Term -> Type -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
a ReduceM (Type -> Arg Term -> Type -> Constraint)
-> ReduceM Type -> ReduceM (Arg Term -> Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
b ReduceM (Arg Term -> Type -> Constraint)
-> ReduceM (Arg Term) -> ReduceM (Type -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
c ReduceM (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
d
  reduce' (CheckDataSort QName
q Sort
s)   = QName -> Sort -> Constraint
CheckDataSort QName
q (Sort -> Constraint) -> ReduceM Sort -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Reduce t => t -> ReduceM t
reduce' Sort
s
  reduce' c :: Constraint
c@CheckMetaInst{}     = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  reduce' (CheckType Type
t)         = Type -> Constraint
CheckType (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = (Maybe Sort -> Modality -> Term -> Constraint)
-> Modality -> Maybe Sort -> Term -> Constraint
forall a b c. (a -> b -> c) -> b -> a -> c
flip (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc) Modality
mod (Maybe Sort -> Term -> Constraint)
-> ReduceM (Maybe Sort) -> ReduceM (Term -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Sort -> ReduceM (Maybe Sort)
forall t. Reduce t => t -> ReduceM t
reduce' Maybe Sort
ms ReduceM (Term -> Constraint) -> ReduceM Term -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t

instance Reduce CompareAs where
  reduce' :: CompareAs -> ReduceM CompareAs
reduce' (AsTermsOf Type
a) = Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> ReduceM Type -> ReduceM CompareAs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
a
  reduce' CompareAs
AsSizes       = CompareAs -> ReduceM CompareAs
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
  reduce' CompareAs
AsTypes       = CompareAs -> ReduceM CompareAs
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsTypes

instance Reduce e => Reduce (Map k e) where
  reduce' :: Map k e -> ReduceM (Map k e)
reduce' = (e -> ReduceM e) -> Map k e -> ReduceM (Map k e)
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) -> Map k a -> f (Map k b)
traverse e -> ReduceM e
forall t. Reduce t => t -> ReduceM t
reduce'

instance Reduce Candidate where
  reduce' :: Candidate -> ReduceM Candidate
reduce' (Candidate CandidateKind
q Term
u Type
t OverlapMode
ov) = CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
q (Term -> Type -> OverlapMode -> Candidate)
-> ReduceM Term -> ReduceM (Type -> OverlapMode -> Candidate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
u ReduceM (Type -> OverlapMode -> Candidate)
-> ReduceM Type -> ReduceM (OverlapMode -> Candidate)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t ReduceM (OverlapMode -> Candidate)
-> ReduceM OverlapMode -> ReduceM Candidate
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OverlapMode -> ReduceM OverlapMode
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OverlapMode
ov

instance Reduce EqualityView where
  reduce' :: EqualityView -> ReduceM EqualityView
reduce' (OtherType Type
t)            = Type -> EqualityView
OtherType
    (Type -> EqualityView) -> ReduceM Type -> ReduceM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (IdiomType Type
t)            = Type -> EqualityView
IdiomType
    (Type -> EqualityView) -> ReduceM Type -> ReduceM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (EqualityType Sort
s QName
eq [Arg Term]
l Arg Term
t Arg Term
a Arg Term
b) = Sort
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType
    (Sort
 -> QName
 -> [Arg Term]
 -> Arg Term
 -> Arg Term
 -> Arg Term
 -> EqualityView)
-> ReduceM Sort
-> ReduceM
     (QName
      -> [Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Reduce t => t -> ReduceM t
reduce' Sort
s
    ReduceM
  (QName
   -> [Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM QName
-> ReduceM
     ([Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> ReduceM QName
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
eq
    ReduceM
  ([Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM [Arg Term]
-> ReduceM (Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Arg Term -> ReduceM (Arg Term))
-> [Arg Term] -> ReduceM [Arg Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' [Arg Term]
l
    ReduceM (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> ReduceM (Arg Term)
-> ReduceM (Arg Term -> Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
t
    ReduceM (Arg Term -> Arg Term -> EqualityView)
-> ReduceM (Arg Term) -> ReduceM (Arg Term -> EqualityView)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
a
    ReduceM (Arg Term -> EqualityView)
-> ReduceM (Arg Term) -> ReduceM EqualityView
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> ReduceM (Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
b

instance Reduce t => Reduce (IPBoundary' t) where
  reduce' :: IPBoundary' t -> ReduceM (IPBoundary' t)
reduce' = (t -> ReduceM t) -> IPBoundary' t -> ReduceM (IPBoundary' t)
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) -> IPBoundary' a -> f (IPBoundary' b)
traverse t -> ReduceM t
forall t. Reduce t => t -> ReduceM t
reduce'
  reduceB' :: IPBoundary' t -> ReduceM (Blocked (IPBoundary' t))
reduceB' = (IPBoundary' (Blocked' Term t) -> Blocked (IPBoundary' t))
-> ReduceM (IPBoundary' (Blocked' Term t))
-> ReduceM (Blocked (IPBoundary' t))
forall a b. (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IPBoundary' (Blocked' Term t) -> Blocked (IPBoundary' t)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
IPBoundary' (f a) -> f (IPBoundary' a)
sequenceA (ReduceM (IPBoundary' (Blocked' Term t))
 -> ReduceM (Blocked (IPBoundary' t)))
-> (IPBoundary' t -> ReduceM (IPBoundary' (Blocked' Term t)))
-> IPBoundary' t
-> ReduceM (Blocked (IPBoundary' t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> ReduceM (Blocked' Term t))
-> IPBoundary' t -> ReduceM (IPBoundary' (Blocked' Term t))
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) -> IPBoundary' a -> f (IPBoundary' b)
traverse t -> ReduceM (Blocked' Term t)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'

---------------------------------------------------------------------------
-- * Simplification
---------------------------------------------------------------------------

-- | Only unfold definitions if this leads to simplification
--   which means that a constructor/literal pattern is matched.
--   We include reduction of IApply patterns, as `p i0` is akin to
--   matcing on the `i0` constructor of interval.
class Simplify t where
  simplify' :: t -> ReduceM t

  default simplify' :: (t ~ f a, Traversable f, Simplify a) => t -> ReduceM t
  simplify' = (a -> ReduceM a) -> f a -> ReduceM (f 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) -> f a -> f (f b)
traverse a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify'

-- boring instances:

instance Simplify t => Simplify [t]
instance Simplify t => Simplify (Map k t)
instance Simplify t => Simplify (Maybe t)
instance Simplify t => Simplify (Strict.Maybe t)

instance Simplify t => Simplify (Arg t)
instance Simplify t => Simplify (Elim' t)
instance Simplify t => Simplify (Named name t)
instance Simplify t => Simplify (IPBoundary' t)

instance (Simplify a, Simplify b) => Simplify (a,b) where
    simplify' :: (a, b) -> ReduceM (a, b)
simplify' (a
x,b
y) = (,) (a -> b -> (a, b)) -> ReduceM a -> ReduceM (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify' a
x ReduceM (b -> (a, b)) -> ReduceM b -> ReduceM (a, b)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM b
forall t. Simplify t => t -> ReduceM t
simplify' b
y

instance (Simplify a, Simplify b, Simplify c) => Simplify (a,b,c) where
    simplify' :: (a, b, c) -> ReduceM (a, b, c)
simplify' (a
x,b
y,c
z) =
        do  (a
x,(b
y,c
z)) <- (a, (b, c)) -> ReduceM (a, (b, c))
forall t. Simplify t => t -> ReduceM t
simplify' (a
x,(b
y,c
z))
            (a, b, c) -> ReduceM (a, b, c)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x,b
y,c
z)

instance Simplify Bool where
  simplify' :: Bool -> ReduceM Bool
simplify' = Bool -> ReduceM Bool
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- interesting instances:

instance Simplify Term where
  simplify' :: Term -> ReduceM Term
simplify' Term
v = do
    Term
v <- Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
    let iapp :: Elims -> ReduceM Term -> ReduceM Term
iapp Elims
es ReduceM Term
m = Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked' Term Term -> Term)
-> ReduceM (Blocked' Term Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> Elims
-> ReduceM (Blocked' Term Term)
reduceIApply' ((Term -> Blocked' Term Term)
-> ReduceM Term -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked (ReduceM Term -> ReduceM (Blocked' Term Term))
-> (Term -> ReduceM Term) -> Term -> ReduceM (Blocked' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ReduceM Term
forall t. Simplify t => t -> ReduceM t
simplify') (Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked (Term -> Blocked' Term Term)
-> ReduceM Term -> ReduceM (Blocked' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM Term
m) Elims
es
    case Term
v of
      Def QName
f Elims
vs   -> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ do
        let keepGoing :: a -> a -> m (a, Blocked' t a)
keepGoing a
simp a
v = (a, Blocked' t a) -> m (a, Blocked' t a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
simp, a -> Blocked' t a
forall a t. a -> Blocked' t a
notBlocked a
v)
        (Simplification
simpl, Blocked' Term Term
v) <- (Simplification
 -> Term -> ReduceM (Simplification, Blocked' Term Term))
-> Term
-> QName
-> Elims
-> ReduceM (Simplification, Blocked' Term Term)
unfoldDefinition' Simplification
-> Term -> ReduceM (Simplification, Blocked' Term Term)
forall {m :: * -> *} {a} {a} {t}.
Monad m =>
a -> a -> m (a, Blocked' t a)
keepGoing (QName -> Elims -> Term
Def QName
f []) QName
f Elims
vs
        Bool -> ReduceM () -> ReduceM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Simplification
simpl Simplification -> Simplification -> Bool
forall a. Eq a => a -> a -> Bool
== Simplification
YesSimplification) (ReduceM () -> ReduceM ()) -> ReduceM () -> ReduceM ()
forall a b. (a -> b) -> a -> b
$
          [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.simplify'" Int
90 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$
            QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"simplify': unfolding definition returns " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Simplification -> [Char]
forall a. Show a => a -> [Char]
show Simplification
simpl) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term Term
v)
        case Simplification
simpl of
          Simplification
YesSimplification -> Blocked' Term Term -> ReduceM Term
forall t. Simplify t => Blocked t -> ReduceM t
simplifyBlocked' Blocked' Term Term
v -- Dangerous, but if @simpl@ then @v /= Def f vs@
          Simplification
NoSimplification  -> QName -> Elims -> Term
Def QName
f (Elims -> Term) -> ReduceM Elims -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      MetaV MetaId
x Elims
vs -> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x  (Elims -> Term) -> ReduceM Elims -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      Con ConHead
c ConInfo
ci Elims
vs-> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> ReduceM Elims -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      Sort Sort
s     -> Sort -> Term
Sort     (Sort -> Term) -> ReduceM Sort -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s
      Level Level
l    -> Level -> Term
levelTm  (Level -> Term) -> ReduceM Level -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReduceM Level
forall t. Simplify t => t -> ReduceM t
simplify' Level
l
      Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
Pi       (Dom Type -> Abs Type -> Term)
-> ReduceM (Dom Type) -> ReduceM (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> ReduceM (Dom Type)
forall t. Simplify t => t -> ReduceM t
simplify' Dom Type
a ReduceM (Abs Type -> Term) -> ReduceM (Abs Type) -> ReduceM Term
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> ReduceM (Abs Type)
forall t. Simplify t => t -> ReduceM t
simplify' Abs Type
b
      Lit Literal
l      -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
      Var Int
i Elims
vs   -> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
i    (Elims -> Term) -> ReduceM Elims -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      Lam ArgInfo
h Abs Term
v    -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h    (Abs Term -> Term) -> ReduceM (Abs Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> ReduceM (Abs Term)
forall t. Simplify t => t -> ReduceM t
simplify' Abs Term
v
      DontCare Term
v -> Term -> Term
dontCare (Term -> Term) -> ReduceM Term -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Simplify t => t -> ReduceM t
simplify' Term
v
      Dummy{}    -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
simplifyBlocked' :: forall t. Simplify t => Blocked t -> ReduceM t
simplifyBlocked' (Blocked Blocker
_ t
t) = t -> ReduceM t
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return t
t
simplifyBlocked' (NotBlocked NotBlocked
_ t
t) = t -> ReduceM t
forall t. Simplify t => t -> ReduceM t
simplify' t
t  -- Andrea(s), 2014-12-05 OK?

instance Simplify t => Simplify (Type' t) where
    simplify' :: Type' t -> ReduceM (Type' t)
simplify' (El Sort
s t
t) = Sort -> t -> Type' t
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> t -> Type' t) -> ReduceM Sort -> ReduceM (t -> Type' t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s ReduceM (t -> Type' t) -> ReduceM t -> ReduceM (Type' t)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> ReduceM t
forall t. Simplify t => t -> ReduceM t
simplify' t
t

instance Simplify Sort where
    simplify' :: Sort -> ReduceM Sort
simplify' Sort
s = do
      case Sort
s of
        PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Dom' Term Term -> Sort -> Abs Sort -> Sort
piSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> ReduceM (Dom' Term Term) -> ReduceM (Sort -> Abs Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term -> ReduceM (Dom' Term Term)
forall t. Simplify t => t -> ReduceM t
simplify' Dom' Term Term
a ReduceM (Sort -> Abs Sort -> Sort)
-> ReduceM Sort -> ReduceM (Abs Sort -> Sort)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s1 ReduceM (Abs Sort -> Sort) -> ReduceM (Abs Sort) -> ReduceM Sort
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Sort -> ReduceM (Abs Sort)
forall t. Simplify t => t -> ReduceM t
simplify' Abs Sort
s2
        FunSort Sort
s1 Sort
s2 -> Sort -> Sort -> Sort
funSort (Sort -> Sort -> Sort) -> ReduceM Sort -> ReduceM (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s1 ReduceM (Sort -> Sort) -> ReduceM Sort -> ReduceM Sort
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s2
        UnivSort Sort
s -> Sort -> Sort
univSort (Sort -> Sort) -> ReduceM Sort -> ReduceM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
s
        Univ Univ
u Level
s   -> Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Sort) -> ReduceM Level -> ReduceM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReduceM Level
forall t. Simplify t => t -> ReduceM t
simplify' Level
s
        Inf Univ
_ Integer
_    -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
SizeUniv   -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
LockUniv   -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
LevelUniv  -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
IntervalUniv -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> ReduceM Elims -> ReduceM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
es
        DefS QName
d Elims
es  -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d (Elims -> Sort) -> ReduceM Elims -> ReduceM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
es
        DummyS{}   -> Sort -> ReduceM Sort
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s

instance Simplify Level where
  simplify' :: Level -> ReduceM Level
simplify' (Max Integer
m [PlusLevel]
as) = Integer -> [PlusLevel] -> Level
levelMax Integer
m ([PlusLevel] -> Level) -> ReduceM [PlusLevel] -> ReduceM Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel] -> ReduceM [PlusLevel]
forall t. Simplify t => t -> ReduceM t
simplify' [PlusLevel]
as

instance Simplify PlusLevel where
  simplify' :: PlusLevel -> ReduceM PlusLevel
simplify' (Plus Integer
n Term
l) = Integer -> Term -> PlusLevel
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel) -> ReduceM Term -> ReduceM PlusLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Simplify t => t -> ReduceM t
simplify' Term
l

instance (Subst a, Simplify a) => Simplify (Abs a) where
    simplify' :: Abs a -> ReduceM (Abs a)
simplify' a :: Abs a
a@(Abs [Char]
x a
_) = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
Abs [Char]
x (a -> Abs a) -> ReduceM a -> ReduceM (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs a -> (a -> ReduceM a) -> ReduceM a
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
a a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify'
    simplify' (NoAbs [Char]
x a
v) = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x (a -> Abs a) -> ReduceM a -> ReduceM (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify' a
v

instance Simplify t => Simplify (Dom t) where
    simplify' :: Dom t -> ReduceM (Dom t)
simplify' = (t -> ReduceM t) -> Dom t -> ReduceM (Dom t)
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 t -> ReduceM t
forall t. Simplify t => t -> ReduceM t
simplify'

instance Simplify a => Simplify (Closure a) where
    simplify' :: Closure a -> ReduceM (Closure a)
simplify' Closure a
cl = do
        a
x <- Closure a -> (a -> ReduceM a) -> ReduceM a
forall c a b. LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b
enterClosure Closure a
cl a -> ReduceM a
forall t. Simplify t => t -> ReduceM t
simplify'
        Closure a -> ReduceM (Closure a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure a -> ReduceM (Closure a))
-> Closure a -> ReduceM (Closure a)
forall a b. (a -> b) -> a -> b
$ Closure a
cl { clValue = x }

instance (Subst a, Simplify a) => Simplify (Tele a) where
  simplify' :: Tele a -> ReduceM (Tele a)
simplify' Tele a
EmptyTel        = Tele a -> ReduceM (Tele a)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele a
forall a. Tele a
EmptyTel
  simplify' (ExtendTel a
a Abs (Tele a)
b) = (a -> Abs (Tele a) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel ((a, Abs (Tele a)) -> Tele a)
-> ReduceM (a, Abs (Tele a)) -> ReduceM (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, Abs (Tele a)) -> ReduceM (a, Abs (Tele a))
forall t. Simplify t => t -> ReduceM t
simplify' (a
a, Abs (Tele a)
b)

instance Simplify ProblemConstraint where
  simplify' :: ProblemConstraint -> ReduceM ProblemConstraint
simplify' (PConstr Set ProblemId
pid Blocker
unblock Closure Constraint
c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
pid Blocker
unblock (Closure Constraint -> ProblemConstraint)
-> ReduceM (Closure Constraint) -> ReduceM ProblemConstraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Closure Constraint -> ReduceM (Closure Constraint)
forall t. Simplify t => t -> ReduceM t
simplify' Closure Constraint
c

instance Simplify Constraint where
  simplify' :: Constraint -> ReduceM Constraint
simplify' (ValueCmp Comparison
cmp CompareAs
t Term
u Term
v) = do
    (CompareAs
t,Term
u,Term
v) <- (CompareAs, Term, Term) -> ReduceM (CompareAs, Term, Term)
forall t. Simplify t => t -> ReduceM t
simplify' (CompareAs
t,Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp CompareAs
t Term
u Term
v
  simplify' (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = do
    ((Term
p,Type
t),Term
u,Term
v) <- ((Term, Type), Term, Term) -> ReduceM ((Term, Type), Term, Term)
forall t. Simplify t => t -> ReduceM t
simplify' ((Term
p,Type
t),Term
u,Term
v)
    Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp (Type -> CompareAs
AsTermsOf Type
t) Term
u Term
v
  simplify' (ElimCmp [Polarity]
cmp [IsForced]
fs Type
t Term
v Elims
as Elims
bs) =
    [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
cmp [IsForced]
fs (Type -> Term -> Elims -> Elims -> Constraint)
-> ReduceM Type -> ReduceM (Term -> Elims -> Elims -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Simplify t => t -> ReduceM t
simplify' Type
t ReduceM (Term -> Elims -> Elims -> Constraint)
-> ReduceM Term -> ReduceM (Elims -> Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Simplify t => t -> ReduceM t
simplify' Term
v ReduceM (Elims -> Elims -> Constraint)
-> ReduceM Elims -> ReduceM (Elims -> Constraint)
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
as ReduceM (Elims -> Constraint)
-> ReduceM Elims -> ReduceM Constraint
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elims -> ReduceM Elims
forall t. Simplify t => t -> ReduceM t
simplify' Elims
bs
  simplify' (LevelCmp Comparison
cmp Level
u Level
v)    = (Level -> Level -> Constraint) -> (Level, Level) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) ((Level, Level) -> Constraint)
-> ReduceM (Level, Level) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Level, Level) -> ReduceM (Level, Level)
forall t. Simplify t => t -> ReduceM t
simplify' (Level
u,Level
v)
  simplify' (SortCmp Comparison
cmp Sort
a Sort
b)     = (Sort -> Sort -> Constraint) -> (Sort, Sort) -> Constraint
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) ((Sort, Sort) -> Constraint)
-> ReduceM (Sort, Sort) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sort, Sort) -> ReduceM (Sort, Sort)
forall t. Simplify t => t -> ReduceM t
simplify' (Sort
a,Sort
b)
  simplify' (UnBlock MetaId
m)           = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
UnBlock MetaId
m
  simplify' (FindInstance MetaId
m Maybe [Candidate]
cs)   = MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m (Maybe [Candidate] -> Constraint)
-> ReduceM (Maybe [Candidate]) -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Candidate] -> ReduceM [Candidate])
-> Maybe [Candidate] -> ReduceM (Maybe [Candidate])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM [Candidate] -> ReduceM [Candidate]
forall t. Simplify t => t -> ReduceM t
simplify' Maybe [Candidate]
cs
  simplify' (ResolveInstanceHead QName
q) = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> ReduceM Constraint)
-> Constraint -> ReduceM Constraint
forall a b. (a -> b) -> a -> b
$ QName -> Constraint
ResolveInstanceHead QName
q
  simplify' (IsEmpty Range
r Type
t)         = Range -> Type -> Constraint
IsEmpty Range
r (Type -> Constraint) -> ReduceM Type -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReduceM Type
forall t. Simplify t => t -> ReduceM t
simplify' Type
t
  simplify' (CheckSizeLtSat Term
t)    = Term -> Constraint
CheckSizeLtSat (Term -> Constraint) -> ReduceM Term -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM Term
forall t. Simplify t => t -> ReduceM t
simplify' Term
t
  simplify' c :: Constraint
c@CheckFunDef{}       = Constraint -> ReduceM Constraint
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  simplify' (HasBiggerSort Sort
a)     = Sort -> Constraint
HasBiggerSort (Sort -> Constraint) -> ReduceM Sort -> ReduceM Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReduceM Sort
forall t. Simplify t => t -> ReduceM t
simplify' Sort
a
  simplify' (HasPTSRule Dom Type
a Abs Sort
b)      =