{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Syntax.Internal.Pattern where
import Control.Arrow ( second )
import Control.Monad ( (>=>), forM )
import Control.Monad.State ( MonadState(..), State, evalState )
import Data.Maybe
import Data.Monoid
import qualified Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size (size)
import Agda.Utils.Impossible
clauseArgs :: Clause -> Args
clauseArgs :: Clause -> Args
clauseArgs Clause
cl = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims ([Elim' Term] -> Maybe Args) -> [Elim' Term] -> Maybe Args
forall a b. (a -> b) -> a -> b
$ Clause -> [Elim' Term]
clauseElims Clause
cl
clauseElims :: Clause -> Elims
clauseElims :: Clause -> [Elim' Term]
clauseElims Clause
cl = [NamedArg DeBruijnPattern] -> [Elim' Term]
patternsToElims ([NamedArg DeBruijnPattern] -> [Elim' Term])
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
class FunArity a where
funArity :: a -> Int
instance {-# OVERLAPPABLE #-} IsProjP p => FunArity [p] where
funArity :: [p] -> Int
funArity = [p] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([p] -> Int) -> ([p] -> [p]) -> [p] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p -> Bool) -> [p] -> [p]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
-> (p -> Maybe (ProjOrigin, AmbiguousQName)) -> p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP)
instance FunArity Clause where
funArity :: Clause -> Int
funArity = [NamedArg DeBruijnPattern] -> Int
forall a. FunArity a => a -> Int
funArity ([NamedArg DeBruijnPattern] -> Int)
-> (Clause -> [NamedArg DeBruijnPattern]) -> Clause -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats
instance {-# OVERLAPPING #-} FunArity [Clause] where
funArity :: [Clause] -> Int
funArity [] = Int
0
funArity [Clause]
cls = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Clause -> Int) -> [Clause] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Int
forall a. FunArity a => a -> Int
funArity [Clause]
cls
class LabelPatVars a b where
type PatVarLabel b
labelPatVars :: a -> State [PatVarLabel b] b
unlabelPatVars :: b -> a
default labelPatVars
:: (Traversable f
, LabelPatVars a' b'
, PatVarLabel b ~ PatVarLabel b'
, f a' ~ a, f b' ~ b)
=> a -> State [PatVarLabel b] b
labelPatVars = (a' -> StateT [PatVarLabel b'] Identity b')
-> f a' -> StateT [PatVarLabel b'] Identity (f b')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> StateT [PatVarLabel b'] Identity b'
forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars
default unlabelPatVars
:: (Traversable f, LabelPatVars a' b', f a' ~ a, f b' ~ b)
=> b -> a
unlabelPatVars = (b' -> a') -> f b' -> f a'
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b' -> a'
forall a b. LabelPatVars a b => b -> a
unlabelPatVars
instance LabelPatVars a b => LabelPatVars (Arg a) (Arg b) where
type PatVarLabel (Arg b) = PatVarLabel b
instance LabelPatVars a b => LabelPatVars (Named x a) (Named x b) where
type PatVarLabel (Named x b) = PatVarLabel b
instance LabelPatVars a b => LabelPatVars [a] [b] where
type PatVarLabel [b] = PatVarLabel b
instance LabelPatVars Pattern DeBruijnPattern where
type PatVarLabel DeBruijnPattern = Int
labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
labelPatVars = \case
VarP PatternInfo
o PatVarName
x -> PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (DBPatVar -> DeBruijnPattern)
-> (Int -> DBPatVar) -> Int -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x (Int -> DeBruijnPattern)
-> StateT [Int] Identity Int
-> StateT [Int] Identity DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [Int] Identity Int
next
DotP PatternInfo
o Term
t -> PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
t DeBruijnPattern
-> StateT [Int] Identity Int
-> StateT [Int] Identity DeBruijnPattern
forall a b. a -> StateT [Int] Identity b -> StateT [Int] Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT [Int] Identity Int
next
ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
ps -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
-> StateT [Int] Identity DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> State
[PatVarLabel [NamedArg DeBruijnPattern]] [NamedArg DeBruijnPattern]
forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars [NamedArg Pattern]
ps
DefP PatternInfo
o QName
q [NamedArg Pattern]
ps -> PatternInfo
-> QName -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
-> StateT [Int] Identity DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> State
[PatVarLabel [NamedArg DeBruijnPattern]] [NamedArg DeBruijnPattern]
forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars [NamedArg Pattern]
ps
LitP PatternInfo
o Literal
l -> DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
forall a. a -> StateT [PatVarLabel DeBruijnPattern] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern)
-> DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Literal -> DeBruijnPattern
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
ProjP ProjOrigin
o QName
q -> DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
forall a. a -> StateT [PatVarLabel DeBruijnPattern] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern)
-> DeBruijnPattern
-> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> DeBruijnPattern
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o QName
q
IApplyP PatternInfo
o Term
u Term
t PatVarName
x -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
u Term
t (DBPatVar -> DeBruijnPattern)
-> (Int -> DBPatVar) -> Int -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x (Int -> DeBruijnPattern)
-> StateT [Int] Identity Int
-> StateT [Int] Identity DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [Int] Identity Int
next
where
next :: StateT [Int] Identity Int
next = StateT [Int] Identity [Int]
-> StateT [Int] Identity Int
-> (Int -> [Int] -> StateT [Int] Identity Int)
-> StateT [Int] Identity Int
forall (m :: * -> *) a b.
Monad m =>
m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM StateT [Int] Identity [Int]
forall s (m :: * -> *). MonadState s m => m s
get StateT [Int] Identity Int
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Int -> [Int] -> StateT [Int] Identity Int)
-> StateT [Int] Identity Int)
-> (Int -> [Int] -> StateT [Int] Identity Int)
-> StateT [Int] Identity Int
forall a b. (a -> b) -> a -> b
$ \Int
x [Int]
xs -> do
[Int] -> StateT [Int] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Int]
xs
Int -> StateT [Int] Identity Int
forall a. a -> StateT [Int] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
unlabelPatVars :: DeBruijnPattern -> Pattern
unlabelPatVars = (DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DBPatVar -> PatVarName
dbPatVarName
{-# SPECIALIZE numberPatVars :: Int -> Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b
numberPatVars :: forall a b.
(LabelPatVars a b, PatVarLabel b ~ Int) =>
Int -> Permutation -> a -> b
numberPatVars Int
err Permutation
perm a
ps = State [Int] b -> [Int] -> b
forall s a. State s a -> s -> a
evalState (a -> State [PatVarLabel b] b
forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars a
ps) ([Int] -> b) -> [Int] -> b
forall a b. (a -> b) -> a -> b
$
Permutation -> [Int]
permPicks (Permutation -> [Int]) -> Permutation -> [Int]
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
flipP (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Int -> Permutation -> Permutation
invertP Int
err Permutation
perm
unnumberPatVars :: LabelPatVars a b => b -> a
unnumberPatVars :: forall a b. LabelPatVars a b => b -> a
unnumberPatVars = b -> a
forall a b. LabelPatVars a b => b -> a
unlabelPatVars
dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm = Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
True
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
countDots [NamedArg DeBruijnPattern]
ps = Int -> [Int] -> Permutation
Perm ([Maybe Int] -> Int
forall a. Sized a => a -> Int
size [Maybe Int]
ixs) ([Int] -> Permutation) -> Maybe [Int] -> Maybe Permutation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Int]
picks
where
ixs :: [Maybe Int]
ixs = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
n :: Int
n = [Int] -> Int
forall a. Sized a => a -> Int
size ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
ixs
picks :: Maybe [Int]
picks = [Int] -> (Int -> Maybe Int) -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ((Int -> Maybe Int) -> Maybe [Int])
-> (Int -> Maybe Int) -> Maybe [Int]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> Maybe Int -> [Maybe Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) [Maybe Int]
ixs
getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP PatternInfo
_ DBPatVar
x) = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]
getIndices (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
getIndices (DefP PatternInfo
_ QName
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
getIndices (DotP PatternInfo
_ Term
_) = [Maybe Int
forall a. Maybe a
Nothing | Bool
countDots]
getIndices (LitP PatternInfo
_ Literal
_) = []
getIndices ProjP{} = []
getIndices (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x) = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]
clausePerm :: Clause -> Maybe Permutation
clausePerm :: Clause -> Maybe Permutation
clausePerm = [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm ([NamedArg DeBruijnPattern] -> Maybe Permutation)
-> (Clause -> [NamedArg DeBruijnPattern])
-> Clause
-> Maybe Permutation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim :: Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg ArgInfo
ai (VarP PatternInfo
o DBPatVar
x)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternToElim (Arg ArgInfo
ai (ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim' Term] -> Term
Con ConHead
c ConInfo
ci ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$
(NamedArg DeBruijnPattern -> Elim' Term)
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg DeBruijnPattern -> Elim' Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
where ci :: ConInfo
ci = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi
patternToElim (Arg ArgInfo
ai (DefP PatternInfo
o QName
q [NamedArg DeBruijnPattern]
ps)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def QName
q ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$
(NamedArg DeBruijnPattern -> Elim' Term)
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg DeBruijnPattern -> Elim' Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
patternToElim (Arg ArgInfo
ai (DotP PatternInfo
o Term
t) ) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
t
patternToElim (Arg ArgInfo
ai (LitP PatternInfo
o Literal
l) ) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
patternToElim (Arg ArgInfo
ai (ProjP ProjOrigin
o QName
dest)) = ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
dest
patternToElim (Arg ArgInfo
ai (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x)) = Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
t Term
u (Term -> Elim' Term) -> Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim' Term]
patternsToElims [NamedArg DeBruijnPattern]
ps = (NamedArg DeBruijnPattern -> Elim' Term)
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> Elim' Term
build [NamedArg DeBruijnPattern]
ps
where
build :: NamedArg DeBruijnPattern -> Elim
build :: NamedArg DeBruijnPattern -> Elim' Term
build = Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg DeBruijnPattern -> Elim' Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing
patternToTerm :: DeBruijnPattern -> Term
patternToTerm :: DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p = case Arg DeBruijnPattern -> Elim' Term
patternToElim (DeBruijnPattern -> Arg DeBruijnPattern
forall a. a -> Arg a
defaultArg DeBruijnPattern
p) of
Apply Arg Term
x -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
Proj{} -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
IApply Term
_ Term
_ Term
x -> Term
x
class MapNamedArgPattern a p where
mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
default mapNamedArgPattern
:: (Functor f, MapNamedArgPattern a p', p ~ f p')
=> (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern = (p' -> p') -> p -> p
(p' -> p') -> f p' -> f p'
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((p' -> p') -> p -> p)
-> ((NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p')
-> (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> p
-> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p'
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern
instance MapNamedArgPattern a (NamedArg (Pattern' a)) where
mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np =
case NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
np of
VarP PatternInfo
o a
x -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
DotP PatternInfo
o Term
t -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
LitP PatternInfo
o Literal
l -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
ProjP ProjOrigin
o QName
q -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
i ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
IApplyP PatternInfo
o Term
u Term
t a
x -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
instance MapNamedArgPattern a p => MapNamedArgPattern a [p] where
class PatternLike a b where
foldrPattern
:: Monoid m
=> (Pattern' a -> m -> m)
-> b -> m
default foldrPattern
:: (Monoid m, Foldable f, PatternLike a p, f p ~ b)
=> (Pattern' a -> m -> m) -> b -> m
foldrPattern = (p -> m) -> b -> m
(p -> m) -> f p -> m
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((p -> m) -> b -> m)
-> ((Pattern' a -> m -> m) -> p -> m)
-> (Pattern' a -> m -> m)
-> b
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> m -> m) -> p -> m
forall m. Monoid m => (Pattern' a -> m -> m) -> p -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern
traversePatternM
:: Monad m
=> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> b -> m b
default traversePatternM
:: (Traversable f, PatternLike a p, f p ~ b, Monad m)
=> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = (p -> m p) -> f p -> m (f p)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((p -> m p) -> f p -> m (f p)) -> (p -> m p) -> f p -> m (f p)
forall a b. (a -> b) -> a -> b
$ (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post
foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m
foldPattern :: forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern Pattern' a -> m
f = (Pattern' a -> m -> m) -> b -> m
forall m. Monoid m => (Pattern' a -> m -> m) -> b -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern ((Pattern' a -> m -> m) -> b -> m)
-> (Pattern' a -> m -> m) -> b -> m
forall a b. (a -> b) -> a -> b
$ \ Pattern' a
p m
m -> Pattern' a -> m
f Pattern' a
p m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` m
m
preTraversePatternM
:: (PatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))
-> b -> m b
preTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM Pattern' a -> m (Pattern' a)
pre = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
postTraversePatternM :: (PatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))
-> b -> m b
postTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
instance PatternLike a (Pattern' a) where
foldrPattern :: forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
foldrPattern Pattern' a -> m -> m
f Pattern' a
p = Pattern' a -> m -> m
f Pattern' a
p (m -> m) -> m -> m
forall a b. (a -> b) -> a -> b
$ case Pattern' a
p of
ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall m.
Monoid m =>
(Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall m.
Monoid m =>
(Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
VarP PatternInfo
_ a
_ -> m
forall a. Monoid a => a
mempty
LitP PatternInfo
_ Literal
_ -> m
forall a. Monoid a => a
mempty
DotP PatternInfo
_ Term
_ -> m
forall a. Monoid a => a
mempty
ProjP ProjOrigin
_ QName
_ -> m
forall a. Monoid a => a
mempty
IApplyP{} -> m
forall a. Monoid a => a
mempty
traversePatternM :: forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = Pattern' a -> m (Pattern' a)
pre (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
recurse (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
post
where
recurse :: Pattern' a -> m (Pattern' a)
recurse Pattern' a
p = case Pattern' a
p of
ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)]
ps -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (Pattern' a)] -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (Pattern' a)] -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
VarP PatternInfo
_ a
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
LitP PatternInfo
_ Literal
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
DotP PatternInfo
_ Term
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
ProjP ProjOrigin
_ QName
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
IApplyP{} -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
instance PatternLike a b => PatternLike a [b] where
instance PatternLike a b => PatternLike a (Arg b) where
instance PatternLike a b => PatternLike a (Named x b) where
class CountPatternVars a where
countPatternVars :: a -> Int
default countPatternVars :: (Foldable f, CountPatternVars b, f b ~ a) =>
a -> Int
countPatternVars = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Sum Int) -> f b -> Sum Int
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (b -> Int) -> b -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars)
instance CountPatternVars a => CountPatternVars [a] where
instance CountPatternVars a => CountPatternVars (Arg a) where
instance CountPatternVars a => CountPatternVars (Named x a) where
instance CountPatternVars (Pattern' x) where
countPatternVars :: Pattern' x -> Int
countPatternVars Pattern' x
p =
case Pattern' x
p of
VarP{} -> Int
1
ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars [NamedArg (Pattern' x)]
ps
DotP{} -> Int
1
Pattern' x
_ -> Int
0
class PatternVarModalities p where
type PatVar p
patternVarModalities :: p -> [(PatVar p, Modality)]
instance PatternVarModalities a => PatternVarModalities [a] where
type PatVar [a] = PatVar a
patternVarModalities :: [a] -> [(PatVar [a], Modality)]
patternVarModalities = (a -> [(PatVar a, Modality)]) -> [a] -> [(PatVar a, Modality)]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> [(PatVar a, Modality)]
forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities
instance PatternVarModalities a => PatternVarModalities (Named s a) where
type PatVar (Named s a) = PatVar a
patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)]
patternVarModalities = (a -> [(PatVar a, Modality)])
-> Named s a -> [(PatVar a, Modality)]
forall m a. Monoid m => (a -> m) -> Named s a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> [(PatVar a, Modality)]
forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities
instance PatternVarModalities a => PatternVarModalities (Arg a) where
type PatVar (Arg a) = PatVar a
patternVarModalities :: Arg a -> [(PatVar (Arg a), Modality)]
patternVarModalities Arg a
arg = ((PatVar a, Modality) -> (PatVar a, Modality))
-> [(PatVar a, Modality)] -> [(PatVar a, Modality)]
forall a b. (a -> b) -> [a] -> [b]
map ((Modality -> Modality)
-> (PatVar a, Modality) -> (PatVar a, Modality)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Modality -> Modality -> Modality
composeModality Modality
m)) (a -> [(PatVar a, Modality)]
forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities (a -> [(PatVar a, Modality)]) -> a -> [(PatVar a, Modality)]
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
arg)
where m :: Modality
m = Arg a -> Modality
forall a. LensModality a => a -> Modality
getModality Arg a
arg
instance PatternVarModalities (Pattern' x) where
type PatVar (Pattern' x) = x
patternVarModalities :: Pattern' x -> [(PatVar (Pattern' x), Modality)]
patternVarModalities Pattern' x
p =
case Pattern' x
p of
VarP PatternInfo
_ x
x -> [(x
PatVar (Pattern' x)
x, Modality
defaultModality)]
ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)]
-> [(PatVar [NamedArg (Pattern' x)], Modality)]
forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
DefP PatternInfo
_ QName
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)]
-> [(PatVar [NamedArg (Pattern' x)], Modality)]
forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
DotP{} -> []
LitP{} -> []
ProjP{} -> []
IApplyP PatternInfo
_ Term
_ Term
_ x
x -> [(x
PatVar (Pattern' x)
x, Modality
defaultModality)]
hasDefP :: [NamedArg DeBruijnPattern] -> Bool
hasDefP :: [NamedArg DeBruijnPattern] -> Bool
hasDefP [NamedArg DeBruijnPattern]
ps = Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ ((DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any)
-> [NamedArg DeBruijnPattern] -> (DeBruijnPattern -> Any) -> Any
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern [NamedArg DeBruijnPattern]
ps ((DeBruijnPattern -> Any) -> Any)
-> (DeBruijnPattern -> Any) -> Any
forall a b. (a -> b) -> a -> b
$ \ (DeBruijnPattern
x :: DeBruijnPattern) ->
case DeBruijnPattern
x of
DefP{} -> Bool -> Any
Any Bool
True
DeBruijnPattern
_ -> Bool -> Any
Any Bool
False