{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Reduce
 -- Meta instantiation
 ( Instantiate, instantiate', instantiate, instantiateWhen
 -- Recursive meta instantiation
 , InstantiateFull, instantiateFull', instantiateFull
 , instantiateFullExceptForDefinitions
 -- 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
 -- Simplification
 , Simplify, simplify, simplifyBlocked'
 -- Normalization
 , Normalise, normalise', normalise
 , slowNormaliseArgs
 ) where

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

import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
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 (workOnTypes, isPropM)
import {-# SOURCE #-} Agda.TypeChecking.Level (reallyUnLevelView)
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 Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.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 = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a. (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
localR (\ReduceEnv
env -> ReduceEnv
env { redPred :: Maybe (MetaId -> ReduceM Bool)
redPred = forall a. a -> Maybe a
Just MetaId -> ReduceM Bool
p }) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall t. InstantiateFull t => t -> ReduceM t
instantiateFull'

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

reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a)
reduceB :: forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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' -> forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker
b, a
a'))
  (\NotBlocked
_ a
a' -> forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker
neverUnblock, a
a'))

-- Reduce a term and call the continuation. If the continuation is
-- blocked, the whole call is blocked either on what blocked the reduction
-- or on what blocked the continuation (using `blockedOnEither`).
withReduced
  :: (Reduce a, IsMeta a, MonadReduce m, MonadBlock m)
  => a -> (a -> m b) -> m b
withReduced :: forall a (m :: * -> *) b.
(Reduce a, IsMeta a, MonadReduce m, MonadBlock m) =>
a -> (a -> m b) -> m b
withReduced a
a a -> m b
cont = 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' -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker Blocker
b forall a b. (a -> b) -> a -> b
$ a -> m b
cont a
a') (\NotBlocked
_ a
a' -> a -> m b
cont a
a')

normalise :: (Normalise a, MonadReduce m) => a -> m a
normalise :: forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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

simplify :: (Simplify a, MonadReduce m) => a -> m a
simplify :: forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
  case MetaInstantiation
inst of
    InstV Instantiation
inst -> forall a. AllMetas a => a -> Bool
noMetas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Instantiation -> Term
instBody Instantiation
inst)
    MetaInstantiation
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | 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 = forall a t. Blocker -> a -> Blocked' t a
blockedOn Blocker
block forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Blocked' t a -> a
ignoreBlocking f (Blocked a)
bs
  where block :: Blocker
block = Set Blocker -> Blocker
unblockOnAll forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. a -> Set a
Set.singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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

-- | 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 = forall a t. Blocker -> a -> Blocked' t a
blockedOn Blocker
block forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Blocked' t a -> a
ignoreBlocking f (Blocked a)
bs
  where block :: Blocker
block = case forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall {t} {a}. Blocked' t a -> [Blocker]
blocker f (Blocked a)
bs of
                  [] -> Blocker
alwaysUnblock -- no blockers
                  [Blocker]
bs -> Set Blocker -> Blocker
unblockOnAny forall a b. (a -> b) -> a -> b
$ 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]

-- | 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 a, Instantiate b) => Instantiate (a,b) where
    instantiate' :: (a, b) -> ReduceM (a, b)
instantiate' (a
x,b
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 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  -> 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) = forall a. MetaId -> ReduceM a -> ReduceM a -> ReduceM a
ifPredicateDoesNotHoldFor MetaId
x (forall (m :: * -> *) a. Monad m => a -> m a
return Term
t) forall a b. (a -> b) -> a -> b
$ do
    Bool
blocking <- forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view Lens' Bool TCState
stInstantiateBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TCState
getTCState

    Maybe (Either RemoteMetaVariable MetaVariable)
m <- 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 ->
           forall t. Instantiate t => t -> ReduceM t
instantiate' (MetaId -> Elims -> Term
MetaV MetaId
m' Elims
es)

         MetaInstantiation
Open -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

         MetaInstantiation
OpenInstance -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

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

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

      Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__
                   (String
"Meta-variable not found: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow MetaId
x)
    where
    cont :: Instantiation -> ReduceM Term
cont Instantiation
i = 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) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length (Instantiation -> [Arg String]
instTel Instantiation
i)) Elims
es
      vs1 :: [Term]
vs1 = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es1
      rho :: Substitution' Term
rho = [Term]
vs1 forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Int -> Substitution' a -> Substitution' a
wkS (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs1) 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 =
        forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
rho
          (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg String -> Term -> Term
mkLam (Instantiation -> Term
instBody Instantiation
i) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es1) (Instantiation -> [Arg String]
instTel Instantiation
i))
          forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2

  instantiate' (Level Level
l) = Level -> Term
levelTm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Level
l
  instantiate' (Sort Sort
s) = Sort -> Term
Sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
  instantiate' Term
t = 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) = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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{} = forall (m :: * -> *) a. Monad m => a -> m a
return Blocked a
v
  instantiate' v :: Blocked a
v@(Blocked Blocker
b a
u) = forall t. Instantiate t => t -> ReduceM t
instantiate' Blocker
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
    Blocker
b | Blocker
b forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock -> forall a t. a -> Blocked' t a
notBlocked forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' a
u
      | Bool
otherwise          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Instantiate t => t -> ReduceM t
instantiate' (forall a. Set a -> [a]
Set.toList Set Blocker
bs)
  instantiate' (UnblockOnAny Set Blocker
bs) = Set Blocker -> Blocker
unblockOnAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Instantiate t => t -> ReduceM t
instantiate' (forall a. Set a -> [a]
Set.toList Set Blocker
bs)
  instantiate' b :: Blocker
b@(UnblockOnMeta MetaId
x) =
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x) (forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock) (forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b)
  instantiate' b :: Blocker
b@UnblockOnProblem{} = forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b
  instantiate' b :: Blocker
b@UnblockOnDef{} = 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 -> forall t. Instantiate t => t -> ReduceM t
instantiate' (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Sort Sort
s'      -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'
      MetaV MetaId
x' Elims
es' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x' Elims
es'
      Def QName
d Elims
es'    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es'
      Term
_            -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Sort
s -> 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) = forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
i Maybe NamedName
n Bool
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe t
tac forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 <- forall a c b. LensClosure a c => c -> (a -> ReduceM b) -> ReduceM b
enterClosure Closure a
cl forall t. Instantiate t => t -> ReduceM t
instantiate'
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Closure a
cl { clValue :: a
clValue = a
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) <- forall t. Instantiate t => t -> ReduceM t
instantiate' (CompareAs
t,Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall t. Instantiate t => t -> ReduceM t
instantiate' ((Term
p,Type
t),Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Elims
as forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Elims
bs
  instantiate' (LevelCmp Comparison
cmp Level
u Level
v)   = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' (Level
u,Level
v)
  instantiate' (SortCmp Comparison
cmp Sort
a Sort
b)    = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' (Sort
a,Sort
b)
  instantiate' (UnBlock MetaId
m)          = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe [Candidate]
cs
  instantiate' (IsEmpty Range
r Type
t)        = Range -> Type -> Constraint
IsEmpty Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (CheckSizeLtSat Term
t)   = Term -> Constraint
CheckSizeLtSat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
t
  instantiate' c :: Constraint
c@CheckFunDef{}      = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  instantiate' (HasBiggerSort Sort
a)    = Sort -> Constraint
HasBiggerSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
a
  instantiate' (HasPTSRule Dom Type
a Abs Sort
b)     = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Sort -> Constraint
HasPTSRule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
d
  instantiate' (UnquoteTactic Term
t Term
h Type
g) = Term -> Term -> Type -> Constraint
UnquoteTactic forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
h forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
g
  instantiate' (CheckDataSort QName
q Sort
s)  = QName -> Sort -> Constraint
CheckDataSort QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
  instantiate' c :: Constraint
c@CheckMetaInst{}    = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  instantiate' (CheckType Type
t)        = Type -> Constraint
CheckType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = forall a b c. (a -> b -> c) -> b -> a -> c
flip (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc) Modality
mod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Maybe Sort
ms forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
a
  instantiate' CompareAs
AsSizes       = forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
  instantiate' CompareAs
AsTypes       = 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 Bool
ov) = CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate CandidateKind
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
ov

instance Instantiate EqualityView where
  instantiate' :: EqualityView -> ReduceM EqualityView
instantiate' (OtherType Type
t)            = Type -> EqualityView
OtherType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Type
t
  instantiate' (IdiomType Type
t)            = Type -> EqualityView
IdiomType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return QName
eq
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Instantiate t => t -> ReduceM t
instantiate' [Arg Term]
l
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
t
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Instantiate t => t -> ReduceM t
instantiate' Arg Term
a
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
_) = forall a. a -> Maybe a
Just MetaId
m
  isMeta Term
_           = forall a. Maybe a
Nothing

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

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

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

instance IsMeta a => IsMeta (Arg a) where
  isMeta :: Arg a -> Maybe MetaId
isMeta = forall a. IsMeta a => a -> Maybe MetaId
isMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]) = forall a. IsMeta a => a -> Maybe MetaId
isMeta PlusLevel' a
l
  isMeta Level' a
_           = forall a. Maybe a
Nothing

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

instance IsMeta CompareAs where
  isMeta :: CompareAs -> Maybe MetaId
isMeta (AsTermsOf Type
a) = forall a. IsMeta a => a -> Maybe MetaId
isMeta Type
a
  isMeta CompareAs
