#if __GLASGOW_HASKELL__ <= 708
#endif
module Agda.Syntax.Internal.Pattern where
import Control.Applicative
import Control.Monad.State
import Data.Maybe
import Data.List
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Abstract (IsProjP(..))
import Agda.Syntax.Internal
import qualified Agda.Syntax.Internal as I
import Agda.Utils.Functor
import Agda.Utils.List
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 $ 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
unlabelPatVars :: b -> a
instance LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i where
labelPatVars = traverse labelPatVars
unlabelPatVars = fmap unlabelPatVars
instance LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i where
labelPatVars = traverse labelPatVars
unlabelPatVars = fmap unlabelPatVars
instance LabelPatVars a b i => LabelPatVars [a] [b] i where
labelPatVars = traverse labelPatVars
unlabelPatVars = fmap unlabelPatVars
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
unlabelPatVars = fmap snd
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
numberPatVars perm ps = evalState (labelPatVars ps) $
permPicks $ flipP $ invertP __IMPOSSIBLE__ perm
unnumberPatVars :: LabelPatVars a b i => b -> a
unnumberPatVars = unlabelPatVars
dbPatPerm :: [NamedArg DeBruijnPattern] -> Permutation
dbPatPerm ps = Perm (size ixs) picks
where
ixs = concatMap (getIndices . namedThing . unArg) ps
n = size $ catMaybes ixs
picks = for (downFrom n) $ \i ->
fromMaybe __IMPOSSIBLE__ $ findIndex (Just i ==) ixs
getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP (i,_)) = [Just i]
getIndices (ConP c _ ps) = concatMap (getIndices . namedThing . unArg) ps
getIndices (DotP _) = [Nothing]
getIndices (LitP _) = []
getIndices (ProjP _) = []
clausePerm :: Clause -> Permutation
clausePerm = dbPatPerm . namedClausePats
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim (Arg ai (VarP (i, _))) = Apply $ Arg ai $ var i
patternToElim (Arg ai (ConP c _ ps)) = Apply $ Arg ai $ Con c $
map (argFromElim . patternToElim . fmap namedThing) ps
patternToElim (Arg ai (DotP t) ) = Apply $ Arg ai t
patternToElim (Arg ai (LitP l) ) = Apply $ Arg ai $ Lit l
patternToElim (Arg ai (ProjP dest) ) = Proj $ dest
patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
patternsToElims ps = map build ps
where
build :: NamedArg DeBruijnPattern -> Elim
build = patternToElim . fmap namedThing
patternToTerm :: DeBruijnPattern -> Term
patternToTerm p = case patternToElim (defaultArg p) of
Apply x -> unArg x
Proj f -> __IMPOSSIBLE__