# LANGUAGE 
   DeriveFunctor 
 , FlexibleContexts 
 , FlexibleInstances 
 , GADTs 
 , OverloadedStrings 
 , ScopedTypeVariables 
 , StandaloneDeriving 
 , TupleSections 
 , UndecidableInstances #
  DeriveFunctor
, FlexibleContexts
, FlexibleInstances
, GADTs
, OverloadedStrings
, ScopedTypeVariables
, StandaloneDeriving
, TupleSections
, UndecidableInstances #-}

  | Helpers for pattern totality checking 

 This is based on the " GADTs meet their match " paper[1 ] , with some minor 
 modifications : 

  - Amulet is non - lazy , and so pattern evaluation order is not 
    defined . Thus we need not consider the " diverging " case in the 
    paper . We also merge computation of the covered and uncovered sets 
    into one computation . 

  - We introduce tuples and record patterns , which are effectively treated 
    as single - constructor types ( they themselves are always matched , and 
    decompose to a single thing ) . 

  - Value abstractions also contain a " literal " and " not literal " case , 
    which match against a single literal , and a set of " all literals but 
    these " . 

 There are a couple of improvements we could in the future , if needs 
 arise : 

  - We currently do not implement variable+pattern constraints , as we do 
    not currently have view patterns . 

  - Our handling of guards is rather naive ( just discard the uncovered set 
    in this case ) . It is worth considering how we can improve this , while 
    still taking into account the lack of purity guarantees . 

  - We could optimise the handling of non - GADT destructure patterns so we 
    do not need to generate as many free type variables , and can rely less 
    on the unifier . The paper[1 ] discusses some ways of doing this . 

  - Improve out handling of uninhabited types . Our checking of 
    inhabitedness is rather naive , and just ducks out on recursive types , 
    even if they are trivially uninhabited ( say , type a = A of a ) . We 
    should also check whether types are inhabited on non - empty arms . 

 [ 1 ] : -us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf 



This is based on the "GADTs meet their match" paper[1], with some minor
modifications:

 - Amulet is non-lazy, and so pattern evaluation order is not
   defined. Thus we need not consider the "diverging" case in the
   paper. We also merge computation of the covered and uncovered sets
   into one computation.

 - We introduce tuples and record patterns, which are effectively treated
   as single-constructor types (they themselves are always matched, and
   decompose to a single thing).

 - Value abstractions also contain a "literal" and "not literal" case,
   which match against a single literal, and a set of "all literals but
   these".

There are a couple of improvements we could in the future, if needs
arise:

 - We currently do not implement variable+pattern constraints, as we do
   not currently have view patterns.

 - Our handling of guards is rather naive (just discard the uncovered set
   in this case). It is worth considering how we can improve this, while
   still taking into account the lack of purity guarantees.

 - We could optimise the handling of non-GADT destructure patterns so we
   do not need to generate as many free type variables, and can rely less
   on the unifier. The paper[1] discusses some ways of doing this.

 - Improve out handling of uninhabited types. Our checking of
   inhabitedness is rather naive, and just ducks out on recursive types,
   even if they are trivially uninhabited (say, type a = A of a). We
   should also check whether types are inhabited on non-empty arms.

[1]: -us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf

-}
module Syntax.Verify.Pattern
  ( Covering, covered, uncovered
  , ValueAbs(..)
  , AbsState
  , emptyAbsState, emptyAlt
  , covering
  , inhabited
  ) where

import Control.Monad.State.Strict
import Control.Monad.Chronicles
import Control.Monad.Namey
import Control.Monad.Infer
import Control.Applicative
import Control.Lens

import qualified Data.Map.Lazy as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Bifunctor
import Data.Foldable
import Data.Reason
import Data.These
import Data.Maybe

import Syntax.Types hiding (constructors)
import Syntax

import Types.Infer.Builtin (expandTypeWith)
import Types.Infer.Pattern (skolGadt)
import Types.Unify

import Text.Pretty.Semantic hiding (empty)

-- | Represents both the covered and uncovered set of a computation.
--
-- This could be thought of as a unification of the list and maybe monad.
data Covering a
  = Covering { covered'   :: Seq.Seq a
             , uncovered' :: Seq.Seq a
             }
  -- | Represents a "pure" version of the covered set. We use this to
  -- represent values constructed via "pure" (and so both the covered and
  -- uncovered sets are identical).
  | PureCovering { pureCover :: Seq.Seq a }
  deriving (Show, Functor)

covered, uncovered :: Covering a -> Seq.Seq a
covered (Covering c _) = c
covered (PureCovering c) = c

uncovered (Covering _ u) = u
uncovered (PureCovering u) = u

instance Applicative Covering where
  pure x = PureCovering (pure x)

  (PureCovering f) <*> (PureCovering x) = PureCovering (f <*> x)
  (Covering fc fu) <*> (Covering xc xu) = Covering (fc <*> xc) (fu <*> xu)
  (Covering fc fu) <*> (PureCovering x) = Covering (fc <*> x) (fu <*> x)
  (PureCovering f) <*> (Covering xc xu) = Covering (f <*> xc) (f <*> xu)

instance Alternative Covering where
  empty = PureCovering empty

  (PureCovering l) <|> (PureCovering r) = PureCovering (l <|> r)
  (Covering lc lu) <|> (Covering rc ru) = Covering (lc <|> rc) (lu <|> ru)
  (Covering lc lu) <|> (PureCovering r) = Covering (lc <|> r) (lu <|> r)
  (PureCovering l) <|> (Covering rc ru) = Covering (l <|> rc) (l <|> ru)

instance Monad Covering where
  (Covering c u) >>= f = Covering (c >>= covered . f) (u >>= uncovered . f)
  (PureCovering x) >>= f = asum (f <$> x)

instance MonadPlus Covering where

class Monad m => MonadCover m where
  -- | Return a computation representing just a covered value.
  cover :: a -> m a
  -- | Return a computation representing just an uncovered value.
  uncover :: a -> m a

instance MonadCover Covering where
  cover x = Covering (pure x) empty
  uncover x = Covering empty (pure x)