AsSizes       = forall a. Maybe a
Nothing
  isMeta CompareAs
AsTypes       = 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 <- 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 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 = forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked t
t (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation) (forall a b. a -> b -> a
const 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 = 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Blocker
m) (\NotBlocked
_ t
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)

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

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

instance Reduce Type where
    reduce' :: Type -> ReduceM Type
reduce'  (El Sort
s Term
t) = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Term
t
    reduceB' :: Type -> ReduceM (Blocked Type)
reduceB' (El Sort
s Term
t) = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t a. Sort' t -> a -> Type'' t a
El Sort
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall t. Instantiate t => t -> ReduceM t
instantiate' Sort
s
      let done :: ReduceM (Blocked Sort)
done | MetaS MetaId
x Elims
_ <- Sort
s = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Sort
s
               | Bool
otherwise      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. a -> Blocked' t a
notBlocked Sort
s
      case Sort
s of
        PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Sort
s1 , Abs Sort
s2) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b (Sort
s1',Abs Sort
s2') -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ 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' <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ 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 -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        FunSort Sort
s1 Sort
s2 -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (Sort
s1 , Sort
s2) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b (Sort
s1',Sort
s2') -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
          NotBlocked NotBlocked
_ (Sort
s1',Sort
s2') -> case Sort -> Sort -> Either Blocker Sort
funSort' Sort
s1' Sort
s2' of
            Left Blocker
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
            Right Sort
s -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        UnivSort Sort
s1 -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Blocked Blocker
b Sort
s1' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t
UnivSort Sort
s1'
            Right Sort
s -> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Sort
s
        Prop Level
l     -> ReduceM (Blocked Sort)
done
        Type Level
l     -> ReduceM (Blocked Sort)
done
        Inf IsFibrant
f Integer
n    -> ReduceM (Blocked Sort)
done
        SSet Level
l     -> ReduceM (Blocked Sort)
done
        Sort
SizeUniv   -> ReduceM (Blocked Sort)
done
        Sort
LockUniv   -> ReduceM (Blocked Sort)
done
        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) = forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
v
  reduce' (Proj ProjOrigin
o QName
f)= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f
  reduce' (IApply Term
x Term
y Term
v) = forall a. a -> a -> a -> Elim' a
IApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Term
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Reduce t => t -> ReduceM t
reduce' [PlusLevel]
as
  reduceB' :: Level -> ReduceM (Blocked Level)
reduceB' (Max Integer
m [PlusLevel]
as) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> [PlusLevel] -> Level
levelMax Integer
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAny forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 String
x a
_) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. String -> a -> Abs a
Abs String
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
b forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'
  reduceB' (NoAbs String
x a
v) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. String -> a -> Abs a
NoAbs String
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 forall a. LensRelevance a => a -> Relevance
getRelevance Arg t
a of
      Relevance
Irrelevant -> forall (m :: * -> *) a. Monad m => a -> m a
return Arg t
a             -- Don't reduce' irr. args!?
                                         -- Andreas, 2018-03-03, caused #2989.
      Relevance
_          -> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Reduce t => t -> ReduceM t
reduce' Arg t
a

    reduceB' :: Arg t -> ReduceM (Blocked (Arg t))
reduceB' Arg t
t = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Reduce t => t -> ReduceM t
reduce'
    reduceB' :: Dom t -> ReduceM (Blocked (Dom t))
reduceB' Dom t
t = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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)  = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' a
x
      Blocked b
y <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' b
y
      let blk :: Blocked' Term ()
blk = forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked a
x forall a. Monoid a => a -> a -> a
`mappend` forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked b
y
          xy :: (a, b)
xy  = (forall t a. Blocked' t a -> a
ignoreBlocking Blocked a
x , forall t a. Blocked' t a -> a
ignoreBlocking Blocked b
y)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Blocked' Term ()
blk 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) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' a
x
      Blocked b
y <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' b
y
      Blocked c
z <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' c
z
      let blk :: Blocked' Term ()
blk = forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked a
x forall a. Monoid a => a -> a -> a
`mappend` forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked b
y forall a. Monoid a => a -> a -> a
`mappend` forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked c
z
          xyz :: (a, b, c)
xyz = (forall t a. Blocked' t a -> a
ignoreBlocking Blocked a
x , forall t a. Blocked' t a -> a
ignoreBlocking Blocked b
y , forall t a. Blocked' t a -> a
ignoreBlocking Blocked c
z)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Blocked' Term ()
blk 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) -> Elims -> ReduceM (Blocked Term)
reduceIApply = (Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply' 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))
-> ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply' Term -> ReduceM (Blocked Term)
red ReduceM (Blocked Term)
d (IApply Term
x Term
y Term
r : Elims
es) = do
  Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Blocked Term
r <- 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 (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
r) of
   IntervalView
IZero -> Term -> ReduceM (Blocked Term)
red (forall t. Apply t => t -> Elims -> t
applyE Term
x Elims
es)
   IntervalView
IOne  -> Term -> ReduceM (Blocked Term)
red (forall t. Apply t => t -> Elims -> t
applyE Term
y Elims
es)
   IntervalView
_     -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Blocked Term
r) ((Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply' Term -> ReduceM (Blocked Term)
red ReduceM (Blocked Term)
d Elims
es)
reduceIApply' Term -> ReduceM (Blocked Term)
red ReduceM (Blocked Term)
d (Elim
_ : Elims
es) = (Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply' Term -> ReduceM (Blocked Term)
red ReduceM (Blocked Term)
d Elims
es
reduceIApply' Term -> ReduceM (Blocked Term)
_   ReduceM (Blocked Term)
d [] = ReduceM (Blocked Term)
d

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

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

shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce = (PragmaOptions -> Bool
optFastReduce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do
  SmallSet AllowedReduction
allowed <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions
  let optionalReductions :: SmallSet AllowedReduction
optionalReductions = forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
NonTerminatingReductions, AllowedReduction
UnconfirmedReductions]
      requiredReductions :: SmallSet AllowedReduction
requiredReductions = SmallSet AllowedReduction
allReductions forall a.
SmallSetElement a =>
SmallSet a -> SmallSet a -> SmallSet a
SmallSet.\\ SmallSet AllowedReduction
optionalReductions
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (SmallSet AllowedReduction
allowed forall a.
SmallSetElement a =>
SmallSet a -> SmallSet a -> SmallSet a
SmallSet.\\ SmallSet AllowedReduction
optionalReductions) forall a. Eq a => a -> a -> Bool
== SmallSet AllowedReduction
requiredReductions

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
maybeFastReduceTerm :: Term -> ReduceM (Blocked 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)
slowReduceTerm Term
v
                 else
    case Term
v of
      MetaV MetaId
x Elims
_ -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall {f :: * -> *}. ReadTCState f => MetaId -> f Bool
isOpen MetaId
x) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Term
v) (Term -> ReduceM (Blocked Term)
maybeFast Term
v)
      Term
_         -> Term -> ReduceM (Blocked Term)
maybeFast Term
v
  where
    isOpen :: MetaId -> f Bool
isOpen MetaId
x = MetaInstantiation -> Bool
isOpenMeta forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
    maybeFast :: Term -> ReduceM (Blocked Term)
maybeFast Term
v = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ReduceM Bool
shouldTryFastReduce (Term -> ReduceM (Blocked Term)
fastReduce Term
v) (Term -> ReduceM (Blocked Term)
slowReduceTerm Term
v)

slowReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm Term
v = do
    Term
v <- forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
    let done :: ReduceM (Blocked Term)
done | MetaV MetaId
x Elims
_ <- Term
v = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x Term
v
             | Bool
otherwise      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. a -> Blocked' t a
notBlocked Term
v
        iapp :: Elims -> ReduceM (Blocked Term)
iapp = ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply ReduceM (Blocked 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)
iapp Elims
es
      Def QName
f Elims
es   -> forall a b c. (a -> b -> c) -> b -> a -> c
flip ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply Elims
es forall a b. (a -> b) -> a -> b
$ Bool
-> (Term -> ReduceM (Blocked Term))
-> Term
-> QName
-> Elims
-> ReduceM (Blocked Term)
unfoldDefinitionE Bool
False 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
v <- forall a b c. (a -> b -> c) -> b -> a -> c
flip ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply Elims
es
                 forall a b. (a -> b) -> a -> b
$ Bool
-> (Term -> ReduceM (Blocked Term))
-> Term
-> QName
-> Elims
-> ReduceM (Blocked Term)
unfoldDefinitionE Bool
False 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
          forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> ReduceM Term
reduceNat Blocked Term
v
      Sort Sort
s   -> ReduceM (Blocked Term)
done
      Level Level
l  -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.member AllowedReduction
LevelReductions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions)
                    {- then -} (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Term
levelTm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Level
l)
                    {- else -} ReduceM (Blocked Term)
done
      Pi Dom Type
_ Abs Type
_   -> ReduceM (Blocked Term)
done
      Lit Literal
_    -> ReduceM (Blocked Term)
done
      Var Int
_ Elims
es  -> Elims -> ReduceM (Blocked Term)
iapp Elims
es
      Lam ArgInfo
_ Abs Term
_  -> ReduceM (Blocked Term)
done
      DontCare Term
