{-# LANGUAGE CPP #-}
module Agda.Interaction.MakeCase where
import Prelude hiding (mapM, mapM_, null)
import Control.Applicative hiding (empty)
import Control.Monad hiding (mapM, mapM_, forM)
import qualified Data.Map as Map
import qualified Data.List as List
import Data.Maybe
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base ( ResolvedName(..), Binder(..) )
import Agda.Syntax.Scope.Monad ( resolveName )
import Agda.Syntax.Translation.ConcreteToAbstract
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.Pretty
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TheTypeChecker
import Agda.Interaction.Options
import Agda.Interaction.BasicOps
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.HashMap as HMap
#include "undefined.h"
import Agda.Utils.Impossible
type CaseContext = Maybe ExtLamInfo
parseVariables
:: QName
-> Telescope
-> InteractionId
-> Range
-> [String]
-> TCM [Int]
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 nlocals = n - size tel
unless (nlocals >= 0) __IMPOSSIBLE__
reportSDoc "interaction.case" 20 $ do
m <- currentModule
tel <- lookupSection m
fv <- getDefFreeVars f
vcat
[ text "parseVariables:"
, text "current module =" <+> prettyTCM m
, text "current section =" <+> inTopContext (prettyTCM tel)
, text $ "function's fvs = " ++ show fv
, text $ "number of locals= " ++ show nlocals
]
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
]
resName <- resolveName $ C.QName $ C.Name r $ C.stringNameParts s
case resName of
DefinedName{} -> failNotVar
FieldName{} -> failNotVar
ConstructorName{} -> failNotVar
PatternSynResName{} -> failNotVar
VarName x b -> do
(v, _) <- getVarInfo x
case (v , b) of
(Var i [] , PatternBound) -> do
when (i < nlocals) __IMPOSSIBLE__
return $ i - nlocals
(Var i [] , LambdaBound)
| i < nlocals -> failLocal
| otherwise -> failModuleBound
(Var i [] , LetBound) -> failLetBound v
(_ , _ ) -> failInstantiatedVar v
UnknownName -> do
case filter ((s ==) . fst) xs of
[] -> failUnbound
[(_,i)] | i < nlocals -> failLocal
| otherwise -> return $ i - nlocals
_ -> failAmbiguous
getClauseForIP :: QName -> Int -> TCM (CaseContext, Clause, [Clause])
getClauseForIP f clauseNo = do
(theDef <$> getConstInfo f) >>= \case
Function{funClauses = cs, funExtLam = extlam} -> do
let (cs1,cs2) = fromMaybe __IMPOSSIBLE__ $ splitExactlyAt clauseNo cs
c = fromMaybe __IMPOSSIBLE__ $ headMaybe cs2
return (extlam, c, cs1)
d -> do
reportSDoc "impossible" 10 $ vcat
[ text "getClauseForIP" <+> prettyTCM f <+> text (show clauseNo)
<+> text "received"
, text (show d)
]
__IMPOSSIBLE__
makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [A.Clause])
makeCase hole rng s = withInteractionId hole $ do
InteractionPoint { ipMeta = mm, ipClause = ipCl} <- lookupInteractionPoint hole
let meta = fromMaybe __IMPOSSIBLE__ mm
(f, clauseNo, rhs) <- case ipCl of
IPClause f clauseNo rhs-> return (f, clauseNo, rhs)
IPNoClause -> typeError $ GenericError $
"Cannot split here, as we are not in a function definition"
(casectxt, clause, prevClauses) <- getClauseForIP f clauseNo
let perm = fromMaybe __IMPOSSIBLE__ $ clausePerm clause
tel = clauseTel clause
ps = namedClausePats clause
reportSDoc "interaction.case" 10 $ vcat
[ text "splitting clause:"
, nest 2 $ vcat
[ text "f =" <+> prettyTCM f
, text "context =" <+> ((inTopContext . prettyTCM) =<< getContextTelescope)
, text "tel =" <+> (inTopContext . prettyTCM) tel
, text "perm =" <+> text (show perm)
, text "ps =" <+> text (show ps)
]
]
let vars = words s
if concat vars == "." then do
cl <- makeAbstractClause f rhs $ clauseToSplitClause clause
return (f, casectxt, [cl])
else if null vars then do
let postProjInExtLam = applyWhen (isJust casectxt) $
withPragmaOptions $ \ opt -> opt { optPostfixProjections = True }
(piTel, sc) <- fixTarget $ 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 . GenericDocError =<< do
text "Cannot split on result here, because" <+> prettyTCM err
let xs = map (dbPatVarIndex . namedArg) trailingPatVars
return [makePatternVarsVisible xs sc]
Right cov -> ifNotM (optCopatterns <$> pragmaOptions) failNoCop $ do
return $ splitClauses cov
checkClauseIsClean ipCl
(f, casectxt,) <$> mapM (makeAbstractClause f rhs) scs
else do
xs <- parseVariables f tel hole rng vars
let (toShow, toSplit) = flip mapEither (zip xs vars) $ \ (x, s) ->
if take 1 s == "." then Left x else Right x
let sc = makePatternVarsVisible toShow $ clauseToSplitClause clause
scs <- split f toSplit sc
scs <- filterM (not <.> isCovered f prevClauses . fst) scs
cs <- forM scs $ \(sc, isAbsurd) -> do
if isAbsurd then makeAbsurdClause f sc else makeAbstractClause f rhs sc
reportSDoc "interaction.case" 65 $ vcat
[ text "split result:"
, nest 2 $ vcat $ map (text . show . A.deepUnscope) 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 <$> use 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 PatOSplit $ SplitPatVar x i ls
mkVis np = np
makeAbsurdClause :: QName -> SplitClause -> TCM A.Clause
makeAbsurdClause f (SClause tel sps _ _ t) = do
let ps = fromSplitPatterns sps
reportSDoc "interaction.case" 10 $ vcat
[ text "Interaction.MakeCase.makeAbsurdClause: split clause:"
, nest 2 $ vcat
[ text "context =" <+> do (inTopContext . prettyTCM) =<< getContextTelescope
, text "tel =" <+> do inTopContext $ prettyTCM tel
, text "ps =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps
]
]
withCurrentModule (qnameModule f) $ do
let c = Clause noRange noRange tel ps Nothing t False Nothing
ps <- addContext tel $ normalise $ namedClausePats c
reportSDoc "interaction.case" 60 $ text "normalized patterns: " <+> text (show ps)
inTopContext $ reify $ QNamed f $ c { namedClausePats = ps }
makeAbstractClause :: QName -> A.RHS -> SplitClause -> TCM A.Clause
makeAbstractClause f rhs cl = do
lhs <- A.clauseLHS <$> makeAbsurdClause f cl
reportSDoc "interaction.case" 60 $ text "reified lhs: " <+> text (show lhs)
return $ A.Clause lhs [] rhs A.noWhereDecls False