{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE OverloadedStrings #-}

module IR.Pattern.Anomaly where

import Common.Compiler (
  Error (..),
  ErrorMsg,
  MonadError (..),
  MonadWriter,
  Pass (..),
  Warning (..),
  fromString,
 )
import Common.Identifiers (
  Identifiable (..),
  Identifier (..),
  TConId (..),
 )
import Control.Monad (
  unless,
  when,
 )
import Control.Monad.Reader (
  MonadReader (..),
  ReaderT (..),
  asks,
 )
import Data.List (
  find,
 )
import qualified Data.Map as M
import qualified Data.Set as S

import qualified IR.IR as I
import IR.Pattern.Common (
  CInfo (..),
  TInfo (..),
  buildConsMap,
  buildTypeMap,
 )
import qualified IR.Pattern.Matrix as PM
import qualified IR.Pattern.Vector as PV


data AnomalyCtx = AnomalyCtx
  { AnomalyCtx -> Map Identifier TInfo
typeMap :: M.Map Identifier TInfo
  , AnomalyCtx -> Map Identifier CInfo
consMap :: M.Map Identifier CInfo
  }


newtype AnomalyFn a = AnomalyFn (ReaderT AnomalyCtx Pass a)
  deriving (a -> AnomalyFn b -> AnomalyFn a
(a -> b) -> AnomalyFn a -> AnomalyFn b
(forall a b. (a -> b) -> AnomalyFn a -> AnomalyFn b)
-> (forall a b. a -> AnomalyFn b -> AnomalyFn a)
-> Functor AnomalyFn
forall a b. a -> AnomalyFn b -> AnomalyFn a
forall a b. (a -> b) -> AnomalyFn a -> AnomalyFn b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> AnomalyFn b -> AnomalyFn a
$c<$ :: forall a b. a -> AnomalyFn b -> AnomalyFn a
fmap :: (a -> b) -> AnomalyFn a -> AnomalyFn b
$cfmap :: forall a b. (a -> b) -> AnomalyFn a -> AnomalyFn b
Functor) via (ReaderT AnomalyCtx Pass)
  deriving (Functor AnomalyFn
a -> AnomalyFn a
Functor AnomalyFn
-> (forall a. a -> AnomalyFn a)
-> (forall a b. AnomalyFn (a -> b) -> AnomalyFn a -> AnomalyFn b)
-> (forall a b c.
    (a -> b -> c) -> AnomalyFn a -> AnomalyFn b -> AnomalyFn c)
-> (forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b)
-> (forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn a)
-> Applicative AnomalyFn
AnomalyFn a -> AnomalyFn b -> AnomalyFn b
AnomalyFn a -> AnomalyFn b -> AnomalyFn a
AnomalyFn (a -> b) -> AnomalyFn a -> AnomalyFn b
(a -> b -> c) -> AnomalyFn a -> AnomalyFn b -> AnomalyFn c
forall a. a -> AnomalyFn a
forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn a
forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b
forall a b. AnomalyFn (a -> b) -> AnomalyFn a -> AnomalyFn b
forall a b c.
(a -> b -> c) -> AnomalyFn a -> AnomalyFn b -> AnomalyFn c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: AnomalyFn a -> AnomalyFn b -> AnomalyFn a
$c<* :: forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn a
*> :: AnomalyFn a -> AnomalyFn b -> AnomalyFn b
$c*> :: forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b
liftA2 :: (a -> b -> c) -> AnomalyFn a -> AnomalyFn b -> AnomalyFn c
$cliftA2 :: forall a b c.
(a -> b -> c) -> AnomalyFn a -> AnomalyFn b -> AnomalyFn c
<*> :: AnomalyFn (a -> b) -> AnomalyFn a -> AnomalyFn b
$c<*> :: forall a b. AnomalyFn (a -> b) -> AnomalyFn a -> AnomalyFn b
pure :: a -> AnomalyFn a
$cpure :: forall a. a -> AnomalyFn a
$cp1Applicative :: Functor AnomalyFn
Applicative) via (ReaderT AnomalyCtx Pass)
  deriving (Applicative AnomalyFn
a -> AnomalyFn a
Applicative AnomalyFn
-> (forall a b. AnomalyFn a -> (a -> AnomalyFn b) -> AnomalyFn b)
-> (forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b)
-> (forall a. a -> AnomalyFn a)
-> Monad AnomalyFn
AnomalyFn a -> (a -> AnomalyFn b) -> AnomalyFn b
AnomalyFn a -> AnomalyFn b -> AnomalyFn b
forall a. a -> AnomalyFn a
forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b
forall a b. AnomalyFn a -> (a -> AnomalyFn b) -> AnomalyFn b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> AnomalyFn a
$creturn :: forall a. a -> AnomalyFn a
>> :: AnomalyFn a -> AnomalyFn b -> AnomalyFn b
$c>> :: forall a b. AnomalyFn a -> AnomalyFn b -> AnomalyFn b
>>= :: AnomalyFn a -> (a -> AnomalyFn b) -> AnomalyFn b
$c>>= :: forall a b. AnomalyFn a -> (a -> AnomalyFn b) -> AnomalyFn b
$cp1Monad :: Applicative AnomalyFn
Monad) via (ReaderT AnomalyCtx Pass)
  deriving (Monad AnomalyFn
Monad AnomalyFn
-> (forall a. String -> AnomalyFn a) -> MonadFail AnomalyFn
String -> AnomalyFn a
forall a. String -> AnomalyFn a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> AnomalyFn a
$cfail :: forall a. String -> AnomalyFn a
$cp1MonadFail :: Monad AnomalyFn
MonadFail) via (ReaderT AnomalyCtx Pass)
  deriving (MonadError Error) via (ReaderT AnomalyCtx Pass)
  deriving (MonadWriter [Warning]) via (ReaderT AnomalyCtx Pass)
  deriving (MonadReader AnomalyCtx) via (ReaderT AnomalyCtx Pass)


buildCtx :: [(TConId, I.TypeDef)] -> AnomalyCtx
buildCtx :: [(TConId, TypeDef)] -> AnomalyCtx
buildCtx [(TConId, TypeDef)]
tds =
  AnomalyCtx :: Map Identifier TInfo -> Map Identifier CInfo -> AnomalyCtx
AnomalyCtx{typeMap :: Map Identifier TInfo
typeMap = [(TConId, TypeDef)] -> Map Identifier TInfo
buildTypeMap [(TConId, TypeDef)]
tds, consMap :: Map Identifier CInfo
consMap = [(TConId, TypeDef)] -> Map Identifier CInfo
buildConsMap [(TConId, TypeDef)]
tds}


-- | Run a AnomalyFn computation.
runAnomalyFn :: AnomalyFn a -> AnomalyCtx -> Pass a
runAnomalyFn :: AnomalyFn a -> AnomalyCtx -> Pass a
runAnomalyFn (AnomalyFn ReaderT AnomalyCtx Pass a
m) = ReaderT AnomalyCtx Pass a -> AnomalyCtx -> Pass a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT AnomalyCtx Pass a
m


checkProgram :: Show t => I.Program t -> Pass ()
checkProgram :: Program t -> Pass ()
checkProgram Program t
topdefs = ((Binder t, Expr t) -> AnomalyFn ())
-> [(Binder t, Expr t)] -> AnomalyFn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr (Expr t -> AnomalyFn ())
-> ((Binder t, Expr t) -> Expr t)
-> (Binder t, Expr t)
-> AnomalyFn ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Binder t, Expr t) -> Expr t
forall a b. (a, b) -> b
snd) [(Binder t, Expr t)]
ds AnomalyFn () -> AnomalyCtx -> Pass ()
forall a. AnomalyFn a -> AnomalyCtx -> Pass a
`runAnomalyFn` AnomalyCtx
ctx
 where
  tds :: [(TConId, TypeDef)]
