module Agda.TypeChecking.Patterns.Abstract where
import Data.List
import Data.Traversable hiding (mapM, sequence)
import Agda.Syntax.Common as Common
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Info as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.Functor
#include "../../undefined.h"
import Agda.Utils.Impossible
expandLitPattern :: A.NamedArg A.Pattern -> TCM (A.NamedArg A.Pattern)
expandLitPattern p = traverse (traverse expand) p
where
expand p = case asView p of
(xs, A.LitP (LitInt r n))
| n < 0 -> __IMPOSSIBLE__
| n > 20 -> tooBig
| otherwise -> do
Con z _ <- ignoreSharing <$> primZero
Con s _ <- ignoreSharing <$> primSuc
let zero = A.ConP cinfo (A.AmbQ [setRange r $ conName z]) []
suc p = A.ConP cinfo (A.AmbQ [setRange r $ conName s]) [defaultNamedArg p]
info = A.PatRange r
cinfo = A.ConPatInfo False info
p' = foldr ($) zero $ genericReplicate n suc
return $ foldr (A.AsP info) p' xs
_ -> return p
tooBig = typeError $ GenericError $
"Matching on natural number literals is done by expanding " ++
"the literal to the corresponding constructor pattern, so " ++
"you probably don't want to do it this way."
class ExpandPatternSynonyms a where
expandPatternSynonyms :: a -> TCM a
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a) where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms a => ExpandPatternSynonyms [a] where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Common.Arg c a) where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms A.Pattern where
expandPatternSynonyms p =
case p of
A.VarP{} -> return p
A.WildP{} -> return p
A.DotP{} -> return p
A.ImplicitP{} -> return p
A.LitP{} -> return p
A.AbsurdP{} -> return p
A.ConP i ds as -> A.ConP i ds <$> expandPatternSynonyms as
A.DefP i q as -> A.DefP i q <$> expandPatternSynonyms as
A.AsP i x p -> A.AsP i x <$> expandPatternSynonyms p
A.PatternSynP i x as -> setCurrentRange (getRange i) $ do
p <- killRange <$> lookupPatternSyn x
instPatternSyn p =<< expandPatternSynonyms as
where
instPatternSyn :: A.PatternSynDefn -> [A.NamedArg A.Pattern] -> TCM A.Pattern
instPatternSyn (ns, p) as = do
p <- expandPatternSynonyms p
case A.insertImplicitPatSynArgs (A.ImplicitP . PatRange) (getRange x) ns as of
Nothing -> typeError $ GenericError $ "Bad arguments to pattern synonym " ++ show x
Just (_, _:_) -> typeError $ GenericError $ "Too few arguments to pattern synonym " ++ show x
Just (s, []) -> return $ setRange (getRange i) $ A.substPattern s p