module Agda.TypeChecking.Patterns.Abstract where
import Data.List
import Data.Traversable hiding (mapM, sequence)
import Data.Void
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Concrete (FieldAssignment')
import Agda.Syntax.Common
import Agda.Syntax.Info as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.Functor
#include "undefined.h"
import Agda.Utils.Impossible
expandLitPattern :: NamedArg A.Pattern -> TCM (NamedArg A.Pattern)
expandLitPattern p = traverse (traverse expand) p
where
expand p = case asView p of
(xs, A.LitP (LitNat 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 ConPCon 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 (Arg a) where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) where
expandPatternSynonyms = traverse expandPatternSynonyms
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' 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.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.RecP i as -> A.RecP i <$> expandPatternSynonyms as
A.PatternSynP i x as -> setCurrentRange i $ do
p <- killRange <$> lookupPatternSyn x
instPatternSyn p =<< expandPatternSynonyms as
where
instPatternSyn :: A.PatternSynDefn -> [NamedArg A.Pattern] -> TCM A.Pattern
instPatternSyn (ns, p) as = do
p <- expandPatternSynonyms (vacuous p)
case A.insertImplicitPatSynArgs (A.WildP . PatRange) (getRange x) ns as of
Nothing -> typeError $ BadArgumentsToPatternSynonym x
Just (_, _:_) -> typeError $ TooFewArgumentsToPatternSynonym x
Just (s, []) -> return $ setRange (getRange i) $ A.substPattern s p