module Agda.TypeChecking.Rewriting where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Reader (local)
import Data.Foldable ( Foldable, foldMap )
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Monoid
import Agda.Interaction.Options
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.TypeChecking.Rewriting.NonLinMatch
import qualified Agda.TypeChecking.Reduce.Monad as Red
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
requireOptionRewriting :: TCM ()
requireOptionRewriting =
unlessM (optRewriting <$> pragmaOptions) $ typeError NeedOptionRewriting
verifyBuiltinRewrite :: Term -> Type -> TCM ()
verifyBuiltinRewrite v t = do
requireOptionRewriting
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 = inTopContext $ do
requireOptionRewriting
Def rel _ <- primRewrite
def <- getConstInfo q
when (isEmptyFunction $ theDef def) $
typeError . GenericDocError =<< hsep
[ text "Rewrite rule from function "
, prettyTCM q
, text " cannot be added before the function definition"
]
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
TelV gamma core <- telView $ defType def
reportSDoc "rewriting" 30 $ do
text "attempting to add rewrite rule of type " <+> do
inTopContext $ prettyTCM gamma <+> text " |- " <+> do
addContext gamma $ prettyTCM core
let failureWrongTarget = typeError . GenericDocError =<< hsep
[ prettyTCM q , text " does not target rewrite relation" ]
let failureMetas = typeError . GenericDocError =<< hsep
[ prettyTCM q , text " is not a legal rewrite rule, since it contains unsolved meta variables" ]
let failureNotDefOrCon = typeError . GenericDocError =<< hsep
[ prettyTCM q , text " is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
let failureFreeVars xs = typeError . GenericDocError =<< do
addContext gamma $ hsep $
[ prettyTCM q , text " is not a legal rewrite rule, since the following variables are not bound by the left hand side: " , prettyList_ (map (prettyTCM . var) xs) ]
let failureLhsReduction lhs = typeError . GenericDocError =<< do
addContext gamma $ hsep $
[ prettyTCM q , text " is not a legal rewrite rule, since the left-hand side " , prettyTCM lhs , text " has top-level reductions" ]
let failureIllegalRule = typeError . GenericDocError =<< hsep
[ prettyTCM q , text " is not a legal rewrite rule" ]
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__
b <- instantiateFull $ applySubst (parallelS $ reverse us) a
gamma <- instantiateFull gamma
f <- case ignoreSharing lhs of
Def f es -> return f
Con c vs -> return $ conName c
_ -> failureNotDefOrCon
lhs <- normaliseArgs lhs
unlessM (isNormal lhs) $ failureLhsReduction lhs
rhs <- etaContract =<< normalise rhs
unless (null $ allMetas (telToList gamma, lhs, rhs, b)) failureMetas
pat <- patternFrom 0 lhs
let rew = RewriteRule q gamma pat rhs b
reportSDoc "rewriting" 10 $ addContext gamma $
text "considering rewrite rule " <+> prettyTCM rew
unlessNull ([0 .. size gamma 1] List.\\ IntSet.toList (nlPatVars pat)) failureFreeVars
addRewriteRules f [rew]
_ -> failureWrongTarget
where
normaliseArgs :: Term -> TCM Term
normaliseArgs v = case ignoreSharing v of
Def f es -> Def f <$> do etaContract =<< normalise es
Con c vs -> Con c <$> do etaContract =<< normalise vs
_ -> __IMPOSSIBLE__
isNormal :: Term -> TCM Bool
isNormal v = do
v' <- normalise v
return $ v == v'
addRewriteRules :: QName -> RewriteRules -> TCM ()
addRewriteRules f rews = do
reportSDoc "rewriting" 10 $ text "rewrite rule ok, adding it to the definition of " <+> prettyTCM f
modifySignature $ addRewriteRulesFor f rews
rules <- getRewriteRulesFor f
reportSDoc "rewriting" 20 $ vcat
[ text "rewrite rules for " <+> prettyTCM f <+> text ":"
, vcat (map prettyTCM rules)
]
rewriteWith :: Maybe Type -> Term -> RewriteRule -> ReduceM (Either (Blocked Term) Term)
rewriteWith mt v (RewriteRule q gamma lhs rhs b) = do
Red.traceSDoc "rewriting" 95 (sep
[ text "attempting to rewrite term " <+> prettyTCM v
, text " with rule " <+> prettyTCM q
]) $ do
result <- nonLinMatch lhs v
case result of
Left block -> return $ Left $ const v <$> block
Right sub -> do
let v' = applySubst sub rhs
Red.traceSDoc "rewriting" 90 (sep
[ text "rewrote " <+> prettyTCM v
, text " to " <+> prettyTCM v'
]) $ return $ Right v'
rewrite :: Blocked Term -> ReduceM (Either (Blocked Term) Term)
rewrite bv = ifNotM (optRewriting <$> pragmaOptions) (return $ Left bv) $ do
let v = ignoreBlocking bv
case ignoreSharing v of
Def f es -> rew f (Def f) es
Con c vs -> rew (conName c) hd (Apply <$> vs)
where hd es = Con c $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
_ -> return $ Left bv
where
rew :: QName -> (Elims -> Term) -> Elims -> ReduceM (Either (Blocked Term) Term)
rew f hd es = do
rules <- getRewriteRulesFor f
case rules of
[] -> return $ Left $ bv $> hd es
_ -> do
es <- etaContract =<< instantiateFull' es
loop (void bv) es rules
where
loop :: Blocked_ -> Elims -> [RewriteRule] -> ReduceM (Either (Blocked Term) Term)
loop block es [] = return $ Left $ block $> hd es
loop block es (rew:rews)
| let n = rewArity rew, length es >= n = do
let (es1, es2) = List.genericSplitAt n es
result <- rewriteWith Nothing (hd es1) rew
case result of
Left (Blocked m u) -> loop (block `mappend` Blocked m ()) es rews
Left (NotBlocked _ _) -> loop block es rews
Right w -> return $ Right $ w `applyE` es2
| otherwise = loop (block `mappend` NotBlocked Underapplied ()) es rews
class NLPatVars a where
nlPatVars :: a -> IntSet
instance (Foldable f, NLPatVars a) => NLPatVars (f a) where
nlPatVars = foldMap nlPatVars
instance NLPatVars NLPat where
nlPatVars p =
case p of
PVar i -> singleton i
PDef _ es -> nlPatVars es
PWild -> empty
PLam _ p' -> nlPatVars $ unAbs p'
PPi a b -> nlPatVars a `IntSet.union` nlPatVars (unAbs b)
PBoundVar _ es -> nlPatVars es
PTerm{} -> empty
rewArity :: RewriteRule -> Int
rewArity rew = case rewLHS rew of
PDef _f es -> length es
_ -> __IMPOSSIBLE__