{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Internal.Pattern where
import Control.Arrow (second)
import Control.Monad.State
import Data.Maybe
import Data.Monoid
import qualified Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Abstract (IsProjP(..))
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 cl :: 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 cl :: 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 (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 [] = 0
funArity cls :: [Clause]
cls = [Int] -> Int
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 i | b -> i where
labelPatVars :: a -> State [i] b
unlabelPatVars :: b -> a
default labelPatVars
:: (Traversable f, LabelPatVars a' b' i, f a' ~ a, f b' ~ b)
=> a -> State [i] b
labelPatVars = (a' -> StateT [i] Identity b')
-> f a' -> StateT [i] Identity (f b')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a' -> StateT [i] Identity b'
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars
default unlabelPatVars
:: (Traversable f, LabelPatVars a' b' i, f a' ~ a, f b' ~ b)
=> b -> a
unlabelPatVars = (b' -> a') -> f b' -> f a'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b' -> a'
forall a b i. LabelPatVars a b i => b -> a
unlabelPatVars
instance LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i where
instance LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i where
instance LabelPatVars a b i => LabelPatVars [a] [b] i where
instance LabelPatVars Pattern DeBruijnPattern Int where
labelPatVars :: Pattern -> State [Int] DeBruijnPattern
labelPatVars p :: Pattern
p =
case Pattern
p of
VarP o :: PatternInfo
o x :: PatVarName
x -> do Int
i <- StateT [Int] Identity Int
next
DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
i)
DotP o :: PatternInfo
o t :: Term
t -> PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
t DeBruijnPattern
-> StateT [Int] Identity Int -> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT [Int] Identity Int
next
ConP c :: ConHead
c mt :: ConPatternInfo
mt ps :: [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]
-> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars [NamedArg Pattern]
ps
DefP o :: PatternInfo
o q :: QName
q ps :: [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]
-> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars [NamedArg Pattern]
ps
LitP o :: PatternInfo
o l :: Literal
l -> DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Literal -> DeBruijnPattern
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
ProjP o :: ProjOrigin
o q :: QName
q -> DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> DeBruijnPattern
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o QName
q
IApplyP o :: PatternInfo
o u :: Term
u t :: Term
t x :: PatVarName
x -> do Int
i <- StateT [Int] Identity Int
next
DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
u Term
t (PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
i)
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
$ \ x :: Int
x xs :: [Int]
xs -> do [Int] -> StateT [Int] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Int]
xs; Int -> StateT [Int] Identity Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
unlabelPatVars :: DeBruijnPattern -> Pattern
unlabelPatVars = (DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern
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 Int => Int -> Permutation -> a -> b
numberPatVars :: Int -> Permutation -> a -> b
numberPatVars err :: Int
err perm :: Permutation
perm ps :: a
ps = State [Int] b -> [Int] -> b
forall s a. State s a -> s -> a
evalState (a -> State [Int] b
forall a b i. LabelPatVars a b i => a -> State [i] 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 i => b -> a
unnumberPatVars :: b -> a
unnumberPatVars = b -> a
forall a b i. LabelPatVars a b i => 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' countDots :: Bool
countDots ps :: [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
$ \ i :: Int
i -> (Maybe Int -> Bool) -> [Maybe Int] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Int]
ixs
getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP _ x :: 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 c :: ConHead
c _ ps :: [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 _ _ ps :: [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 _ _) = [Maybe Int
forall a. Maybe a
Nothing | Bool
countDots]
getIndices (LitP _ _) = []
getIndices ProjP{} = []
getIndices (IApplyP _ _ _ x :: 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 ai :: ArgInfo
ai (VarP o :: PatternInfo
o x :: 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 ai :: ArgInfo
ai (ConP c :: ConHead
c cpi :: ConPatternInfo
cpi ps :: [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 (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 ai :: ArgInfo
ai (DefP o :: PatternInfo
o q :: QName
q ps :: [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 (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 ai :: ArgInfo
ai (DotP o :: PatternInfo
o t :: 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 ai :: ArgInfo
ai (LitP o :: PatternInfo
o l :: 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 ai :: ArgInfo
ai (ProjP o :: ProjOrigin
o dest :: QName
dest)) = ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
dest
patternToElim (Arg ai :: ArgInfo
ai (IApplyP o :: PatternInfo
o t :: Term
t u :: Term
u x :: 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 ps :: [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 (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 p :: DeBruijnPattern
p = case Arg DeBruijnPattern -> Elim' Term
patternToElim (DeBruijnPattern -> Arg DeBruijnPattern
forall a. a -> Arg a
defaultArg DeBruijnPattern
p) of
Apply x :: Arg Term
x -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
Proj{} -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
IApply _ _ x :: 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') -> f p' -> f p'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((p' -> p') -> f p' -> f p')
-> ((NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p')
-> (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> f p'
-> f 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 f :: NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f np :: NamedArg (Pattern' a)
np =
case NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
np of
VarP o :: PatternInfo
o x :: a
x -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
DotP o :: PatternInfo
o t :: Term
t -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
LitP o :: PatternInfo
o l :: Literal
l -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
ProjP o :: ProjOrigin
o q :: QName
q -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
ConP c :: ConHead
c i :: ConPatternInfo
i ps :: [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 o :: PatternInfo
o q :: QName
q ps :: [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 o :: PatternInfo
o u :: Term
u t :: Term
t x :: 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) -> f p -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((p -> m) -> f p -> m)
-> ((Pattern' a -> m -> m) -> p -> m)
-> (Pattern' a -> m -> m)
-> f p
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 pre :: Pattern' a -> m (Pattern' a)
pre post :: Pattern' a -> m (Pattern' a)
post = (p -> m p) -> b -> m b
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((p -> m p) -> b -> m b) -> (p -> m p) -> b -> m b
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
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 :: (Pattern' a -> m) -> b -> m
foldPattern f :: Pattern' a -> m
f = (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
$ \ p :: Pattern' a
p m :: 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 :: (Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM pre :: 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
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' 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 :: (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
traversePatternM Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return
instance PatternLike a (Pattern' a) where
foldrPattern :: (Pattern' a -> m -> m) -> Pattern' a -> m
foldrPattern f :: Pattern' a -> m -> m
f p :: 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 _ _ ps :: [NamedArg (Pattern' a)]
ps -> (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 _ _ ps :: [NamedArg (Pattern' a)]
ps -> (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 _ _ -> m
forall a. Monoid a => a
mempty
LitP _ _ -> m
forall a. Monoid a => a
mempty
DotP _ _ -> m
forall a. Monoid a => a
mempty
ProjP _ _ -> m
forall a. Monoid a => a
mempty
IApplyP{} -> m
forall a. Monoid a => a
mempty
traversePatternM :: (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traversePatternM pre :: Pattern' a -> m (Pattern' a)
pre post :: 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 p :: Pattern' a
p = case Pattern' a
p of
ConP c :: ConHead
c ci :: ConPatternInfo
ci ps :: [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
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
DefP o :: PatternInfo
o q :: QName
q ps :: [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
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
VarP _ _ -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
LitP _ _ -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
DotP _ _ -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
ProjP _ _ -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
IApplyP{} -> Pattern' a -> m (Pattern' 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) -> (f b -> Sum Int) -> f b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Sum Int) -> f b -> Sum Int
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 p :: Pattern' x
p =
case Pattern' x
p of
VarP{} -> 1
ConP _ _ ps :: [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars [NamedArg (Pattern' x)]
ps
DotP{} -> 1
_ -> 0
class PatternVarModalities p x | p -> x where
patternVarModalities :: p -> [(x, Modality)]
instance PatternVarModalities a x => PatternVarModalities [a] x where
patternVarModalities :: [a] -> [(x, Modality)]
patternVarModalities = (a -> [(x, Modality)]) -> [a] -> [(x, Modality)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities
instance PatternVarModalities a x => PatternVarModalities (Named s a) x where
patternVarModalities :: Named s a -> [(x, Modality)]
patternVarModalities = (a -> [(x, Modality)]) -> Named s a -> [(x, Modality)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities
instance PatternVarModalities a x => PatternVarModalities (Arg a) x where
patternVarModalities :: Arg a -> [(x, Modality)]
patternVarModalities arg :: Arg a
arg = ((x, Modality) -> (x, Modality))
-> [(x, Modality)] -> [(x, Modality)]
forall a b. (a -> b) -> [a] -> [b]
map ((Modality -> Modality) -> (x, Modality) -> (x, Modality)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Modality
m Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<>)) (a -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities (a -> [(x, Modality)]) -> a -> [(x, 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) x where
patternVarModalities :: Pattern' x -> [(x, Modality)]
patternVarModalities p :: Pattern' x
p =
case Pattern' x
p of
VarP _ x :: x
x -> [(x
x, Modality
defaultModality)]
ConP _ _ ps :: [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
DefP _ _ ps :: [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
DotP{} -> []
LitP{} -> []
ProjP{} -> []
IApplyP _ _ _ x :: x
x -> [(x
x, Modality
defaultModality)]