    {-# LANGUAGE NondecreasingIndentation #-}
    {-# LANGUAGE GADTs #-}

    {-# OPTIONS_GHC -fno-warn-orphans #-}

    -- | Rewriting with arbitrary rules.
    --
    --   The user specifies a relation symbol by the pragma
    --   @
    --       {-\# BUILTIN REWRITE rel \#-}
    --   @
    --   where @rel@ should be of type @Δ → (lhs rhs : A) → Set i@.
    --
    --   Then the user can add rewrite rules by the pragma
    --   @
    --       {-\# REWRITE q \#-}
    --   @
    --   where @q@ should be a closed term of type @Γ → rel us lhs rhs@.
    --
    --   We then intend to add a rewrite rule
    --   @
    --       Γ ⊢ lhs ↦ rhs : B
    --   @
    --   to the signature where @B = A[us/Δ]@.
    --
    --   To this end, we normalize @lhs@, which should be of the form
    --   @
    --       f ts
    --   @
    --   for a @'Def'@-symbol f (postulate, function, data, record, constructor).
    --   Further, @FV(ts) = dom(Γ)@.
    --   The rule @q :: Γ ⊢ f ts ↦ rhs : B@ is added to the signature
    --   to the definition of @f@.
    --
    --   When reducing a term @Ψ ⊢ f vs@ is stuck, we try the rewrites for @f@,
    --   by trying to unify @vs@ with @ts@.
    --   This is for now done by substituting fresh metas Xs for the bound
    --   variables in @ts@ and checking equality with @vs@
    --   @
    --       Ψ ⊢ (f ts)[Xs/Γ] = f vs : B[Xs/Γ]
    --   @
    --   If successful (no open metas/constraints), we replace @f vs@ by
    --   @rhs[Xs/Γ]@ and continue reducing.

    module Agda.TypeChecking.Rewriting where

    import Prelude hiding (null)

    import Control.Monad

    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List

    import Agda.Interaction.Options

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.MetaVars

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Conversion
    import qualified Agda.TypeChecking.Positivity.Occurrence as Pos
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive ( getBuiltinName )
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Rewriting.Confluence
    import Agda.TypeChecking.Rewriting.NonLinMatch
    import Agda.TypeChecking.Rewriting.NonLinPattern
    import Agda.TypeChecking.Warnings

    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Size
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

    requireOptionRewriting :: TCM ()
    requireOptionRewriting :: TCM ()
    requireOptionRewriting =
      TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    NeedOptionRewriting

    -- | Check that the name given to the BUILTIN REWRITE is actually
    --   a relation symbol.
    --   I.e., its type should be of the form @Δ → (lhs : A) (rhs : B) → Set ℓ@.
    --   Note: we do not care about hiding/non-hiding of lhs and rhs.
    verifyBuiltinRewrite :: Term -> Type -> TCM ()
    verifyBuiltinRewrite :: Term -> Type -> TCM ()
    verifyBuiltinRewrite Term
    v Type
    t = do
      TCM ()
    requireOptionRewriting
      let failure :: TCMT IO Doc -> TCM ()
    failure TCMT IO Doc
    reason = TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
           [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " does not have the right type for a rewriting relation"
           , TCMT IO Doc
    reason
           ]
      TCMT IO (Maybe RelView) -> TCM () -> (RelView -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Type -> TCMT IO (Maybe RelView)
    relView Type
    t)
        (TCMT IO Doc -> TCM ()
    failure (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "because it should accept at least two arguments") ((RelView -> TCM ()) -> TCM ()) -> (RelView -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        \ (RelView Tele (Dom Type)
    tel [Dom (ArgName, Type)]
    delta Dom Type
    a Dom Type
    b Type
    core) -> do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    a Bool -> Bool -> Bool
    && Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    b) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCM ()
    failure (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "because its two final arguments are not both visible."
        case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    core of
          Sort{}   -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Con{}    -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level{}  -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lam{}    -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Pi{}     -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> TCMT IO Doc -> TCM ()
    failure (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "because its type does not end in a sort, but in "
                 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    core

    -- | Deconstructing a type into @Δ → t → t' → core@.
    data RelView = RelView
      { RelView -> Tele (Dom Type)
    relViewTel   :: Telescope  -- ^ The whole telescope @Δ, t, t'@.
      , RelView -> [Dom (ArgName, Type)]
    relViewDelta :: ListTel    -- ^ @Δ@.
      , RelView -> Dom Type
    relViewType  :: Dom Type   -- ^ @t@.
      , RelView -> Dom Type
    relViewType' :: Dom Type   -- ^ @t'@.
      , RelView -> Type
    relViewCore  :: Type       -- ^ @core@.
      }

    -- | Deconstructing a type into @Δ → t → t' → core@.
    --   Returns @Nothing@ if not enough argument types.
    relView :: Type -> TCM (Maybe RelView)
    relView :: Type -> TCMT IO (Maybe RelView)
    relView Type
    t = do
      TelV Tele (Dom Type)
    tel Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
      let n :: Int
    n                = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
          ([Dom (ArgName, Type)]
    delta, [Dom (ArgName, Type)]
    lastTwo) = Int
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2) ([Dom (ArgName, Type)]
     -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel
      if [Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    lastTwo Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    2 then Maybe RelView -> TCMT IO (Maybe RelView)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe RelView
    forall a. Maybe a
    Nothing else do
        let [Dom Type
    a, Dom Type
    b] = ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd (Dom (ArgName, Type) -> Dom Type)
    -> [Dom (ArgName, Type)] -> [Dom Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Dom (ArgName, Type)]
    lastTwo
        Maybe RelView -> TCMT IO (Maybe RelView)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe RelView -> TCMT IO (Maybe RelView))
    -> Maybe RelView -> TCMT IO (Maybe RelView)
    forall a b. (a -> b) -> a -> b
    $ RelView -> Maybe RelView
    forall a. a -> Maybe a
    Just (RelView -> Maybe RelView) -> RelView -> Maybe RelView
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type)
    -> [Dom (ArgName, Type)] -> Dom Type -> Dom Type -> Type -> RelView
    RelView Tele (Dom Type)
    tel [Dom (ArgName, Type)]
    delta Dom Type
    a Dom Type
    b Type
    core

    -- | Check the given rewrite rules and add them to the signature.
    addRewriteRules :: [QName] -> TCM ()
    addRewriteRules :: [QName] -> TCM ()
    addRewriteRules [QName]
    qs = do

      -- Check the rewrite rules
      RewriteRules
    rews <- (QName -> TCMT IO RewriteRule) -> [QName] -> TCMT IO RewriteRules
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM QName -> TCMT IO RewriteRule
    checkRewriteRule [QName]
    qs

      -- Add rewrite rules to the signature
      RewriteRules -> (RewriteRule -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ RewriteRules
    rews ((RewriteRule -> TCM ()) -> TCM ())
    -> (RewriteRule -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \RewriteRule
    rew -> do
        let f :: QName
    f = RewriteRule -> QName
    rewHead RewriteRule
    rew
            matchables :: [QName]
    matchables = RewriteRule -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables RewriteRule
    rew
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "adding rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
          TCMT IO Doc
    "to the definition of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "matchable symbols: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [QName]
    matchables
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor QName
    f [RewriteRule
    rew] [QName]
    matchables

      -- Run confluence check for the new rules
      -- (should be done after adding all rules, see #3795)
      TCMT IO (Maybe ConfluenceCheck)
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ConfluenceCheck
    confChk -> do
        -- Global confluence checker requires rules to be sorted
        -- according to the generality of their lhs
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ConfluenceCheck
    confChk ConfluenceCheck -> ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck
    GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ((QName -> QName) -> [QName] -> [QName]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn QName -> QName
    forall a. a -> a
    id ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ (RewriteRule -> QName) -> RewriteRules -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteRule -> QName
    rewHead RewriteRules
    rews) QName -> TCM ()
    sortRulesOfSymbol
        ConfluenceCheck -> RewriteRules -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk RewriteRules
    rews
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "done checking confluence of rules" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((RewriteRule -> TCMT IO Doc) -> RewriteRules -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> TCMT IO Doc)
    -> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> QName
    rewName) RewriteRules
    rews)

    -- | Check the validity of @q : Γ → rel us lhs rhs@ as rewrite rule
    --   @
    --       Γ ⊢ lhs ↦ rhs : B
    --   @
    --   where @B = A[us/Δ]@.
    --   Remember that @rel : Δ → A → A → Set i@, so
    --   @rel us : (lhs rhs : A[us/Δ]) → Set i@.
    --   Returns the checked rewrite rule to be added to the signature.
    checkRewriteRule :: QName -> TCM RewriteRule
    checkRewriteRule :: QName -> TCMT IO RewriteRule
    checkRewriteRule QName
    q = do
      TCM ()
    requireOptionRewriting
      let failNoBuiltin :: TCMT IO a
    failNoBuiltin = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> ArgName -> TypeError
    forall a b. (a -> b) -> a -> b
    $
            ArgName
    "Cannot add rewrite rule without prior BUILTIN REWRITE"
      QName
    rel <- TCMT IO QName -> TCMT IO (Maybe QName) -> TCMT IO QName
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM TCMT IO QName
    forall {a}. TCMT IO a
    failNoBuiltin (TCMT IO (Maybe QName) -> TCMT IO QName)
    -> TCMT IO (Maybe QName) -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    ArgName -> m (Maybe QName)
    getBuiltinName ArgName
    builtinRewrite
      Definition
    def <- Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      -- Issue 1651: Check that we are not adding a rewrite rule
      -- for a type signature whose body has not been type-checked yet.
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Defn -> Bool
    isEmptyFunction (Defn -> Bool) -> Defn -> Bool
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
          [ TCMT IO Doc
    "Rewrite rule from function "
          , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q
          , TCMT IO Doc
    " cannot be added before the function definition"
          ]
      -- We know that the type of rel is that of a relation.
      Maybe RelView
    relV <- Type -> TCMT IO (Maybe RelView)
    relView (Type -> TCMT IO (Maybe RelView))
    -> TCMT IO Type -> TCMT IO (Maybe RelView)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    rel
      let RelView Tele (Dom Type)
    _tel [Dom (ArgName, Type)]
    delta Dom Type
    a Dom Type
    _a' Type
    _core = RelView -> Maybe RelView -> RelView
    forall a. a -> Maybe a -> a
    fromMaybe RelView
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe RelView
    relV
      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCMT IO Doc
    "rewrite relation at type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
          TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList [Dom (ArgName, Type)]
    delta) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " |- " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
            [Dom (ArgName, Type)] -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext [Dom (ArgName, Type)]
    delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a
      -- Get rewrite rule (type of q).
      TelV Tele (Dom Type)
    gamma1 Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "attempting to add rewrite rule of type "
        , Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    gamma1
        , TCMT IO Doc
    " |- " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    gamma1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    core
        ]
      let failureWrongTarget :: TCM a
          failureWrongTarget :: forall {a}. TCMT IO a
    failureWrongTarget = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " does not target rewrite relation" ]
      let failureMetas :: TCM a
          failureMetas :: forall {a}. TCMT IO a
    failureMetas       = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " is not a legal rewrite rule, since it contains unsolved meta variables" ]
      let failureNotDefOrCon :: TCM a
          failureNotDefOrCon :: forall {a}. TCMT IO a
    failureNotDefOrCon = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
      let failureFreeVars :: IntSet -> TCM a
          failureFreeVars :: forall a. IntSet -> TCM a
    failureFreeVars IntSet
    xs = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " is not a legal rewrite rule, since the following variables are not bound by the left hand side: " , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Int -> TCMT IO Doc) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> (Int -> Term) -> Int -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) ([Int] -> [TCMT IO Doc]) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ IntSet -> [Int]
    IntSet.toList IntSet
    xs) ]
      let failureIllegalRule :: TCM a -- TODO:: Defined but not used
          failureIllegalRule :: forall {a}. TCMT IO a
    failureIllegalRule = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " is not a legal rewrite rule" ]

      -- Check that type of q targets rel.
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    core of
        Def QName
    rel' es :: Elims
    es@(Elim' Term
    _:Elim' Term
    _:Elims
    _) | QName
    rel QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    rel' -> do
          -- Because of the type of rel (Γ → sort), all es are applications.
          let vs :: [Term]
    vs = (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          -- The last two arguments are lhs and rhs.
              n :: Int
    n  = [Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    vs
              ([Term]
    us, [Term
    lhs, Term
    rhs]) = Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2) [Term]
    vs
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    delta Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    us) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    lhs <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    lhs
          Term
    rhs <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    rhs
          Dom Type
    b   <- Dom Type -> TCMT IO (Dom Type)
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Dom Type -> TCMT IO (Dom Type)) -> Dom Type -> TCMT IO (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    us) Dom Type
    a

          Tele (Dom Type)
    gamma0 <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
          Tele (Dom Type)
    gamma1 <- Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Tele (Dom Type)
    gamma1
          let gamma :: Tele (Dom Type)
    gamma = Tele (Dom Type)
    gamma0 Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    `abstract` Tele (Dom Type)
    gamma1

          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom (ArgName, Type)] -> Bool
    forall a. AllMetas a => a -> Bool
    noMetas (Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    gamma1)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "metas in gamma1: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([MetaId] -> ArgName
    forall a. Show a => a -> ArgName
    show ([MetaId] -> ArgName) -> [MetaId] -> ArgName
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> [MetaId]
    forall a. AllMetas a => a -> [MetaId]
    allMetasList ([Dom (ArgName, Type)] -> [MetaId])
    -> [Dom (ArgName, Type)] -> [MetaId]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    gamma1)
            TCM ()
    forall {a}. TCMT IO a
    failureMetas

          -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
          -- This is necessary to replace copies created by imports by their
          -- original definition.
          Term
    lhs <- (AllowedReductions -> AllowedReductions)
    -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions (AllowedReductions -> AllowedReductions -> AllowedReductions
    forall a b. a -> b -> a
    const (AllowedReductions -> AllowedReductions -> AllowedReductions)
    -> AllowedReductions -> AllowedReductions -> AllowedReductions
    forall a b. (a -> b) -> a -> b
    $ AllowedReduction -> AllowedReductions
    forall a. SmallSetElement a => a -> SmallSet a
    SmallSet.singleton AllowedReduction
    InlineReductions) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    lhs

          -- Find head symbol f of the lhs, its type, its parameters (in case of a constructor), and its arguments.
          (QName
    f , Elims -> Term
    hd , Type
    t , [Int]
    pars , Elims
    es) <- case Term
    lhs of
            Def QName
    f Elims
    es -> do
              Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
              QName -> Definition -> TCM ()
    checkAxFunOrCon QName
    f Definition
    def
              (QName, Elims -> Term, Type, [Int], Elims)
    -> TCMT IO (QName, Elims -> Term, Type, [Int], Elims)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f , QName -> Elims -> Term
    Def QName
    f , Definition -> Type
    defType Definition
    def , [] , Elims
    es)
            Con ConHead
    c ConInfo
    ci Elims
    vs -> do
              let hd :: Elims -> Term
    hd = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci
              ~(Just ((QName
    _ , Type
    _ , [Arg Term]
    pars) , Type
    t)) <- ConHead
    -> Type -> TCMT IO (Maybe ((QName, Type, [Arg Term]), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
    getFullyAppliedConType ConHead
    c (Type -> TCMT IO (Maybe ((QName, Type, [Arg Term]), Type)))
    -> Type -> TCMT IO (Maybe ((QName, Type, [Arg Term]), Type))
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    b
              [Int]
    pars <- Tele (Dom Type) -> TCMT IO [Int] -> TCMT IO [Int]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    gamma1 (TCMT IO [Int] -> TCMT IO [Int]) -> TCMT IO [Int] -> TCMT IO [Int]
    forall a b. (a -> b) -> a -> b
    $ ConHead -> [Arg Term] -> TCMT IO [Int]
    checkParametersAreGeneral ConHead
    c [Arg Term]
    pars
              (QName, Elims -> Term, Type, [Int], Elims)
    -> TCMT IO (QName, Elims -> Term, Type, [Int], Elims)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead -> QName
    conName ConHead
    c , Elims -> Term
    hd , Type
    t , [Int]
    pars , Elims
    vs)
            Term
    _        -> TCMT IO (QName, Elims -> Term, Type, [Int], Elims)
    forall {a}. TCMT IO a
    failureNotDefOrCon

          QName -> TCMT IO RewriteRule -> TCMT IO RewriteRule
    ifNotAlreadyAdded QName
    f (TCMT IO RewriteRule -> TCMT IO RewriteRule)
    -> TCMT IO RewriteRule -> TCMT IO RewriteRule
    forall a b. (a -> b) -> a -> b
    $ do

          Tele (Dom Type) -> TCMT IO RewriteRule -> TCMT IO RewriteRule
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    gamma1 (TCMT IO RewriteRule -> TCMT IO RewriteRule)
    -> TCMT IO RewriteRule -> TCMT IO RewriteRule
    forall a b. (a -> b) -> a -> b
    $ do

            QName -> (Elims -> Term) -> Elims -> TCM ()
    checkNoLhsReduction QName
    f Elims -> Term
    hd Elims
    es

            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ((Elims, Term, Dom Type) -> Bool
    forall a. AllMetas a => a -> Bool
    noMetas (Elims
    es, Term
    rhs, Dom Type
    b)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "metas in lhs: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([MetaId] -> ArgName
    forall a. Show a => a -> ArgName
    show ([MetaId] -> ArgName) -> [MetaId] -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Elims -> [MetaId]
    forall a. AllMetas a => a -> [MetaId]
    allMetasList Elims
    es)
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "metas in rhs: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([MetaId] -> ArgName
    forall a. Show a => a -> ArgName
    show ([MetaId] -> ArgName) -> [MetaId] -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Term -> [MetaId]
    forall a. AllMetas a => a -> [MetaId]
    allMetasList Term
    rhs)
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "metas in b  : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([MetaId] -> ArgName
    forall a. Show a => a -> ArgName
    show ([MetaId] -> ArgName) -> [MetaId] -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> [MetaId]
    forall a. AllMetas a => a -> [MetaId]
    allMetasList Dom Type
    b)
              TCM ()
    forall {a}. TCMT IO a
    failureMetas

            PElims
    ps <- Relevance -> Int -> (Type, Term) -> Elims -> TCM PElims
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    Relevant Int
    0 (Type
    t , QName -> Elims -> Term
    Def QName
    f []) Elims
    es
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "Pattern generated from lhs: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NLPat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> PElims -> NLPat
    PDef QName
    f PElims
    ps)

            -- We need to check two properties on the variables used in the rewrite rule
            -- 1. For actually being able to apply the rewrite rule, we need
            --    that all variables that occur in the rule (on the left or the right)
            --    are bound in a pattern position on the left.
            -- 2. To preserve soundness, we need that all the variables that are used
            --    in the *proof* of the rewrite rule are bound in the lhs.
            --    For rewrite rules on constructors, we consider parameters to be bound
            --    even though they don't appear in the lhs, since they can be reconstructed.
            --    For postulated or abstract rewrite rules, we consider all arguments
            --    as 'used' (see #5238).
            let boundVars :: IntSet
    boundVars = PElims -> IntSet
    forall a. NLPatVars a => a -> IntSet
    nlPatVars PElims
    ps
                freeVars :: IntSet
    freeVars  = (PElims, Term) -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars (PElims
    ps,Term
    rhs)
                allVars :: IntSet
    allVars   = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    gamma
                usedVars :: IntSet
    usedVars  = case Definition -> Defn
    theDef Definition
    def of
                  Function{}     -> Definition -> IntSet
    usedArgs Definition
    def
                  Axiom{}        -> IntSet
    allVars
                  AbstractDefn{} -> IntSet
    allVars
                  Defn
    _              -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "variables bound by the pattern: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (IntSet -> ArgName
    forall a. Show a => a -> ArgName
    show IntSet
    boundVars)
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "variables free in the rewrite rule: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (IntSet -> ArgName
    forall a. Show a => a -> ArgName
    show IntSet
    freeVars)
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "variables used by the rewrite rule: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (IntSet -> ArgName
    forall a. Show a => a -> ArgName
    show IntSet
    usedVars)
            IntSet -> (IntSet -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull (IntSet
    freeVars IntSet -> IntSet -> IntSet
    IntSet.\\ IntSet
    boundVars) IntSet -> TCM ()
    forall a. IntSet -> TCM a
    failureFreeVars
            IntSet -> (IntSet -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull (IntSet
    usedVars IntSet -> IntSet -> IntSet
    IntSet.\\ (IntSet
    boundVars IntSet -> IntSet -> IntSet
    `IntSet.union` [Int] -> IntSet
    IntSet.fromList [Int]
    pars)) IntSet -> TCM ()
    forall a. IntSet -> TCM a
    failureFreeVars

            let rew :: RewriteRule
    rew = QName
    -> Tele (Dom Type)
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> RewriteRule
    RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    f PElims
    ps Term
    rhs (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    b) Bool
    False

            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "checked rewrite rule" , RewriteRule -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM RewriteRule
    rew ]
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "checked rewrite rule" , ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (RewriteRule -> ArgName
    forall a. Show a => a -> ArgName
    show RewriteRule
    rew) ]

            RewriteRule -> TCMT IO RewriteRule
    forall (m :: * -> *) a. Monad m => a -> m a
    return RewriteRule
    rew

        Term
    _ -> TCMT IO RewriteRule
    forall {a}. TCMT IO a
    failureWrongTarget

      where
        checkNoLhsReduction :: QName -> (Elims -> Term)  -> Elims -> TCM ()
        checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> TCM ()
    checkNoLhsReduction QName
    f Elims -> Term
    hd Elims
    es = do
          -- Skip this check when global confluence check is enabled, as
          -- redundant rewrite rules may be required to prove confluence.
          TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ((Maybe ConfluenceCheck -> Maybe ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck -> Maybe ConfluenceCheck
    forall a. a -> Maybe a
    Just ConfluenceCheck
    GlobalConfluenceCheck) (Maybe ConfluenceCheck -> Bool)
    -> (PragmaOptions -> Maybe ConfluenceCheck)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          let v :: Term
    v = Elims -> Term
    hd Elims
    es
          Term
    v' <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          let fail :: TCM a
              fail :: forall {a}. TCMT IO a
    fail = do
                ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Term -> ArgName
    forall a. Show a => a -> ArgName
    show Term
    v)
                ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Term -> ArgName
    forall a. Show a => a -> ArgName
    show Term
    v')
                TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
                  [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " is not a legal rewrite rule, since the left-hand side "
                  , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " reduces to " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v' ]
          Elims
    es' <- case Term
    v' of
            Def QName
    f' Elims
    es'   | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'         -> Elims -> TCMT IO Elims
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elims
    es'
            Con ConHead
    c' ConInfo
    _ Elims
    es' | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c' -> Elims -> TCMT IO Elims
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elims
    es'
            Term
    _                              -> TCMT IO Elims
    forall {a}. TCMT IO a
    fail
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Elims -> Bool
    forall a. Null a => a -> Bool
    null Elims
    es Bool -> Bool -> Bool
    && Elims -> Bool
    forall a. Null a => a -> Bool
    null Elims
    es') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Type
    a   <- QName -> Elims -> Elims -> TCMT IO Type
    forall (m :: * -> *).
    MonadConversion m =>
    QName -> Elims -> Elims -> m Type
    computeElimHeadType QName
    f Elims
    es Elims
    es'
            [Polarity]
    pol <- Comparison -> QName -> TCMT IO [Polarity]
    forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    CmpEq QName
    f
            Bool
    ok  <- TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m () -> m Bool
    tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $
                     [Polarity]
    -> [IsForced] -> Type -> Term -> Elims -> Elims -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    compareElims [Polarity]
    pol [] Type
    a (QName -> Elims -> Term
    Def QName
    f []) Elims
    es Elims
    es'
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    ok TCM ()
    forall {a}. TCMT IO a
    fail

        checkAxFunOrCon :: QName -> Definition -> TCM ()
        checkAxFunOrCon :: QName -> Definition -> TCM ()
    checkAxFunOrCon QName
    f Definition
    def = case Definition -> Defn
    theDef Definition
    def of
          Axiom{}        -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Function{}     -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Constructor{}  -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          AbstractDefn{} -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Primitive{}    -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- TODO: is this fine?
          Defn
    _              -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q , TCMT IO Doc
    " is not a legal rewrite rule, since the head symbol"
            , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f , TCMT IO Doc
    "is not a postulate, a function, or a constructor"
            ]

        ifNotAlreadyAdded :: QName -> TCM RewriteRule -> TCM RewriteRule
        ifNotAlreadyAdded :: QName -> TCMT IO RewriteRule -> TCMT IO RewriteRule
    ifNotAlreadyAdded QName
    f TCMT IO RewriteRule
    cont = do
          RewriteRules
    rews <- QName -> TCMT IO RewriteRules
    forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
    getRewriteRulesFor QName
    f
          -- check if q is already an added rewrite rule
          case (RewriteRule -> Bool) -> RewriteRules -> Maybe RewriteRule
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (QName -> Bool) -> (RewriteRule -> QName) -> RewriteRule -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> QName
    rewName) RewriteRules
    rews of
            Just RewriteRule
    rew -> do
              Doc -> TCM ()
    forall (m :: * -> *). MonadWarning m => Doc -> m ()
    genericWarning (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
                TCMT IO Doc
    "Rewrite rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " has already been added"
              RewriteRule -> TCMT IO RewriteRule
    forall (m :: * -> *) a. Monad m => a -> m a
    return RewriteRule
    rew
            Maybe RewriteRule
    Nothing -> TCMT IO RewriteRule
    cont

        usedArgs :: Definition -> IntSet
        usedArgs :: Definition -> IntSet
    usedArgs Definition
    def = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ ((Occurrence, Int) -> Int) -> [(Occurrence, Int)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Occurrence, Int) -> Int
    forall a b. (a, b) -> b
    snd ([(Occurrence, Int)] -> [Int]) -> [(Occurrence, Int)] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [(Occurrence, Int)]
    usedIxs
          where
            occs :: [Occurrence]
    occs = Definition -> [Occurrence]
    defArgOccurrences Definition
    def
            allIxs :: [(Occurrence, Int)]
    allIxs = [Occurrence] -> [Int] -> [(Occurrence, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Occurrence]
    occs ([Int] -> [(Occurrence, Int)]) -> [Int] -> [(Occurrence, Int)]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Occurrence] -> Int
    forall a. Sized a => a -> Int
    size [Occurrence]
    occs
            usedIxs :: [(Occurrence, Int)]
    usedIxs = ((Occurrence, Int) -> Bool)
    -> [(Occurrence, Int)] -> [(Occurrence, Int)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Occurrence -> Bool
    used (Occurrence -> Bool)
    -> ((Occurrence, Int) -> Occurrence) -> (Occurrence, Int) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Occurrence, Int) -> Occurrence
    forall a b. (a, b) -> a
    fst) [(Occurrence, Int)]
    allIxs
            used :: Occurrence -> Bool
    used Occurrence
    Pos.Unused = Bool
    False
            used Occurrence
    _          = Bool
    True

        checkParametersAreGeneral :: ConHead -> Args -> TCM [Int]
        checkParametersAreGeneral :: ConHead -> [Arg Term] -> TCMT IO [Int]
    checkParametersAreGeneral ConHead
    c [Arg Term]
    vs = do
            [Int]
    is <- [Arg Term] -> TCMT IO [Int]
    loop [Arg Term]
    vs
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Int] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Int]
    is) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    forall {a}. TCMT IO a
    errorNotGeneral
            [Int] -> TCMT IO [Int]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Int]
    is
          where
            loop :: [Arg Term] -> TCMT IO [Int]
    loop []       = [Int] -> TCMT IO [Int]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            loop (Arg Term
    v : [Arg Term]
    vs) = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v of
              Var Int
    i [] -> (Int
    i Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :) ([Int] -> [Int]) -> TCMT IO [Int] -> TCMT IO [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> TCMT IO [Int]
    loop [Arg Term]
    vs
              Term
    _        -> TCMT IO [Int]
    forall {a}. TCMT IO a
    errorNotGeneral

            errorNotGeneral :: TCM a
            errorNotGeneral :: forall {a}. TCMT IO a
    errorNotGeneral = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    " is not a legal rewrite rule, since the constructor parameters are not fully general:"
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "Constructor: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ConHead
    c
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "Parameters: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    vs)
                ]

    -- | @rewriteWith t f es rew@ where @f : t@
    --   tries to rewrite @f es@ with @rew@, returning the reduct if successful.
    rewriteWith :: Type
                -> (Elims -> Term)
                -> RewriteRule
                -> Elims
                -> ReduceM (Either (Blocked Term) Term)
    rewriteWith :: Type
    -> (Elims -> Term)
    -> RewriteRule
    -> Elims
    -> ReduceM (Either (Blocked Term) Term)
    rewriteWith Type
    t Elims -> Term
    hd rew :: RewriteRule
    rew@(RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    _ PElims
    ps Term
    rhs Type
    b Bool
    isClause) Elims
    es
     | Bool
    isClause = Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Either (Blocked Term) Term
    forall a b. a -> Either a b
    Left (Blocked Term -> Either (Blocked Term) Term)
    -> Blocked Term -> Either (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> Term -> Blocked Term
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked (Term -> Blocked Term) -> Term -> Blocked Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hd Elims
    es
     | Bool
    otherwise = do
      ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "{ attempting to rewrite term " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es)
        , TCMT IO Doc
    " having head " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        , TCMT IO Doc
    " with rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> RewriteRule -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM RewriteRule
    rew
        ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
      ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    90 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "raw: attempting to rewrite term " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Term -> ArgName) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ArgName
    forall a. Show a => a -> ArgName
    show) (Elims -> Term
    hd Elims
    es)
        , TCMT IO Doc
    " having head " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Term -> ArgName) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ArgName
    forall a. Show a => a -> ArgName
    show) (Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Type -> ArgName) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ArgName
    forall a. Show a => a -> ArgName
    show) Type
    t
        , TCMT IO Doc
    " with rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (RewriteRule -> ArgName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> ArgName
    forall a. Show a => a -> ArgName
    show) RewriteRule
    rew
        ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
      Either Blocked_ (Substitution' Term)
    result <- Tele (Dom Type)
    -> (Type, Elims -> Term)
    -> PElims
    -> Elims
    -> ReduceM (Either Blocked_ (Substitution' Term))
    forall (m :: * -> *) t a b.
    (PureTCM m, Match t a b) =>
    Tele (Dom Type)
    -> t -> a -> b -> m (Either Blocked_ (Substitution' Term))
    nonLinMatch Tele (Dom Type)
    gamma (Type
    t,Elims -> Term
    hd) PElims
    ps Elims
    es
      case Either Blocked_ (Substitution' Term)
    result of
        Left Blocked_
    block -> ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 TCMT IO Doc
    "}" (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $
          Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Either (Blocked Term) Term
    forall a b. a -> Either a b
    Left (Blocked Term -> Either (Blocked Term) Term)
    -> Blocked Term -> Either (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Blocked_
    block Blocked_ -> Term -> Blocked Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd Elims
    es -- TODO: remember reductions
        Right Substitution' Term
    sub  -> do
          let v' :: Term
    v' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Term)
    sub Term
    rhs
          ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "rewrote " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es)
            , TCMT IO Doc
    " to " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "}"
            ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
          Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Either (Blocked Term) Term
    forall a b. b -> Either a b
    Right Term
    v'

    -- | @rewrite b v rules es@ tries to rewrite @v@ applied to @es@ with the
    --   rewrite rules @rules@. @b@ is the default blocking tag.
    rewrite :: Blocked_ -> (Elims -> Term) -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
    rewrite :: Blocked_
    -> (Elims -> Term)
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    rewrite Blocked_
    block Elims -> Term
    hd RewriteRules
    rules Elims
    es = do
      Bool
    rewritingAllowed <- PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      if (Bool
    rewritingAllowed Bool -> Bool -> Bool
    && Bool -> Bool
    not (RewriteRules -> Bool
    forall a. Null a => a -> Bool
    null RewriteRules
    rules)) then do
        (QName
    _ , Type
    t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
    -> ReduceM (Maybe (QName, Type)) -> ReduceM (QName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> ReduceM (Maybe (QName, Type))
    forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead (Elims -> Term
    hd [])
        Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop Blocked_
    block Type
    t RewriteRules
    rules (Elims -> ReduceM (Reduced (Blocked Term) Term))
    -> ReduceM Elims -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Elims -> ReduceM Elims
    forall t. InstantiateFull t => t -> ReduceM t
    instantiateFull' Elims
    es -- TODO: remove instantiateFull?
      else
        Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Term) Term
     -> ReduceM (Reduced (Blocked Term) Term))
    -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Reduced (Blocked Term) Term
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked_
    block Blocked_ -> Term -> Blocked Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd Elims
    es)
      where
        loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
        loop :: Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop Blocked_
    block Type
    t [] Elims
    es =
          ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Reduced (Blocked Term) Term)
    -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    20 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "failed to rewrite " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es)
            , TCMT IO Doc
    "blocking tag" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Blocked_ -> ArgName
    forall a. Show a => a -> ArgName
    show Blocked_
    block)
            ]) (ReduceM (Reduced (Blocked Term) Term)
     -> ReduceM (Reduced (Blocked Term) Term))
    -> ReduceM (Reduced (Blocked Term) Term)
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
          Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Term) Term
     -> ReduceM (Reduced (Blocked Term) Term))
    -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Reduced (Blocked Term) Term
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked Term -> Reduced (Blocked Term) Term)
    -> Blocked Term -> Reduced (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Blocked_
    block Blocked_ -> Term -> Blocked Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd Elims
    es
        loop Blocked_
    block Type
    t (RewriteRule
    rew:RewriteRules
    rews) Elims
    es
         | let n :: Int
    n = RewriteRule -> Int
    rewArity RewriteRule
    rew, Elims -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Elims
    es Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n = do
              let (Elims
    es1, Elims
    es2) = Int -> Elims -> (Elims, Elims)
    forall i a. Integral i => i -> [a] -> ([a], [a])
    List.genericSplitAt Int
    n Elims
    es
              Either (Blocked Term) Term
    result <- Type
    -> (Elims -> Term)
    -> RewriteRule
    -> Elims
    -> ReduceM (Either (Blocked Term) Term)
    rewriteWith Type
    t Elims -> Term
    hd RewriteRule
    rew Elims
    es1
              case Either (Blocked Term) Term
    result of
                Left (Blocked Blocker
    m Term
    u)    -> Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop (Blocked_
    block Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    m ()) Type
    t RewriteRules
    rews Elims
    es
                Left (NotBlocked NotBlocked' Term
    _ Term
    _) -> Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop Blocked_
    block Type
    t RewriteRules
    rews Elims
    es
                Right Term
    w               -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Term) Term
     -> ReduceM (Reduced (Blocked Term) Term))
    -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> Term -> Reduced (Blocked Term) Term
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    YesSimplification (Term -> Reduced (Blocked Term) Term)
    -> Term -> Reduced (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Term
    w Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es2
         | Bool
    otherwise = Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop (Blocked_
    block Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied ()) Type
    t RewriteRules
    rews Elims
    es

        rewArity :: RewriteRule -> Int
        rewArity :: RewriteRule -> Int
    rewArity = PElims -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (PElims -> Int) -> (RewriteRule -> PElims) -> RewriteRule -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> PElims
    rewPats