tds = Program t -> [(TConId, TypeDef)]
forall t. Program t -> [(TConId, TypeDef)]
I.typeDefs Program t
topdefs
  ds :: [(Binder t, Expr t)]
ds = Program t -> [(Binder t, Expr t)]
forall t. Program t -> [(Binder t, Expr t)]
I.programDefs Program t
topdefs
  ctx :: AnomalyCtx
ctx = [(TConId, TypeDef)] -> AnomalyCtx
buildCtx [(TConId, TypeDef)]
tds


checkDefs :: Show t => [(I.VarId, I.Expr t)] -> AnomalyFn ()
checkDefs :: [(VarId, Expr t)] -> AnomalyFn ()
checkDefs = ((VarId, Expr t) -> AnomalyFn ())
-> [(VarId, Expr t)] -> AnomalyFn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(VarId
_, Expr t
e) -> Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr Expr t
e)


checkExprs :: Show t => [I.Expr t] -> AnomalyFn ()
checkExprs :: [Expr t] -> AnomalyFn ()
checkExprs = (Expr t -> AnomalyFn ()) -> [Expr t] -> AnomalyFn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr


checkExpr :: Show t => I.Expr t -> AnomalyFn ()
checkExpr :: Expr t -> AnomalyFn ()
checkExpr (I.Var VarId
_ t
_) = () -> AnomalyFn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkExpr (I.Data DConId
_ t
_) = () -> AnomalyFn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkExpr (I.Lit Literal
_ t
_) = () -> AnomalyFn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkExpr (I.App Expr t
e1 Expr t
e2 t
_) = [Expr t] -> AnomalyFn ()
forall t. Show t => [Expr t] -> AnomalyFn ()
checkExprs [Expr t
e1, Expr t
e2]
checkExpr (I.Let [(Binder t, Expr t)]
bindings Expr t
e t
_) =
  let ([Binder t]
_, [Expr t]
es) = [(Binder t, Expr t)] -> ([Binder t], [Expr t])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Binder t, Expr t)]
bindings in [Expr t] -> AnomalyFn ()
forall t. Show t => [Expr t] -> AnomalyFn ()
checkExprs [Expr t]
es AnomalyFn () -> AnomalyFn () -> AnomalyFn ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr Expr t
e
checkExpr (I.Lambda Binder t
_ Expr t
e t
_) = Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr Expr t
e
checkExpr (I.Match Expr t
e [(Alt t, Expr t)]
arms t
_) =
  let ([Alt t]
ps, [Expr t]
es) = [(Alt t, Expr t)] -> ([Alt t], [Expr t])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Alt t, Expr t)]
arms in Expr t -> AnomalyFn ()
forall t. Show t => Expr t -> AnomalyFn ()
checkExpr Expr t
e AnomalyFn () -> AnomalyFn () -> AnomalyFn ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr t] -> AnomalyFn ()
forall t. Show t => [Expr t] -> AnomalyFn ()
checkExprs [Expr t]
es AnomalyFn () -> AnomalyFn () -> AnomalyFn ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Alt t] -> AnomalyFn ()
forall t. Show t => [Alt t] -> AnomalyFn ()
checkPats [Alt t]
ps
checkExpr (I.Prim Primitive
_ [Expr t]
es t
_) = [Expr t] -> AnomalyFn ()
forall t. Show t => [Expr t] -> AnomalyFn ()
checkExprs [Expr t]
es
checkExpr (I.Exception ExceptType
_ t
_) = () -> AnomalyFn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


