module Agda.Interaction.MakeCase where
import Prelude hiding (mapM, mapM_, null)
import Control.Applicative hiding (empty)
import Control.Monad hiding (mapM, mapM_, forM)
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.Info as A
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Monad (resolveName, ResolvedName(..))
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.InternalToAbstract
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
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.Functor
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
data CaseContext
= FunctionDef
| ExtendedLambda Int Int
deriving (Eq)
findClause :: MetaId -> TCM (CaseContext, QName, Clause)
findClause m = do
sig <- getImportedSignature
let res = do
def <- HMap.elems $ sigDefinitions sig
Function{funClauses = cs, funExtLam = extlam} <- [theDef def]
c <- cs
unless (rhsIsm $ clauseBody c) []
return (defName def, c, extlam)
case res of
[] -> do
reportSDoc "interaction.case" 10 $ vcat $
[ text "Interaction.MakeCase.findClause fails"
, text "expected rhs to be meta var" <+> (text $ show m)
, text "but could not find it in the signature"
]
reportSDoc "interaction.case" 100 $ vcat $ map (text . show) (HMap.elems $ sigDefinitions sig)
ifM (isInstantiatedMeta m)
(typeError $ GenericError "Since goal is solved, further case distinction is not supported; try `Solve constraints' instead")
(typeError $ GenericError "Right hand side must be a single hole when making a case distinction")
[(n,c, Just (h, nh))] -> return (ExtendedLambda h nh , n , c)
[(n,c, Nothing)] -> return (FunctionDef , n , c)
_ -> __IMPOSSIBLE__
where
rhsIsm (Bind b) = rhsIsm $ unAbs b
rhsIsm NoBody = False
rhsIsm (Body e) = case ignoreSharing e of
MetaV m' _ -> m == m'
_ -> False
parseVariables :: InteractionId -> Range -> [String] -> TCM [Int]
parseVariables 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)
fv <- getModuleFreeVars =<< currentModule
let numSplittableVars = n fv
forM ss $ \ s -> do
let failNotVar = typeError $ GenericError $ "Not a (splittable) variable: " ++ s
done i
| i < numSplittableVars = return i
| otherwise = failNotVar
resName <- resolveName $ C.QName $ C.Name r $ C.stringNameParts s
case resName of
DefinedName{} -> failNotVar
FieldName{} -> failNotVar
ConstructorName{} -> failNotVar
PatternSynResName{} -> failNotVar
VarName x -> do
(v, _) <- getVarInfo x
case ignoreSharing v of
Var i [] -> done i
_ -> failNotVar
UnknownName -> do
case filter ((s ==) . fst) xs of
[] -> typeError $ GenericError $ "Unbound variable " ++ s
[(_,i)] -> done i
_ -> typeError $ GenericError $ "Ambiguous variable " ++ s
makeCase :: InteractionId -> Range -> String -> TCM (CaseContext , [A.Clause])
makeCase hole rng s = withInteractionId hole $ do
meta <- lookupInteractionId hole
(casectxt, f, clause@(Clause{ clauseTel = tel, clausePerm = perm, namedClausePats = ps })) <- findClause meta
reportSDoc "interaction.case" 10 $ vcat
[ text "splitting clause:"
, nest 2 $ vcat
[ text "f =" <+> prettyTCM f
, text "context =" <+> (prettyTCM =<< getContextTelescope)
, text "tel =" <+> prettyTCM tel
, text "perm =" <+> text (show perm)
, text "ps =" <+> text (show ps)
]
]
let vars = words s
if null vars then do
(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 do
res <- splitResult f sc
case res of
Nothing -> typeError $ GenericError $ "Cannot split on result here"
Just cov -> ifNotM (optCopatterns <$> pragmaOptions) failNoCop $ do
mapM (snd <.> fixTarget) $ splitClauses cov
(casectxt,) <$> mapM (makeAbstractClause f) scs
else do
vars <- parseVariables hole rng vars
(casectxt,) <$> do split f vars $ clauseToSplitClause clause
where
failNoCop = typeError $ GenericError $
"OPTION --copatterns needed to split on result here"
split :: QName -> [Nat] -> SplitClause -> TCM [A.Clause]
split f [] clause = singleton <$> makeAbstractClause f clause
split f (var : vars) clause = do
z <- splitClauseWithAbsurd clause var
case z of
Left err -> typeError $ SplitError err
Right (Left cl) -> (:[]) <$> makeAbsurdClause f cl
Right (Right cov)
| null vars -> mapM (makeAbstractClause f) $ splitClauses cov
| otherwise -> concat <$> do
forM (splitClauses cov) $ \ cl ->
split f (mapMaybe (newVar cl) vars) cl
newVar :: SplitClause -> Nat -> Maybe Nat
newVar c x = case ignoreSharing $ applySubst (scSubst c) (var x) of
Var y [] -> Just y
_ -> Nothing
makeAbsurdClause :: QName -> SplitClause -> TCM A.Clause
makeAbsurdClause f (SClause tel perm ps _ t) = do
reportSDoc "interaction.case" 10 $ vcat
[ text "Interaction.MakeCase.makeCase: split clause:"
, nest 2 $ vcat
[ text "context =" <+> (prettyTCM =<< getContextTelescope)
, text "tel =" <+> prettyTCM tel
, text "perm =" <+> text (show perm)
, text "ps =" <+> text (show ps)
]
]
withCurrentModule (qnameModule f) $ do
c <- translateRecordPatterns $ Clause noRange tel perm ps NoBody t
ps <- addCtxTel tel $ normalise $ namedClausePats c
inTopContext $ reify $ QNamed f $ c { namedClausePats = ps }
makeAbstractClause :: QName -> SplitClause -> TCM A.Clause
makeAbstractClause f cl = do
A.Clause lhs _ _ <- makeAbsurdClause f cl
let ii = __IMPOSSIBLE__
let info = A.emptyMetaInfo
return $ A.Clause lhs (A.RHS $ A.QuestionMark info ii) []
deBruijnIndex :: A.Expr -> TCM Nat
deBruijnIndex e = do
(v, _) <-
applyRelevanceToContext Irrelevant $
inferExpr e
case ignoreSharing v of
Var n _ -> return n
_ -> typeError . GenericError . show =<< (fsep $
pwords "The scrutinee of a case distinction must be a variable,"
++ [ prettyTCM v ] ++ pwords "isn't.")