_ -> ReduceM (Blocked Term)
done
      Dummy{}    -> ReduceM (Blocked 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  <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinZero
        case Term
v of
          Term
_ | forall a. a -> Maybe a
Just Term
v forall a. Eq a => a -> a -> Bool
== Maybe Term
mz  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall a b. (a -> b) -> a -> b
$ Integer -> Literal
LitNat Integer
0
          Term
_                 -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
      reduceNat v :: Term
v@(Con ConHead
c ConInfo
ci [Apply Arg Term
a]) | forall a. LensHiding a => a -> Bool
visible Arg Term
a Bool -> Bool -> Bool
&& forall a. LensRelevance a => a -> Bool
isRelevant Arg Term
a = do
        Maybe Term
ms  <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSuc
        case Term
v of
          Term
_ | forall a. a -> Maybe a
Just (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) forall a. Eq a => a -> a -> Bool
== Maybe Term
ms -> Term -> Term
inc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' (forall e. Arg e -> e
unArg Arg Term
a)
          Term
_                         -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          where
            inc :: Term -> Term
inc = \case
              Lit (LitNat Integer
n) -> Literal -> Term
Lit forall a b. (a -> b) -> a -> b
$ Integer -> Literal
LitNat forall a b. (a -> b) -> a -> b
$ Integer
n forall a. Num a => a -> a -> a
+ Integer
1
              Term
w              -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
w]
      reduceNat Term
v = 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)           = forall a t. a -> Blocked' t a
notBlocked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
p
unfoldCorecursionE (Apply (Arg ArgInfo
info Term
v)) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  Term -> ReduceM (Blocked Term)
unfoldCorecursion Term
v
unfoldCorecursionE (IApply Term
x Term
y Term
r) = do -- TODO check if this makes sense
   [Blocked Term
x,Blocked Term
y,Blocked Term
r] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ReduceM (Blocked Term)
unfoldCorecursion [Term
x,Term
y,Term
r]
   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> a -> Elim' a
IApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Blocked Term
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Blocked Term
r

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

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

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

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

unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep :: Bool
-> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep Bool
unfoldDelayed Term
v0 QName
f Elims
es =
  {-# SCC "reduceDef" #-} do
  forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.reduce" Int
90 (TCMT IO Doc
"unfoldDefinitionStep v0" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v0) forall a b. (a -> b) -> a -> b
$ do
  Definition
info <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  [RewriteRule]
rewr <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
[RewriteRule] -> m [RewriteRule]
instantiateRewriteRules forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
  SmallSet AllowedReduction
allowed <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SmallSet AllowedReduction
envAllowedReductions
  Either Blocker Bool
prp <- forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
info
  Bool
defOk <- forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
shouldReduceDef QName
f
  let def :: Defn
def = Definition -> Defn
theDef Definition
info
      v :: Term
v   = Term
v0 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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
or
        [ Definition -> Bool
defNonterminating Definition
info Bool -> Bool -> Bool
&& forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.notMember AllowedReduction
NonTerminatingReductions SmallSet AllowedReduction
allowed
        , Definition -> Bool
defTerminationUnconfirmed Definition
info Bool -> Bool -> Bool
&& forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.notMember AllowedReduction
UnconfirmedReductions SmallSet AllowedReduction
allowed
        , Definition -> Delayed
defDelayed Definition
info forall a. Eq a => a -> a -> Bool
== Delayed
Delayed Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
unfoldDelayed
        , Either Blocker Bool
prp forall a. Eq a => a -> a -> Bool
== forall a b. b -> Either a b
Right Bool
True
        , 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 forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
f) ConInfo
ConOSystem
      Blocked' Term ()
-> (Elims -> Term)
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()) Elims -> Term
hd [RewriteRule]
rewr Elims
es
    Primitive{primAbstr :: Defn -> IsAbstract
primAbstr = IsAbstract
ConcreteDef, primName :: Defn -> String
primName = String
x, primClauses :: Defn -> [Clause]
primClauses = [Clause]
cls} -> do
      PrimFun
pf <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' String
x
      if AllowedReduction
FunctionReductions forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
        then String
-> Term
-> QName
-> Elims
-> PrimFun
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> ReduceM (Reduced (Blocked Term) Term)
reducePrimitive String
x Term
v0 QName
f Elims
es PrimFun
pf Bool
dontUnfold
                             [Clause]
cls (Definition -> Maybe CompiledClauses
defCompiled Definition
info) [RewriteRule]
rewr
        else forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ forall a t. a -> Blocked' t a
notBlocked Term
v
    PrimitiveSort{ primSortSort :: Defn -> Sort
primSortSort = Sort
s } -> forall {m :: * -> *} {a} {no}.
Monad m =>
Simplification -> a -> m (Reduced no a)
yesReduction Simplification
NoSimplification forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s forall t. Apply t => t -> Elims -> t
`applyE` Elims
es

    Defn
_  -> do
      if forall (t :: * -> *). Foldable t => t Bool -> Bool
or
          [ AllowedReduction
RecursiveReductions forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
          , forall a. Maybe a -> Bool
isJust (Defn -> Maybe Projection
isProjection_ Defn
def) Bool -> Bool -> Bool
&& AllowedReduction
ProjectionReductions 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 forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
          , Defn -> Bool
definitelyNonRecursive_ Defn
def Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
or
            [ Bool
copatterns Bool -> Bool -> Bool
&& AllowedReduction
CopatternReductions forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
            , AllowedReduction
FunctionReductions forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed
            ]
          ]
        then
          Term
-> QName
-> [MaybeReduced Elim]
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> ReduceM (Reduced (Blocked Term) Term)
reduceNormalE Term
v0 QName
f (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced Elims
es) Bool
dontUnfold
                       (Definition -> [Clause]
defClauses Definition
info) (Definition -> Maybe CompiledClauses
defCompiled Definition
info) [RewriteRule]
rewr
        else forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ forall a t. a -> Blocked' t a
notBlocked Term
v  -- Andrea(s), 2014-12-05 OK?

  where
    noReduction :: a -> ReduceM (Reduced a yes)
noReduction    = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall no yes. no -> Reduced no yes
NoReduction
    yesReduction :: Simplification -> a -> m (Reduced no a)
yesReduction Simplification
s = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
s
    reducePrimitive :: String
-> Term
-> QName
-> Elims
-> PrimFun
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> ReduceM (Reduced (Blocked Term) Term)
reducePrimitive String
x Term
v0 QName
f Elims
es PrimFun
pf Bool
dontUnfold [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es forall a. Ord a => a -> a -> Bool
< Int
ar
                  = forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
Underapplied forall a b. (a -> b) -> a -> b
$ Term
v0 forall t. Apply t => t -> Elims -> t
`applyE` Elims
es -- not fully applied
      | Bool
otherwise = {-# SCC "reducePrimitive" #-} do
          let (Elims
es1,Elims
es2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
ar Elims
es
              args1 :: [Arg Term]
args1     = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 (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' = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args1'
              if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Clause]
cls Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewriteRule]
rewr then do
                forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> Elims -> t
applyE (QName -> Elims -> Term
Def QName
f []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
                  forall (f :: * -> *) a.
(Functor f, Foldable f) =>
f (Blocked a) -> Blocked (f a)
blockAll forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. IsMeta t => MaybeReduced t -> Blocked t
mredToBlocked [MaybeReduced Elim]
es1' forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a t. a -> Blocked' t a
notBlocked Elims
es2
               else
                Term
-> QName
-> [MaybeReduced Elim]
-> Bool
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> ReduceM (Reduced (Blocked Term) Term)
reduceNormalE Term
v0 QName
f ([MaybeReduced Elim]
es1' forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced Elims
es2) Bool
dontUnfold [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr
            YesReduction Simplification
simpl Term
v -> forall {m :: * -> *} {a} {no}.
Monad m =>
Simplification -> a -> m (Reduced no a)
yesReduction Simplification
simpl forall a b. (a -> b) -> a -> b
$ Term
v 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) = forall a t. a -> Blocked' t a
notBlocked t
e
          mredToBlocked (MaybeRed (Reduced Blocked' Term ()
b) t
e) = t
e 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
-> [RewriteRule]
-> ReduceM (Reduced (Blocked Term) Term)
reduceNormalE Term
v0 QName
f [MaybeReduced Elim]
es Bool
dontUnfold [Clause]
def Maybe CompiledClauses
mcc [RewriteRule]
rewr = {-# SCC "reduceNormal" #-} do
      forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.reduce" Int
90 (TCMT IO Doc
"reduceNormalE v0 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v0) forall a b. (a -> b) -> a -> b
$ do
      case ([Clause]
def,[RewriteRule]
rewr) of
        ([Clause], [RewriteRule])
_ | Bool
dontUnfold -> forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
traceSLn String
"tc.reduce" Int
90 String
"reduceNormalE: don't unfold (non-terminating or delayed)" forall a b. (a -> b) -> a -> b
$
                          ReduceM (Reduced (Blocked Term) Term)
defaultResult -- non-terminating or delayed
        ([],[])        -> forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
traceSLn String
"tc.reduce" Int
90 String
"reduceNormalE: no clauses or rewrite rules" forall a b. (a -> b) -> a -> b
$ do
          -- no definition for head
          Blocked' Term ()
blk <- Definition -> Blocked' Term ()
defBlocked forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ Blocked' Term ()
blk forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
vfull
        ([Clause]
cls,[RewriteRule]
rewr)     -> do
          Reduced (Blocked Term) Term
ev <- QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr [MaybeReduced Elim]
es
          Reduced (Blocked Term) Term -> ReduceM ()
debugReduce Reduced (Blocked Term) Term
ev
          forall (m :: * -> *) a. Monad m => a -> m a
return Reduced (Blocked Term) Term
ev
      where
      defaultResult :: ReduceM (Reduced (Blocked Term) Term)
defaultResult = forall {a} {yes}. a -> ReduceM (Reduced a yes)
noReduction forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked Term
vfull
      vfull :: Term
vfull         = Term
v0 forall t. Apply t => t -> Elims -> t
`applyE` forall a b. (a -> b) -> [a] -> [b]
map forall a. MaybeReduced a -> a
ignoreReduced [MaybeReduced Elim]
es
      debugReduce :: Reduced (Blocked Term) Term -> ReduceM ()
debugReduce Reduced (Blocked Term) Term
ev = forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"tc.reduce" Int
90 forall a b. (a -> b) -> a -> b
$ do
        case Reduced (Blocked Term) Term
ev of
          NoReduction Blocked Term
v -> do
            forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.reduce" Int
90 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"*** tried to reduce " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
              , TCMT IO Doc
"    es =  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. MaybeReduced a -> a
ignoreReduced) [MaybeReduced Elim]
es)
              -- , "*** tried to reduce " <+> pretty vfull
              , TCMT IO Doc
"    stuck on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
v)
              ]
          YesReduction Simplification
_simpl Term
v -> do
            forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.reduce"  Int
90 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"*** reduced definition: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
            forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.reduce"  Int
95 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"    result" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 = 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  case Definition -> Defn
theDef Definition
info of
    Defn
_ | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Definition -> Bool
defCopy Definition
info     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction ()
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = 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 String] -> Term -> Term
unlamView [Arg String]
xs, Elims
newes)
              where
                etaArgs :: NAPs -> [a] -> [Arg String]