checkPats :: Show t => [I.Alt t] -> AnomalyFn ()
checkPats :: [Alt t] -> AnomalyFn ()
checkPats [Alt t]
ps = do
  [Alt t] -> AnomalyFn ()
forall t. Show t => [Alt t] -> AnomalyFn ()
checkUseless [Alt t]
ps
  [Alt t] -> AnomalyFn ()
forall t. Show t => [Alt t] -> AnomalyFn ()
checkExhaustive [Alt t]
ps


checkUseless :: Show t => [I.Alt t] -> AnomalyFn ()
checkUseless :: [Alt t] -> AnomalyFn ()
checkUseless [Alt t]
ps = ((PatMat t, PatVec t) -> AnomalyFn ())
-> [(PatMat t, PatVec t)] -> AnomalyFn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((PatMat t -> PatVec t -> AnomalyFn ())
-> (PatMat t, PatVec t) -> AnomalyFn ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry PatMat t -> PatVec t -> AnomalyFn ()
forall t. Show t => PatMat t -> PatVec t -> AnomalyFn ()
checkUselessEach) [(PatMat t, PatVec t)]
cases
 where
  checkUselessEach :: PatMat t -> PatVec t -> AnomalyFn ()
checkUselessEach PatMat t
pm PatVec t
p = do
    Bool
