content: -- {-# OPTIONS_GHC -Wunused-imports #-}  -- no, because of liftA2
  {-# OPTIONS_GHC -Wunused-matches #-}
  {-# OPTIONS_GHC -Wunused-binds #-}
  
  -- | Tools for patterns in concrete syntax.
  
  module Agda.Syntax.Concrete.Pattern where
  
  import Control.Applicative ( liftA2 )
  import Control.Arrow ( first )
  import Control.Monad ( (>=>) )
  import Control.Monad.Identity
  
  import Data.Monoid ( Any(..), Endo(..), Sum(..) )
  
  import Agda.Syntax.Common
  import Agda.Syntax.Concrete
  
  import Agda.Utils.AffineHole
  import Agda.Utils.Functor
  import Agda.Utils.Impossible
  import Agda.Utils.List
  import Agda.Utils.List1  ( List1, pattern (:|), (<|) )
  import Agda.Utils.List2  ( List2 )
  import Agda.Utils.Maybe
  import Agda.Utils.Singleton
  import qualified Agda.Utils.List1 as List1
  
  
  -- | Check for ellipsis @...@.
  
  class IsEllipsis a where
    isEllipsis :: a -> Bool
  
  -- | Is the pattern just @...@?
  instance IsEllipsis Pattern where
    isEllipsis = \case
      EllipsisP{}         -> True
      ParenP _ p          -> isEllipsis p
      _ -> False
  
  -- | Has the lhs an occurrence of the ellipsis @...@?
  
  class HasEllipsis a where
    hasEllipsis :: a -> Bool
  
  instance HasEllipsis Pattern where
    hasEllipsis p =
      case hasEllipsis' p of
        ZeroHoles _ -> False
        OneHole _ _ -> True
        ManyHoles   -> True
  
  -- | Does the lhs contain an ellipsis?
  instance HasEllipsis LHS where
    hasEllipsis (LHS p _ _) = hasEllipsis p
    -- clauses that are already expanded don't have an ellipsis
  
  -- | Check for with-pattern @| p@.
  
  class IsWithP p where
    isWithP :: p -> Maybe p
  
    default isWithP :: (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p
    isWithP = traverseF isWithP
  
  instance IsWithP Pattern where
    isWithP = \case
      WithP _ p           -> Just p
      ParenP _ p          -> isWithP p
      _ -> Nothing
  
  instance IsWithP p => IsWithP (Arg p) where
  instance IsWithP p => IsWithP (Named n p) where
  
  
  -- * LHS manipulation (see also ''Agda.Syntax.Abstract.Pattern'')
  
  -- | The next patterns are ...
  --
  -- (This view discards 'PatInfo'.)
  data LHSPatternView
    = LHSAppP  (List1 (NamedArg Pattern))
        -- ^ Application patterns (non-empty list).
    | LHSWithP (List1 Pattern)
        -- ^ With patterns (non-empty list).
        --   These patterns are not prefixed with 'WithP'.
  
  -- | Construct the 'LHSPatternView' of the given list (if not empty).
  --
  -- Return the view and the remaining patterns.
  
  lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
  lhsPatternView [] = Nothing
  lhsPatternView (p0 : ps) =
    case namedArg p0 of
      WithP _i p   -> Just (LHSWithP (p :| map namedArg ps1), ps2)
        where
        (ps1, ps2) = spanJust isWithP ps
      -- If the next pattern is an application pattern, collect more of these
      _ -> Just (LHSAppP (p0 :| ps1), ps2)
        where
        (ps1, ps2) = span (isNothing . isWithP) ps
  
  -- | Add applicative patterns (non-projection / non-with patterns) to the right.
  lhsCoreApp :: LHSCore -> List1 (NamedArg Pattern) -> LHSCore
  lhsCoreApp (LHSEllipsis r core) ps = LHSEllipsis r $ lhsCoreApp core ps
  lhsCoreApp core ps = core { lhsPats = lhsPats core ++ List1.toList ps }
  
  -- | Add with-patterns to the right.
  lhsCoreWith :: LHSCore -> List1 Pattern -> LHSCore
  lhsCoreWith (LHSWith core wps []) wps' = LHSWith core (wps <> wps') []
  lhsCoreWith core                  wps' = LHSWith core wps' []
  
  -- | Append patterns to 'LHSCore', separating with patterns from the rest.
  lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
  lhsCoreAddSpine core ps0 =
    -- Recurse on lhsPatternView until no patterns left.
    case lhsPatternView ps0 of
      Nothing       -> core
      Just (LHSAppP  ps , ps') -> lhsCoreApp  core ps  `lhsCoreAddSpine` ps'
      Just (LHSWithP wps, ps') -> lhsCoreWith core wps `lhsCoreAddSpine` ps'
  
  
  -- | Modify the 'Pattern' component in 'LHS'.
  mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
  mapLhsOriginalPattern f lhs@LHS{ lhsOriginalPattern = p } =
    lhs { lhsOriginalPattern = f p }
  
  -- | Effectfully modify the 'Pattern' component in 'LHS'.
  mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
  mapLhsOriginalPatternM f lhs@LHS{ lhsOriginalPattern = p } = f p <&> \ p' ->
    lhs { lhsOriginalPattern = p' }
  
  -- | Does the LHS contain projection patterns?
  hasCopatterns :: LHSCore -> Bool
  hasCopatterns = \case
    LHSHead{}     -> False
    LHSProj{}     -> True
    LHSWith h _ _ -> hasCopatterns h
    LHSEllipsis{} -> False
  
  -- * Generic fold
  
  -- | Generic pattern traversal.
  --
  -- See 'Agda.Syntax.Abstract.Pattern.APatternLike'.
  
  class CPatternLike p where
  
    -- | Fold pattern.
    foldrCPattern
      :: Monoid m
      => (Pattern -> m -> m)
           -- ^ Combine a pattern and the value computed from its subpatterns.
      -> p -> m
  
    default foldrCPattern
      :: (Monoid m, Foldable f, CPatternLike q, f q ~ p)
      => (Pattern -> m -> m) -> p -> m
    foldrCPattern = foldMap . foldrCPattern
  
    -- | Traverse pattern with option of post-traversal modification.
    traverseCPatternA :: (Applicative m, Functor m)
        => (Pattern -> m Pattern -> m Pattern)
           -- ^ Combine a pattern and the its recursively computed version.
        -> p -> m p
  
    default traverseCPatternA :: (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m)
        => (Pattern -> m Pattern -> m Pattern)
        -> p -> m p
    traverseCPatternA = traverse . traverseCPatternA
  
    -- | Traverse pattern.
    traverseCPatternM :: Monad m
      => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
      -> (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
      -> p -> m p
  
    default traverseCPatternM
      :: (Traversable f, CPatternLike q, f q ~ p, Monad m)
      => (Pattern -> m Pattern)
      -> (Pattern -> m Pattern)
      -> p -> m p
    traverseCPatternM pre post = traverse $ traverseCPatternM pre post
  
  instance CPatternLike Pattern where
    foldrCPattern f p0 = f p0 $
      case p0 of
        -- Recursive cases:
        AppP p ps       -> foldrCPattern f (p, ps)
        RawAppP _ ps    -> foldrCPattern f ps
        OpAppP _ _ _ ps -> foldrCPattern f ps
        HiddenP _ ps    -> foldrCPattern f ps
        InstanceP _ ps  -> foldrCPattern f ps
        ParenP _ p      -> foldrCPattern f p
        AsP _ _ p       -> foldrCPattern f p
        WithP _ p       -> foldrCPattern f p
        RecP _ _ ps     -> foldrCPattern f ps
        EllipsisP _ mp  -> foldrCPattern f mp
        -- Nonrecursive cases:
        IdentP _ _      -> mempty
        WildP _         -> mempty
        DotP _ _ _      -> mempty
        AbsurdP _       -> mempty
        LitP _ _        -> mempty
        QuoteP _        -> mempty
        EqualP _ _      -> mempty
  
    traverseCPatternA f p0 = f p0 $ case p0 of
        -- Recursive cases:
        AppP        p ps    -> liftA2 AppP (traverseCPatternA f p) (traverseCPatternA f ps)
        RawAppP   r ps      -> RawAppP r     <$> traverseCPatternA f ps
        OpAppP    r x xs ps -> OpAppP r x xs <$> traverseCPatternA f ps
        HiddenP   r p       -> HiddenP r     <$> traverseCPatternA f p
        InstanceP r p       -> InstanceP r   <$> traverseCPatternA f p
        ParenP    r p       -> ParenP r      <$> traverseCPatternA f p
        AsP       r x p     -> AsP r x       <$> traverseCPatternA f p
        WithP     r p       -> WithP r       <$> traverseCPatternA f p
        RecP  kwr r ps      -> RecP kwr r    <$> traverseCPatternA f ps
        EllipsisP r mp      -> EllipsisP r   <$> traverseCPatternA f mp
        -- Nonrecursive cases:
        IdentP _ _      -> pure p0
        WildP _         -> pure p0
        DotP _ _ _      -> pure p0
        AbsurdP _       -> pure p0
        LitP _ _        -> pure p0
        QuoteP _        -> pure p0
        EqualP _ _      -> pure p0
  
    traverseCPatternM pre post = pre >=> recurse >=> post
      where
      recurse p0 = case p0 of
        -- Recursive cases:
        AppP        p ps    -> uncurry AppP  <$> traverseCPatternM pre post (p, ps)
        RawAppP   r ps      -> RawAppP r     <$> traverseCPatternM pre post ps
        OpAppP    r x xs ps -> OpAppP r x xs <$> traverseCPatternM pre post ps
        HiddenP   r p       -> HiddenP r     <$> traverseCPatternM pre post p
        InstanceP r p       -> InstanceP r   <$> traverseCPatternM pre post p
        ParenP    r p       -> ParenP r      <$> traverseCPatternM pre post p
        AsP       r x p     -> AsP r x       <$> traverseCPatternM pre post p
        WithP     r p       -> WithP r       <$> traverseCPatternM pre post p
        RecP  kwr r ps      -> RecP kwr r    <$> traverseCPatternM pre post ps
        EllipsisP r mp      -> EllipsisP r   <$> traverseCPatternM pre post mp
        -- Nonrecursive cases:
        IdentP _ _      -> return p0
        WildP _         -> return p0
        DotP _ _ _      -> return p0
        AbsurdP _       -> return p0
        LitP _ _        -> return p0
        QuoteP _        -> return p0
        EqualP _ _      -> return p0
  
  instance (CPatternLike a, CPatternLike b) => CPatternLike (a,b) where
    foldrCPattern f (p, p') =
      foldrCPattern f p `mappend` foldrCPattern f p'
  
    traverseCPatternA f (p, p') =
      liftA2 (,)
        (traverseCPatternA f p)
        (traverseCPatternA f p')
  
    traverseCPatternM pre post (p, p') =
      liftA2 (,)
        (traverseCPatternM pre post p)
        (traverseCPatternM pre post p')
  
  instance CPatternLike p => CPatternLike (Arg p)
  instance CPatternLike p => CPatternLike (Named n p)
  instance CPatternLike p => CPatternLike [p]
  instance CPatternLike p => CPatternLike (List1 p)
  instance CPatternLike p => CPatternLike (List2 p)
  instance CPatternLike p => CPatternLike (Maybe p)
  instance CPatternLike p => CPatternLike (FieldAssignment' p)
  
  -- | Compute a value from each subpattern and collect all values in a monoid.
  
  foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
  foldCPattern f = foldrCPattern $ \ p m -> f p `mappend` m
  
  -- | Traverse pattern(s) with a modification before the recursive descent.
  
  preTraverseCPatternM
    :: (CPatternLike p, Monad m)
    => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
    -> p -> m p
  preTraverseCPatternM pre p = traverseCPatternM pre return p
  
  -- | Traverse pattern(s) with a modification after the recursive descent.
  
  postTraverseCPatternM
    :: (CPatternLike p, Monad m)
    => (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
    -> p -> m p
  postTraverseCPatternM post p = traverseCPatternM return post p
  
  -- | Map pattern(s) with a modification after the recursive descent.
  
  mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
  mapCPattern f = runIdentity . postTraverseCPatternM (Identity . f)
  
  
  -- * Specific folds.
  
  -- | Get all the identifiers in a pattern in left-to-right order.
  --
  -- Implemented using difference lists.
  patternQNames :: CPatternLike p => p -> [QName]
  patternQNames p = foldCPattern f p `appEndo` []
    where
    f :: Pattern -> Endo [QName]
    f = \case
      IdentP _ x     -> Endo (x :)
      OpAppP _ x _ _ -> Endo (x :)
      AsP _ _x _     -> mempty  -- _x must be a bound name, can't be a constructor!
      AppP _ _       -> mempty
      WithP _ _      -> mempty
      RawAppP _ _    -> mempty
      HiddenP _ _    -> mempty
      ParenP _ _     -> mempty
      WildP _        -> mempty
      AbsurdP _      -> mempty
      DotP _ _ _     -> mempty
      LitP _ _       -> mempty
      QuoteP _       -> mempty
      InstanceP _ _  -> mempty
      RecP _ _ _     -> mempty
      EqualP _ _     -> mempty
      EllipsisP _ _  -> mempty
  
  -- | Get all the identifiers in a pattern in left-to-right order.
  patternNames :: Pattern -> [Name]
  patternNames = map unqualify . patternQNames
  
  -- | Does the pattern contain a with-pattern?
  -- (Shortcutting.)
  hasWithPatterns :: CPatternLike p => p -> Bool
  hasWithPatterns = getAny . foldCPattern (Any . isWithPattern)
  
  -- | Is 'WithP'?
  isWithPattern :: Pattern -> Bool
  isWithPattern = \case
    WithP{} -> True
    _ -> False
  
  -- | Count the number of with-subpatterns in a pattern?
  numberOfWithPatterns :: CPatternLike p => p -> Int
  numberOfWithPatterns = getSum . foldCPattern (Sum . f)
    where f p = if isWithPattern p then 1 else 0
  
  -- | Compute the context in which the ellipsis occurs, if at all.
  --   If there are several occurrences, this is an error.
  --   This only counts ellipsis that haven't already been expanded.
  hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
  hasEllipsis' = traverseCPatternA $ \ p mp ->
    case p of
      EllipsisP _ Nothing -> OneHole id p
      _                   -> mp
  
  -- | Reconstruct the ellipsis, used in printing (AbstractToConcrete).
  reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
  reintroduceEllipsis (ExpandedEllipsis r k) p | hasWithPatterns p =
    let (args, wargs) = splitEllipsis k $ List1.toList $ patternAppView p
        (hd,args') = fromMaybe __IMPOSSIBLE__ $ uncons args
        core = foldl AppP (namedArg hd) args'
    in foldl AppP (EllipsisP r $ Just $ core) wargs
  reintroduceEllipsis _ p = p
  
  splitEllipsis :: (IsWithP p) => Int -> [p] -> ([p],[p])
  splitEllipsis _ [] = ([] , [])
  splitEllipsis k (p:ps)
    | isJust (isWithP p) = if
        | k == 0    -> ([] , p:ps)
        | otherwise -> first (p:) $ splitEllipsis (k-1) ps
    | otherwise = first (p:) $ splitEllipsis k ps
  
  ---------------------------------------------------------------------------
  -- * Helpers for pattern and lhs parsing
  ---------------------------------------------------------------------------
  
  -- | View a pattern @p@ as a list @p0 .. pn@ where @p0@ is the identifier
  --   (in most cases a constructor).
  --
  --  Pattern needs to be parsed already (operators resolved).
  patternAppView :: Pattern -> List1 (NamedArg Pattern)
  patternAppView = \case
      AppP p arg      -> patternAppView p `List1.appendList` [arg]
      OpAppP _ x _ ps -> defaultNamedArg (IdentP True x) <| ps
      ParenP _ p      -> patternAppView p
      RawAppP _ _     -> __IMPOSSIBLE__
      p               -> singleton $ defaultNamedArg p
  