module Agda.Syntax.Fixity where
import Data.Foldable
import Data.Function
import Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable
import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Common
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Notation
import Agda.Utils.List
#include "undefined.h"
import Agda.Utils.Impossible
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
, notaNames :: Set A.Name
, notaFixity :: Fixity
, notation :: Notation
} deriving (Typeable, Show)
namesToNotation :: QName -> A.Name -> NewNotation
namesToNotation q n = NewNotation
{ notaName = q
, notaNames = Set.singleton n
, notaFixity = f
, notation = if null syn then syntaxOf $ unqualify q else syn
}
where Fixity' f syn = A.nameFixity n
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
noFixity' :: Fixity'
noFixity' = Fixity' noFixity noNotation
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations = map (merge . fixFixities) . groupOn notation
where
fixFixities ns
| allEqual (map notaFixity ns) = ns
| otherwise =
map (\n -> n { notaFixity = defaultFixity }) ns
merge :: [NewNotation] -> NewNotation
merge [] = __IMPOSSIBLE__
merge ns@(n : _) = n { notaNames = Set.unions $ map notaNames ns }
data Associativity = NonAssoc | LeftAssoc | RightAssoc
deriving (Eq, Ord, Show, Typeable)
data Fixity =
Fixity { fixityRange :: Range
, fixityLevel :: Integer
, fixityAssoc :: Associativity
}
deriving (Typeable, Show)
instance Eq Fixity where
f1 == f2 = compare f1 f2 == EQ
instance Ord Fixity where
compare = compare `on` (\f -> (fixityLevel f, fixityAssoc f))
defaultFixity :: Fixity
defaultFixity = Fixity noRange 20 NonAssoc
noFixity :: Fixity
noFixity = Fixity noRange (negate 666) NonAssoc
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 (Fixity _ n1 LeftAssoc)
(LeftOperandCtx (Fixity _ n2 LeftAssoc)) | n1 >= n2 = False
opBrackets (Fixity _ n1 RightAssoc)
(RightOperandCtx (Fixity _ n2 RightAssoc)) | 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 f = f { fixityRange = noRange }
instance KillRange Fixity' where
killRange (Fixity' f n) = killRange2 Fixity' f n
instance KillRange x => KillRange (ThingWithFixity x) where
killRange (ThingWithFixity c f) = ThingWithFixity (killRange c) f