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

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

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

module Agda.TypeChecking.Rewriting where

import Prelude hiding (null)

import Control.Monad

import Data.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 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Type
a Bool -> Bool -> Bool
&& Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Type
b) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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 Tele (Dom Type)
tel Type
core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let n :: Int
n                = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
      ([Dom (ArgName, Type)]
delta, [Dom (ArgName, Type)]
lastTwo) = Int
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) ([Dom (ArgName, Type)]
 -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel
  if [Dom (ArgName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
lastTwo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 then Maybe RelView -> TCMT IO (Maybe RelView)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe RelView
forall a. Maybe a
Nothing else do
    let [Dom Type
a, Dom Type
b] = ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd (Dom (ArgName, Type) -> Dom Type)
-> [Dom (ArgName, Type)] -> [Dom Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom (ArgName, Type)]
lastTwo
    Maybe RelView -> TCMT IO (Maybe RelView)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe RelView -> TCMT IO (Maybe RelView))
-> Maybe RelView -> TCMT IO (Maybe RelView)
forall a b. (a -> b) -> a -> b
$ RelView -> Maybe RelView
forall a. a -> Maybe a
Just (RelView -> Maybe RelView) -> RelView -> Maybe RelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> [Dom (ArgName, Type)] -> Dom Type -> Dom Type -> Type -> RelView
RelView Tele (Dom Type)
tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
b Type
core

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

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

  -- Add rewrite rules to the signature
  RewriteRules -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RewriteRules
rews ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
    let f :: QName
f = RewriteRule -> QName
rewHead RewriteRule
rew
        matchables :: [QName]
matchables = RewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables RewriteRule
rew
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"adding rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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)
  TCMT IO (Maybe ConfluenceCheck)
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ConfluenceCheck
confChk -> do
    -- Warn if --cubical is enabled
    TCMT IO (Maybe Cubical) -> (Cubical -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Maybe Cubical)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe Cubical)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) ((Cubical -> TCM ()) -> TCM ()) -> (Cubical -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Cubical
_ -> Doc -> TCM ()
forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning
      Doc
"Confluence checking for --cubical is not yet supported, confluence checking might be incomplete"
    -- Global confluence checker requires rules to be sorted
    -- according to the generality of their lhs
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConfluenceCheck
confChk ConfluenceCheck -> ConfluenceCheck -> Bool
forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((QName -> QName) -> [QName] -> [QName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn QName -> QName
forall a. a -> a
id ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ (RewriteRule -> QName) -> RewriteRules -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> QName
rewHead RewriteRules
rews) QName -> TCM ()
sortRulesOfSymbol
    ConfluenceCheck -> RewriteRules -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk RewriteRules
rews
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"done checking confluence of rules" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((RewriteRule -> TCMT IO Doc) -> RewriteRules -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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.
  Maybe RelView
relV <- Type -> TCMT IO (Maybe RelView)
relView (Type -> TCMT IO (Maybe RelView))
-> TCMT IO Type -> TCMT IO (Maybe RelView)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
rel
  let RelView Tele (Dom Type)
_tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
_a' Type
_core = RelView -> Maybe RelView -> RelView
forall a. a -> Maybe a -> a
fromMaybe RelView
forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe RelView
relV
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    TCMT IO Doc
"rewrite relation at type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
      TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM ([Dom (ArgName, Type)] -> Tele (Dom Type)
telFromList [Dom (ArgName, Type)]
delta) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" |- " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        [Dom (ArgName, Type)] -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
[Dom (ArgName, Type)] -> m a -> m a
addContext [Dom (ArgName, Type)]
delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
  ([Dom (ArgName, Type)], Dom Type)
-> TCM ([Dom (ArgName, Type)], Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dom (ArgName, Type)]
delta, Dom Type
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 RewriteRule
checkRewriteRule :: QName -> TCMT IO RewriteRule
checkRewriteRule QName
q = do
  TCM ()
requireOptionRewriting
  let failNoBuiltin :: TCMT IO a
failNoBuiltin = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$
        ArgName
"Cannot add rewrite rule without prior BUILTIN REWRITE"
  Set QName
rels <- TCMT IO (Set QName)
-> TCMT IO (Maybe (Set QName)) -> TCMT IO (Set QName)
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCMT IO (Set QName)
forall {a}. TCMT IO a
failNoBuiltin TCMT IO (Maybe (Set QName))
forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting.relations" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Rewrite relations:"
    , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (QName -> TCMT IO Doc) -> [QName] -> [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]) -> [QName] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set QName
rels
    ]
  Definition
def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  -- Issue 1651: Check that we are not adding a rewrite rule
  -- for a type signature whose body has not been type-checked yet.
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Defn -> Bool
isEmptyFunction (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q IllegalRewriteRuleReason
BeforeFunctionDefinition
  -- Get rewrite rule (type of q).
  TelV Tele (Dom Type)
gamma1 Type
core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"attempting to add rewrite rule of type "
    , Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
gamma1
    , TCMT IO Doc
" |- " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
core
    ]
  let failureBlocked :: Blocker -> TCM a
      failureBlocked :: forall a. Blocker -> TCM a
failureBlocked Blocker
b
        | Bool -> Bool
not (Set MetaId -> Bool
forall a. Null a => a -> Bool
null Set MetaId
ms) = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (Set MetaId -> IllegalRewriteRuleReason
ContainsUnsolvedMetaVariables Set MetaId
ms)
        | Bool -> Bool
not (Set ProblemId -> Bool
forall a. Null a => a -> Bool
null Set ProblemId
ps) = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (Set ProblemId -> IllegalRewriteRuleReason
BlockedOnProblems Set ProblemId
ps)
        | Bool -> Bool
not (Set QName -> Bool
forall a. Null a => a -> Bool
null Set QName
qs) = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (Set QName -> IllegalRewriteRuleReason
RequiresDefinitions Set QName
qs)
        | Bool
otherwise = TCMT IO a
forall a. HasCallStack => a
__IMPOSSIBLE__
        where
          ms :: Set MetaId
ms = Blocker -> Set MetaId
allBlockingMetas Blocker
b
          ps :: Set ProblemId
ps = Blocker -> Set ProblemId
allBlockingProblems Blocker
b
          qs :: Set QName
qs = Blocker -> Set QName
allBlockingDefs Blocker
b
  let failureFreeVars :: IntSet -> TCM a
      failureFreeVars :: forall a. IntSet -> TCM a
failureFreeVars IntSet
xs = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (IntSet -> IllegalRewriteRuleReason
VariablesNotBoundByLHS IntSet
xs)
  let failureNonLinearPars :: IntSet -> TCM a
      failureNonLinearPars :: forall a. IntSet -> TCM a
failureNonLinearPars IntSet
xs = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (IntSet -> IllegalRewriteRuleReason
VariablesBoundMoreThanOnce IntSet
xs)
  let failureIllegalRule :: TCM a -- TODO:: Defined but not used
      failureIllegalRule :: forall {a}. TCMT IO a
failureIllegalRule = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q IllegalRewriteRuleReason
EmptyReason

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

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

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

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

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

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

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

        PElims
ps <- (Blocker -> TCMT IO PElims) -> TCMT IO PElims -> TCMT IO PElims
forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr Blocker -> TCMT IO PElims
forall a. Blocker -> TCM a
failureBlocked (TCMT IO PElims -> TCMT IO PElims)
-> TCMT IO PElims -> TCMT IO PElims
forall a b. (a -> b) -> a -> b
$
          Relevance -> Int -> TypeOf Elims -> Elims -> TCMT IO PElims
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
Relevant Int
0 (Type
t , QName -> Elims -> Term
Def QName
f) Elims
es

        ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Pattern generated from lhs: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (QName -> PElims -> NLPat
PDef QName
f PElims
ps)

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

        ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"variables bound in (erased) parameter position: " 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 ([Int] -> ArgName
forall a. Show a => a -> ArgName
show [Int]
pars)
        IntSet -> (IntSet -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (IntSet
boundVars IntSet -> IntSet -> IntSet
`IntSet.intersection` [Int] -> IntSet
IntSet.fromList [Int]
pars) IntSet -> TCM ()
forall a. IntSet -> TCM a
failureNonLinearPars

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

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

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

    Term
_ -> TypeError -> TCMT IO RewriteRule
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO RewriteRule)
-> TypeError -> TCMT IO RewriteRule
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q IllegalRewriteRuleReason
DoesNotTargetRewriteRelation

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

    checkAxFunOrCon :: QName -> Definition -> TCM ()
    checkAxFunOrCon :: QName -> Definition -> TCM ()
checkAxFunOrCon QName
f Definition
def = case Definition -> Defn
theDef Definition
def of
      Axiom{}        -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      def :: Defn
def@Function{} -> do
        Maybe Projection -> (Projection -> TCM ()) -> TCM ()
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 -> TCM ()) -> TCM ())
-> (Projection -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Projection
proj -> case Projection -> Maybe QName
projProper Projection
proj of
          Just{} -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (QName -> IllegalRewriteRuleReason
HeadSymbolIsProjection QName
f)
          Maybe QName
Nothing -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (QName -> IllegalRewriteRuleReason
HeadSymbolIsProjectionLikeFunction QName
f)
        TCMT IO Bool -> TCM () -> TCM ()
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) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          let simpleClause :: Clause -> (Elims, Maybe Term)
simpleClause Clause
cl = ([NamedArg DeBruijnPattern] -> Elims
patternsToElims (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) , Clause -> Maybe Term
clauseBody Clause
cl)
          [(Elims, Maybe Term)]
