{-# LANGUAGE DeriveDataTypeable #-}
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
data ThingWithFixity x = ThingWithFixity x Fixity'
deriving (Functor, Foldable, Traversable, Data, Show)
instance LensFixity' (ThingWithFixity a) where
lensFixity' f (ThingWithFixity a fix') = ThingWithFixity a <$> f fix'
instance LensFixity (ThingWithFixity a) where
lensFixity = lensFixity' . lensFixity
data ParenPreference = PreferParen | PreferParenless
deriving (Eq, Ord, Show, Data)
preferParen :: ParenPreference -> Bool
preferParen p = PreferParen == p
preferParenless :: ParenPreference -> Bool
preferParenless p = PreferParenless == p
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
type PrecedenceStack = [Precedence]
pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
pushPrecedence TopCtx _ = []
pushPrecedence p ps = p : ps
headPrecedence :: PrecedenceStack -> Precedence
headPrecedence [] = TopCtx
headPrecedence (p : _) = p
argumentCtx_ :: Precedence
argumentCtx_ = ArgumentCtx PreferParen
opBrackets :: Fixity -> PrecedenceStack -> Bool
opBrackets = opBrackets' False
opBrackets' :: Bool ->
Fixity -> PrecedenceStack -> Bool
opBrackets' isLam f ps = brack f (headPrecedence ps)
where
false = isLam && lamBrackets ps
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
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
appBrackets :: PrecedenceStack -> Bool
appBrackets = appBrackets' False
appBrackets' :: Bool ->
PrecedenceStack -> Bool
appBrackets' isLam ps = brack (headPrecedence ps)
where
brack ArgumentCtx{} = True
brack DotPatternCtx = True
brack _ = isLam && lamBrackets ps
withAppBrackets :: PrecedenceStack -> Bool
withAppBrackets = brack . headPrecedence
where
brack TopCtx = False
brack FunctionSpaceDomainCtx = False
brack WithFunCtx = False
brack _ = True
piBrackets :: PrecedenceStack -> Bool
piBrackets [] = False
piBrackets _ = True
roundFixBrackets :: PrecedenceStack -> Bool
roundFixBrackets ps = DotPatternCtx == headPrecedence ps
instance KillRange x => KillRange (ThingWithFixity x) where
killRange (ThingWithFixity c f) = ThingWithFixity (killRange c) f