    {-# LANGUAGE CPP           #-}

    module Agda.TypeChecking.Coverage.Match
      ( Match(..), match
      , SplitPattern, SplitPatVar(..), fromSplitPatterns, toSplitPatterns
      , toSplitPSubst, applySplitPSubst
      , isTrivialPattern
      , BlockingVar(..), BlockingVars, BlockedOnResult(..)
      , setBlockingVarOverlap
      , ApplyOrIApply(..)
      ) where

    import Control.Monad.State

    import Prelude hiding ( null )

    import qualified Data.List as List
    import Data.Maybe (mapMaybe, isJust, fromMaybe)
    import Data.Monoid ( Monoid, mempty, mappend, mconcat )
    import Data.Semigroup ( Semigroup, (<>), Any(..) )
    import Data.Traversable (traverse)

    import Agda.Syntax.Abstract (IsProjP(..))
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern ()
    import Agda.Syntax.Literal
    import Agda.Syntax.Position

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Pretty ( PrettyTCM(..) )
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Pretty ( Pretty(..), text, (<+>), cat , prettyList_ )
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Size
    import Agda.Utils.List
    import Agda.Utils.Monad

    #include "undefined.h"
    import Agda.Utils.Impossible

    {-| Given

        1. the function clauses @cs@
        2. the patterns @ps@

    we want to compute a variable index of the split clause to split on next.

    First, we find the set @cs'@ of all the clauses that are
    instances (via substitutions @rhos@) of the split clause.

    In these substitutions, we look for a column that has only constructor patterns.
    We try to split on this column first.
    -}

    type SplitAssignment = (Nat,SplitPattern)

    -- | Match the given patterns against a list of clauses
    match :: (MonadReduce m , HasConstInfo m , HasBuiltins m) => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat,[SplitAssignment]))
    match cs ps = foldr choice (return No) $ zipWith matchIt [0..] cs
      where
        matchIt :: (MonadReduce m , HasConstInfo m , HasBuiltins m) => Nat -> Clause -> m (Match (Nat,[SplitAssignment]))
        matchIt i c = fmap (i,) <$> matchClause ps c

    -- | For each variable in the patterns of a split clause, we remember the
    --   de Bruijn-index and the literals excluded by previous matches.
    data SplitPatVar = SplitPatVar
      { splitPatVarName   :: PatVarName
      , splitPatVarIndex  :: Int
      , splitExcludedLits :: [Literal]
      } deriving (Show)

    instance Pretty SplitPatVar where
      prettyPrec _ x =
        (text $ patVarNameToString (splitPatVarName x)) P.<>
        (text $ "@" ++ show (splitPatVarIndex x)) P.<>
        (ifNull (splitExcludedLits x) empty $ \lits ->
          "\\{" P.<> prettyList_ lits P.<> "}")

    instance PrettyTCM SplitPatVar where
      prettyTCM = prettyTCM . var . splitPatVarIndex

    type SplitPattern = Pattern' SplitPatVar

    toSplitVar :: DBPatVar -> SplitPatVar
    toSplitVar x = SplitPatVar (dbPatVarName x) (dbPatVarIndex x) []

    fromSplitVar :: SplitPatVar -> DBPatVar
    fromSplitVar x = DBPatVar (splitPatVarName x) (splitPatVarIndex x)

    instance DeBruijn SplitPatVar where
      deBruijnView x = deBruijnView (fromSplitVar x)
      debruijnNamedVar n i = toSplitVar (debruijnNamedVar n i)

    toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
    toSplitPatterns = (fmap . fmap . fmap . fmap) toSplitVar

    fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
    fromSplitPatterns = (fmap . fmap . fmap . fmap) fromSplitVar

    instance DeBruijn SplitPattern where
      debruijnNamedVar n i  = varP $ SplitPatVar n i []
      deBruijnView _        = Nothing

    type SplitPSubstitution = Substitution' SplitPattern

    toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
    toSplitPSubst = (fmap . fmap) toSplitVar

    fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
    fromSplitPSubst = (fmap . fmap) fromSplitVar

    applySplitPSubst :: (Subst Term a) => SplitPSubstitution -> a -> a
    applySplitPSubst = applyPatSubst . fromSplitPSubst

    -- TODO: merge this instance and the one for DeBruijnPattern in
    -- Substitute.hs into one for Subst (Pattern' a) (Pattern' a).
    instance Subst SplitPattern SplitPattern where
      applySubst IdS p = p
      applySubst rho p = case p of
        VarP o x     ->
          usePatOrigin o $
          useName (splitPatVarName x) $
          useExcludedLits (splitExcludedLits x) $
          lookupS rho $ splitPatVarIndex x
        DotP o u     -> DotP o $ applySplitPSubst rho u
        ConP c ci ps -> ConP c ci $ applySubst rho ps
        DefP o q ps -> DefP o q $ applySubst rho ps
        LitP x       -> p
        ProjP{}      -> p
        IApplyP o l r x  ->
          useEndPoints (applySplitPSubst rho l) (applySplitPSubst rho r) $
          usePatOrigin o $
          useName (splitPatVarName x) $
          useExcludedLits (splitExcludedLits x) $
          lookupS rho $ splitPatVarIndex x

        where
          -- see Subst for DeBruijnPattern
          useEndPoints :: Term -> Term -> SplitPattern -> SplitPattern
          useEndPoints l r (VarP o x)        = IApplyP o l r x
          useEndPoints l r (IApplyP o _ _ x) = IApplyP o l r x
          useEndPoints l r x                 = __IMPOSSIBLE__

          useName :: PatVarName -> SplitPattern -> SplitPattern
          useName n (VarP o x)
            | isUnderscore (splitPatVarName x)
            = VarP o $ x { splitPatVarName = n }
          useName _ x = x

          useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
          useExcludedLits lits = \case
            (VarP o x) -> VarP o $ x
              { splitExcludedLits = lits ++ splitExcludedLits x }
            p -> p

    -- | A pattern that matches anything (modulo eta).
    isTrivialPattern :: (HasConstInfo m) => Pattern' a -> m Bool
    isTrivialPattern p = case p of
      VarP{}      -> return True
      DotP{}      -> return True
      ConP c i ps -> andM $ (isEtaCon $ conName c)
                          : (map (isTrivialPattern . namedArg) ps)
      DefP{}      -> return False
      LitP{}      -> return False
      ProjP{}     -> return False
      IApplyP{}   -> return True

    -- | If matching succeeds, we return the instantiation of the clause pattern vector
    --   to obtain the split clause pattern vector.
    type MatchResult = Match [SplitAssignment]

    -- | If matching is inconclusive (@Block@) we want to know which
    --   variables or projections are blocking the match.
    data Match a
      = Yes a   -- ^ Matches unconditionally.
      | No      -- ^ Definitely does not match.
      | Block
        { blockedOnResult :: BlockedOnResult
          -- ^ @BlockedOnProj o@ if the clause has a result split
        , blockedOnVars :: BlockingVars
          -- ^ @BlockingVar i cs ls o@ means variable @i@ is blocked on
          -- constructors @cs@ and literals @ls@.
        }
      deriving (Functor)

    data ApplyOrIApply = IsApply | IsIApply

    data BlockedOnResult
      = BlockedOnProj      -- ^ Blocked on unsplit projection
         { blockedOnResultOverlap :: Bool
           -- ^ True if there are also matching clauses without an unsplit
           -- copattern.
         }
      | BlockedOnApply     -- ^ Blocked on unintroduced argument
         { blockedOnResultIApply :: ApplyOrIApply
           -- ^ True if the unintroduced argument was an IApply pattern
         }
      | NotBlockedOnResult

    -- | Variable blocking a match.
    data BlockingVar = BlockingVar
      { blockingVarNo  :: Nat
        -- ^ De Bruijn index of variable blocking the match.
      , blockingVarCons :: [ConHead]
        -- ^ Constructors in this position.
      , blockingVarLits :: [Literal]
        -- ^ Literals in this position.
      , blockingVarOverlap :: Bool
        -- ^ True if at least one clause has a variable pattern in this
        --   position.
      } deriving (Show)

    instance Pretty BlockingVar where
      pretty (BlockingVar i cs ls o) = cat
        [ text ("variable " ++ show i)
        , if null cs then empty else " blocked on constructors" <+> pretty cs
        , if null ls then empty else " blocked on literals" <+> pretty ls
        , if o then " (overlapping)" else empty
        ]

    type BlockingVars = [BlockingVar]

    yes :: Monad m => a -> m (Match a)
    yes = return . Yes

    no :: Monad m => m (Match a)
    no = return No

    blockedOnConstructor :: Monad m => Nat -> ConHead -> m (Match a)
    blockedOnConstructor i c = return $ Block NotBlockedOnResult [BlockingVar i [c] [] False]

    blockedOnLiteral :: Monad m => Nat -> Literal -> m (Match a)
    blockedOnLiteral i l = return $ Block NotBlockedOnResult [BlockingVar i [] [l] False]

    blockedOnProjection :: Monad m => m (Match a)
    blockedOnProjection = return $ Block (BlockedOnProj False) []

    blockedOnApplication :: Monad m => ApplyOrIApply -> m (Match a)
    blockedOnApplication b = return $ Block (BlockedOnApply b) []

    -- | Lens for 'blockingVarCons'.
    mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar
    mapBlockingVarCons f b = b { blockingVarCons = f (blockingVarCons b) }

    -- | Lens for 'blockingVarLits'.
    mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar
    mapBlockingVarLits f b = b { blockingVarLits = f (blockingVarLits b) }

    setBlockingVarOverlap :: BlockingVar -> BlockingVar
    setBlockingVarOverlap = \x -> x { blockingVarOverlap = True }

    overlapping :: BlockingVars -> BlockingVars
    overlapping = map setBlockingVarOverlap

    -- | Left dominant merge of blocking vars.
    zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
    zipBlockingVars xs ys = map upd xs
      where
        upd (BlockingVar x cons lits o) = case List.find ((x ==) . blockingVarNo) ys of
          Just (BlockingVar _ cons' lits' o') -> BlockingVar x (cons ++ cons') (lits ++ lits') (o || o')
          Nothing -> BlockingVar x cons lits True

    setBlockedOnResultOverlap :: BlockedOnResult -> BlockedOnResult
    setBlockedOnResultOverlap b = case b of
      BlockedOnProj{}      -> b { blockedOnResultOverlap = True }
      BlockedOnApply{}     -> b
      NotBlockedOnResult{} -> b

    anyBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    anyBlockedOnResult b1 b2 = case (b1,b2) of
      (NotBlockedOnResult , b2                ) -> b2
      (b1                 , NotBlockedOnResult) -> b1
      (_                  , _                 ) -> __IMPOSSIBLE__

    -- | Left dominant merge of `BlockedOnResult`.
    choiceBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    choiceBlockedOnResult b1 b2 = case (b1,b2) of
      (NotBlockedOnResult  , _                 ) -> NotBlockedOnResult
      (BlockedOnProj _     , NotBlockedOnResult) -> BlockedOnProj True
      (BlockedOnProj o1    , BlockedOnProj o2  ) -> BlockedOnProj (o1 || o2)
      (BlockedOnProj o1    , BlockedOnApply{}  ) -> BlockedOnProj True
      (BlockedOnApply b    , _                 ) -> BlockedOnApply b

    -- | @choice m m'@ combines the match results @m@ of a function clause
    --   with the (already combined) match results $m'$ of the later clauses.
    --   It is for skipping clauses that definitely do not match ('No').
    --   It is left-strict, to be used with @foldr@.
    --   If one clause unconditionally matches ('Yes') we do not look further.
    choice :: Monad m => m (Match a) -> m (Match a) -> m (Match a)
    choice m m' = m >>= \case
      Yes a -> yes a
      Block r xs -> m' >>= \case
        Block s ys -> return $ Block (choiceBlockedOnResult r s) $ zipBlockingVars xs ys
        Yes _      -> return $ Block (setBlockedOnResultOverlap r) $ overlapping xs
        No         -> return $ Block r xs
      No    -> m'

    -- | @matchClause qs i c@ checks whether clause @c@
    --   covers a split clause with patterns @qs@.
    matchClause
      :: (MonadReduce m , HasConstInfo m , HasBuiltins m)
      => [NamedArg SplitPattern]
         -- ^ Split clause patterns @qs@.
      -> Clause
         -- ^ Clause @c@ to cover split clause.
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes' the instantiation @rs@ such that @(namedClausePats c)[rs] == qs@.
    matchClause qs c = matchPats (namedClausePats c) qs

    -- | @matchPats ps qs@ checks whether a function clause with patterns
    --   @ps@ covers a split clause with patterns @qs@.
    --
    --   Issue #842 / #1986: This is accepted:
    --   @
    --     F : Bool -> Set1
    --     F true = Set
    --     F      = \ x -> Set
    --   @
    --   For the second clause, the split clause is @F false@,
    --   so there are more patterns in the split clause than
    --   in the considered clause.  These additional patterns
    --   are simply dropped by @zipWith@.  This will result
    --   in @mconcat []@ which is @Yes []@.

    matchPats
      :: (MonadReduce m , HasConstInfo m , HasBuiltins m, DeBruijn a)
      => [NamedArg (Pattern' a)]
         -- ^ Clause pattern vector @ps@ (to cover split clause pattern vector).
      -> [NamedArg SplitPattern]
         -- ^ Split clause pattern vector @qs@ (to be covered by clause pattern vector).
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes' the instantiation @rs@ such that @ps[rs] == qs@.
    matchPats [] [] = yes []
    matchPats (p:ps) (q:qs) =
      matchPat (namedArg p) (namedArg q) `combine` matchPats ps qs

    -- Patterns left in split clause:
    -- Andreas, 2016-06-03, issue #1986:
    -- catch-all for copatterns is inconsistent as found by Ulf.
    -- Thus, if the split clause has copatterns left,
    -- the current (shorter) clause is not considered covering.
    matchPats [] qs@(_:_) = case mapMaybe isProjP qs of
      [] -> yes [] -- no proj. patterns left
      _  -> no     -- proj. patterns left

    -- Patterns left in candidate clause:
    -- If the current clause has additional copatterns in
    -- comparison to the split clause, we should split on them.
    matchPats (p:ps) [] = case isProjP p of
      Just{}  -> blockedOnProjection
      Nothing -> blockedOnApplication (case namedArg p of IApplyP{} -> IsIApply; _ -> IsApply)

    -- | Combine results of checking whether function clause patterns
    --   covers split clause patterns.
    --
    --   'No' is dominant: if one function clause pattern is disjoint to
    --   the corresponding split clause pattern, then
    --   the whole clauses are disjoint.
    --
    --   'Yes' is neutral: for a match, all patterns have to match.
    --
    --   'Block' accumulates variables of the split clause
    --   that have to be instantiated (an projection names of copattern matches)
    --   to make the split clause an instance of the function clause.
    combine :: (Monad m, Semigroup a) => m (Match a) -> m (Match a) -> m (Match a)
    combine m m' = m >>= \case
        Yes a -> m' >>= \case
          Yes b -> yes (a <> b)
          y     -> return y
        No    -> no
        x@(Block r xs) -> m' >>= \case
          No    -> no
          Block s ys -> return $ Block (anyBlockedOnResult r s) (xs ++ ys)
          Yes{} -> return x

    -- | @matchPat p q@ checks whether a function clause pattern @p@
    --   covers a split clause pattern @q@.  There are three results:
    --   @Yes rs@ means it covers, because @p@ is a variable pattern. @rs@ collects
    --   the instantiations of the variables in @p@ s.t. @p[rs] = q@.
    --   @No@ means it does not cover.
    --   @Block [x]@ means @p@ is a proper instance of @q@ and could become
    --   a cover if @q@ was split on variable @x@.
    --   @BlockLit [x] means @p@ is a proper instance of @q@ and could become
    --   a cover if variable @x@ is instantiated with an appropriate literal.

    matchPat
      :: (MonadReduce m , HasConstInfo m , HasBuiltins m, DeBruijn a)
      => Pattern' a
         -- ^ Clause pattern @p@ (to cover split clause pattern).
      -> SplitPattern
         -- ^ Split clause pattern @q@ (to be covered by clause pattern).
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes', also the instantiation @rs@ of the clause pattern variables
         --   to produce the split clause pattern, @p[rs] = q@.
    matchPat p q = case p of
      VarP _ x   -> yes [(fromMaybe __IMPOSSIBLE__ (deBruijnView x),q)]
      DotP{}   -> yes []
      -- Jesper, 2014-11-04: putting 'Yes [q]' here triggers issue 1333.
      -- Not checking for trivial patterns should be safe here, as dot patterns are
      -- guaranteed to match if the rest of the pattern does, so some extra splitting
      -- on them doesn't change the reduction behaviour.
      p@(LitP l) -> case q of
        VarP _ x -> if l `elem` splitExcludedLits x
                    then no
                    else blockedOnLiteral (splitPatVarIndex x) l
        _ -> isLitP q >>= \case
          Just l' -> if l == l' then yes [] else no
          Nothing -> no
      ProjP _ d -> case q of
        ProjP _ d' -> do
          d <- getOriginalProjection d
          if d == d' then yes [] else no
        _          -> __IMPOSSIBLE__
      IApplyP _ _ _ x -> yes [(fromMaybe __IMPOSSIBLE__ (deBruijnView x),q)]
      ConP c _ ps -> unDotP q >>= \case
        VarP _ x -> blockedOnConstructor (splitPatVarIndex x) c
        ConP c' i qs
          | c == c'   -> matchPats ps qs
          | otherwise -> no
        DotP o t  -> no
        LitP l    -> isLitP p >>= \case
          Just l' -> if l == l' then yes [] else no
          Nothing -> no
        DefP{}   -> no
        ProjP{}   -> __IMPOSSIBLE__  -- excluded by typing
        IApplyP _ _ _ x -> blockedOnConstructor (splitPatVarIndex x) c
      (DefP o c ps) -> unDotP q >>= \case
        VarP _ x -> __IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c
        ConP c' i qs -> no
        DotP o t  -> no
        LitP _    -> no
        DefP o c' qs
          | c == c'   -> matchPats ps qs
          | otherwise -> no
        ProjP{}   -> __IMPOSSIBLE__  -- excluded by typing
        IApplyP _ _ _ x -> __IMPOSSIBLE__ --blockedOnConstructor (splitPatVarIndex x) c

    -- unfold one level of a dot pattern to a proper pattern if possible
    unDotP :: (MonadReduce m, DeBruijn (Pattern' a)) => Pattern' a -> m (Pattern' a)
    unDotP (DotP o v) = reduce v >>= \case
      Var i [] -> return $ deBruijnVar i
      Con c _ vs -> do
        let ps = map (fmap $ unnamed . DotP o) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims vs
        return $ ConP c noConPatternInfo ps
      Lit l -> return $ LitP l
      v     -> return $ dotP v
    unDotP p = return p

    isLitP :: (MonadReduce m, HasBuiltins m) => Pattern' a -> m (Maybe Literal)
    isLitP (LitP l) = return $ Just l
    isLitP (DotP _ u) = reduce u >>= \case
      Lit l -> return $ Just l
      _     -> return $ Nothing
    isLitP (ConP c ci []) = do
      Con zero _ [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinZero
      if | c == zero -> return $ Just $ LitNat (getRange c) 0
         | otherwise -> return Nothing
    isLitP (ConP c ci [a]) | visible a && isRelevant a = do
      Con suc _ [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSuc
      if | c == suc  -> fmap inc <$> isLitP (namedArg a)
         | otherwise -> return Nothing
      where
        inc :: Literal -> Literal
        inc (LitNat r n) = LitNat (fuseRange c r) $ n + 1
        inc _ = __IMPOSSIBLE__
    isLitP _ = return Nothing