{-# 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 Data.Function (on)
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.Telescope
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 :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations c t =
ifM (not . optForcing <$> commandLineOptions)
(return []) $ do
t <- instantiateFull t
TelV tel (El _ a) <- telViewPath 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 for " ++ show c
, " xs = " ++ show (map snd 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 IApply{} = []
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
case rebind of
Nothing -> return ps
Just rebind -> do
reportSDoc "tc.force" 50 $ "forcingTranslation" <?> vcat
[ "patterns:" <?> pretty ps
, "dotted: " <?> pretty qs
, "rebind: " <?> pretty rebind ]
rs <- foldM rebindForcedPattern qs rebind
when (not $ null rebind) $ reportSDoc "tc.force" 50 $ nest 2 $ "result: " <?> pretty rs
forcingTranslation 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 = map (`lookup` mods) $ downFrom $ size delta
delta' = telFromList $ zipWith (maybe id setModality) ms $ telToList delta
reportSDoc "tc.force" 60 $ nest 2 $ "delta' =" <?> prettyTCM delta'
return delta'
rebindForcedPattern :: [NamedArg DeBruijnPattern] -> DeBruijnPattern -> TCM [NamedArg DeBruijnPattern]
rebindForcedPattern ps toRebind = do
reportSDoc "tc.force" 50 $ hsep ["rebinding", pretty toRebind, "in"] <?> pretty ps
ps' <- go $ zip (repeat NotForced) ps
reportSDoc "tc.force" 50 $ nest 2 $ hsep ["result:", pretty ps']
return ps'
where
targetDotP = patternToTerm toRebind
go [] = __IMPOSSIBLE__
go ((Forced, p) : ps) = (p :) <$> go ps
go ((NotForced, p) : ps) | namedArg p `rebinds` toRebind
= return $ p : map snd 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'
DefP o q qs -> do
fs <- defForced <$> getConstInfo q
fqs <- return $ zip (fs ++ repeat NotForced) qs
qps <- go (fqs ++ ps)
let (qs', ps') = splitAt (length qs) qps
return $ fmap (DefP o q qs' <$) p : ps'
LitP{} -> (p :) <$> go ps
ProjP{} -> (p :) <$> go ps
IApplyP{} -> (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
rebinds :: DeBruijnPattern -> DeBruijnPattern -> Bool
VarP{} `rebinds` DotP{} = True
VarP _ x `rebinds` VarP _ y = dbPatVarIndex x == dbPatVarIndex y
DotP _ u `rebinds` DotP _ v = u == v
ConP c _ ps `rebinds` ConP c' _ qs = c == c' && and (zipWith (rebinds `on` namedArg) ps qs)
LitP l `rebinds` LitP l' = l == l'
ProjP _ f `rebinds` ProjP _ g = f == g
IApplyP _ u v x `rebinds` IApplyP _ u' v' y = u == u' && v == v' && x == y
DefP _ f ps `rebinds` DefP _ g qs = f == g && and (zipWith (rebinds `on` namedArg) ps qs)
_ `rebinds` _ = False
dotForcedPatterns :: [NamedArg DeBruijnPattern] -> TCM ([NamedArg DeBruijnPattern], Maybe [DeBruijnPattern])
dotForcedPatterns ps = runWriterT $ (traverse . traverse . traverse) (forced NotForced) ps
where
forced :: IsForced -> DeBruijnPattern -> WriterT (Maybe [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 (Just [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
DefP o q ps -> do
fs <- defForced <$> getConstInfo q
DefP o q <$> zipWithM forcedArg (fs ++ repeat NotForced) ps
IApplyP{} -> return p
forcedArg f = (traverse . traverse) (forced f)
isProperMatch LitP{} = return True
isProperMatch IApplyP{} = return False
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)
isProperMatch DefP{} = return True