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

import Control.DeepSeq

import GHC.Generics (Generic)

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

import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- The Fixity data type is now defined in Agda.Syntax.Common.
-- Andreas, 2019-08-16, issue #1346

-- | Decorating something with @Fixity'@.
data ThingWithFixity x = ThingWithFixity x Fixity'
  deriving (forall a b. a -> ThingWithFixity b -> ThingWithFixity a
forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ThingWithFixity b -> ThingWithFixity a
$c<$ :: forall a b. a -> ThingWithFixity b -> ThingWithFixity a
fmap :: forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
$cfmap :: forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
Functor, forall a. Eq a => a -> ThingWithFixity a -> Bool
forall a. Num a => ThingWithFixity a -> a
forall a. Ord a => ThingWithFixity a -> a
forall m. Monoid m => ThingWithFixity m -> m
forall a. ThingWithFixity a -> Bool
forall a. ThingWithFixity a -> Int
forall a. ThingWithFixity a -> [a]
forall a. (a -> a -> a) -> ThingWithFixity a -> a
forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => ThingWithFixity a -> a
$cproduct :: forall a. Num a => ThingWithFixity a -> a
sum :: forall a. Num a => ThingWithFixity a -> a
$csum :: forall a. Num a => ThingWithFixity a -> a
minimum :: forall a. Ord a => ThingWithFixity a -> a
$cminimum :: forall a. Ord a => ThingWithFixity a -> a
maximum :: forall a. Ord a => ThingWithFixity a -> a
$cmaximum :: forall a. Ord a => ThingWithFixity a -> a
elem :: forall a. Eq a => a -> ThingWithFixity a -> Bool
$celem :: forall a. Eq a => a -> ThingWithFixity a -> Bool
length :: forall a. ThingWithFixity a -> Int
$clength :: forall a. ThingWithFixity a -> Int
null :: forall a. ThingWithFixity a -> Bool
$cnull :: forall a. ThingWithFixity a -> Bool
toList :: forall a. ThingWithFixity a -> [a]
$ctoList :: forall a. ThingWithFixity a -> [a]
foldl1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
foldr1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
fold :: forall m. Monoid m => ThingWithFixity m -> m
$cfold :: forall m. Monoid m => ThingWithFixity m -> m
Foldable, Functor ThingWithFixity
Foldable ThingWithFixity
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
ThingWithFixity (m a) -> m (ThingWithFixity a)
forall (f :: * -> *) a.
Applicative f =>
ThingWithFixity (f a) -> f (ThingWithFixity a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
sequence :: forall (m :: * -> *) a.
Monad m =>
ThingWithFixity (m a) -> m (ThingWithFixity a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
ThingWithFixity (m a) -> m (ThingWithFixity a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
ThingWithFixity (f a) -> f (ThingWithFixity a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
ThingWithFixity (f a) -> f (ThingWithFixity a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
Traversable, Int -> ThingWithFixity x -> ShowS
forall x. Show x => Int -> ThingWithFixity x -> ShowS
forall x. Show x => [ThingWithFixity x] -> ShowS
forall x. Show x => ThingWithFixity x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThingWithFixity x] -> ShowS
$cshowList :: forall x. Show x => [ThingWithFixity x] -> ShowS
show :: ThingWithFixity x -> String
$cshow :: forall x. Show x => ThingWithFixity x -> String
showsPrec :: Int -> ThingWithFixity x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> ThingWithFixity x -> ShowS
Show)

instance LensFixity' (ThingWithFixity a) where
  lensFixity' :: Lens' Fixity' (ThingWithFixity a)
lensFixity' Fixity' -> f Fixity'
f (ThingWithFixity a
a Fixity'
fix') = forall x. x -> Fixity' -> ThingWithFixity x
ThingWithFixity a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fixity' -> f Fixity'
f Fixity'
fix'

instance LensFixity (ThingWithFixity a) where
  lensFixity :: Lens' Fixity (ThingWithFixity a)
lensFixity = forall a. LensFixity' a => Lens' Fixity' a
lensFixity' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensFixity a => Lens' Fixity a
lensFixity

-- | Do we prefer parens around arguments like @λ x → x@ or not?
--   See 'lamBrackets'.
data ParenPreference = PreferParen | PreferParenless
  deriving (ParenPreference -> ParenPreference -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParenPreference -> ParenPreference -> Bool
$c/= :: ParenPreference -> ParenPreference -> Bool
== :: ParenPreference -> ParenPreference -> Bool
$c== :: ParenPreference -> ParenPreference -> Bool
Eq, Eq ParenPreference
ParenPreference -> ParenPreference -> Bool
ParenPreference -> ParenPreference -> Ordering
ParenPreference -> ParenPreference -> ParenPreference
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ParenPreference -> ParenPreference -> ParenPreference
$cmin :: ParenPreference -> ParenPreference -> ParenPreference
max :: ParenPreference -> ParenPreference -> ParenPreference
$cmax :: ParenPreference -> ParenPreference -> ParenPreference
>= :: ParenPreference -> ParenPreference -> Bool
$c>= :: ParenPreference -> ParenPreference -> Bool
> :: ParenPreference -> ParenPreference -> Bool
$c> :: ParenPreference -> ParenPreference -> Bool
<= :: ParenPreference -> ParenPreference -> Bool
$c<= :: ParenPreference -> ParenPreference -> Bool
< :: ParenPreference -> ParenPreference -> Bool
$c< :: ParenPreference -> ParenPreference -> Bool
compare :: ParenPreference -> ParenPreference -> Ordering
$ccompare :: ParenPreference -> ParenPreference -> Ordering
Ord, Int -> ParenPreference -> ShowS
[ParenPreference] -> ShowS
ParenPreference -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ParenPreference] -> ShowS
$cshowList :: [ParenPreference] -> ShowS
show :: ParenPreference -> String
$cshow :: ParenPreference -> String
showsPrec :: Int -> ParenPreference -> ShowS
$cshowsPrec :: Int -> ParenPreference -> ShowS
Show, forall x. Rep ParenPreference x -> ParenPreference
forall x. ParenPreference -> Rep ParenPreference x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ParenPreference x -> ParenPreference
$cfrom :: forall x. ParenPreference -> Rep ParenPreference x
Generic)

instance NFData ParenPreference

preferParen :: ParenPreference -> Bool
preferParen :: ParenPreference -> Bool
preferParen ParenPreference
p = ParenPreference
PreferParen forall a. Eq a => a -> a -> Bool
== ParenPreference
p

preferParenless :: ParenPreference -> Bool
preferParenless :: ParenPreference -> Bool
preferParenless ParenPreference
p = ParenPreference
PreferParenless forall a. Eq a => a -> a -> Bool
== ParenPreference
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 (Int -> Precedence -> ShowS
[Precedence] -> ShowS
Precedence -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Precedence] -> ShowS
$cshowList :: [Precedence] -> ShowS
show :: Precedence -> String
$cshow :: Precedence -> String
showsPrec :: Int -> Precedence -> ShowS
$cshowsPrec :: Int -> Precedence -> ShowS
Show, Precedence -> Precedence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Precedence -> Precedence -> Bool
$c/= :: Precedence -> Precedence -> Bool
== :: Precedence -> Precedence -> Bool
$c== :: Precedence -> Precedence -> Bool
Eq, forall x. Rep Precedence x -> Precedence
forall x. Precedence -> Rep Precedence x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Precedence x -> Precedence
$cfrom :: forall x. Precedence -> Rep Precedence x
Generic)

instance NFData Precedence

instance Pretty Precedence where
  pretty :: Precedence -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
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 :: Precedence -> [Precedence] -> [Precedence]
pushPrecedence Precedence
TopCtx [Precedence]
_  = []
pushPrecedence Precedence
p      [Precedence]
ps = Precedence
p forall a. a -> [a] -> [a]
: [Precedence]
ps

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

-- | Argument context preferring parens.
argumentCtx_ :: Precedence
argumentCtx_ :: Precedence
argumentCtx_ = ParenPreference -> Precedence
ArgumentCtx ParenPreference
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 :: Fixity -> [Precedence] -> Bool
opBrackets = Bool -> Fixity -> [Precedence] -> Bool
opBrackets' Bool
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' :: Bool -> Fixity -> [Precedence] -> Bool
opBrackets' Bool
isLam Fixity
f [Precedence]
ps = Fixity -> Precedence -> Bool
brack Fixity
f ([Precedence] -> Precedence
headPrecedence [Precedence]
ps)
  where
    false :: Bool
false = Bool
isLam Bool -> Bool -> Bool
&& [Precedence] -> Bool
lamBrackets [Precedence]
ps -- require more parens for `e >>= λ x → e₁` than `e >>= e₁`
    brack :: Fixity -> Precedence -> Bool
brack                        (Fixity Range
_ (Related PrecedenceLevel
n1) Associativity
LeftAssoc)
               (LeftOperandCtx   (Fixity Range
_ (Related PrecedenceLevel
n2) Associativity
LeftAssoc))  | PrecedenceLevel
n1 forall a. Ord a => a -> a -> Bool
>= PrecedenceLevel
n2 = Bool
false
    brack                        (Fixity Range
_ (Related PrecedenceLevel
n1) Associativity
RightAssoc)
               (RightOperandCtx  (Fixity Range
_ (Related PrecedenceLevel
n2) Associativity
RightAssoc) ParenPreference
_) | PrecedenceLevel
n1 forall a. Ord a => a -> a -> Bool
>= PrecedenceLevel
n2 = Bool
false
    brack Fixity
f1   (LeftOperandCtx  Fixity
f2) | Related PrecedenceLevel
f1 <- Fixity -> FixityLevel
fixityLevel Fixity
f1
                                    , Related PrecedenceLevel
f2 <- Fixity -> FixityLevel
fixityLevel Fixity
f2
                                    , PrecedenceLevel
f1 forall a. Ord a => a -> a -> Bool
> PrecedenceLevel
f2 = Bool
false
    brack Fixity
f1   (RightOperandCtx Fixity
f2 ParenPreference
_) | Related PrecedenceLevel
f1 <- Fixity -> FixityLevel
fixityLevel Fixity
f1
                                    , Related PrecedenceLevel
f2 <- Fixity -> FixityLevel
fixityLevel Fixity
f2
                                    , PrecedenceLevel
f1 forall a. Ord a => a -> a -> Bool
> PrecedenceLevel
f2 = Bool
false
    brack Fixity
_ Precedence
TopCtx                 = Bool
false
    brack Fixity
_ Precedence
FunctionSpaceDomainCtx = Bool
false
    brack Fixity
_ Precedence
InsideOperandCtx       = Bool
false
    brack Fixity
_ Precedence
WithArgCtx             = Bool
false
    brack Fixity
_ Precedence
WithFunCtx             = Bool
false
    brack Fixity
_ Precedence
_                      = Bool
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 :: [Precedence] -> Bool
lamBrackets []       = Bool
False
lamBrackets (Precedence
p : [Precedence]
ps) = case Precedence
p of
  Precedence
TopCtx                 -> forall a. HasCallStack => a
__IMPOSSIBLE__
  ArgumentCtx ParenPreference
pref       -> ParenPreference -> Bool
preferParen ParenPreference
pref Bool -> Bool -> Bool
|| [Precedence] -> Bool
lamBrackets [Precedence]
ps
  RightOperandCtx Fixity
_ ParenPreference
pref -> ParenPreference -> Bool
preferParen ParenPreference
pref Bool -> Bool -> Bool
|| [Precedence] -> Bool
lamBrackets [Precedence]
ps
  Precedence
FunctionSpaceDomainCtx -> Bool
True
  LeftOperandCtx{}       -> Bool
True
  Precedence
FunctionCtx            -> Bool
True
  Precedence
InsideOperandCtx       -> Bool
True
  Precedence
WithFunCtx             -> Bool
True
  Precedence
WithArgCtx             -> Bool
True
  Precedence
DotPatternCtx          -> Bool
True

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

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

-- | Does a with application need brackets?
withAppBrackets :: PrecedenceStack -> Bool
withAppBrackets :: [Precedence] -> Bool
withAppBrackets = Precedence -> Bool
brack forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Precedence] -> Precedence
headPrecedence
  where
    brack :: Precedence -> Bool
brack Precedence
TopCtx                 = Bool
False
    brack Precedence
FunctionSpaceDomainCtx = Bool
False
    brack Precedence
WithFunCtx             = Bool
False
    brack Precedence
_                      = Bool
True

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

roundFixBrackets :: PrecedenceStack -> Bool
roundFixBrackets :: [Precedence] -> Bool
roundFixBrackets [Precedence]
ps = Precedence
DotPatternCtx forall a. Eq a => a -> a -> Bool
== [Precedence] -> Precedence
headPrecedence [Precedence]
ps

instance KillRange x => KillRange (ThingWithFixity x) where
  killRange :: KillRangeT (ThingWithFixity x)
killRange (ThingWithFixity x
c Fixity'
f) = forall x. x -> Fixity' -> ThingWithFixity x
ThingWithFixity (forall a. KillRange a => KillRangeT a
killRange x
c) Fixity'
f