#if __GLASGOW_HASKELL__ <= 708
#endif
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
#if __GLASGOW_HASKELL__ >= 710
instance IsProjP p => FunArity [p] where
#else
instance IsProjP p => FunArity [p] where
#endif
funArity = length . takeWhile (isNothing . isProjP)
instance FunArity Clause where
funArity = funArity . clausePats
#if __GLASGOW_HASKELL__ >= 710
instance FunArity [Clause] where
#else
instance FunArity [Clause] where
#endif
funArity [] = 0
funArity cls = minimum $ map funArity cls
class LabelPatVars a b i | b -> i where
labelPatVars :: a -> State [i] b
instance LabelPatVars a b i => LabelPatVars (Arg c a) (Arg c b) i where
labelPatVars = traverse labelPatVars
instance LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i where
labelPatVars = traverse labelPatVars
instance LabelPatVars a b i => LabelPatVars [a] [b] i where
labelPatVars = traverse labelPatVars
instance LabelPatVars (Pattern' x) (Pattern' (i,x)) i where
labelPatVars p =
case p of
VarP x -> VarP . (,x) <$> next
DotP t -> DotP t <$ next
ConP c mt ps -> ConP c mt <$> labelPatVars ps
LitP l -> return $ LitP l
ProjP q -> return $ ProjP q
where next = do (x:xs) <- get; put xs; return x
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
numberPatVars perm ps = evalState (labelPatVars ps) $
permPicks $ flipP $ invertP __IMPOSSIBLE__ perm
patternsToElims :: Permutation -> [I.NamedArg Pattern] -> [Elim]
patternsToElims perm ps = map build' $ numberPatVars perm ps
where
build' :: NamedArg (Pattern' (Int, PatVarName)) -> Elim
build' = build . fmap namedThing
build :: I.Arg (Pattern' (Int, PatVarName)) -> Elim
build (Arg ai (VarP (i, _))) = Apply $ Arg ai $ var i
build (Arg ai (ConP c _ ps)) = Apply $ Arg ai $ Con c $
map (argFromElim . build') ps
build (Arg ai (DotP t) ) = Apply $ Arg ai t
build (Arg ai (LitP l) ) = Apply $ Arg ai $ Lit l
build (Arg ai (ProjP dest) ) = 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)