u <- PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful PatMat t
pm PatVec t
p
    Bool -> AnomalyFn () -> AnomalyFn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
      Bool
u
      ( Error -> AnomalyFn ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> AnomalyFn ()) -> Error -> AnomalyFn ()
forall a b. (a -> b) -> a -> b
$
          ErrorMsg -> Error
PatternError (ErrorMsg -> Error) -> ErrorMsg -> Error
forall a b. (a -> b) -> a -> b
$
            ErrorMsg
"Pattern is useless"
              ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> (String -> ErrorMsg
forall a. IsString a => String -> a
fromString (String -> ErrorMsg)
-> (PatVec t -> String) -> PatVec t -> ErrorMsg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVec t -> String
forall a. Show a => a -> String
show (PatVec t -> ErrorMsg) -> PatVec t -> ErrorMsg
forall a b. (a -> b) -> a -> b
$ PatVec t
p)
      )
  cases :: [(PatMat t, PatVec t)]
cases =
    let vecs :: [PatVec t]
vecs = (Alt t -> PatVec t) -> [Alt t] -> [PatVec t]
forall a b. (a -> b) -> [a] -> [b]
map (\Alt t
pat -> [Alt t] -> PatVec t
forall t. [Alt t] -> PatVec t
PV.fromList [Alt t
pat]) [Alt t]
ps
        pats :: [PatMat t]
pats = (PatVec t -> PatMat t) -> [PatVec t] -> [PatMat t]
forall a b. (a -> b) -> [a] -> [b]
map PatVec t -> PatMat t
forall t. PatVec t -> PatMat t
PM.fromPatVec [PatVec t]
vecs
        emptyMat :: PatMat t
emptyMat = let PatMat t
p : [PatMat t]
_ = [PatMat t]
pats in Int -> PatMat t
forall t. Int -> PatMat t
PM.emptyWithCols (Int -> PatMat t) -> Int -> PatMat t
forall a b. (a -> b) -> a -> b
$ PatMat t -> Int
forall t. PatMat t -> Int
PM.ncol PatMat t
p
        patsBeforeIdx :: [PatMat t]
patsBeforeIdx =
          let accumRows :: ([PatMat t], PatMat t) -> PatMat t -> ([PatMat t], PatMat t)
accumRows = (\([PatMat t]
ms, PatMat t
m) PatMat t
p -> (PatMat t
m PatMat t -> [PatMat t] -> [PatMat t]
forall a. a -> [a] -> [a]
: [PatMat t]
ms, PatMat t -> PatMat t -> PatMat t
forall t. PatMat t -> PatMat t -> PatMat t
PM.extend PatMat t
m PatMat t
p))
              ([PatMat t]
pms, PatMat t
_) = (([PatMat t], PatMat t) -> PatMat t -> ([PatMat t], PatMat t))
-> ([PatMat t], PatMat t) -> [PatMat t] -> ([PatMat t], PatMat t)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([PatMat t], PatMat t) -> PatMat t -> ([PatMat t], PatMat t)
forall t.
([PatMat t], PatMat t) -> PatMat t -> ([PatMat t], PatMat t)
accumRows ([], PatMat t
forall t. PatMat t
emptyMat) [PatMat t]
pats
           in [PatMat t] -> [PatMat t]
