{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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 =
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optRewriting forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionRewriting
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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v 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
]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCM (Maybe RelView)
relView Type
t)
(TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because it should accept at least two arguments") 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensHiding a => a -> Bool
visible Dom Type
a Bool -> Bool -> Bool
&& forall a. LensHiding a => a -> Bool
visible Dom Type
b) forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because its two final arguments are not both visible."
case forall t a. Type'' t a -> a
unEl Type
core of
Sort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Con{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Level{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Lam{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Pi{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Term
_ -> TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because its type does not end in a sort, but in "
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core
data RelView = RelView
{ RelView -> Tele (Dom Type)
relViewTel :: Telescope
, RelView -> [Dom (ArgName, Type)]
relViewDelta :: ListTel
, RelView -> Dom Type
relViewType :: Dom Type
, RelView -> Dom Type
relViewType' :: Dom Type
, RelView -> Type
relViewCore :: Type
}
relView :: Type -> TCM (Maybe RelView)
relView :: Type -> TCM (Maybe RelView)
relView Type
t = do
TelV Tele (Dom Type)
tel Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
let n :: Int
n = forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
([Dom (ArgName, Type)]
delta, [Dom (ArgName, Type)]
lastTwo) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n forall a. Num a => a -> a -> a
- Int
2) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel
if forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
lastTwo forall a. Ord a => a -> a -> Bool
< Int
2 then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else do
let [Dom Type
a, Dom Type
b] = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom (ArgName, Type)]
lastTwo
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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
addRewriteRules :: [QName] -> TCM ()
addRewriteRules :: [QName] -> TCM ()
addRewriteRules [QName]
qs = do
RewriteRules
rews <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM RewriteRule
checkRewriteRule [QName]
qs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RewriteRules
rews forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
let f :: QName
f = RewriteRule -> QName
rewHead RewriteRule
rew
matchables :: [QName]
matchables = forall a. GetMatchables a => a -> [QName]
getMatchables RewriteRule
rew
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"adding rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
"to the definition of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"matchable symbols: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
matchables
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor QName
f [RewriteRule
rew] [QName]
matchables
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ \ConfluenceCheck
confChk -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConfluenceCheck
confChk forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> QName
rewHead RewriteRules
rews) QName -> TCM ()
sortRulesOfSymbol
ConfluenceCheck -> RewriteRules -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk RewriteRules
rews
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"done checking confluence of rules" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) RewriteRules
rews)
checkRewriteRule :: QName -> TCM RewriteRule
checkRewriteRule :: QName -> TCM RewriteRule
checkRewriteRule QName
q = do
TCM ()
requireOptionRewriting
let failNoBuiltin :: TCMT IO a
failNoBuiltin = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
ArgName
"Cannot add rewrite rule without prior BUILTIN REWRITE"
QName
rel <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM forall {a}. TCMT IO a
failNoBuiltin forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
ArgName -> m (Maybe QName)
getBuiltinName ArgName
builtinRewrite
Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Defn -> Bool
isEmptyFunction forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ TCMT IO Doc
"Rewrite rule from function "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
, TCMT IO Doc
" cannot be added before the function definition"
]
Maybe RelView
relV <- Type -> TCM (Maybe RelView)
relView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe RelView
relV
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ do
TCMT IO Doc
"rewrite relation at type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Dom (ArgName, Type)] -> Tele (Dom Type)
telFromList [Dom (ArgName, Type)]
delta) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" |- " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Dom (ArgName, Type)]
delta forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
TelV Tele (Dom Type)
gamma1 Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"attempting to add rewrite rule of type "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
gamma1
, TCMT IO Doc
" |- " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core
]
let failureWrongTarget :: TCM a
failureWrongTarget :: forall {a}. TCMT IO a
failureWrongTarget = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" does not target rewrite relation" ]
let failureMetas :: TCM a
failureMetas :: forall {a}. TCMT IO a
failureMetas = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since it contains unsolved meta variables" ]
let failureNotDefOrCon :: TCM a
failureNotDefOrCon :: forall {a}. TCMT IO a
failureNotDefOrCon = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
let failureFreeVars :: IntSet -> TCM a
failureFreeVars :: forall a. IntSet -> TCM a
failureFreeVars IntSet
xs = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ 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: " , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
xs) ]
let failureIllegalRule :: TCM a
failureIllegalRule :: forall {a}. TCMT IO a
failureIllegalRule = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule" ]
case forall t a. Type'' t a -> a
unEl Type
core of
Def QName
rel' es :: Elims
es@(Elim' Term
_:Elim' Term
_:Elims
_) | QName
rel forall a. Eq a => a -> a -> Bool
== QName
rel' -> do
let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
n :: Int
n = forall a. Sized a => a -> Int
size [Term]
vs
([Term]
us, [Term
lhs, Term
rhs]) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n forall a. Num a => a -> a -> a
- Int
2) [Term]
vs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
delta forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Term]
us) forall a. HasCallStack => a
__IMPOSSIBLE__
Term
lhs <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
lhs
Term
rhs <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
rhs
Dom Type
b <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Term]
us) Dom Type
a
Tele (Dom Type)
gamma0 <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
Tele (Dom Type)
gamma1 <- 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 forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
gamma1
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. AllMetas a => a -> Bool
noMetas (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
gamma1)) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metas in gamma1: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. AllMetas a => a -> [MetaId]
allMetasList forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
gamma1)
forall {a}. TCMT IO a
failureMetas
Term
lhs <- forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. SmallSetElement a => a -> SmallSet a
SmallSet.singleton AllowedReduction
InlineReductions) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
lhs
(QName
f , Elims -> Term
hd , Type
t , [Int]
pars , Elims
es) <- case Term
lhs of
Def QName
f Elims
es -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
QName -> Definition -> TCM ()
checkAxFunOrCon QName
f Definition
def
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)) <- forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
getFullyAppliedConType ConHead
c forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
b
[Int]
pars <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ ConHead -> [Arg Term] -> TCMT IO [Int]
checkParametersAreGeneral ConHead
c [Arg Term]
pars
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> QName
conName ConHead
c , Elims -> Term
hd , Type
t , [Int]
pars , Elims
vs)
Term
_ -> forall {a}. TCMT IO a
failureNotDefOrCon
QName -> TCM RewriteRule -> TCM RewriteRule
ifNotAlreadyAdded QName
f forall a b. (a -> b) -> a -> b
$ do
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ do
QName -> (Elims -> Term) -> Elims -> TCM ()
checkNoLhsReduction QName
f Elims -> Term
hd Elims
es
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. AllMetas a => a -> Bool
noMetas (Elims
es, Term
rhs, Dom Type
b)) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metas in lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. AllMetas a => a -> [MetaId]
allMetasList Elims
es)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metas in rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. AllMetas a => a -> [MetaId]
allMetasList Term
rhs)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metas in b : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. AllMetas a => a -> [MetaId]
allMetasList Dom Type
b)
forall {a}. TCMT IO a
failureMetas
PElims
ps <- 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
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Pattern generated from lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> PElims -> NLPat
PDef QName
f PElims
ps)
let boundVars :: IntSet
boundVars = forall a. NLPatVars a => a -> IntSet
nlPatVars PElims
ps
freeVars :: IntSet
freeVars = forall t. Free t => t -> IntSet
allFreeVars (PElims
ps,Term
rhs)
allVars :: IntSet
allVars = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ 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
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"variables bound by the pattern: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
boundVars)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"variables free in the rewrite rule: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
freeVars)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"variables used by the rewrite rule: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
usedVars)
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (IntSet
freeVars IntSet -> IntSet -> IntSet
IntSet.\\ IntSet
boundVars) forall a. IntSet -> TCM a
failureFreeVars
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)) forall a. IntSet -> TCM a
failureFreeVars
let rew :: RewriteRule
rew = QName
-> Tele (Dom Type)
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
q Tele (Dom Type)
gamma QName
f PElims
ps Term
rhs (forall t e. Dom' t e -> e
unDom Dom Type
b) Bool
False
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checked rewrite rule" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew ]
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
90 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checked rewrite rule" , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show RewriteRule
rew) ]
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew
Term
_ -> forall {a}. TCMT IO a
failureWrongTarget
where
checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> TCM ()
checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> TCM ()
checkNoLhsReduction QName
f Elims -> Term
hd Elims
es = do
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just ConfluenceCheck
GlobalConfluenceCheck) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
let v :: Term
v = Elims -> Term
hd Elims
es
Term
v' <- 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
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Term
v)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Term
v')
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not a legal rewrite rule, since the left-hand side "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" reduces to " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' ]
Elims
es' <- case Term
v' of
Def QName
f' Elims
es' | QName
f forall a. Eq a => a -> a -> Bool
== QName
f' -> forall (m :: * -> *) a. Monad m => a -> m a
return Elims
es'
Con ConHead
c' ConInfo
_ Elims
es' | QName
f forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c' -> forall (m :: * -> *) a. Monad m => a -> m a
return Elims
es'
Term
_ -> forall {a}. TCMT IO a
fail
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Elims
es Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Elims
es') forall a b. (a -> b) -> a -> b
$ do
Type
a <- forall (m :: * -> *).
MonadConversion m =>
QName -> Elims -> Elims -> m Type
computeElimHeadType QName
f Elims
es Elims
es'
[Polarity]
pol <- forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
f
Bool
ok <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$
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'
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Function{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Constructor{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
AbstractDefn{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Primitive{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ 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"
, 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 -> TCM RewriteRule -> TCM RewriteRule
ifNotAlreadyAdded QName
f TCM RewriteRule
cont = do
RewriteRules
rews <- forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
f
case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((QName
q forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) RewriteRules
rews of
Just RewriteRule
rew -> do
forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
TCMT IO Doc
"Rewrite rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has already been added"
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew
Maybe RewriteRule
Nothing -> TCM RewriteRule
cont
usedArgs :: Definition -> IntSet
usedArgs :: Definition -> IntSet
usedArgs Definition
def = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ [(Occurrence, Int)]
usedIxs
where
occs :: [Occurrence]
occs = Definition -> [Occurrence]
defArgOccurrences Definition
def
allIxs :: [(Occurrence, Int)]
allIxs = forall a b. [a] -> [b] -> [(a, b)]
zip [Occurrence]
occs forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size [Occurrence]
occs
usedIxs :: [(Occurrence, Int)]
usedIxs = forall a. (a -> Bool) -> [a] -> [a]
filter (Occurrence -> Bool
used forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => [a] -> Bool
fastDistinct [Int]
is) forall a b. (a -> b) -> a -> b
$ forall {a}. TCMT IO a
errorNotGeneral
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
is
where
loop :: [Arg Term] -> TCMT IO [Int]
loop [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
loop (Arg Term
v : [Arg Term]
vs) = case forall e. Arg e -> e
unArg Arg Term
v of
Var Int
i [] -> (Int
i forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TCMT IO [Int]
loop [Arg Term]
vs
Term
_ -> forall {a}. TCMT IO a
errorNotGeneral
errorNotGeneral :: TCM a
errorNotGeneral :: forall {a}. TCMT IO a
errorNotGeneral = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Constructor: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
]
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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd Elims
es
| Bool
otherwise = do
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"{ attempting to rewrite term " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
, TCMT IO Doc
" having head " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, TCMT IO Doc
" with rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew
]) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
90 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"raw: attempting to rewrite term " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) (Elims -> Term
hd Elims
es)
, TCMT IO Doc
" having head " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Type
t
, TCMT IO Doc
" with rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) RewriteRule
rew
]) forall a b. (a -> b) -> a -> b
$ do
Either Blocked_ Substitution
result <- forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
Tele (Dom Type) -> t -> 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 -> forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 TCMT IO Doc
"}" forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Blocked_
block forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd Elims
es
Right Substitution
sub -> do
let v' :: Term
v' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub Term
rhs
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"rewrote " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
, TCMT IO Doc
" to " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"}"
]) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Term
v'
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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
if (Bool
rewritingAllowed Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null RewriteRules
rules)) then do
(QName
_ , Type
t) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
es
else
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction (Blocked_
block 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 =
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
20 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"failed to rewrite " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
, TCMT IO Doc
"blocking tag" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Blocked_
block)
]) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ Blocked_
block 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, forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es forall a. Ord a => a -> a -> Bool
>= Int
n = do
let (Elims
es1, Elims
es2) = 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 forall a. Monoid a => a -> a -> a
`mappend` 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification forall a b. (a -> b) -> a -> b
$ Term
w forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2
| Bool
otherwise = Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block forall a. Monoid a => a -> a -> a
`mappend` forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
Underapplied ()) Type
t RewriteRules
rews Elims
es
rewArity :: RewriteRule -> Int
rewArity :: RewriteRule -> Int
rewArity = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> PElims
rewPats