module Agda.Syntax.Fixity where
import Prelude hiding (concatMap)
import Control.DeepSeq
import Data.Foldable
import Data.Function
import qualified Data.List as List
import Data.Maybe
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.Lens
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
, notaIsOperator :: Bool
} 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
, notaIsOperator = null syn
}
where Fixity' f syn = A.nameFixity n
useDefaultFixity :: NewNotation -> NewNotation
useDefaultFixity n
| notaFixity n == noFixity = n { notaFixity = defaultFixity }
| otherwise = 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
noFixity' :: Fixity'
noFixity' = Fixity' noFixity noNotation
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations =
map merge .
concatMap groupIfLevelsMatch .
groupOn (\n -> ( notation n
, notaIsOperator n
))
where
groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch [] = __IMPOSSIBLE__
groupIfLevelsMatch ns@(n : _) =
if allEqual (map fixityLevel related)
then [sameAssoc (sameLevel ns)]
else map (: []) ns
where
related = mapMaybe (\f -> case fixityLevel f of
Unrelated -> Nothing
Related {} -> Just f)
(map notaFixity ns)
sameLevel = map (set (_notaFixity . _fixityLevel) level)
where
level = case related of
f : _ -> fixityLevel f
[] -> Unrelated
sameAssoc = map (set (_notaFixity . _fixityAssoc) assoc)
where
assoc = case related of
f : _ | allEqual (map fixityAssoc related) -> fixityAssoc f
_ -> NonAssoc
merge :: [NewNotation] -> NewNotation
merge [] = __IMPOSSIBLE__
merge ns@(n : _) = n { notaNames = Set.unions $ map notaNames ns }
data NotationSection = NotationSection
{ sectNotation :: NewNotation
, sectKind :: NotationKind
, sectLevel :: Maybe PrecedenceLevel
, sectIsSection :: Bool
}
deriving Show
noSection :: NewNotation -> NotationSection
noSection n = NotationSection
{ sectNotation = n
, sectKind = notationKind (notation n)
, sectLevel = Just (fixityLevel (notaFixity n))
, sectIsSection = False
}
data PrecedenceLevel = Unrelated | Related !Integer
deriving (Eq, Ord, Show, Typeable)
data Associativity = NonAssoc | LeftAssoc | RightAssoc
deriving (Eq, Ord, Show, Typeable)
data Fixity =
Fixity { fixityRange :: Range
, fixityLevel :: !PrecedenceLevel
, 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))
noFixity :: Fixity
noFixity = Fixity noRange Unrelated NonAssoc
defaultFixity :: Fixity
defaultFixity = Fixity noRange (Related 20) NonAssoc
data Precedence = TopCtx | FunctionSpaceDomainCtx
| LeftOperandCtx Fixity | RightOperandCtx Fixity
| FunctionCtx | ArgumentCtx | InsideOperandCtx
| WithFunCtx | WithArgCtx | DotPatternCtx
deriving (Show, Typeable, Eq)
hiddenArgumentCtx :: Hiding -> Precedence
hiddenArgumentCtx NotHidden = ArgumentCtx
hiddenArgumentCtx Hidden = TopCtx
hiddenArgumentCtx Instance = TopCtx
opBrackets :: Fixity -> Precedence -> Bool
opBrackets (Fixity _ (Related n1) LeftAssoc)
(LeftOperandCtx (Fixity _ (Related n2) LeftAssoc)) | n1 >= n2 = False
opBrackets (Fixity _ (Related n1) RightAssoc)
(RightOperandCtx (Fixity _ (Related n2) RightAssoc)) | n1 >= n2 = False
opBrackets f1
(LeftOperandCtx f2) | Related f1 <- fixityLevel f1
, Related f2 <- fixityLevel f2
, f1 > f2 = False
opBrackets f1
(RightOperandCtx f2) | Related f1 <- fixityLevel f1
, Related f2 <- fixityLevel f2
, f1 > 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
_notaFixity :: Lens' Fixity NewNotation
_notaFixity f r = f (notaFixity r) <&> \x -> r { notaFixity = x }
_fixityAssoc :: Lens' Associativity Fixity
_fixityAssoc f r = f (fixityAssoc r) <&> \x -> r { fixityAssoc = x }
_fixityLevel :: Lens' PrecedenceLevel Fixity
_fixityLevel f r = f (fixityLevel r) <&> \x -> r { fixityLevel = x }
instance NFData Fixity' where
rnf (Fixity' _ a) = rnf a
instance NFData Fixity where
rnf (Fixity _ _ _) = ()