{-# 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 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 <+> " does not have the right type for a rewriting relation"
, reason
]
caseMaybeM (relView t)
(failure $ "because it should accept at least two arguments") $
\ (RelView tel delta a b core) -> do
unless (visible a && visible b) $ failure $ "because its two final arguments are not both visible."
case unEl core of
Sort{} -> return ()
Con{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Pi{} -> __IMPOSSIBLE__
_ -> failure $ "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 :: Dom Type
, relViewType' :: Dom 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] = fmap snd <$> lastTwo
return $ Just $ RelView tel delta a b core
addRewriteRules :: [QName] -> TCM ()
addRewriteRules qs = do
rews <- mapM checkRewriteRule qs
forM_ rews $ \rew -> do
let f = rewHead rew
matchables = getMatchables rew
reportSDoc "rewriting" 10 $
"adding rule" <+> prettyTCM (rewName rew) <+>
"to the definition of" <+> prettyTCM f
reportSDoc "rewriting" 30 $ "matchable symbols: " <+> prettyTCM matchables
modifySignature $ addRewriteRulesFor f [rew] matchables
whenM (optConfluenceCheck <$> pragmaOptions) $
checkConfluenceOfRules rews
checkRewriteRule :: QName -> TCM RewriteRule
checkRewriteRule q = do
requireOptionRewriting
let failNoBuiltin = typeError $ GenericError $
"Cannot add rewrite rule without prior BUILTIN REWRITE"
rel <- fromMaybeM failNoBuiltin $ getBuiltinName builtinRewrite
def <- instantiateDef =<< getConstInfo q
when (isEmptyFunction $ theDef def) $
typeError . GenericDocError =<< hsep
[ "Rewrite rule from function "
, prettyTCM q
, " cannot be added before the function definition"
]
relV <- relView =<< do defType <$> getConstInfo rel
let RelView _tel delta a _a' _core = fromMaybe __IMPOSSIBLE__ relV
reportSDoc "rewriting" 30 $ do
"rewrite relation at type " <+> do
inTopContext $ prettyTCM (telFromList delta) <+> " |- " <+> do
addContext delta $ prettyTCM a
TelV gamma1 core <- telView $ defType def
reportSDoc "rewriting" 30 $ vcat
[ "attempting to add rewrite rule of type "
, prettyTCM gamma1
, " |- " <+> do addContext gamma1 $ prettyTCM core
]
let failureWrongTarget :: TCM a
failureWrongTarget = typeError . GenericDocError =<< hsep
[ prettyTCM q , " does not target rewrite relation" ]
let failureMetas :: TCM a
failureMetas = typeError . GenericDocError =<< hsep
[ prettyTCM q , " is not a legal rewrite rule, since it contains unsolved meta variables" ]
let failureNotDefOrCon :: TCM a
failureNotDefOrCon = typeError . GenericDocError =<< hsep
[ prettyTCM q , " 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 xs = typeError . GenericDocError =<< hsep
[ prettyTCM q , " is not a legal rewrite rule, since the following variables are not bound by the left hand side: " , prettyList_ (map (prettyTCM . var) $ IntSet.toList xs) ]
let failureIllegalRule :: TCM a
failureIllegalRule = typeError . GenericDocError =<< hsep
[ prettyTCM q , " is not a legal rewrite rule" ]
case 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__
rhs <- instantiateFull rhs
b <- instantiateFull $ applySubst (parallelS $ reverse us) a
gamma0 <- getContextTelescope
gamma1 <- instantiateFull gamma1
let gamma = gamma0 `abstract` gamma1
unless (noMetas (telToList gamma1)) $ do
reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetasList $ telToList gamma1)
failureMetas
lhs <- modifyAllowedReductions (const [InlineReductions]) $ normalise lhs
(f , hd , t , es) <- case lhs of
Def f es -> do
def <- getConstInfo f
checkAxFunOrCon f def
return (f , Def f , defType def , es)
Con c ci vs -> do
let hd = Con c ci
~(Just ((_ , _ , pars) , t)) <- getFullyAppliedConType c $ unDom b
addContext gamma1 $ checkParametersAreGeneral c (size gamma1) pars
return (conName c , hd , t , vs)
_ -> failureNotDefOrCon
ifNotAlreadyAdded f $ do
addContext gamma1 $ do
es <- normalise es
checkNoLhsReduction f es
unless (noMetas (es, rhs, b)) $ do
reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetasList es)
reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetasList rhs)
reportSDoc "rewriting" 30 $ "metas in b : " <+> text (show $ allMetasList b)
failureMetas
ps <- patternFrom Relevant 0 (t , Def f []) es
reportSDoc "rewriting" 30 $
"Pattern generated from lhs: " <+> prettyTCM (PDef f ps)
let freeVars = usedArgs (defArgOccurrences def) `IntSet.union` allFreeVars (ps,rhs)
boundVars = nlPatVars ps
reportSDoc "rewriting" 70 $
"variables bound by the pattern: " <+> text (show boundVars)
reportSDoc "rewriting" 70 $
"variables free in the rewrite rule: " <+> text (show freeVars)
unlessNull (freeVars IntSet.\\ boundVars) failureFreeVars
let rew = RewriteRule q gamma f ps rhs (unDom b)
reportSDoc "rewriting" 10 $ vcat
[ "checked rewrite rule" , prettyTCM rew ]
reportSDoc "rewriting" 90 $ vcat
[ "checked rewrite rule" , text (show rew) ]
return rew
_ -> failureWrongTarget
where
checkNoLhsReduction :: QName -> Elims -> TCM ()
checkNoLhsReduction f es = do
let v = Def f es
v' <- reduce v
let fail = do
reportSDoc "rewriting" 20 $ "v = " <+> text (show v)
reportSDoc "rewriting" 20 $ "v' = " <+> text (show v')
typeError . GenericDocError =<< fsep
[ prettyTCM q <+> " is not a legal rewrite rule, since the left-hand side "
, prettyTCM v <+> " reduces to " <+> prettyTCM v' ]
case v' of
Def f' es' | f == f' -> do
a <- computeElimHeadType f es es'
pol <- getPolarity' CmpEq f
ok <- dontAssignMetas $ tryConversion $
compareElims pol [] a (Def f []) es es'
unless ok fail
_ -> fail
checkAxFunOrCon :: QName -> Definition -> TCM ()
checkAxFunOrCon f def = case theDef def of
Axiom{} -> return ()
Function{} -> return ()
Constructor{} -> return ()
AbstractDefn{} -> return ()
Primitive{} -> return ()
_ -> typeError . GenericDocError =<< hsep
[ prettyTCM q , " is not a legal rewrite rule, since the head symbol"
, prettyTCM f , "is not a postulate, a function, or a constructor"
]
ifNotAlreadyAdded :: QName -> TCM RewriteRule -> TCM RewriteRule
ifNotAlreadyAdded f cont = do
rews <- getRewriteRulesFor f
case List.find ((q ==) . rewName) rews of
Just rew -> do
genericWarning =<< do
"Rewrite rule " <+> prettyTCM q <+> " has already been added"
return rew
Nothing -> cont
usedArgs :: [Pos.Occurrence] -> IntSet
usedArgs occs = IntSet.fromList $ map snd $ usedIxs
where
allIxs = zip occs $ downFrom $ size occs
usedIxs = filter (used . fst) allIxs
used Pos.Unused = False
used _ = True
checkParametersAreGeneral :: ConHead -> Int -> Args -> TCM ()
checkParametersAreGeneral c k vs = do
is <- loop vs
unless (fastDistinct is) $ errorNotGeneral
where
loop [] = return []
loop (v : vs) = case unArg v of
Var i [] | i < k -> (i :) <$> loop vs
_ -> errorNotGeneral
errorNotGeneral :: TCM a
errorNotGeneral = typeError . GenericDocError =<< vcat
[ prettyTCM q <+> text " is not a legal rewrite rule, since the constructor parameters are not fully general:"
, nest 2 $ text "Constructor: " <+> prettyTCM c
, nest 2 $ text "Parameters: " <+> prettyList (map prettyTCM vs)
]
rewriteWith :: Type
-> Term
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith t v rew@(RewriteRule q gamma _ ps rhs b) es = do
traceSDoc "rewriting.rewrite" 50 (sep
[ "{ attempting to rewrite term " <+> prettyTCM (v `applyE` es)
, " having head " <+> prettyTCM v <+> " of type " <+> prettyTCM t
, " with rule " <+> prettyTCM rew
]) $ do
traceSDoc "rewriting.rewrite" 90 (sep
[ "raw: attempting to rewrite term " <+> (text . show) (v `applyE` es)
, " having head " <+> (text . show) v <+> " of type " <+> (text . show) t
, " with rule " <+> (text . show) rew
]) $ do
result <- nonLinMatch gamma (t,v) ps es
case result of
Left block -> traceSDoc "rewriting.rewrite" 50 "}" $
return $ Left $ block $> v `applyE` es
Right sub -> do
let v' = applySubst sub rhs
traceSDoc "rewriting.rewrite" 50 (sep
[ "rewrote " <+> prettyTCM (v `applyE` es)
, " to " <+> prettyTCM v' <+> "}"
]) $ do
return $ Right v'
rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
rewrite block v rules es = do
rewritingAllowed <- optRewriting <$> pragmaOptions
if (rewritingAllowed && not (null rules)) then do
t <- case v of
Def f [] -> defType <$> getConstInfo f
Con c _ [] -> typeOfConst $ conName c
_ -> __IMPOSSIBLE__
loop block t rules =<< instantiateFull' es
else
return $ NoReduction (block $> v `applyE` es)
where
loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
loop block t [] es =
traceSDoc "rewriting.rewrite" 20 (sep
[ "failed to rewrite " <+> prettyTCM (v `applyE` es)
, "blocking tag" <+> text (show block)
]) $ do
return $ NoReduction $ block $> v `applyE` es
loop block t (rew:rews) es
| let n = rewArity rew, length es >= n = do
let (es1, es2) = List.genericSplitAt n es
result <- rewriteWith t v rew es1
case result of
Left (Blocked m u) -> loop (block `mappend` Blocked m ()) t rews es
Left (NotBlocked _ _) -> loop block t rews es
Right w -> return $ YesReduction YesSimplification $ w `applyE` es2
| otherwise = loop (block `mappend` NotBlocked Underapplied ()) t rews es
rewArity :: RewriteRule -> Int
rewArity = length . rewPats