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

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

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

module Agda.TypeChecking.Rewriting where

import Prelude hiding (null)

import Control.Monad

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

import Agda.Interaction.Options

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

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

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

import Agda.Utils.Impossible

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

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

-- | Deconstructing a type into @Δ → t → t' → core@.
data RelView = RelView
  { RelView -> Telescope
relViewTel   :: Telescope  -- ^ The whole telescope @Δ, t, t'@.
  , RelView -> ListTel
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 Telescope
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                = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
      (ListTel
delta, ListTel
lastTwo) = Int -> ListTel -> (ListTel, ListTel)
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) (ListTel -> (ListTel, ListTel)) -> ListTel -> (ListTel, ListTel)
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
  if ListTel -> Int
forall a. Sized a => a -> Int
size ListTel
lastTwo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 then Maybe RelView -> TCMT IO (Maybe RelView)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe RelView
forall a. Maybe a
Nothing else do
    let [Dom Type
a, Dom Type
b] = ((ArgName, Type) -> Type) -> Dom' Term (ArgName, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd (Dom' Term (ArgName, Type) -> Dom Type) -> ListTel -> [Dom Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListTel
lastTwo
    Maybe RelView -> TCMT IO (Maybe RelView)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe RelView -> TCMT IO (Maybe RelView))
-> Maybe RelView -> TCMT IO (Maybe RelView)
forall a b. (a -> b) -> a -> b
$ RelView -> Maybe RelView
forall a. a -> Maybe a
Just (RelView -> Maybe RelView) -> RelView -> Maybe RelView
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel -> Dom Type -> Dom Type -> Type -> RelView
RelView Telescope
tel ListTel
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
  [RewriteRule]
rews <- (QName -> TCMT IO RewriteRule) -> [QName] -> TCMT IO [RewriteRule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO RewriteRule
checkRewriteRule [QName]
qs

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


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

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

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

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

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

      -- Find head symbol f of the lhs, its type and its arguments.
      (QName
f , Elims -> Term
hd , Type
t , 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, Elims)
-> TCMT IO (QName, Elims -> Term, Type, Elims)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f , QName -> Elims -> Term
Def QName
f , Definition -> Type
defType Definition
def , Elims
es)
        Con ConHead
c ConInfo
ci Elims
vs -> do
          let hd :: Elims -> Term
hd = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci
          ~(Just ((QName
_ , Type
_ , [Arg Term]
pars) , Type
t)) <- ConHead
-> Type -> TCMT IO (Maybe ((QName, Type, [Arg Term]), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug 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
          Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma1 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ConHead -> Int -> [Arg Term] -> TCM ()
checkParametersAreGeneral ConHead
c (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma1) [Arg Term]
pars
          (QName, Elims -> Term, Type, Elims)
-> TCMT IO (QName, Elims -> Term, Type, Elims)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> QName
conName ConHead
c , Elims -> Term
hd , Type
t  , Elims
vs)
        Term
_        -> TCMT IO (QName, Elims -> Term, Type, Elims)
forall a. TCMT IO a
failureNotDefOrCon

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

      Telescope -> TCMT IO RewriteRule -> TCMT IO RewriteRule
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma1 (TCMT IO RewriteRule -> TCMT IO RewriteRule)
-> TCMT IO RewriteRule -> TCMT IO RewriteRule
forall a b. (a -> b) -> a -> b
$ do
        -- Normalize lhs args: we do not want to match redexes.
        Elims
es <- Elims -> TCMT IO Elims
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Elims
es

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

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

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

        -- check that FV(rhs) ⊆ nlPatVars(lhs)
        let freeVars :: IntSet
freeVars  = [Occurrence] -> IntSet
usedArgs (Definition -> [Occurrence]
defArgOccurrences Definition
def) IntSet -> IntSet -> IntSet
`IntSet.union` (PElims, Term) -> IntSet
forall t. Free t => t -> IntSet
allFreeVars (PElims
ps,Term
rhs)
            boundVars :: IntSet
boundVars = PElims -> IntSet
forall a. NLPatVars a => a -> IntSet
nlPatVars PElims
ps
        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 :: * -> *). Monad 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 :: * -> *). Monad m => ArgName -> m Doc
text (IntSet -> ArgName
forall a. Show a => a -> ArgName
show IntSet
freeVars)
        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

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

        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 :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCMT IO Doc
"checked rewrite rule" , RewriteRule -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew ]
        ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCMT IO Doc
"checked rewrite rule" , ArgName -> TCMT IO Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text (RewriteRule -> ArgName
forall a. Show a => a -> ArgName
show RewriteRule
rew) ]

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

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

  where
    checkNoLhsReduction :: QName -> Elims -> TCM ()
    checkNoLhsReduction :: QName -> Elims -> TCM ()
checkNoLhsReduction QName
f Elims
es = do
      let v :: Term
v = QName -> Elims -> Term
Def QName
f Elims
es
      Term
