{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
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.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.Pretty
#include "undefined.h"
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'
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
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 noRange
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, Data)
data Associativity = NonAssoc | LeftAssoc | RightAssoc
deriving (Eq, Ord, Show, Data)
data Fixity = Fixity
{ fixityRange :: Range
, fixityLevel :: !PrecedenceLevel
, fixityAssoc :: !Associativity
}
deriving (Data, 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 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 HasRange Fixity where
getRange = fixityRange
instance KillRange Fixity where
killRange f = f { fixityRange = noRange }
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 }
_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 _ _ _) = ()