{-# LANGUAGE NondecreasingIndentation #-}

{-# 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.Trans.Maybe ( MaybeT(..), runMaybeT )

import Data.Either (partitionEithers)
import Data.Foldable (toList)
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set

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.Syntax.Internal.Pattern

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.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 qualified Agda.Utils.Set1 as Set1
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.VarSet (VarSet)

import Agda.Utils.Impossible
import Agda.Utils.Either
import Agda.Utils.List1 (nonEmpty)

-- | Require '--rewriting' for global REWRITE rules
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'' Term Term -> TCM ()
verifyBuiltinRewrite Term
v Type'' Term Term
t = do
  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'' Term Term -> TCMT IO (Maybe RelView)
relView Type'' Term Term
t)
    (TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
IncorrectTypeForRewriteRelation Term
v IncorrectTypeForRewriteRelationReason
ShouldAcceptAtLeastTwoArguments) ((RelView -> TCM ()) -> TCM ()) -> (RelView -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$
    \ (RelView Tele (Dom' Term (Type'' Term Term))
tel [Dom (ArgName, Type'' Term Term)]
delta Dom' Term (Type'' Term Term)
a Dom' Term (Type'' Term Term)
b Type'' Term Term
core) -> do
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term (Type'' Term Term)
a Bool -> Bool -> Bool
&& Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term (Type'' Term Term)
b) (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 ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
IncorrectTypeForRewriteRelation Term
v IncorrectTypeForRewriteRelationReason
FinalTwoArgumentsNotVisible
    case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
core of
      Sort{}   -> () -> TCM ()
forall a. a -> TCMT IO a
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
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
IncorrectTypeForRewriteRelation Term
v (Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> IncorrectTypeForRewriteRelationReason
TypeDoesNotEndInSort Type'' Term Term
core Tele (Dom' Term (Type'' Term Term))
tel)

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

-- | Deconstructing a type into @Δ → t → t' → core@.
--   Returns @Nothing@ if not enough argument types.
relView :: Type -> TCM (Maybe RelView)
relView :: Type'' Term Term -> TCMT IO (Maybe RelView)
relView Type'' Term Term
t = do
  TelV tel core <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telView Type'' Term Term
t
  let n                = Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel
      (delta, lastTwo) = splitAt (n - 2) $ telToList tel
  if size lastTwo < 2 then return Nothing else do
    let [a, b] = fmap snd <$> lastTwo
    return $ Just $ RelView tel delta a b 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
  rews <- (QName -> TCMT IO (Maybe GlobalRewriteRule))
-> [QName] -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM QName -> TCMT IO (Maybe GlobalRewriteRule)
checkRewriteRule [QName]
qs

  -- Add rewrite rules to the signature
  forM_ rews $ \GlobalRewriteRule
rew -> do
    let f :: QName
f = GlobalRewriteRule -> QName
grHead GlobalRewriteRule
rew
        matchables :: [QName]
matchables = GlobalRewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables GlobalRewriteRule
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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
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
forall (m :: * -> *). MonadPretty m => QName -> 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
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM [QName]
matchables
    QName -> [GlobalRewriteRule] -> [QName] -> TCM ()
addRewriteRulesFor QName
f [GlobalRewriteRule
rew] [QName]
matchables

  -- Run confluence check for the new rules
  -- (should be done after adding all rules, see #3795)
  whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
confChk -> do
    -- Warn if --cubical is enabled
    TCMT IO (Maybe Cubical) -> (Cubical -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption ((Cubical -> TCM ()) -> TCM ()) -> (Cubical -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Cubical
_ -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
ConfluenceForCubicalNotSupported
    -- Global confluence checker requires rules to be sorted
    -- according to the generality of their lhs
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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
$ (GlobalRewriteRule -> QName) -> [GlobalRewriteRule] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map GlobalRewriteRule -> QName
grHead [GlobalRewriteRule]
rews) QName -> TCM ()
sortRulesOfSymbol
    ConfluenceCheck -> [GlobalRewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [GlobalRewriteRule]
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_ ((GlobalRewriteRule -> TCMT IO Doc)
-> [GlobalRewriteRule] -> [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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> TCMT IO Doc)
-> (GlobalRewriteRule -> QName) -> GlobalRewriteRule -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRewriteRule -> QName
grName) [GlobalRewriteRule]
rews)

-- Auxiliary function for checkRewriteRule.
-- | Get domain of rewrite relation.
rewriteRelationDom :: QName -> TCM (ListTel, Dom Type)
rewriteRelationDom :: QName
-> TCM
     ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
rewriteRelationDom QName
rel = do
  -- We know that the type of rel is that of a relation.
  relV <- Type'' Term Term -> TCMT IO (Maybe RelView)
relView (Type'' Term Term -> TCMT IO (Maybe RelView))
-> TCMT IO (Type'' Term Term) -> TCMT IO (Maybe RelView)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCMT IO (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
rel
  let RelView _tel delta a _a' _core = fromMaybe __IMPOSSIBLE__ relV
  reportSDoc "rewriting" 30 $ do
    "rewrite relation at type " <+> do
      inTopContext $ prettyTCM (telFromList delta) <+> " |- " <+> do
        addContext delta $ prettyTCM a
  return (delta, a)

checkEquationValid ::
  RewriteSource -> RewriteAnn -> Type -> TCM (Maybe LocalEquation)
checkEquationValid :: RewriteSource
-> RewriteAnn
-> Type'' Term Term
-> TCM (Maybe (LocalEquation' Term))
checkEquationValid RewriteSource
s RewriteAnn
rewAnn Type'' Term Term
t
  | RewriteAnn -> Bool
forall a. LensRewriteAnn a => a -> Bool
isRewrite RewriteAnn
rewAnn = MaybeT (TCMT IO) (LocalEquation' Term)
-> TCM (Maybe (LocalEquation' Term))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) (LocalEquation' Term)
 -> TCM (Maybe (LocalEquation' Term)))
-> MaybeT (TCMT IO) (LocalEquation' Term)
-> TCM (Maybe (LocalEquation' Term))
forall a b. (a -> b) -> a -> b
$ RewriteSource
-> Type'' Term Term -> MaybeT (TCMT IO) (LocalEquation' Term)
checkIsRewriteRelation RewriteSource
s Type'' Term Term
t
  | Bool
otherwise        = Maybe (LocalEquation' Term) -> TCM (Maybe (LocalEquation' Term))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (LocalEquation' Term)
forall a. Maybe a
Nothing

checkIsRewriteRelation ::
  RewriteSource -> Type -> MaybeT TCM LocalEquation
checkIsRewriteRelation :: RewriteSource
-> Type'' Term Term -> MaybeT (TCMT IO) (LocalEquation' Term)
checkIsRewriteRelation RewriteSource
q Type'' Term Term
t = do
  rels <- TCM (Set QName) -> MaybeT (TCMT IO) (Set QName)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (Set QName)
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Set QName)
getBuiltinRewriteRelations
  reportSDoc "rewriting.relations" 40 $ vcat
    [ "Rewrite relations:"
    , prettyList $ map prettyTCM $ toList rels
    ]
  TelV gamma1 core <- telView $ t
  reportSDoc "rewriting" 30 $ vcat
    [ "attempting to add rewrite rule of type "
    , prettyTCM gamma1
    , " |- " <+> do addContext gamma1 $ prettyTCM core
    ]
  case unEl core of
    Def QName
rel es :: [Elim]
es@(Elim
_:Elim
_:[Elim]
_) | QName
rel QName -> Set QName -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
rels -> do
        (delta, a) <- TCM
  ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
-> MaybeT
     (TCMT IO)
     ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM
   ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
 -> MaybeT
      (TCMT IO)
      ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term)))
-> TCM
     ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
-> MaybeT
     (TCMT IO)
     ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ QName
-> TCM
     ([Dom (ArgName, Type'' Term Term)], Dom' Term (Type'' Term Term))
rewriteRelationDom QName
rel
        -- Because of the type of rel (Γ → sort), all es are applications.
        let 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
$ [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es
        -- The last two arguments are lhs and rhs.
            n  = [Term] -> Int
forall a. Sized a => a -> Int
size [Term]
vs
            (us, [lhs, rhs]) = splitAt (n - 2) vs
        unless (size delta == size us) __IMPOSSIBLE__
        lhs <- instantiateFull lhs
        rhs <- instantiateFull rhs
        b   <- instantiateFull $ applySubst (parallelS $ reverse us) a
        gamma1 <- instantiateFull gamma1
        pure $ LocalEquation gamma1  lhs rhs (unDom b)
    Term
_ -> RewriteSource
-> IllegalRewriteRuleReason
-> MaybeT (TCMT IO) (LocalEquation' Term)
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
q IllegalRewriteRuleReason
DoesNotTargetRewriteRelation

-- | 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 (Maybe GlobalRewriteRule)
checkRewriteRule :: QName -> TCMT IO (Maybe GlobalRewriteRule)
checkRewriteRule QName
q = MaybeT (TCMT IO) GlobalRewriteRule
-> TCMT IO (Maybe GlobalRewriteRule)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) GlobalRewriteRule
 -> TCMT IO (Maybe GlobalRewriteRule))
-> MaybeT (TCMT IO) GlobalRewriteRule
-> TCMT IO (Maybe GlobalRewriteRule)
forall a b. (a -> b) -> a -> b
$ QName
-> MaybeT (TCMT IO) GlobalRewriteRule
-> MaybeT (TCMT IO) GlobalRewriteRule
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
q do
  TCM () -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM ()
requireOptionRewriting
  rels <- TCM (Set QName) -> MaybeT (TCMT IO) (Set QName)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (Set QName)
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Set QName)
getBuiltinRewriteRelations
  reportSDoc "rewriting.relations" 40 $ vcat
    [ "Rewrite relations:"
    , prettyList $ map prettyTCM $ toList rels
    ]
  def <- instantiateDef =<< getConstInfo q

  -- Issue 1651: Check that we are not adding a rewrite rule
  -- for a type signature whose body has not been type-checked yet.
  when (isEmptyFunction $ theDef def) $
    illegalRule (GlobalRewrite def) BeforeFunctionDefinition
  -- Issue 6643: Also check that there are no mutual definitions
  -- that are not yet defined.
  whenJustM (viewTC eMutualBlock) \ MutualId
mb -> do
    qs <- MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> MaybeT (TCMT IO) MutualBlock -> MaybeT (TCMT IO) (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> MaybeT (TCMT IO) MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
mb
    when (Set.member q qs) $ forM_ qs $ \QName
r -> do
      MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Defn -> Bool
isEmptyFunction (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool)
-> MaybeT (TCMT IO) Definition -> MaybeT (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> MaybeT (TCMT IO) Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
r) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
-> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule (Definition -> RewriteSource
GlobalRewrite Definition
def) (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason
BeforeMutualFunctionDefinition QName
r

  eq <- checkIsRewriteRelation (GlobalRewrite def) (defType def)
  RewriteRule g h ps rhs b <- checkRewriteRule' eq (GlobalRewrite def)
  f <- case h of
    RewDefHead QName
f -> QName -> MaybeT (TCMT IO) QName
forall a. a -> MaybeT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
f
    RewVarHead Int
x -> RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) QName
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule (Definition -> RewriteSource
GlobalRewrite Definition
def) IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor

  top <- fromMaybe __IMPOSSIBLE__ <$> currentTopLevelModule

  pure $ GlobalRewriteRule q g f ps  rhs b False top

checkLocalRewriteRule ::
  RewriteSource -> LocalEquation -> TCM (Maybe RewriteRule)
checkLocalRewriteRule :: RewriteSource -> LocalEquation' Term -> TCM (Maybe RewriteRule)
checkLocalRewriteRule RewriteSource
s LocalEquation' Term
eq = MaybeT (TCMT IO) RewriteRule -> TCM (Maybe RewriteRule)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) RewriteRule -> TCM (Maybe RewriteRule))
-> MaybeT (TCMT IO) RewriteRule -> TCM (Maybe RewriteRule)
forall a b. (a -> b) -> a -> b
$
  -- For now, we fail if the local rewrite rule contains metas ANYWHERE
  -- I think it should be possible to do better than this, but it is hard
  Set MetaId
-> MaybeT (TCMT IO) RewriteRule
-> (Set1 MetaId -> MaybeT (TCMT IO) RewriteRule)
-> MaybeT (TCMT IO) RewriteRule
forall a b. Set a -> b -> (Set1 a -> b) -> b
Set1.ifNull ((MetaId -> Set MetaId) -> LocalEquation' Term -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> LocalEquation' Term -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton LocalEquation' Term
eq)
  {- then -} (LocalEquation' Term
-> RewriteSource -> MaybeT (TCMT IO) RewriteRule
checkRewriteRule' LocalEquation' Term
eq RewriteSource
s)
  {- else -} (RewriteSource
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule)
-> (Set1 MetaId -> IllegalRewriteRuleReason)
-> Set1 MetaId
-> MaybeT (TCMT IO) RewriteRule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set1 MetaId -> IllegalRewriteRuleReason
ContainsUnsolvedMetaVariables)

checkRewriteRule' :: LocalEquation -> RewriteSource -> MaybeT TCM RewriteRule
checkRewriteRule' :: LocalEquation' Term
-> RewriteSource -> MaybeT (TCMT IO) RewriteRule
checkRewriteRule' eq :: LocalEquation' Term
eq@(LocalEquation Tele (Dom' Term (Type'' Term Term))
gamma1 Term
lhs Term
rhs Type'' Term Term
b) RewriteSource
s = do
  ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Checking rewrite rule: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LocalEquation' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => LocalEquation' Term -> m Doc
prettyTCM LocalEquation' Term
eq

  let failureBlocked :: Blocker -> MaybeT TCM a
      failureBlocked :: forall a. Blocker -> MaybeT (TCMT IO) a
failureBlocked Blocker
b
        | Set1.IsNonEmpty Set1 MetaId
ms <- Blocker -> Set MetaId
allBlockingMetas    Blocker
b = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Set1 MetaId -> IllegalRewriteRuleReason
ContainsUnsolvedMetaVariables Set1 MetaId
ms
        | Set1.IsNonEmpty NESet ProblemId
ps <- Blocker -> Set ProblemId
allBlockingProblems Blocker
b = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ NESet ProblemId -> IllegalRewriteRuleReason
BlockedOnProblems NESet ProblemId
ps
        | Set1.IsNonEmpty NESet QName
qs <- Blocker -> Set QName
allBlockingDefs     Blocker
b = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ NESet QName -> IllegalRewriteRuleReason
RequiresDefinitions NESet QName
qs
        | Bool
otherwise = MaybeT (TCMT IO) a
forall a. HasCallStack => a
__IMPOSSIBLE__
  let failureFreeVars :: VarSet -> MaybeT TCM a
      failureFreeVars :: forall a. VarSet -> MaybeT (TCMT IO) a
failureFreeVars VarSet
xs = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ VarSet -> IllegalRewriteRuleReason
VariablesNotBoundByLHS VarSet
xs
  let warnUnsafeVars :: VarSet -> MaybeT TCM ()
      warnUnsafeVars :: VarSet -> MaybeT (TCMT IO) ()
warnUnsafeVars VarSet
xs = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m ()
unsafeRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ VarSet -> IllegalRewriteRuleReason
VariablesBoundInSingleton VarSet
xs
  let failureNonLinearPars :: VarSet -> MaybeT TCM a
      failureNonLinearPars :: forall a. VarSet -> MaybeT (TCMT IO) a
failureNonLinearPars VarSet
xs = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ VarSet -> IllegalRewriteRuleReason
VariablesBoundMoreThanOnce VarSet
xs

  gamma0 <- MaybeT (TCMT IO) (Tele (Dom' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
getContextTelescope
  let gamma = Tele (Dom' Term (Type'' Term Term))
gamma0 Tele (Dom' Term (Type'' Term Term))
-> Tele (Dom' Term (Type'' Term Term))
-> Tele (Dom' Term (Type'' Term Term))
forall t.
Abstract t =>
Tele (Dom' Term (Type'' Term Term)) -> t -> t
`abstract` Tele (Dom' Term (Type'' Term Term))
gamma1

  reportSDoc "rewriting" 40 $
    "Full context: " <+> prettyTCM gamma

  -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
  -- This is necessary to replace copies created by imports by their
  -- original definition.
  lhs <- modifyAllowedReductions (const $ SmallSet.singleton InlineReductions) $ reduce lhs

  -- Find head symbol f of the lhs, its type, its parameters (in case of a constructor), and its arguments.
  (f , hd , t , pars , es) <- case lhs of
    Def QName
f [Elim]
es -> do
      def <- QName -> MaybeT (TCMT IO) Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      checkAxFunOrCon f def
      return (RewDefHead f , Def f , defType def , [] , es)
    Con ConHead
c ConInfo
ci [Elim]
vs -> do
      let hd :: [Elim] -> Term
hd = ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci
      ~(Just ((_ , _ , pars) , t)) <- ConHead
-> Type'' Term Term
-> MaybeT
     (TCMT IO)
     (Maybe ((QName, Type'' Term Term, [Arg Term]), Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
ConHead
-> Type'' Term Term
-> m (Maybe
        ((QName, Type'' Term Term, [Arg Term]), Type'' Term Term))
getFullyAppliedConType ConHead
c Type'' Term Term
b
      pars <- addContext gamma1 $ checkParametersAreGeneral c pars
      return (RewDefHead $ conName c , hd , t , pars , vs)
    Var Int
x [Elim]
es | RewriteSource -> Bool
isLocalRewrite RewriteSource
s -> do
      t <- Tele (Dom' Term (Type'' Term Term))
-> MaybeT (TCMT IO) (Type'' Term Term)
-> MaybeT (TCMT IO) (Type'' Term Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
gamma1 (MaybeT (TCMT IO) (Type'' Term Term)
 -> MaybeT (TCMT IO) (Type'' Term Term))
-> MaybeT (TCMT IO) (Type'' Term Term)
-> MaybeT (TCMT IO) (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Int -> MaybeT (TCMT IO) (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
x
      return (RewVarHead (x - size gamma1), Var x , t , [] , es)
    Term
_ -> do
      ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting.rule.check" Int
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
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
hsep
        [ TCMT IO Doc
"LHSNotDefinitionOrConstructor: ", Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs ]
      RewriteSource
-> IllegalRewriteRuleReason
-> MaybeT
     (TCMT IO)
     (RewriteHead, [Elim] -> Term, Type'' Term Term, [Int], [Elim])
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor

  ifNotAlreadyAdded s f $ do

  let rewGamma = if RewriteSource -> Bool
isLocalRewrite RewriteSource
s then Tele (Dom' Term (Type'' Term Term))
gamma1 else Tele (Dom' Term (Type'' Term Term))
gamma

      telStart = Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
rewGamma

  addContext gamma1 $ do

    checkNoLhsReduction telStart f hd es

    ps <- fromRightM failureBlocked $ lift $
      catchPatternErr (pure . Left) $
        Right <$> patternFrom
          NeverSing NeverSing telStart 0 (t , headToTerm telStart f) es

    reportSDoc "rewriting" 30 $
      "Pattern generated from lhs: " <+> prettyTCM (headToPat telStart f 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 PatVars neverSingPatVars maybeSingPatVars = nlPatVars ps
        boundVars   = VarSet
neverSingPatVars VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
maybeSingPatVars
        telVars     = Int -> VarSet
VarSet.full Int
telStart
        freeVarsLhs = VarSet
telVars VarSet -> VarSet -> VarSet
`VarSet.intersection` Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
lhs
        freeVarsRhs = VarSet
telVars VarSet -> VarSet -> VarSet
`VarSet.intersection` Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
rhs
        freeVars    = VarSet
freeVarsLhs VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
freeVarsRhs
        usedVars    = case RewriteSource
s of
          LocalRewrite Context
_ Maybe Name
_ Type'' Term Term
_ -> VarSet
VarSet.empty
          GlobalRewrite Definition
def  -> case Definition -> Defn
theDef Definition
def of
            Function{}         -> Definition -> VarSet
usedArgs Definition
def
            Axiom{}            -> VarSet
telVars
            AbstractDefn{}     -> VarSet
telVars
            Constructor{}      -> VarSet
telVars
            Primitive{}        -> VarSet
telVars
            DataOrRecSig{}     -> VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
            GeneralizableVar{} -> VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
            Datatype{}         -> VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
            Record{}           -> VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
            PrimitiveSort{}    -> VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
    reportSDoc "rewriting" 70 $
      "variables bound by pattern never singularly: " <+>
      text (show neverSingPatVars)
    reportSDoc "rewriting" 70 $
      "variables bound by the pattern: " <+> text (show boundVars)
    reportSDoc "rewriting" 70 $
      "variables free in the lhs: " <+> text (show freeVarsLhs)
    reportSDoc "rewriting" 70 $
      "variables free in the rhs: " <+> text (show freeVarsRhs)
    reportSDoc "rewriting" 70 $
      "variables used by the rewrite rule: " <+> text (show usedVars)

    -- All variables occurring in the rewrite must be bound somewhere
    -- (otherwise the rewrite will simply never fire)
    unlessNull (freeVars VarSet.\\ boundVars) failureFreeVars
    -- #5238: All variables used in the proof of the rewrite must be
    -- present in the context for the rewrite to fire safely.
    -- Searching the context is not feasible though, so we instead use the
    -- tighter criteria that the variables must occur somewhere on the LHS.
    unlessNull (usedVars VarSet.\\ (boundVars `VarSet.union` VarSet.fromList pars)) failureFreeVars
    reportSDoc "rewriting" 70 $
      "variables bound in (erased) parameter position: " <+> text (show pars)
    unlessNull (boundVars `VarSet.intersection` VarSet.fromList pars) failureNonLinearPars

    -- #5929: All variables occurring on the rhs should be bound in
    -- contexts that will never become definitionally singular (even after
    -- a substitution), otherwise we can lose subject reduction.
    unlessNull (freeVarsRhs VarSet.\\ neverSingPatVars) warnUnsafeVars

    top <- fromMaybe __IMPOSSIBLE__ <$> currentTopLevelModule
    let rew = Tele (Dom' Term (Type'' Term Term))
-> RewriteHead
-> [Elim' NLPat]
-> Term
-> Type'' Term Term
-> RewriteRule
RewriteRule Tele (Dom' Term (Type'' Term Term))
rewGamma RewriteHead
f [Elim' NLPat]
ps Term
rhs Type'' Term Term
b

    reportSDoc "rewriting" 10 $ vcat
      [ "checked rewrite rule" , prettyTCM rew ]
    reportSDoc "rewriting" 90 $ vcat
      [ "checked rewrite rule" , text (show rew) ]

    return rew
  where
    ifNotAlreadyAdded ::
         RewriteSource -> RewriteHead -> MaybeT TCM RewriteRule
      -> MaybeT TCM RewriteRule
    ifNotAlreadyAdded :: RewriteSource
-> RewriteHead
-> MaybeT (TCMT IO) RewriteRule
-> MaybeT (TCMT IO) RewriteRule
ifNotAlreadyAdded (GlobalRewrite Definition
def) (RewDefHead QName
f) MaybeT (TCMT IO) RewriteRule
cont = do
      rews <- QName -> MaybeT (TCMT IO) [GlobalRewriteRule]
forall (m :: * -> *).
HasConstInfo m =>
QName -> m [GlobalRewriteRule]
getGlobalRewriteRulesFor QName
f
      -- check if q is already an added rewrite rule
      case List.find ((defName def ==) . grName) rews of
        Just GlobalRewriteRule
rew -> RewriteSource
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule (Definition -> RewriteSource
GlobalRewrite Definition
def) IllegalRewriteRuleReason
DuplicateRewriteRule
        Maybe GlobalRewriteRule
Nothing -> MaybeT (TCMT IO) RewriteRule
cont
    ifNotAlreadyAdded (GlobalRewrite Definition
def) (RewVarHead Int
x) MaybeT (TCMT IO) RewriteRule
cont = MaybeT (TCMT IO) RewriteRule
forall a. HasCallStack => a
__IMPOSSIBLE__
    ifNotAlreadyAdded (LocalRewrite Context
_ Maybe Name
_ Type'' Term Term
_) RewriteHead
f MaybeT (TCMT IO) RewriteRule
cont = MaybeT (TCMT IO) RewriteRule
cont

    checkNoLhsReduction ::
         Nat -> RewriteHead -> (Elims -> Term) -> Elims
      -> MaybeT TCM ()
    checkNoLhsReduction :: Int
-> RewriteHead -> ([Elim] -> Term) -> [Elim] -> MaybeT (TCMT IO) ()
checkNoLhsReduction Int
telStart RewriteHead
f [Elim] -> Term
hd [Elim]
es = do
      -- Skip this check when global confluence check is enabled, as
      -- redundant rewrite rules may be required to prove confluence.
      MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
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)
-> MaybeT (TCMT IO) PragmaOptions -> MaybeT (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (TCMT IO) PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
-> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
      let v :: Term
v = [Elim] -> Term
hd [Elim]
es
      v' <- Term -> MaybeT (TCMT IO) Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      let fail :: MaybeT TCM a
          fail = do
            ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
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 -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
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')
            RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Term -> Term -> IllegalRewriteRuleReason
LHSReduces Term
v Term
v'
      es' <- case (f, v') of
        (RewDefHead QName
f, Def QName
f' [Elim]
es')   | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'            -> [Elim] -> MaybeT (TCMT IO) [Elim]
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Elim]
es'
        (RewDefHead QName
f, Con ConHead
c' ConInfo
_ [Elim]
es') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c'    -> [Elim] -> MaybeT (TCMT IO) [Elim]
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Elim]
es'
        (RewVarHead Int
x, Var Int
x' [Elim]
es')   | Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
telStart Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> [Elim] -> MaybeT (TCMT IO) [Elim]
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Elim]
es'
        (RewriteHead, Term)
_                              -> MaybeT (TCMT IO) [Elim]
forall a. MaybeT (TCMT IO) a
fail
      unless (null es && null es') $ do
        a   <- lift $ computeRewHeadType telStart f es es'
        pol <- case f of
          RewDefHead QName
f -> Comparison -> QName -> MaybeT (TCMT IO) [Polarity]
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
f
          RewVarHead Int
x -> [Polarity] -> MaybeT (TCMT IO) [Polarity]
forall a. a -> MaybeT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        ok  <- lift $ dontAssignMetas $ tryConversion $
                 compareElims pol [] a (headToTerm telStart f []) es es'
        unless ok fail

    checkAxFunOrCon :: QName -> Definition -> MaybeT TCM ()
    checkAxFunOrCon :: QName -> Definition -> MaybeT (TCMT IO) ()
checkAxFunOrCon QName
f Definition
def = case Definition -> Defn
theDef Definition
def of
      Axiom{}        -> () -> MaybeT (TCMT IO) ()
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      def :: Defn
def@Function{} -> do
        Maybe Projection
-> (Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Either ProjectionLikenessMissing Projection -> Maybe Projection
forall a b. Either a b -> Maybe b
maybeRight (Defn -> Either ProjectionLikenessMissing Projection
funProjection Defn
def)) ((Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ())
-> (Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \Projection
proj -> case Projection -> Maybe QName
projProper Projection
proj of
          Maybe QName
Nothing -> RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason
HeadSymbolIsProjectionLikeFunction QName
f
          Just{} -> MaybeT (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__
            -- Andreas, 2024-08-20
            -- A projection ought to be impossible in the head, since they are represented
            -- in post-fix in the internal syntax.
            -- Thus, a lone projection @p@ will be @λ x → x .p@
            -- and an applied projection @p t@ will be @t .p@.
        MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Maybe ConfluenceCheck -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ConfluenceCheck -> Bool)
-> (PragmaOptions -> Maybe ConfluenceCheck)
-> PragmaOptions
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck (PragmaOptions -> Bool)
-> MaybeT (TCMT IO) PragmaOptions -> MaybeT (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (TCMT IO) PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
-> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
          let simpleClause :: Clause -> ([Elim], Maybe Term)
simpleClause Clause
cl = ([NamedArg DeBruijnPattern] -> [Elim]
patternsToElims (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) , Clause -> Maybe Term
clauseBody Clause
cl)
          cls <- [([Elim], Maybe Term)] -> MaybeT (TCMT IO) [([Elim], Maybe Term)]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([([Elim], Maybe Term)] -> MaybeT (TCMT IO) [([Elim], Maybe Term)])
-> [([Elim], Maybe Term)]
-> MaybeT (TCMT IO) [([Elim], Maybe Term)]
forall a b. (a -> b) -> a -> b
$ (Clause -> ([Elim], Maybe Term))
-> [Clause] -> [([Elim], Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> ([Elim], Maybe Term)
simpleClause ([Clause] -> [([Elim], Maybe Term)])
-> [Clause] -> [([Elim], Maybe Term)]
forall a b. (a -> b) -> a -> b
$ Defn -> [Clause]
funClauses Defn
def
          unless (noMetas cls) $ illegalRule s $ HeadSymbolContainsMetas f

      Constructor{}  -> () -> MaybeT (TCMT IO) ()
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      AbstractDefn{} -> () -> MaybeT (TCMT IO) ()
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Primitive{}    -> () -> MaybeT (TCMT IO) ()
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: is this fine?
      Datatype{}     -> MaybeT (TCMT IO) ()
illegalHead
      Record{}       -> MaybeT (TCMT IO) ()
illegalHead
      DatatypeDefn{} -> MaybeT (TCMT IO) ()
illegalHead
      RecordDefn{}   -> MaybeT (TCMT IO) ()
illegalHead
      DataOrRecSig{} -> MaybeT (TCMT IO) ()
illegalHead
      PrimitiveSort{}-> MaybeT (TCMT IO) ()
illegalHead
      GeneralizableVar{} -> MaybeT (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

      where
        illegalHead :: MaybeT (TCMT IO) ()
illegalHead = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason
HeadSymbolIsTypeConstructor QName
f

    usedArgs :: Definition -> VarSet
    usedArgs :: Definition -> VarSet
usedArgs Definition
def = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
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 -> MaybeT TCM [Int]
    checkParametersAreGeneral :: ConHead -> [Arg Term] -> MaybeT (TCMT IO) [Int]
checkParametersAreGeneral ConHead
c [Arg Term]
vs = do
        is <- [Arg Term] -> MaybeT (TCMT IO) [Int]
loop [Arg Term]
vs
        unless (fastDistinct is) $ errorNotGeneral
        return is
      where
        loop :: [Arg Term] -> MaybeT (TCMT IO) [Int]
loop []       = [Int] -> MaybeT (TCMT IO) [Int]
forall a. a -> MaybeT (TCMT IO) a
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])
-> MaybeT (TCMT IO) [Int] -> MaybeT (TCMT IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> MaybeT (TCMT IO) [Int]
loop [Arg Term]
vs
          Term
_        -> MaybeT (TCMT IO) [Int]
forall a. MaybeT (TCMT IO) a
errorNotGeneral

        errorNotGeneral :: MaybeT TCM a
        errorNotGeneral :: forall a. MaybeT (TCMT IO) a
errorNotGeneral = RewriteSource -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ ConHead -> Args1 -> IllegalRewriteRuleReason
ConstructorParametersNotGeneral ConHead
c (Args1 -> IllegalRewriteRuleReason)
-> Args1 -> IllegalRewriteRuleReason
forall a b. (a -> b) -> a -> b
$
          Args1 -> Maybe Args1 -> Args1
forall a. a -> Maybe a -> a
fromMaybe Args1
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args1 -> Args1) -> Maybe Args1 -> Args1
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe Args1
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Arg Term]
vs

checkRewConstraint :: LocalEquation -> TCM ()
checkRewConstraint :: LocalEquation' Term -> TCM ()
checkRewConstraint
  eq :: LocalEquation' Term
eq@(LocalEquation {lEqContext :: forall t. LocalEquation' t -> Tele (Dom' t (Type'' t t))
lEqContext = Tele (Dom' Term (Type'' Term Term))
g, lEqLHS :: forall t. LocalEquation' t -> t
lEqLHS = Term
l, lEqRHS :: forall t. LocalEquation' t -> t
lEqRHS = Term
r, lEqType :: forall t. LocalEquation' t -> Type'' t t
lEqType = Type'' Term Term
t}) = do
  c <- Lens' TCEnv (Maybe (Closure Call))
-> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe (Closure Call) -> f (Maybe (Closure Call)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Maybe (Closure Call))
eCall
  traceCall (CheckLocalRewriteConstraint eq c) $ addContext g $ equalTerm t l r

-- | @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'' Term Term
-> ([Elim] -> Term)
-> RewriteRule
-> [Elim]
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type'' Term Term
t [Elim] -> Term
hd rew :: RewriteRule
rew@(RewriteRule Tele (Dom' Term (Type'' Term Term))
gamma RewriteHead
_ [Elim' NLPat]
ps Term
rhs Type'' Term Term
b) [Elim]
es = 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd [Elim]
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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> 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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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
forall (m :: * -> *). MonadPretty m => RewriteRule -> 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) ([Elim] -> Term
hd [Elim]
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) ([Elim] -> 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'' Term Term -> ArgName) -> Type'' Term Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> ArgName
forall a. Show a => a -> ArgName
show) Type'' Term Term
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
  result <- Tele (Dom' Term (Type'' Term Term))
-> TypeOf [Elim]
-> [Elim' NLPat]
-> [Elim]
-> ReduceM (Either (Blocked' Term ()) Substitution)
forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Tele (Dom' Term (Type'' Term Term))
-> TypeOf b -> a -> b -> m (Either (Blocked' Term ()) Substitution)
nonLinMatch Tele (Dom' Term (Type'' Term Term))
gamma (Type'' Term Term
t,[Elim] -> Term
hd) [Elim' NLPat]
ps [Elim]
es
  case result of
    Left Blocked' Term ()
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 a. a -> ReduceM a
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' Term ()
block Blocked' Term () -> Term -> Blocked Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> [Elim] -> Term
hd [Elim]
es -- TODO: remember reductions
    Right Substitution
sub  -> do
      let v' :: Term
v' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd [Elim]
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
forall (m :: * -> *). MonadPretty m => Term -> 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 a. a -> ReduceM a
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' Term ()
-> ([Elim] -> Term)
-> [RewriteRule]
-> [Elim]
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked' Term ()
block [Elim] -> Term
hd [RewriteRule]
rules [Elim]
es = do
  rewritingAllowed <- ReduceM Bool
forall (m :: * -> *). HasOptions m => m Bool
anyRewritingOption
  if (rewritingAllowed && not (null rules)) then do
    (_ , t) <- fromMaybe __IMPOSSIBLE__ <$> getLocalHeadType (hd [])
    loop block t rules es
  else
    return $ NoReduction (block $> hd es)
  where
    loop ::
         Blocked_ -> Type -> RewriteRules -> Elims
      -> ReduceM (Reduced (Blocked Term) Term)
    loop :: Blocked' Term ()
-> Type'' Term Term
-> [RewriteRule]
-> [Elim]
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked' Term ()
block Type'' Term Term
t [] [Elim]
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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd [Elim]
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' Term () -> ArgName
forall a. Show a => a -> ArgName
show Blocked' Term ()
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 a. a -> ReduceM a
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' Term ()
block Blocked' Term () -> Term -> Blocked Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> [Elim] -> Term
hd [Elim]
es
    loop Blocked' Term ()
block Type'' Term Term
t (RewriteRule
rew:[RewriteRule]
rews) [Elim]
es
     | let n :: Int
n = RewriteRule -> Int
rewArity RewriteRule
rew, [Elim] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Elim]
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = do
          let ([Elim]
es1, [Elim]
es2) = Int -> [Elim] -> ([Elim], [Elim])
forall i a. Integral i => i -> [a] -> ([a], [a])
List.genericSplitAt Int
n [Elim]
es
          result <- Type'' Term Term
-> ([Elim] -> Term)
-> RewriteRule
-> [Elim]
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type'' Term Term
t [Elim] -> Term
hd RewriteRule
rew [Elim]
es1
          case result of
            Left (Blocked Blocker
m Term
u)    -> Blocked' Term ()
-> Type'' Term Term
-> [RewriteRule]
-> [Elim]
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked' Term ()
block Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` Blocker -> () -> Blocked' Term ()
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
m ()) Type'' Term Term
t [RewriteRule]
rews [Elim]
es
            Left (NotBlocked NotBlocked' Term
_ Term
_) -> Blocked' Term ()
-> Type'' Term Term
-> [RewriteRule]
-> [Elim]
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked' Term ()
block Type'' Term Term
t [RewriteRule]
rews [Elim]
es
            Right Term
w               -> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall a. a -> ReduceM a
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 -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es2
     | Bool
otherwise = Blocked' Term ()
-> Type'' Term Term
-> [RewriteRule]
-> [Elim]
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked' Term ()
block Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
Underapplied ()) Type'' Term Term
t [RewriteRule]
rews [Elim]
es

    rewArity :: RewriteRule -> Int
rewArity = [Elim' NLPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Elim' NLPat] -> Int)
-> (RewriteRule -> [Elim' NLPat]) -> RewriteRule -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> [Elim' NLPat]
rewPats