    module Agda.Syntax.Internal.Pattern where

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Utils.Tuple

    data OneHolePatterns = OHPats [Arg Pattern] (Arg OneHolePattern) [Arg Pattern]
      deriving (Show)
    data OneHolePattern  = Hole
    		     | OHCon QName OneHolePatterns
      deriving (Show)

    plugHole :: Pattern -> OneHolePatterns -> [Arg Pattern]
    plugHole p (OHPats ps hole qs) = ps ++ [fmap (plug p) hole] ++ qs
      where
        plug p Hole	       = p
        plug p (OHCon c h) = ConP c $ plugHole p h

    allHoles :: [Arg Pattern] -> [OneHolePatterns]
    allHoles = map snd . allHolesWithContents

    allHolesWithContents :: [Arg Pattern] -> [(Pattern, OneHolePatterns)]
    allHolesWithContents []       = []
    allHolesWithContents (p : ps) = map left phs ++ map (right p) (allHolesWithContents ps)
      where
        phs :: [(Pattern, Arg OneHolePattern)]
        phs = map (id -*- Arg (argHiding p)) (holes $ unArg p)

        holes :: Pattern -> [(Pattern, OneHolePattern)]
        holes p@(VarP _)  = [(p, Hole)]
        holes p@(DotP _)  = [(p, Hole)]
        holes (ConP c qs) = map (id -*- OHCon c) $ allHolesWithContents qs
        holes _           = []

        left  (p, ph)               = (p, OHPats [] ph ps)
        right q (p, OHPats ps h qs) = (p, OHPats (q : ps) h qs)