1 2 3{-| As a concrete name, a notation is a non-empty list of alternating 'IdPart's and holes. 4 In contrast to concrete names, holes can be binders. 5 6 Example: 7 @ 8 syntax fmap (λ x → e) xs = for x ∈ xs return e 9 @ 10 11 The declared notation for @fmap@ is @for_∈_return_@ where the first hole is a binder. 12-} 13 14module Agda.Syntax.Notation where 15 16import Prelude hiding (null) 17 18import Control.DeepSeq 19import Control.Monad 20import Control.Monad.Except 21 22import qualified Data.List as List 23import Data.Maybe 24import Data.Set (Set) 25import qualified Data.Set as Set 26 27import GHC.Generics (Generic) 28 29import qualified Agda.Syntax.Abstract.Name as A 30import Agda.Syntax.Common 31import Agda.Syntax.Concrete.Name 32import Agda.Syntax.Concrete.Pretty() 33import Agda.Syntax.Position 34 35import Agda.Utils.Lens 36import Agda.Utils.List 37import qualified Agda.Utils.List1 as List1 38import Agda.Utils.Null 39import Agda.Utils.Pretty 40 41import Agda.Utils.Impossible 42 43-- | Data type constructed in the Happy parser; converted to 'GenPart' 44-- before it leaves the Happy code. 45data HoleName 46 = LambdaHole { _bindHoleName :: RString 47 , holeName :: RString } 48 -- ^ @\ x -> y@; 1st argument is the bound name (unused for now). 49 | ExprHole { holeName :: RString } 50 -- ^ Simple named hole with hiding. 51 52-- | Is the hole a binder? 53isLambdaHole :: HoleName -> Bool 54isLambdaHole (LambdaHole _ _) = True 55isLambdaHole _ = False 56 57-- | Get a flat list of identifier parts of a notation. 58stringParts :: Notation -> [String] 59stringParts gs = [ rangedThing x | IdPart x <- gs ] 60 61-- | Target argument position of a part (Nothing if it is not a hole). 62holeTarget :: GenPart -> Maybe Int 63holeTarget (BindHole _ n) = Just $ rangedThing n 64holeTarget (WildHole n) = Just $ rangedThing n 65holeTarget (NormalHole _ n) = Just $ rangedThing $ namedArg n 66holeTarget IdPart{} = Nothing 67 68-- | Is the part a hole? WildHoles don't count since they don't correspond to 69-- anything the user writes. 70isAHole :: GenPart -> Bool 71isAHole BindHole{} = True 72isAHole NormalHole{} = True 73isAHole WildHole{} = False 74isAHole IdPart{} = False 75 76-- | Is the part a normal hole? 77isNormalHole :: GenPart -> Bool 78isNormalHole NormalHole{} = True 79isNormalHole BindHole{} = False 80isNormalHole WildHole{} = False 81isNormalHole IdPart{} = False 82 83-- | Is the part a binder? 84isBindingHole :: GenPart -> Bool 85isBindingHole BindHole{} = True 86isBindingHole WildHole{} = True 87isBindingHole _ = False 88 89-- | Classification of notations. 90 91data NotationKind 92 = InfixNotation -- ^ Ex: @_bla_blub_@. 93 | PrefixNotation -- ^ Ex: @_bla_blub@. 94 | PostfixNotation -- ^ Ex: @bla_blub_@. 95 | NonfixNotation -- ^ Ex: @bla_blub@. 96 | NoNotation 97 deriving (Eq, Show, Generic) 98 99-- | Classify a notation by presence of leading and/or trailing 100-- /normal/ holes. 101notationKind :: Notation -> NotationKind 102notationKind [] = NoNotation 103notationKind (h:syn) = 104 case (isNormalHole h, isNormalHole $ last1 h syn) of 105 (True , True ) -> InfixNotation 106 (True , False) -> PostfixNotation 107 (False, True ) -> PrefixNotation 108 (False, False) -> NonfixNotation 109 110-- | From notation with names to notation with indices. 111-- 112-- Example: 113-- @ 114-- ids = ["for", "x", "∈", "xs", "return", "e"] 115-- holes = [ LambdaHole "x" "e", ExprHole "xs" ] 116-- @ 117-- creates the notation 118-- @ 119-- [ IdPart "for" , BindHole 0 120-- , IdPart "∈" , NormalHole 1 121-- , IdPart "return" , NormalHole 0 122-- ] 123-- @ 124mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation 125mkNotation _ [] = throwError "empty notation is disallowed" 126mkNotation holes ids = do 127 unless uniqueHoleNames $ throwError "syntax must use unique argument names" 128 let xs :: Notation = map mkPart ids 129 unless (noAdjacentHoles xs) $ throwError $ concat 130 [ "syntax must not contain adjacent holes (" 131 , prettyHoles 132 , ")" 133 ] 134 unless (isExprLinear xs) $ throwError "syntax must use holes exactly once" 135 unless (isLambdaLinear xs) $ throwError "syntax must use binding holes exactly once" 136 -- Andreas, 2018-10-18, issue #3285: 137 -- syntax that is just a single hole is ill-formed and crashes the operator parser 138 when (isSingleHole xs) $ throwError "syntax cannot be a single hole" 139 return $ insertWildHoles xs 140 where 141 holeNames :: [RString] 142 holeNames = map namedArg holes >>= \case 143 LambdaHole x y -> [x, y] 144 ExprHole y -> [y] 145 146 prettyHoles :: String 147 prettyHoles = List.unwords $ map (rawNameToString . rangedThing) holeNames 148 149 mkPart ident = maybe (IdPart ident) (`withRangeOf` ident) $ lookup ident holeMap 150 151 holeNumbers = [0 .. length holes - 1] 152 153 numberedHoles :: [(Int, NamedArg HoleName)] 154 numberedHoles = zip holeNumbers holes 155 156 -- The WildHoles don't correspond to anything in the right-hand side so 157 -- we add them next to their corresponding body. Slightly subtle: due to 158 -- the way the operator parsing works they can't be added first or last. 159 insertWildHoles :: [GenPart] -> [GenPart] 160 insertWildHoles xs = foldr ins xs wilds 161 where 162 wilds = [ i | (_, WildHole i) <- holeMap ] 163 ins w (NormalHole r h : hs) 164 | namedArg h == w = NormalHole r h : WildHole w : hs 165 ins w (h : hs) = h : insBefore w hs 166 ins _ [] = __IMPOSSIBLE__ 167 168 insBefore w (NormalHole r h : hs) 169 | namedArg h == w = WildHole w : NormalHole r h : hs 170 insBefore w (h : hs) = h : insBefore w hs 171 insBefore _ [] = __IMPOSSIBLE__ 172 173 -- Create a map (association list) from hole names to holes. 174 -- A @LambdaHole@ contributes two entries: 175 -- both names are mapped to the same number, 176 -- but distinguished by BindHole vs. NormalHole. 177 holeMap :: [(RString, GenPart)] 178 holeMap = do 179 (i, h) <- numberedHoles -- v This range is filled in by mkPart 180 let ri x = Ranged (getRange x) i 181 normalHole y = NormalHole noRange $ fmap (ri y <$) h 182 case namedArg h of 183 ExprHole y -> [(y, normalHole y)] 184 LambdaHole x y 185 | "_" <- rangedThing x -> [(x, WildHole (ri x)), (y, normalHole y)] 186 | otherwise -> [(x, BindHole noRange (ri x)), (y, normalHole y)] 187 -- Filled in by mkPart 188 189 -- Check whether all hole names are distinct. 190 -- The hole names are the keys of the @holeMap@. 191 uniqueHoleNames = distinct [ x | (x, _) <- holeMap, rangedThing x /= "_" ] 192 193 isExprLinear xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers 194 isLambdaLinear xs = List.sort [ rangedThing x | BindHole _ x <- xs ] == 195 [ i | (i, h) <- numberedHoles, 196 LambdaHole x _ <- [namedArg h], rangedThing x /= "_" ] 197 198 noAdjacentHoles :: [GenPart] -> Bool 199 noAdjacentHoles [] = __IMPOSSIBLE__ 200 noAdjacentHoles [x] = True 201 noAdjacentHoles (x:y:xs) = 202 not (isAHole x && isAHole y) && noAdjacentHoles (y:xs) 203 204 isSingleHole :: [GenPart] -> Bool 205 isSingleHole = \case 206 [ IdPart{} ] -> False 207 [ _hole ] -> True 208 _ -> False 209 210-- | All the notation information related to a name. 211data NewNotation = NewNotation 212 { notaName :: QName 213 , notaNames :: Set A.Name 214 -- ^ The names the syntax and/or fixity belong to. 215 -- 216 -- Invariant: The set is non-empty. Every name in the list matches 217 -- 'notaName'. 218 , notaFixity :: Fixity 219 -- ^ Associativity and precedence (fixity) of the names. 220 , notation :: Notation 221 -- ^ Syntax associated with the names. 222 , notaIsOperator :: Bool 223 -- ^ True if the notation comes from an operator (rather than a 224 -- syntax declaration). 225 } deriving (Show, Generic) 226 227instance LensFixity NewNotation where 228 lensFixity f nota = f (notaFixity nota) <&> \ fx -> nota { notaFixity = fx } 229 230-- | If an operator has no specific notation, then it is computed from 231-- its name. 232namesToNotation :: QName -> A.Name -> NewNotation 233namesToNotation q n = NewNotation 234 { notaName = q 235 , notaNames = Set.singleton n 236 , notaFixity = f 237 , notation = if null syn then syntaxOf (unqualify q) else syn 238 , notaIsOperator = null syn 239 } 240 where Fixity' f syn _ = A.nameFixity n 241 242-- | Replace 'noFixity' by 'defaultFixity'. 243useDefaultFixity :: NewNotation -> NewNotation 244useDefaultFixity n 245 | notaFixity n == noFixity = n { notaFixity = defaultFixity } 246 | otherwise = n 247 248-- | Return the 'IdPart's of a notation, the first part qualified, 249-- the other parts unqualified. 250-- This allows for qualified use of operators, e.g., 251-- @M.for x ∈ xs return e@, or @x ℕ.+ y@. 252notationNames :: NewNotation -> [QName] 253notationNames (NewNotation q _ _ parts _) = 254 zipWith ($) (reQualify : repeat QName) [simpleName $ rangedThing x | IdPart x <- parts ] 255 where 256 -- The qualification of @q@. 257 modules = List1.init (qnameParts q) 258 -- Putting the qualification onto @x@. 259 reQualify x = List.foldr Qual (QName x) modules 260 261-- | Create a 'Notation' (without binders) from a concrete 'Name'. 262-- Does the obvious thing: 263-- 'Hole's become 'NormalHole's, 'Id's become 'IdParts'. 264-- If 'Name' has no 'Hole's, it returns 'noNotation'. 265syntaxOf :: Name -> Notation 266syntaxOf y 267 | isOperator y = mkSyn 0 $ List1.toList $ nameNameParts y 268 | otherwise = noNotation 269 where 270 -- Turn a concrete name into a Notation, 271 -- numbering the holes from left to right. 272 -- Result will have no 'BindingHole's. 273 mkSyn :: Int -> [NamePart] -> Notation 274 mkSyn n [] = [] 275 mkSyn n (Hole : xs) = NormalHole noRange (defaultNamedArg $ unranged n) : mkSyn (1 + n) xs 276 mkSyn n (Id x : xs) = IdPart (unranged x) : mkSyn n xs 277 278-- | Merges 'NewNotation's that have the same precedence level and 279-- notation, with two exceptions: 280-- 281-- * Operators and notations coming from syntax declarations are kept 282-- separate. 283-- 284-- * If /all/ instances of a given 'NewNotation' have the same 285-- precedence level or are \"unrelated\", then they are merged. They 286-- get the given precedence level, if any, and otherwise they become 287-- unrelated (but related to each other). 288-- 289-- If 'NewNotation's that are merged have distinct associativities, 290-- then they get 'NonAssoc' as their associativity. 291-- 292-- Precondition: No 'A.Name' may occur in more than one list element. 293-- Every 'NewNotation' must have the same 'notaName'. 294-- 295-- Postcondition: No 'A.Name' occurs in more than one list element. 296mergeNotations :: [NewNotation] -> [NewNotation] 297mergeNotations = 298 map merge . 299 concatMap groupIfLevelsMatch . 300 groupOn (\n -> ( notation n 301 , notaIsOperator n 302 )) 303 where 304 groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]] 305 groupIfLevelsMatch [] = __IMPOSSIBLE__ 306 groupIfLevelsMatch ns@(n : _) = 307 if allEqual (map fixityLevel related) 308 then [sameAssoc (sameLevel ns)] 309 else map (: []) ns 310 where 311 -- Fixities of operators whose precedence level is not Unrelated. 312 related = mapMaybe ((\f -> case fixityLevel f of 313 Unrelated -> Nothing 314 Related {} -> Just f) 315 . notaFixity) ns 316 317 -- Precondition: All related operators have the same precedence 318 -- level. 319 -- 320 -- Gives all unrelated operators the same level. 321 sameLevel = map (set (_notaFixity . _fixityLevel) level) 322 where 323 level = case related of 324 f : _ -> fixityLevel f 325 [] -> Unrelated 326 327 -- If all related operators have the same associativity, then the 328 -- unrelated operators get the same associativity, and otherwise 329 -- all operators get the associativity NonAssoc. 330 sameAssoc = map (set (_notaFixity . _fixityAssoc) assoc) 331 where 332 assoc = case related of 333 f : _ | allEqual (map fixityAssoc related) -> fixityAssoc f 334 _ -> NonAssoc 335 336 merge :: [NewNotation] -> NewNotation 337 merge [] = __IMPOSSIBLE__ 338 merge ns@(n : _) = n { notaNames = Set.unions $ map notaNames ns } 339 340-- | Lens for 'Fixity' in 'NewNotation'. 341 342_notaFixity :: Lens' Fixity NewNotation 343_notaFixity f r = f (notaFixity r) <&> \x -> r { notaFixity = x } 344 345-- * Sections 346 347-- | Sections, as well as non-sectioned operators. 348 349data NotationSection = NotationSection 350 { sectNotation :: NewNotation 351 , sectKind :: NotationKind 352 -- ^ For non-sectioned operators this should match the notation's 353 -- 'notationKind'. 354 , sectLevel :: Maybe FixityLevel 355 -- ^ Effective precedence level. 'Nothing' for closed notations. 356 , sectIsSection :: Bool 357 -- ^ 'False' for non-sectioned operators. 358 } 359 deriving (Show, Generic) 360 361-- | Converts a notation to a (non-)section. 362 363noSection :: NewNotation -> NotationSection 364noSection n = NotationSection 365 { sectNotation = n 366 , sectKind = notationKind (notation n) 367 , sectLevel = Just (fixityLevel (notaFixity n)) 368 , sectIsSection = False 369 } 370 371 372-- * Pretty printing 373 374instance Pretty NewNotation where 375 pretty (NewNotation x _xs fx nota isOp) = hsepWith "=" px pn 376 where 377 px = fsep [ if isOp then empty else "syntax" , pretty fx , pretty x ] 378 pn = if isOp then empty else pretty nota 379 380instance Pretty NotationKind where pretty = pshow 381 382instance Pretty NotationSection where 383 pretty (NotationSection nota kind mlevel isSection) 384 | isSection = fsep 385 [ "section" 386 , pretty kind 387 , maybe empty pretty mlevel 388 , pretty nota 389 ] 390 | otherwise = pretty nota 391 392-- NFData instances 393 394instance NFData NotationKind 395instance NFData NewNotation 396instance NFData NotationSection 397