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 Agda.TypeChecking.Coverage
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecker
import Agda.Interaction.BasicOps
import Agda.Utils.Size
import Agda.Utils.Permutation
#include "../undefined.h"
import Agda.Utils.Impossible
findClause :: MetaId -> TCM (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
[] -> typeError $ GenericError "Right hand side must be a single hole when making a case distinction."
[r] -> return r
_ -> __IMPOSSIBLE__
where
rhsIsm (Bind b) = rhsIsm $ absBody b
rhsIsm (NoBind b) = rhsIsm b
rhsIsm NoBody = False
rhsIsm (Body e) = case e of
MetaV m' _ -> m == m'
_ -> False
makeCase :: InteractionId -> Range -> String -> TCM [A.Clause]
makeCase hole rng s = withInteractionId hole $ do
meta <- lookupInteractionId hole
(f, clause@(Clause{ clauseTel = tel, clausePerm = perm, clausePats = ps })) <- findClause meta
reportSDoc "interaction.case" 10 $ vcat
[ text "splitting clause:"
, nest 2 $ vcat
[ 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 =<< prettySplitError err
Right (Left cl) -> (:[]) <$> makeAbsurdClause f cl
Right (Right c) -> mapM (makeAbstractClause f) c
prettySplitError :: SplitError -> TCM Doc
prettySplitError err = case err of
NotADatatype t -> fsep $
pwords "Cannot pattern match on non-datatype" ++ [prettyTCM t]
CantSplit c tel cIxs gIxs flex -> addCtxTel tel $ vcat
[ fsep $ pwords "Cannot pattern match on constructor" ++ [prettyTCM c <> text ","] ++
pwords "since the inferred indices"
, nest 2 $ prettyTCM cIxs
, fsep $ pwords "cannot be unified with the expected indices"
, nest 2 $ prettyTCM gIxs
, fsep $ pwords "for some" ++ punctuate comma (map prettyTCM flex)
]
GenericSplitError s -> fsep $
pwords "Split failed:" ++ pwords s
makeAbsurdClause :: QName -> SplitClause -> TCM A.Clause
makeAbsurdClause f (SClause tel perm ps _) = do
reportSDoc "interaction.case" 10 $ vcat
[ text "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, _) <- 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.")