instance (Monad (t m), MonadCover m, MonadTrans t) => MonadCover (t m) where
  cover = lift . cover
  uncover = lift . uncover

-- | An abstract representation of a value.
--
-- With the exception of 'VNotLiteral', this is a subset of both
-- expressions and patterns, and allows representing what values are
-- covered and uncovered by a given pattern.
data ValueAbs p
  = VVariable (Var p) (Type p)
  | VDestructure (Var p) (Maybe (ValueAbs p))
  | VRecord (Map.Map T.Text (ValueAbs p))
  | VTuple (ValueAbs p) (ValueAbs p)

  | VLiteral Lit
  | VNotLiteral (Var p) (Set.Set Lit)

deriving instance ShowPhrase p => Show (ValueAbs p)

instance Pretty (Var p) => Pretty (ValueAbs p) where
  pretty VVariable{} = skeyword "_"
  pretty (VDestructure k Nothing) = stypeCon (pretty k)
  pretty (VDestructure k (Just p)) = stypeCon (pretty k) <+>
    case p of
      VDestructure _ Just{} -> parens (prettyIn p)
      _ -> prettyIn p
  pretty (VRecord fs)
    -- Should we filter out wildcard fields here?
    = enclose (lbrace <> space) (space <> rbrace)
    . hsep . punctuate comma
    . map (\(n, v) -> text n <+> equals <+> prettyIn v)
    . Map.toList $ fs
  pretty t@VTuple{} = hsep . punctuate comma . extract $ t where
    extract (VTuple l r) = prettyIn l : extract r
    extract p = [prettyIn p]

  pretty (VLiteral l) = pretty l
  pretty VNotLiteral{} = skeyword "_"

-- | Pretty-print an internal value
prettyIn :: Pretty (Var p) => ValueAbs p -> Doc
prettyIn v@VTuple{} = parens (pretty v)
prettyIn v = pretty v

  | Wraps the state of one pattern alternative , capturing constraints ,
-- substitution sets and the latest fresh variable.
data AbsState
  = AbsState
  { altSub :: SolveState
  , altTyc :: Seq.Seq (Constraint Typed)
  , altFresh :: VarResolved
  }
  deriving (Show)

-- | Construct an empty pattern abstraction state from a fresh variable,
emptyAbsState :: Var Typed -> AbsState
emptyAbsState = AbsState emptyState mempty

-- | Construct an empty value abstraction from a abstraction state and
-- the type of the test variable.
emptyAlt :: AbsState -> Type Typed -> (AbsState, ValueAbs Typed)
emptyAlt alt ty =
  let v@(TgName _ i) = altFresh alt
  in (alt { altFresh = TgName "a" (i + 1) }, VVariable v ty)

-- | A type-safe list of constraints between patterns and value
-- abstractions.
--
-- We use this to ensure that each iteration of the solver consumes and
-- produces exactly the same number of terms.
data PatPair a where
  Nil :: PatPair ()
  (:*:) :: (Pattern Typed, ValueAbs Typed) -> PatPair b -> PatPair (ValueAbs Typed, b)

infixr 9 :*:

-- | Extract the pattern part of a 'PatPair', suitable for building an
-- uncovered set.
patPair :: PatPair a -> a
patPair Nil = ()
patPair ((_, x) :*: xs) = (x, patPair xs)

type CoverState = (SolveState, Seq.Seq (Constraint Typed))

-- | The type of the covering monad
type CoveringM = StateT CoverState (NameyT Covering)

-- | Run the value abstraction monad.
covering :: Env -> Pattern Typed
         -> Seq.Seq (AbsState, ValueAbs Typed)
         -> Covering (AbsState, ValueAbs Typed)