cls <- [(Elims, Maybe Term)] -> TCMT IO [(Elims, Maybe Term)]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([(Elims, Maybe Term)] -> TCMT IO [(Elims, Maybe Term)])
-> [(Elims, Maybe Term)] -> 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
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Elims, Maybe Term)] -> Bool
forall a. AllMetas a => a -> Bool
noMetas [(Elims, Maybe Term)]
cls) (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
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (QName -> IllegalRewriteRuleReason
HeadSymbolDefContainsMetas QName
f)

      Constructor{}  -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      AbstractDefn{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Primitive{}    -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: is this fine?
      Defn
_              -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (QName -> IllegalRewriteRuleReason
HeadSymbolNotPostulateFunctionConstructor QName
f)

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

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

    checkParametersAreGeneral :: ConHead -> Args -> TCM [Int]
    checkParametersAreGeneral :: ConHead -> [Arg Term] -> TCMT IO [Int]
checkParametersAreGeneral ConHead
c [Arg Term]
vs = do
        [Int]
is <- [Arg Term] -> TCMT IO [Int]
loop [Arg Term]
vs
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Int]
is) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall {a}. TCMT IO a
errorNotGeneral
        [Int] -> TCMT IO [Int]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
is
      where
        loop :: [Arg Term] -> TCMT IO [Int]
