{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Forcing where
import Control.Arrow (first, second)
import Control.Monad
import Control.Monad.Trans.Maybe
import Control.Monad.Writer (WriterT(..), tell)
import Data.Foldable hiding (any)
import Data.Traversable
import Data.Semigroup hiding (Arg)
import Data.Maybe
import Data.List ((\\))
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.TypeChecking.Telescope
import Agda.Utils.Function
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
computeForcingAnnotations :: Type -> TCM [IsForced]
computeForcingAnnotations t =
ifM (not . optForcing <$> commandLineOptions)
(return []) $ do
t <- instantiateFull t
TelV tel (El _ a) <- telView t
let vs = case a of
Def _ us -> us
_ -> __IMPOSSIBLE__
n = size tel
xs = forcedVariables vs
isForced m i = getRelevance m /= Irrelevant &&
any (\ (m', j) -> i == j && related m' POLE m) xs
forcedArgs =
[ if isForced m i then Forced else NotForced
| (i, m) <- zip (downFrom n) $ map getModality (telToList tel)
]
reportSLn "tc.force" 60 $ unlines
[ "Forcing analysis"
, " xs = " ++ show xs
, " forcedArgs = " ++ show forcedArgs
]
return forcedArgs
class ForcedVariables a where
forcedVariables :: a -> [(Modality, Nat)]
default forcedVariables :: (ForcedVariables b, Foldable t, a ~ t b) => a -> [(Modality, Nat)]
forcedVariables = foldMap forcedVariables
instance ForcedVariables a => ForcedVariables [a] where
instance ForcedVariables a => ForcedVariables (Elim' a) where
forcedVariables (Apply x) = forcedVariables x
forcedVariables Proj{} = []
instance ForcedVariables a => ForcedVariables (Arg a) where
forcedVariables x = [ (m <> m', i) | (m', i) <- forcedVariables (unArg x) ]
where m = getModality x
instance ForcedVariables Term where
forcedVariables t = case t of
Var i [] -> [(mempty, i)]
Con _ _ vs -> forcedVariables vs
_ -> []
isForced :: IsForced -> Bool
isForced Forced = True
isForced NotForced = False
nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced [] = (NotForced, [])
nextIsForced (f:fs) = (f, fs)
forcingTranslation :: [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
forcingTranslation ps = do
(qs, rebind) <- dotForcedPatterns ps
reportSDoc "tc.force" 50 $ text "forcingTranslation" <?> vcat
[ text "patterns:" <?> pretty ps
, text "dotted: " <?> pretty qs
, text "rebind: " <?> pretty rebind ]
rs <- foldM rebindForcedPattern qs rebind
when (not $ null rebind) $ reportSDoc "tc.force" 50 $ nest 2 $ text "result: " <?> pretty rs
return rs
forceTranslateTelescope :: Telescope -> [NamedArg DeBruijnPattern] -> TCM Telescope
forceTranslateTelescope delta qs = do
qs' <- forcingTranslation qs
let xms = patternVarModalities qs
xms' = patternVarModalities qs'
old = xms \\ xms'
new = xms' \\ xms
if null new then return delta else do
reportSLn "tc.force" 40 $ "Updating modalities of forced arguments\n" ++
" from: " ++ show old ++ "\n" ++
" to: " ++ show new
let mods = map (first dbPatVarIndex) new
ms = reverse [ lookup i mods | i <- [0..size delta - 1] ]
delta' = telFromList $ zipWith (maybe id setModality) ms $ telToList delta
reportSDoc "tc.force" 60 $ nest 2 $ text "delta' =" <?> prettyTCM delta'
return delta'
rebindForcedPattern :: [NamedArg DeBruijnPattern] -> DeBruijnPattern -> TCM [NamedArg DeBruijnPattern]
rebindForcedPattern ps toRebind = go $ zip (repeat NotForced) ps
where
targetDotP = patternToTerm toRebind
go [] = __IMPOSSIBLE__
go ((Forced, p) : ps) = (p :) <$> go ps
go ((NotForced, p) : ps) =
case namedArg p of
VarP{} -> (p :) <$> go ps
DotP _ v -> mkPat v >>= \ case
Nothing -> (p :) <$> go ps
Just q' -> return $ fmap (q' <$) p : map snd ps
ConP c i qs -> do
fqs <- withForced c qs
qps <- go (fqs ++ ps)
let (qs', ps') = splitAt (length qs) qps
return $ fmap (ConP c i qs' <$) p : ps'
LitP{} -> (p :) <$> go ps
ProjP{} -> (p :) <$> go ps
withForced :: ConHead -> [a] -> TCM [(IsForced, a)]
withForced c qs = do
fs <- defForced <$> getConstInfo (conName c)
return $ zip (fs ++ repeat NotForced) qs
mkPat :: Term -> TCM (Maybe DeBruijnPattern)
mkPat v = mkPat' (NotForced, v)
mkPat' :: (IsForced, Term) -> TCM (Maybe DeBruijnPattern)
mkPat' (Forced, _) = return Nothing
mkPat' (NotForced, v) | targetDotP == v = return (Just toRebind)
mkPat' (NotForced, v) =
case v of
Con c co es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
fvs <- withForced c vs
let fvs' = [ (f,) <$> a | (f, a) <- fvs ] :: [Arg (IsForced, Term)]
mps :: [Maybe (Arg DeBruijnPattern)] <- mapM (runMaybeT . traverse (MaybeT . mkPat')) fvs'
case break (isJust . snd) (zip vs mps) of
(mvs1, (_, Just p) : mvs2) -> do
let vs1 = map fst mvs1
vs2 = map fst mvs2
ci = (toConPatternInfo co) { conPLazy = True }
dots = (map . fmap) dotP
return $ Just $ ConP c ci $ doname $ dots vs1 ++ [p] ++ dots vs2
_ -> return Nothing
_ -> return Nothing
where
doname = (map . fmap) unnamed
dotForcedPatterns :: [NamedArg DeBruijnPattern] -> TCM ([NamedArg DeBruijnPattern], [DeBruijnPattern])
dotForcedPatterns ps = runWriterT $ (traverse . traverse . traverse) (forced NotForced) ps
where
forced :: IsForced -> DeBruijnPattern -> WriterT [DeBruijnPattern] TCM DeBruijnPattern
forced f p =
case p of
DotP{} -> return p
ProjP{} -> return p
_ | f == Forced -> do
properMatch <- isProperMatch p
dotP (patternToTerm p) <$ tell [p | properMatch || length p > 0]
VarP{} -> return p
LitP{} -> return p
ConP c i ps -> do
fs <- defForced <$> getConstInfo (conName c)
ConP c i <$> zipWithM forcedArg (fs ++ repeat NotForced) ps
forcedArg f = (traverse . traverse) (forced f)
isProperMatch LitP{} = return True
isProperMatch VarP{} = return False
isProperMatch ProjP{} = return False
isProperMatch DotP{} = return False
isProperMatch (ConP c i ps) =
ifM (isEtaCon $ conName c)
(anyM ps (isProperMatch . namedArg))
(return True)