etaArgs [] [a]
_ = []
                etaArgs (NamedArg DeBruijnPattern
p : NAPs
ps) []
                  | VarP PatternInfo
_ DBPatVar
x <- forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p = forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg DeBruijnPattern
p) (DBPatVar -> String
dbPatVarName DBPatVar
x) forall a. a -> [a] -> [a]
: NAPs -> [a] -> [Arg String]
etaArgs NAPs
ps []
                  | Bool
otherwise              = []
                etaArgs (NamedArg DeBruijnPattern
_ : NAPs
ps) (a
_ : [a]
es) = NAPs -> [a] -> [Arg String]
etaArgs NAPs
ps [a]
es
                xs :: [Arg String]
xs  = forall {a}. NAPs -> [a] -> [Arg String]
etaArgs NAPs
ps Elims
es
                n :: Int
n   = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg String]
xs
                newes :: Elims
newes = forall a. Subst a => Int -> a -> a
raise Int
n Elims
es forall a. [a] -> [a] -> [a]
++ [ forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg String
x | (Int
i, Arg String
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Integral a => a -> [a]
downFrom Int
n) [Arg String]
xs ]
        if (Definition -> Delayed
defDelayed Definition
info forall a. Eq a => a -> a -> Bool
== Delayed
Delayed) Bool -> Bool -> Bool
|| (Definition -> Bool
defNonterminating Definition
info)
         then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction ()
         else do
            Reduced (Blocked Term) Term
ev <- forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE_ QName
f Term
v0 [Clause
cl] forall a. Maybe a
Nothing forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced Elims
es'
            case Reduced (Blocked Term) Term
ev of
              YesReduction Simplification
simpl Term
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl (Term -> Term
lam Term
t)
              NoReduction{}        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction ()
      []    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction ()  -- copies of generalizable variables have no clauses (and don't need unfolding)
      Clause
_:Clause
_:[Clause]
_ -> 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)
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 <- forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
  forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.inj.reduce" Int
30 (forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"reduceHead" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v) forall a b. (a -> b) -> a -> b
$ do
  case Term
v of
    Def QName
f Elims
es -> do

      AbstractMode
abstractMode <- TCEnv -> AbstractMode
envAbstractMode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
      Bool
isAbstract <- forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
treatAbstractly QName
f
      forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
traceSLn String
"tc.inj.reduce" Int
50 (
        String
"reduceHead: we are in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AbstractMode
abstractModeforall a. [a] -> [a] -> [a]
++ String
"; " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
f forall a. [a] -> [a] -> [a]
++
        String
" is treated " forall a. [a] -> [a] -> [a]
++ if Bool
isAbstract then String
"abstractly" else String
"concretely"
        ) forall a b. (a -> b) -> a -> b
$ do
      let v0 :: Term
v0  = QName -> Elims -> Term
Def QName
f []
          red :: m (Blocked Term)
red = forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ Bool
-> (Term -> ReduceM (Blocked Term))
-> Term
-> QName
-> Elims
-> ReduceM (Blocked Term)
unfoldDefinitionE Bool
False forall (m :: * -> *). PureTCM m => Term -> m (Blocked Term)
reduceHead Term
v0 QName
f Elims
es
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_ ], funDelayed :: Defn -> Delayed
funDelayed = Delayed
NotDelayed, funTerminates :: Defn -> Maybe Bool
funTerminates = Just Bool
True } -> do
          forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
traceSLn String
"tc.inj.reduce" Int
50 (String
"reduceHead: head " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ String
" is Function") forall a b. (a -> b) -> a -> b
$ do
          m (Blocked Term)
red
        Datatype{ dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
_ } -> m (Blocked Term)
red
        Record{ recClause :: Defn -> Maybe Clause
recClause = Just Clause
_ }    -> m (Blocked Term)
red
        Defn
_                               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a t. a -> Blocked' t a
notBlocked Term
v
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eWorkingOnTypes
  case Term
v of
    Term
_ | Bool
inTypes -> 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      let def :: Defn
def = Definition -> Defn
theDef Definition
info
          irr :: Bool
irr = forall a. LensRelevance a => a -> Bool
isIrrelevant forall a b. (a -> b) -> a -> b
$ Definition -> ArgInfo
defArgInfo Definition
info
      case Defn
def of   -- Only for simple definitions with no pattern matching (TODO: maybe copatterns?)
        Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just Done{}, funDelayed :: Defn -> Delayed
funDelayed = Delayed
NotDelayed }
          | Defn
def forall o i. o -> Lens' i o -> i
^. Lens' Bool Defn
funInline , Bool -> Bool
not Bool
irr -> forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$
          forall t a. Blocked' t a -> a
ignoreBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> (Term -> ReduceM (Blocked Term))
-> Term
-> QName
-> Elims
-> ReduceM (Blocked Term)
unfoldDefinitionE Bool
False (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. a -> Blocked' t a
notBlocked) (QName -> Elims -> Term
Def QName
f []) QName
f Elims
es
        Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    Term
_ -> 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
-> [RewriteRule]
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked Term) Term)
appDef_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr MaybeReducedArgs
args = QName
-> Term
-> [Clause]
-> Maybe CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE_ QName
f Term
v0 [Clause]
cls Maybe CompiledClauses
mcc [RewriteRule]
rewr [MaybeReduced Elim]
args =
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envAppDef :: Maybe QName
envAppDef = forall a. a -> Maybe a
Just QName
f }) forall a b. (a -> b) -> a -> b
$
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Term
-> [Clause]
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE'' Term
v0 [Clause]
cls [RewriteRule]
rewr [MaybeReduced Elim]
args)
        (\CompiledClauses
cc -> Term
-> CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE Term
v0 CompiledClauses
cc [RewriteRule]
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
-> [RewriteRule]
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked Term) Term)
appDef Term
v CompiledClauses
cc [RewriteRule]
rewr MaybeReducedArgs
args = Term
-> CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE Term
v CompiledClauses
cc [RewriteRule]
rewr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args

appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE :: Term
-> CompiledClauses
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE Term
v CompiledClauses
cc [RewriteRule]
rewr [MaybeReduced Elim]
es = do
  forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.reduce" Int
90 (TCMT IO Doc
"appDefE v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v) 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl Term
t
    NoReduction Blocked' Term Elims
es'      -> Blocked' Term ()
-> (Elims -> Term)
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite (forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked' Term Elims
es') (forall t. Apply t => t -> Elims -> t
applyE Term
v) [RewriteRule]
rewr (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]
-> [RewriteRule]
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked Term) Term)
appDef' QName
f Term
v [Clause]
cls [RewriteRule]
rewr MaybeReducedArgs
args = QName
-> Term
-> [Clause]
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE' QName
f Term
v [Clause]
cls [RewriteRule]
rewr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args

appDefE' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE' :: QName
-> Term
-> [Clause]
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE' QName
f Term
v [Clause]
cls [RewriteRule]
rewr [MaybeReduced Elim]
es =
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envAppDef :: Maybe QName
envAppDef = forall a. a -> Maybe a
Just QName
f }) forall a b. (a -> b) -> a -> b
$
  Term
-> [Clause]
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE'' Term
v [Clause]
cls [RewriteRule]
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]
-> [RewriteRule]
-> [MaybeReduced Elim]
-> ReduceM (Reduced (Blocked Term) Term)
appDefE'' Term
v [Clause]
cls [RewriteRule]
rewr [MaybeReduced Elim]
es = forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.reduce" Int
90 (TCMT IO Doc
"appDefE' v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v) forall a b. (a -> b) -> a -> b
$ do
  [Clause] -> Elims -> ReduceM (Reduced (Blocked Term) Term)
goCls [Clause]
cls forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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)
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 <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe QName
envAppDef
          Blocked' Term ()
