{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Patterns.Match where
import Prelude hiding (null)
import Control.Monad
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad hiding (constructorForm)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.Utils.Empty
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Match a = Yes Simplification (IntMap (Arg a))
| No
| DontKnow (Blocked ())
deriving a -> Match b -> Match a
(a -> b) -> Match a -> Match b
(forall a b. (a -> b) -> Match a -> Match b)
-> (forall a b. a -> Match b -> Match a) -> Functor Match
forall a b. a -> Match b -> Match a
forall a b. (a -> b) -> Match a -> Match b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Match b -> Match a
$c<$ :: forall a b. a -> Match b -> Match a
fmap :: (a -> b) -> Match a -> Match b
$cfmap :: forall a b. (a -> b) -> Match a -> Match b
Functor
instance Null (Match a) where
empty :: Match a
empty = Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
forall a. Null a => a
empty IntMap (Arg a)
forall a. Null a => a
empty
null :: Match a -> Bool
null (Yes simpl :: Simplification
simpl as :: IntMap (Arg a)
as) = Simplification -> Bool
forall a. Null a => a -> Bool
null Simplification
simpl Bool -> Bool -> Bool
&& IntMap (Arg a) -> Bool
forall a. Null a => a -> Bool
null IntMap (Arg a)
as
null _ = Bool
False
matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs err :: Empty
err n :: Int
n vs :: IntMap (Arg a)
vs = (Int -> Arg a) -> [Int] -> [Arg a]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Arg a
get [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
where
get :: Int -> Arg a
get k :: Int
k = Arg a -> Maybe (Arg a) -> Arg a
forall a. a -> Maybe a -> a
fromMaybe (Empty -> Arg a
forall a. Empty -> a
absurd Empty
err) (Maybe (Arg a) -> Arg a) -> Maybe (Arg a) -> Arg a
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Arg a) -> Maybe (Arg a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
k IntMap (Arg a)
vs
buildSubstitution :: (DeBruijn a)
=> Empty -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution :: Empty -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution err :: Empty
err n :: Int
n vs :: IntMap (Arg a)
vs = [a] -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([a] -> Substitution' a) -> [a] -> Substitution' a
forall a b. (a -> b) -> a -> b
$ (Arg a -> a) -> [Arg a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Arg a -> a
forall e. Arg e -> e
unArg ([Arg a] -> [a]) -> [Arg a] -> [a]
forall a b. (a -> b) -> a -> b
$ Empty -> Int -> IntMap (Arg a) -> [Arg a]
forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs Empty
err Int
n IntMap (Arg a)
vs
instance Semigroup (Match a) where
DontKnow b :: Blocked ()
b <> :: Match a -> Match a -> Match a
<> DontKnow b' :: Blocked ()
b' = Blocked () -> Match a
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match a) -> Blocked () -> Match a
forall a b. (a -> b) -> a -> b
$ Blocked ()
b Blocked () -> Blocked () -> Blocked ()
forall a. Semigroup a => a -> a -> a
<> Blocked ()
b'
DontKnow m :: Blocked ()
m <> _ = Blocked () -> Match a
forall a. Blocked () -> Match a
DontKnow Blocked ()
m
_ <> DontKnow m :: Blocked ()
m = Blocked () -> Match a
forall a. Blocked () -> Match a
DontKnow Blocked ()
m
No <> _ = Match a
forall a. Match a
No
_ <> No = Match a
forall a. Match a
No
Yes s :: Simplification
s us :: IntMap (Arg a)
us <> Yes s' :: Simplification
s' vs :: IntMap (Arg a)
vs = Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes (Simplification
s Simplification -> Simplification -> Simplification
forall a. Semigroup a => a -> a -> a
<> Simplification
s') (IntMap (Arg a)
us IntMap (Arg a) -> IntMap (Arg a) -> IntMap (Arg a)
forall a. Semigroup a => a -> a -> a
<> IntMap (Arg a)
vs)
instance Monoid (Match a) where
mempty :: Match a
mempty = Match a
forall a. Null a => a
empty
mappend :: Match a -> Match a -> Match a
mappend = Match a -> Match a -> Match a
forall a. Semigroup a => a -> a -> a
(<>)
foldMatch
:: forall p v . IsProjP p => (p -> v -> ReduceM (Match Term, v))
-> [p] -> [v] -> ReduceM (Match Term, [v])
foldMatch :: (p -> v -> ReduceM (Match Term, v))
-> [p] -> [v] -> ReduceM (Match Term, [v])
foldMatch match :: p -> v -> ReduceM (Match Term, v)
match = [p] -> [v] -> ReduceM (Match Term, [v])
loop where
loop :: [p] -> [v] -> ReduceM (Match Term, [v])
loop :: [p] -> [v] -> ReduceM (Match Term, [v])
loop ps0 :: [p]
ps0 vs0 :: [v]
vs0 = do
case ([p]
ps0, [v]
vs0) of
([], []) -> (Match Term, [v]) -> ReduceM (Match Term, [v])
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Null a => a
empty, [])
(p :: p
p : ps :: [p]
ps, v :: v
v : vs :: [v]
vs) -> do
(r :: Match Term
r, v' :: v
v') <- p -> v -> ReduceM (Match Term, v)
match p
p v
v
case Match Term
r of
No | Just{} <- p -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP p
p -> (Match Term, [v]) -> ReduceM (Match Term, [v])
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Match a
No, v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs)
No -> do
(r' :: Match Term
r', _vs' :: [v]
_vs') <- [p] -> [v] -> ReduceM (Match Term, [v])
loop [p]
ps [v]
vs
(Match Term, [v]) -> ReduceM (Match Term, [v])
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
r Match Term -> Match Term -> Match Term
forall a. Semigroup a => a -> a -> a
<> Match Term
r', v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs)
DontKnow m :: Blocked ()
m -> (Match Term, [v]) -> ReduceM (Match Term, [v])
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow Blocked ()
m, v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs)
Yes{} -> do
(r' :: Match Term
r', vs' :: [v]
vs') <- [p] -> [v] -> ReduceM (Match Term, [v])
loop [p]
ps [v]
vs
(Match Term, [v]) -> ReduceM (Match Term, [v])
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
r Match Term -> Match Term -> Match Term
forall a. Semigroup a => a -> a -> a
<> Match Term
r', v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs')
_ -> ReduceM (Match Term, [v])
forall a. HasCallStack => a
__IMPOSSIBLE__
mergeElim :: Elim -> Arg Term -> Elim
mergeElim :: Elim -> Arg Term -> Elim
mergeElim Apply{} arg :: Arg Term
arg = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg
mergeElim (IApply x :: Term
x y :: Term
y _) arg :: Arg Term
arg = Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
mergeElim Proj{} _ = Elim
forall a. HasCallStack => a
__IMPOSSIBLE__
mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims = (Elim -> Arg Term -> Elim) -> [Elim] -> [Arg Term] -> [Elim]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Elim -> Arg Term -> Elim
mergeElim
matchCopatterns :: [NamedArg DeBruijnPattern]
-> [Elim]
-> ReduceM (Match Term, [Elim])
matchCopatterns :: [NamedArg DeBruijnPattern]
-> [Elim] -> ReduceM (Match Term, [Elim])
matchCopatterns ps :: [NamedArg DeBruijnPattern]
ps vs :: [Elim]
vs = do
VerboseKey
-> Int
-> TCM Doc
-> ReduceM (Match Term, [Elim])
-> ReduceM (Match Term, [Elim])
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "tc.match" 50
([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ "matchCopatterns"
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "ps =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCM Doc)
-> [NamedArg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (DeBruijnPattern -> TCM Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps)
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "vs =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCM Doc) -> [Elim] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Elim]
vs)
]) (ReduceM (Match Term, [Elim]) -> ReduceM (Match Term, [Elim]))
-> ReduceM (Match Term, [Elim]) -> ReduceM (Match Term, [Elim])
forall a b. (a -> b) -> a -> b
$ do
(NamedArg DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim))
-> [NamedArg DeBruijnPattern]
-> [Elim]
-> ReduceM (Match Term, [Elim])
forall p v.
IsProjP p =>
(p -> v -> ReduceM (Match Term, v))
-> [p] -> [v] -> ReduceM (Match Term, [v])
foldMatch (DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim)
matchCopattern (DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim))
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim
-> ReduceM (Match Term, Elim)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps [Elim]
vs
matchCopattern :: DeBruijnPattern
-> Elim
-> ReduceM (Match Term, Elim)
matchCopattern :: DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim)
matchCopattern pat :: DeBruijnPattern
pat@ProjP{} elim :: Elim
elim@(Proj _ q :: QName
q) = do
ProjP _ p :: QName
p <- DeBruijnPattern -> ReduceM DeBruijnPattern
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP DeBruijnPattern
pat
QName
q <- QName -> ReduceM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
q
(Match Term, Elim) -> ReduceM (Match Term, Elim)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Match Term, Elim) -> ReduceM (Match Term, Elim))
-> (Match Term, Elim) -> ReduceM (Match Term, Elim)
forall a b. (a -> b) -> a -> b
$ if QName
p QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q then (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg Term)
forall a. Null a => a
empty, Elim
elim)
else (Match Term
forall a. Match a
No, Elim
elim)
matchCopattern ProjP{} elim :: Elim
elim@Apply{} = (Match Term, Elim) -> ReduceM (Match Term, Elim)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Match a
No , Elim
elim)
matchCopattern _ elim :: Elim
elim@Proj{} = (Match Term, Elim) -> ReduceM (Match Term, Elim)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Match a
No , Elim
elim)
matchCopattern p :: DeBruijnPattern
p (Apply v :: Arg Term
v) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ((Match Term, Arg Term) -> (Match Term, Elim))
-> ReduceM (Match Term, Arg Term) -> ReduceM (Match Term, Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern DeBruijnPattern
p Arg Term
v
matchCopattern p :: DeBruijnPattern
p e :: Elim
e@(IApply x :: Term
x y :: Term
y r :: Term
r) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (Elim -> Arg Term -> Elim
mergeElim Elim
e) ((Match Term, Arg Term) -> (Match Term, Elim))
-> ReduceM (Match Term, Arg Term) -> ReduceM (Match Term, Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
r)
matchPatterns :: [NamedArg DeBruijnPattern]
-> [Arg Term]
-> ReduceM (Match Term, [Arg Term])
matchPatterns :: [NamedArg DeBruijnPattern]
-> [Arg Term] -> ReduceM (Match Term, [Arg Term])
matchPatterns ps :: [NamedArg DeBruijnPattern]
ps vs :: [Arg Term]
vs = do
VerboseKey -> Int -> TCM Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.match" 20 (TCM Doc -> ReduceM ()) -> TCM Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$
[TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ "matchPatterns"
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "ps =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg DeBruijnPattern] -> TCM Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
ps
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "vs =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCM Doc) -> [Arg Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
]
VerboseKey
-> Int
-> TCM Doc
-> ReduceM (Match Term, [Arg Term])
-> ReduceM (Match Term, [Arg Term])
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "tc.match" 50
([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ "matchPatterns"
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "ps =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCM Doc)
-> [NamedArg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (NamedArg DeBruijnPattern -> VerboseKey)
-> NamedArg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [NamedArg DeBruijnPattern]
ps)
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "vs =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCM Doc) -> [Arg Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
]) (ReduceM (Match Term, [Arg Term])
-> ReduceM (Match Term, [Arg Term]))
-> ReduceM (Match Term, [Arg Term])
-> ReduceM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ do
(NamedArg DeBruijnPattern
-> Arg Term -> ReduceM (Match Term, Arg Term))
-> [NamedArg DeBruijnPattern]
-> [Arg Term]
-> ReduceM (Match Term, [Arg Term])
forall p v.
IsProjP p =>
(p -> v -> ReduceM (Match Term, v))
-> [p] -> [v] -> ReduceM (Match Term, [v])
foldMatch (DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern (DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term))
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Arg Term
-> ReduceM (Match Term, Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps [Arg Term]
vs
matchPattern :: DeBruijnPattern
-> Arg Term
-> ReduceM (Match Term, Arg Term)
matchPattern :: DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern p :: DeBruijnPattern
p u :: Arg Term
u = case (DeBruijnPattern
p, Arg Term
u) of
(ProjP{}, _ ) -> ReduceM (Match Term, Arg Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
(IApplyP _ _ _ x :: DBPatVar
x , arg :: Arg Term
arg ) -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
where entry :: IntMap (Arg Term)
entry = (Int, Arg Term) -> IntMap (Arg Term)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg Term
arg)
(VarP _ x :: DBPatVar
x , arg :: Arg Term
arg ) -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
where entry :: IntMap (Arg Term)
entry = (Int, Arg Term) -> IntMap (Arg Term)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg Term
arg)
(DotP _ _ , arg :: Arg Term
arg@(Arg _ v :: Term
v)) -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
forall a. Null a => a
empty, Arg Term
arg)
(LitP _ l :: Literal
l , arg :: Arg Term
arg@(Arg _ v :: Term
v)) -> do
Blocked Term
w <- Term -> ReduceM (Blocked Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
v
let arg' :: Arg Term
arg' = Arg Term
arg Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
w
case Blocked Term
w of
NotBlocked _ (Lit l' :: Literal
l')
| Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l' -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg Term)
forall a. Null a => a
empty , Arg Term
arg')
| Bool
otherwise -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Match a
No , Arg Term
arg')
NotBlocked _ (MetaV x :: MetaId
x _) -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked ()
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x () , Arg Term
arg')
Blocked x :: MetaId
x _ -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked ()
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x () , Arg Term
arg')
NotBlocked r :: NotBlocked
r t :: Term
t -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ NotBlocked -> () -> Blocked ()
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
r' () , Arg Term
arg')
where r' :: NotBlocked
r' = Elim -> NotBlocked -> NotBlocked
stuckOn (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg') NotBlocked
r
(ConP c :: ConHead
c cpi :: ConPatternInfo
cpi ps :: [NamedArg DeBruijnPattern]
ps, Arg info :: ArgInfo
info v :: Term
v) -> do
if Bool -> Bool
not (ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi) then ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback ConHead
c [NamedArg DeBruijnPattern]
ps (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v) else do
QName -> ReduceM (Maybe [Arg QName])
isEtaRecordCon (ConHead -> QName
conName ConHead
c) ReduceM (Maybe [Arg QName])
-> (Maybe [Arg QName] -> ReduceM (Match Term, Arg Term))
-> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Nothing -> ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback ConHead
c [NamedArg DeBruijnPattern]
ps (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
Just fs :: [Arg QName]
fs -> do
Bool -> ReduceM () -> ReduceM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Arg QName] -> Int
forall a. Sized a => a -> Int
size [Arg QName]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg DeBruijnPattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg DeBruijnPattern]
ps) ReduceM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
([Arg Term] -> Arg Term)
-> (Match Term, [Arg Term]) -> (Match Term, Arg Term)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Arg Term)
-> ([Arg Term] -> Term) -> [Arg Term] -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c (ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi) ([Elim] -> Term) -> ([Arg Term] -> [Elim]) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) ((Match Term, [Arg Term]) -> (Match Term, Arg Term))
-> ReduceM (Match Term, [Arg Term])
-> ReduceM (Match Term, Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[NamedArg DeBruijnPattern]
-> [Arg Term] -> ReduceM (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps ([Arg Term] -> ReduceM (Match Term, [Arg Term]))
-> [Arg Term] -> ReduceM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ [Arg QName] -> (Arg QName -> Arg Term) -> [Arg Term]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> [Arg Term])
-> (Arg QName -> Arg Term) -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ \ (Arg ai :: ArgInfo
ai f :: QName
f) -> 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
$ Term
v Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
where
isEtaRecordCon :: QName -> ReduceM (Maybe [Arg QName])
isEtaRecordCon :: QName -> ReduceM (Maybe [Arg QName])
isEtaRecordCon c :: QName
c = do
(Definition -> Defn
theDef (Definition -> Defn) -> ReduceM Definition -> ReduceM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c) ReduceM Defn
-> (Defn -> ReduceM (Maybe [Arg QName]))
-> ReduceM (Maybe [Arg QName])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Constructor{ conData :: Defn -> QName
conData = QName
d } -> do
(Definition -> Defn
theDef (Definition -> Defn) -> ReduceM Definition -> ReduceM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) ReduceM Defn
-> (Defn -> ReduceM (Maybe [Arg QName]))
-> ReduceM (Maybe [Arg QName])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
r :: Defn
r@Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } | HasEta
YesEta <- Defn -> HasEta
recEtaEquality Defn
r -> Maybe [Arg QName] -> ReduceM (Maybe [Arg QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Arg QName] -> ReduceM (Maybe [Arg QName]))
-> Maybe [Arg QName] -> ReduceM (Maybe [Arg QName])
forall a b. (a -> b) -> a -> b
$ [Arg QName] -> Maybe [Arg QName]
forall a. a -> Maybe a
Just ([Arg QName] -> Maybe [Arg QName])
-> [Arg QName] -> Maybe [Arg QName]
forall a b. (a -> b) -> a -> b
$ (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs
_ -> Maybe [Arg QName] -> ReduceM (Maybe [Arg QName])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Arg QName]
forall a. Maybe a
Nothing
_ -> ReduceM (Maybe [Arg QName])
forall a. HasCallStack => a
__IMPOSSIBLE__
(DefP o :: PatternInfo
o q :: QName
q ps :: [NamedArg DeBruijnPattern]
ps, v :: Arg Term
v) -> do
let f :: Term -> Maybe ([Elim] -> Term, [Elim])
f (Def q' :: QName
q' vs :: [Elim]
vs) | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
q, [Elim]
vs)
f _ = Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f [NamedArg DeBruijnPattern]
ps Arg Term
v
where
fallback :: ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback c :: ConHead
c ps :: [NamedArg DeBruijnPattern]
ps v :: Arg Term
v = do
Blocked Term -> Maybe Term
isMatchable <- ReduceM (Blocked Term -> Maybe Term)
isMatchable'
let f :: Term -> Maybe ([Elim] -> Term, [Elim])
f (Con c' :: ConHead
c' ci' :: ConInfo
ci' vs :: [Elim]
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c' ConInfo
ci',[Elim]
vs)
f _ = Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f [NamedArg DeBruijnPattern]
ps Arg Term
v
isMatchable' :: ReduceM (Blocked Term -> Maybe Term)
isMatchable' = do
Maybe QName
mhcomp <- VerboseKey -> ReduceM (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getName' VerboseKey
builtinHComp
(Blocked Term -> Maybe Term)
-> ReduceM (Blocked Term -> Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Blocked Term -> Maybe Term)
-> ReduceM (Blocked Term -> Maybe Term))
-> (Blocked Term -> Maybe Term)
-> ReduceM (Blocked Term -> Maybe Term)
forall a b. (a -> b) -> a -> b
$ \ r :: Blocked Term
r ->
case Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
r of
t :: Term
t@Con{} -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t
t :: Term
t@(Def q :: QName
q [l :: Elim
l,a :: Elim
a,phi :: Elim
phi,u :: Elim
u,u0 :: Elim
u0]) | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcomp
-> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t
_ -> Maybe Term
forall a. Maybe a
Nothing
fallback' :: (Term -> Maybe ([Elim] -> Term, [Elim]))
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> ReduceM (Match Term, Arg Term)
fallback' mtc :: Term -> Maybe ([Elim] -> Term, [Elim])
mtc ps :: [NamedArg DeBruijnPattern]
ps (Arg info :: ArgInfo
info v :: Term
v) = do
Blocked Term -> Maybe Term
isMatchable <- ReduceM (Blocked Term -> Maybe Term)
isMatchable'
Blocked Term
w <- Term -> ReduceM (Blocked Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Term
v
Blocked Term
w <- (Term -> ReduceM Term) -> Blocked Term -> ReduceM (Blocked Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Blocked Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> ReduceM (Blocked Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Blocked Term
w of
NotBlocked r :: NotBlocked
r u :: Term
u -> Term -> ReduceM (Blocked Term)
unfoldCorecursion Term
u
_ -> Blocked Term -> ReduceM (Blocked Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked Term
w
let v :: Term
v = Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
w
arg :: Arg Term
arg = ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v
case Blocked Term
w of
b :: Blocked Term
b | Just t :: Term
t <- Blocked Term -> Maybe Term
isMatchable Blocked Term
b ->
case Term -> Maybe ([Elim] -> Term, [Elim])
mtc Term
t of
Just (bld :: [Elim] -> Term
bld, vs :: [Elim]
vs) -> do
(m :: Match Term
m, vs1 :: [Arg Term]
vs1) <- (Match Term, [Arg Term]) -> (Match Term, [Arg Term])
forall a b. (Match a, b) -> (Match a, b)
yesSimplification ((Match Term, [Arg Term]) -> (Match Term, [Arg Term]))
-> ReduceM (Match Term, [Arg Term])
-> ReduceM (Match Term, [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern]
-> [Arg Term] -> ReduceM (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
vs)
(Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
m, ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
bld ([Elim] -> [Arg Term] -> [Elim]
mergeElims [Elim]
vs [Arg Term]
vs1))
Nothing
-> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Match a
No , Arg Term
arg)
NotBlocked _ (MetaV x :: MetaId
x vs :: [Elim]
vs) -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked ()
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x () , Arg Term
arg)
Blocked x :: MetaId
x _ -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked ()
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x () , Arg Term
arg)
NotBlocked r :: NotBlocked
r _ -> (Match Term, Arg Term) -> ReduceM (Match Term, Arg Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked () -> Match Term
forall a. Blocked () -> Match a
DontKnow (Blocked () -> Match Term) -> Blocked () -> Match Term
forall a b. (a -> b) -> a -> b
$ NotBlocked -> () -> Blocked ()
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
r' () , Arg Term
arg)
where r' :: NotBlocked
r' = Elim -> NotBlocked -> NotBlocked
stuckOn (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg) NotBlocked
r
yesSimplification :: (Match a, b) -> (Match a, b)
yesSimplification :: (Match a, b) -> (Match a, b)
yesSimplification (Yes _ vs :: IntMap (Arg a)
vs, us :: b
us) = (Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg a)
vs, b
us)
yesSimplification r :: (Match a, b)
r = (Match a, b)
r
matchPatternP :: DeBruijnPattern
-> Arg DeBruijnPattern
-> ReduceM (Match DeBruijnPattern)
matchPatternP :: DeBruijnPattern
-> Arg DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
matchPatternP p :: DeBruijnPattern
p (Arg info :: ArgInfo
info (DotP _ v :: Term
v)) = do
(m :: Match Term
m, arg :: Arg Term
arg) <- DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern))
-> Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ (Term -> DeBruijnPattern) -> Match Term -> Match DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo) Match Term
m
matchPatternP p :: DeBruijnPattern
p arg :: Arg DeBruijnPattern
arg@(Arg info :: ArgInfo
info q :: DeBruijnPattern
q) = do
let varMatch :: DBPatVar -> m (Match DeBruijnPattern)
varMatch x :: DBPatVar
x = Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
-> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Simplification
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification (IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern)
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ (Int, Arg DeBruijnPattern) -> IntMap (Arg DeBruijnPattern)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg DeBruijnPattern
arg)
termMatch :: ReduceM (Match (Pattern' x))
termMatch = do
(m :: Match Term
m, arg :: Arg Term
arg) <- DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
matchPattern DeBruijnPattern
p ((DeBruijnPattern -> Term) -> Arg DeBruijnPattern -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm Arg DeBruijnPattern
arg)
Match (Pattern' x) -> ReduceM (Match (Pattern' x))
forall (m :: * -> *) a. Monad m => a -> m a
return (Match (Pattern' x) -> ReduceM (Match (Pattern' x)))
-> Match (Pattern' x) -> ReduceM (Match (Pattern' x))
forall a b. (a -> b) -> a -> b
$ (Term -> Pattern' x) -> Match Term -> Match (Pattern' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatternInfo -> Term -> Pattern' x
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo) Match Term
m
case DeBruijnPattern
p of
ProjP{} -> ReduceM (Match DeBruijnPattern)
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP _ _ _ x :: DBPatVar
x -> DBPatVar -> ReduceM (Match DeBruijnPattern)
forall (m :: * -> *).
Monad m =>
DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x
VarP _ x :: DBPatVar
x -> DBPatVar -> ReduceM (Match DeBruijnPattern)
forall (m :: * -> *).
Monad m =>
DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x
DotP _ _ -> Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern))
-> Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Simplification
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg DeBruijnPattern)
forall a. Null a => a
empty
LitP{} -> ReduceM (Match DeBruijnPattern)
forall x. ReduceM (Match (Pattern' x))
termMatch
DefP{} -> ReduceM (Match DeBruijnPattern)
forall x. ReduceM (Match (Pattern' x))
termMatch
ConP c :: ConHead
c cpi :: ConPatternInfo
cpi ps :: [NamedArg DeBruijnPattern]
ps ->
case DeBruijnPattern
q of
ConP c' :: ConHead
c' _ qs :: [NamedArg DeBruijnPattern]
qs | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' -> [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> ReduceM (Match DeBruijnPattern)
matchPatternsP [NamedArg DeBruijnPattern]
ps (((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
-> ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern]
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]
qs)
| Bool
otherwise -> Match DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
forall (m :: * -> *) a. Monad m => a -> m a
return Match DeBruijnPattern
forall a. Match a
No
LitP{} -> (Pattern' Any -> DeBruijnPattern)
-> Match (Pattern' Any) -> Match DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' Any -> DeBruijnPattern
forall x a. Pattern' x -> Pattern' a
toLitP (Match (Pattern' Any) -> Match DeBruijnPattern)
-> ReduceM (Match (Pattern' Any))
-> ReduceM (Match DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM (Match (Pattern' Any))
forall x. ReduceM (Match (Pattern' x))
termMatch
where toLitP :: Pattern' x -> Pattern' a
toLitP (DotP _ (Lit l :: Literal
l)) = Literal -> Pattern' a
forall a. Literal -> Pattern' a
litP Literal
l
toLitP _ = Pattern' a
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> ReduceM (Match DeBruijnPattern)
forall x. ReduceM (Match (Pattern' x))
termMatch
matchPatternsP :: [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern]
-> ReduceM (Match DeBruijnPattern)
matchPatternsP :: [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> ReduceM (Match DeBruijnPattern)
matchPatternsP ps :: [NamedArg DeBruijnPattern]
ps qs :: [Arg DeBruijnPattern]
qs = do
[Match DeBruijnPattern] -> Match DeBruijnPattern
forall a. Monoid a => [a] -> a
mconcat ([Match DeBruijnPattern] -> Match DeBruijnPattern)
-> ReduceM [Match DeBruijnPattern]
-> ReduceM (Match DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DeBruijnPattern
-> Arg DeBruijnPattern -> ReduceM (Match DeBruijnPattern))
-> [DeBruijnPattern]
-> [Arg DeBruijnPattern]
-> ReduceM [Match DeBruijnPattern]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DeBruijnPattern
-> Arg DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
matchPatternP ((NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg [NamedArg DeBruijnPattern]
ps) [Arg DeBruijnPattern]
qs