{-# LANGUAGE DeriveDataTypeable #-}

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

import Control.DeepSeq

import qualified Data.List as List
import Data.Maybe

import Data.Data (Data)

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

import Agda.Utils.List
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 (a -> ThingWithFixity b -> ThingWithFixity a
(a -> b) -> ThingWithFixity a -> ThingWithFixity b
(forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b)
-> (forall a b. a -> ThingWithFixity b -> ThingWithFixity a)
-> Functor ThingWithFixity
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
<$ :: a -> ThingWithFixity b -> ThingWithFixity a
$c<$ :: forall a b. a -> ThingWithFixity b -> ThingWithFixity a
fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b
$cfmap :: forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
Functor, ThingWithFixity a -> Bool
(a -> m) -> ThingWithFixity a -> m
(a -> b -> b) -> b -> ThingWithFixity a -> b
(forall m. Monoid m => ThingWithFixity m -> m)
-> (forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m)
-> (forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m)
-> (forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b)
-> (forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b)
-> (forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b)
-> (forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b)
-> (forall a. (a -> a -> a) -> ThingWithFixity a -> a)
-> (forall a. (a -> a -> a) -> ThingWithFixity a -> a)
-> (forall a. ThingWithFixity a -> [a])
-> (forall a. ThingWithFixity a -> Bool)
-> (forall a. ThingWithFixity a -> Int)
-> (forall a. Eq a => a -> ThingWithFixity a -> Bool)
-> (forall a. Ord a => ThingWithFixity a -> a)
-> (forall a. Ord a => ThingWithFixity a -> a)
-> (forall a. Num a => ThingWithFixity a -> a)
-> (forall a. Num a => ThingWithFixity a -> a)
-> Foldable ThingWithFixity
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 :: ThingWithFixity a -> a
$cproduct :: forall a. Num a => ThingWithFixity a -> a
sum :: ThingWithFixity a -> a
$csum :: forall a. Num a => ThingWithFixity a -> a
minimum :: ThingWithFixity a -> a
$cminimum :: forall a. Ord a => ThingWithFixity a -> a
maximum :: ThingWithFixity a -> a
$cmaximum :: forall a. Ord a => ThingWithFixity a -> a
elem :: a -> ThingWithFixity a -> Bool
$celem :: forall a. Eq a => a -> ThingWithFixity a -> Bool
length :: ThingWithFixity a -> Int
$clength :: forall a. ThingWithFixity a -> Int
null :: ThingWithFixity a -> Bool
$cnull :: forall a. ThingWithFixity a -> Bool
toList :: ThingWithFixity a -> [a]
$ctoList :: forall a. ThingWithFixity a -> [a]
foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
foldMap' :: (a -> m) -> ThingWithFixity a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
foldMap :: (a -> m) -> ThingWithFixity a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
fold :: ThingWithFixity m -> m
$cfold :: forall m. Monoid m => ThingWithFixity m -> m
Foldable, Functor ThingWithFixity
Foldable ThingWithFixity
Functor ThingWithFixity
-> Foldable ThingWithFixity
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b))
-> (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 (m :: * -> *) a.
    Monad m =>
    ThingWithFixity (m a) -> m (ThingWithFixity a))
-> Traversable ThingWithFixity
(a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
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 :: ThingWithFixity (m a) -> m (ThingWithFixity a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
ThingWithFixity (m a) -> m (ThingWithFixity a)
mapM :: (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
sequenceA :: ThingWithFixity (f a) -> f (ThingWithFixity a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
ThingWithFixity (f a) -> f (ThingWithFixity a)
traverse :: (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
$cp2Traversable :: Foldable ThingWithFixity
$cp1Traversable :: Functor ThingWithFixity
Traversable, Typeable (ThingWithFixity x)
DataType
Constr
Typeable (ThingWithFixity x)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> ThingWithFixity x
    -> c (ThingWithFixity x))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x))
-> (ThingWithFixity x -> Constr)
-> (ThingWithFixity x -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (ThingWithFixity x)))
-> ((forall b. Data b => b -> b)
    -> ThingWithFixity x -> ThingWithFixity x)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ThingWithFixity x -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ThingWithFixity x -> m (ThingWithFixity x))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ThingWithFixity x -> m (ThingWithFixity x))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ThingWithFixity x -> m (ThingWithFixity x))