forall a. [a] -> [a]
reverse [PatMat t]
pms
     in [PatMat t] -> [PatVec t] -> [(PatMat t, PatVec t)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PatMat t]
patsBeforeIdx [PatVec t]
vecs


checkExhaustive :: Show t => [I.Alt t] -> AnomalyFn ()
checkExhaustive :: [Alt t] -> AnomalyFn ()
checkExhaustive [Alt t]
ps = do
  let pm :: PatMat t
pm = [Alt t] -> PatMat t
forall t. [Alt t] -> PatMat t
PM.singleCol [Alt t]
ps
      ty :: t
ty = Alt t -> t
forall (c :: * -> *) a. Carrier c => c a -> a
I.extract (Alt t -> t) -> Alt t -> t
forall a b. (a -> b) -> a -> b
$ [Alt t] -> Alt t
forall a. [a] -> a
head [Alt t]
ps
  Bool
u <- PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful PatMat t
pm (Alt t -> PatVec t
forall t. Alt t -> PatVec t
PV.singleton (Alt t -> PatVec t) -> Alt t -> PatVec t
forall a b. (a -> b) -> a -> b
$ Binder t -> Alt t
forall t. Binder t -> Alt t
I.AltBinder (t -> Binder t
forall t. t -> Binder t
I.BindAnon t
ty))
  Bool -> AnomalyFn () -> AnomalyFn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
    Bool
u
    ( Error -> AnomalyFn ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> AnomalyFn ()) -> Error -> AnomalyFn ()
forall a b. (a -> b) -> a -> b
$
        ErrorMsg -> Error
PatternError (ErrorMsg -> Error) -> ErrorMsg -> Error
forall a b. (a -> b) -> a -> b
$
          ErrorMsg
"Patterns are not exhaustive"
            ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> (String -> ErrorMsg
forall a. IsString a => String -> a
fromString (String -> ErrorMsg) -> ([Alt t] -> String) -> [Alt t] -> ErrorMsg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Alt t] -> String
forall a. Show a => a -> String
show ([Alt t] -> ErrorMsg) -> [Alt t] -> ErrorMsg
forall a b. (a -> b) -> a -> b
$ [Alt t]
ps)
    )


useful :: PM.PatMat t -> PV.PatVec t -> AnomalyFn Bool
useful :: PatMat t -> PatVec t -> AnomalyFn Bool
useful PatMat t
pm PatVec t
pv = do
  case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (PatMat t -> Int
forall t. PatMat t -> Int
PM.ncol PatMat t
pm) Int
0 of
    Ordering
LT -> AnomalyFn Bool
forall a. AnomalyFn a
throwMalformedError
    Ordering
EQ -> AnomalyFn Bool
baseCase
    Ordering
GT -> PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
usefulInductive PatMat t
pm PatVec t
pv
 where
  baseCase :: AnomalyFn Bool
baseCase = Bool -> AnomalyFn Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> AnomalyFn Bool) -> Bool -> AnomalyFn Bool
forall a b. (a -> b) -> a -> b
$ PatMat t -> Int
forall t. PatMat t -> Int
PM.nrow PatMat t
pm Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0


usefulInductive :: PM.PatMat t -> PV.PatVec t -> AnomalyFn Bool
usefulInductive :: PatMat t -> PatVec t -> AnomalyFn Bool
usefulInductive PatMat t
pm PatVec t
pv =
  let wildCase :: AnomalyFn Bool
wildCase = case PatMat t -> Maybe (Alt t)
forall t. PatMat t -> Maybe (Alt t)
samplePat PatMat t
pm of
        Maybe (Alt t)
Nothing -> PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful (PatMat t -> PatMat t
forall t. PatMat t -> PatMat t
PM.defaultize PatMat t
pm) (PatVec t -> PatVec t
forall t. PatVec t -> PatVec t
PV.tl PatVec t
pv)
        Just Alt t
sample ->
          let wildCaseCons :: Identifier -> AnomalyFn Bool
wildCaseCons Identifier
cid = do
                CInfo
c <- Identifier -> AnomalyFn CInfo
askCInfo Identifier
cid
                TInfo