v' <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      let fail :: TCM ()
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 :: * -> *). Monad 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 :: * -> *). Monad m => ArgName -> m Doc
text (Term -> ArgName
forall a. Show a => a -> ArgName
show Term
v')
            TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
              [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not a legal rewrite rule, since the left-hand side "
              , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" reduces to " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' ]
      case Term
v' of
        Def QName
f' Elims
es' | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> 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 ()
fail
        Term
_ -> TCM ()
fail

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

    ifNotAlreadyAdded :: QName -> TCM RewriteRule -> TCM RewriteRule
    ifNotAlreadyAdded :: QName -> TCMT IO RewriteRule -> TCMT IO RewriteRule
ifNotAlreadyAdded QName
f TCMT IO RewriteRule
cont = do
      [RewriteRule]
rews <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
      -- check if q is already an added rewrite rule
      case (RewriteRule -> Bool) -> [RewriteRule] -> 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) [RewriteRule]
rews of
        Just RewriteRule
rew -> do
          Doc -> TCM ()
forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            TCMT IO Doc
"Rewrite rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has already been added"
          RewriteRule -> TCMT IO RewriteRule
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew
        Maybe RewriteRule
Nothing -> TCMT IO RewriteRule
cont

    usedArgs :: [Pos.Occurrence] -> IntSet
    usedArgs :: [Occurrence] -> IntSet
usedArgs [Occurrence]
occs = [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
        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 -> Int -> Args -> TCM ()
    checkParametersAreGeneral :: ConHead -> Int -> [Arg Term] -> TCM ()
checkParametersAreGeneral ConHead
c Int
k [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
      where
        loop :: [Arg Term] -> TCMT IO [Int]
loop []       = [Int] -> TCMT IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        loop (Arg Term
v : [Arg Term]
vs) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
          Var Int
i [] | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> (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 :: TCM a
errorNotGeneral = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text ArgName
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text ArgName
"Constructor: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text ArgName
"Parameters: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
            ]

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

-- | @rewrite b v rules es@ tries to rewrite @v@ applied to @es@ with the
--   rewrite rules @rules@. @b@ is the default blocking tag.
rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
rewrite :: Blocked_
-> Term
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked_
block Term
v [RewriteRule]
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 ([RewriteRule] -> Bool
forall a. Null a => a -> Bool
null [RewriteRule]
rules)) then do
    Type
t <- case Term
v of
      Def QName
f []   -> Definition -> Type
defType (Definition -> Type) -> ReduceM Definition -> ReduceM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      Con ConHead
c ConInfo
_ [] -> QName -> ReduceM Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst (QName -> ReduceM Type) -> QName -> ReduceM Type
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
        -- Andreas, 2018-09-08, issue #3211:
        -- discount module parameters for constructor heads
      Term
_ -> ReduceM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
    Blocked_
-> Type
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t [RewriteRule]
rules (Elims -> ReduceM (Reduced (Blocked Term) Term))
-> ReduceM Elims -> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> ReduceM Elims
forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
es -- TODO: remove instantiateFull?
  else
    Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Term) Term
 -> ReduceM (Reduced (Blocked Term) Term))
-> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Reduced (Blocked Term) Term
forall no yes. no -> Reduced no yes
NoReduction (Blocked_
block Blocked_ -> Term -> Blocked Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es)
  where
    loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
    loop :: Blocked_
-> Type
-> [RewriteRule]
-> 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 :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ TCMT IO Doc
"failed to rewrite " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` 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 :: * -> *). Monad m => ArgName -> m Doc
text (Blocked_ -> ArgName
forall a. Show a => a -> ArgName
show Blocked_
block)
        ]) (ReduceM (Reduced (Blocked Term) Term)
 -> ReduceM (Reduced (Blocked Term) Term))
-> ReduceM (Reduced (Blocked Term) Term)
-> ReduceM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ do
      Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Term) Term
 -> ReduceM (Reduced (Blocked Term) Term))
-> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Reduced (Blocked Term) Term
forall no yes. no -> Reduced no yes
NoReduction (Blocked Term -> Reduced (Blocked Term) Term)
-> Blocked Term -> Reduced (Blocked Term) Term
forall a b. (a -> b) -> a -> b
$ Blocked_
block Blocked_ -> Term -> Blocked Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
    loop Blocked_
block Type
t (RewriteRule
rew:[RewriteRule]
rews) Elims
es
     | let n :: Int
n = RewriteRule -> Int
rewArity RewriteRule
rew, Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = do
          let (Elims
es1, Elims
es2) = Int -> Elims -> (Elims, Elims)
forall i a. Integral i => i -> [a] -> ([a], [a])
List.genericSplitAt Int
n Elims
es
          Either (Blocked Term) Term
result <- Type
-> Term
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type
t Term
v RewriteRule
rew Elims
es1
          case Either (Blocked Term) Term
result of
            Left (Blocked MetaId
m Term
u)    -> Blocked_
-> Type
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block Blocked_ -> Blocked_ -> Blocked_
forall a. Monoid a => a -> a -> a
`mappend` MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ()) Type
t [RewriteRule]
rews Elims
es
            Left (NotBlocked NotBlocked
_ Term
_) -> Blocked_
-> Type
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t [RewriteRule]
rews Elims
es
            Right Term
w               -> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Term) Term
 -> ReduceM (Reduced (Blocked Term) Term))
-> Reduced (Blocked Term) Term
-> ReduceM (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced (Blocked Term) Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (Term -> Reduced (Blocked Term) Term)
-> Term -> Reduced (Blocked Term) Term
forall a b. (a -> b) -> a -> b
$ Term
w Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2
     | Bool
otherwise = Blocked_
-> Type
-> [RewriteRule]
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block Blocked_ -> Blocked_ -> Blocked_
forall a. Monoid a => a -> a -> a
`mappend` NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
Underapplied ()) Type
t [RewriteRule]
rews Elims
es

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