module Agda.TypeChecking.Rewriting where
import Control.Monad
import Control.Monad.Reader (local)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
verifyBuiltinRewrite :: Term -> Type -> TCM ()
verifyBuiltinRewrite v t = do
let failure reason = typeError . GenericDocError =<< sep
[ prettyTCM v <+> text " does not have the right type for a rewriting relation"
, reason
]
caseMaybeM (relView t)
(failure $ text "because it should accept at least two arguments") $
\ (RelView tel delta a b core) -> do
case ignoreSharing (unEl core) of
Sort{} -> do
unlessM (tryConversion $
inTopContext $ addContext tel $ escapeContext 1 $
equalType (raise 1 a) b) $
failure $ text $ "because the types of the last two arguments are different"
Con{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Pi{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
_ -> failure $ text "because its type does not end in a sort, but in "
<+> do inTopContext $ addContext tel $ prettyTCM core
data RelView = RelView
{ relViewTel :: Telescope
, relViewDelta :: ListTel
, relViewType :: Type
, relViewType' :: Type
, relViewCore :: Type
}
relView :: Type -> TCM (Maybe RelView)
relView t = do
TelV tel core <- telView t
let n = size tel
(delta, lastTwo) = splitAt (n 2) $ telToList tel
if size lastTwo < 2 then return Nothing else do
let [a, b] = snd . unDom <$> lastTwo
return $ Just $ RelView tel delta a b core
addRewriteRule :: QName -> TCM ()
addRewriteRule q = do
let failureWrongTarget = typeError . GenericDocError =<< sep
[ prettyTCM q , text " does not target rewrite relation" ]
let failureMetas = typeError . GenericDocError =<< sep
[ prettyTCM q , text " is not a legal rewrite rule, since it contains unsolved meta variables" ]
let failureFreeVars = typeError . GenericDocError =<< sep
[ prettyTCM q , text " is not a legal rewrite rule, since not all variables are bound by the left hand side" ]
let failureIllegalRule = typeError . GenericDocError =<< sep
[ prettyTCM q , text " is not a legal rewrite rule" ]
Def rel _ <- primRewrite
Just (RelView _tel delta a _a' _core) <- relView =<< do
defType <$> getConstInfo rel
reportSDoc "rewriting" 30 $ do
text "rewrite relation at type " <+> do
inTopContext $ prettyTCM (telFromList delta) <+> text " |- " <+> do
addContext delta $ prettyTCM a
t <- defType <$> getConstInfo q
TelV gamma core <- telView t
case ignoreSharing $ unEl core of
Def rel' es@(_:_:_) | rel == rel' -> do
let vs = map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
n = size vs
(us, [lhs, rhs]) = splitAt (n 2) vs
unless (size delta == size us) __IMPOSSIBLE__
let b = applySubst (parallelS $ reverse us) a
lhs <- etaContract =<< normalise lhs
rhs <- etaContract =<< normalise rhs
unless (null $ allMetas (telToList gamma, lhs, rhs, b)) failureMetas
let rew = RewriteRule q gamma lhs rhs b
reportSDoc "rewriting" 10 $
text "considering rewrite rule " <+> prettyTCM rew
addContext gamma $
unlessM (isJust <$> rewriteWith (Just b) lhs rew) $
failureFreeVars
case ignoreSharing lhs of
Def f _ -> do
addRewriteRules f [rew]
_ -> failureIllegalRule
_ -> failureWrongTarget
addRewriteRules :: QName -> RewriteRules -> TCM ()
addRewriteRules f rews =
modifySignature $ updateDefinition f $ updateRewriteRules $ (++ rews)
updateRewriteRules :: (RewriteRules -> RewriteRules) -> Definition -> Definition
updateRewriteRules f def = def { defRewriteRules = f (defRewriteRules def) }
rewriteWith :: Maybe Type -> Term -> RewriteRule -> TCM (Maybe Term)
rewriteWith mt v (RewriteRule q gamma lhs rhs b) = do
xs <- newTelMeta gamma
let sigma = parallelS $ map unArg xs
(lhs', rhs', b') = applySubst sigma (lhs, rhs, b)
ok <- tryConversion $ do
whenJust mt $ \ t -> leqType t b'
local (\ e -> e {envCompareBlocked = True}) $ equalTerm b' lhs' v
unlessM (isInstantiatedMeta xs) $ do
reportSDoc "rewriting" 20 $ text "lhs variables solved with: " <+> do
sep $ map prettyTCM xs
typeError $ GenericError $ "free variables not bound by left hand side"
if ok then return $ Just rhs' else return Nothing
rewrite :: Term -> TCM (Maybe Term)
rewrite v = do
case ignoreSharing v of
Def f es -> do
rews <- defRewriteRules <$> getConstInfo f
loop rews
where
loop [] = return Nothing
loop (rew:rews) = do
caseMaybeM (rewriteWith Nothing v rew) (loop rews) (return . Just)
_ -> return Nothing