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

    {-| Definitions for fixity, precedence levels, and declared syntax.
    -}
    module Agda.Syntax.Fixity where

    import Prelude hiding (concatMap)

    import Control.DeepSeq

    import Data.Foldable
    import Data.Function
    import qualified Data.List as List
    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Traversable

    import Data.Data (Data)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import qualified Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Concrete.Name
    import Agda.Syntax.Notation

    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Pretty

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

    -- * Notation coupled with 'Fixity'

    -- | The notation is handled as the fixity in the renamer.
    --   Hence, they are grouped together in this type.
    data Fixity' = Fixity'
        { theFixity   :: !Fixity
        , theNotation :: Notation
        , theNameRange :: Range
          -- ^ Range of the name in the fixity declaration
          --   (used for correct highlighting, see issue #2140).
        }
      deriving (Data, Show)

    instance Eq Fixity' where
      Fixity' f n _ == Fixity' f' n' _ = f == f' && n == n'

    -- | Decorating something with @Fixity'@.
    data ThingWithFixity x = ThingWithFixity x Fixity'
      deriving (Functor, Foldable, Traversable, Data, Show)

    -- | All the notation information related to a name.
    data NewNotation = NewNotation
      { notaName  :: QName
      , notaNames :: Set A.Name
        -- ^ The names the syntax and/or fixity belong to.
        --
        -- Invariant: The set is non-empty. Every name in the list matches
        -- 'notaName'.
      , notaFixity :: Fixity
        -- ^ Associativity and precedence (fixity) of the names.
      , notation :: Notation
        -- ^ Syntax associated with the names.
      , notaIsOperator :: Bool
        -- ^ True if the notation comes from an operator (rather than a
        -- syntax declaration).
      } deriving Show

    -- | If an operator has no specific notation, then it is computed from
    -- its name.
    namesToNotation :: QName -> A.Name -> NewNotation
    namesToNotation q n = NewNotation
      { notaName       = q
      , notaNames      = Set.singleton n
      , notaFixity     = f
      , notation       = if null syn then syntaxOf (unqualify q) else syn
      , notaIsOperator = null syn
      }
      where Fixity' f syn _ = A.nameFixity n

    -- | Replace 'noFixity' by 'defaultFixity'.
    useDefaultFixity :: NewNotation -> NewNotation
    useDefaultFixity n
      | notaFixity n == noFixity = n { notaFixity = defaultFixity }
      | otherwise                = n

    -- | Return the 'IdPart's of a notation, the first part qualified,
    --   the other parts unqualified.
    --   This allows for qualified use of operators, e.g.,
    --   @M.for x ∈ xs return e@, or @x ℕ.+ y@.
    notationNames :: NewNotation -> [QName]
    notationNames (NewNotation q _ _ parts _) =
      zipWith ($) (reQualify : repeat QName) [Name noRange InScope [Id $ rangedThing x] | IdPart x <- parts ]
      where
        -- The qualification of @q@.
        modules     = init (qnameParts q)
        -- Putting the qualification onto @x@.
        reQualify x = List.foldr Qual (QName x) modules

    -- | Create a 'Notation' (without binders) from a concrete 'Name'.
    --   Does the obvious thing:
    --   'Hole's become 'NormalHole's, 'Id's become 'IdParts'.
    --   If 'Name' has no 'Hole's, it returns 'noNotation'.
    syntaxOf :: Name -> Notation
    syntaxOf (NoName _ _)    = noNotation
    syntaxOf (Name _ _ [_])  = noNotation
    syntaxOf (Name _ _ xs)   = mkSyn 0 xs
      where
        -- Turn a concrete name into a Notation,
        -- numbering the holes from left to right.
        -- Result will have no 'BindingHole's.
        mkSyn :: Int -> [NamePart] -> Notation
        mkSyn n []          = []
        mkSyn n (Hole : xs) = NormalHole noRange (defaultNamedArg $ unranged n) : mkSyn (1 + n) xs
        mkSyn n (Id x : xs) = IdPart (unranged x) : mkSyn n xs

    noFixity' :: Fixity'
    noFixity' = Fixity' noFixity noNotation noRange

    -- | Merges 'NewNotation's that have the same precedence level and
    -- notation, with two exceptions:
    --
    -- * Operators and notations coming from syntax declarations are kept
    --   separate.
    --
    -- * If /all/ instances of a given 'NewNotation' have the same
    --   precedence level or are \"unrelated\", then they are merged. They
    --   get the given precedence level, if any, and otherwise they become
    --   unrelated (but related to each other).
    --
    -- If 'NewNotation's that are merged have distinct associativities,
    -- then they get 'NonAssoc' as their associativity.
    --
    -- Precondition: No 'A.Name' may occur in more than one list element.
    -- Every 'NewNotation' must have the same 'notaName'.
    --
    -- Postcondition: No 'A.Name' occurs in more than one list element.
    mergeNotations :: [NewNotation] -> [NewNotation]
    mergeNotations =
      map merge .
      concatMap groupIfLevelsMatch .
      groupOn (\n -> ( notation n
                     , notaIsOperator n
                     ))
      where
      groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
      groupIfLevelsMatch []         = __IMPOSSIBLE__
      groupIfLevelsMatch ns@(n : _) =
        if allEqual (map fixityLevel related)
        then [sameAssoc (sameLevel ns)]
        else map (: []) ns
        where
        -- Fixities of operators whose precedence level is not Unrelated.
        related = mapMaybe (\f -> case fixityLevel f of
                                    Unrelated  -> Nothing
                                    Related {} -> Just f)
                           (map notaFixity ns)

        -- Precondition: All related operators have the same precedence
        -- level.
        --
        -- Gives all unrelated operators the same level.
        sameLevel = map (set (_notaFixity . _fixityLevel) level)
          where
          level = case related of
            f : _ -> fixityLevel f
            []    -> Unrelated

        -- If all related operators have the same associativity, then the
        -- unrelated operators get the same associativity, and otherwise
        -- all operators get the associativity NonAssoc.
        sameAssoc = map (set (_notaFixity . _fixityAssoc) assoc)
          where
          assoc = case related of
            f : _ | allEqual (map fixityAssoc related) -> fixityAssoc f
            _                                          -> NonAssoc

      merge :: [NewNotation] -> NewNotation
      merge []         = __IMPOSSIBLE__
      merge ns@(n : _) = n { notaNames = Set.unions $ map notaNames ns }

    -- * Sections

    -- | Sections, as well as non-sectioned operators.

    data NotationSection = NotationSection
      { sectNotation  :: NewNotation
      , sectKind      :: NotationKind
        -- ^ For non-sectioned operators this should match the notation's
        -- 'notationKind'.
      , sectLevel     :: Maybe PrecedenceLevel
        -- ^ Effective precedence level. 'Nothing' for closed notations.
      , sectIsSection :: Bool
        -- ^ 'False' for non-sectioned operators.
      }
      deriving Show

    -- | Converts a notation to a (non-)section.

    noSection :: NewNotation -> NotationSection
    noSection n = NotationSection
      { sectNotation  = n
      , sectKind      = notationKind (notation n)
      , sectLevel     = Just (fixityLevel (notaFixity n))
      , sectIsSection = False
      }

    -- * Fixity

    -- | Precedence levels for operators.

    data PrecedenceLevel
      = Unrelated
        -- ^ No fixity declared.
      | Related !Integer
        -- ^ Fixity level declared as the @Integer@.
      deriving (Eq, Ord, Show, Data)

    -- | Associativity.

    data Associativity = NonAssoc | LeftAssoc | RightAssoc
       deriving (Eq, Ord, Show, Data)

    -- | Fixity of operators.

    data Fixity = Fixity
      { fixityRange :: Range
        -- ^ Range of the whole fixity declaration.
      , fixityLevel :: !PrecedenceLevel
      , fixityAssoc :: !Associativity
      }
      deriving (Data, Show)

    instance Eq Fixity where
      f1 == f2 = compare f1 f2 == EQ

    instance Ord Fixity where
      compare = compare `on` (\f -> (fixityLevel f, fixityAssoc f))

    -- For @instance Pretty Fixity@, see Agda.Syntax.Concrete.Pretty

    noFixity :: Fixity
    noFixity = Fixity noRange Unrelated NonAssoc

    defaultFixity :: Fixity
    defaultFixity = Fixity noRange (Related 20) NonAssoc

    -- | Do we prefer parens around arguments like @λ x → x@ or not?
    --   See 'lamBrackets'.
    data ParenPreference = PreferParen | PreferParenless
      deriving (Eq, Ord, Show, Data)

    preferParen :: ParenPreference -> Bool
    preferParen p = PreferParen == p

    preferParenless :: ParenPreference -> Bool
    preferParenless p = PreferParenless == p

    -- * Precendence

    -- | Precedence is associated with a context.
    data Precedence = TopCtx | FunctionSpaceDomainCtx
                    | LeftOperandCtx Fixity | RightOperandCtx Fixity ParenPreference
                    | FunctionCtx | ArgumentCtx ParenPreference | InsideOperandCtx
                    | WithFunCtx | WithArgCtx | DotPatternCtx
        deriving (Show, Data, Eq)

    instance Pretty Precedence where
      pretty = text . show

    -- | When printing we keep track of a stack of precedences in order to be able
    --   to decide whether it's safe to leave out parens around lambdas. An empty
    --   stack is equivalent to `TopCtx`. Invariant: `notElem TopCtx`.
    type PrecedenceStack = [Precedence]

    pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
    pushPrecedence TopCtx _  = []
    pushPrecedence p      ps = p : ps

    headPrecedence :: PrecedenceStack -> Precedence
    headPrecedence []      = TopCtx
    headPrecedence (p : _) = p

    -- | Argument context preferring parens.
    argumentCtx_ :: Precedence
    argumentCtx_ = ArgumentCtx PreferParen

    -- | Do we need to bracket an operator application of the given fixity
    --   in a context with the given precedence.
    opBrackets :: Fixity -> PrecedenceStack -> Bool
    opBrackets = opBrackets' False

    -- | Do we need to bracket an operator application of the given fixity
    --   in a context with the given precedence.
    opBrackets' :: Bool ->   -- Is the last argument a parenless lambda?
                   Fixity -> PrecedenceStack -> Bool
    opBrackets' isLam f ps = brack f (headPrecedence ps)
      where
        false = isLam && lamBrackets ps -- require more parens for `e >>= λ x → e₁` than `e >>= e₁`
        brack                        (Fixity _ (Related n1) LeftAssoc)
                   (LeftOperandCtx   (Fixity _ (Related n2) LeftAssoc))  | n1 >= n2 = false
        brack                        (Fixity _ (Related n1) RightAssoc)
                   (RightOperandCtx  (Fixity _ (Related n2) RightAssoc) _) | n1 >= n2 = false
        brack f1   (LeftOperandCtx  f2) | Related f1 <- fixityLevel f1
                                        , Related f2 <- fixityLevel f2
                                        , f1 > f2 = false
        brack f1   (RightOperandCtx f2 _) | Related f1 <- fixityLevel f1
                                        , Related f2 <- fixityLevel f2
                                        , f1 > f2 = false
        brack _ TopCtx                 = false
        brack _ FunctionSpaceDomainCtx = false
        brack _ InsideOperandCtx       = false
        brack _ WithArgCtx             = false
        brack _ WithFunCtx             = false
        brack _ _                      = True

    -- | Does a lambda-like thing (lambda, let or pi) need brackets in the
    -- given context? A peculiar thing with lambdas is that they don't
    -- need brackets in certain right operand contexts. To decide we need to look
    -- at the stack of precedences and not just the current precedence.
    -- Example: @m₁ >>= (λ x → x) >>= m₂@ (for @_>>=_@ left associative).
    lamBrackets :: PrecedenceStack -> Bool
    lamBrackets []       = False
    lamBrackets (p : ps) = case p of
      TopCtx                 -> __IMPOSSIBLE__
      ArgumentCtx pref       -> preferParen pref || lamBrackets ps
      RightOperandCtx _ pref -> preferParen pref || lamBrackets ps
      FunctionSpaceDomainCtx -> True
      LeftOperandCtx{}       -> True
      FunctionCtx            -> True
      InsideOperandCtx       -> True
      WithFunCtx             -> True
      WithArgCtx             -> True
      DotPatternCtx          -> True

    -- | Does a function application need brackets?
    appBrackets :: PrecedenceStack -> Bool
    appBrackets = appBrackets' False

    -- | Does a function application need brackets?
    appBrackets' :: Bool ->   -- Is the argument of the application a parenless lambda?
                    PrecedenceStack -> Bool
    appBrackets' isLam ps = brack (headPrecedence ps)
      where
        brack ArgumentCtx{} = True
        brack DotPatternCtx = True
        brack _             = isLam && lamBrackets ps -- allow e + e₁ λ x → e₂

    -- | Does a with application need brackets?
    withAppBrackets :: PrecedenceStack -> Bool
    withAppBrackets = brack . headPrecedence
      where
        brack TopCtx                 = False
        brack FunctionSpaceDomainCtx = False
        brack WithFunCtx             = False
        brack _                      = True

    -- | Does a function space need brackets?
    piBrackets :: PrecedenceStack -> Bool
    piBrackets [] = False
    piBrackets _  = True

    roundFixBrackets :: PrecedenceStack -> Bool
    roundFixBrackets ps = DotPatternCtx == headPrecedence ps

    instance HasRange Fixity where
      getRange = fixityRange

    instance KillRange Fixity where
      killRange f = f { fixityRange = noRange }

    instance KillRange Fixity' where
      killRange (Fixity' f n r) = killRange3 Fixity' f n r

    instance KillRange x => KillRange (ThingWithFixity x) where
      killRange (ThingWithFixity c f) = ThingWithFixity (killRange c) f

    -- * Some lenses

    _notaFixity :: Lens' Fixity NewNotation
    _notaFixity f r = f (notaFixity r) <&> \x -> r { notaFixity = x }

    _fixityAssoc :: Lens' Associativity Fixity
    _fixityAssoc f r = f (fixityAssoc r) <&> \x -> r { fixityAssoc = x }

    _fixityLevel :: Lens' PrecedenceLevel Fixity
    _fixityLevel f r = f (fixityLevel r) <&> \x -> r { fixityLevel = x }

    ------------------------------------------------------------------------
    -- * Printing
    ------------------------------------------------------------------------

    -- deriving instance Show Fixity'

    ------------------------------------------------------------------------
    -- * NFData instances
    ------------------------------------------------------------------------

    instance NFData Fixity' where
      rnf (Fixity' _ a _) = rnf a

    -- | Ranges are not forced.

    instance NFData Fixity where
      rnf (Fixity _ _ _) = ()