module Agda.Syntax.Fixity where
import Data.Foldable
import Data.List as List
import Data.Traversable
import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Notation
import Agda.Utils.List
data Fixity' = Fixity'
{ theFixity :: Fixity
, theNotation :: Notation
}
deriving (Typeable, Show, Eq)
data ThingWithFixity x = ThingWithFixity x Fixity'
deriving (Functor, Foldable, Traversable, Typeable, Show)
data NewNotation = NewNotation
{ notaName :: QName
, notaFixity :: Fixity
, notation :: Notation
} deriving (Typeable, Show)
oldToNewNotation :: (QName, Fixity') -> NewNotation
oldToNewNotation (name, Fixity' f syn) = NewNotation
{ notaName = name
, notaFixity = f
, notation = if null syn then syntaxOf $ unqualify name else syn
}
notationNames :: NewNotation -> [QName]
notationNames (NewNotation q _ parts) =
zipWith ($) (reQualify : repeat QName) [Name noRange [Id x] | IdPart x <- parts ]
where
modules = init (qnameParts q)
reQualify x = List.foldr Qual (QName x) modules
syntaxOf :: Name -> Notation
syntaxOf (NoName _ _) = noNotation
syntaxOf (Name _ [_]) = noNotation
syntaxOf (Name _ xs) = mkSyn 0 xs
where
mkSyn :: Int -> [NamePart] -> Notation
mkSyn n [] = []
mkSyn n (Hole : xs) = NormalHole (defaultNamedArg n) : mkSyn (1 + n) xs
mkSyn n (Id x : xs) = IdPart x : mkSyn n xs
defaultFixity' :: Fixity'
defaultFixity' = Fixity' defaultFixity defaultNotation
interestingFixities :: [Fixity'] -> [Fixity']
interestingFixities fixs = if null fixs' then [defaultFixity'] else fixs'
where fixs' = filter (not . (== defaultFixity')) fixs
chooseFixity :: [Fixity'] -> Fixity'
chooseFixity fixs = if allEqual fixs' then head fixs' else defaultFixity'
where fixs' = interestingFixities fixs
data Fixity
= LeftAssoc { fixityRange :: Range, fixityLevel :: Integer }
| RightAssoc { fixityRange :: Range, fixityLevel :: Integer }
| NonAssoc { fixityRange :: Range, fixityLevel :: Integer }
deriving (Typeable, Show)
instance Eq Fixity where
LeftAssoc _ n == LeftAssoc _ m = n == m
RightAssoc _ n == RightAssoc _ m = n == m
NonAssoc _ n == NonAssoc _ m = n == m
_ == _ = False
defaultFixity :: Fixity
defaultFixity = NonAssoc noRange 20
noFixity :: Fixity
noFixity = NonAssoc noRange (negate 666)
data Precedence = TopCtx | FunctionSpaceDomainCtx
| LeftOperandCtx Fixity | RightOperandCtx Fixity
| FunctionCtx | ArgumentCtx | InsideOperandCtx
| WithFunCtx | WithArgCtx | DotPatternCtx
deriving (Show,Typeable)
hiddenArgumentCtx :: Hiding -> Precedence
hiddenArgumentCtx NotHidden = ArgumentCtx
hiddenArgumentCtx Hidden = TopCtx
hiddenArgumentCtx Instance = TopCtx
opBrackets :: Fixity -> Precedence -> Bool
opBrackets (LeftAssoc _ n1)
(LeftOperandCtx (LeftAssoc _ n2)) | n1 >= n2 = False
opBrackets (RightAssoc _ n1)
(RightOperandCtx (RightAssoc _ n2)) | n1 >= n2 = False
opBrackets f1
(LeftOperandCtx f2) | fixityLevel f1 > fixityLevel f2 = False
opBrackets f1
(RightOperandCtx f2) | fixityLevel f1 > fixityLevel f2 = False
opBrackets _ TopCtx = False
opBrackets _ FunctionSpaceDomainCtx = False
opBrackets _ InsideOperandCtx = False
opBrackets _ WithArgCtx = False
opBrackets _ WithFunCtx = False
opBrackets _ _ = True
lamBrackets :: Precedence -> Bool
lamBrackets TopCtx = False
lamBrackets _ = True
appBrackets :: Precedence -> Bool
appBrackets ArgumentCtx = True
appBrackets DotPatternCtx = True
appBrackets _ = False
withAppBrackets :: Precedence -> Bool
withAppBrackets TopCtx = False
withAppBrackets FunctionSpaceDomainCtx = False
withAppBrackets WithFunCtx = False
withAppBrackets _ = True
piBrackets :: Precedence -> Bool
piBrackets TopCtx = False
piBrackets _ = True
roundFixBrackets :: Precedence -> Bool
roundFixBrackets DotPatternCtx = True
roundFixBrackets _ = False
instance HasRange Fixity where
getRange = fixityRange
instance KillRange Fixity where
killRange (LeftAssoc _ n) = LeftAssoc noRange n
killRange (RightAssoc _ n) = RightAssoc noRange n
killRange (NonAssoc _ n) = NonAssoc noRange n
instance KillRange Fixity' where
killRange (Fixity' f n) = killRange1 (flip Fixity' n) f