loop []       = [Int] -> TCMT IO [Int]
forall a. a -> 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]) -> TCMT IO [Int] -> TCMT IO [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TCMT IO [Int]
loop [Arg Term]
vs
          Term
_        -> TCMT IO [Int]
forall {a}. TCMT IO a
errorNotGeneral

        errorNotGeneral :: TCM a
        errorNotGeneral :: forall {a}. TCMT IO a
errorNotGeneral = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> IllegalRewriteRuleReason -> TypeError
IllegalRewriteRule QName
q (ConHead -> [Arg Term] -> IllegalRewriteRuleReason
ConstructorParamsNotGeneral 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
  Either Blocked_ Substitution
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 Either Blocked_ Substitution
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
  Bool
rewritingAllowed <- PragmaOptions -> Bool
optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  if (Bool
rewritingAllowed Bool -> Bool -> Bool
&& Bool -> Bool
not (RewriteRules -> Bool
forall a. Null a => a -> Bool
null RewriteRules
rules)) then do
    (QName
_ , Type
t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
forall a. a -> Maybe a -> a
fromMaybe (QName, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
-> ReduceM (Maybe (QName, Type)) -> ReduceM (QName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReduceM (Maybe (QName, Type))
forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead (Elims -> Term
hd [])
    Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t RewriteRules
rules (Elims -> ReduceM (Reduced (Blocked Term) Term))
-> ReduceM Elims -> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> ReduceM Elims
forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
es -- TODO: remove instantiateFull?
  else
    Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall 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_
block Blocked_ -> Term -> Blocked Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd Elims
es)
  where
    loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
    loop :: Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t [] Elims
es =
      ArgName
-> Int
-> TCMT IO Doc
-> ReduceM (Reduced (Blocked Term) Term)
-> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
20 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"failed to rewrite " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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
          Either (Blocked Term) Term
result <- Type
-> (Elims -> Term)
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type
t Elims -> Term
hd RewriteRule
rew Elims
es1
          case Either (Blocked Term) Term
result of
            Left (Blocked Blocker
m Term
u)    -> Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block Blocked_ -> Blocked_ -> Blocked_
forall a. Monoid a => a -> a -> a
`mappend` Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
m ()) Type
t RewriteRules
rews Elims
es
            Left (NotBlocked NotBlocked' Term
_ Term
_) -> Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t RewriteRules
rews Elims
es
            Right Term
w               -> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall 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