content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  module Agda.Syntax.Internal.Pattern where
  
  import Control.Arrow       ( second )
  import Control.Monad       ( (>=>), forM )
  import Control.Monad.State ( MonadState(..), State, evalState )
  
  import Data.Maybe
  import Data.Monoid
  import qualified Data.List as List
  
  import Agda.Syntax.Common
  import Agda.Syntax.Internal
  
  import Agda.Utils.List
  import Agda.Utils.Permutation
  import Agda.Utils.Size (size)
  
  import Agda.Utils.Impossible
  
  -- * Tools for clauses
  
  -- | Translate the clause patterns to terms with free variables bound by the
  --   clause telescope.
  --
  --   Precondition: no projection patterns.
  clauseArgs :: Clause -> Args
  clauseArgs cl = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ clauseElims cl
  
  -- | Translate the clause patterns to an elimination spine
  --   with free variables bound by the clause telescope.
  clauseElims :: Clause -> Elims
  clauseElims cl = patternsToElims $ namedClausePats cl
  
  -- | Arity of a function, computed from clauses.
  class FunArity a where
    funArity :: a -> Int
  
  -- | Get the number of initial 'Apply' patterns.
  
  instance {-# OVERLAPPABLE #-} IsProjP p => FunArity [p] where
    funArity = length . takeWhile (isNothing . isProjP)
  
  -- | Get the number of initial 'Apply' patterns in a clause.
  instance FunArity Clause where
    funArity = funArity . namedClausePats
  
  -- | Get the number of common initial 'Apply' patterns in a list of clauses.
  instance {-# OVERLAPPING #-} FunArity [Clause] where
    funArity []  = 0
    funArity cls = minimum $ map funArity cls
  
  -- * Tools for patterns
  
  -- | Label the pattern variables from left to right
  --   using one label for each variable pattern and one for each dot pattern.
  class LabelPatVars a b where
    type PatVarLabel b
    labelPatVars :: a -> State [PatVarLabel b] b
    unlabelPatVars :: b -> a
    -- ^ Intended, but unpractical due to the absence of type-level lambda, is:
    --   @labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))@
  
    default labelPatVars
      :: (Traversable f
        , LabelPatVars a' b'
        , PatVarLabel b ~  PatVarLabel b'
        , f a' ~ a, f b' ~ b)
      => a -> State [PatVarLabel b] b
    labelPatVars = traverse labelPatVars
  
    default unlabelPatVars
      :: (Traversable f, LabelPatVars a' b', f a' ~ a, f b' ~ b)
      => b -> a
    unlabelPatVars = fmap unlabelPatVars
  
  instance LabelPatVars a b => LabelPatVars (Arg a) (Arg b) where
    type PatVarLabel (Arg b) = PatVarLabel b
  
  instance LabelPatVars a b => LabelPatVars (Named x a) (Named x b) where
    type PatVarLabel (Named x b) = PatVarLabel b
  
  instance LabelPatVars a b => LabelPatVars [a] [b] where
    type PatVarLabel [b] = PatVarLabel b
  
  instance LabelPatVars Pattern DeBruijnPattern where
    type PatVarLabel DeBruijnPattern = Int
  
    labelPatVars = \case
      VarP o x        -> VarP o . DBPatVar x <$> next
      DotP o t        -> DotP o t <$ next
      ConP c mt ps    -> ConP c mt <$> labelPatVars ps
      DefP o q  ps    -> DefP o q <$> labelPatVars ps
      LitP  o l       -> return $ LitP o l
      ProjP o q       -> return $ ProjP o q
      IApplyP o u t x -> IApplyP o u t . DBPatVar x <$> next
     where
      next = caseListM get __IMPOSSIBLE__ $ \x xs -> do
        put xs
        return x
    unlabelPatVars = fmap dbPatVarName
  
  -- | Augment pattern variables with their de Bruijn index.
  {-# SPECIALIZE numberPatVars :: Int -> Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
  --
  --  Example:
  --  @
  --    f : (A : Set) (n : Nat) (v : Vec A n) -> ...
  --    f A .(suc n) (cons n x xs)
  --
  --    clauseTel = (A : Set) (n : Nat) (x : A) (xs : Vec A n)
  --    perm      = Perm 5 [0,2,3,4]
  --    invertP __IMPOSSIBLE__ perm = Perm 4 [0,__IMPOSSIBLE__,1,2,3]
  --    flipP ... = Perm 4 [3,__IMPOSSIBLE__,2,1,0]
  --    pats      = A .(suc 2) (cons n x xs)
  --    dBpats    = 3 .(suc 2) (cons 2 1 0 )
  --  @
  --
  numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b
  numberPatVars err perm ps = evalState (labelPatVars ps) $
    permPicks $ flipP $ invertP err perm
  
  unnumberPatVars :: LabelPatVars a b => b -> a
  unnumberPatVars = unlabelPatVars
  
  dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
  dbPatPerm = dbPatPerm' True
  
  -- | Computes the permutation from the clause telescope
  --   to the pattern variables.
  --
  --   Use as @fromMaybe __IMPOSSIBLE__ . dbPatPerm@ to crash
  --   in a controlled way if a de Bruijn index is out of scope here.
  --
  --   The first argument controls whether dot patterns counts as variables or
  --   not.
  dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
  dbPatPerm' countDots ps = Perm (size ixs) <$> picks
    where
      ixs   = concatMap (getIndices . namedThing . unArg) ps
      n     = size $ catMaybes ixs
      picks = forM (downFrom n) $ \ i -> List.elemIndex (Just i) ixs
  
      getIndices :: DeBruijnPattern -> [Maybe Int]
      getIndices (VarP _ x)    = [Just $ dbPatVarIndex x]
      getIndices (ConP c _ ps) = concatMap (getIndices . namedThing . unArg) ps
      getIndices (DefP _ _ ps) = concatMap (getIndices . namedThing . unArg) ps
      getIndices (DotP _ _)    = [Nothing | countDots]
      getIndices (LitP _ _)    = []
      getIndices ProjP{}       = []
      getIndices (IApplyP _ _ _ x) = [Just $ dbPatVarIndex x]
  
  -- | Computes the permutation from the clause telescope
  --   to the pattern variables.
  --
  --   Use as @fromMaybe __IMPOSSIBLE__ . clausePerm@ to crash
  --   in a controlled way if a de Bruijn index is out of scope here.
  clausePerm :: Clause -> Maybe Permutation
  clausePerm = dbPatPerm . namedClausePats
  
  -- | Turn a pattern into a term.
  --   Projection patterns are turned into projection eliminations,
  --   other patterns into apply elimination.
  patternToElim :: Arg DeBruijnPattern -> Elim
  patternToElim (Arg ai (VarP o x)) = Apply $ Arg ai $ var $ dbPatVarIndex x
  patternToElim (Arg ai (ConP c cpi ps)) = Apply $ Arg ai $ Con c ci $
        map (patternToElim . fmap namedThing) ps
    where ci = fromConPatternInfo cpi
  patternToElim (Arg ai (DefP o q ps)) = Apply $ Arg ai $ Def q $
        map (patternToElim . fmap namedThing) ps
  patternToElim (Arg ai (DotP o t)   ) = Apply $ Arg ai t
  patternToElim (Arg ai (LitP o l)    ) = Apply $ Arg ai $ Lit l
  patternToElim (Arg ai (ProjP o dest)) = Proj o dest
  patternToElim (Arg ai (IApplyP o t u x)) = IApply t u $ var $ dbPatVarIndex x
  
  patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
  patternsToElims ps = map build ps
    where
      build :: NamedArg DeBruijnPattern -> Elim
      build = patternToElim . fmap namedThing
  
  patternToTerm :: DeBruijnPattern -> Term
  patternToTerm p = case patternToElim (defaultArg p) of
    Apply x -> unArg x
    Proj{}  -> __IMPOSSIBLE__
    IApply _ _ x -> x
  
  
  class MapNamedArgPattern a p where
    mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
  
    default mapNamedArgPattern
      :: (Functor f, MapNamedArgPattern a p', p ~ f p')
      => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
    mapNamedArgPattern = fmap . mapNamedArgPattern
  
  -- | Modify the content of @VarP@, and the closest surrounding @NamedArg@.
  --
  --   Note: the @mapNamedArg@ for @Pattern'@ is not expressible simply
  --   by @fmap@ or @traverse@ etc., since @ConP@ has @NamedArg@ subpatterns,
  --   which are taken into account by @mapNamedArg@.
  
  instance MapNamedArgPattern a (NamedArg (Pattern' a)) where
    mapNamedArgPattern f np =
      case namedArg np of
        VarP o x    -> f np
        DotP  o t   -> f np
        LitP o l    -> f np
        ProjP o q   -> f np
        ConP c i ps -> f $ setNamedArg np $ ConP c i $ mapNamedArgPattern f ps
        DefP o q ps -> f $ setNamedArg np $ DefP o q $ mapNamedArgPattern f ps
        IApplyP o u t x -> f np
  
  instance MapNamedArgPattern a p => MapNamedArgPattern a [p] where
  
  
  -- | Generic pattern traversal.
  --
  --   Pre-applies a pattern modification, recurses, and post-applies another one.
  
  class PatternLike a b where
  
    -- | Fold pattern.
    foldrPattern
      :: Monoid m
      => (Pattern' a -> m -> m)
           -- ^ Combine a pattern and the value computed from its subpatterns.
      -> b -> m
  
    default foldrPattern
      :: (Monoid m, Foldable f, PatternLike a p, f p ~ b)
      => (Pattern' a -> m -> m) -> b -> m
    foldrPattern = foldMap . foldrPattern
  
    -- | Traverse pattern.
    traversePatternM
      :: Monad m
      => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
      -> (Pattern' a -> m (Pattern' a))  -- ^ @post@: Modification after recursion.
      -> b -> m b
  
    default traversePatternM
      :: (Traversable f, PatternLike a p, f p ~ b, Monad m)
      => (Pattern' a -> m (Pattern' a))
      -> (Pattern' a -> m (Pattern' a))
      -> b -> m b
  
    traversePatternM pre post = traverse $ traversePatternM pre post
  
  -- | Compute from each subpattern a value and collect them all in a monoid.
  
  foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m
  foldPattern f = foldrPattern $ \ p m -> f p `mappend` m
  
  -- | Traverse pattern(s) with a modification before the recursive descent.
  
  preTraversePatternM
    :: (PatternLike a b, Monad m)
    => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
    -> b -> m b
  preTraversePatternM pre = traversePatternM pre return
  
  -- | Traverse pattern(s) with a modification after the recursive descent.
  
  postTraversePatternM :: (PatternLike a b, Monad m)
                       => (Pattern' a -> m (Pattern' a))  -- ^ @post@: Modification after recursion.
                       -> b -> m b
  postTraversePatternM = traversePatternM return
  
  -- This is where the action is:
  
  instance PatternLike a (Pattern' a) where
  
    foldrPattern f p = f p $ case p of
      ConP _ _ ps -> foldrPattern f ps
      DefP _ _ ps -> foldrPattern f ps
      VarP _ _    -> mempty
      LitP _ _    -> mempty
      DotP _ _    -> mempty
      ProjP _ _   -> mempty
      IApplyP{}   -> mempty
  
    traversePatternM pre post = pre >=> recurse >=> post
      where
      recurse p = case p of
        ConP c ci ps -> ConP c ci <$> traversePatternM pre post ps
        DefP o q ps  -> DefP o q <$> traversePatternM pre post ps
        VarP  _ _    -> return p
        LitP  _ _    -> return p
        DotP  _ _    -> return p
        ProjP _ _    -> return p
        IApplyP{}    -> return p
  
  -- Boilerplate instances:
  
  instance PatternLike a b => PatternLike a [b]         where
  instance PatternLike a b => PatternLike a (Arg b)     where
  instance PatternLike a b => PatternLike a (Named x b) where
  
  -- Counting pattern variables ---------------------------------------------
  
  class CountPatternVars a where
    countPatternVars :: a -> Int
  
    default countPatternVars :: (Foldable f, CountPatternVars b, f b ~ a) =>
                                a -> Int
    countPatternVars = getSum . foldMap (Sum . countPatternVars)
  
  instance CountPatternVars a => CountPatternVars [a] where
  instance CountPatternVars a => CountPatternVars (Arg a) where
  instance CountPatternVars a => CountPatternVars (Named x a) where
  
  instance CountPatternVars (Pattern' x) where
    countPatternVars p =
      case p of
        VarP{}      -> 1
        ConP _ _ ps -> countPatternVars ps
        DotP{}      -> 1   -- dot patterns are treated as variables in the clauses
        _           -> 0
  
  -- Computing modalities of pattern variables ------------------------------
  
  class PatternVarModalities p where
    type PatVar p
    -- | Get the list of pattern variables annotated with modalities.
    patternVarModalities :: p -> [(PatVar p, Modality)]
  
  instance PatternVarModalities a => PatternVarModalities [a] where
    type PatVar [a] = PatVar a
    patternVarModalities = foldMap patternVarModalities
  
  instance PatternVarModalities a => PatternVarModalities (Named s a) where
    type PatVar (Named s a) = PatVar a
    patternVarModalities = foldMap patternVarModalities
  
  instance PatternVarModalities a => PatternVarModalities (Arg a) where
    type PatVar (Arg a) = PatVar a
    patternVarModalities arg = map (second (composeModality m)) (patternVarModalities $ unArg arg)
      where m = getModality arg
  
  -- UNUSED:
  -- instance PatternVarModalities a x => PatternVarModalities (Elim' a) x where
  --   patternVarModalities (Apply x) = patternVarModalities x -- Note: x :: Arg a
  --   patternVarModalities (IApply x y p) = patternVarModalities [x, y, p]
  --   patternVarModalities Proj{}    = []
  
  instance PatternVarModalities (Pattern' x) where
    type PatVar (Pattern' x) = x
    patternVarModalities p =
      case p of
        VarP _ x    -> [(x, defaultModality)]
        ConP _ _ ps -> patternVarModalities ps
        DefP _ _ ps -> patternVarModalities ps
        DotP{}      -> []
        LitP{}      -> []
        ProjP{}     -> []
        IApplyP _ _ _ x -> [(x, defaultModality)]
  
  
  hasDefP :: [NamedArg DeBruijnPattern] -> Bool
  hasDefP ps = getAny $ flip foldPattern ps $ \ (x :: DeBruijnPattern) ->
                    case x of
                      DefP{} -> Any True
                      _      -> Any False
  