module Agda.Syntax.Fixity where
import Data.Generics (Typeable, Data)
import Data.Foldable
import Data.Traversable
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Notation
data Fixity' = Fixity'
{theFixity :: Fixity,
theNotation :: Notation}
deriving (Typeable, Data, Show, Eq)
data ThingWithFixity x = ThingWithFixity x Fixity' deriving (Functor,Foldable,Traversable,Typeable,Data,Show)
type NewNotation = (Name, Fixity, Notation)
oldToNewNotation :: (Name, Fixity') -> NewNotation
oldToNewNotation (name, Fixity' f []) = (name, f, syntaxOf name)
oldToNewNotation (name, Fixity' f syn) = (name, f, syn)
syntaxOf :: Name -> Notation
syntaxOf (NoName _ _) = []
syntaxOf (Name _ [_]) = []
syntaxOf (Name _ xs) = mkSyn 0 xs
where mkSyn :: Int -> [NamePart] -> Notation
mkSyn n [] = []
mkSyn n (Hole:xs) = NormalHole n : mkSyn (1+n) xs
mkSyn n (Id x:xs) = IdPart x : mkSyn n xs
defaultFixity' = Fixity' defaultFixity defaultNotation
noFixity = NonAssoc noRange (negate 666)
data Fixity = LeftAssoc Range Nat
| RightAssoc Range Nat
| NonAssoc Range Nat
deriving (Typeable, Data, Show)
instance Eq Fixity where
LeftAssoc _ n == LeftAssoc _ m = n == m
RightAssoc _ n == RightAssoc _ m = n == m
NonAssoc _ n == NonAssoc _ m = n == m
_ == _ = False
fixityLevel :: Fixity -> Nat
fixityLevel (LeftAssoc _ n) = n
fixityLevel (RightAssoc _ n) = n
fixityLevel (NonAssoc _ n) = n
defaultFixity :: Fixity
defaultFixity = NonAssoc noRange 20
data Precedence = TopCtx | FunctionSpaceDomainCtx
| LeftOperandCtx Fixity | RightOperandCtx Fixity
| FunctionCtx | ArgumentCtx | InsideOperandCtx
| WithFunCtx | WithArgCtx | DotPatternCtx
deriving (Show,Typeable,Data)
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 (LeftAssoc r _) = r
getRange (RightAssoc r _) = r
getRange (NonAssoc r _) = r