{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Interaction.MakeCase where
import Prelude hiding (mapM, mapM_, null)
import Control.Monad hiding (mapM, mapM_, forM)
import Data.Either
import qualified Data.Map as Map
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Traversable (mapM, forM)
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.Syntax.Concrete (NameInScope(..))
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Pattern as C
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Pattern as A
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base ( ResolvedName(..), BindingSource(..), KindOfName(..), exceptKindsOfNames )
import Agda.Syntax.Scope.Monad ( resolveName' )
import Agda.Syntax.Translation.InternalToAbstract
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( SplitPatVar(..) , SplitPattern , applySplitPSubst , fromSplitPatterns )
import Agda.TypeChecking.Empty ( isEmptyTel )
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def (checkClauseLHS)
import Agda.TypeChecking.Rules.LHS (LHSResult(..))
import Agda.TypeChecking.Rules.Term (isModuleFreeVar)
import Agda.Interaction.Options
import Agda.Interaction.BasicOps
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
type CaseContext = Maybe ExtLamInfo
parseVariables
:: QName
-> Telescope
-> InteractionId
-> Range
-> [String]
-> TCM [(Int,NameInScope)]
parseVariables f tel ii rng ss = do
mId <- lookupInteractionId ii
updateMetaVarRange mId rng
mi <- getMetaInfo <$> lookupMeta mId
enterClosure mi $ \ r -> do
n <- getContextSize
xs <- forM (downFrom n) $ \ i -> do
(,i) . P.render <$> prettyTCM (var i)
let nPatVars = size tel
let nlocals = n - nPatVars
unless (nlocals >= 0) __IMPOSSIBLE__
fv <- getDefFreeVars f
reportSDoc "interaction.case" 20 $ do
m <- currentModule
tel <- lookupSection m
cxt <- getContextTelescope
vcat
[ "parseVariables:"
, "current module =" <+> prettyTCM m
, "current section =" <+> inTopContext (prettyTCM tel)
, text $ "function's fvs = " ++ show fv
, text $ "number of locals= " ++ show nlocals
, "context =" <+> do inTopContext $ prettyTCM cxt
, "checkpoints =" <+> do (text . show) =<< asksTC envCheckpoints
]
forM ss $ \ s -> do
let failNotVar = typeError $ GenericError $ "Not a variable: " ++ s
failUnbound = typeError $ GenericError $ "Unbound variable " ++ s
failAmbiguous = typeError $ GenericError $ "Ambiguous variable " ++ s
failLocal = typeError $ GenericError $
"Cannot split on local variable " ++ s
failModuleBound = typeError $ GenericError $
"Cannot split on module parameter " ++ s
failLetBound v = typeError . GenericError $
"Cannot split on let-bound variable " ++ s
failInstantiatedVar v = typeError . GenericDocError =<< sep
[ text $ "Cannot split on variable " ++ s ++ ", because it is bound to"
, prettyTCM v
]
failCaseLet = typeError $ GenericError $
"Cannot split on variable " ++ s ++
", because let-declarations may not be defined by pattern-matching"
let cname = C.QName $ C.Name r C.InScope $ C.stringNameParts s
resolveName' (exceptKindsOfNames [GeneralizeName]) Nothing cname >>= \case
DefinedName{} -> failNotVar
FieldName{} -> failNotVar
ConstructorName{} -> failNotVar
PatternSynResName{} -> failNotVar
VarName x b -> do
(v, _) <- getVarInfo x
case (v , b) of
(Var i [] , PatternBound) -> do
reportSLn "interaction.case" 30 $ "resolved variable " ++ show x ++ " = " ++ show i
when (i < nlocals) failCaseLet
return (i - nlocals , C.InScope)
(Var i [] , LambdaBound)
| i < nlocals -> failLocal
| otherwise -> failModuleBound
(Var i [] , LetBound) -> failLetBound v
(_ , _ ) -> failInstantiatedVar v
UnknownName -> do
let xs' = filter ((s ==) . fst) xs
when (null xs') $ failUnbound
reportSLn "interaction.case" 20 $ "matching names corresponding to indices " ++ show xs'
let xs'' = mapMaybe (\ (_,i) -> if i < nlocals then Nothing else Just $ i - nlocals) xs'
when (null xs'') $ typeError $ GenericError $
"Cannot make hidden lambda-bound variable " ++ s ++ " visible"
params <- moduleParamsToApply $ qnameModule f
let isParam i = any ((== var i) . unArg) params
xs''' = filter (not . isParam) xs''
when (null xs''') $ typeError $ GenericError $
"Cannot make hidden module parameter " ++ s ++ " visible"
case xs''' of
[] -> failModuleBound
[i] -> return (i , C.NotInScope)
_ -> failAmbiguous
type ClauseZipper =
( [Clause]
, Clause
, [Clause]
)
getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP f clauseNo = do
(theDef <$> getConstInfo f) >>= \case
Function{funClauses = cs, funExtLam = extlam} -> do
let (cs1,ccs2) = fromMaybe __IMPOSSIBLE__ $ splitExactlyAt clauseNo cs
(c,cs2) = fromMaybe __IMPOSSIBLE__ $ uncons ccs2
return (extlam, (cs1, c, cs2))
d -> do
reportSDoc "impossible" 10 $ vcat
[ "getClauseZipperForIP" <+> prettyTCM f <+> text (show clauseNo)
<+> "received"
, text (show d)
]
__IMPOSSIBLE__
recheckAbstractClause :: Type -> Maybe Substitution -> A.SpineClause -> TCM Clause
recheckAbstractClause t sub cl = checkClauseLHS t sub cl $ \ lhs ->
return Clause{ clauseLHSRange = getRange cl
, clauseFullRange = getRange cl
, clauseTel = lhsVarTele lhs
, namedClausePats = lhsPatterns lhs
, clauseBody = Nothing
, clauseType = Just (lhsBodyType lhs)
, clauseCatchall = False
, clauseRecursive = Nothing
, clauseUnreachable = Nothing
, clauseEllipsis = lhsEllipsis $ A.spLhsInfo $ A.clauseLHS cl
}
makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [A.Clause])
makeCase hole rng s = withInteractionId hole $ locallyTC eMakeCase (const True) $ do
localTC (\ e -> e { envPrintMetasBare = True }) $ do
InteractionPoint { ipMeta = mm, ipClause = ipCl} <- lookupInteractionPoint hole
let meta = fromMaybe __IMPOSSIBLE__ mm
(f, clauseNo, clTy, clWithSub, absCl@A.Clause{ clauseRHS = rhs }, clClos) <- case ipCl of
IPClause f i t sub cl clo _ -> return (f, i, t, sub, cl, clo)
IPNoClause -> typeError $ GenericError $
"Cannot split here, as we are not in a function definition"
(casectxt, (prevClauses0, _clause, follClauses0)) <- getClauseZipperForIP f clauseNo
clause <- enterClosure clClos $ \ _ -> locallyTC eMakeCase (const True) $
recheckAbstractClause clTy clWithSub absCl
let (prevClauses, follClauses) = killRange (prevClauses0, follClauses0)
let perm = fromMaybe __IMPOSSIBLE__ $ clausePerm clause
tel = clauseTel clause
ps = namedClausePats clause
ell = clauseEllipsis clause
reportSDoc "interaction.case" 10 $ vcat
[ "splitting clause:"
, nest 2 $ vcat
[ "f =" <+> prettyTCM f
, "context =" <+> ((inTopContext . prettyTCM) =<< getContextTelescope)
, "tel =" <+> (inTopContext . prettyTCM) tel
, "perm =" <+> text (show perm)
, "ps =" <+> prettyTCMPatternList ps
, "ell =" <+> text (show ell)
]
]
reportSDoc "interaction.case" 60 $ vcat
[ "splitting clause:"
, nest 2 $ vcat
[ "f =" <+> (text . show) f
, "context =" <+> ((inTopContext . (text . show)) =<< getContextTelescope)
, "tel =" <+> (text . show) tel
, "perm =" <+> text (show perm)
, "ps =" <+> (text . show) ps
]
]
let vars = words s
if concat vars == "." then do
cl <- makeAbstractClause f rhs NoEllipsis $ clauseToSplitClause clause
return (f, casectxt, [cl])
else if null vars then do
let postProjInExtLam = applyWhen (isJust casectxt) $
withPragmaOptions $ \ opt -> opt { optPostfixProjections = True }
(piTel, sc) <- insertTrailingArgs $ clauseToSplitClause clause
newPats <- if null piTel then return False else do
imp <- optShowImplicit <$> pragmaOptions
return $ imp || any visible (telToList piTel)
scs <- if newPats then return [sc] else postProjInExtLam $ do
res <- splitResult f sc
case res of
Left err -> do
let trailingPatVars :: [NamedArg DBPatVar]
trailingPatVars = takeWhileJust isVarP $ reverse ps
isVarP (Arg ai (Named n (VarP _ x))) = Just $ Arg ai $ Named n x
isVarP _ = Nothing
when (all ((UserWritten ==) . getOrigin) trailingPatVars) $ do
typeError $ SplitError err
let xs = map (dbPatVarIndex . namedArg) trailingPatVars
return [makePatternVarsVisible xs sc]
Right cov -> ifNotM (optCopatterns <$> pragmaOptions) failNoCop $ do
return cov
checkClauseIsClean ipCl
(f, casectxt,) <$> mapM (makeAbstractClause f rhs ell) scs
else do
xs <- parseVariables f tel hole rng vars
reportSLn "interaction.case" 30 $ "parsedVariables: " ++ show (zip xs vars)
let (toShow, toSplit) = partitionEithers $ for (zip xs vars) $ \ ((x,nis), s) ->
if (nis == C.NotInScope) then Left x else Right x
let sc = makePatternVarsVisible toShow $ clauseToSplitClause clause
scs <- split f toSplit sc
reportSLn "interaction.case" 70 $ "makeCase: survived the splitting"
splitNames <- mapM nameOfBV toSplit
shouldExpandEllipsis <- return (not $ null toShow) `or2M` anyEllipsisVar f absCl splitNames
let ell' | shouldExpandEllipsis = NoEllipsis
| otherwise = ell
let sclause = clauseToSplitClause clause
fcs <- filterM (\ cl -> (isCovered f [clause] (clauseToSplitClause cl)) `and2M`
(not <$> isCovered f [cl] sclause))
follClauses
scs <- filterM (not <.> isCovered f (prevClauses ++ fcs) . fst) scs
reportSLn "interaction.case" 70 $ "makeCase: survived filtering out already covered clauses"
cs <- catMaybes <$> do
forM scs $ \ (sc, isAbsurd) -> if isAbsurd
then Just <$> makeAbsurdClause f ell' sc
else
ifM (liftTCM $ isEmptyTel (scTel sc))
(pure Nothing)
(Just <$> makeAbstractClause f rhs ell' sc)
reportSLn "interaction.case" 70 $ "makeCase: survived filtering out impossible clauses"
cs <- if not (null cs) then pure cs
else mapM (makeAbstractClause f rhs ell' . fst) scs
reportSDoc "interaction.case" 65 $ vcat
[ "split result:"
, nest 2 $ vcat $ map prettyA cs
]
checkClauseIsClean ipCl
return (f, casectxt, cs)
where
failNoCop = typeError $ GenericError $
"OPTION --copatterns needed to split on result here"
split :: QName -> [Nat] -> SplitClause -> TCM [(SplitClause, Bool)]
split f [] clause = return [(clause,False)]
split f (var : vars) clause = do
z <- dontAssignMetas $ splitClauseWithAbsurd clause var
case z of
Left err -> typeError $ SplitError err
Right (Left cl) -> return [(cl,True)]
Right (Right cov) -> concat <$> do
forM (splitClauses cov) $ \ cl ->
split f (mapMaybe (newVar cl) vars) cl
newVar :: SplitClause -> Nat -> Maybe Nat
newVar c x = case applySplitPSubst (scSubst c) (var x) of
Var y [] -> Just y
_ -> Nothing
checkClauseIsClean :: IPClause -> TCM ()
checkClauseIsClean ipCl = do
sips <- filter ipSolved . Map.elems <$> useTC stInteractionPoints
when (List.any ((== ipCl) . ipClause) sips) $
typeError $ GenericError $ "Cannot split as clause rhs has been refined. Please reload"
makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause
makePatternVarsVisible [] sc = sc
makePatternVarsVisible is sc@SClause{ scPats = ps } =
sc{ scPats = mapNamedArgPattern mkVis ps }
where
mkVis :: NamedArg SplitPattern -> NamedArg SplitPattern
mkVis (Arg ai (Named n (VarP o (SplitPatVar x i ls))))
| i `elem` is =
Arg (setOrigin CaseSplit ai) $ Named n $ VarP (PatternInfo PatOSplit []) $ SplitPatVar x i ls
mkVis np = np
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbsurdClause f ell (SClause tel sps _ _ t) = do
let ps = fromSplitPatterns sps
reportSDoc "interaction.case" 10 $ vcat
[ "Interaction.MakeCase.makeAbsurdClause: split clause:"
, nest 2 $ vcat
[ "context =" <+> do (inTopContext . prettyTCM) =<< getContextTelescope
, "tel =" <+> do inTopContext $ prettyTCM tel
, "ps =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps
, "ell =" <+> text (show ell)
]
]
withCurrentModule (qnameModule f) $ do
let c = Clause noRange noRange tel ps Nothing (argFromDom <$> t) False Nothing Nothing ell
ps <- addContext tel $ normalise $ namedClausePats c
reportSDoc "interaction.case" 60 $ "normalized patterns: " <+> prettyTCMPatternList ps
inTopContext $ reify $ QNamed f $ c { namedClausePats = ps }
makeAbstractClause :: QName -> A.RHS -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbstractClause f rhs ell cl = do
lhs <- A.clauseLHS <$> makeAbsurdClause f ell cl
reportSDoc "interaction.case" 60 $ "reified lhs: " <+> prettyA lhs
return $ A.Clause lhs [] rhs A.noWhereDecls False
anyEllipsisVar :: QName -> A.SpineClause -> [Name] -> TCM Bool
anyEllipsisVar f cl xs = do
let lhs = A.clauseLHS cl
ps = A.spLhsPats lhs
ell = lhsEllipsis $ A.spLhsInfo lhs
anyVar :: A.Pattern -> Any -> Any
anyVar p acc = Any $ getAny acc || case p of
A.VarP x -> A.unBind x `elem` xs
_ -> False
case ell of
NoEllipsis -> return False
ExpandedEllipsis _ k -> do
ps' <- snd <$> reifyDisplayFormP f ps []
let ellipsisPats :: A.Patterns
ellipsisPats = fst $ C.splitEllipsis k ps'
reportSDoc "interaction.case.ellipsis" 40 $ vcat
[ "should we expand the ellipsis?"
, nest 2 $ "xs =" <+> prettyList_ (map prettyA xs)
, nest 2 $ "ellipsisPats =" <+> prettyList_ (map prettyA ellipsisPats)
]
return $ getAny $ A.foldrAPattern anyVar ellipsisPats