-> (Elims -> Term)
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) (forall t. Apply t => t -> Elims -> t
applyE Term
v) [RewriteRule]
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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
pats
              nvars :: Int
nvars = forall a. Sized a => a -> Int
size forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl
          -- if clause is underapplied, skip to next clause
          if forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es forall a. Ord a => a -> a -> Bool
< Int
npats then [Clause] -> Elims -> ReduceM (Reduced (Blocked Term) Term)
goCls [Clause]
cls Elims
es else do
            let (Elims
es0, Elims
es1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
npats Elims
es
            (Match Term
m, Elims
es0) <- forall (m :: * -> *).
MonadMatch m =>
NAPs -> Elims -> m (Match Term, Elims)
matchCopatterns NAPs
pats Elims
es0
            let es :: Elims
es = Elims
es0 forall a. [a] -> [a] -> [a]
++ Elims
es1
            case Match Term
m of
              Match Term
No         -> [Clause] -> Elims -> ReduceM (Reduced (Blocked Term) Term)
goCls [Clause]
cls Elims
es
              DontKnow Blocked' Term ()
b -> Blocked' Term ()
-> (Elims -> Term)
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked' Term ()
b (forall t. Apply t => t -> Elims -> t
applyE Term
v) [RewriteRule]
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 = forall a.
DeBruijn a =>
Impossible -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution HasCallStack => Impossible
impossible Int
nvars IntMap (Arg Term)
vs
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sigma Term
w forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1
                | Bool
otherwise     -> Blocked' Term ()
-> (Elims -> Term)
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
AbsurdMatch ()) (forall t. Apply t => t -> Elims -> t
applyE Term
v) [RewriteRule]
rewr Elims
es

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

instance Reduce Telescope where
  reduce' :: Telescope -> ReduceM Telescope
reduce' Telescope
EmptyTel          = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Tele a
EmptyTel
  reduce' (ExtendTel Dom Type
a Abs Telescope
tel) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Dom Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) <- forall t. Reduce t => t -> ReduceM t
reduce' (CompareAs
t,Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall t. Reduce t => t -> ReduceM t
reduce' ((Term
p,Type
t),Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Term
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Elims
as forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Elims
bs
  reduce' (LevelCmp Comparison
cmp Level
u Level
v)    = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' (Level
u,Level
v)
  reduce' (SortCmp Comparison
cmp Sort
a Sort
b)     = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' (Sort
a,Sort
b)
  reduce' (UnBlock MetaId
m)           = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Reduce t => t -> ReduceM t
reduce' Maybe [Candidate]
cs
  reduce' (IsEmpty Range
r Type
t)         = Range -> Type -> Constraint
IsEmpty Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (CheckSizeLtSat Term
t)    = Term -> Constraint
CheckSizeLtSat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Term
t
  reduce' c :: Constraint
c@CheckFunDef{}       = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  reduce' (HasBiggerSort Sort
a)     = Sort -> Constraint
HasBiggerSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Sort
a
  reduce' (HasPTSRule Dom Type
a Abs Sort
b)      = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Sort -> Constraint
HasPTSRule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Term
h forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Type
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Type
d
  reduce' (CheckDataSort QName
q Sort
s)   = QName -> Sort -> Constraint
CheckDataSort QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Sort
s
  reduce' c :: Constraint
c@CheckMetaInst{}     = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  reduce' (CheckType Type
t)         = Type -> Constraint
CheckType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = forall a b c. (a -> b -> c) -> b -> a -> c
flip (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc) Modality
mod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Maybe Sort
ms forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Type
a
  reduce' CompareAs
AsSizes       = forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
  reduce' CompareAs
AsTypes       = 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Reduce t => t -> ReduceM t
reduce'

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

instance Reduce EqualityView where
  reduce' :: EqualityView -> ReduceM EqualityView
reduce' (OtherType Type
t)            = Type -> EqualityView
OtherType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Type
t
  reduce' (IdiomType Type
t)            = Type -> EqualityView
IdiomType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Sort
s
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return QName
eq
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Reduce t => t -> ReduceM t
reduce' [Arg Term]
l
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
t
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Arg Term
a
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Reduce t => t -> ReduceM t
reduce'
  reduceB' :: IPBoundary' t -> ReduceM (Blocked (IPBoundary' t))
reduceB' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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)) <- forall t. Simplify t => t -> ReduceM t
simplify' (a
x,(b
y,c
z))
            forall (m :: * -> *) a. Monad m => a -> m a
return (a
x,b
y,c
z)

instance Simplify Bool where
  simplify' :: Bool -> ReduceM Bool
simplify' = 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 <- forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
    let iapp :: Elims -> ReduceM Term -> ReduceM Term
iapp Elims
es ReduceM Term
m = forall t a. Blocked' t a -> a
ignoreBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> Elims -> ReduceM (Blocked Term)
reduceIApply' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a t. a -> Blocked' t a
notBlocked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Simplify t => t -> ReduceM t
simplify') (forall a t. a -> Blocked' t a
notBlocked 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 forall a b. (a -> b) -> a -> b
$ do
        let keepGoing :: a -> a -> m (a, Blocked' t a)
keepGoing a
simp a
v = forall (m :: * -> *) a. Monad m => a -> m a
return (a
simp, forall a t. a -> Blocked' t a
notBlocked a
v)
        (Simplification
simpl, Blocked Term
v) <- Bool
-> (Simplification
    -> Term -> ReduceM (Simplification, Blocked Term))
-> Term
-> QName
-> Elims
-> ReduceM (Simplification, Blocked Term)
unfoldDefinition' Bool
False 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
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Simplification
simpl forall a. Eq a => a -> a -> Bool
== Simplification
YesSimplification) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.simplify'" Int
90 forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"simplify': unfolding definition returns " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Simplification
simpl) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
v)
        case Simplification
simpl of
          Simplification
YesSimplification -> forall t. Simplify t => Blocked t -> ReduceM t
simplifyBlocked' Blocked Term
v -- Dangerous, but if @simpl@ then @v /= Def f vs@
          Simplification
NoSimplification  -> QName -> Elims -> Term
Def QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      MetaV MetaId
x Elims
vs -> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      Sort Sort
s     -> Sort -> Term
Sort     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s
      Level Level
l    -> Level -> Term
levelTm  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Level
l
      Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
Pi       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Dom Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Abs Type
b
      Lit Literal
l      -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
      Var Int
i Elims
vs   -> Elims -> ReduceM Term -> ReduceM Term
iapp Elims
vs forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
i    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
vs
      Lam ArgInfo
h Abs Term
v    -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Abs Term
v
      DontCare Term
v -> Term -> Term
dontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Term
v
      Dummy{}    -> 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) = forall (m :: * -> *) a. Monad m => a -> m a
return t
t
simplifyBlocked' (NotBlocked NotBlocked
_ t
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) = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Dom' Term Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Abs Sort
s2
        FunSort Sort
s1 Sort
s2 -> Sort -> Sort -> Sort
funSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s2
        UnivSort Sort
s -> Sort -> Sort
univSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s
        Type Level
s     -> forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Level
s
        Prop Level
s     -> forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Level
s
        Inf IsFibrant
_ Integer
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        SSet Level
s     -> forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Level
s
        Sort
SizeUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
LockUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        MetaS MetaId
x Elims
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
es
        DefS QName
d Elims
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
es
        DummyS{}   -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' [PlusLevel]
as

instance Simplify PlusLevel where
  simplify' :: PlusLevel -> ReduceM PlusLevel
simplify' (Plus Integer
n Term
l) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 String
x a
_) = forall a. String -> a -> Abs a
Abs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
a forall t. Simplify t => t -> ReduceM t
simplify'
    simplify' (NoAbs String
x a
v) = forall a. String -> a -> Abs a
NoAbs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' a
v

instance Simplify t => Simplify (Dom t) where
    simplify' :: Dom t -> ReduceM (Dom t)
simplify' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 <- forall a c b. LensClosure a c => c -> (a -> ReduceM b) -> ReduceM b
enterClosure Closure a
cl forall t. Simplify t => t -> ReduceM t
simplify'
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Closure a
cl { clValue :: a
clValue = a
x }

instance (Subst a, Simplify a) => Simplify (Tele a) where
  simplify' :: Tele a -> ReduceM (Tele a)
simplify' Tele a
EmptyTel        = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Tele a
EmptyTel
  simplify' (ExtendTel a
a Abs (Tele a)
b) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. a -> Abs (Tele a) -> Tele a
ExtendTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) <- forall t. Simplify t => t -> ReduceM t
simplify' (CompareAs
t,Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall t. Simplify t => t -> ReduceM t
simplify' ((Term
p,Type
t),Term
u,Term
v)
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Term
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Elims
as forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Elims
bs
  simplify' (LevelCmp Comparison
cmp Level
u Level
v)    = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' (Level
u,Level
v)
  simplify' (SortCmp Comparison
cmp Sort
a Sort
b)     = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' (Sort
a,Sort
b)
  simplify' (UnBlock MetaId