t <- Identifier -> AnomalyFn TInfo
askTInfo (CInfo -> Identifier
cType CInfo
c)
                if Set Identifier -> PatMat t -> Bool
forall t. Set Identifier -> PatMat t -> Bool
hasCompleteCons (TInfo -> Set Identifier
tCSet TInfo
t) PatMat t
pm
                  then
                    let f :: Identifier -> AnomalyFn Bool
f Identifier
ck = do
                          CInfo
ck' <- Identifier -> AnomalyFn CInfo
askCInfo Identifier
ck
                          let arity :: Int
arity = CInfo -> Int
cArity CInfo
ck'
                          PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful
                            (Int -> Identifier -> PatMat t -> PatMat t
forall t. Int -> Identifier -> PatMat t -> PatMat t
PM.specializeCons Int
arity Identifier
ck PatMat t
pm)
                            (Int -> PatVec t -> PatVec t
forall t. Int -> PatVec t -> PatVec t
PV.specializeWild Int
arity PatVec t
pv)
                     in ([Bool] -> Bool) -> AnomalyFn [Bool] -> AnomalyFn Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (AnomalyFn [Bool] -> AnomalyFn Bool)
-> ([Identifier] -> AnomalyFn [Bool])
-> [Identifier]
-> AnomalyFn Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Identifier -> AnomalyFn Bool) -> [Identifier] -> AnomalyFn [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Identifier -> AnomalyFn Bool
f ([Identifier] -> AnomalyFn Bool) -> [Identifier] -> AnomalyFn Bool
forall a b. (a -> b) -> a -> b
$ Set Identifier -> [Identifier]
forall a. Set a -> [a]
S.toList (TInfo -> Set Identifier
tCSet TInfo
t)
                  else PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful (PatMat t -> PatMat t
forall t. PatMat t -> PatMat t
PM.defaultize PatMat t
pm) (PatVec t -> PatVec t
forall t. PatVec t -> PatVec t
PV.tl PatVec t
pv)
           in case Alt t
sample of
                I.AltLit{} -> PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful (PatMat t -> PatMat t
forall t. PatMat t -> PatMat t
PM.defaultize PatMat t
pm) (PatVec t -> PatVec t
forall t. PatVec t -> PatVec t
PV.tl PatVec t
pv)
                I.AltData (I.DConId Identifier
i) [Alt t]
_ t
_ -> Identifier -> AnomalyFn Bool
wildCaseCons Identifier
i
                I.AltBinder Binder t
_ -> String -> AnomalyFn Bool
forall a. HasCallStack => String -> a
error String
"can't happen"
   in case PatVec t -> Alt t
forall t. PatVec t -> Alt t
PV.hd PatVec t
pv of
        I.AltBinder Binder t
_ -> AnomalyFn Bool
wildCase
        I.AltData (I.DConId Identifier
i) [Alt t]
_ t
_ -> do
          CInfo
c <- Identifier -> AnomalyFn CInfo
askCInfo Identifier
i
          PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful (Int -> Identifier -> PatMat t -> PatMat t
forall t. Int -> Identifier -> PatMat t -> PatMat t
PM.specializeCons (CInfo -> Int
cArity CInfo
c) Identifier
i PatMat t
pm) (PatVec t -> PatVec t
forall t. PatVec t -> PatVec t
PV.specialize PatVec t
pv)
        I.AltLit Literal
lit t
_ -> PatMat t -> PatVec t -> AnomalyFn Bool
forall t. PatMat t -> PatVec t -> AnomalyFn Bool
useful (Literal -> PatMat t -> PatMat t
forall t. Literal -> PatMat t -> PatMat t
PM.specializeLit Literal
lit PatMat t
pm) (PatVec t -> PatVec t
forall t. PatVec t -> PatVec t
PV.specialize PatVec t
pv)


samplePat :: PM.PatMat t -> Maybe (I.Alt t)
samplePat :: PatMat t -> Maybe (Alt t)
samplePat PatMat t
pm = case Maybe (PatVec t)
firstConsPatVec of
  Maybe (PatVec t)
Nothing -> Maybe (Alt t)
forall a. Maybe a
Nothing
  Just PatVec t
pv -> Alt t -> Maybe (Alt t)
forall t. Alt t -> Maybe (Alt t)
stripPat (PatVec t -> Alt t
forall t. PatVec t -> Alt t
PV.hd PatVec t
pv)
 where
  firstConsPatVec :: Maybe (PatVec t)
firstConsPatVec = (PatVec t -> Bool) -> [PatVec t] -> Maybe (PatVec t)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Alt t -> Bool
forall t. Alt t -> Bool
isConstructor (Alt t -> Bool) -> (PatVec t -> Alt t) -> PatVec t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVec t -> Alt t
forall t. PatVec t -> Alt t
PV.hd) (PatMat t -> [PatVec t]
forall t. PatMat t -> [PatVec t]
PM.toList PatMat t
pm)
   where
    isConstructor :: Alt t -> Bool
