1{-# LANGUAGE GADTs #-} 2 3-- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's. 4-- 5-- * Attach fixity and syntax declarations to the definition they refer to. 6-- 7-- * Distribute the following attributes to the individual definitions: 8-- @abstract@, 9-- @instance@, 10-- @postulate@, 11-- @primitive@, 12-- @private@, 13-- termination pragmas. 14-- 15-- * Gather the function clauses belonging to one function definition. 16-- 17-- * Expand ellipsis @...@ in function clauses following @with@. 18-- 19-- * Infer mutual blocks. 20-- A block starts when a lone signature is encountered, and ends when 21-- all lone signatures have seen their definition. 22-- 23-- * Handle interleaved mutual blocks. 24-- In an `interleaved mutual' block we: 25-- * leave the data and fun sigs in place 26-- * classify signatures in `constructor' block based on their return type 27-- and group them all as a data def at the position in the block where the 28-- first constructor for the data sig in question occured 29-- * classify fun clauses based on the declared function used and group them 30-- all as a fundef at the position in the block where the first such fun 31-- clause appeared 32-- 33-- * Report basic well-formedness error, 34-- when one of the above transformation fails. 35-- When possible, errors should be deferred to the scope checking phase 36-- (ConcreteToAbstract), where we are in the TCM and can produce more 37-- informative error messages. 38 39 40module Agda.Syntax.Concrete.Definitions 41 ( NiceDeclaration(..) 42 , NiceConstructor, NiceTypeSignature 43 , Clause(..) 44 , DeclarationException(..) 45 , DeclarationWarning(..), DeclarationWarning'(..), unsafeDeclarationWarning 46 , Nice, runNice 47 , niceDeclarations 48 , notSoNiceDeclarations 49 , niceHasAbstract 50 , Measure 51 , declarationWarningName 52 ) where 53 54 55import Prelude hiding (null) 56 57import Control.Monad.Except 58import Control.Monad.State 59 60import Data.Bifunctor 61import Data.Data (Data) 62import Data.Either (isLeft, isRight) 63import Data.Function (on) 64import qualified Data.Map as Map 65import Data.Map (Map) 66import Data.Maybe 67import Data.Semigroup ( Semigroup(..) ) 68import qualified Data.List as List 69import qualified Data.Foldable as Fold 70import qualified Data.Traversable as Trav 71 72import Agda.Syntax.Concrete 73import Agda.Syntax.Concrete.Pattern 74import Agda.Syntax.Common hiding (TerminationCheck()) 75import qualified Agda.Syntax.Common as Common 76import Agda.Syntax.Position 77import Agda.Syntax.Notation 78import Agda.Syntax.Concrete.Pretty () --instance only 79import Agda.Syntax.Concrete.Fixity 80 81import Agda.Syntax.Concrete.Definitions.Errors 82import Agda.Syntax.Concrete.Definitions.Monad 83import Agda.Syntax.Concrete.Definitions.Types 84 85import Agda.Interaction.Options.Warnings 86 87import Agda.Utils.AffineHole 88import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack ) 89import Agda.Utils.Functor 90import Agda.Utils.Lens 91import Agda.Utils.List (isSublistOf, spanJust) 92import Agda.Utils.List1 (List1, pattern (:|)) 93import qualified Agda.Utils.List1 as List1 94import Agda.Utils.Maybe 95import Agda.Utils.Null 96import Agda.Utils.Pretty 97import Agda.Utils.Singleton 98import Agda.Utils.Three 99import Agda.Utils.Tuple 100import Agda.Utils.Update 101 102import Agda.Utils.Impossible 103 104{-------------------------------------------------------------------------- 105 The niceifier 106 --------------------------------------------------------------------------} 107 108-- | Check that declarations in a mutual block are consistently 109-- equipped with MEASURE pragmas, or whether there is a 110-- NO_TERMINATION_CHECK pragma. 111combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck 112combineTerminationChecks r tcs = loop tcs where 113 loop :: [TerminationCheck] -> Nice TerminationCheck 114 loop [] = return TerminationCheck 115 loop (tc : tcs) = do 116 let failure r = declarationException $ InvalidMeasureMutual r 117 tc' <- loop tcs 118 case (tc, tc') of 119 (TerminationCheck , tc' ) -> return tc' 120 (tc , TerminationCheck ) -> return tc 121 (NonTerminating , NonTerminating ) -> return NonTerminating 122 (NoTerminationCheck , NoTerminationCheck ) -> return NoTerminationCheck 123 (NoTerminationCheck , Terminating ) -> return Terminating 124 (Terminating , NoTerminationCheck ) -> return Terminating 125 (Terminating , Terminating ) -> return Terminating 126 (TerminationMeasure{} , TerminationMeasure{} ) -> return tc 127 (TerminationMeasure r _, NoTerminationCheck ) -> failure r 128 (TerminationMeasure r _, Terminating ) -> failure r 129 (NoTerminationCheck , TerminationMeasure r _) -> failure r 130 (Terminating , TerminationMeasure r _) -> failure r 131 (TerminationMeasure r _, NonTerminating ) -> failure r 132 (NonTerminating , TerminationMeasure r _) -> failure r 133 (NoTerminationCheck , NonTerminating ) -> failure r 134 (Terminating , NonTerminating ) -> failure r 135 (NonTerminating , NoTerminationCheck ) -> failure r 136 (NonTerminating , Terminating ) -> failure r 137 138combineCoverageChecks :: [CoverageCheck] -> CoverageCheck 139combineCoverageChecks = Fold.fold 140 141combinePositivityChecks :: [PositivityCheck] -> PositivityCheck 142combinePositivityChecks = Fold.fold 143 144data DeclKind 145 = LoneSigDecl Range DataRecOrFun Name 146 | LoneDefs DataRecOrFun [Name] 147 | OtherDecl 148 deriving (Eq, Show) 149 150declKind :: NiceDeclaration -> DeclKind 151declKind (FunSig r _ _ _ _ _ tc cc x _) = LoneSigDecl r (FunName tc cc) x 152declKind (NiceRecSig r _ _ pc uc x pars _) = LoneSigDecl r (RecName pc uc) x 153declKind (NiceDataSig r _ _ pc uc x pars _) = LoneSigDecl r (DataName pc uc) x 154declKind (FunDef r _ abs ins tc cc x _) = LoneDefs (FunName tc cc) [x] 155declKind (NiceDataDef _ _ _ pc uc x pars _) = LoneDefs (DataName pc uc) [x] 156declKind (NiceRecDef _ _ _ pc uc x _ pars _) = LoneDefs (RecName pc uc) [x] 157declKind (NiceUnquoteDef _ _ _ tc cc xs _) = LoneDefs (FunName tc cc) xs 158declKind Axiom{} = OtherDecl 159declKind NiceField{} = OtherDecl 160declKind PrimitiveFunction{} = OtherDecl 161declKind NiceMutual{} = OtherDecl 162declKind NiceModule{} = OtherDecl 163declKind NiceModuleMacro{} = OtherDecl 164declKind NiceOpen{} = OtherDecl 165declKind NiceImport{} = OtherDecl 166declKind NicePragma{} = OtherDecl 167declKind NiceFunClause{} = OtherDecl 168declKind NicePatternSyn{} = OtherDecl 169declKind NiceGeneralize{} = OtherDecl 170declKind NiceUnquoteDecl{} = OtherDecl 171declKind NiceLoneConstructor{} = OtherDecl 172 173-- | Replace (Data/Rec/Fun)Sigs with Axioms for postulated names 174-- The first argument is a list of axioms only. 175replaceSigs 176 :: LoneSigs -- ^ Lone signatures to be turned into Axioms 177 -> [NiceDeclaration] -- ^ Declarations containing them 178 -> [NiceDeclaration] -- ^ In the output, everything should be defined 179replaceSigs ps = if Map.null ps then id else \case 180 [] -> __IMPOSSIBLE__ 181 (d:ds) -> 182 case replaceable d of 183 -- If declaration d of x is mentioned in the map of lone signatures then replace 184 -- it with an axiom 185 Just (x, axiom) 186 | (Just (LoneSig _ x' _), ps') <- Map.updateLookupWithKey (\ _ _ -> Nothing) x ps 187 , getRange x == getRange x' 188 -- Use the range as UID to ensure we do not replace the wrong signature. 189 -- This could happen if the user wrote a duplicate definition. 190 -> axiom : replaceSigs ps' ds 191 _ -> d : replaceSigs ps ds 192 193 where 194 195 -- A @replaceable@ declaration is a signature. It has a name and we can make an 196 -- @Axiom@ out of it. 197 replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration) 198 replaceable = \case 199 FunSig r acc abst inst _ argi _ _ x' e -> 200 -- #4881: Don't use the unique NameId for NoName lookups. 201 let x = if isNoName x' then noName (nameRange x') else x' in 202 Just (x, Axiom r acc abst inst argi x' e) 203 NiceRecSig r acc abst _ _ x pars t -> 204 let e = Generalized $ makePi (lamBindingsToTelescope r pars) t in 205 Just (x, Axiom r acc abst NotInstanceDef defaultArgInfo x e) 206 NiceDataSig r acc abst _ _ x pars t -> 207 let e = Generalized $ makePi (lamBindingsToTelescope r pars) t in 208 Just (x, Axiom r acc abst NotInstanceDef defaultArgInfo x e) 209 _ -> Nothing 210 211-- | Main. Fixities (or more precisely syntax declarations) are needed when 212-- grouping function clauses. 213niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration] 214niceDeclarations fixs ds = do 215 216 -- Run the nicifier in an initial environment. But keep the warnings. 217 st <- get 218 put $ initNiceEnv { niceWarn = niceWarn st } 219 nds <- nice ds 220 221 -- Check that every signature got its definition. 222 ps <- use loneSigs 223 checkLoneSigs ps 224 -- We postulate the missing ones and insert them in place of the corresponding @FunSig@ 225 let ds = replaceSigs ps nds 226 227 -- Note that loneSigs is ensured to be empty. 228 -- (Important, since inferMutualBlocks also uses loneSigs state). 229 res <- inferMutualBlocks ds 230 231 -- Restore the old state, but keep the warnings. 232 warns <- gets niceWarn 233 put $ st { niceWarn = warns } 234 return res 235 236 where 237 238 inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration] 239 inferMutualBlocks [] = return [] 240 inferMutualBlocks (d : ds) = 241 case declKind d of 242 OtherDecl -> (d :) <$> inferMutualBlocks ds 243 LoneDefs{} -> (d :) <$> inferMutualBlocks ds -- Andreas, 2017-10-09, issue #2576: report error in ConcreteToAbstract 244 LoneSigDecl r k x -> do 245 _ <- addLoneSig r x k 246 InferredMutual checks nds0 ds1 <- untilAllDefined (mutualChecks k) ds 247 -- If we still have lone signatures without any accompanying definition, 248 -- we postulate the definition and substitute the axiom for the lone signature 249 ps <- use loneSigs 250 checkLoneSigs ps 251 let ds0 = replaceSigs ps (d : nds0) -- NB: don't forget the LoneSig the block started with! 252 -- We then keep processing the rest of the block 253 tc <- combineTerminationChecks (getRange d) (mutualTermination checks) 254 let cc = combineCoverageChecks (mutualCoverage checks) 255 let pc = combinePositivityChecks (mutualPositivity checks) 256 (NiceMutual (getRange ds0) tc cc pc ds0 :) <$> inferMutualBlocks ds1 257 where 258 untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual 259 untilAllDefined checks ds = do 260 done <- noLoneSigs 261 if done then return (InferredMutual checks [] ds) else 262 case ds of 263 [] -> return (InferredMutual checks [] ds) 264 d : ds -> case declKind d of 265 LoneSigDecl r k x -> do 266 void $ addLoneSig r x k 267 extendInferredBlock d <$> untilAllDefined (mutualChecks k <> checks) ds 268 LoneDefs k xs -> do 269 mapM_ removeLoneSig xs 270 extendInferredBlock d <$> untilAllDefined (mutualChecks k <> checks) ds 271 OtherDecl -> extendInferredBlock d <$> untilAllDefined checks ds 272 273 nice :: [Declaration] -> Nice [NiceDeclaration] 274 nice [] = return [] 275 nice ds = do 276 (xs , ys) <- nice1 ds 277 (xs ++) <$> nice ys 278 279 nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration]) 280 nice1 [] = return ([], []) -- Andreas, 2017-09-16, issue #2759: no longer __IMPOSSIBLE__ 281 nice1 (d:ds) = do 282 let justWarning :: HasCallStack => DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]) 283 justWarning w = do 284 -- NOTE: This is the location of the invoker of justWarning, not here. 285 withCallerCallStack $ declarationWarning' w 286 nice1 ds 287 288 case d of 289 290 TypeSig info _tac x t -> do 291 termCheck <- use terminationCheckPragma 292 covCheck <- use coverageCheckPragma 293 -- Andreas, 2020-09-28, issue #4950: take only range of identifier, 294 -- since parser expands type signatures with several identifiers 295 -- (like @x y z : A@) into several type signatures (with imprecise ranges). 296 let r = getRange x 297 -- register x as lone type signature, to recognize clauses later 298 x' <- addLoneSig r x $ FunName termCheck covCheck 299 return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x' t] , ds) 300 301 -- Should not show up: all FieldSig are part of a Field block 302 FieldSig{} -> __IMPOSSIBLE__ 303 304 Generalize r [] -> justWarning $ EmptyGeneralize r 305 Generalize r sigs -> do 306 gs <- forM sigs $ \case 307 sig@(TypeSig info tac x t) -> do 308 return $ NiceGeneralize (getRange sig) PublicAccess info tac x t 309 _ -> __IMPOSSIBLE__ 310 return (gs, ds) 311 312 (FunClause lhs _ _ _) -> do 313 termCheck <- use terminationCheckPragma 314 covCheck <- use coverageCheckPragma 315 catchall <- popCatchallPragma 316 xs <- loneFuns <$> use loneSigs 317 -- for each type signature 'x' waiting for clauses, we try 318 -- if we have some clauses for 'x' 319 case [ (x, (x', fits, rest)) 320 | (x, x') <- xs 321 , let (fits, rest) = 322 -- Anonymous declarations only have 1 clause each! 323 if isNoName x then ([d], ds) 324 else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds) 325 , not (null fits) 326 ] of 327 328 -- case: clauses match none of the sigs 329 [] -> case lhs of 330 -- Subcase: The lhs is single identifier (potentially anonymous). 331 -- Treat it as a function clause without a type signature. 332 LHS p [] [] | Just x <- isSingleIdentifierP p -> do 333 d <- mkFunDef (setOrigin Inserted defaultArgInfo) termCheck covCheck x Nothing [d] -- fun def without type signature is relevant 334 return (d , ds) 335 -- Subcase: The lhs is a proper pattern. 336 -- This could be a let-pattern binding. Pass it on. 337 -- A missing type signature error might be raise in ConcreteToAbstract 338 _ -> do 339 return ([NiceFunClause (getRange d) PublicAccess ConcreteDef termCheck covCheck catchall d] , ds) 340 341 -- case: clauses match exactly one of the sigs 342 [(x,(x',fits,rest))] -> do 343 -- The x'@NoName{} is the unique version of x@NoName{}. 344 removeLoneSig x 345 ds <- expandEllipsis fits 346 cs <- mkClauses x' ds False 347 return ([FunDef (getRange fits) fits ConcreteDef NotInstanceDef termCheck covCheck x' cs] , rest) 348 349 -- case: clauses match more than one sigs (ambiguity) 350 xf:xfs -> declarationException $ AmbiguousFunClauses lhs $ List1.reverse $ fmap fst $ xf :| xfs 351 -- "ambiguous function clause; cannot assign it uniquely to one type signature" 352 353 Field r [] -> justWarning $ EmptyField r 354 Field _ fs -> (,ds) <$> niceAxioms FieldBlock fs 355 356 DataSig r x tel t -> do 357 pc <- use positivityCheckPragma 358 uc <- use universeCheckPragma 359 _ <- addLoneSig r x $ DataName pc uc 360 (,ds) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x (Just (tel, t)) Nothing 361 362 Data r x tel t cs -> do 363 pc <- use positivityCheckPragma 364 -- Andreas, 2018-10-27, issue #3327 365 -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition. 366 -- Universe check is performed if both the current value of 367 -- 'universeCheckPragma' AND the one from the signature say so. 368 uc <- use universeCheckPragma 369 uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x 370 mt <- defaultTypeSig (DataName pc uc) x (Just t) 371 (,ds) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x ((tel,) <$> mt) (Just (tel, cs)) 372 373 DataDef r x tel cs -> do 374 pc <- use positivityCheckPragma 375 -- Andreas, 2018-10-27, issue #3327 376 -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition. 377 -- Universe check is performed if both the current value of 378 -- 'universeCheckPragma' AND the one from the signature say so. 379 uc <- use universeCheckPragma 380 uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x 381 mt <- defaultTypeSig (DataName pc uc) x Nothing 382 (,ds) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x ((tel,) <$> mt) (Just (tel, cs)) 383 384 RecordSig r x tel t -> do 385 pc <- use positivityCheckPragma 386 uc <- use universeCheckPragma 387 _ <- addLoneSig r x $ RecName pc uc 388 return ([NiceRecSig r PublicAccess ConcreteDef pc uc x tel t] , ds) 389 390 Record r x dir tel t cs -> do 391 pc <- use positivityCheckPragma 392 -- Andreas, 2018-10-27, issue #3327 393 -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition. 394 -- Universe check is performed if both the current value of 395 -- 'universeCheckPragma' AND the one from the signature say so. 396 uc <- use universeCheckPragma 397 uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x 398 mt <- defaultTypeSig (RecName pc uc) x (Just t) 399 (,ds) <$> dataOrRec pc uc (\ r o a pc uc x tel cs -> NiceRecDef r o a pc uc x dir tel cs) NiceRecSig 400 return r x ((tel,) <$> mt) (Just (tel, cs)) 401 402 RecordDef r x dir tel cs -> do 403 pc <- use positivityCheckPragma 404 -- Andreas, 2018-10-27, issue #3327 405 -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition. 406 -- Universe check is performed if both the current value of 407 -- 'universeCheckPragma' AND the one from the signature say so. 408 uc <- use universeCheckPragma 409 uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x 410 mt <- defaultTypeSig (RecName pc uc) x Nothing 411 (,ds) <$> dataOrRec pc uc (\ r o a pc uc x tel cs -> NiceRecDef r o a pc uc x dir tel cs) NiceRecSig 412 return r x ((tel,) <$> mt) (Just (tel, cs)) 413 414 RecordDirective r -> justWarning $ InvalidRecordDirective (getRange r) 415 416 Mutual r ds' -> do 417 -- The lone signatures encountered so far are not in scope 418 -- for the mutual definition 419 forgetLoneSigs 420 case ds' of 421 [] -> justWarning $ EmptyMutual r 422 _ -> (,ds) <$> (singleton <$> (mkOldMutual r =<< nice ds')) 423 424 InterleavedMutual r ds' -> do 425 -- The lone signatures encountered so far are not in scope 426 -- for the mutual definition 427 forgetLoneSigs 428 case ds' of 429 [] -> justWarning $ EmptyMutual r 430 _ -> (,ds) <$> (singleton <$> (mkInterleavedMutual r =<< nice ds')) 431 432 LoneConstructor r [] -> justWarning $ EmptyConstructor r 433 LoneConstructor r ds' -> 434 ((,ds) . singleton . NiceLoneConstructor r) <$> niceAxioms ConstructorBlock ds' 435 436 437 Abstract r [] -> justWarning $ EmptyAbstract r 438 Abstract r ds' -> 439 (,ds) <$> (abstractBlock r =<< nice ds') 440 441 Private r UserWritten [] -> justWarning $ EmptyPrivate r 442 Private r o ds' -> 443 (,ds) <$> (privateBlock r o =<< nice ds') 444 445 InstanceB r [] -> justWarning $ EmptyInstance r 446 InstanceB r ds' -> 447 (,ds) <$> (instanceBlock r =<< nice ds') 448 449 Macro r [] -> justWarning $ EmptyMacro r 450 Macro r ds' -> 451 (,ds) <$> (macroBlock r =<< nice ds') 452 453 Postulate r [] -> justWarning $ EmptyPostulate r 454 Postulate _ ds' -> 455 (,ds) <$> niceAxioms PostulateBlock ds' 456 457 Primitive r [] -> justWarning $ EmptyPrimitive r 458 Primitive _ ds' -> (,ds) <$> (map toPrim <$> niceAxioms PrimitiveBlock ds') 459 460 Module r x tel ds' -> return $ 461 ([NiceModule r PublicAccess ConcreteDef x tel ds'] , ds) 462 463 ModuleMacro r x modapp op is -> return $ 464 ([NiceModuleMacro r PublicAccess x modapp op is] , ds) 465 466 -- Fixity and syntax declarations and polarity pragmas have 467 -- already been processed. 468 Infix _ _ -> return ([], ds) 469 Syntax _ _ -> return ([], ds) 470 471 PatternSyn r n as p -> do 472 return ([NicePatternSyn r PublicAccess n as p] , ds) 473 Open r x is -> return ([NiceOpen r x is] , ds) 474 Import r x as op is -> return ([NiceImport r x as op is] , ds) 475 476 UnquoteDecl r xs e -> do 477 tc <- use terminationCheckPragma 478 cc <- use coverageCheckPragma 479 return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds) 480 481 UnquoteDef r xs e -> do 482 sigs <- map fst . loneFuns <$> use loneSigs 483 List1.ifNotNull (filter (`notElem` sigs) xs) 484 {-then-} (declarationException . UnquoteDefRequiresSignature) 485 {-else-} $ do 486 mapM_ removeLoneSig xs 487 return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds) 488 489 Pragma p -> nicePragma p ds 490 491 nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration]) 492 493 nicePragma (TerminationCheckPragma r (TerminationMeasure _ x)) ds = 494 if canHaveTerminationMeasure ds then 495 withTerminationCheckPragma (TerminationMeasure r x) $ nice1 ds 496 else do 497 declarationWarning $ InvalidTerminationCheckPragma r 498 nice1 ds 499 500 nicePragma (TerminationCheckPragma r NoTerminationCheck) ds = do 501 -- This PRAGMA has been deprecated in favour of (NON_)TERMINATING 502 -- We warn the user about it and then assume the function is NON_TERMINATING. 503 declarationWarning $ PragmaNoTerminationCheck r 504 nicePragma (TerminationCheckPragma r NonTerminating) ds 505 506 nicePragma (TerminationCheckPragma r tc) ds = 507 if canHaveTerminationCheckPragma ds then 508 withTerminationCheckPragma tc $ nice1 ds 509 else do 510 declarationWarning $ InvalidTerminationCheckPragma r 511 nice1 ds 512 513 nicePragma (NoCoverageCheckPragma r) ds = 514 if canHaveCoverageCheckPragma ds then 515 withCoverageCheckPragma NoCoverageCheck $ nice1 ds 516 else do 517 declarationWarning $ InvalidCoverageCheckPragma r 518 nice1 ds 519 520 nicePragma (CatchallPragma r) ds = 521 if canHaveCatchallPragma ds then 522 withCatchallPragma True $ nice1 ds 523 else do 524 declarationWarning $ InvalidCatchallPragma r 525 nice1 ds 526 527 nicePragma (NoPositivityCheckPragma r) ds = 528 if canHaveNoPositivityCheckPragma ds then 529 withPositivityCheckPragma NoPositivityCheck $ nice1 ds 530 else do 531 declarationWarning $ InvalidNoPositivityCheckPragma r 532 nice1 ds 533 534 nicePragma (NoUniverseCheckPragma r) ds = 535 if canHaveNoUniverseCheckPragma ds then 536 withUniverseCheckPragma NoUniverseCheck $ nice1 ds 537 else do 538 declarationWarning $ InvalidNoUniverseCheckPragma r 539 nice1 ds 540 541 nicePragma p@CompilePragma{} ds = do 542 declarationWarning $ PragmaCompiled (getRange p) 543 return ([NicePragma (getRange p) p], ds) 544 545 nicePragma (PolarityPragma{}) ds = return ([], ds) 546 547 nicePragma (BuiltinPragma r str qn@(QName x)) ds = do 548 return ([NicePragma r (BuiltinPragma r str qn)], ds) 549 550 nicePragma p ds = return ([NicePragma (getRange p) p], ds) 551 552 canHaveTerminationMeasure :: [Declaration] -> Bool 553 canHaveTerminationMeasure [] = False 554 canHaveTerminationMeasure (d:ds) = case d of 555 TypeSig{} -> True 556 (Pragma p) | isAttachedPragma p -> canHaveTerminationMeasure ds 557 _ -> False 558 559 canHaveTerminationCheckPragma :: [Declaration] -> Bool 560 canHaveTerminationCheckPragma [] = False 561 canHaveTerminationCheckPragma (d:ds) = case d of 562 Mutual _ ds -> any (canHaveTerminationCheckPragma . singleton) ds 563 TypeSig{} -> True 564 FunClause{} -> True 565 UnquoteDecl{} -> True 566 (Pragma p) | isAttachedPragma p -> canHaveTerminationCheckPragma ds 567 _ -> False 568 569 canHaveCoverageCheckPragma :: [Declaration] -> Bool 570 canHaveCoverageCheckPragma = canHaveTerminationCheckPragma 571 572 canHaveCatchallPragma :: [Declaration] -> Bool 573 canHaveCatchallPragma [] = False 574 canHaveCatchallPragma (d:ds) = case d of 575 FunClause{} -> True 576 (Pragma p) | isAttachedPragma p -> canHaveCatchallPragma ds 577 _ -> False 578 579 canHaveNoPositivityCheckPragma :: [Declaration] -> Bool 580 canHaveNoPositivityCheckPragma [] = False 581 canHaveNoPositivityCheckPragma (d:ds) = case d of 582 Mutual _ ds -> any (canHaveNoPositivityCheckPragma . singleton) ds 583 Data{} -> True 584 DataSig{} -> True 585 DataDef{} -> True 586 Record{} -> True 587 RecordSig{} -> True 588 RecordDef{} -> True 589 Pragma p | isAttachedPragma p -> canHaveNoPositivityCheckPragma ds 590 _ -> False 591 592 canHaveNoUniverseCheckPragma :: [Declaration] -> Bool 593 canHaveNoUniverseCheckPragma [] = False 594 canHaveNoUniverseCheckPragma (d:ds) = case d of 595 Data{} -> True 596 DataSig{} -> True 597 DataDef{} -> True 598 Record{} -> True 599 RecordSig{} -> True 600 RecordDef{} -> True 601 Pragma p | isAttachedPragma p -> canHaveNoPositivityCheckPragma ds 602 _ -> False 603 604 -- Pragma that attaches to the following declaration. 605 isAttachedPragma :: Pragma -> Bool 606 isAttachedPragma = \case 607 TerminationCheckPragma{} -> True 608 CatchallPragma{} -> True 609 NoPositivityCheckPragma{} -> True 610 NoUniverseCheckPragma{} -> True 611 _ -> False 612 613 -- We could add a default type signature here, but at the moment we can't 614 -- infer the type of a record or datatype, so better to just fail here. 615 defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr) 616 defaultTypeSig k x t@Just{} = return t 617 defaultTypeSig k x Nothing = do 618 caseMaybeM (getSig x) (return Nothing) $ \ k' -> do 619 unless (sameKind k k') $ declarationException $ WrongDefinition x k' k 620 Nothing <$ removeLoneSig x 621 622 dataOrRec 623 :: forall a decl 624 . PositivityCheck 625 -> UniverseCheck 626 -> (Range -> Origin -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> [decl] -> NiceDeclaration) 627 -- Construct definition. 628 -> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration) 629 -- Construct signature. 630 -> ([a] -> Nice [decl]) -- Constructor checking. 631 -> Range 632 -> Name -- Data/record type name. 633 -> Maybe ([LamBinding], Expr) -- Parameters and type. If not @Nothing@ a signature is created. 634 -> Maybe ([LamBinding], [a]) -- Parameters and constructors. If not @Nothing@, a definition body is created. 635 -> Nice [NiceDeclaration] 636 dataOrRec pc uc mkDef mkSig niceD r x mt mcs = do 637 mds <- Trav.forM mcs $ \ (tel, cs) -> (tel,) <$> niceD cs 638 -- We set origin to UserWritten if the user split the data/rec herself, 639 -- and to Inserted if the she wrote a single declaration that we're 640 -- splitting up here. We distinguish these because the scoping rules for 641 -- generalizable variables differ in these cases. 642 let o | isJust mt && isJust mcs = Inserted 643 | otherwise = UserWritten 644 return $ catMaybes $ 645 [ mt <&> \ (tel, t) -> mkSig (fuseRange x t) PublicAccess ConcreteDef pc uc x tel t 646 , mds <&> \ (tel, ds) -> mkDef r o ConcreteDef pc uc x (caseMaybe mt tel $ const $ concatMap dropTypeAndModality tel) ds 647 -- If a type is given (mt /= Nothing), we have to delete the types in @tel@ 648 -- for the data definition, lest we duplicate them. And also drop modalities (#1886). 649 ] 650 -- Translate axioms 651 niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration] 652 niceAxioms b ds = List.concat <$> mapM (niceAxiom b) ds 653 654 niceAxiom :: KindOfBlock -> TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration] 655 niceAxiom b = \case 656 d@(TypeSig rel _tac x t) -> do 657 return [ Axiom (getRange d) PublicAccess ConcreteDef NotInstanceDef rel x t ] 658 d@(FieldSig i tac x argt) | b == FieldBlock -> do 659 return [ NiceField (getRange d) PublicAccess ConcreteDef i tac x argt ] 660 InstanceB r decls -> do 661 instanceBlock r =<< niceAxioms InstanceBlock decls 662 Pragma p@(RewritePragma r _ _) -> do 663 return [ NicePragma r p ] 664 d -> declarationException $ WrongContentBlock b $ getRange d 665 666 toPrim :: NiceDeclaration -> NiceDeclaration 667 toPrim (Axiom r p a i rel x t) = PrimitiveFunction r p a x (Arg rel t) 668 toPrim _ = __IMPOSSIBLE__ 669 670 -- Create a function definition. 671 mkFunDef info termCheck covCheck x mt ds0 = do 672 ds <- expandEllipsis ds0 673 cs <- mkClauses x ds False 674 return [ FunSig (fuseRange x t) PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x t 675 , FunDef (getRange ds0) ds0 ConcreteDef NotInstanceDef termCheck covCheck x cs ] 676 where 677 t = fromMaybe (underscore (getRange x)) mt 678 679 underscore r = Underscore r Nothing 680 681 682 expandEllipsis :: [Declaration] -> Nice [Declaration] 683 expandEllipsis [] = return [] 684 expandEllipsis (d@(FunClause lhs@(LHS p _ _) _ _ _) : ds) 685 | hasEllipsis p = (d :) <$> expandEllipsis ds 686 | otherwise = (d :) <$> expand (killRange p) ds 687 where 688 expand :: Pattern -> [Declaration] -> Nice [Declaration] 689 expand _ [] = return [] 690 expand p (d : ds) = do 691 case d of 692 Pragma (CatchallPragma _) -> do 693 (d :) <$> expand p ds 694 FunClause (LHS p0 eqs es) rhs wh ca -> do 695 case hasEllipsis' p0 of 696 ManyHoles -> declarationException $ MultipleEllipses p0 697 OneHole cxt ~(EllipsisP r Nothing) -> do 698 -- Replace the ellipsis by @p@. 699 let p1 = cxt $ EllipsisP r $ Just $ setRange r p 700 let d' = FunClause (LHS p1 eqs es) rhs wh ca 701 -- If we have with-expressions (es /= []) then the following 702 -- ellipses also get the additional patterns in p0. 703 (d' :) <$> expand (if null es then p else killRange p1) ds 704 ZeroHoles _ -> do 705 -- We can have ellipses after a fun clause without. 706 -- They refer to the last clause that introduced new with-expressions. 707 -- Same here: If we have new with-expressions, the next ellipses will 708 -- refer to us. 709 -- Andreas, Jesper, 2017-05-13, issue #2578 710 -- Need to update the range also on the next with-patterns. 711 (d :) <$> expand (if null es then p else killRange p0) ds 712 _ -> __IMPOSSIBLE__ 713 expandEllipsis _ = __IMPOSSIBLE__ 714 715 -- Turn function clauses into nice function clauses. 716 mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause] 717 mkClauses _ [] _ = return [] 718 mkClauses x (Pragma (CatchallPragma r) : cs) True = do 719 declarationWarning $ InvalidCatchallPragma r 720 mkClauses x cs True 721 mkClauses x (Pragma (CatchallPragma r) : cs) False = do 722 when (null cs) $ declarationWarning $ InvalidCatchallPragma r 723 mkClauses x cs True 724 725 mkClauses x (FunClause lhs rhs wh ca : cs) catchall 726 | null (lhsWithExpr lhs) || hasEllipsis lhs = 727 (Clause x (ca || catchall) lhs rhs wh [] :) <$> mkClauses x cs False -- Will result in an error later. 728 729 mkClauses x (FunClause lhs rhs wh ca : cs) catchall = do 730 when (null withClauses) $ declarationException $ MissingWithClauses x lhs 731 wcs <- mkClauses x withClauses False 732 (Clause x (ca || catchall) lhs rhs wh wcs :) <$> mkClauses x cs' False 733 where 734 (withClauses, cs') = subClauses cs 735 736 -- A clause is a subclause if the number of with-patterns is 737 -- greater or equal to the current number of with-patterns plus the 738 -- number of with arguments. 739 numWith = numberOfWithPatterns p + length (filter visible es) where LHS p _ es = lhs 740 741 subClauses :: [Declaration] -> ([Declaration],[Declaration]) 742 subClauses (c@(FunClause (LHS p0 _ _) _ _ _) : cs) 743 | isEllipsis p0 || 744 numberOfWithPatterns p0 >= numWith = mapFst (c:) (subClauses cs) 745 | otherwise = ([], c:cs) 746 subClauses (c@(Pragma (CatchallPragma r)) : cs) = case subClauses cs of 747 ([], cs') -> ([], c:cs') 748 (cs, cs') -> (c:cs, cs') 749 subClauses [] = ([],[]) 750 subClauses _ = __IMPOSSIBLE__ 751 mkClauses _ _ _ = __IMPOSSIBLE__ 752 753 couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool 754 couldBeCallOf mFixity x p = 755 let 756 pns = patternNames p 757 xStrings = nameStringParts x 758 patStrings = concatMap nameStringParts pns 759 in 760-- trace ("x = " ++ prettyShow x) $ 761-- trace ("pns = " ++ show pns) $ 762-- trace ("xStrings = " ++ show xStrings) $ 763-- trace ("patStrings = " ++ show patStrings) $ 764-- trace ("mFixity = " ++ show mFixity) $ 765 case (listToMaybe pns, mFixity) of 766 -- first identifier in the patterns is the fun.symbol? 767 (Just y, _) | x == y -> True -- trace ("couldBe since y = " ++ prettyShow y) $ True 768 -- are the parts of x contained in p 769 _ | xStrings `isSublistOf` patStrings -> True -- trace ("couldBe since isSublistOf") $ True 770 -- looking for a mixfix fun.symb 771 (_, Just fix) -> -- also matches in case of a postfix 772 let notStrings = stringParts (theNotation fix) 773 in -- trace ("notStrings = " ++ show notStrings) $ 774 -- trace ("patStrings = " ++ show patStrings) $ 775 not (null notStrings) && (notStrings `isSublistOf` patStrings) 776 -- not a notation, not first id: give up 777 _ -> False -- trace ("couldBe not (case default)") $ False 778 779 780 -- for finding nice clauses for a type sig in mutual blocks 781 couldBeNiceFunClauseOf :: Maybe Fixity' -> Name -> NiceDeclaration 782 -> Maybe (MutualChecks, Declaration) 783 couldBeNiceFunClauseOf mf n (NiceFunClause _ _ _ tc cc _ d) 784 = (MutualChecks [tc] [cc] [], d) <$ guard (couldBeFunClauseOf mf n d) 785 couldBeNiceFunClauseOf _ _ _ = Nothing 786 787 -- for finding clauses for a type sig in mutual blocks 788 couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool 789 couldBeFunClauseOf mFixity x (Pragma (CatchallPragma{})) = True 790 couldBeFunClauseOf mFixity x (FunClause (LHS p _ _) _ _ _) = 791 hasEllipsis p || couldBeCallOf mFixity x p 792 couldBeFunClauseOf _ _ _ = False -- trace ("couldBe not (fun default)") $ False 793 794 -- Turn a new style `interleaved mutual' block into a new style mutual block 795 -- by grouping the declarations in blocks. 796 mkInterleavedMutual 797 :: Range -- Range of the whole @mutual@ block. 798 -> [NiceDeclaration] -- Declarations inside the block. 799 -> Nice NiceDeclaration -- Returns a 'NiceMutual'. 800 mkInterleavedMutual r ds' = do 801 (other, (m, checks, _)) <- runStateT (groupByBlocks r ds') (empty, mempty, 0) 802 let idecls = other ++ concatMap (uncurry interleavedDecl) (Map.toList m) 803 let decls0 = map snd $ List.sortBy (compare `on` fst) idecls 804 ps <- use loneSigs 805 checkLoneSigs ps 806 let decls = replaceSigs ps decls0 807 -- process the checks 808 tc <- combineTerminationChecks r (mutualTermination checks) 809 let cc = combineCoverageChecks (mutualCoverage checks) 810 let pc = combinePositivityChecks (mutualPositivity checks) 811 pure $ NiceMutual r tc cc pc decls 812 813 where 814 815 ------------------------------------------------------------------------------ 816 -- Adding Signatures 817 addType :: Name -> (Int -> a) -> MutualChecks 818 -> StateT (Map Name a, MutualChecks, Int) Nice () 819 addType n c mc = do 820 (m, checks, i) <- get 821 when (isJust $ Map.lookup n m) $ lift $ declarationException $ DuplicateDefinition n 822 put (Map.insert n (c i) m, mc <> checks, i+1) 823 824 addFunType d@(FunSig _ _ _ _ _ _ tc cc n _) = do 825 let checks = MutualChecks [tc] [cc] [] 826 addType n (\ i -> InterleavedFun (i, d) Nothing) checks 827 addFunType _ = __IMPOSSIBLE__ 828 829 addDataType d@(NiceDataSig _ _ _ pc uc n _ _) = do 830 let checks = MutualChecks [] [] [pc] 831 addType n (\ i -> InterleavedData (i, d) Nothing) checks 832 addDataType _ = __IMPOSSIBLE__ 833 834 ------------------------------------------------------------------------------ 835 -- Adding constructors & clauses 836 837 addDataConstructors :: Maybe Name -- Data type the constructors belong to 838 -> [NiceConstructor] -- Constructors to add 839 -> StateT (InterleavedMutual, MutualChecks, Int) Nice () 840 -- if we know the type's name, we can go ahead 841 addDataConstructors (Just n) ds = do 842 (m, checks, i) <- get 843 case Map.lookup n m of 844 Just (InterleavedData (i0, sig) cs) -> do 845 lift $ removeLoneSig n 846 -- add the constructors to the existing ones (if any) 847 let (cs', i') = case cs of 848 Nothing -> ((i, [ds]) , i+1) 849 Just (i1, ds1) -> ((i1, ds:ds1), i) 850 put (Map.insert n (InterleavedData (i0, sig) (Just cs')) m, checks, i') 851 _ -> __IMPOSSIBLE__ -- we have resolved the name `n` already and it comes from a DataSig! 852 853 addDataConstructors Nothing [] = pure () 854 855 -- Otherwise we try to guess which datasig the constructor is referring to 856 addDataConstructors Nothing (d : ds) = do 857 -- get the candidate data types that are in this interleaved mutual block 858 (m, _, _) <- get 859 let sigs = mapMaybe (\ (n, d) -> n <$ isInterleavedData d) $ Map.toList m 860 -- check whether this constructor matches any of them 861 case isConstructor sigs d of 862 Right n -> do 863 -- if so grab the whole block that may work and add them 864 let (ds0, ds1) = span (isRight . isConstructor [n]) ds 865 addDataConstructors (Just n) (d : ds0) 866 -- and then repeat the process for the rest of the block 867 addDataConstructors Nothing ds1 868 Left (n, ns) -> lift $ declarationException $ AmbiguousConstructor (getRange d) n ns 869 870 addFunDef :: NiceDeclaration -> StateT (InterleavedMutual, MutualChecks, Int) Nice () 871 addFunDef (FunDef _ ds _ _ tc cc n cs) = do 872 let check = MutualChecks [tc] [cc] [] 873 (m, checks, i) <- get 874 case Map.lookup n m of 875 Just (InterleavedFun (i0, sig) cs0) -> do 876 let (cs', i') = case cs0 of 877 Nothing -> ((i, [(ds, cs)]) , i+1) 878 Just (i1, cs1) -> ((i1, (ds, cs):cs1), i) 879 put (Map.insert n (InterleavedFun (i0, sig) (Just cs')) m, check <> checks, i') 880 _ -> __IMPOSSIBLE__ -- A FunDef always come after an existing FunSig! 881 addFunDef _ = __IMPOSSIBLE__ 882 883 addFunClauses :: Range -> [NiceDeclaration] 884 -> StateT (InterleavedMutual, MutualChecks, Int) Nice [(Int, NiceDeclaration)] 885 addFunClauses r (nd@(NiceFunClause _ _ _ tc cc _ d@(FunClause lhs _ _ _)) : ds) = do 886 -- get the candidate functions that are in this interleaved mutual block 887 (m, checks, i) <- get 888 let sigs = mapMaybe (\ (n, d) -> n <$ isInterleavedFun d) $ Map.toList m 889 -- find the funsig candidates for the funclause of interest 890 case [ (x, fits, rest) 891 | x <- sigs 892 , let (fits, rest) = spanJust (couldBeNiceFunClauseOf (Map.lookup x fixs) x) (nd : ds) 893 , not (null fits) 894 ] of 895 -- no candidate: keep the isolated fun clause, we'll complain about it later 896 [] -> do 897 let check = MutualChecks [tc] [cc] [] 898 put (m, check <> checks, i+1) 899 ((i,nd) :) <$> groupByBlocks r ds 900 -- exactly one candidate: attach the funclause to the definition 901 [(n, fits0, rest)] -> do 902 let (checkss, fits) = unzip fits0 903 ds <- lift $ expandEllipsis fits 904 cs <- lift $ mkClauses n ds False 905 case Map.lookup n m of 906 Just (InterleavedFun (i0, sig) cs0) -> do 907 let (cs', i') = case cs0 of 908 Nothing -> ((i, [(fits,cs)]), i+1) 909 Just (i1, cs1) -> ((i1, (fits,cs):cs1), i) 910 let checks' = Fold.fold checkss 911 put (Map.insert n (InterleavedFun (i0, sig) (Just cs')) m, checks' <> checks, i') 912 _ -> __IMPOSSIBLE__ 913 groupByBlocks r rest 914 -- more than one candidate: fail, complaining about the ambiguity! 915 xf:xfs -> lift $ declarationException 916 $ AmbiguousFunClauses lhs 917 $ List1.reverse $ fmap (\ (a,_,_) -> a) $ xf :| xfs 918 addFunClauses _ _ = __IMPOSSIBLE__ 919 920 groupByBlocks :: Range -> [NiceDeclaration] 921 -> StateT (InterleavedMutual, MutualChecks, Int) Nice [(Int, NiceDeclaration)] 922 groupByBlocks r [] = pure [] 923 groupByBlocks r (d : ds) = do 924 -- for most branches we deal with the one declaration and move on 925 let oneOff act = act >>= \ ns -> (ns ++) <$> groupByBlocks r ds 926 case d of 927 NiceDataSig{} -> oneOff $ [] <$ addDataType d 928 NiceDataDef _ _ _ _ _ n _ ds -> oneOff $ [] <$ addDataConstructors (Just n) ds 929 NiceLoneConstructor r ds -> oneOff $ [] <$ addDataConstructors Nothing ds 930 FunSig{} -> oneOff $ [] <$ addFunType d 931 FunDef _ _ _ _ _ _ n cs 932 | not (isNoName n) -> oneOff $ [] <$ addFunDef d 933 -- It's a bit different for fun clauses because we may need to grab a lot 934 -- of clauses to handle ellipses properly. 935 NiceFunClause{} -> addFunClauses r (d:ds) 936 -- We do not need to worry about RecSig vs. RecDef: we know there's exactly one 937 -- of each for record definitions and leaving them in place should be enough! 938 _ -> oneOff $ do 939 (m, c, i) <- get -- TODO: grab checks from c? 940 put (m, c, i+1) 941 pure [(i,d)] 942 943 -- Extract the name of the return type (if any) of a potential constructor. 944 -- In case of failure return the name of the constructor and the list of candidates 945 -- for the return type. 946 -- A `constructor' block should only contain NiceConstructors so we crash with 947 -- an IMPOSSIBLE otherwise 948 isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name 949 isConstructor ns (Axiom _ _ _ _ _ n e) 950 -- extract the return type & see it as an LHS-style pattern 951 | Just p <- exprToPatternWithHoles <$> returnExpr e = 952 case [ x | x <- ns 953 , couldBeCallOf (Map.lookup x fixs) x p 954 ] of 955 [x] -> Right x 956 xs -> Left (n, xs) 957 -- which may fail (e.g. if the "return type" is a hole 958 | otherwise = Left (n, []) 959 isConstructor _ _ = __IMPOSSIBLE__ 960 961 -- Turn an old-style mutual block into a new style mutual block 962 -- by pushing the definitions to the end. 963 mkOldMutual 964 :: Range -- Range of the whole @mutual@ block. 965 -> [NiceDeclaration] -- Declarations inside the block. 966 -> Nice NiceDeclaration -- Returns a 'NiceMutual'. 967 mkOldMutual r ds' = do 968 -- Postulate the missing definitions 969 let ps = loneSigsFromLoneNames loneNames 970 checkLoneSigs ps 971 let ds = replaceSigs ps ds' 972 973 -- -- Remove the declarations that aren't allowed in old style mutual blocks 974 -- ds <- fmap catMaybes $ forM ds $ \ d -> let success = pure (Just d) in case d of 975 -- -- Andreas, 2013-11-23 allow postulates in mutual blocks 976 -- Axiom{} -> success 977 -- -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature 978 -- -- in ConcreteToAbstract rather than here. 979 -- NiceFunClause{} -> success 980 -- -- Andreas, 2018-05-11, issue #3052, allow pat.syn.s in mutual blocks 981 -- NicePatternSyn{} -> success 982 -- -- Otherwise, only categorized signatures and definitions are allowed: 983 -- -- Data, Record, Fun 984 -- _ -> if (declKind d /= OtherDecl) then success 985 -- else Nothing <$ declarationWarning (NotAllowedInMutual (getRange d) $ declName d) 986 -- Sort the declarations in the mutual block. 987 -- Declarations of names go to the top. (Includes module definitions.) 988 -- Definitions of names go to the bottom. 989 -- Some declarations are forbidden, as their positioning could confuse 990 -- the user. 991 (top, bottom, invalid) <- forEither3M ds $ \ d -> do 992 let top = return (In1 d) 993 bottom = return (In2 d) 994 invalid s = In3 d <$ do declarationWarning $ NotAllowedInMutual (getRange d) s 995 case d of 996 -- Andreas, 2013-11-23 allow postulates in mutual blocks 997 Axiom{} -> top 998 NiceField{} -> top 999 PrimitiveFunction{} -> top 1000 -- Andreas, 2019-07-23 issue #3932: 1001 -- Nested mutual blocks are not supported. 1002 NiceMutual{} -> invalid "mutual blocks" 1003 -- Andreas, 2018-10-29, issue #3246 1004 -- We could allow modules (top), but this is potentially confusing. 1005 NiceModule{} -> invalid "Module definitions" 1006 -- Lone constructors are only allowed in new-style mutual blocks 1007 NiceLoneConstructor{} -> invalid "Lone constructors" 1008 NiceModuleMacro{} -> top 1009 NiceOpen{} -> top 1010 NiceImport{} -> top 1011 NiceRecSig{} -> top 1012 NiceDataSig{} -> top 1013 -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature 1014 -- in ConcreteToAbstract rather than here. 1015 NiceFunClause{} -> bottom 1016 FunSig{} -> top 1017 FunDef{} -> bottom 1018 NiceDataDef{} -> bottom 1019 NiceRecDef{} -> bottom 1020 -- Andreas, 2018-05-11, issue #3051, allow pat.syn.s in mutual blocks 1021 -- Andreas, 2018-10-29: We shift pattern synonyms to the bottom 1022 -- since they might refer to constructors defined in a data types 1023 -- just above them. 1024 NicePatternSyn{} -> bottom 1025 NiceGeneralize{} -> top 1026 NiceUnquoteDecl{} -> top 1027 NiceUnquoteDef{} -> bottom 1028 NicePragma r pragma -> case pragma of 1029 1030 OptionsPragma{} -> top -- error thrown in the type checker 1031 1032 -- Some builtins require a definition, and they affect type checking 1033 -- Thus, we do not handle BUILTINs in mutual blocks (at least for now). 1034 BuiltinPragma{} -> invalid "BUILTIN pragmas" 1035 1036 -- The REWRITE pragma behaves differently before or after the def. 1037 -- and affects type checking. Thus, we refuse it here. 1038 RewritePragma{} -> invalid "REWRITE pragmas" 1039 1040 -- Compiler pragmas are not needed for type checking, thus, 1041 -- can go to the bottom. 1042 ForeignPragma{} -> bottom 1043 CompilePragma{} -> bottom 1044 1045 StaticPragma{} -> bottom 1046 InlinePragma{} -> bottom 1047 1048 ImpossiblePragma{} -> top -- error thrown in scope checker 1049 EtaPragma{} -> bottom -- needs record definition 1050 WarningOnUsage{} -> top 1051 WarningOnImport{} -> top 1052 InjectivePragma{} -> top -- only needs name, not definition 1053 DisplayPragma{} -> top -- only for printing 1054 1055 -- The attached pragmas have already been handled at this point. 1056 CatchallPragma{} -> __IMPOSSIBLE__ 1057 TerminationCheckPragma{} -> __IMPOSSIBLE__ 1058 NoPositivityCheckPragma{} -> __IMPOSSIBLE__ 1059 PolarityPragma{} -> __IMPOSSIBLE__ 1060 NoUniverseCheckPragma{} -> __IMPOSSIBLE__ 1061 NoCoverageCheckPragma{} -> __IMPOSSIBLE__ 1062 1063 -- -- Pull type signatures to the top 1064 -- let (sigs, other) = List.partition isTypeSig ds 1065 1066 -- -- Push definitions to the bottom 1067 -- let (other, defs) = flip List.partition ds $ \case 1068 -- FunDef{} -> False 1069 -- NiceDataDef{} -> False 1070 -- NiceRecDef{} -> False 1071 -- NiceFunClause{} -> False 1072 -- NicePatternSyn{} -> False 1073 -- NiceUnquoteDef{} -> False 1074 -- _ -> True 1075 1076 -- Compute termination checking flag for mutual block 1077 tc0 <- use terminationCheckPragma 1078 let tcs = map termCheck ds 1079 tc <- combineTerminationChecks r (tc0:tcs) 1080 1081 -- Compute coverage checking flag for mutual block 1082 cc0 <- use coverageCheckPragma 1083 let ccs = map covCheck ds 1084 let cc = combineCoverageChecks (cc0:ccs) 1085 1086 -- Compute positivity checking flag for mutual block 1087 pc0 <- use positivityCheckPragma 1088 let pcs = map positivityCheckOldMutual ds 1089 let pc = combinePositivityChecks (pc0:pcs) 1090 1091 return $ NiceMutual r tc cc pc $ top ++ bottom 1092 -- return $ NiceMutual r tc pc $ other ++ defs 1093 -- return $ NiceMutual r tc pc $ sigs ++ other 1094 where 1095 1096 -- isTypeSig Axiom{} = True 1097 -- isTypeSig d | LoneSig{} <- declKind d = True 1098 -- isTypeSig _ = False 1099 1100 sigNames = [ (r, x, k) | LoneSigDecl r k x <- map declKind ds' ] 1101 defNames = [ (x, k) | LoneDefs k xs <- map declKind ds', x <- xs ] 1102 -- compute the set difference with equality just on names 1103 loneNames = [ (r, x, k) | (r, x, k) <- sigNames, List.all ((x /=) . fst) defNames ] 1104 1105 termCheck :: NiceDeclaration -> TerminationCheck 1106 -- Andreas, 2013-02-28 (issue 804): 1107 -- do not termination check a mutual block if any of its 1108 -- inner declarations comes with a {-# NO_TERMINATION_CHECK #-} 1109 termCheck (FunSig _ _ _ _ _ _ tc _ _ _) = tc 1110 termCheck (FunDef _ _ _ _ tc _ _ _) = tc 1111 -- ASR (28 December 2015): Is this equation necessary? 1112 termCheck (NiceMutual _ tc _ _ _) = tc 1113 termCheck (NiceUnquoteDecl _ _ _ _ tc _ _ _) = tc 1114 termCheck (NiceUnquoteDef _ _ _ tc _ _ _) = tc 1115 termCheck Axiom{} = TerminationCheck 1116 termCheck NiceField{} = TerminationCheck 1117 termCheck PrimitiveFunction{} = TerminationCheck 1118 termCheck NiceModule{} = TerminationCheck 1119 termCheck NiceModuleMacro{} = TerminationCheck 1120 termCheck NiceOpen{} = TerminationCheck 1121 termCheck NiceImport{} = TerminationCheck 1122 termCheck NicePragma{} = TerminationCheck 1123 termCheck NiceRecSig{} = TerminationCheck 1124 termCheck NiceDataSig{} = TerminationCheck 1125 termCheck NiceFunClause{} = TerminationCheck 1126 termCheck NiceDataDef{} = TerminationCheck 1127 termCheck NiceRecDef{} = TerminationCheck 1128 termCheck NicePatternSyn{} = TerminationCheck 1129 termCheck NiceGeneralize{} = TerminationCheck 1130 termCheck NiceLoneConstructor{} = TerminationCheck 1131 1132 covCheck :: NiceDeclaration -> CoverageCheck 1133 covCheck (FunSig _ _ _ _ _ _ _ cc _ _) = cc 1134 covCheck (FunDef _ _ _ _ _ cc _ _) = cc 1135 -- ASR (28 December 2015): Is this equation necessary? 1136 covCheck (NiceMutual _ _ cc _ _) = cc 1137 covCheck (NiceUnquoteDecl _ _ _ _ _ cc _ _) = cc 1138 covCheck (NiceUnquoteDef _ _ _ _ cc _ _) = cc 1139 covCheck Axiom{} = YesCoverageCheck 1140 covCheck NiceField{} = YesCoverageCheck 1141 covCheck PrimitiveFunction{} = YesCoverageCheck 1142 covCheck NiceModule{} = YesCoverageCheck 1143 covCheck NiceModuleMacro{} = YesCoverageCheck 1144 covCheck NiceOpen{} = YesCoverageCheck 1145 covCheck NiceImport{} = YesCoverageCheck 1146 covCheck NicePragma{} = YesCoverageCheck 1147 covCheck NiceRecSig{} = YesCoverageCheck 1148 covCheck NiceDataSig{} = YesCoverageCheck 1149 covCheck NiceFunClause{} = YesCoverageCheck 1150 covCheck NiceDataDef{} = YesCoverageCheck 1151 covCheck NiceRecDef{} = YesCoverageCheck 1152 covCheck NicePatternSyn{} = YesCoverageCheck 1153 covCheck NiceGeneralize{} = YesCoverageCheck 1154 covCheck NiceLoneConstructor{} = YesCoverageCheck 1155 1156 -- ASR (26 December 2015): Do not positivity check a mutual 1157 -- block if any of its inner declarations comes with a 1158 -- NO_POSITIVITY_CHECK pragma. See Issue 1614. 1159 positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck 1160 positivityCheckOldMutual (NiceDataDef _ _ _ pc _ _ _ _) = pc 1161 positivityCheckOldMutual (NiceDataSig _ _ _ pc _ _ _ _) = pc 1162 positivityCheckOldMutual (NiceMutual _ _ _ pc _) = pc 1163 positivityCheckOldMutual (NiceRecSig _ _ _ pc _ _ _ _) = pc 1164 positivityCheckOldMutual (NiceRecDef _ _ _ pc _ _ _ _ _) = pc 1165 positivityCheckOldMutual _ = YesPositivityCheck 1166 1167 -- A mutual block cannot have a measure, 1168 -- but it can skip termination check. 1169 1170 abstractBlock _ [] = return [] 1171 abstractBlock r ds = do 1172 (ds', anyChange) <- runChangeT $ mkAbstract ds 1173 let inherited = r == noRange 1174 if anyChange then return ds' else do 1175 -- hack to avoid failing on inherited abstract blocks in where clauses 1176 unless inherited $ declarationWarning $ UselessAbstract r 1177 return ds -- no change! 1178 1179 privateBlock _ _ [] = return [] 1180 privateBlock r o ds = do 1181 (ds', anyChange) <- runChangeT $ mkPrivate o ds 1182 if anyChange then return ds' else do 1183 when (o == UserWritten) $ declarationWarning $ UselessPrivate r 1184 return ds -- no change! 1185 1186 instanceBlock 1187 :: Range -- Range of @instance@ keyword. 1188 -> [NiceDeclaration] 1189 -> Nice [NiceDeclaration] 1190 instanceBlock _ [] = return [] 1191 instanceBlock r ds = do 1192 let (ds', anyChange) = runChange $ mapM (mkInstance r) ds 1193 if anyChange then return ds' else do 1194 declarationWarning $ UselessInstance r 1195 return ds -- no change! 1196 1197 -- Make a declaration eligible for instance search. 1198 mkInstance 1199 :: Range -- Range of @instance@ keyword. 1200 -> Updater NiceDeclaration 1201 mkInstance r0 = \case 1202 Axiom r p a i rel x e -> (\ i -> Axiom r p a i rel x e) <$> setInstance r0 i 1203 FunSig r p a i m rel tc cc x e -> (\ i -> FunSig r p a i m rel tc cc x e) <$> setInstance r0 i 1204 NiceUnquoteDecl r p a i tc cc x e -> (\ i -> NiceUnquoteDecl r p a i tc cc x e) <$> setInstance r0 i 1205 NiceMutual r tc cc pc ds -> NiceMutual r tc cc pc <$> mapM (mkInstance r0) ds 1206 NiceLoneConstructor r ds -> NiceLoneConstructor r <$> mapM (mkInstance r0) ds 1207 d@NiceFunClause{} -> return d 1208 FunDef r ds a i tc cc x cs -> (\ i -> FunDef r ds a i tc cc x cs) <$> setInstance r0 i 1209 d@NiceField{} -> return d -- Field instance are handled by the parser 1210 d@PrimitiveFunction{} -> return d 1211 d@NiceUnquoteDef{} -> return d 1212 d@NiceRecSig{} -> return d 1213 d@NiceDataSig{} -> return d 1214 d@NiceModuleMacro{} -> return d 1215 d@NiceModule{} -> return d 1216 d@NicePragma{} -> return d 1217 d@NiceOpen{} -> return d 1218 d@NiceImport{} -> return d 1219 d@NiceDataDef{} -> return d 1220 d@NiceRecDef{} -> return d 1221 d@NicePatternSyn{} -> return d 1222 d@NiceGeneralize{} -> return d 1223 1224 setInstance 1225 :: Range -- Range of @instance@ keyword. 1226 -> Updater IsInstance 1227 setInstance r0 = \case 1228 i@InstanceDef{} -> return i 1229 _ -> dirty $ InstanceDef r0 1230 1231 macroBlock r ds = mapM mkMacro ds 1232 1233 mkMacro :: NiceDeclaration -> Nice NiceDeclaration 1234 mkMacro = \case 1235 FunSig r p a i _ rel tc cc x e -> return $ FunSig r p a i MacroDef rel tc cc x e 1236 d@FunDef{} -> return d 1237 d -> declarationException (BadMacroDef d) 1238 1239-- | Make a declaration abstract. 1240-- 1241-- Mark computation as 'dirty' if there was a declaration that could be made abstract. 1242-- If no abstraction is taking place, we want to complain about 'UselessAbstract'. 1243-- 1244-- Alternatively, we could only flag 'dirty' if a non-abstract thing was abstracted. 1245-- Then, nested @abstract@s would sometimes also be complained about. 1246 1247class MakeAbstract a where 1248 mkAbstract :: UpdaterT Nice a 1249 1250 default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => UpdaterT Nice a 1251 mkAbstract = traverse mkAbstract 1252 1253instance MakeAbstract a => MakeAbstract [a] 1254 1255-- Leads to overlap with 'WhereClause': 1256-- instance (Traversable f, MakeAbstract a) => MakeAbstract (f a) where 1257-- mkAbstract = traverse mkAbstract 1258 1259instance MakeAbstract IsAbstract where 1260 mkAbstract = \case 1261 a@AbstractDef -> return a 1262 ConcreteDef -> dirty $ AbstractDef 1263 1264instance MakeAbstract NiceDeclaration where 1265 mkAbstract = \case 1266 NiceMutual r termCheck cc pc ds -> NiceMutual r termCheck cc pc <$> mkAbstract ds 1267 NiceLoneConstructor r ds -> NiceLoneConstructor r <$> mkAbstract ds 1268 FunDef r ds a i tc cc x cs -> (\ a -> FunDef r ds a i tc cc x) <$> mkAbstract a <*> mkAbstract cs 1269 NiceDataDef r o a pc uc x ps cs -> (\ a -> NiceDataDef r o a pc uc x ps) <$> mkAbstract a <*> mkAbstract cs 1270 NiceRecDef r o a pc uc x dir ps cs -> (\ a -> NiceRecDef r o a pc uc x dir ps cs) <$> mkAbstract a 1271 NiceFunClause r p a tc cc catchall d -> (\ a -> NiceFunClause r p a tc cc catchall d) <$> mkAbstract a 1272 -- The following declarations have an @InAbstract@ field 1273 -- but are not really definitions, so we do count them into 1274 -- the declarations which can be made abstract 1275 -- (thus, do not notify progress with @dirty@). 1276 Axiom r p a i rel x e -> return $ Axiom r p AbstractDef i rel x e 1277 FunSig r p a i m rel tc cc x e -> return $ FunSig r p AbstractDef i m rel tc cc x e 1278 NiceRecSig r p a pc uc x ls t -> return $ NiceRecSig r p AbstractDef pc uc x ls t 1279 NiceDataSig r p a pc uc x ls t -> return $ NiceDataSig r p AbstractDef pc uc x ls t 1280 NiceField r p _ i tac x e -> return $ NiceField r p AbstractDef i tac x e 1281 PrimitiveFunction r p _ x e -> return $ PrimitiveFunction r p AbstractDef x e 1282 -- Andreas, 2016-07-17 it does have effect on unquoted defs. 1283 -- Need to set updater state to dirty! 1284 NiceUnquoteDecl r p _ i tc cc x e -> tellDirty $> NiceUnquoteDecl r p AbstractDef i tc cc x e 1285 NiceUnquoteDef r p _ tc cc x e -> tellDirty $> NiceUnquoteDef r p AbstractDef tc cc x e 1286 d@NiceModule{} -> return d 1287 d@NiceModuleMacro{} -> return d 1288 d@NicePragma{} -> return d 1289 d@(NiceOpen _ _ directives) -> do 1290 whenJust (publicOpen directives) $ lift . declarationWarning . OpenPublicAbstract 1291 return d 1292 d@NiceImport{} -> return d 1293 d@NicePatternSyn{} -> return d 1294 d@NiceGeneralize{} -> return d 1295 1296instance MakeAbstract Clause where 1297 mkAbstract (Clause x catchall lhs rhs wh with) = do 1298 Clause x catchall lhs rhs <$> mkAbstract wh <*> mkAbstract with 1299 1300-- | Contents of a @where@ clause are abstract if the parent is. 1301instance MakeAbstract WhereClause where 1302 mkAbstract NoWhere = return $ NoWhere 1303 mkAbstract (AnyWhere r ds) = dirty $ AnyWhere r [Abstract noRange ds] 1304 mkAbstract (SomeWhere r m a ds) = dirty $ SomeWhere r m a [Abstract noRange ds] 1305 1306-- | Make a declaration private. 1307-- 1308-- Andreas, 2012-11-17: 1309-- Mark computation as 'dirty' if there was a declaration that could be privatized. 1310-- If no privatization is taking place, we want to complain about 'UselessPrivate'. 1311-- 1312-- Alternatively, we could only flag 'dirty' if a non-private thing was privatized. 1313-- Then, nested @private@s would sometimes also be complained about. 1314 1315class MakePrivate a where 1316 mkPrivate :: Origin -> UpdaterT Nice a 1317 1318 default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => Origin -> UpdaterT Nice a 1319 mkPrivate o = traverse $ mkPrivate o 1320 1321instance MakePrivate a => MakePrivate [a] 1322 1323-- Leads to overlap with 'WhereClause': 1324-- instance (Traversable f, MakePrivate a) => MakePrivate (f a) where 1325-- mkPrivate = traverse mkPrivate 1326 1327instance MakePrivate Access where 1328 mkPrivate o = \case 1329 p@PrivateAccess{} -> return p -- OR? return $ PrivateAccess o 1330 _ -> dirty $ PrivateAccess o 1331 1332instance MakePrivate NiceDeclaration where 1333 mkPrivate o = \case 1334 Axiom r p a i rel x e -> (\ p -> Axiom r p a i rel x e) <$> mkPrivate o p 1335 NiceField r p a i tac x e -> (\ p -> NiceField r p a i tac x e) <$> mkPrivate o p 1336 PrimitiveFunction r p a x e -> (\ p -> PrimitiveFunction r p a x e) <$> mkPrivate o p 1337 NiceMutual r tc cc pc ds -> (\ ds-> NiceMutual r tc cc pc ds) <$> mkPrivate o ds 1338 NiceLoneConstructor r ds -> NiceLoneConstructor r <$> mkPrivate o ds 1339 NiceModule r p a x tel ds -> (\ p -> NiceModule r p a x tel ds) <$> mkPrivate o p 1340 NiceModuleMacro r p x ma op is -> (\ p -> NiceModuleMacro r p x ma op is) <$> mkPrivate o p 1341 FunSig r p a i m rel tc cc x e -> (\ p -> FunSig r p a i m rel tc cc x e) <$> mkPrivate o p 1342 NiceRecSig r p a pc uc x ls t -> (\ p -> NiceRecSig r p a pc uc x ls t) <$> mkPrivate o p 1343 NiceDataSig r p a pc uc x ls t -> (\ p -> NiceDataSig r p a pc uc x ls t) <$> mkPrivate o p 1344 NiceFunClause r p a tc cc catchall d -> (\ p -> NiceFunClause r p a tc cc catchall d) <$> mkPrivate o p 1345 NiceUnquoteDecl r p a i tc cc x e -> (\ p -> NiceUnquoteDecl r p a i tc cc x e) <$> mkPrivate o p 1346 NiceUnquoteDef r p a tc cc x e -> (\ p -> NiceUnquoteDef r p a tc cc x e) <$> mkPrivate o p 1347 NicePatternSyn r p x xs p' -> (\ p -> NicePatternSyn r p x xs p') <$> mkPrivate o p 1348 NiceGeneralize r p i tac x t -> (\ p -> NiceGeneralize r p i tac x t) <$> mkPrivate o p 1349 d@NicePragma{} -> return d 1350 d@(NiceOpen _ _ directives) -> do 1351 whenJust (publicOpen directives) $ lift . declarationWarning . OpenPublicPrivate 1352 return d 1353 d@NiceImport{} -> return d 1354 -- Andreas, 2016-07-08, issue #2089 1355 -- we need to propagate 'private' to the named where modules 1356 FunDef r ds a i tc cc x cls -> FunDef r ds a i tc cc x <$> mkPrivate o cls 1357 d@NiceDataDef{} -> return d 1358 d@NiceRecDef{} -> return d 1359 1360instance MakePrivate Clause where 1361 mkPrivate o (Clause x catchall lhs rhs wh with) = do 1362 Clause x catchall lhs rhs <$> mkPrivate o wh <*> mkPrivate o with 1363 1364instance MakePrivate WhereClause where 1365 mkPrivate o = \case 1366 d@NoWhere -> return d 1367 -- @where@-declarations are protected behind an anonymous module, 1368 -- thus, they are effectively private by default. 1369 d@AnyWhere{} -> return d 1370 -- Andreas, 2016-07-08 1371 -- A @where@-module is private if the parent function is private. 1372 -- The contents of this module are not private, unless declared so! 1373 -- Thus, we do not recurse into the @ds@ (could not anyway). 1374 SomeWhere r m a ds -> mkPrivate o a <&> \ a' -> SomeWhere r m a' ds 1375 1376-- The following function is (at the time of writing) only used three 1377-- times: for building Lets, and for printing error messages. 1378 1379-- | (Approximately) convert a 'NiceDeclaration' back to a list of 1380-- 'Declaration's. 1381notSoNiceDeclarations :: NiceDeclaration -> [Declaration] 1382notSoNiceDeclarations = \case 1383 Axiom _ _ _ i rel x e -> inst i [TypeSig rel Nothing x e] 1384 NiceField _ _ _ i tac x argt -> [FieldSig i tac x argt] 1385 PrimitiveFunction r _ _ x e -> [Primitive r [TypeSig (argInfo e) Nothing x (unArg e)]] 1386 NiceMutual r _ _ _ ds -> [Mutual r $ concatMap notSoNiceDeclarations ds] 1387 NiceLoneConstructor r ds -> [LoneConstructor r $ concatMap notSoNiceDeclarations ds] 1388 NiceModule r _ _ x tel ds -> [Module r x tel ds] 1389 NiceModuleMacro r _ x ma o dir -> [ModuleMacro r x ma o dir] 1390 NiceOpen r x dir -> [Open r x dir] 1391 NiceImport r x as o dir -> [Import r x as o dir] 1392 NicePragma _ p -> [Pragma p] 1393 NiceRecSig r _ _ _ _ x bs e -> [RecordSig r x bs e] 1394 NiceDataSig r _ _ _ _ x bs e -> [DataSig r x bs e] 1395 NiceFunClause _ _ _ _ _ _ d -> [d] 1396 FunSig _ _ _ i _ rel _ _ x e -> inst i [TypeSig rel Nothing x e] 1397 FunDef _ ds _ _ _ _ _ _ -> ds 1398 NiceDataDef r _ _ _ _ x bs cs -> [DataDef r x bs $ concatMap notSoNiceDeclarations cs] 1399 NiceRecDef r _ _ _ _ x dir bs ds -> [RecordDef r x dir bs ds] 1400 NicePatternSyn r _ n as p -> [PatternSyn r n as p] 1401 NiceGeneralize r _ i tac n e -> [Generalize r [TypeSig i tac n e]] 1402 NiceUnquoteDecl r _ _ i _ _ x e -> inst i [UnquoteDecl r x e] 1403 NiceUnquoteDef r _ _ _ _ x e -> [UnquoteDef r x e] 1404 where 1405 inst (InstanceDef r) ds = [InstanceB r ds] 1406 inst NotInstanceDef ds = ds 1407 1408-- | Has the 'NiceDeclaration' a field of type 'IsAbstract'? 1409niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract 1410niceHasAbstract = \case 1411 Axiom{} -> Nothing 1412 NiceField _ _ a _ _ _ _ -> Just a 1413 PrimitiveFunction _ _ a _ _ -> Just a 1414 NiceMutual{} -> Nothing 1415 NiceLoneConstructor{} -> Nothing 1416 NiceModule _ _ a _ _ _ -> Just a 1417 NiceModuleMacro{} -> Nothing 1418 NiceOpen{} -> Nothing 1419 NiceImport{} -> Nothing 1420 NicePragma{} -> Nothing 1421 NiceRecSig{} -> Nothing 1422 NiceDataSig{} -> Nothing 1423 NiceFunClause _ _ a _ _ _ _ -> Just a 1424 FunSig{} -> Nothing 1425 FunDef _ _ a _ _ _ _ _ -> Just a 1426 NiceDataDef _ _ a _ _ _ _ _ -> Just a 1427 NiceRecDef _ _ a _ _ _ _ _ _ -> Just a 1428 NicePatternSyn{} -> Nothing 1429 NiceGeneralize{} -> Nothing 1430 NiceUnquoteDecl _ _ a _ _ _ _ _ -> Just a 1431 NiceUnquoteDef _ _ a _ _ _ _ -> Just a 1432