{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Syntax.Fixity where
import Prelude hiding (null)
import Control.DeepSeq
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Data (Data)
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
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data Fixity' = Fixity'
{ theFixity :: !Fixity
, theNotation :: Notation
, theNameRange :: Range
}
deriving (Data, Show)
instance Eq Fixity' where
Fixity' f n _ == Fixity' f' n' _ = f == f' && n == n'
instance Null Fixity' where
null (Fixity' f n _) = null f && null n
empty = noFixity'
noFixity' :: Fixity'
noFixity' = Fixity' noFixity noNotation noRange
data ThingWithFixity x = ThingWithFixity x Fixity'
deriving (Functor, Foldable, Traversable, Data, Show)
data NewNotation = NewNotation
{ notaName :: QName
, notaNames :: Set A.Name
, notaFixity :: Fixity
, notation :: Notation
, notaIsOperator :: Bool
} deriving Show
class LensFixity' a where
lensFixity' :: Lens' Fixity' a
instance LensFixity' Fixity' where
lensFixity' = id
instance LensFixity' (ThingWithFixity a) where
lensFixity' f (ThingWithFixity a fix') = ThingWithFixity a <$> f fix'
instance LensFixity Fixity' where
lensFixity f fix' = f (theFixity fix') <&> \ fx -> fix' { theFixity = fx }
instance LensFixity NewNotation where
lensFixity f nota = f (notaFixity nota) <&> \ fx -> nota { notaFixity = fx }
instance LensFixity (ThingWithFixity a) where
lensFixity = lensFixity' . lensFixity
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 InScope [Id $ rangedThing 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 noRange (defaultNamedArg $ unranged n) : mkSyn (1 + n) xs
mkSyn n (Id x : xs) = IdPart (unranged x) : mkSyn n xs
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 FixityLevel
, sectIsSection :: Bool
}
deriving Show
noSection :: NewNotation -> NotationSection
noSection n = NotationSection
{ sectNotation = n
, sectKind = notationKind (notation n)
, sectLevel = Just (fixityLevel (notaFixity n))
, sectIsSection = False
}
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 NFData Fixity' where
rnf (Fixity' _ a _) = rnf a
instance KillRange Fixity' where
killRange (Fixity' f n r) = killRange3 Fixity' f n r
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 }