module Agda.Syntax.Internal.Pattern where
import Control.Applicative
import Control.Monad.State
import Data.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Common as Common hiding (NamedArg)
import Agda.Syntax.Abstract (IsProjP(..))
import Agda.Syntax.Internal hiding (Arg)
import qualified Agda.Syntax.Internal as I
import Agda.Utils.List
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Permutation
import Agda.Utils.Size (size)
import Agda.Utils.Tuple
#include "../../undefined.h"
import Agda.Utils.Impossible
clauseArgs :: Clause -> Args
clauseArgs cl = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ clauseElims cl
clauseElims :: Clause -> Elims
clauseElims cl = patternsToElims (clausePerm cl) (namedClausePats cl)
class FunArity a where
funArity :: a -> Int
instance IsProjP p => FunArity [p] where
funArity = length . takeWhile (isNothing . isProjP)
instance FunArity Clause where
funArity = funArity . clausePats
instance FunArity [Clause] where
funArity [] = 0
funArity cls = minimum $ map funArity cls
instance IsProjP Pattern where
isProjP (ProjP d) = Just d
isProjP _ = Nothing
patternsToElims :: Permutation -> [I.NamedArg Pattern] -> [Elim]
patternsToElims perm ps = evalState (mapM build' ps) xs
where
xs = permute (invertP perm) $ downFrom (size perm)
tick :: State [Int] Int
tick = do x : xs <- get; put xs; return x
build' :: NamedArg Pattern -> State [Int] Elim
build' = build . fmap namedThing
build :: I.Arg Pattern -> State [Int] Elim
build (Arg ai (VarP _) ) = Apply . Arg ai . var <$> tick
build (Arg ai (ConP c _ ps)) =
Apply . Arg ai . Con c <$> mapM (argFromElim <.> build') ps
build (Arg ai (DotP t) ) = Apply (Arg ai t) <$ tick
build (Arg ai (LitP l) ) = return $ Apply $ Arg ai $ Lit l
build (Arg ai (ProjP dest) ) = return $ Proj $ dest
data OneHolePatterns = OHPats [NamedArg Pattern]
(NamedArg OneHolePattern)
[NamedArg Pattern]
deriving (Show)
data OneHolePattern = Hole
| OHCon ConHead ConPatternInfo OneHolePatterns
deriving (Show)
plugHole :: Pattern -> OneHolePatterns -> [NamedArg Pattern]
plugHole p (OHPats ps hole qs) = ps ++ [fmap (plug p <$>) hole] ++ qs
where
plug p Hole = p
plug p (OHCon c mt h) = ConP c mt $ plugHole p h
allHoles :: [NamedArg Pattern] -> [OneHolePatterns]
allHoles = map snd . allHolesWithContents
allHolesWithContents :: [NamedArg Pattern] -> [(Pattern, OneHolePatterns)]
allHolesWithContents [] = []
allHolesWithContents (p : ps) = map left phs ++ map (right p) (allHolesWithContents ps)
where
phs :: [(Pattern, NamedArg OneHolePattern)]
phs = map (id -*- \h -> fmap (h <$) p)
(holes $ namedArg p)
holes :: Pattern -> [(Pattern, OneHolePattern)]
holes p@(VarP _) = [(p, Hole)]
holes p@(DotP _) = [(p, Hole)]
holes (ConP c mt qs) = map (id -*- OHCon c mt) $ allHolesWithContents qs
holes LitP{} = []
holes ProjP{} = []
left (p, ph) = (p, OHPats [] ph ps)
right q (p, OHPats ps h qs) = (p, OHPats (q : ps) h qs)