m)           = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. Simplify t => t -> ReduceM t
simplify' Maybe [Candidate]
cs
  simplify' (IsEmpty Range
r Type
t)         = Range -> Type -> Constraint
IsEmpty Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Type
t
  simplify' (CheckSizeLtSat Term
t)    = Term -> Constraint
CheckSizeLtSat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Term
t
  simplify' c :: Constraint
c@CheckFunDef{}       = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  simplify' (HasBiggerSort Sort
a)     = Sort -> Constraint
HasBiggerSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
a
  simplify' (HasPTSRule Dom Type
a Abs Sort
b)      = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Sort -> Constraint
HasPTSRule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' (Dom Type
a,Abs Sort
b)
  simplify' (UnquoteTactic Term
t Term
h Type
g) = Term -> Term -> Type -> Constraint
UnquoteTactic forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Term
h forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Type
g
  simplify' (CheckLockedVars Term
a Type
b Arg Term
c Type
d) =
    Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Type
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Arg Term
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Type
d
  simplify' (CheckDataSort QName
q Sort
s)   = QName -> Sort -> Constraint
CheckDataSort QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Sort
s
  simplify' c :: Constraint
c@CheckMetaInst{}     = forall (m :: * -> *) a. Monad m => a -> m a
return Constraint
c
  simplify' (CheckType Type
t)         = Type -> Constraint
CheckType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Type
t
  simplify' (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = forall a b c. (a -> b -> c) -> b -> a -> c
flip (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc) Modality
mod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Maybe Sort
ms forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Simplify t => t -> ReduceM t
simplify' Term
t

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

-- UNUSED
-- instance Simplify ConPatternInfo where
--   simplify' (ConPatternInfo mr mt) = ConPatternInfo mr <$> simplify' mt

-- UNUSED
-- instance Simplify Pattern where
--   simplify' p = case p of
--     VarP _       -> return p
--     LitP _       -> return p
--     ConP c ci ps -> ConP c <$> simplify' ci <*> simplify' ps
--     DotP v       -> DotP <$> simplify' v
--     ProjP _      -> return p

instance Simplify DisplayForm where
  simplify' :: DisplayForm -> ReduceM DisplayForm
simplify' (Display Int
n Elims
ps DisplayTerm
v) = Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Simplify t => t -> ReduceM t
simplify' Elims
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return DisplayTerm
v

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

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

---------------------------------------------------------------------------
-- * Normalisation
---------------------------------------------------------------------------

class Normalise t where
  normalise' :: t -> ReduceM t

  default normalise' :: (t ~ f a, Traversable f, Normalise a) => t -> ReduceM t
  normalise' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Normalise t => t -> ReduceM t
normalise'

-- boring instances:

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

-- Arg not included since we do not normalize irrelevant subterms
-- Elim' not included since it contains Arg
instance Normalise t => Normalise (Named name t)
instance Normalise t => Normalise (IPBoundary' t)
instance Normalise t => Normalise (WithHiding t)

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

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

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

instance Normalise Char where
  normalise' :: Char -> ReduceM Char
normalise' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance Normalise Int where
  normalise' :: Int -> ReduceM Int
normalise' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance Normalise DBPatVar where
  normalise' :: DBPatVar -> ReduceM DBPatVar
normalise' = forall (m :: * -> *) a. Monad m => a -> m a
return

-- interesting instances:

instance Normalise Sort where
    normalise' :: Sort -> ReduceM Sort
normalise' Sort
s = do
      Sort
s <- forall t. Reduce t => t -> ReduceM t
reduce' Sort
s
      case Sort
s of
        PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Dom' Term Term -> Sort -> Abs Sort -> Sort
piSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Dom' Term Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' Abs Sort
s2
        FunSort Sort
s1 Sort
s2 -> Sort -> Sort -> Sort
funSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' Sort
s2
        UnivSort Sort
s -> Sort -> Sort
univSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Sort
s
        Prop Level
s     -> forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Level
s
        Type Level
s     -> forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Level
s
        Inf IsFibrant
_ Integer
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        SSet Level
s     -> forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Level
s
        Sort
SizeUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
SizeUniv
        Sort
LockUniv   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
LockUniv
        Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
IntervalUniv
        MetaS MetaId
x Elims
es -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        DefS QName
d Elims
es  -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        DummyS{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s

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

instance Normalise Term where
    normalise' :: Term -> ReduceM Term
normalise' Term
v = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ReduceM Bool
shouldTryFastReduce (Term -> ReduceM Term
fastNormalise Term
v) (Term -> ReduceM Term
slowNormaliseArgs forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t. Reduce t => t -> ReduceM t
reduce' Term
v)

slowNormaliseArgs :: Term -> ReduceM Term
slowNormaliseArgs :: Term -> ReduceM Term
slowNormaliseArgs = \case
  Var Int
n Elims
vs    -> Int -> Elims -> Term
Var Int
n      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Elims
vs
  Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Elims
vs
  Def QName
f Elims
vs    -> QName -> Elims -> Term
Def QName
f      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Elims
vs
  MetaV MetaId
x Elims
vs  -> MetaId -> Elims -> Term
MetaV MetaId
x    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Elims
vs
  v :: Term
v@(Lit Literal
_)   -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  Level Level
l     -> Level -> Term
levelTm    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Level
l
  Lam ArgInfo
h Abs Term
b     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Abs Term
b
  Sort Sort
s      -> Sort -> Term
Sort       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Sort
s
  Pi Dom Type
a Abs Type
b      -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' (Dom Type
a, Abs Type
b)
  v :: Term
v@DontCare{}-> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  v :: Term
v@Dummy{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- Note: not the default instance for Elim' since we do something special for Arg.
instance Normalise t => Normalise (Elim' t) where
  normalise' :: Elim' t -> ReduceM (Elim' t)
normalise' (Apply Arg t
v) = forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Arg t
v  -- invokes Normalise Arg here
  normalise' (Proj ProjOrigin
o QName
f)= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f
  normalise' (IApply t
x t
y t
v) = forall a. a -> a -> a -> Elim' a
IApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' t
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' t
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' t
v

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

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

instance (Subst a, Normalise a) => Normalise (Abs a) where
    normalise' :: Abs a -> ReduceM (Abs a)
normalise' a :: Abs a
a@(Abs String
x a
_) = forall a. String -> a -> Abs a
Abs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
a forall t. Normalise t => t -> ReduceM t
normalise'
    normalise' (NoAbs String
x a
v) = forall a. String -> a -> Abs a
NoAbs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' a
v

instance Normalise t => Normalise (Arg t) where
    normalise' :: Arg t -> ReduceM (Arg t)
normalise' Arg t
a
      | forall a. LensRelevance a => a -> Bool
isIrrelevant Arg t
a = forall (m :: * -> *) a. Monad m => a -> m a
return Arg t
a -- Andreas, 2012-04-02: Do not normalize irrelevant terms!?
      | Bool
otherwise      = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Normalise t => t -> ReduceM t
normalise' Arg t
a

instance Normalise t => Normalise (Dom t) where
    normalise' :: Dom t -> ReduceM (Dom t)
normalise' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Normalise t => t -> ReduceM t
normalise'

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

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

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

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

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

instance Normalise ConPatternInfo where
  normalise' :: ConPatternInfo -> ReduceM ConPatternInfo
normalise' ConPatternInfo
i = forall t. Normalise t => t -> ReduceM t
normalise' (ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Maybe (Arg Type)
t -> ConPatternInfo
i { conPType :: Maybe (Arg Type)
conPType = Maybe (Arg Type)
t }

