{-# LANGUAGE OverloadedStrings #-}

-- | This module is loosely based off /Warnings for pattern matching/ by Luc
-- Maranget
module Language.Dickinson.Pattern.Useless ( PatternM
                                          , PatternEnv
                                          , runPatternM
                                          , isExhaustive
                                          , patternEnvDecls
                                          , useful
                                          -- * Exported for testing
                                          , specializeTuple
                                          , specializeTag
                                          ) where

import           Control.Monad              (forM_)
import           Control.Monad.State.Strict (State, execState)
import           Data.Coerce                (coerce)
import           Data.Foldable              (toList, traverse_)
import           Data.Functor               (void)
import           Data.IntMap.Strict         (findWithDefault)
import qualified Data.IntMap.Strict         as IM
import qualified Data.IntSet                as IS
import           Language.Dickinson.Name
import           Language.Dickinson.Type
import           Language.Dickinson.Unique
import           Lens.Micro                 (Lens')
import           Lens.Micro.Mtl             (modifying)

-- all constructors of a
data PatternEnv = PatternEnv { PatternEnv -> IntMap IntSet
allCons :: IM.IntMap IS.IntSet -- ^ all constructors indexed by type
                             , PatternEnv -> IntMap Int
types   :: IM.IntMap Int -- ^ all types indexed by constructor
                             }

allConsLens :: Lens' PatternEnv (IM.IntMap IS.IntSet)
allConsLens :: Lens' PatternEnv (IntMap IntSet)
allConsLens IntMap IntSet -> f (IntMap IntSet)
f PatternEnv
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap IntSet
x -> PatternEnv
s { allCons :: IntMap IntSet
allCons = IntMap IntSet
x }) (IntMap IntSet -> f (IntMap IntSet)
f (PatternEnv -> IntMap IntSet
allCons PatternEnv
s))

typesLens :: Lens' PatternEnv (IM.IntMap Int)
typesLens :: Lens' PatternEnv (IntMap Int)
typesLens IntMap Int -> f (IntMap Int)
f PatternEnv
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap Int
x -> PatternEnv
s { types :: IntMap Int
types = IntMap Int
x }) (IntMap Int -> f (IntMap Int)
f (PatternEnv -> IntMap Int
types PatternEnv
s))

declAdd :: Declaration a -> PatternM ()
declAdd :: forall a. Declaration a -> PatternM ()
declAdd Define{}         = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
declAdd (TyDecl a
_ (Name NonEmpty Text
_ (Unique Int
i) a
_) NonEmpty (Name a)
cs) = do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ NonEmpty (Name a)
cs forall a b. (a -> b) -> a -> b
$ \(Name NonEmpty Text
_ (Unique Int
j) a
_) ->
        forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying Lens' PatternEnv (IntMap Int)
typesLens (forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
j Int
i)
    let cons :: IntSet
cons = [Int] -> IntSet
IS.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Unique -> Int
unUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name a -> Unique
unique forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Name a)
cs)
    forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying Lens' PatternEnv (IntMap IntSet)
allConsLens (forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i IntSet
cons)

patternEnvDecls :: [Declaration a] -> PatternM ()
patternEnvDecls :: forall a. [Declaration a] -> PatternM ()
patternEnvDecls = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Declaration a -> PatternM ()
declAdd

-- TODO: just reader monad... writer at beginning?
type PatternM = State PatternEnv

runPatternM :: PatternM a -> PatternEnv
runPatternM :: forall a. PatternM a -> PatternEnv
runPatternM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState (IntMap IntSet -> IntMap Int -> PatternEnv
PatternEnv forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)