-> Data (ThingWithFixity x)
ThingWithFixity x -> DataType
ThingWithFixity x -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))
(forall b. Data b => b -> b)
-> ThingWithFixity x -> ThingWithFixity x
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ThingWithFixity x
-> c (ThingWithFixity x)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)
forall x. Data x => Typeable (ThingWithFixity x)
forall x. Data x => ThingWithFixity x -> DataType
forall x. Data x => ThingWithFixity x -> Constr
forall x.
Data x =>
(forall b. Data b => b -> b)
-> ThingWithFixity x -> ThingWithFixity x
forall x u.
Data x =>
Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u
forall x u.
Data x =>
(forall d. Data d => d -> u) -> ThingWithFixity x -> [u]
forall x r r'.
Data x =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
forall x r r'.
Data x =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
forall x (m :: * -> *).
(Data x, Monad m) =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
forall x (c :: * -> *).
Data x =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)
forall x (c :: * -> *).
Data x =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ThingWithFixity x
-> c (ThingWithFixity x)
forall x (t :: * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))
forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ThingWithFixity x))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u
forall u. (forall d. Data d => d -> u) -> ThingWithFixity x -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ThingWithFixity x
-> c (ThingWithFixity x)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ThingWithFixity x))
$cThingWithFixity :: Constr
$tThingWithFixity :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
$cgmapMo :: forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
gmapMp :: (forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
$cgmapMp :: forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
gmapM :: (forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
$cgmapM :: forall x (m :: * -> *).
(Data x, Monad m) =>
(forall d. Data d => d -> m d)
-> ThingWithFixity x -> m (ThingWithFixity x)
gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u
$cgmapQi :: forall x u.
Data x =>
Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u
gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u]
$cgmapQ :: forall x u.
Data x =>
(forall d. Data d => d -> u) -> ThingWithFixity x -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
$cgmapQr :: forall x r r'.
Data x =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
$cgmapQl :: forall x r r'.
Data x =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r
gmapT :: (forall b. Data b => b -> b)
-> ThingWithFixity x -> ThingWithFixity x
$cgmapT :: forall x.
Data x =>
(forall b. Data b => b -> b)
-> ThingWithFixity x -> ThingWithFixity x
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ThingWithFixity x))
$cdataCast2 :: forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ThingWithFixity x))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))
$cdataCast1 :: forall x (t :: * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))
dataTypeOf :: ThingWithFixity x -> DataType
$cdataTypeOf :: forall x. Data x => ThingWithFixity x -> DataType
toConstr :: ThingWithFixity x -> Constr
$ctoConstr :: forall x. Data x => ThingWithFixity x -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)
$cgunfold :: forall x (c :: * -> *).
Data x =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ThingWithFixity x
-> c (ThingWithFixity x)
$cgfoldl :: forall x (c :: * -> *).
Data x =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ThingWithFixity x
-> c (ThingWithFixity x)
$cp1Data :: forall x. Data x => Typeable (ThingWithFixity x)
Data, Int -> ThingWithFixity x -> ShowS
[ThingWithFixity x] -> ShowS
ThingWithFixity x -> String
(Int -> ThingWithFixity x -> ShowS)
-> (ThingWithFixity x -> String)
-> ([ThingWithFixity x] -> ShowS)
-> Show (ThingWithFixity x)
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' :: (Fixity' -> f Fixity')
-> ThingWithFixity a -> f (ThingWithFixity a)
lensFixity' Fixity' -> f Fixity'
f (ThingWithFixity a
a Fixity'
fix') = a -> Fixity' -> ThingWithFixity a
forall x. x -> Fixity' -> ThingWithFixity x
ThingWithFixity a
a (Fixity' -> ThingWithFixity a)
-> f Fixity' -> f (ThingWithFixity 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 :: (Fixity -> f Fixity) -> ThingWithFixity a -> f (ThingWithFixity a)
lensFixity = (Fixity' -> f Fixity')
-> ThingWithFixity a -> f (ThingWithFixity a)
forall a. LensFixity' a => Lens' Fixity' a
lensFixity' ((Fixity' -> f Fixity')
 -> ThingWithFixity a -> f (ThingWithFixity a))
-> ((Fixity -> f Fixity) -> Fixity' -> f Fixity')
-> (Fixity -> f Fixity)
-> ThingWithFixity a
-> f (ThingWithFixity a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Fixity -> f Fixity) -> Fixity' -> f Fixity'
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
(ParenPreference -> ParenPreference -> Bool)
-> (ParenPreference -> ParenPreference -> Bool)
-> Eq ParenPreference
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
Eq ParenPreference
-> (ParenPreference -> ParenPreference -> Ordering)
-> (ParenPreference -> ParenPreference -> Bool)
-> (ParenPreference -> ParenPreference -> Bool)
-> (ParenPreference -> ParenPreference -> Bool)
-> (ParenPreference -> ParenPreference -> Bool)
-> (ParenPreference -> ParenPreference -> ParenPreference)
-> (ParenPreference -> ParenPreference -> ParenPreference)
-> Ord 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
$cp1Ord :: Eq ParenPreference
Ord, Int -> ParenPreference -> ShowS
[ParenPreference] -> ShowS
ParenPreference -> String
(Int -> ParenPreference -> ShowS)
-> (ParenPreference -> String)
-> ([ParenPreference] -> ShowS)
-> Show ParenPreference
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, Typeable ParenPreference
DataType
Constr
Typeable ParenPreference
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ParenPreference -> c ParenPreference)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ParenPreference)
-> (ParenPreference -> Constr)
-> (ParenPreference -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ParenPreference))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ParenPreference))
-> ((forall b. Data b => b -> b)
    -> ParenPreference -> ParenPreference)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ParenPreference -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ParenPreference -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ParenPreference -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ParenPreference -> m ParenPreference)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ParenPreference -> m ParenPreference)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ParenPreference -> m ParenPreference)