isConstructor Alt t
p = case Alt t
p of
      I.AltLit{} -> Bool
True
      I.AltData{} -> Bool
True
      I.AltBinder Binder t
_ -> Bool
False
  stripPat :: Alt t -> Maybe (Alt t)
stripPat Alt t
p = case Alt t
p of
    I.AltLit{} -> Alt t -> Maybe (Alt t)
forall a. a -> Maybe a
Just Alt t
p
    I.AltData{} -> Alt t -> Maybe (Alt t)
forall a. a -> Maybe a
Just Alt t
p
    I.AltBinder (I.BindAnon t
_) -> String -> Maybe (Alt t)
forall a. HasCallStack => String -> a
error String
"can't happen"
    I.AltBinder Binder t
_ -> Alt t -> Maybe (Alt t)
forall a. a -> Maybe a
Just Alt t
p


askCInfo :: Identifier -> AnomalyFn CInfo
askCInfo :: Identifier -> AnomalyFn CInfo
askCInfo Identifier
i = do
  Maybe CInfo
cs <- (AnomalyCtx -> Maybe CInfo) -> AnomalyFn (Maybe CInfo)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((AnomalyCtx -> Maybe CInfo) -> AnomalyFn (Maybe CInfo))
-> (AnomalyCtx -> Maybe CInfo) -> AnomalyFn (Maybe CInfo)
forall a b. (a -> b) -> a -> b
$ Identifier -> Map Identifier CInfo -> Maybe CInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Identifier
i (Map Identifier CInfo -> Maybe CInfo)
-> (AnomalyCtx -> Map Identifier CInfo)
-> AnomalyCtx
-> Maybe CInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnomalyCtx -> Map Identifier CInfo
consMap
  case Maybe CInfo
cs of
    Maybe CInfo
Nothing ->
      Error -> AnomalyFn CInfo
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> AnomalyFn CInfo) -> Error -> AnomalyFn CInfo
forall a b. (a -> b) -> a -> b
$
        ErrorMsg -> Error
PatternError (ErrorMsg -> Error) -> ErrorMsg -> Error
forall a b. (a -> b) -> a -> b
$
          ErrorMsg
"askArity: Data constructor does not exist: "
            ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> Identifier -> ErrorMsg
showId Identifier
i
    Just CInfo
cs' -> CInfo -> AnomalyFn CInfo
forall (m :: * -> *) a. Monad m => a -> m a
return CInfo
cs'


askTInfo :: Identifier -> AnomalyFn TInfo
askTInfo :: Identifier -> AnomalyFn TInfo
askTInfo Identifier
i = do
  Maybe TInfo
ts <- (AnomalyCtx -> Maybe TInfo) -> AnomalyFn (Maybe TInfo)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((AnomalyCtx -> Maybe TInfo) -> AnomalyFn (Maybe TInfo))
-> (AnomalyCtx -> Maybe TInfo) -> AnomalyFn (Maybe TInfo)
forall a b. (a -> b) -> a -> b
$ Identifier -> Map Identifier TInfo -> Maybe TInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Identifier
i (Map Identifier TInfo -> Maybe TInfo)
-> (AnomalyCtx -> Map Identifier TInfo)
-> AnomalyCtx
-> Maybe TInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnomalyCtx -> Map Identifier TInfo
typeMap
  case Maybe TInfo
