module Agda.Interaction.MakeCase where
import Prelude hiding (mapM, mapM_)
import Control.Applicative
import Control.Monad hiding (mapM, mapM_)
import Control.Monad.State hiding (mapM, mapM_)
import qualified Data.Map as Map
import Data.Traversable
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Scope.Base (emptyScopeInfo)
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Context as Context
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecker
import Agda.Interaction.BasicOps
import Agda.Utils.Size
import Agda.Utils.Permutation
#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 <- Map.elems $ sigDefinitions sig
Function{funClauses = cs} <- [theDef def]
c <- cs
unless (rhsIsm $ clauseBody c) []
return (defName def, c)
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" 20 $ vcat $ map (text . show) (Map.elems $ sigDefinitions sig)
typeError $ GenericError "Right hand side must be a single hole when making a case distinction."
[(n,c)] | isPrefixOf extendlambdaname $ show $ A.qnameName n -> do
Just (h , nh) <- Map.lookup n <$> getExtLambdaTele
return (ExtendedLambda h nh , n , c)
| otherwise -> return (FunctionDef , n , c)
_ -> __IMPOSSIBLE__
where
rhsIsm (Bind b) = rhsIsm $ unAbs b
rhsIsm NoBody = False
rhsIsm (Body e) = case e of
MetaV m' _ -> m == m'
_ -> False
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, clausePats = 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)
]
]
var <- deBruijnIndex =<< parseExprIn hole rng s
z <- splitClauseWithAbs clause var
(case z of
Left err -> typeError . GenericError . show =<< prettyTCM err
Right (Left cl) -> ((:[]) <$> makeAbsurdClause f cl)
Right (Right c) -> (mapM (makeAbstractClause f) c)) >>= (\ x -> return (casectxt , x))
makeAbsurdClause :: QName -> SplitClause -> TCM A.Clause
makeAbsurdClause f (SClause tel perm ps _) = 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
ps <- addCtxTel tel $ normalise ps
inContext [] $ reify $ NamedClause f $ Clause noRange tel perm ps NoBody
makeAbstractClause :: QName -> SplitClause -> TCM A.Clause
makeAbstractClause f cl = do
A.Clause lhs _ _ <- makeAbsurdClause f cl
return $ mkClause lhs
where
mkClause :: A.LHS -> A.Clause
mkClause lhs = A.Clause lhs (A.RHS $ A.QuestionMark info) []
where
info = A.MetaInfo noRange emptyScopeInfo Nothing
deBruijnIndex :: A.Expr -> TCM Nat
deBruijnIndex e = do
(v, _) <-
applyRelevanceToContext Irrelevant $
inferExpr e
case 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.")