{-# 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 Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
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 Agda.Utils.Impossible
import Agda.Utils.Either

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
  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)
    (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 Type)
tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
b Type
core) -> do
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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
$ 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
forall t a. Type'' t a -> a
unEl Type
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 -> Tele (Dom Type) -> IncorrectTypeForRewriteRelationReason
TypeDoesNotEndInSort Type
core Tele (Dom Type)
tel)

-- | 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 tel core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let n                = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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 RewriteRule))
-> [QName] -> TCMT IO RewriteRules
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM QName -> TCMT IO (Maybe RewriteRule)
checkRewriteRule [QName]
qs

  -- Add rewrite rules to the signature
  forM_ rews $ \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
forall (m :: * -> *). MonadPretty m => QName -> 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
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
    (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)
  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
$ (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
forall (m :: * -> *). MonadPretty m => QName -> 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)

-- Auxiliary function for checkRewriteRule.
-- | Get domain of rewrite relation.
rewriteRelationDom :: QName -> TCM (ListTel, Dom Type)
rewriteRelationDom :: QName -> TCM ([Dom (ArgName, Type)], Dom Type)
rewriteRelationDom QName
rel = do
  -- We know that the type of rel is that of a relation.
  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 _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)

-- | 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 RewriteRule)
checkRewriteRule :: QName -> TCMT IO (Maybe RewriteRule)
checkRewriteRule QName
q = MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule))
-> MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule)
forall a b. (a -> b) -> a -> b
$ QName
-> MaybeT (TCMT IO) RewriteRule -> MaybeT (TCMT IO) RewriteRule
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 <- TCMT IO (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 TCMT IO (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 BeforeFunctionDefinition
  -- Issue 6643: Also check that there are no mututal definitions
  -- that are not yet defined.
  whenJustM (asksTC envMutualBlock) \ 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 => 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
$
        IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason
BeforeMutualFunctionDefinition QName
r


  -- Get rewrite rule (type of q).
  TelV gamma1 core <- telView $ defType def
  reportSDoc "rewriting" 30 $ vcat
    [ "attempting to add rewrite rule of type "
    , prettyTCM gamma1
    , " |- " <+> do addContext gamma1 $ prettyTCM core
    ]
  let failureBlocked :: Blocker -> MaybeT TCM a
      failureBlocked Blocker
b
        | Set1.IsNonEmpty NESet MetaId
ms <- Blocker -> Set MetaId
allBlockingMetas    Blocker
b = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ NESet MetaId -> IllegalRewriteRuleReason
ContainsUnsolvedMetaVariables NESet MetaId
ms
        | Set1.IsNonEmpty NESet ProblemId
ps <- Blocker -> Set ProblemId
allBlockingProblems Blocker
b = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (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 = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (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 :: IntSet -> MaybeT TCM a
      failureFreeVars IntSet
xs = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ IntSet -> IllegalRewriteRuleReason
VariablesNotBoundByLHS IntSet
xs
  let failureNonLinearPars :: IntSet -> MaybeT TCM a
      failureNonLinearPars IntSet
xs = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ IntSet -> IllegalRewriteRuleReason
VariablesBoundMoreThanOnce IntSet
xs

  -- Check that type of q targets rel.
  case unEl core of
    Def QName
rel es :: Elims
es@(Elim' Term
_:Elim' Term
_:Elims
_) | 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)], Dom Type)
-> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type)
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)], Dom Type)
 -> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type))
-> TCM ([Dom (ArgName, Type)], Dom Type)
-> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type)
forall a b. (a -> b) -> a -> b
$ QName -> TCM ([Dom (ArgName, Type)], Dom Type)
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
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
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

      gamma0 <- getContextTelescope
      gamma1 <- instantiateFull gamma1
      let 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

      -- 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 Elims
es -> do
          def <- QName -> MaybeT (TCMT IO) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          checkAxFunOrCon f def
          return (f , Def f , defType def , [] , es)
        Con ConHead
c ConInfo
ci Elims
vs -> do
          let hd :: Elims -> Term
hd = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci
          ~(Just ((_ , _ , pars) , t)) <- ConHead
-> Type
-> MaybeT (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
 -> MaybeT (TCMT IO) (Maybe ((QName, Type, [Arg Term]), Type)))
-> Type
-> MaybeT (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
          pars <- addContext gamma1 $ checkParametersAreGeneral c pars
          return (conName c , hd , t , pars , vs)
        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 ]
          IllegalRewriteRuleReason