ts of
    Maybe TInfo
Nothing ->
      Error -> AnomalyFn TInfo
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> AnomalyFn TInfo) -> Error -> AnomalyFn TInfo
forall a b. (a -> b) -> a -> b
$
        ErrorMsg -> Error
PatternError (ErrorMsg -> Error) -> ErrorMsg -> Error
forall a b. (a -> b) -> a -> b
$
          ErrorMsg
"askArity: Data constructor does not exist: "
            ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> Identifier -> ErrorMsg
showId Identifier
i
    Just TInfo
ts' -> TInfo -> AnomalyFn TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return TInfo
ts'


hasCompleteCons :: S.Set Identifier -> PM.PatMat t -> Bool
hasCompleteCons :: Set Identifier -> PatMat t -> Bool
hasCompleteCons Set Identifier
cset PatMat t
pm = Set Identifier
forall a. Set a
S.empty Set Identifier -> Set Identifier -> Bool
forall a. Eq a => a -> a -> Bool
== (PatVec t -> Set Identifier -> Set Identifier)
-> Set Identifier -> [PatVec t] -> Set Identifier
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PatVec t -> Set Identifier -> Set Identifier
forall t. PatVec t -> Set Identifier -> Set Identifier
removeC Set Identifier
cset (PatMat t -> [PatVec t]
forall t. PatMat t -> [PatVec t]
PM.toList PatMat t
pm)
 where
  removeC :: PatVec t -> Set Identifier -> Set Identifier
removeC PatVec t
pv Set Identifier
cset' = Alt t -> Set Identifier -> Set Identifier
forall t. Alt t -> Set Identifier -> Set Identifier
removeC' (PatVec t -> Alt t
forall t. PatVec t -> Alt t
PV.hd PatVec t
pv) Set Identifier
cset'
  removeC' :: Alt t -> Set Identifier -> Set Identifier
removeC' Alt t
p Set Identifier
cset' = case Alt t
p of
    I.AltData (I.DConId Identifier
i) [Alt t]
_ t
_ -> Identifier -> Set Identifier -> Set Identifier
forall a. Ord a => a -> Set a -> Set a
S.delete Identifier
i Set Identifier
cset'
    I.AltBinder (I.BindVar (I.VarId Identifier
i) t
_) -> Identifier -> Set Identifier -> Set Identifier
forall a. Ord a => a -> Set a -> Set a
S.delete Identifier
i Set Identifier
cset'
    Alt t
_ -> Set Identifier
cset'


-- | Report 'Identifier' for error reporting.
showId :: Identifier -> ErrorMsg
showId :: Identifier -> ErrorMsg
showId Identifier
s = ErrorMsg
"'" ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> String -> ErrorMsg
forall a. IsString a => String -> a
fromString (Identifier -> String
forall i. Identifiable i => i -> String
ident Identifier
s) ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> ErrorMsg
"'"


showSet :: S.Set Identifier -> ErrorMsg
showSet :: Set Identifier -> ErrorMsg
showSet Set Identifier
set = ErrorMsg
"'" ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> String -> ErrorMsg
forall a. IsString a => String -> a
fromString (Set Identifier -> String
forall a. Show a => a -> String
show Set Identifier
set) ErrorMsg -> ErrorMsg -> ErrorMsg
forall a. Semigroup a => a -> a -> a
<> ErrorMsg
"'"


throwMalformedError :: AnomalyFn a
throwMalformedError :: AnomalyFn a
throwMalformedError = Error -> AnomalyFn a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> AnomalyFn a) -> Error -> AnomalyFn a
forall a b. (a -> b) -> a -> b
$ ErrorMsg -> Error
PatternError ErrorMsg
"Pattern is not well-formed."