-- given a constructor name, get the IntSet of all constructors of that type
assocUniques :: PatternEnv -> Name a -> IS.IntSet
assocUniques :: forall a. PatternEnv -> Name a -> IntSet
assocUniques PatternEnv
env (Name NonEmpty Text
_ (Unique Int
i) a
_) = {-# SCC "assocUniques" #-}
    let ty :: Int
ty = forall a. a -> Int -> IntMap a -> a
findWithDefault forall a. a
internalError Int
i (PatternEnv -> IntMap Int
types PatternEnv
env)
        in forall a. a -> Int -> IntMap a -> a
findWithDefault forall a. a
internalError Int
ty (PatternEnv -> IntMap IntSet
allCons PatternEnv
env)

internalError :: a
internalError :: forall a. a
internalError = forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: lookup in a PatternEnv failed"

isExhaustive :: PatternEnv -> [Pattern a] -> Bool
isExhaustive :: forall a. PatternEnv -> [Pattern a] -> Bool
isExhaustive PatternEnv
env [Pattern a]
ps = {-# SCC "isExhaustive" #-} Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. PatternEnv -> [Pattern a] -> Pattern a -> Bool
useful PatternEnv
env [Pattern a]
ps (forall a. a -> Pattern a
Wildcard forall a. HasCallStack => a
undefined)

isCompleteSet :: PatternEnv -> [Name a] -> Maybe [Name ()]
isCompleteSet :: forall a. PatternEnv -> [Name a] -> Maybe [Name ()]
isCompleteSet PatternEnv
_ []       = forall a. Maybe a
Nothing
isCompleteSet PatternEnv
env ns :: [Name a]
ns@(Name a
n:[Name a]
_) =
    let allU :: IntSet
allU = forall a. PatternEnv -> Name a -> IntSet
assocUniques PatternEnv
env Name a
n
        ty :: [Int]
ty = coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. Name a -> Unique
unique forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name a]
ns)
        in if IntSet -> Bool
IS.null (IntSet
allU IntSet -> IntSet -> IntSet
IS.\\ [Int] -> IntSet
IS.fromList [Int]
ty)
            then forall a. a -> Maybe a