-> Data ParenPreference
ParenPreference -> DataType
ParenPreference -> Constr
(forall b. Data b => b -> b) -> ParenPreference -> ParenPreference
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParenPreference -> c ParenPreference
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParenPreference
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ParenPreference -> u
forall u. (forall d. Data d => d -> u) -> ParenPreference -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParenPreference
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParenPreference -> c ParenPreference
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ParenPreference)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParenPreference)
$cPreferParenless :: Constr
$cPreferParen :: Constr
$tParenPreference :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
gmapMp :: (forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
gmapM :: (forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ParenPreference -> m ParenPreference
gmapQi :: Int -> (forall d. Data d => d -> u) -> ParenPreference -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ParenPreference -> u
gmapQ :: (forall d. Data d => d -> u) -> ParenPreference -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ParenPreference -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ParenPreference -> r
gmapT :: (forall b. Data b => b -> b) -> ParenPreference -> ParenPreference
$cgmapT :: (forall b. Data b => b -> b) -> ParenPreference -> ParenPreference
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParenPreference)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ParenPreference)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ParenPreference)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ParenPreference)
dataTypeOf :: ParenPreference -> DataType
$cdataTypeOf :: ParenPreference -> DataType
toConstr :: ParenPreference -> Constr
$ctoConstr :: ParenPreference -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParenPreference
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ParenPreference
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParenPreference -> c ParenPreference
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ParenPreference -> c ParenPreference
$cp1Data :: Typeable ParenPreference
Data)

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

preferParenless :: ParenPreference -> Bool
preferParenless :: ParenPreference -> Bool
preferParenless ParenPreference
p = ParenPreference
PreferParenless ParenPreference -> ParenPreference -> Bool
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
(Int -> Precedence -> ShowS)
-> (Precedence -> String)
-> ([Precedence] -> ShowS)
-> Show Precedence
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, Typeable Precedence
DataType
Constr
Typeable Precedence
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Precedence -> c Precedence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Precedence)
-> (Precedence -> Constr)
-> (Precedence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Precedence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Precedence))
-> ((forall b. Data b => b -> b) -> Precedence -> Precedence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Precedence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Precedence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Precedence -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Precedence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Precedence -> m Precedence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Precedence -> m Precedence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Precedence -> m Precedence)
-> Data Precedence
Precedence -> DataType
Precedence -> Constr
(forall b. Data b => b -> b) -> Precedence -> Precedence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Precedence -> c Precedence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Precedence
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Precedence -> u
forall u. (forall d. Data d => d -> u) -> Precedence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Precedence -> m Precedence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Precedence -> m Precedence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Precedence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Precedence -> c Precedence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Precedence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence)
$cDotPatternCtx :: Constr
$cWithArgCtx :: Constr
$cWithFunCtx :: Constr
$cInsideOperandCtx :: Constr
$cArgumentCtx :: Constr
$cFunctionCtx :: Constr
$cRightOperandCtx :: Constr
$cLeftOperandCtx :: Constr
$cFunctionSpaceDomainCtx :: Constr
$cTopCtx :: Constr
$tPrecedence :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Precedence -> m Precedence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Precedence -> m Precedence
gmapMp :: (forall d. Data d => d -> m d) -> Precedence -> m Precedence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Precedence -> m Precedence
gmapM :: (forall d. Data d => d -> m d) -> Precedence -> m Precedence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Precedence -> m Precedence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Precedence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Precedence -> u
gmapQ :: (forall d. Data d => d -> u) -> Precedence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Precedence -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Precedence -> r
gmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence
$cgmapT :: (forall b. Data b => b -> b) -> Precedence -> Precedence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Precedence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Precedence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Precedence)
dataTypeOf :: Precedence -> DataType
$cdataTypeOf :: Precedence -> DataType
toConstr :: Precedence -> Constr
$ctoConstr :: Precedence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Precedence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Precedence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Precedence -> c Precedence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Precedence -> c Precedence
$cp1Data :: Typeable Precedence
Data, Precedence -> Precedence -> Bool
(Precedence -> Precedence -> Bool)
-> (Precedence -> Precedence -> Bool) -> Eq Precedence
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)

instance Pretty Precedence where
  pretty :: Precedence -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Precedence -> String) -> Precedence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precedence -> String
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 Precedence -> [Precedence] -> [Precedence]
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 PrecedenceLevel -> PrecedenceLevel -> Bool
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 PrecedenceLevel -> PrecedenceLevel -> Bool
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 PrecedenceLevel -> PrecedenceLevel -> Bool
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 PrecedenceLevel -> PrecedenceLevel -> Bool
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                 -> Bool
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 (Precedence -> Bool)
-> ([Precedence] -> Precedence) -> [Precedence] -> Bool
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 Precedence -> Precedence -> Bool
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) = x -> Fixity' -> ThingWithFixity x
forall x. x -> Fixity' -> ThingWithFixity x
ThingWithFixity (KillRangeT x
forall a. KillRange a => KillRangeT a
killRange x
c) Fixity'
f