covering env p xs = msum . flip fmap xs $ \(AbsState st cs i, v) -> do
  (((v', ()), (st', cs')), i') <- flip runNameyT i
                                . flip runStateT (st, cs)
                                $ covering' env ((p, v) :*: Nil)
  pure (AbsState st' cs' i', v')

covering' :: Env -> PatPair a -> CoveringM a
covering' env = go where
  go :: PatPair a -> CoveringM a

  -- Nil
  go Nil = cover ()

  -- FIXME: This is unquestionably wrong!
  go ((POr l _ _, v) :*: xs) = go ((l, v) :*: xs)

  -- ConCon for constructors: If the constructors are the same, just
  -- recurse. Otherwise, that constructor is uncovered.
  go ((Destructure k (Just p) _, v@(VDestructure k' (Just u))) :*: xs)
    | k == k' = first (VDestructure k' . Just) <$> go ((p, u):*:xs)
    | otherwise = uncover (v, patPair xs)
  go ((Destructure k Nothing _, v@(VDestructure k' Nothing)) :*: xs)
    | k == k' = (VDestructure k' Nothing,) <$> go xs
    | otherwise = uncover (v, patPair xs)
  go ((Destructure{}, v@VDestructure{}) :*: xs) = uncover (v, patPair xs)

  go ((PGadtCon k _ _ (Just p) _, v@(VDestructure k' (Just u))) :*: xs)
    | k == k' = first (VDestructure k' . Just) <$> go ((p, u):*:xs)
    | otherwise = uncover (v, patPair xs)
  go ((PGadtCon k _ _ Nothing _, v@(VDestructure k' Nothing)) :*: xs)
    | k == k' = (VDestructure k' Nothing,) <$> go xs
    | otherwise = uncover (v, patPair xs)
  go ((PGadtCon{}, v@VDestructure{}) :*: xs) = uncover (v, patPair xs)

  ConVar for constructors : We always perform the UConVar implementation here -
  -- namely we find every possible case.
  go ((p@(Destructure _ _ (_, ty)), VVariable v vTy) :*: xs) = do
    (k, arg) <- constructors env ty vTy
    maybe (pure ()) guardInhabited arg
    guardAll xs
    case arg of
      Nothing -> onVar p v (VDestructure k Nothing) xs
      Just arg -> do
        v' <- genName
        onVar p v (VDestructure k (Just (VVariable v' arg))) xs

  go ((p@(PGadtCon _ _ _ _ (_, ty)), VVariable v vTy) :*: xs) = do
    (k, arg) <- constructors env ty vTy
    maybe (pure ()) guardInhabited arg
    guardAll xs
    case arg of
      Nothing -> onVar p v (VDestructure k Nothing) xs
      Just arg -> do
        v' <- genName
        onVar p v (VDestructure k (Just (VVariable v' arg))) xs

  go ((Destructure{}, _) :*: _) = error "Mismatch on Destructure"
  go ((PGadtCon{}, _) :*: _) = error "Mismatch on PGadtCon"

  -- ConCon for literals
  go ((PLiteral li _, v@(VLiteral li')) :*: xs)
    | li == li' = (v,) <$> go xs
    | otherwise = uncover (v, patPair xs)

  -- ConCon for bounded literals: Like normal constructors, we can just enumerate each value.
  go ((p@(PLiteral LiUnit{} _), VVariable v _) :*: xs) = onVar p v (VLiteral LiUnit) xs
  go ((p@(PLiteral LiBool{} _), VVariable v _) :*: xs)
    =   onVar p v (VLiteral (LiBool True)) xs
    <|> onVar p v (VLiteral (LiBool False)) xs

  -- For other literals, we have an infinite number of values, so we
  -- consider this specific literal, and the set of all other literals.
  go ((p@(PLiteral li _), VVariable v _) :*: xs)
    =   onVar p v (VLiteral li) xs
    <|> onVar p v (VNotLiteral v (Set.singleton li)) xs
  This case is a little messy , as it 's both  and ConVar . Namely , if
  -- we're not in the excluded set, treat it as a variable. If we are, treat it
  -- as a constructor (and so it is uncovered).
  go ((p@(PLiteral li _), n@(VNotLiteral v lis)) :*: xs)
    | li `Set.notMember` lis
      =   onVar p v (VLiteral li) xs
      <|> onVar p v (VNotLiteral v (Set.insert li lis)) xs
    | otherwise = uncover (n, patPair xs)

  go ((PLiteral{}, _) :*: _) = error "Mismatch on PLiteral"

  -- As tuple patterns can be of differing sizes, we can't just zip them
  -- up. Thus we represent them as pairs, and hope it all works out.
  go ((PTuple [p] _, u) :*: xs) = go ((p, u) :*: xs)
  -- ConCon for tuples: This always matches, so we just visit the children.
  go ((PTuple (p1:p2) a, VTuple u1 u2) :*: xs) = do
    (u1', (u2', xs')) <- go ((p1, u1) :*: (mkTuple p2 a, u2) :*: xs)
    pure (VTuple u1' u2', xs')
  ConVar for tuples : This always matches , so we just build up child value
  -- abstractions and then visit as normal.
  go ((p@(PTuple _ _), VVariable v vTy) :*: xs) = do
    (ty1, ty2) <- tupleTy vTy
    u1 <- flip VVariable ty1 <$> genName
    u2 <- flip VVariable ty2 <$> genName
    onVar p v (VTuple u1 u2) xs

  go ((PTuple{}, _) :*: _) = error "Mismatch on PTuple"

  -- ConCon for records: This always matches, so we just visit each field.
  go ((PRecord ps _, VRecord us') :*: xs) = first VRecord <$> foldRecord ps us' xs
  ConVar for records : This always matches , so we build up a child value for
  -- each field and visit as normal.
  go ((p@(PRecord _ (_, ty)), VVariable v vTy) :*: xs) = do
    constrain [mkUni vTy ty]
    us <- traverse (\ty -> flip VVariable ty <$> genName) (rowTy ty)
    onVar p v (VRecord us) xs
  go ((PRecord{}, _) :*: _) = error "Mismatch on PTuple"

  Var : Match the remaining patterns , extend the environment , and unify the
  -- bound variable with the abstraction.
  go ((w@(Wildcard _), u) :*: xs) = do
    guardInhabited (getType w)
    (u,) <$> go xs
  go ((w@(Capture v _), u) :*: xs) = do
    constrainVal v u
    guardInhabited (getType w)
    (u,) <$> go xs
  go ((PAs p v _, u) :*: xs) = onVar p v u xs

  -- Boring wrappers
  go ((PType p _ _, u) :*: xs) = go ((p, u) :*: xs)
  go ((PList{}, _) :*: _) = error "PList is handled by desugar"

  -- | Add a unification constraint between a variable and value
  -- abstraction, then continue matching
  onVar :: Pattern Typed -> Var Typed -> ValueAbs Typed -> PatPair a -> CoveringM (ValueAbs Typed, a)
  onVar p v u xs = constrainVal v u >> go ((p, u) :*: xs)

  mkTuple [] _ = error "Empty tuple"
  mkTuple [x] _ = x
  mkTuple xs a = PTuple xs a

  tupleTy (TyTuple t1 t2) = pure (t1, t2)
  tupleTy ty = do
    v1 <- freshTV; v2 <- freshTV
    constrain [mkUni ty (TyTuple v1 v2)]
    pure (v1, v2)

  rowTy TyVar{} = mempty
  rowTy (TyRows f fs) = rowTy f <> Map.fromList fs
  rowTy (TyExactRows fs) = Map.fromList fs
  rowTy (TyParens t) = rowTy t
  rowTy (TyWithConstraints _ t) = rowTy t
  rowTy t = error $ "Cannot get row from "++ show t

  -- | Abort if this type is uninhabited.
  guardInhabited :: Type Typed -> CoveringM ()
  guardInhabited ty = do
    (solve, cs) <- get
    name <- genName
    unless (inhabited env (AbsState solve cs name) ty) mzero

  -- | Abort if the remaining pairs are uninhabited.
  guardAll :: PatPair a -> CoveringM ()
  guardAll Nil = pure ()
  guardAll ((x, _) :*: xs) = do
    guardInhabited (getType x)
    guardAll xs

  -- | Visit over each field in a record
  foldRecord :: [(T.Text, Pattern Typed)] -> Map.Map T.Text (ValueAbs Typed)
             -> PatPair a -> CoveringM (Map.Map T.Text (ValueAbs Typed), a)
  foldRecord [] vs xs = (vs,) <$> go xs
  foldRecord ((f, p):fs) us xs = do
    let u = fromMaybe (error $ "Cannot find field " ++ show f ++ " in record") (Map.lookup f us)
    (us', (u', xs')) <- foldRecord fs us ((p, u) :*: xs)
    pure (Map.insert f u' us', xs')

-- | Return all constructors matching this constraint
constructors :: (MonadPlus m, MonadState CoverState m, MonadNamey m)
             => Env -> Type Typed -> Type Typed
             -> m (Var Typed, Maybe (Type Typed))
constructors env kty vty = do
  k <- asum . map pure . toList . ctors $ kty
  (pty, _) <- skolGadt k =<< instantiate Strong Expression (fromJust (env ^. (names . at k)))
  let (cs, ty) = case pty of
                   TyWithConstraints cs ty -> (cs, ty)
                   _ -> ([], pty)
      (arg, res) = unwrapCtor ty

  Unify our result with the child , including any additional GADT constraints .
  constrain (mkUni res (expandTypeWith (env ^. tySyms) vty):map (uncurry mkUni) cs)
  pure (k, arg)

  where
    -- | Get the constructors for a given type
    ctors :: Type Typed -> Set.Set (Var Typed)
    ctors (TyCon v _) = maybe (error $ "Cannot find constructors for " ++ show v) _tdConstructors (env ^. (types . at v))
    ctors (TyApp f _) = ctors f
    ctors t = error $ "Cannot get type name from " ++ show (pretty t)

    -- | Unwrap a constructor, returning the argument and result type
    unwrapCtor :: Type p -> (Maybe (Type p), Type p)
    unwrapCtor (TyPi bind res) = case bind of
      Anon arg -> (Just arg, res)
      Implicit _ -> unwrapCtor res
      Invisible {} -> unwrapCtor res
    unwrapCtor (TyWithConstraints _ t) = unwrapCtor t
    unwrapCtor (TyParens t) = unwrapCtor t
    unwrapCtor t = (Nothing, t)

-- | Determines if a given type is inhabited
inhabited :: Env -> AbsState -> Type Typed -> Bool
inhabited env (AbsState st cs i)
  = not . Seq.null
  . flip evalNameyT i
  . flip evalStateT (st, cs)
  . go mempty
  where

  inhb :: Monad m => m ()
  inhb = pure ()

  go :: (MonadPlus m, MonadNamey m, MonadState CoverState m)
     => Set.Set (Var Typed) -> Type Typed -> m ()
  go c (TyVar v _) = do
    let c' = Set.insert v c
    t' <- gets (typeWithin v . fst)
    case t' of
      -- If there's no substitution, or a loop in the substitution, assume it's inhabited.
      Nothing -> inhb
      Just (TyVar v' _) | Set.member v' c' -> inhb
      Just t' -> go c' t'

  go c t@TyApp{} = ctorCheck c t
  go c t@TyCon{} = ctorCheck c t
  -- We don't really have the concept of uninhabited types, so we assume
  -- type names are.
  go _ TyPromotedCon{} = inhb
  -- For now, we'll just assume all Pi types are inhabited. Thankfully,
  -- they all are.
  go _ TyPi{} = inhb
  -- All the boring types: just determine if the children are inhabited
  go c (TyRows f fs) = go c f >> traverse_ (go c . snd) fs
  go c (TyExactRows fs) = traverse_ (go c . snd) fs
  go c (TyTuple l r) = go c l >> go c r
  go c (TyOperator l v r) = go c (TyApp (TyApp v l) r)
  go c (TyWildcard t) = maybe inhb (go c) t
  go c (TyParens t) = go c t

  go _ TySkol{} = inhb
  go c (TyWithConstraints _ t) = go c t
  go _ TyType = inhb
  go _ TyLit{} = inhb
  go _ TyTupleL{} = inhb

  | Returns the type name if this type is concrete ( defined as has 0 or more
  -- constructors, rather than being abstract).
  --
  -- We pass in a set of previously visited type names to avoid getting into
  -- loops.
  concreteTy c (TyCon v _)
    | v `Set.notMember` c
    , isJust (env ^. (types . at v))
    = Just v
    | otherwise = Nothing
  concreteTy c (TyApp f _) = concreteTy c f
  concreteTy _ _ = Nothing

  -- | A naive check to determine if a constructor is inhabited.
  ctorCheck :: (MonadPlus m, MonadNamey m, MonadState CoverState m)
            => Set.Set (Var Typed) -> Type Typed -> m ()
  ctorCheck c t
    | Just v <- concreteTy c t =
        case maybe Unknown _tdInhabited (env ^. (types . at v)) of
          Uninhabited -> mzero
          Inhabited -> inhb
          Unknown ->
            do
            let c' = Set.insert v c
            (_, arg) <- constructors env t t
            maybe inhb (go c') arg
    | otherwise = inhb

-- | Make a unification constraint
mkUni :: Type Typed -> Type Typed -> Constraint Typed
mkUni = ConUnify (It'sThis (BecauseInternal "pmcheck")) mempty undefined

  | Add one or more type constraints into the current environment ,
-- failing if an error occurs.
constrain :: (MonadPlus m, MonadNamey m, MonadState CoverState m) => [Constraint Typed] -> m ()
constrain css = maybe empty put =<< doConstrain css where
  doConstrain css = do
    (sub, cs) <- get
    x <- runChronicleT . solveImplies sub mempty . (cs<>) $ Seq.fromList css
    pure $ case x of
      These Seq.Empty (sub', cs') -> Just (sub', Seq.fromList cs')
      That (sub', cs') ->  Just (sub', Seq.fromList cs')
      These _ _ -> Nothing
      This _ -> Nothing

-- | Require a variable to match a given pattern
--
-- Note this is not currently used, but may do something useful in the
-- future when we add view patterns.
constrainVal :: Var Typed -> ValueAbs Typed -> CoveringM ()
constrainVal _ _ = pure ()

 | Represents both the covered and uncovered set of a computation.

 This could be thought of as a unification of the list and maybe monad.
 | Represents a "pure" version of the covered set. We use this to
 represent values constructed via "pure" (and so both the covered and
 uncovered sets are identical).
 | Return a computation representing just a covered value.
 | Return a computation representing just an uncovered value.
 | An abstract representation of a value.

 With the exception of 'VNotLiteral', this is a subset of both
 expressions and patterns, and allows representing what values are
 covered and uncovered by a given pattern.
 Should we filter out wildcard fields here?
 | Pretty-print an internal value
 substitution sets and the latest fresh variable.
 | Construct an empty pattern abstraction state from a fresh variable,
 | Construct an empty value abstraction from a abstraction state and
 the type of the test variable.
 | A type-safe list of constraints between patterns and value
 abstractions.

 We use this to ensure that each iteration of the solver consumes and
 produces exactly the same number of terms.
 | Extract the pattern part of a 'PatPair', suitable for building an
 uncovered set.
 | The type of the covering monad
 | Run the value abstraction monad.
 Nil
 FIXME: This is unquestionably wrong!
 ConCon for constructors: If the constructors are the same, just
 recurse. Otherwise, that constructor is uncovered.
 namely we find every possible case.
 ConCon for literals
 ConCon for bounded literals: Like normal constructors, we can just enumerate each value.
 For other literals, we have an infinite number of values, so we
 consider this specific literal, and the set of all other literals.
 we're not in the excluded set, treat it as a variable. If we are, treat it
 as a constructor (and so it is uncovered).
 As tuple patterns can be of differing sizes, we can't just zip them
 up. Thus we represent them as pairs, and hope it all works out.
 ConCon for tuples: This always matches, so we just visit the children.
 abstractions and then visit as normal.
 ConCon for records: This always matches, so we just visit each field.
 each field and visit as normal.
 bound variable with the abstraction.
 Boring wrappers
 | Add a unification constraint between a variable and value
 abstraction, then continue matching
 | Abort if this type is uninhabited.
 | Abort if the remaining pairs are uninhabited.
 | Visit over each field in a record
 | Return all constructors matching this constraint
 | Get the constructors for a given type
 | Unwrap a constructor, returning the argument and result type
 | Determines if a given type is inhabited
 If there's no substitution, or a loop in the substitution, assume it's inhabited.
 We don't really have the concept of uninhabited types, so we assume
 type names are.
 For now, we'll just assume all Pi types are inhabited. Thankfully,
 they all are.
 All the boring types: just determine if the children are inhabited
 constructors, rather than being abstract).

 We pass in a set of previously visited type names to avoid getting into
 loops.
 | A naive check to determine if a constructor is inhabited.
 | Make a unification constraint
 failing if an error occurs.
 | Require a variable to match a given pattern

 Note this is not currently used, but may do something useful in the
 future when we add view patterns.
# LANGUAGE 
   DeriveFunctor 
 , FlexibleContexts 
 , FlexibleInstances 
 , GADTs 
 , OverloadedStrings 
 , ScopedTypeVariables 
 , StandaloneDeriving 
 , TupleSections 
 , UndecidableInstances #
  DeriveFunctor
, FlexibleContexts
, FlexibleInstances
, GADTs
, OverloadedStrings
, ScopedTypeVariables
, StandaloneDeriving
, TupleSections
, UndecidableInstances #-}

  | Helpers for pattern totality checking 

 This is based on the " GADTs meet their match " paper[1 ] , with some minor 
 modifications : 

  - Amulet is non - lazy , and so pattern evaluation order is not 
    defined . Thus we need not consider the " diverging " case in the 
    paper . We also merge computation of the covered and uncovered sets 
    into one computation . 

  - We introduce tuples and record patterns , which are effectively treated 
    as single - constructor types ( they themselves are always matched , and 
    decompose to a single thing ) . 

  - Value abstractions also contain a " literal " and " not literal " case , 
    which match against a single literal , and a set of " all literals but 
    these " . 

 There are a couple of improvements we could in the future , if needs 
 arise : 

  - We currently do not implement variable+pattern constraints , as we do 
    not currently have view patterns . 

  - Our handling of guards is rather naive ( just discard the uncovered set 
    in this case ) . It is worth considering how we can improve this , while 
    still taking into account the lack of purity guarantees . 

  - We could optimise the handling of non - GADT destructure patterns so we 
    do not need to generate as many free type variables , and can rely less 
    on the unifier . The paper[1 ] discusses some ways of doing this . 

  - Improve out handling of uninhabited types . Our checking of 
    inhabitedness is rather naive , and just ducks out on recursive types , 
    even if they are trivially uninhabited ( say , type a = A of a ) . We 
    should also check whether types are inhabited on non - empty arms . 

 [ 1 ] : -us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf 



This is based on the "GADTs meet their match" paper[1], with some minor
modifications:

 - Amulet is non-lazy, and so pattern evaluation order is not
   defined. Thus we need not consider the "diverging" case in the
   paper. We also merge computation of the covered and uncovered sets
   into one computation.

 - We introduce tuples and record patterns, which are effectively treated
   as single-constructor types (they themselves are always matched, and
   decompose to a single thing).

 - Value abstractions also contain a "literal" and "not literal" case,
   which match against a single literal, and a set of "all literals but
   these".

There are a couple of improvements we could in the future, if needs
arise:

 - We currently do not implement variable+pattern constraints, as we do
   not currently have view patterns.

 - Our handling of guards is rather naive (just discard the uncovered set
   in this case). It is worth considering how we can improve this, while
   still taking into account the lack of purity guarantees.

 - We could optimise the handling of non-GADT destructure patterns so we
   do not need to generate as many free type variables, and can rely less
   on the unifier. The paper[1] discusses some ways of doing this.

 - Improve out handling of uninhabited types. Our checking of
   inhabitedness is rather naive, and just ducks out on recursive types,
   even if they are trivially uninhabited (say, type a = A of a). We
   should also check whether types are inhabited on non-empty arms.

[1]: -us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf

-}
module Syntax.Verify.Pattern
  ( Covering, covered, uncovered
  , ValueAbs(..)
  , AbsState
  , emptyAbsState, emptyAlt
  , covering
  , inhabited
  ) where

import Control.Monad.State.Strict
import Control.Monad.Chronicles
import Control.Monad.Namey
import Control.Monad.Infer
import Control.Applicative
import Control.Lens

import qualified Data.Map.Lazy as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Bifunctor
import Data.Foldable
import Data.Reason
import Data.These
import Data.Maybe

import Syntax.Types hiding (constructors)
import Syntax

import Types.Infer.Builtin (expandTypeWith)
import Types.Infer.Pattern (skolGadt)
import Types.Unify

import Text.Pretty.Semantic hiding (empty)

data Covering a
  = Covering { covered'   :: Seq.Seq a
             , uncovered' :: Seq.Seq a
             }
  | PureCovering { pureCover :: Seq.Seq a }
  deriving (Show, Functor)

covered, uncovered :: Covering a -> Seq.Seq a
covered (Covering c _) = c
covered (PureCovering c) = c

uncovered (Covering _ u) = u
uncovered (PureCovering u) = u

instance Applicative Covering where
  pure x = PureCovering (pure x)

  (PureCovering f) <*> (PureCovering x) = PureCovering (f <*> x)
  (Covering fc fu) <*> (Covering xc xu) = Covering (fc <*> xc) (fu <*> xu)
  (Covering fc fu) <*> (PureCovering x) = Covering (fc <*> x) (fu <*> x)
  (PureCovering f) <*> (Covering xc xu) = Covering (f <*> xc) (f <*> xu)

instance Alternative Covering where
  empty = PureCovering empty

  (PureCovering l) <|> (PureCovering r) = PureCovering (l <|> r)
  (Covering lc lu) <|> (Covering rc ru) = Covering (lc <|> rc) (lu <|> ru)
  (Covering lc lu) <|> (PureCovering r) = Covering (lc <|> r) (lu <|> r)
  (PureCovering l) <|> (Covering rc ru) = Covering (l <|> rc) (l <|> ru)

instance Monad Covering where
  (Covering c u) >>= f = Covering (c >>= covered . f) (u >>= uncovered . f)
  (PureCovering x) >>= f = asum (f <$> x)

instance MonadPlus Covering where

class Monad m => MonadCover m where
  cover :: a -> m a
  uncover :: a -> m a

instance MonadCover Covering where
  cover x = Covering (pure x) empty
  uncover x = Covering empty (pure x)

instance (Monad (t m), MonadCover m, MonadTrans t) => MonadCover (t m) where
  cover = lift . cover
  uncover = lift . uncover

data ValueAbs p
  = VVariable (Var p) (Type p)
  | VDestructure (Var p) (Maybe (ValueAbs p))
  | VRecord (Map.Map T.Text (ValueAbs p))
  | VTuple (ValueAbs p) (ValueAbs p)

  | VLiteral Lit
  | VNotLiteral (Var p) (Set.Set Lit)

deriving instance ShowPhrase p => Show (ValueAbs p)

instance Pretty (Var p) => Pretty (ValueAbs p) where
  pretty VVariable{} = skeyword "_"
  pretty (VDestructure k Nothing) = stypeCon (pretty k)
  pretty (VDestructure k (Just p)) = stypeCon (pretty k) <+>
    case p of
      VDestructure _ Just{} -> parens (prettyIn p)
      _ -> prettyIn p
  pretty (VRecord fs)
    = enclose (lbrace <> space) (space <> rbrace)
    . hsep . punctuate comma
    . map (\(n, v) -> text n <+> equals <+> prettyIn v)
    . Map.toList $ fs
  pretty t@VTuple{} = hsep . punctuate comma . extract $ t where
    extract (VTuple l r) = prettyIn l : extract r
    extract p = [prettyIn p]

  pretty (VLiteral l) = pretty l
  pretty VNotLiteral{} = skeyword "_"

prettyIn :: Pretty (Var p) => ValueAbs p -> Doc
prettyIn v@VTuple{} = parens (pretty v)
prettyIn v = pretty v

  | Wraps the state of one pattern alternative , capturing constraints ,
data AbsState
  = AbsState
  { altSub :: SolveState
  , altTyc :: Seq.Seq (Constraint Typed)
  , altFresh :: VarResolved
  }
  deriving (Show)

emptyAbsState :: Var Typed -> AbsState
emptyAbsState = AbsState emptyState mempty

emptyAlt :: AbsState -> Type Typed -> (AbsState, ValueAbs Typed)
emptyAlt alt ty =
  let v@(TgName _ i) = altFresh alt
  in (alt { altFresh = TgName "a" (i + 1) }, VVariable v ty)

data PatPair a where
  Nil :: PatPair ()
  (:*:) :: (Pattern Typed, ValueAbs Typed) -> PatPair b -> PatPair (ValueAbs Typed, b)

infixr 9 :*:

patPair :: PatPair a -> a
patPair Nil = ()
patPair ((_, x) :*: xs) = (x, patPair xs)

type CoverState = (SolveState, Seq.Seq (Constraint Typed))

type CoveringM = StateT CoverState (NameyT Covering)

covering :: Env -> Pattern Typed
         -> Seq.Seq (AbsState, ValueAbs Typed)
         -> Covering (AbsState, ValueAbs Typed)
covering env p xs = msum . flip fmap xs $ \(AbsState st cs i, v) -> do
  (((v', ()), (st', cs')), i') <- flip runNameyT i
                                . flip runStateT (st, cs)
                                $ covering' env ((p, v) :*: Nil)
  pure (AbsState st' cs' i', v')

covering' :: Env -> PatPair a -> CoveringM a
covering' env = go where
  go :: PatPair a -> CoveringM a

  go Nil = cover ()

  go ((POr l _ _, v) :*: xs) = go ((l, v) :*: xs)

  go ((Destructure k (Just p) _, v@(VDestructure k' (Just u))) :*: xs)
    | k == k' = first (VDestructure k' . Just) <$> go ((p, u):*:xs)
    | otherwise = uncover (v, patPair xs)
  go ((Destructure k Nothing _, v@(VDestructure k' Nothing)) :*: xs)
    | k == k' = (VDestructure k' Nothing,) <$> go xs
    | otherwise = uncover (v, patPair xs)
  go ((Destructure{}, v@VDestructure{}) :*: xs) = uncover (v, patPair xs)

  go ((PGadtCon k _ _ (Just p) _, v@(VDestructure k' (Just u))) :*: xs)
    | k == k' = first (VDestructure k' . Just) <$> go ((p, u):*:xs)
    | otherwise = uncover (v, patPair xs)
  go ((PGadtCon k _ _ Nothing _, v@(VDestructure k' Nothing)) :*: xs)
    | k == k' = (VDestructure k' Nothing,) <$> go xs
    | otherwise = uncover (v, patPair xs)
  go ((PGadtCon{}, v@VDestructure{}) :*: xs) = uncover (v, patPair xs)

  ConVar for constructors : We always perform the UConVar implementation here -
  go ((p@(Destructure _ _ (_, ty)), VVariable v vTy) :*: xs) = do
    (k, arg) <- constructors env ty vTy
    maybe (pure ()) guardInhabited arg
    guardAll xs
    case arg of
      Nothing -> onVar p v (VDestructure k Nothing) xs
      Just arg -> do
        v' <- genName
        onVar p v (VDestructure k (Just (VVariable v' arg))) xs

  go ((p@(PGadtCon _ _ _ _ (_, ty)), VVariable v vTy) :*: xs) = do
    (k, arg) <- constructors env ty vTy
    maybe (pure ()) guardInhabited arg
    guardAll xs
    case arg of
      Nothing -> onVar p v (VDestructure k Nothing) xs
      Just arg -> do
        v' <- genName
        onVar p v (VDestructure k (Just (VVariable v' arg))) xs

  go ((Destructure{}, _) :*: _) = error "Mismatch on Destructure"
  go ((PGadtCon{}, _) :*: _) = error "Mismatch on PGadtCon"

  go ((PLiteral li _, v@(VLiteral li')) :*: xs)
    | li == li' = (v,) <$> go xs
    | otherwise = uncover (v, patPair xs)

  go ((p@(PLiteral LiUnit{} _), VVariable v _) :*: xs) = onVar p v (VLiteral LiUnit) xs
  go ((p@(PLiteral LiBool{} _), VVariable v _) :*: xs)
    =   onVar p v (VLiteral (LiBool True)) xs
    <|> onVar p v (VLiteral (LiBool False)) xs

  go ((p@(PLiteral li _), VVariable v _) :*: xs)
    =   onVar p v (VLiteral li) xs
    <|> onVar p v (VNotLiteral v (Set.singleton li)) xs
  This case is a little messy , as it 's both  and ConVar . Namely , if
  go ((p@(PLiteral li _), n@(VNotLiteral v lis)) :*: xs)
    | li `Set.notMember` lis
      =   onVar p v (VLiteral li) xs
      <|> onVar p v (VNotLiteral v (Set.insert li lis)) xs
    | otherwise = uncover (n, patPair xs)

  go ((PLiteral{}, _) :*: _) = error "Mismatch on PLiteral"

  go ((PTuple [p] _, u) :*: xs) = go ((p, u) :*: xs)
  go ((PTuple (p1:p2) a, VTuple u1 u2) :*: xs) = do
    (u1', (u2', xs')) <- go ((p1, u1) :*: (mkTuple p2 a, u2) :*: xs)
    pure (VTuple u1' u2', xs')
  ConVar for tuples : This always matches , so we just build up child value
  go ((p@(PTuple _ _), VVariable v vTy) :*: xs) = do
    (ty1, ty2) <- tupleTy vTy
    u1 <- flip VVariable ty1 <$> genName
    u2 <- flip VVariable ty2 <$> genName
    onVar p v (VTuple u1 u2) xs

  go ((PTuple{}, _) :*: _) = error "Mismatch on PTuple"

  go ((PRecord ps _, VRecord us') :*: xs) = first VRecord <$> foldRecord ps us' xs
  ConVar for records : This always matches , so we build up a child value for
  go ((p@(PRecord _ (_, ty)), VVariable v vTy) :*: xs) = do
    constrain [mkUni vTy ty]
    us <- traverse (\ty -> flip VVariable ty <$> genName) (rowTy ty)
    onVar p v (VRecord us) xs
  go ((PRecord{}, _) :*: _) = error "Mismatch on PTuple"

  Var : Match the remaining patterns , extend the environment , and unify the
  go ((w@(Wildcard _), u) :*: xs) = do
    guardInhabited (getType w)
    (u,) <$> go xs
  go ((w@(Capture v _), u) :*: xs) = do
    constrainVal v u
    guardInhabited (getType w)
    (u,) <$> go xs
  go ((PAs p v _, u) :*: xs) = onVar p v u xs

  go ((PType p _ _, u) :*: xs) = go ((p, u) :*: xs)
  go ((PList{}, _) :*: _) = error "PList is handled by desugar"

  onVar :: Pattern Typed -> Var Typed -> ValueAbs Typed -> PatPair a -> CoveringM (ValueAbs Typed, a)
  onVar p v u xs = constrainVal v u >> go ((p, u) :*: xs)

  mkTuple [] _ = error "Empty tuple"
  mkTuple [x] _ = x
  mkTuple xs a = PTuple xs a

  tupleTy (TyTuple t1 t2) = pure (t1, t2)
  tupleTy ty = do
    v1 <- freshTV; v2 <- freshTV
    constrain [mkUni ty (TyTuple v1 v2)]
    pure (v1, v2)

  rowTy TyVar{} = mempty
  rowTy (TyRows f fs) = rowTy f <> Map.fromList fs
  rowTy (TyExactRows fs) = Map.fromList fs
  rowTy (TyParens t) = rowTy t
  rowTy (TyWithConstraints _ t) = rowTy t
  rowTy t = error $ "Cannot get row from "++ show t

  guardInhabited :: Type Typed -> CoveringM ()
  guardInhabited ty = do
    (solve, cs) <- get
    name <- genName
    unless (inhabited env (AbsState solve cs name) ty) mzero

  guardAll :: PatPair a -> CoveringM ()
  guardAll Nil = pure ()
  guardAll ((x, _) :*: xs) = do
    guardInhabited (getType x)
    guardAll xs

  foldRecord :: [(T.Text, Pattern Typed)] -> Map.Map T.Text (ValueAbs Typed)
             -> PatPair a -> CoveringM (Map.Map T.Text (ValueAbs Typed), a)
  foldRecord [] vs xs = (vs,) <$> go xs
  foldRecord ((f, p):fs) us xs = do
    let u = fromMaybe (error $ "Cannot find field " ++ show f ++ " in record") (Map.lookup f us)
    (us', (u', xs')) <- foldRecord fs us ((p, u) :*: xs)
    pure (Map.insert f u' us', xs')

constructors :: (MonadPlus m, MonadState CoverState m, MonadNamey m)
             => Env -> Type Typed -> Type Typed
             -> m (Var Typed, Maybe (Type Typed))
constructors env kty vty = do
  k <- asum . map pure . toList . ctors $ kty
  (pty, _) <- skolGadt k =<< instantiate Strong Expression (fromJust (env ^. (names . at k)))
  let (cs, ty) = case pty of
                   TyWithConstraints cs ty -> (cs, ty)
                   _ -> ([], pty)
      (arg, res) = unwrapCtor ty

  Unify our result with the child , including any additional GADT constraints .
  constrain (mkUni res (expandTypeWith (env ^. tySyms) vty):map (uncurry mkUni) cs)
  pure (k, arg)

  where
    ctors :: Type Typed -> Set.Set (Var Typed)
    ctors (TyCon v _) = maybe (error $ "Cannot find constructors for " ++ show v) _tdConstructors (env ^. (types . at v))
    ctors (TyApp f _) = ctors f
    ctors t = error $ "Cannot get type name from " ++ show (pretty t)

    unwrapCtor :: Type p -> (Maybe (Type p), Type p)
    unwrapCtor (TyPi bind res) = case bind of
      Anon arg -> (Just arg, res)
      Implicit _ -> unwrapCtor res
      Invisible {} -> unwrapCtor res
    unwrapCtor (TyWithConstraints _ t) = unwrapCtor t
    unwrapCtor (TyParens t) = unwrapCtor t
    unwrapCtor t = (Nothing, t)

inhabited :: Env -> AbsState -> Type Typed -> Bool
inhabited env (AbsState st cs i)
  = not . Seq.null
  . flip evalNameyT i
  . flip evalStateT (st, cs)
  . go mempty
  where

  inhb :: Monad m => m ()
  inhb = pure ()

  go :: (MonadPlus m, MonadNamey m, MonadState CoverState m)
     => Set.Set (Var Typed) -> Type Typed -> m ()
  go c (TyVar v _) = do
    let c' = Set.insert v c
    t' <- gets (typeWithin v . fst)
    case t' of
      Nothing -> inhb
      Just (TyVar v' _) | Set.member v' c' -> inhb
      Just t' -> go c' t'

  go c t@TyApp{} = ctorCheck c t
  go c t@TyCon{} = ctorCheck c t
  go _ TyPromotedCon{} = inhb
  go _ TyPi{} = inhb
  go c (TyRows f fs) = go c f >> traverse_ (go c . snd) fs
  go c (TyExactRows fs) = traverse_ (go c . snd) fs
  go c (TyTuple l r) = go c l >> go c r
  go c (TyOperator l v r) = go c (TyApp (TyApp v l) r)
  go c (TyWildcard t) = maybe inhb (go c) t
  go c (TyParens t) = go c t

  go _ TySkol{} = inhb
  go c (TyWithConstraints _ t) = go c t
  go _ TyType = inhb
  go _ TyLit{} = inhb
  go _ TyTupleL{} = inhb

  | Returns the type name if this type is concrete ( defined as has 0 or more
  concreteTy c (TyCon v _)
    | v `Set.notMember` c
    , isJust (env ^. (types . at v))
    = Just v
    | otherwise = Nothing
  concreteTy c (TyApp f _) = concreteTy c f
  concreteTy _ _ = Nothing

  ctorCheck :: (MonadPlus m, MonadNamey m, MonadState CoverState m)
            => Set.Set (Var Typed) -> Type Typed -> m ()
  ctorCheck c t
    | Just v <- concreteTy c t =
        case maybe Unknown _tdInhabited (env ^. (types . at v)) of
          Uninhabited -> mzero
          Inhabited -> inhb
          Unknown ->
            do
            let c' = Set.insert v c
            (_, arg) <- constructors env t t
            maybe inhb (go c') arg
    | otherwise = inhb

mkUni :: Type Typed -> Type Typed -> Constraint Typed
mkUni = ConUnify (It'sThis (BecauseInternal "pmcheck")) mempty undefined

  | Add one or more type constraints into the current environment ,
constrain :: (MonadPlus m, MonadNamey m, MonadState CoverState m) => [Constraint Typed] -> m ()
constrain css = maybe empty put =<< doConstrain css where
  doConstrain css = do
    (sub, cs) <- get
    x <- runChronicleT . solveImplies sub mempty . (cs<>) $ Seq.fromList css
    pure $ case x of
      These Seq.Empty (sub', cs') -> Just (sub', Seq.fromList cs')
      That (sub', cs') ->  Just (sub', Seq.fromList cs')
      These _ _ -> Nothing
      This _ -> Nothing

constrainVal :: Var Typed -> ValueAbs Typed -> CoveringM ()
constrainVal _ _ = pure ()