Just ((\Int
u -> forall a. NonEmpty Text -> Unique -> a -> Name a
Name forall a. HasCallStack => a
undefined (Int -> Unique
Unique Int
u) ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> [Int]
IS.toList IntSet
allU)
            else forall a. Maybe a
Nothing

useful :: PatternEnv -> [Pattern a] -> Pattern a -> Bool
useful :: forall a. PatternEnv -> [Pattern a] -> Pattern a -> Bool
useful PatternEnv
env [Pattern a]
ps Pattern a
p = forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env [[Pattern a
p'] | Pattern a
p' <- [Pattern a]
ps] [Pattern a
p]

sanityFailed :: a
sanityFailed :: forall a. a
sanityFailed = forall a. HasCallStack => [Char] -> a
error [Char]
"Sanity check failed! Perhaps you ran the pattern match exhaustiveness checker on an ill-typed program?"

specializeTag :: Name a -> [[Pattern a]] -> [[Pattern a]]
specializeTag :: forall a. Name a -> [[Pattern a]] -> [[Pattern a]]
specializeTag Name a
c = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [Pattern a] -> [[Pattern a]]
withRow
    where withRow :: [Pattern a] -> [[Pattern a]]
withRow (PatternCons a
_ Name a
c':[Pattern a]
ps) | Name a
c' forall a. Eq a => a -> a -> Bool
== Name a
c = [[Pattern a]
ps]
                                        | Bool
otherwise = []
          withRow (PatternTuple{}:[Pattern a]
_)    = forall a. a
sanityFailed
          withRow (Wildcard{}:[Pattern a]
ps)       = [[Pattern a]
ps]
          withRow (PatternVar{}:[Pattern a]
ps)     = [[Pattern a]
ps]
          withRow (OrPattern a
_ NonEmpty (Pattern a)
rs:[Pattern a]
ps)   = forall a. Name a -> [[Pattern a]] -> [[Pattern a]]
specializeTag Name a
c [Pattern a
rforall a. a -> [a] -> [a]
:[Pattern a]
ps | Pattern a
r <- forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
rs] -- TODO: unit test case for this
          withRow []                    = forall a. a
emptySpecialize

specializeTuple :: Int -> [[Pattern a]] -> [[Pattern a]]
specializeTuple :: forall a. Int -> [[Pattern a]] -> [[Pattern a]]
specializeTuple Int
n = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. [Pattern a] -> [[Pattern a]]
withRow
    where withRow :: [Pattern a] -> [[Pattern a]]
withRow (PatternTuple a
_ NonEmpty (Pattern a)
ps:[Pattern a]
ps') = [forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
ps forall a. [a] -> [a] -> [a]
++ [Pattern a]
ps']
          withRow (p :: Pattern a
p@Wildcard{}:[Pattern a]
ps')      = [forall a. Int -> a -> [a]
replicate Int
n Pattern a
p forall a. [a] -> [a] -> [a]
++ [Pattern a]
ps']
          withRow (p :: Pattern a
p@PatternVar{}:[Pattern a]
ps')    = [forall a. Int -> a -> [a]
replicate Int
n Pattern a
p forall a. [a] -> [a] -> [a]
++ [Pattern a]
ps']
          withRow (OrPattern a
_ NonEmpty (Pattern a)
rs:[Pattern a]
ps)     = forall a. Int -> [[Pattern a]] -> [[Pattern a]]
specializeTuple Int
n [Pattern a
rforall a. a -> [a] -> [a]
:[Pattern a]
ps | Pattern a
r <- forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
rs]
          withRow (PatternCons{}:[Pattern a]
_)       = forall a. a
sanityFailed
          withRow []                      = forall a. a
emptySpecialize

emptySpecialize :: a
emptySpecialize :: forall a. a
emptySpecialize = forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: tried to take specialized matrix of an empty row"

-- | \\( \matcal(D) \\) in the Maranget paper
defaultMatrix :: [[Pattern a]] -> [[Pattern a]]
defaultMatrix :: forall a. [[Pattern a]] -> [[Pattern a]]
defaultMatrix = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. [Pattern a] -> [[Pattern a]]
withRow where
    withRow :: [Pattern a] -> [[Pattern a]]
withRow []                  = forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: tried to take default matrix of an empty row"
    withRow (PatternTuple{}:[Pattern a]
_)  = forall a. HasCallStack => [Char] -> a
error [Char]
"Sanity check failed!" -- because a tuple would be complete by itself
    withRow (PatternCons{}:[Pattern a]
_)   = []
    withRow (Wildcard{}:[Pattern a]
ps)     = [[Pattern a]
ps]
    withRow (PatternVar{}:[Pattern a]
ps)   = [[Pattern a]
ps]
    withRow (OrPattern a
_ NonEmpty (Pattern a)
rs:[Pattern a]
ps) = forall a. [[Pattern a]] -> [[Pattern a]]
defaultMatrix [Pattern a
rforall a. a -> [a] -> [a]
:[Pattern a]
ps | Pattern a
r <- forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
rs]

data Complete a = NotComplete
                | CompleteTuple Int
                | CompleteTags [Name a]

extrCons :: Pattern a -> [Name a]
extrCons :: forall a. Pattern a -> [Name a]
extrCons (PatternCons a
_ TyName a
c) = [TyName a
c]
extrCons (OrPattern a
_ NonEmpty (Pattern a)
ps)  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. Pattern a -> [Name a]
extrCons (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
ps)
extrCons Pattern a
_                 = []

-- Is the first column of the pattern matrix complete?
fstComplete :: PatternEnv -> [[Pattern a]] -> Complete ()
fstComplete :: forall a. PatternEnv -> [[Pattern a]] -> Complete ()
fstComplete PatternEnv
env [[Pattern a]]
ps = {-# SCC "fstComplete" #-}
    if Int
maxTupleLength forall a. Ord a => a -> a -> Bool
> Int
0
        then forall a. Int -> Complete a
CompleteTuple Int
maxTupleLength
        else forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Complete a
NotComplete forall a. [Name a] -> Complete a
CompleteTags
                forall a b. (a -> b) -> a -> b
$ forall a. PatternEnv -> [Name a] -> Maybe [Name ()]
isCompleteSet PatternEnv
env (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. Pattern a -> [Name a]
extrCons [Pattern a]
fstColumn)
    where fstColumn :: [Pattern a]
fstColumn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> a
head [[Pattern a]]
ps
          tuple :: Pattern a -> Int
tuple (PatternTuple a
_ NonEmpty (Pattern a)
ps') = forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (Pattern a)
ps'
          tuple (OrPattern a
_ NonEmpty (Pattern a)
ps')    = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Pattern a -> Int
tuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Pattern a)
ps')
          tuple Pattern a
_                    = Int
0
          maxTupleLength :: Int
maxTupleLength = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (forall {a}. Pattern a -> Int
tuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern a]
fstColumn)

-- follows maranget paper
usefulMaranget :: PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget :: forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
_ [] [Pattern a]
_                       = Bool
True
usefulMaranget PatternEnv
_ [[Pattern a]]
_ []                       = Bool
False
usefulMaranget PatternEnv
env [[Pattern a]]
ps (PatternCons a
_ TyName a
c:[Pattern a]
qs)    = forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env (forall a. Name a -> [[Pattern a]] -> [[Pattern a]]
specializeTag TyName a
c [[Pattern a]]
ps) [Pattern a]
qs
usefulMaranget PatternEnv
env [[Pattern a]]
ps (PatternTuple a
_ NonEmpty (Pattern a)
ps':[Pattern a]
qs) = forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env (forall a. Int -> [[Pattern a]] -> [[Pattern a]]
specializeTuple (forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (Pattern a)
ps') [[Pattern a]]
ps) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Pattern a)
ps' forall a. [a] -> [a] -> [a]
++ [Pattern a]
qs)
usefulMaranget PatternEnv
env [[Pattern a]]
ps (OrPattern a
_ NonEmpty (Pattern a)
ps':[Pattern a]
qs)    = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Pattern a
p -> forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env [[Pattern a]]
ps (Pattern a
pforall a. a -> [a] -> [a]
:[Pattern a]
qs)) NonEmpty (Pattern a)
ps'
usefulMaranget PatternEnv
env [[Pattern a]]
ps (Pattern a
q:[Pattern a]
qs)                  = -- var or wildcard
    let cont :: Complete ()
cont = forall a. PatternEnv -> [[Pattern a]] -> Complete ()
fstComplete PatternEnv
env [[Pattern a]]
ps in
    case Complete ()
cont of
        Complete ()
NotComplete     -> forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env (forall a. [[Pattern a]] -> [[Pattern a]]
defaultMatrix [[Pattern a]]
ps) [Pattern a]
qs
        CompleteTuple Int
n -> forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env (forall a. Int -> [[Pattern a]] -> [[Pattern a]]
specializeTuple Int
n [[Pattern a]]
ps) (forall a. Int -> Pattern a -> [Pattern a] -> [Pattern a]
specializeTupleVector Int
n Pattern a
q [Pattern a]
qs)
        CompleteTags [Name ()]
ns -> forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name ()
n -> forall a. PatternEnv -> [[Pattern a]] -> [Pattern a] -> Bool
usefulMaranget PatternEnv
env (forall a. Name a -> [[Pattern a]] -> [[Pattern a]]
specializeTag Name ()
n (forall a. [[Pattern a]] -> [[Pattern ()]]
forget [[Pattern a]]
ps)) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Functor f => f a -> f ()
void [Pattern a]
qs)) [Name ()]
ns

specializeTupleVector :: Int -> Pattern a -> [Pattern a] -> [Pattern a]
specializeTupleVector :: forall a. Int -> Pattern a -> [Pattern a] -> [Pattern a]
specializeTupleVector Int
n Pattern a
p [Pattern a]
ps = {-# SCC "specializeTupleVector" #-} forall a. Int -> a -> [a]
replicate Int
n Pattern a
p forall a. [a] -> [a] -> [a]
++ [Pattern a]
ps

forget :: [[Pattern a]] -> [[Pattern ()]]
forget :: forall a. [[Pattern a]] -> [[Pattern ()]]
forget = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Functor f => f a -> f ()
void)