{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Syntax.Notation where
import Prelude hiding (null)
import Control.DeepSeq
import Control.Monad
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Data (Data)
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Functor ((<&>))
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Impossible
data HoleName
= LambdaHole { _bindHoleName :: RString
, holeName :: RString }
| ExprHole { holeName :: RString }
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False
stringParts :: Notation -> [String]
stringParts gs = [ rangedThing x | IdPart x <- gs ]
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole _ n) = Just $ rangedThing n
holeTarget (WildHole n) = Just $ rangedThing n
holeTarget (NormalHole _ n) = Just $ rangedThing $ namedArg n
holeTarget IdPart{} = Nothing
isAHole :: GenPart -> Bool
isAHole BindHole{} = True
isAHole NormalHole{} = True
isAHole WildHole{} = False
isAHole IdPart{} = False
isNormalHole :: GenPart -> Bool
isNormalHole NormalHole{} = True
isNormalHole BindHole{} = False
isNormalHole WildHole{} = False
isNormalHole IdPart{} = False
isBindingHole :: GenPart -> Bool
isBindingHole BindHole{} = True
isBindingHole WildHole{} = True
isBindingHole _ = False
data NotationKind
= InfixNotation
| PrefixNotation
| PostfixNotation
| NonfixNotation
| NoNotation
deriving (Eq, Show)
notationKind :: Notation -> NotationKind
notationKind [] = NoNotation
notationKind syn =
case (isNormalHole $ head syn, isNormalHole $ last syn) of
(True , True ) -> InfixNotation
(True , False) -> PostfixNotation
(False, True ) -> PrefixNotation
(False, False) -> NonfixNotation
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation _ [] = throwError "empty notation is disallowed"
mkNotation holes ids = do
unless uniqueHoleNames $ throwError "syntax must use unique argument names"
let xs :: Notation = map mkPart ids
unless (isAlternating xs) $ throwError $ concat
[ "syntax must alternate holes ("
, prettyHoles
, ") and non-holes ("
, prettyNonHoles xs
, ")"
]
unless (isExprLinear xs) $ throwError "syntax must use holes exactly once"
unless (isLambdaLinear xs) $ throwError "syntax must use binding holes exactly once"
when (isSingleHole xs) $ throwError "syntax cannot be a single hole"
return $ insertWildHoles xs
where
holeNames :: [RString]
holeNames = map namedArg holes >>= \case
LambdaHole x y -> [x, y]
ExprHole y -> [y]
prettyHoles :: String
prettyHoles = List.unwords $ map (rawNameToString . rangedThing) holeNames
nonHoleNames :: Notation -> [RString]
nonHoleNames xs = flip mapMaybe xs $ \case
WildHole{} -> Just $ unranged "_"
IdPart x -> Just x
BindHole{} -> Nothing
NormalHole{} -> Nothing
prettyNonHoles :: Notation -> String
prettyNonHoles = List.unwords . map (rawNameToString . rangedThing) . nonHoleNames
mkPart ident = maybe (IdPart ident) (`withRangeOf` ident) $ lookup ident holeMap
holeNumbers = [0 .. length holes - 1]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles = zip holeNumbers holes
insertWildHoles :: [GenPart] -> [GenPart]
insertWildHoles xs = foldr ins xs wilds
where
wilds = [ i | (_, WildHole i) <- holeMap ]
ins w (NormalHole r h : hs)
| namedArg h == w = NormalHole r h : WildHole w : hs
ins w (h : hs) = h : insBefore w hs
ins _ [] = __IMPOSSIBLE__
insBefore w (NormalHole r h : hs)
| namedArg h == w = WildHole w : NormalHole r h : hs
insBefore w (h : hs) = h : insBefore w hs
insBefore _ [] = __IMPOSSIBLE__
holeMap :: [(RString, GenPart)]
holeMap = do
(i, h) <- numberedHoles
let ri x = Ranged (getRange x) i
normalHole y = NormalHole noRange $ fmap (ri y <$) h
case namedArg h of
ExprHole y -> [(y, normalHole y)]
LambdaHole x y
| "_" <- rangedThing x -> [(x, WildHole (ri x)), (y, normalHole y)]
| otherwise -> [(x, BindHole noRange (ri x)), (y, normalHole y)]
uniqueHoleNames = distinct [ x | (x, _) <- holeMap, rangedThing x /= "_" ]
isExprLinear xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers
isLambdaLinear xs = List.sort [ rangedThing x | BindHole _ x <- xs ] ==
[ i | (i, h) <- numberedHoles,
LambdaHole x _ <- [namedArg h], rangedThing x /= "_" ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
isSingleHole :: [GenPart] -> Bool
isSingleHole = \case
[ IdPart{} ] -> False
[ _hole ] -> True
_ -> False
data NewNotation = NewNotation
{ notaName :: QName
, notaNames :: Set A.Name
, notaFixity :: Fixity
, notation :: Notation
, notaIsOperator :: Bool
} deriving Show
instance LensFixity NewNotation where
lensFixity f nota = f (notaFixity nota) <&> \ fx -> nota { notaFixity = fx }
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)
. 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 }
_notaFixity :: Lens' Fixity NewNotation
_notaFixity f r = f (notaFixity r) <&> \x -> r { notaFixity = x }
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
}