-> MaybeT (TCMT IO) (QName, Elims -> Term, Type, [Int], Elims)
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor

      ifNotAlreadyAdded f $ do

      addContext gamma1 $ do

        checkNoLhsReduction f hd es

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

        reportSDoc "rewriting" 30 $
          "Pattern generated from lhs: " <+> prettyTCM (PDef 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 boundVars = PElims -> IntSet
forall a. NLPatVars a => a -> IntSet
nlPatVars PElims
ps
            freeVars  = (PElims, Term) -> IntSet
forall t. Free t => t -> IntSet
allFreeVars (PElims
ps,Term
rhs)
            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  = 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__
        reportSDoc "rewriting" 70 $
          "variables bound by the pattern: " <+> text (show boundVars)
        reportSDoc "rewriting" 70 $
          "variables free in the rewrite rule: " <+> text (show freeVars)
        reportSDoc "rewriting" 70 $
          "variables used by the rewrite rule: " <+> text (show usedVars)
        unlessNull (freeVars IntSet.\\ boundVars) failureFreeVars
        unlessNull (usedVars IntSet.\\ (boundVars `IntSet.union` IntSet.fromList pars)) failureFreeVars

        reportSDoc "rewriting" 70 $
          "variables bound in (erased) parameter position: " <+> text (show pars)
        unlessNull (boundVars `IntSet.intersection` IntSet.fromList pars) failureNonLinearPars

        let 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

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

        return rew

    Term
_ -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule IllegalRewriteRuleReason
DoesNotTargetRewriteRelation

  where
    illegalRule :: IllegalRewriteRuleReason -> MaybeT TCM a
    illegalRule :: forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule IllegalRewriteRuleReason
reason = 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 () -> MaybeT (TCMT IO) ()) -> TCM () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> Warning
IllegalRewriteRule QName
q IllegalRewriteRuleReason
reason
      MaybeT (TCMT IO) a
forall a. MaybeT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> MaybeT TCM ()
    checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> MaybeT (TCMT IO) ()
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.
      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 = Elims -> Term
hd Elims
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')
            IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (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 v' of
        Def QName
f' Elims
es'   | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'         -> Elims -> MaybeT (TCMT IO) Elims
forall a. a -> MaybeT (TCMT IO) a
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 -> MaybeT (TCMT IO) Elims
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Elims
es'
        Term
_                              -> MaybeT (TCMT IO) Elims
forall a. MaybeT (TCMT IO) a
fail
      unless (null es && null es') $ do
        a   <- lift $ computeElimHeadType f es es'
        pol <- getPolarity' CmpEq f
        ok  <- lift $ dontAssignMetas $ tryConversion $
                 compareElims pol [] a (Def 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 -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (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 -> (Elims, Maybe Term)
simpleClause Clause
cl = ([NamedArg DeBruijnPattern] -> Elims
patternsToElims (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) , Clause -> Maybe Term
clauseBody Clause
cl)
          cls <- [(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)])
-> [(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)]
forall a b. (a -> b) -> a -> b
$ (Clause -> (Elims, Maybe Term))
-> [Clause] -> [(Elims, Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> (Elims, Maybe Term)
simpleClause ([Clause] -> [(Elims, Maybe Term)])
-> [Clause] -> [(Elims, Maybe Term)]
forall a b. (a -> b) -> a -> b
$ Defn -> [Clause]
funClauses Defn
def
          unless (noMetas cls) $ illegalRule $ 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 = IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason
HeadSymbolIsTypeConstructor QName
f

    ifNotAlreadyAdded :: QName -> MaybeT TCM RewriteRule -> MaybeT TCM RewriteRule
    ifNotAlreadyAdded :: QName
-> MaybeT (TCMT IO) RewriteRule -> MaybeT (TCMT IO) RewriteRule
ifNotAlreadyAdded QName
f MaybeT (TCMT IO) RewriteRule
cont = do
      rews <- QName -> MaybeT (TCMT IO) RewriteRules
forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
f
      -- check if q is already an added rewrite rule
      case List.find ((q ==) . rewName) rews of
        Just RewriteRule
rew -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule IllegalRewriteRuleReason
DuplicateRewriteRule
        Maybe RewriteRule
Nothing -> MaybeT (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 -> 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 = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ ConHead -> [Arg Term] -> IllegalRewriteRuleReason
ConstructorParametersNotGeneral ConHead
c [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 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
$ 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
forall (m :: * -> *). MonadPretty m => Term -> 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
forall (m :: * -> *). MonadPretty m => Term -> 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
forall (m :: * -> *). MonadPretty m => Type -> 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
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) (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
  result <- Tele (Dom Type)
-> TypeOf Elims
-> PElims
-> Elims
-> ReduceM (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Tele (Dom Type)
-> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Tele (Dom Type)
gamma (Type
t,Elims -> Term
hd) PElims
ps Elims
es
  case 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 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_
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
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 (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
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_
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked_
block Elims -> Term
hd RewriteRules
rules Elims
es = do
  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 (rewritingAllowed && not (null rules)) then do
    (_ , t) <- fromMaybe __IMPOSSIBLE__ <$> getTypedHead (hd [])
    loop block t rules =<< instantiateFull' es -- TODO: remove instantiateFull?
  else
    return $ NoReduction (block $> hd 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
forall (m :: * -> *). MonadPretty m => Term -> 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 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_
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
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
          result <- Type
-> (Elims -> Term)
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type
t Elims -> Term
hd RewriteRule
rew Elims
es1
          case 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 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 -> 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 a. [a] -> 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