instance Normalise a => Normalise (Pattern' a) where
  normalise' :: Pattern' a -> ReduceM (Pattern' a)
normalise' Pattern' a
p = case Pattern' a
p of
    VarP PatternInfo
o a
x     -> forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' a
x
    LitP{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
    ConP ConHead
c ConPatternInfo
mt [NamedArg (Pattern' a)]
ps -> forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' ConPatternInfo
mt forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' [NamedArg (Pattern' a)]
ps
    DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps  -> forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' [NamedArg (Pattern' a)]
ps
    DotP PatternInfo
o Term
v     -> forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Term
v
    ProjP{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
    IApplyP PatternInfo
o Term
t Term
u a
x -> forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Normalise t => t -> ReduceM t
normalise' a
x

instance Normalise DisplayForm where
  normalise' :: DisplayForm -> ReduceM DisplayForm
normalise' (Display Int
n Elims
ps DisplayTerm
v) = Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Normalise t => t -> ReduceM t
normalise' Elims
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return DisplayTerm
v

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

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

---------------------------------------------------------------------------
-- * Full instantiation
---------------------------------------------------------------------------

-- | @instantiateFull'@ 'instantiate's metas everywhere (and recursively)
--   but does not 'reduce'.
class InstantiateFull t where
  instantiateFull' :: t -> ReduceM t

  default instantiateFull' :: (t ~ f a, Traversable f, InstantiateFull a) => t -> ReduceM t
  instantiateFull' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. InstantiateFull t => t -> ReduceM t
instantiateFull'

-- Traversables (doesn't include binders like Abs, Tele):

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

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

-- Tuples:

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

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

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

-- Base types:

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

instance InstantiateFull Char where
    instantiateFull' :: Char -> ReduceM Char
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull Int where
    instantiateFull' :: Int -> ReduceM Int
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull ModuleName where
    instantiateFull' :: ModuleName -> ReduceM ModuleName
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull Name where
    instantiateFull' :: Name -> ReduceM Name
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull QName where
  instantiateFull' :: QName -> ReduceM QName
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull Scope where
    instantiateFull' :: Scope -> ReduceM Scope
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull ConHead where
  instantiateFull' :: ConHead -> ReduceM ConHead
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

instance InstantiateFull DBPatVar where
    instantiateFull' :: DBPatVar -> ReduceM DBPatVar
instantiateFull' = forall (m :: * -> *) a. Monad m => a -> m a
return

-- Rest:

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

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

instance InstantiateFull Term where
    instantiateFull' :: Term -> ReduceM Term
instantiateFull' = forall t. Instantiate t => t -> ReduceM t
instantiate' forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term -> ReduceM Term
recurse forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
Term -> m Term
etaOnce
      -- Andreas, 2010-11-12 DONT ETA!? eta-reduction breaks subject reduction
      -- but removing etaOnce now breaks everything
      where
        recurse :: Term -> ReduceM Term
recurse = \case
          Var Int
n Elims
vs    -> Int -> Elims -> Term
Var Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
vs
          Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
vs
          Def QName
f Elims
vs    -> QName -> Elims -> Term
Def QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
vs
          MetaV MetaId
x Elims
vs  -> MetaId -> Elims -> Term
MetaV MetaId
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
vs
          v :: Term
v@Lit{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Level Level
l     -> Level -> Term
levelTm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Level
l
          Lam ArgInfo
h Abs Term
b     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Abs Term
b
          Sort Sort
s      -> Sort -> Term
Sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Sort
s
          Pi Dom Type
a Abs Type
b      -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Dom Type
a,Abs Type
b)
          DontCare Term
v  -> Term -> Term
dontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
v
          v :: Term
v@Dummy{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

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

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

instance InstantiateFull Substitution where
  instantiateFull' :: Substitution' Term -> ReduceM (Substitution' Term)
instantiateFull' Substitution' Term
sigma =
    case Substitution' Term
sigma of
      Substitution' Term
IdS                    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Substitution' a
IdS
      EmptyS Impossible
err             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Impossible -> Substitution' a
EmptyS Impossible
err
      Wk   Int
n Substitution' Term
sigma           -> forall a. Int -> Substitution' a -> Substitution' a
Wk   Int
n           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Substitution' Term
sigma
      Lift Int
n Substitution' Term
sigma           -> forall a. Int -> Substitution' a -> Substitution' a
Lift Int
n           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Substitution' Term
sigma
      Strengthen Impossible
bot Int
n Substitution' Term
sigma -> forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
bot Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Substitution' Term
sigma
      Term
t :# Substitution' Term
sigma             -> forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
t
                                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Substitution' Term
sigma

instance InstantiateFull ConPatternInfo where
    instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo
instantiateFull' ConPatternInfo
i = forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Maybe (Arg Type)
t -> ConPatternInfo
i { conPType :: Maybe (Arg Type)
conPType = Maybe (Arg Type)
t }

instance InstantiateFull a => InstantiateFull (Pattern' a) where
    instantiateFull' :: Pattern' a -> ReduceM (Pattern' a)
instantiateFull' (VarP PatternInfo
o a
x)     = forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' a
x
    instantiateFull' (DotP PatternInfo
o Term
t)     = forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
t
    instantiateFull' (ConP ConHead
n ConPatternInfo
mt [NamedArg (Pattern' a)]
ps) = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' ConPatternInfo
mt forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [NamedArg (Pattern' a)]
ps
    instantiateFull' (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps) = forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [NamedArg (Pattern' a)]
ps
    instantiateFull' l :: Pattern' a
l@LitP{}       = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
l
    instantiateFull' p :: Pattern' a
p@ProjP{}      = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
    instantiateFull' (IApplyP PatternInfo
o Term
t Term
u a
x) = forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' a
x

instance (Subst a, InstantiateFull a) => InstantiateFull (Abs a) where
    instantiateFull' :: Abs a -> ReduceM (Abs a)
instantiateFull' a :: Abs a
a@(Abs String
x a
_) = forall a. String -> a -> Abs a
Abs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
a forall t. InstantiateFull t => t -> ReduceM t
instantiateFull'
    instantiateFull' (NoAbs String
x a
a) = forall a. String -> a -> Abs a
NoAbs String
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' a
a

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

-- Andreas, 2021-09-13, issue #5544, need to traverse @checkpoints@ map
instance InstantiateFull t => InstantiateFull (Open t) where
  instantiateFull' :: Open t -> ReduceM (Open t)
instantiateFull' (OpenThing CheckpointId
checkpoint Map CheckpointId (Substitution' Term)
checkpoints ModuleNameHash
modl t
t) =
    forall a.
CheckpointId
-> Map CheckpointId (Substitution' Term)
-> ModuleNameHash
-> a
-> Open a
OpenThing CheckpointId
checkpoint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {m :: * -> *} {a}.
MonadTCEnv m =>
Map CheckpointId a -> m (Map CheckpointId a)
prune Map CheckpointId (Substitution' Term)
checkpoints)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleNameHash
modl
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' t
t
    where
      -- Ulf, 2021-11-17, #5544
      --  Remove checkpoints that are no longer in scope, since they can
      --  mention functions that deadcode elimination will get rid of.
      prune :: Map CheckpointId a -> m (Map CheckpointId a)
prune Map CheckpointId a
cps = do
        Map CheckpointId (Substitution' Term)
inscope <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map CheckpointId a
cps forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.intersection` Map CheckpointId (Substitution' Term)
inscope

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

instance InstantiateFull ProblemConstraint where
  instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint
instantiateFull' (PConstr Set ProblemId
p Blocker
u Closure Constraint
c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
p Blocker
u forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Closure Constraint
c

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

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

instance InstantiateFull Signature where
  instantiateFull' :: Signature -> ReduceM Signature
instantiateFull' (Sig Sections
a Definitions
b RewriteRuleMap
c) = forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 Sections -> Definitions -> RewriteRuleMap -> Signature
Sig forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Sections
a, Definitions
b, RewriteRuleMap
c)

instance InstantiateFull Section where
  instantiateFull' :: Section -> ReduceM Section
instantiateFull' (Section Telescope
tel) = Telescope -> Section
Section forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
tel

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

instance InstantiateFull Definition where
    instantiateFull' :: Definition -> ReduceM Definition
instantiateFull' def :: Definition
def@Defn{ defType :: Definition -> Type
defType = Type
t ,defDisplay :: Definition -> [LocalDisplayForm]
defDisplay = [LocalDisplayForm]
df, theDef :: Definition -> Defn
theDef = Defn
d } = do
      (Type
t, [LocalDisplayForm]
df, Defn
d) <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Type
t, [LocalDisplayForm]
df, Defn
d)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Definition
def{ defType :: Type
defType = Type
t, defDisplay :: [LocalDisplayForm]
defDisplay = [LocalDisplayForm]
df, theDef :: Defn
theDef = Defn
d }

instance InstantiateFull NLPat where
  instantiateFull' :: NLPat -> ReduceM NLPat
instantiateFull' (PVar Int
x [Arg Int]
y) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [Arg Int] -> NLPat
PVar Int
x [Arg Int]
y
  instantiateFull' (PDef QName
x PElims
y) = QName -> PElims -> NLPat
PDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' QName
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' PElims
y
  instantiateFull' (PLam ArgInfo
x Abs NLPat
y) = ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Abs NLPat
y
  instantiateFull' (PPi Dom NLPType
x Abs NLPType
y)  = Dom NLPType -> Abs NLPType -> NLPat
PPi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Dom NLPType
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Abs NLPType
y
  instantiateFull' (PSort NLPSort
x)  = NLPSort -> NLPat
PSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPSort
x
  instantiateFull' (PBoundVar Int
x PElims
y) = Int -> PElims -> NLPat
PBoundVar Int
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' PElims
y
  instantiateFull' (PTerm Term
x)  = Term -> NLPat
PTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
x

instance InstantiateFull NLPType where
  instantiateFull' :: NLPType -> ReduceM NLPType
instantiateFull' (NLPType NLPSort
s NLPat
a) = NLPSort -> NLPat -> NLPType
NLPType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPSort
s
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPat
a

instance InstantiateFull NLPSort where
  instantiateFull' :: NLPSort -> ReduceM NLPSort
instantiateFull' (PType NLPat
x) = NLPat -> NLPSort
PType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPat
x
  instantiateFull' (PProp NLPat
x) = NLPat -> NLPSort
PProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPat
x
  instantiateFull' (PSSet NLPat
x) = NLPat -> NLPSort
PSSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NLPat
x
  instantiateFull' (PInf IsFibrant
f Integer
n) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> NLPSort
PInf IsFibrant
f Integer
n
  instantiateFull' NLPSort
PSizeUniv = forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
  instantiateFull' NLPSort
PLockUniv = forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLockUniv
  instantiateFull' NLPSort
PIntervalUniv = forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PIntervalUniv

instance InstantiateFull RewriteRule where
  instantiateFull' :: RewriteRule -> ReduceM RewriteRule
instantiateFull' (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
t Bool
c) =
    QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
q
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
gamma
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
f
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' PElims
ps
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
rhs
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Type
t
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
c

instance InstantiateFull DisplayForm where
  instantiateFull' :: DisplayForm -> ReduceM DisplayForm
instantiateFull' (Display Int
n Elims
ps DisplayTerm
v) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Elims
ps, DisplayTerm
v)

instance InstantiateFull DisplayTerm where
  instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm
instantiateFull' (DTerm Term
v)       = Term -> DisplayTerm
DTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
v
  instantiateFull' (DDot  Term
v)       = Term -> DisplayTerm
DDot  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
v
  instantiateFull' (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)  = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [Arg DisplayTerm]
vs
  instantiateFull' (DDef QName
c [Elim' DisplayTerm]
es)     = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [Elim' DisplayTerm]
es
  instantiateFull' (DWithApp DisplayTerm
v [DisplayTerm]
vs Elims
ws) = forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (DisplayTerm
v, [DisplayTerm]
vs, Elims
ws)

instance InstantiateFull Defn where
    instantiateFull' :: Defn -> ReduceM Defn
instantiateFull' Defn
d = case Defn
d of
      Axiom{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Defn
d
      DataOrRecSig{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Defn
d
      GeneralizableVar{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Defn
d
      AbstractDefn Defn
d -> Defn -> Defn
AbstractDefn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Defn
d
      Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam } -> do
        ([Clause]
cs, Maybe CompiledClauses
cc, [Clause]
cov, FunctionInverse
inv) <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' ([Clause]
cs, Maybe CompiledClauses
cc, [Clause]
cov, FunctionInverse
inv)
        Maybe ExtLamInfo
extLam <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe ExtLamInfo
extLam
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Defn
d { funClauses :: [Clause]
funClauses = [Clause]
cs, funCompiled :: Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: [Clause]
funCovering = [Clause]
cov, funInv :: FunctionInverse
funInv = FunctionInverse
inv, funExtLam :: Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam }
      Datatype{ dataSort :: Defn -> Sort
dataSort = Sort
s, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } -> do
        Sort
s  <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Sort
s
        Maybe Clause
cl <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe Clause
cl
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Defn
d { dataSort :: Sort
dataSort = Sort
s, dataClause :: Maybe Clause
dataClause = Maybe Clause
cl }
      Record{ recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Telescope
recTel = Telescope
tel } -> do
        Maybe Clause
cl  <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe Clause
cl
        Telescope
tel <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
tel
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Defn
d { recClause :: Maybe Clause
recClause = Maybe Clause
cl, recTel :: Telescope
recTel = Telescope
tel }
      Constructor{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Defn
d
      Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } -> do
        [Clause]
cs <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [Clause]
cs
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Defn
d { primClauses :: [Clause]
primClauses = [Clause]
cs }
      PrimitiveSort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Defn
d

instance InstantiateFull ExtLamInfo where
  instantiateFull' :: ExtLamInfo -> ReduceM ExtLamInfo
instantiateFull' e :: ExtLamInfo
e@(ExtLamInfo { extLamSys :: ExtLamInfo -> Maybe System
extLamSys = Maybe System
sys}) = do
    Maybe System
sys <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe System
sys
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExtLamInfo
e { extLamSys :: Maybe System
extLamSys = Maybe System
sys}

instance InstantiateFull System where
  instantiateFull' :: System -> ReduceM System
instantiateFull' (System Telescope
tel [(Face, Term)]
sys) = Telescope -> [(Face, Term)] -> System
System forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [(Face, Term)]
sys

instance InstantiateFull FunctionInverse where
  instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse
instantiateFull' FunctionInverse
NotInjective = forall (m :: * -> *) a. Monad m => a -> m a
return forall c. FunctionInverse' c
NotInjective
  instantiateFull' (Inverse InversionMap Clause
inv) = forall c. InversionMap c -> FunctionInverse' c
Inverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' InversionMap Clause
inv

instance InstantiateFull a => InstantiateFull (Case a) where
  instantiateFull' :: Case a -> ReduceM (Case a)
instantiateFull' (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) =
    forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Map QName (WithArity a)
cs
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe (ConHead, WithArity a)
eta
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Map Literal a
ls
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe a
m
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Bool
b
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
lz

instance InstantiateFull CompiledClauses where
  instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses
instantiateFull' (Fail [Arg String]
xs)   = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Arg String] -> CompiledClauses' a
Fail [Arg String]
xs
  instantiateFull' (Done [Arg String]
m Term
t)  = forall a. [Arg String] -> a -> CompiledClauses' a
Done [Arg String]
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
t
  instantiateFull' (Case Arg Int
n Case CompiledClauses
bs) = forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Case CompiledClauses
bs

instance InstantiateFull Clause where
    instantiateFull' :: Clause -> ReduceM Clause
instantiateFull' (Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
b Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
       Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
tel
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' NAPs
ps
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe Term
b
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Maybe (Arg Type)
t
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
catchall
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
exact
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
recursive
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
unreachable
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return ExpandedEllipsis
ell
       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ModuleName
wm

instance InstantiateFull Instantiation where
  instantiateFull' :: Instantiation -> ReduceM Instantiation
instantiateFull' (Instantiation [Arg String]
a Term
b) =
    [Arg String] -> Term -> Instantiation
Instantiation [Arg String]
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
b

instance InstantiateFull (Judgement MetaId) where
  instantiateFull' :: Judgement MetaId -> ReduceM (Judgement MetaId)
instantiateFull' (HasType MetaId
a Comparison
b Type
c) =
    forall a. a -> Comparison -> Type -> Judgement a
HasType MetaId
a Comparison
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Type
c
  instantiateFull' (IsSort MetaId
a Type
b) =
    forall a. a -> Type -> Judgement a
IsSort MetaId
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Type
b

instance InstantiateFull RemoteMetaVariable where
  instantiateFull' :: RemoteMetaVariable -> ReduceM RemoteMetaVariable
instantiateFull' (RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c) = Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Instantiation
a
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Modality
b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Judgement MetaId
c

instance InstantiateFull Interface where
  instantiateFull' :: Interface -> ReduceM Interface
instantiateFull' Interface
i = do
    Definitions
defs <- forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Interface
i forall o i. o -> Lens' i o -> i
^. Lens' Signature Interface
intSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Definitions Signature
sigDefinitions)
    Interface -> ReduceM Interface
instantiateFullExceptForDefinitions'
      (forall i o. Lens' i o -> LensSet i o
set (Lens' Signature Interface
intSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Definitions Signature
sigDefinitions) Definitions
defs Interface
i)

-- | Instantiates everything except for definitions in the signature.

instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface
instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface
instantiateFullExceptForDefinitions'
  (Interface Hash
h Text
s FileType
ft [(TopLevelModuleName, Hash)]
ms ModuleName
mod TopLevelModuleName
tlmod Map ModuleName Scope
scope ScopeInfo
inside Signature
sig RemoteMetaStore
metas DisplayForms
display Map QName Text
userwarn
     Maybe Text
importwarn BuiltinThings (String, QName)
b Map String [ForeignCode]
foreignCode HighlightingInfo
highlighting [OptionsPragma]
libPragmas [OptionsPragma]
filePragmas
     PragmaOptions
usedOpts PatternSynDefns
patsyns [TCWarning]
warnings Set QName
partialdefs) =
  Hash
-> Text
-> FileType
-> [(TopLevelModuleName, Hash)]
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
Interface Hash
h Text
s FileType
ft [(TopLevelModuleName, Hash)]
ms ModuleName
mod TopLevelModuleName
tlmod Map ModuleName Scope
scope ScopeInfo
inside
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((\Sections
s RewriteRuleMap
r -> Sig { _sigSections :: Sections
_sigSections     = Sections
s
                      , _sigDefinitions :: Definitions
_sigDefinitions  = Signature
sig forall o i. o -> Lens' i o -> i
^. Lens' Definitions Signature
sigDefinitions
                      , _sigRewriteRules :: RewriteRuleMap
_sigRewriteRules = RewriteRuleMap
r
                      })
         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Signature
sig forall o i. o -> Lens' i o -> i
^. Lens' Sections Signature
sigSections)
         forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' (Signature
sig forall o i. o -> Lens' i o -> i
^. Lens' RewriteRuleMap Signature
sigRewriteRules))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' RemoteMetaStore
metas
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' DisplayForms
display
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Map QName Text
userwarn
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Text
importwarn
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' BuiltinThings (String, QName)
b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Map String [ForeignCode]
foreignCode
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingInfo
highlighting
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return [OptionsPragma]
libPragmas
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return [OptionsPragma]
filePragmas
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return PragmaOptions
usedOpts
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefns
patsyns
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return [TCWarning]
warnings
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
partialdefs

-- | Instantiates everything except for definitions in the signature.

instantiateFullExceptForDefinitions ::
  MonadReduce m => Interface -> m Interface
instantiateFullExceptForDefinitions :: forall (m :: * -> *). MonadReduce m => Interface -> m Interface
instantiateFullExceptForDefinitions =
  forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ReduceM Interface
instantiateFullExceptForDefinitions'

instance InstantiateFull a => InstantiateFull (Builtin a) where
    instantiateFull' :: Builtin a -> ReduceM (Builtin a)
instantiateFull' (Builtin Term
t) = forall pf. Term -> Builtin pf
Builtin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
t
    instantiateFull' (Prim a
x)   = forall pf. pf -> Builtin pf
Prim forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' a
x
    instantiateFull' b :: Builtin a
b@(BuiltinRewriteRelations Set QName
xs) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Builtin a
b

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

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