    {-# LANGUAGE CPP          #-}
    {-# LANGUAGE GADTs        #-}
    {-# LANGUAGE TypeFamilies #-}

    module Agda.Syntax.Concrete.Operators.Parser where

    import Control.Applicative ( Alternative((<|>), many) )

    import Data.Either
    import Data.Hashable
    import Data.Maybe
    import qualified Data.Strict.Maybe as Strict
    import Data.Set (Set)

    import Agda.Syntax.Position
    import qualified Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Common
    import Agda.Syntax.Fixity
    import Agda.Syntax.Notation
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
    import qualified Agda.Syntax.Concrete.Operators.Parser.Monad as P

    import Agda.Utils.Pretty
    import Agda.Utils.List ( spanEnd )

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

    placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
    placeholder p =
      doc (text ("_" ++ show p)) $
      sat $ \t ->
      case t of
        Placeholder p' | p' == p -> True
        _                        -> False

    maybePlaceholder ::
      Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
    maybePlaceholder mp p = case mp of
      Nothing -> p'
      Just h  -> placeholder h <|> p'
      where
      p' = noPlaceholder <$> p

    satNoPlaceholder :: (e -> Maybe a) -> Parser e a
    satNoPlaceholder p = sat' $ \tok ->
      case tok of
        NoPlaceholder _ e -> p e
        Placeholder _     -> Nothing

    data ExprView e
        = LocalV QName
        | WildV e
        | OtherV e
        | AppV e (NamedArg e)
        | OpAppV QName (Set A.Name) [NamedArg (MaybePlaceholder (OpApp e))]
          -- ^ The 'QName' is possibly ambiguous, but it must correspond
          -- to one of the names in the set.
        | HiddenArgV (Named_ e)
        | InstanceArgV (Named_ e)
        | LamV [LamBinding] e
        | ParenV e
    --    deriving (Show)

    class HasRange e => IsExpr e where
        exprView   :: e -> ExprView e
        unExprView :: ExprView e -> e

    instance IsExpr e => HasRange (ExprView e) where
      getRange = getRange . unExprView

    instance IsExpr Expr where
        exprView e = case e of
            Ident x         -> LocalV x
            App _ e1 e2     -> AppV e1 e2
            OpApp r d ns es -> OpAppV d ns es
            HiddenArg _ e   -> HiddenArgV e
            InstanceArg _ e -> InstanceArgV e
            Paren _ e       -> ParenV e
            Lam _ bs    e   -> LamV bs e
            Underscore{}    -> WildV e
            _               -> OtherV e
        unExprView e = case e of
            LocalV x       -> Ident x
            AppV e1 e2     -> App (fuseRange e1 e2) e1 e2
            OpAppV d ns es -> OpApp (fuseRange d es) d ns es
            HiddenArgV e   -> HiddenArg (getRange e) e
            InstanceArgV e -> InstanceArg (getRange e) e
            ParenV e       -> Paren (getRange e) e
            LamV bs e      -> Lam (fuseRange bs e) bs e
            WildV e        -> e
            OtherV e       -> e

    instance IsExpr Pattern where
        exprView e = case e of
            IdentP x         -> LocalV x
            AppP e1 e2       -> AppV e1 e2
            OpAppP r d ns es -> OpAppV d ns ((map . fmap . fmap)
                                               (noPlaceholder . Ordinary) es)
            HiddenP _ e      -> HiddenArgV e
            InstanceP _ e    -> InstanceArgV e
            ParenP _ e       -> ParenV e
            WildP{}          -> WildV e
            _                -> OtherV e
        unExprView e = case e of
            LocalV x       -> IdentP x
            AppV e1 e2     -> AppP e1 e2
            OpAppV d ns es -> let ess :: [NamedArg Pattern]
                                  ess = (map . fmap . fmap)
                                          (\x -> case x of
                                              Placeholder{}     -> __IMPOSSIBLE__
                                              NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)
                                          es
                              in OpAppP (fuseRange d ess) d ns ess
            HiddenArgV e   -> HiddenP (getRange e) e
            InstanceArgV e -> InstanceP (getRange e) e
            ParenV e       -> ParenP (getRange e) e
            LamV _ _       -> __IMPOSSIBLE__
            WildV e        -> e
            OtherV e       -> e

    -- | Should sections be parsed?
    data ParseSections = ParseSections | DoNotParseSections
      deriving (Eq, Show)

    -- | Runs a parser. If sections should be parsed, then identifiers
    -- with at least two name parts are split up into multiple tokens,
    -- using 'PositionInName' to record the tokens' original positions
    -- within their respective identifiers.

    parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
    parse (DoNotParseSections, p) es = P.parse p (map noPlaceholder es)
    parse (ParseSections,      p) es = P.parse p (concat $ map splitExpr es)
      where
      splitExpr :: IsExpr e => e -> [MaybePlaceholder e]
      splitExpr e = case exprView e of
        LocalV n -> splitName n
        _        -> noSplit
        where
        noSplit = [noPlaceholder e]

        splitName n = case last ns of
          Name r nis ps@(_ : _ : _) -> splitParts r nis (init ns) Beginning ps
          _                         -> noSplit
          where
          ns = qnameParts n

          -- Note that the same range is used for every name part. This is
          -- not entirely correct, but will hopefully not lead to any
          -- problems.

          -- Note also that the module qualifier, if any, is only applied
          -- to the first name part.

          splitParts _ _   _ _ []          = __IMPOSSIBLE__
          splitParts _ _   _ _ (Hole : []) = [Placeholder End]
          splitParts r nis m _ (Id s : []) = [part r nis m End s]
          splitParts r nis m w (Hole : ps) = Placeholder w : splitParts r nis m  Middle ps
          splitParts r nis m w (Id s : ps) = part r nis m w s : splitParts r nis [] Middle ps

          part r nis m w s =
            NoPlaceholder (Strict.Just w)
                          (unExprView $ LocalV $
                             foldr Qual (QName (Name r nis [Id s])) m)

    ---------------------------------------------------------------------------
    -- * Parser combinators
    ---------------------------------------------------------------------------

    ----------------------------
    -- Specific combinators

    -- | Parse a specific identifier as a NamePart
    partP :: IsExpr e => [Name] -> RawName -> Parser e Range
    partP ms s =
      doc (text (show str)) $
      satNoPlaceholder isLocal
      where
      str = prettyShow $ foldr Qual (QName $ Name noRange InScope [Id s]) ms
      isLocal e = case exprView e of
          LocalV y | str == prettyShow y -> Just $ getRange y
          _ -> Nothing

    -- | Parses a split-up, unqualified name consisting of at least two
    -- name parts.
    --
    -- The parser does not check that underscores and other name parts
    -- alternate. The range of the resulting name is the range of the
    -- first name part that is not an underscore.

    atLeastTwoParts :: IsExpr e => Parser e Name
    atLeastTwoParts =
      (\p1 ps p2 ->
          let all = p1 : ps ++ [p2] in
          case mapMaybe fst all of
            (r,nis) : _ -> Name r nis (map snd all)
            []          -> __IMPOSSIBLE__)
      <$> part Beginning
      <*> many (part Middle)
      <*> part End
      where
      part pos = sat' $ \tok -> case tok of
        Placeholder pos'                   | pos == pos' -> Just ( Nothing
                                                                 , Hole
                                                                 )
        NoPlaceholder (Strict.Just pos') e | pos == pos' ->
          case exprView e of
            LocalV (QName (Name r nis [Id s])) -> Just (Just (r,nis), Id s)
            _                                  -> Nothing
        _ -> Nothing

    -- | Either a wildcard (@_@), or an unqualified name (possibly
    -- containing multiple name parts).

    wildOrUnqualifiedName :: IsExpr e => Parser e (Maybe Name)
    wildOrUnqualifiedName =
      (Nothing <$ partP [] "_")
        <|>
      (satNoPlaceholder $ \e ->
         case exprView e of
           LocalV (QName n) -> Just (Just n)
           WildV _          -> Just Nothing
           _                -> Nothing)
        <|>
      Just <$> atLeastTwoParts

    -- | Used to define the return type of 'opP'.

    type family OperatorType (k :: NotationKind) (e :: *) :: *
    type instance OperatorType 'InfixNotation   e = MaybePlaceholder e -> MaybePlaceholder e -> e
    type instance OperatorType 'PrefixNotation  e = MaybePlaceholder e -> e
    type instance OperatorType 'PostfixNotation e = MaybePlaceholder e -> e
    type instance OperatorType 'NonfixNotation  e = e

    -- | A singleton type for 'NotationKind' (except for the constructor
    -- 'NoNotation').

    data NK (k :: NotationKind) :: * where
      In   :: NK 'InfixNotation
      Pre  :: NK 'PrefixNotation
      Post :: NK 'PostfixNotation
      Non  :: NK 'NonfixNotation

    -- | Parse the \"operator part\" of the given notation.
    --
    -- Normal holes (but not binders) at the beginning and end are
    -- ignored.
    --
    -- If the notation does not contain any binders, then a section
    -- notation is allowed.
    opP :: forall e k. IsExpr e
        => ParseSections
        -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    opP parseSections p (NewNotation q names _ syn isOp) kind =
      flip fmap (worker (init $ qnameParts q)
                        withoutExternalHoles) $ \(range, hs) ->

      let (normal, binders) = partitionEithers hs
          lastHole          = maximum $ mapMaybe holeTarget syn

          app :: ([(MaybePlaceholder e, NamedArg (Ranged Int))] ->
                  [(MaybePlaceholder e, NamedArg (Ranged Int))]) -> e
          app f =
            -- If we have an operator and there is exactly one
            -- placeholder for every hole, then we only return
            -- the operator.
            if isOp && noPlaceholders args == lastHole + 1 then
              -- Note that the information in the set "names" is thrown
              -- away here.
              unExprView (LocalV q')
            else
              unExprView (OpAppV q' names args)
            where
            args = map (findExprFor (f normal) binders) [0..lastHole]
            q'   = setRange range q
      in

      case kind of
        In   -> \x y -> app (\es -> (x, leadingHole) : es ++ [(y, trailingHole)])
        Pre  -> \  y -> app (\es ->                    es ++ [(y, trailingHole)])
        Post -> \x   -> app (\es -> (x, leadingHole) : es)
        Non  ->         app (\es ->                    es)

      where

      (leadingHoles, syn1)                  = span    isNormalHole syn
      (withoutExternalHoles, trailingHoles) = spanEnd isNormalHole syn1

      leadingHole = case leadingHoles of
        [NormalHole _ h] -> h
        _                -> __IMPOSSIBLE__

      trailingHole = case trailingHoles of
        [NormalHole _ h] -> h
        _                -> __IMPOSSIBLE__

      worker ::
        [Name] -> Notation ->
        Parser e (Range, [Either (MaybePlaceholder e, NamedArg (Ranged Int))
                                 (LamBinding, Ranged Int)])
      worker ms []              = pure (noRange, [])
      worker ms (IdPart x : xs) =
        (\r1 (r2, es) -> (fuseRanges r1 r2, es))
          <$> partP ms (rangedThing x)
          <*> worker [] xs
              -- Only the first part is qualified.
      worker ms (NormalHole _ h : xs) =
        (\e (r, es) -> (r, Left (e, h) : es))
          <$> maybePlaceholder
                (if isOp && parseSections == ParseSections
                 then Just Middle else Nothing)
                p
          <*> worker ms xs
      worker ms (WildHole h : xs) =
        (\(r, es) -> (r, Right (mkBinding h $ Name noRange InScope [Hole]) : es))
          <$> worker ms xs
      worker ms (BindHole _ h : xs) = do
        (\e (r, es) ->
            let x = case e of
                      Just name -> name
                      Nothing   -> Name noRange InScope [Hole]
            in (r, Right (mkBinding h x) : es))
               -- Andreas, 2011-04-07 put just 'Relevant' here, is this
               -- correct?
          <$> wildOrUnqualifiedName
          <*> worker ms xs

      mkBinding h x = (DomainFree $ defaultNamedArg $ mkBoundName_ x, h)

      set x arg = fmap (fmap (const x)) arg

      findExprFor ::
        [(MaybePlaceholder e, NamedArg (Ranged Int))] ->
        [(LamBinding, Ranged Int)] -> Int ->
        NamedArg (MaybePlaceholder (OpApp e))
      findExprFor normalHoles binders n =
        case [ h | h@(_, m) <- normalHoles, rangedThing (namedArg m) == n ] of
          [(Placeholder p,     arg)] -> set (Placeholder p) arg
          [(NoPlaceholder _ e, arg)] -> case [b | (b, m) <- binders, rangedThing m == n] of
            [] -> set (noPlaceholder (Ordinary e)) arg -- no variable to bind
            bs -> set (noPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg
          _ -> __IMPOSSIBLE__

      noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int
      noPlaceholders = sum . map (isPlaceholder . namedArg)
        where
        isPlaceholder NoPlaceholder{} = 0
        isPlaceholder Placeholder{}   = 1

    argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
    argsP p = many (mkArg <$> p)
      where
      mkArg e = case exprView e of
        HiddenArgV   e -> hide (defaultArg e)
        InstanceArgV e -> makeInstance (defaultArg e)
        _              -> defaultArg (unnamed e)

    appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
    appP p pa = foldl app <$> p <*> pa
        where
            app e = unExprView . AppV e

    atomP :: IsExpr e => (QName -> Bool) -> Parser e e
    atomP p =
      doc "<atom>" $
      satNoPlaceholder $ \e ->
      case exprView e of
        LocalV x | not (p x) -> Nothing
        _                    -> Just e