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