    {-# LANGUAGE CPP                 #-}
    {-# LANGUAGE DeriveDataTypeable  #-}

    {-| As a concrete name, a notation is a non-empty list of alternating 'IdPart's and holes.
        In contrast to concrete names, holes can be binders.

        Example:
        @
           syntax fmap (λ x → e) xs = for x ∈ xs return e
        @

        The declared notation for @fmap@ is @for_∈_return_@ where the first hole is a binder.
    -}

    module Agda.Syntax.Notation where

    import Control.DeepSeq
    import Control.Monad

    import qualified Data.List as List
    import Data.Maybe

    import Data.Data (Data)

    import Agda.Syntax.Common
    import Agda.Syntax.Position

    import Agda.Utils.Except ( MonadError(throwError) )
    import Agda.Utils.List

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

    -- | Data type constructed in the Happy parser; converted to 'GenPart'
    --   before it leaves the Happy code.
    data HoleName
      = LambdaHole { _bindHoleName :: RString
                   , holeName      :: RString }
        -- ^ @\ x -> y@; 1st argument is the bound name (unused for now).
      | ExprHole   { holeName      :: RString }
        -- ^ Simple named hole with hiding.

    -- | Is the hole a binder?
    isLambdaHole :: HoleName -> Bool
    isLambdaHole (LambdaHole _ _) = True
    isLambdaHole _ = False

    -- | Notation as provided by the @syntax@ declaration.
    type Notation = [GenPart]

    -- | Part of a Notation
    data GenPart
      = BindHole Range (Ranged Int)
        -- ^ Argument is the position of the hole (with binding) where the binding should occur.
        --   First range is the rhs range and second is the binder.
      | NormalHole Range (NamedArg (Ranged Int))
        -- ^ Argument is where the expression should go.
      | WildHole (Ranged Int)
        -- ^ An underscore in binding position.
      | IdPart RString
      deriving (Data, Show)

    instance Eq GenPart where
      BindHole _ i   == BindHole _ j   = i == j
      NormalHole _ x == NormalHole _ y = x == y
      WildHole i     == WildHole j     = i == j
      IdPart x       == IdPart y       = x == y
      _              == _              = False

    instance Ord GenPart where
      BindHole _ i   `compare` BindHole _ j   = i `compare` j
      NormalHole _ x `compare` NormalHole _ y = x `compare` y
      WildHole i     `compare` WildHole j     = i `compare` j
      IdPart x       `compare` IdPart y       = x `compare` y
      BindHole{}     `compare` _              = LT
      _              `compare` BindHole{}     = GT
      NormalHole{}   `compare` _              = LT
      _              `compare` NormalHole{}   = GT
      WildHole{}     `compare` _              = LT
      _              `compare` WildHole{}     = GT

    instance HasRange GenPart where
      getRange p = case p of
        IdPart x       -> getRange x
        BindHole r _   -> r
        WildHole i     -> getRange i
        NormalHole r _ -> r

    instance SetRange GenPart where
      setRange r p = case p of
        IdPart x       -> IdPart x
        BindHole _ i   -> BindHole r i
        WildHole i     -> WildHole i
        NormalHole _ i -> NormalHole r i

    instance KillRange GenPart where
      killRange p = case p of
        IdPart x       -> IdPart $ killRange x
        BindHole _ i   -> BindHole noRange $ killRange i
        WildHole i     -> WildHole $ killRange i
        NormalHole _ x -> NormalHole noRange $ killRange x

    instance NFData GenPart where
      rnf (BindHole _ a)   = rnf a
      rnf (NormalHole _ a) = rnf a
      rnf (WildHole a)     = rnf a
      rnf (IdPart a)       = rnf a

    -- | Get a flat list of identifier parts of a notation.
    stringParts :: Notation -> [String]
    stringParts gs = [ rangedThing x | IdPart x <- gs ]

    -- | Target argument position of a part (Nothing if it is not a hole).
    holeTarget :: GenPart -> Maybe Int
    holeTarget (BindHole _   n) = Just $ rangedThing n
    holeTarget (WildHole     n) = Just $ rangedThing n
    holeTarget (NormalHole _ n) = Just $ rangedThing $ namedArg n
    holeTarget IdPart{}         = Nothing

    -- | Is the part a hole? WildHoles don't count since they don't correspond to
    --   anything the user writes.
    isAHole :: GenPart -> Bool
    isAHole BindHole{}   = True
    isAHole NormalHole{} = True
    isAHole WildHole{}   = False
    isAHole IdPart{}     = False

    -- | Is the part a normal hole?
    isNormalHole :: GenPart -> Bool
    isNormalHole NormalHole{} = True
    isNormalHole BindHole{}   = False
    isNormalHole WildHole{}   = False
    isNormalHole IdPart{}     = False

    -- | Is the part a binder?
    isBindingHole :: GenPart -> Bool
    isBindingHole BindHole{} = True
    isBindingHole WildHole{} = True
    isBindingHole _          = False

    -- | Classification of notations.

    data NotationKind
      = InfixNotation   -- ^ Ex: @_bla_blub_@.
      | PrefixNotation  -- ^ Ex: @_bla_blub@.
      | PostfixNotation -- ^ Ex: @bla_blub_@.
      | NonfixNotation  -- ^ Ex: @bla_blub@.
      | NoNotation
       deriving (Eq, Show)

    -- | Classify a notation by presence of leading and/or trailing
    -- /normal/ holes.
    notationKind :: Notation -> NotationKind
    notationKind []  = NoNotation
    notationKind syn =
      case (isNormalHole $ head syn, isNormalHole $ last syn) of
        (True , True ) -> InfixNotation
        (True , False) -> PostfixNotation
        (False, True ) -> PrefixNotation
        (False, False) -> NonfixNotation

    -- | From notation with names to notation with indices.
    --
    --   Example:
    --   @
    --      ids   = ["for", "x", "∈", "xs", "return", "e"]
    --      holes = [ LambdaHole "x" "e",  ExprHole "xs" ]
    --   @
    --   creates the notation
    --   @
    --      [ IdPart "for"    , BindHole 0
    --      , IdPart "∈"      , NormalHole 1
    --      , IdPart "return" , NormalHole 0
    --      ]
    --   @
    mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
    mkNotation _ [] = throwError "empty notation is disallowed"
    mkNotation holes ids = do
      unless uniqueHoleNames     $ throwError "syntax must use unique argument names"
      let xs :: Notation = map mkPart ids
      unless (isAlternating xs)  $ throwError $ concat
         [ "syntax must alternate holes ("
         , prettyHoles
         , ") and non-holes ("
         , prettyNonHoles xs
         , ")"
         ]
      unless (isExprLinear xs)   $ throwError "syntax must use holes exactly once"
      unless (isLambdaLinear xs) $ throwError "syntax must use binding holes exactly once"
      -- Andreas, 2018-10-18, issue #3285:
      -- syntax that is just a single hole is ill-formed and crashes the operator parser
      when   (isSingleHole xs)   $ throwError "syntax cannot be a single hole"
      return $ insertWildHoles xs
        where
          holeNames :: [RString]
          holeNames = map namedArg holes >>= \case
            LambdaHole x y -> [x, y]
            ExprHole y     -> [y]

          prettyHoles :: String
          prettyHoles = List.unwords $ map (rawNameToString . rangedThing) holeNames

          nonHoleNames :: Notation -> [RString]
          nonHoleNames xs = flip mapMaybe xs $ \case
            WildHole{}   -> Just $ unranged "_"
            IdPart x     -> Just x
            BindHole{}   -> Nothing
            NormalHole{} -> Nothing

          prettyNonHoles :: Notation -> String
          prettyNonHoles = List.unwords . map (rawNameToString . rangedThing) . nonHoleNames

          mkPart ident = maybe (IdPart ident) (`withRangeOf` ident) $ lookup ident holeMap

          holeNumbers   = [0 .. length holes - 1]

          numberedHoles :: [(Int, NamedArg HoleName)]
          numberedHoles = zip holeNumbers holes

          -- The WildHoles don't correspond to anything in the right-hand side so
          -- we add them next to their corresponding body. Slightly subtle: due to
          -- the way the operator parsing works they can't be added first or last.
          insertWildHoles :: [GenPart] -> [GenPart]
          insertWildHoles xs = foldr ins xs wilds
            where
              wilds = [ i | (_, WildHole i) <- holeMap ]
              ins w (NormalHole r h : hs)
                | namedArg h == w = NormalHole r h : WildHole w : hs
              ins w (h : hs) = h : insBefore w hs
              ins _ [] = __IMPOSSIBLE__

              insBefore w (NormalHole r h : hs)
                | namedArg h == w = WildHole w : NormalHole r h : hs
              insBefore w (h : hs) = h : insBefore w hs
              insBefore _ [] = __IMPOSSIBLE__

          -- Create a map (association list) from hole names to holes.
          -- A @LambdaHole@ contributes two entries:
          -- both names are mapped to the same number,
          -- but distinguished by BindHole vs. NormalHole.
          holeMap :: [(RString, GenPart)]
          holeMap = do
            (i, h) <- numberedHoles    -- v This range is filled in by mkPart
            let ri x = Ranged (getRange x) i
                normalHole y = NormalHole noRange $ fmap (ri y <$) h
            case namedArg h of
              ExprHole y       -> [(y, normalHole y)]
              LambdaHole x y
                | "_" <- rangedThing x -> [(x, WildHole (ri x)),         (y, normalHole y)]
                | otherwise            -> [(x, BindHole noRange (ri x)), (y, normalHole y)]
                                                     -- Filled in by mkPart

          -- Check whether all hole names are distinct.
          -- The hole names are the keys of the @holeMap@.
          uniqueHoleNames = distinct [ x | (x, _) <- holeMap, rangedThing x /= "_" ]

          isExprLinear   xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers
          isLambdaLinear xs = List.sort [ rangedThing x | BindHole _ x <- xs ] ==
                              [ i | (i, h) <- numberedHoles,
                                    LambdaHole x _ <- [namedArg h], rangedThing x /= "_" ]

          isAlternating :: [GenPart] -> Bool
          isAlternating []       = __IMPOSSIBLE__
          isAlternating [x]      = True
          isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)

          isSingleHole :: [GenPart] -> Bool
          isSingleHole = \case
            [ IdPart{} ] -> False
            [ _hole ]    -> True
            _            -> False

    noNotation :: Notation
    noNotation = []