{- |
Module: Agda.Unused

Check an Agda project for unused code.
-}
module Agda.Unused.Check
  ( checkUnused
  , checkUnusedGlobal
  , checkUnusedWith
  ) where

import Agda.Unused
  (Unused(..), UnusedItems(..), UnusedOptions(..))
import Agda.Unused.Monad.Error
  (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..),
    liftLookup)
import Agda.Unused.Monad.Reader
  (Environment(..), Mode(..), askGlobalMain, askIncludes, askLocal, askRoot,
    askSkip, localGlobal, localSkip)
import Agda.Unused.Monad.State
  (ModuleState(..), State, getModule, getSources, modifyBlock, modifyCheck,
    modifyDelete, modifyInsert, modifySources, stateEmpty, stateItems,
    stateModules)
import Agda.Unused.Types.Access
  (Access(..), fromAccess)
import Agda.Unused.Types.Context
  (AccessContext, AccessModule(..), Context, LookupError(..),
    accessContextConstructor, accessContextDefine, accessContextDefineFields,
    accessContextField, accessContextImport, accessContextItem,
    accessContextLookup, accessContextLookupDefining, accessContextLookupModule,
    accessContextLookupSpecial, accessContextMatch, accessContextModule,
    accessContextModule', accessContextPattern, accessContextRanges,
    accessContextUnion, contextDelete, contextDeleteModule, contextItem,
    contextLookupItem, contextLookupModule, contextModule, contextRanges,
    fromContext, moduleRanges, toContext)
import qualified Agda.Unused.Types.Context
  as C
import Agda.Unused.Types.Name
  (Name(..), QName(..), fromAsName, fromModuleName, fromName, fromNameRange,
    fromQName, fromQNameRange, nameIds, pathQName, qNamePath, toQName)
import Agda.Unused.Types.Range
  (RangeInfo(..), RangeType(..), rangePath)
import Agda.Unused.Utils
  (liftMaybe, mapLeft)

import Agda.Interaction.FindFile
  (findFile'', srcFilePath)
import Agda.Interaction.Options
  (CommandLineOptions(..), defaultOptions)
import Agda.Syntax.Common
  (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..),
    Named(..), Ranged(..), RecordDirectives'(..), Renaming'(..),
    RewriteEqn'(..), Using'(..), namedThing, unArg)
import qualified Agda.Syntax.Common
  as Common
import Agda.Syntax.Concrete
  (Binder, Binder'(..), BoundName(..), Declaration, DoStmt(..), Expr(..),
    FieldAssignment, FieldAssignment'(..), ImportDirective, ImportedName,
    LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module(..),
    ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..),
    RecordAssignment, RecordDirectives, Renaming, RewriteEqn, RHS, RHS'(..),
    TypedBinding, TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA,
    topLevelModuleName)
import Agda.Syntax.Concrete.Definitions
  (Clause(..), NiceConstructor, NiceDeclaration(..), niceDeclarations, runNice)
import Agda.Syntax.Concrete.Fixity
  (DoWarn(..), Fixities, fixitiesAndPolarities)
import Agda.Syntax.Concrete.Name
  (NameInScope(..), NamePart(..), nameRange, projectRoot, toTopLevelModuleName)
import qualified Agda.Syntax.Concrete.Name
  as N
import Agda.Syntax.Parser
  (moduleParser, parseFile, runPMIO)
import Agda.Syntax.Position
  (Range, Range'(..), getRange)
import Agda.TypeChecking.Monad.Base
  (TCM, runTCMTop)
import Agda.TypeChecking.Monad.Options
  (getIncludeDirs, setCommandLineOptions)
import Agda.Utils.FileName
  (filePath, mkAbsolute)
import qualified Agda.Utils.List2
  as List2
import Agda.Utils.List2
  (List2(..))
import Control.Monad
  (foldM, unless, void, when)
import Control.Monad.Except
  (ExceptT, MonadError, liftEither, runExceptT, throwError)
import Control.Monad.IO.Class
  (MonadIO, liftIO)
import Control.Monad.Reader
  (MonadReader, runReaderT)
import Control.Monad.State
  (MonadState, runStateT)
import Data.Bool
  (bool)
import Data.Foldable
  (traverse_)
import qualified Data.List.NonEmpty
  as NonEmpty
import Data.List.NonEmpty
  (NonEmpty(..), nonEmpty)
import qualified Data.Map.Strict
  as Map
import Data.Maybe
  (catMaybes)
import Data.Set
  (Set)
import qualified Data.Set
  as Set
import qualified Data.Text
  as T
import System.Directory
  (doesDirectoryExist, doesFileExist, listDirectory)
import System.FilePath
  ((</>))

-- ## Context

-- Do nothing if `askSkip` returns true.
contextInsertRangeAll
  :: MonadReader Environment m
  => Range
  -> Context
  -> m Context
contextInsertRangeAll :: forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r Context
c
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> a -> Bool -> a
bool (Range -> Context -> Context
C.contextInsertRangeAll Range
r Context
c) Context
c

-- Do nothing if `askSkip` returns true.
accessContextInsertRangeAll
  :: MonadReader Environment m
  => Range
  -> AccessContext
  -> m AccessContext
accessContextInsertRangeAll :: forall (m :: * -> *).
MonadReader Environment m =>
Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll Range
r AccessContext
c
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> a -> Bool -> a
bool (Range -> AccessContext -> AccessContext
C.accessContextInsertRangeAll Range
r AccessContext
c) AccessContext
c

-- ## Syntax

syntax
  :: Fixities
  -> Name
  -> Maybe Name
syntax :: Fixities -> Name -> Maybe Name
syntax Fixities
fs (Name NonEmpty NamePart
ps)
  = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Range -> NameInScope -> NonEmpty NamePart -> Name
N.Name forall a. Range' a
NoRange NameInScope
InScope NonEmpty NamePart
ps) Fixities
fs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fixity' -> Maybe Name
fromFixity

fromFixity
  :: Fixity'
  -> Maybe Name
fromFixity :: Fixity' -> Maybe Name
fromFixity (Fixity' Fixity
_ Notation
ps Range
_)
  = NonEmpty NamePart -> Name
Name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (GenPart -> NamePart
fromGenPart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notation
ps)

fromGenPart
  :: GenPart
  -> NamePart
fromGenPart :: GenPart -> NamePart
fromGenPart (BindHole Range
_ Ranged Int
_)
  = NamePart
Hole
fromGenPart (NormalHole Range
_ NamedArg (Ranged Int)
_)
  = NamePart
Hole
fromGenPart (WildHole Ranged Int
_)
  = NamePart
Hole
fromGenPart (IdPart (Ranged Range
_ FilePath
s))
  = FilePath -> NamePart
Id FilePath
s

-- ## Lists

checkSequence
  :: Monad m
  => Monoid c
  => (a -> b -> m c)
  -> a
  -> [b]
  -> m c
checkSequence :: forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence a -> b -> m c
f a
x [b]
ys
  = forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (a -> b -> m c
f a
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
ys)

checkSequence1
  :: Monad m
  => Monoid c
  => (a -> b -> m c)
  -> a
  -> NonEmpty b
  -> m c
checkSequence1 :: forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> NonEmpty b -> m c
checkSequence1 a -> b -> m c
f a
x NonEmpty b
ys
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence a -> b -> m c
f a
x (forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty b
ys)

checkFold
  :: Monad m
  => Monoid a
  => (a -> b -> m a)
  -> a
  -> [b]
  -> m a
checkFold :: forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold
  = forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith forall a. Monoid a => a
mempty forall a. Semigroup a => a -> a -> a
(<>)

checkFold1
  :: Monad m
  => Monoid a
  => (a -> b -> m a)
  -> a
  -> NonEmpty b
  -> m a
checkFold1 :: forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> NonEmpty b -> m a
checkFold1 a -> b -> m a
f a
x NonEmpty b
ys
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold a -> b -> m a
f a
x (forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty b
ys)

checkFoldUnion
  :: Monad m
  => (AccessContext -> b -> m AccessContext)
  -> AccessContext
  -> [b]
  -> m AccessContext
checkFoldUnion :: forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion
  = forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith forall a. Monoid a => a
mempty AccessContext -> AccessContext -> AccessContext
accessContextUnion

checkFoldWith
  :: Monad m
  => a
  -> (a -> a -> a)
  -> (a -> b -> m a)
  -> a
  -> [b]
  -> m a
checkFoldWith :: forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith a
x a -> a -> a
f a -> b -> m a
g a
x' [b]
ys
  = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\a
x'' b
y -> a -> a -> a
f a
x'' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m a
g (a -> a -> a
f a
x' a
x'') b
y) a
x [b]
ys

-- ## Names

checkName
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Fixities
  -> Access
  -> RangeType
  -> Range
  -> Name
  -> m AccessContext
checkName :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
_ Fixities
_ Access
_ RangeType
_ Range
NoRange Name
_
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkName Bool
_ Fixities
_ Access
_ RangeType
_ Range
_ (Name (NamePart
Hole :| []))
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkName Bool
p Fixities
fs Access
a RangeType
t r :: Range
r@(Range SrcFile
_ Seq IntervalWithoutFile
_) Name
n
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t (Name -> QName
QName Name
n))
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> a -> Bool -> a
bool Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextItem Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextPattern Bool
p Name
n Access
a (forall a. a -> Set a
Set.singleton Range
r)
    (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n))

checkName'
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Fixities
  -> Access
  -> RangeType
  -> N.Name
  -> m AccessContext
checkName' :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
p Fixities
fs Access
a RangeType
t Name
n
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
p Fixities
fs Access
a RangeType
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
n)

checkNames'
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Access
  -> RangeType
  -> [N.Name]
  -> m AccessContext
checkNames' :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' Bool
p Access
a
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
p forall a. Monoid a => a
mempty Access
a)

checkQNameP
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m AccessContext
checkQNameP :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m AccessContext
checkQNameP AccessContext
c Range
r QName
n
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
checkQNamePWith (QName -> AccessContext -> Maybe Bool
accessContextLookupSpecial QName
n AccessContext
c) AccessContext
c Range
r QName
n

checkQNamePWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Maybe Bool
  -> AccessContext
  -> Range
  -> QName
  -> m AccessContext
checkQNamePWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
checkQNamePWith Maybe Bool
Nothing AccessContext
_ Range
r QName
n
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Access -> RangeType -> Range -> QName -> m AccessContext
checkQName Access
Public RangeType
RangeVariable Range
r QName
n
checkQNamePWith (Just Bool
False) AccessContext
_ Range
_ QName
_
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkQNamePWith (Just Bool
True) AccessContext
c Range
r QName
n
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c Range
r QName
n forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

checkQNameP'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> N.QName
  -> m AccessContext
checkQNameP' :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m AccessContext
checkQNameP' AccessContext
c QName
n
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m AccessContext
checkQNameP AccessContext
c)) (QName -> Maybe (Range, QName)
fromQNameRange QName
n)

checkQName
  :: MonadReader Environment m
  => MonadState State m
  => Access
  -> RangeType
  -> Range
  -> QName
  -> m AccessContext
checkQName :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Access -> RangeType -> Range -> QName -> m AccessContext
checkQName Access
a RangeType
t Range
r (QName Name
n)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
False forall a. Monoid a => a
mempty Access
a RangeType
t Range
r Name
n
checkQName Access
_ RangeType
_ Range
_ (Qual Name
_ QName
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

checkModuleName
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> Access
  -> Range
  -> Name
  -> m AccessContext
checkModuleName :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c Access
a Range
r Name
n
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
RangeModule (Name -> QName
QName Name
n))
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r Context
c
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> AccessModule -> AccessContext
accessContextModule Name
n (Access -> Set Range -> Context -> AccessModule
AccessModule Access
a (forall a. a -> Set a
Set.singleton Range
r) Context
c'))

checkModuleNameMay
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> Access
  -> Range
  -> Maybe Name
  -- ^ If `Nothing`, the module is anonymous.
  -> m AccessContext
checkModuleNameMay :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
_ Access
_ Range
_ Maybe Name
Nothing
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkModuleNameMay Context
c Access
a Range
r (Just Name
n)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c Access
a Range
r Name
n

touchName
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Name
  -> m ()
touchName :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName AccessContext
c Name
n
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Either LookupError (Bool, Set Range) -> Bool -> m ()
touchNameWith (QName -> AccessContext -> Either LookupError (Bool, Set Range)
accessContextLookupDefining (Name -> QName
QName Name
n) AccessContext
c)

touchNameWith
  :: MonadReader Environment m
  => MonadState State m
  => Either LookupError (Bool, Set Range)
  -> Bool
  -> m ()
touchNameWith :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Either LookupError (Bool, Set Range) -> Bool -> m ()
touchNameWith (Right (Bool
False, Set Range
rs)) Bool
False
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
touchNameWith Either LookupError (Bool, Set Range)
_ Bool
_
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

touchNames
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> [Name]
  -> m ()
touchNames :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName

touchQName
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m ()
touchQName :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c Range
r QName
n
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Range
-> QName -> Either LookupError (Bool, Set Range) -> Bool -> m ()
touchQNameWith Range
r QName
n (QName -> AccessContext -> Either LookupError (Bool, Set Range)
accessContextLookupDefining QName
n AccessContext
c)

touchQNameWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Range
  -> QName
  -> Either LookupError (Bool, Set Range)
  -> Bool
  -> m ()
touchQNameWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Range
-> QName -> Either LookupError (Bool, Set Range) -> Bool -> m ()
touchQNameWith Range
r QName
n (Left LookupError
LookupAmbiguous) Bool
False
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorAmbiguous Range
r QName
n)
touchQNameWith Range
_ QName
_ Either LookupError (Bool, Set Range)
rs Bool
b
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Either LookupError (Bool, Set Range) -> Bool -> m ()
touchNameWith Either LookupError (Bool, Set Range)
rs Bool
b

touchQName'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> N.QName
  -> m ()
touchQName' :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m ()
touchQName' AccessContext
c QName
n
  = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c)) (QName -> Maybe (Range, QName)
fromQNameRange QName
n)

-- ## Bindings

checkBinder
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> Binder
  -> m AccessContext
checkBinder :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b AccessContext
c (Binder Maybe Pattern
p (BName Name
n Fixity'
_ TacticAttribute
_))
  = forall a. a -> a -> Bool -> a
bool forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip forall a. a -> a
id Bool
b (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay AccessContext
c Maybe Pattern
p
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkBinders1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> NonEmpty Binder
  -> m AccessContext
checkBinders1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty Binder -> m AccessContext
checkBinders1 Bool
b
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> NonEmpty b -> m c
checkSequence1 (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b)

checkLamBinding
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> LamBinding
  -> m AccessContext
checkLamBinding :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding Bool
b AccessContext
c (DomainFree (Arg ArgInfo
_ (Named Maybe NamedName
_ Binder
b')))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b AccessContext
c Binder
b'
checkLamBinding Bool
b AccessContext
c (DomainFull TypedBinding
b')
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b AccessContext
c TypedBinding
b'

checkLamBindings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [LamBinding]
  -> m AccessContext
checkLamBindings :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
b
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding Bool
b)

checkLamBindings1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> NonEmpty LamBinding
  -> m AccessContext
checkLamBindings1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty LamBinding -> m AccessContext
checkLamBindings1 Bool
b
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> NonEmpty b -> m a
checkFold1 (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding Bool
b)

checkTypedBinding
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> TypedBinding
  -> m AccessContext
checkTypedBinding :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b AccessContext
c (TBind Range
_ List1 (Arg (Named_ Binder))
bs Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty Binder -> m AccessContext
checkBinders1 Bool
b AccessContext
c (forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Arg (Named_ Binder))
bs)
checkTypedBinding Bool
_ AccessContext
c (TLet Range
_ List1 Declaration
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 Declaration -> m AccessContext
checkDeclarations1 AccessContext
c List1 Declaration
ds

checkTypedBindings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [TypedBinding]
  -> m AccessContext
checkTypedBindings :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
b
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b)

checkTypedBindings1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> NonEmpty TypedBinding
  -> m AccessContext
checkTypedBindings1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty TypedBinding -> m AccessContext
checkTypedBindings1 Bool
b
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> NonEmpty b -> m a
checkFold1 (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b)

-- ## Patterns
 
checkPattern
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Pattern
  -> m AccessContext
checkPattern :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c (IdentP QName
n)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m AccessContext
checkQNameP' AccessContext
c QName
n
checkPattern AccessContext
_ (QuoteP Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
c (RawAppP Range
_ List2 Pattern
ps)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkRawAppP AccessContext
c (forall l. IsList l => l -> [Item l]
List2.toList List2 Pattern
ps)
checkPattern AccessContext
_ (OpAppP Range
r QName
_ Set Name
_ [NamedArg Pattern]
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedOpAppP Range
r))
checkPattern AccessContext
c (HiddenP Range
_ (Named Maybe NamedName
_ Pattern
p))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern AccessContext
c (InstanceP Range
_ (Named Maybe NamedName
_ Pattern
p))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern AccessContext
c (ParenP Range
_ Pattern
p)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern AccessContext
_ (WildP Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (AbsurdP Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
c (DotP Range
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (LitP Range
_ Literal
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
c (RecP Range
_ [FieldAssignment' Pattern]
as)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c (forall a. FieldAssignment' a -> a
_exprFieldA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldAssignment' Pattern]
as)
checkPattern AccessContext
c (EqualP Range
_ [(Expr, Expr)]
es)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs AccessContext
c [(Expr, Expr)]
es forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (EllipsisP Range
_ Maybe Pattern
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPattern AccessContext
c (WithP Range
_ Pattern
p)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPattern AccessContext
c (AppP Pattern
p (Arg ArgInfo
_ (Named Maybe NamedName
_ Pattern
p')))
  = forall a. Semigroup a => a -> a -> a
(<>)
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p'

checkPattern AccessContext
c (AsP Range
_ Name
n Pattern
p)
  = forall a. Semigroup a => a -> a -> a
(<>)
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPatternMay
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Maybe Pattern
  -> m AccessContext
checkPatternMay :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay AccessContext
_ Maybe Pattern
Nothing
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkPatternMay AccessContext
c (Just Pattern
p)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPatterns
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Pattern]
  -> m AccessContext
checkPatterns :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern

checkRawAppP
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Pattern]
  -> m AccessContext
checkRawAppP :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkRawAppP AccessContext
c [Pattern]
ps
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FilePath] -> AccessContext -> [Name]
accessContextMatch ([Pattern] -> [FilePath]
patternNames [Pattern]
ps) AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[Name]
ns -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c [Name]
ns
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c ([Name] -> [Pattern] -> [Pattern]
patternDelete [Name]
ns [Pattern]
ps)

patternMatch
  :: [Name]
  -> Pattern
  -> Bool
patternMatch :: [Name] -> Pattern -> Bool
patternMatch [Name]
ns Pattern
p
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Name -> [FilePath]
nameIds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ns))) (Pattern -> Maybe FilePath
patternName Pattern
p)

patternDelete
  :: [Name]
  -> [Pattern]
  -> [Pattern]
patternDelete :: [Name] -> [Pattern] -> [Pattern]
patternDelete [Name]
ns
  = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Pattern -> Bool
patternMatch [Name]
ns)

patternName
  :: Pattern
  -> Maybe String
patternName :: Pattern -> Maybe FilePath
patternName (IdentP (N.QName (N.Name Range
_ NameInScope
_ (Id FilePath
n :| []))))
  = forall a. a -> Maybe a
Just FilePath
n
patternName Pattern
_
  = forall a. Maybe a
Nothing

patternNames
  :: [Pattern]
  -> [String]
patternNames :: [Pattern] -> [FilePath]
patternNames
  = forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Maybe FilePath
patternName

-- ## Expressions

checkExpr
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Expr
  -> m ()
checkExpr :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c (Ident QName
n)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m ()
touchQName' AccessContext
c QName
n
checkExpr AccessContext
_ (Lit Range
_ Literal
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (QuestionMark Range
_ Maybe Int
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (Underscore Range
_ Maybe FilePath
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (RawApp Range
_ List2 Expr
es)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkRawApp AccessContext
c (forall l. IsList l => l -> [Item l]
List2.toList List2 Expr
es)
checkExpr AccessContext
c (App Range
_ Expr
e (Arg ArgInfo
_ (Named Maybe NamedName
_ Expr
e')))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e'
checkExpr AccessContext
_ (OpApp Range
r QName
_ Set Name
_ OpAppArgs
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedOpApp Range
r))
checkExpr AccessContext
c (WithApp Range
_ Expr
e [Expr]
es)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
checkExpr AccessContext
c (HiddenArg Range
_ (Named Maybe NamedName
_ Expr
e))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
c (InstanceArg Range
_ (Named Maybe NamedName
_ Expr
e))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
c (Lam Range
_ NonEmpty LamBinding
bs Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty LamBinding -> m AccessContext
checkLamBindings1 Bool
True AccessContext
c NonEmpty LamBinding
bs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr AccessContext
_ (AbsurdLam Range
_ Hiding
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (ExtendedLam Range
_ Erased
_ List1 LamClause
ls)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 LamClause -> m ()
checkLamClauses1_ AccessContext
c List1 LamClause
ls
checkExpr AccessContext
c (Fun Range
_ (Arg ArgInfo
_ Expr
e) Expr
e')
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e'
checkExpr AccessContext
c (Pi NonEmpty TypedBinding
bs Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> NonEmpty TypedBinding -> m AccessContext
checkTypedBindings1 Bool
True AccessContext
c NonEmpty TypedBinding
bs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr AccessContext
c (Rec Range
_ RecordAssignments
rs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignments -> m ()
checkRecordAssignments AccessContext
c RecordAssignments
rs
checkExpr AccessContext
c (RecUpdate Range
_ Expr
e [FieldAssignment]
fs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [FieldAssignment] -> m ()
checkFieldAssignments AccessContext
c [FieldAssignment]
fs
checkExpr AccessContext
c (Paren Range
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
c (IdiomBrackets Range
_ [Expr]
es)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
checkExpr AccessContext
c (DoBlock Range
_ List1 DoStmt
ss)
  = forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 DoStmt -> m AccessContext
checkDoStmts1 AccessContext
c List1 DoStmt
ss)
checkExpr AccessContext
_ (Absurd Range
r)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedAbsurd Range
r))
checkExpr AccessContext
_ (As Range
r Name
_ Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedAs Range
r))
checkExpr AccessContext
c (Dot Range
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
c (DoubleDot Range
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
_ e :: Expr
e@(ETel [TypedBinding]
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedETel (forall a. HasRange a => a -> Range
getRange Expr
e)))
checkExpr AccessContext
_ (Quote Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (QuoteTerm Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (Tactic Range
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr AccessContext
_ (Unquote Range
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ e :: Expr
e@(DontCare Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedDontCare (forall a. HasRange a => a -> Range
getRange Expr
e)))
checkExpr AccessContext
_ (Equal Range
r Expr
_ Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedEqual Range
r))
checkExpr AccessContext
_ (Ellipsis Range
r)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedEllipsis Range
r))
checkExpr AccessContext
c (Generalized Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkExpr AccessContext
c (Let Range
_ List1 Declaration
ds TacticAttribute
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 Declaration -> m AccessContext
checkDeclarations1 AccessContext
c List1 Declaration
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c')) TacticAttribute
e

checkExprs
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Expr]
  -> m ()
checkExprs :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr

checkExprs1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> NonEmpty Expr
  -> m ()
checkExprs1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> NonEmpty Expr -> m ()
checkExprs1
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> NonEmpty b -> m c
checkSequence1 forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr

checkExprPair
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> (Expr, Expr)
  -> m ()
checkExprPair :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Expr, Expr) -> m ()
checkExprPair AccessContext
c (Expr
e1, Expr
e2)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e2

checkExprPairs
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [(Expr, Expr)]
  -> m ()
checkExprPairs :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Expr, Expr) -> m ()
checkExprPair

checkRawApp
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Expr]
  -> m ()
checkRawApp :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkRawApp AccessContext
c [Expr]
es
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c ([FilePath] -> AccessContext -> [Name]
accessContextMatch ([Expr] -> [FilePath]
exprNames [Expr]
es) AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es

exprName
  :: Expr
  -> Maybe String
exprName :: Expr -> Maybe FilePath
exprName (Ident (N.QName (N.Name Range
_ NameInScope
_ (Id FilePath
n :| []))))
  = forall a. a -> Maybe a
Just FilePath
n
exprName Expr
_
  = forall a. Maybe a
Nothing

exprNames
  :: [Expr]
  -> [String]
exprNames :: [Expr] -> [FilePath]
exprNames
  = forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Maybe FilePath
exprName

-- ## Assignments

checkRecordAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RecordAssignment
  -> m ()
checkRecordAssignment :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignment -> m ()
checkRecordAssignment AccessContext
c (Left FieldAssignment
f)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> FieldAssignment -> m ()
checkFieldAssignment AccessContext
c FieldAssignment
f
checkRecordAssignment AccessContext
c (Right ModuleAssignment
m)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> ModuleAssignment -> m ()
checkModuleAssignment AccessContext
c ModuleAssignment
m

checkRecordAssignments
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [RecordAssignment]
  -> m ()
checkRecordAssignments :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignments -> m ()
checkRecordAssignments
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignment -> m ()
checkRecordAssignment

checkFieldAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> FieldAssignment
  -> m ()
checkFieldAssignment :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> FieldAssignment -> m ()
checkFieldAssignment AccessContext
c (FieldAssignment Name
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkFieldAssignments
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [FieldAssignment]
  -> m ()
checkFieldAssignments :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [FieldAssignment] -> m ()
checkFieldAssignments
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> FieldAssignment -> m ()
checkFieldAssignment

checkModuleAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> ModuleAssignment
  -> m ()
checkModuleAssignment :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> ModuleAssignment -> m ()
checkModuleAssignment AccessContext
c a :: ModuleAssignment
a@(ModuleAssignment QName
n [Expr]
es ImportDirective
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchModule AccessContext
c (forall a. HasRange a => a -> Range
getRange ModuleAssignment
a)) (QName -> Maybe QName
fromQName QName
n)

-- ## Definitions

checkLHS
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LHS
  -> m AccessContext
checkLHS :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c (LHS Pattern
p [RewriteEqn]
rs [WithExpr]
ws)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [RewriteEqn] -> m AccessContext
checkRewriteEqns (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [RewriteEqn]
rs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') (forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [WithExpr]
ws)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkRHS
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RHS
  -> m ()
checkRHS :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS AccessContext
_ RHS
AbsurdRHS
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkRHS AccessContext
c (RHS Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Clause
  -> m AccessContext
checkClause :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Clause -> m AccessContext
checkClause AccessContext
c (Clause Name
n Bool
_ LHS
l RHS
r WhereClause
w [Clause]
cs)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id Name -> AccessContext -> AccessContext
accessContextDefine (Name -> Maybe Name
fromName Name
n) AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c' LHS
l
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') WhereClause
w
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(AccessContext
m, AccessContext
c''') -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') RHS
r
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') [Clause]
cs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
m' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
m forall a. Semigroup a => a -> a -> a
<> AccessContext
m')

checkClauses
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Clause]
  -> m AccessContext
checkClauses :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Clause -> m AccessContext
checkClause

checkLamClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LamClause
  -> m AccessContext
checkLamClause :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m AccessContext
checkLamClause AccessContext
c (LamClause [Pattern]
ps RHS
r Bool
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c [Pattern]
ps
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') RHS
r
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
c'

checkLamClause_
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LamClause
  -> m ()
checkLamClause_ :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m ()
checkLamClause_ AccessContext
c LamClause
ls
  = forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m AccessContext
checkLamClause AccessContext
c LamClause
ls)

checkLamClauses
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [LamClause]
  -> m AccessContext
checkLamClauses :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [LamClause] -> m AccessContext
checkLamClauses
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m AccessContext
checkLamClause

-- Do not propogate context from one clause to the next.
checkLamClauses1_
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> NonEmpty LamClause
  -> m ()
checkLamClauses1_ :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 LamClause -> m ()
checkLamClauses1_
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> NonEmpty b -> m c
checkSequence1 forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m ()
checkLamClause_

checkWhereClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> WhereClause
  -> m (AccessContext, AccessContext)
  -- ^ A context for the named where block, then the full context.
checkWhereClause :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause AccessContext
_ WhereClause
NoWhere
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty)
checkWhereClause AccessContext
c (AnyWhere Range
_ [Declaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, AccessContext
c')
checkWhereClause AccessContext
c (SomeWhere Range
_ Name
n Access
a [Declaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay (AccessContext -> Context
toContext AccessContext
c') (Access -> Access
fromAccess Access
a) (forall a. HasRange a => a -> Range
getRange Name
n)
    (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c'' , AccessContext
c')

checkRewriteEqn
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RewriteEqn
  -> m AccessContext
checkRewriteEqn :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RewriteEqn -> m AccessContext
checkRewriteEqn AccessContext
c (Rewrite List1 ((), Expr)
rs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> NonEmpty Expr -> m ()
checkExprs1 AccessContext
c (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 ((), Expr)
rs) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkRewriteEqn AccessContext
c (Invert ()
_ List1 (Named Name (Pattern, Expr))
ws)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> NonEmpty (Pattern, Expr) -> m AccessContext
checkIrrefutableWiths AccessContext
c (forall name a. Named name a -> a
namedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Named Name (Pattern, Expr))
ws)

checkRewriteEqns
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [RewriteEqn]
  -> m AccessContext
checkRewriteEqns :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [RewriteEqn] -> m AccessContext
checkRewriteEqns
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RewriteEqn -> m AccessContext
checkRewriteEqn

checkIrrefutableWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> (Pattern, Expr)
  -> m AccessContext
checkIrrefutableWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Pattern, Expr) -> m AccessContext
checkIrrefutableWith AccessContext
c (Pattern
p, Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkIrrefutableWiths
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> NonEmpty (Pattern, Expr)
  -> m AccessContext
checkIrrefutableWiths :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> NonEmpty (Pattern, Expr) -> m AccessContext
checkIrrefutableWiths
  = forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> NonEmpty b -> m a
checkFold1 forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Pattern, Expr) -> m AccessContext
checkIrrefutableWith

checkDoStmt
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> DoStmt
  -> m AccessContext
checkDoStmt :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> DoStmt -> m AccessContext
checkDoStmt AccessContext
c (DoBind Range
_ Pattern
p Expr
e [LamClause]
cs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [LamClause] -> m AccessContext
checkLamClauses AccessContext
c [LamClause]
cs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Pattern
p
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')
checkDoStmt AccessContext
c (DoThen Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkDoStmt AccessContext
c (DoLet Range
_ List1 Declaration
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 Declaration -> m AccessContext
checkDeclarations1 AccessContext
c List1 Declaration
ds

checkDoStmts1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> NonEmpty DoStmt
  -> m AccessContext
checkDoStmts1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 DoStmt -> m AccessContext
checkDoStmts1 AccessContext
c (DoStmt
s :| [DoStmt]
ss)
  = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoStmt -> [DoStmt] -> Bool
hasBind DoStmt
s [DoStmt]
ss) (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName AccessContext
c Name
bind)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoStmt -> [DoStmt] -> Bool
hasBind_ DoStmt
s [DoStmt]
ss) (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName AccessContext
c Name
bind_)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> DoStmt -> m AccessContext
checkDoStmt AccessContext
c (DoStmt
s forall a. a -> [a] -> [a]
: [DoStmt]
ss)

hasBind
  :: DoStmt
  -> [DoStmt]
  -> Bool
hasBind :: DoStmt -> [DoStmt] -> Bool
hasBind DoStmt
_ []
  = Bool
False
hasBind (DoBind Range
_ Pattern
_ Expr
_ [LamClause]
_) (DoStmt
_ : [DoStmt]
_)
  = Bool
True
hasBind DoStmt
_ (DoStmt
s : [DoStmt]
ss)
  = DoStmt -> [DoStmt] -> Bool
hasBind DoStmt
s [DoStmt]
ss

hasBind_
  :: DoStmt
  -> [DoStmt]
  -> Bool
hasBind_ :: DoStmt -> [DoStmt] -> Bool
hasBind_ DoStmt
_ []
  = Bool
False
hasBind_ (DoThen Expr
_) (DoStmt
_ : [DoStmt]
_)
  = Bool
True
hasBind_ DoStmt
_ (DoStmt
s : [DoStmt]
ss)
  = DoStmt -> [DoStmt] -> Bool
hasBind_ DoStmt
s [DoStmt]
ss

bind
  :: Name
bind :: Name
bind
  = NonEmpty NamePart -> Name
Name
  forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> NonEmpty a
(:|) NamePart
Hole
  forall a b. (a -> b) -> a -> b
$ (:) (FilePath -> NamePart
Id FilePath
">>=")
  forall a b. (a -> b) -> a -> b
$ (:) NamePart
Hole
  forall a b. (a -> b) -> a -> b
$ []

bind_
  :: Name
bind_ :: Name
bind_
  = NonEmpty NamePart -> Name
Name
  forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> NonEmpty a
(:|) NamePart
Hole
  forall a b. (a -> b) -> a -> b
$ (:) (FilePath -> NamePart
Id FilePath
">>")
  forall a b. (a -> b) -> a -> b
$ (:) NamePart
Hole
  forall a b. (a -> b) -> a -> b
$ []

-- ## Declarations

checkDeclarations
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarations :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations
  = forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations

checkDeclarations1
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> NonEmpty Declaration
  -> m AccessContext
checkDeclarations1 :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> List1 Declaration -> m AccessContext
checkDeclarations1 AccessContext
c List1 Declaration
ds
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c (forall a. NonEmpty a -> [a]
NonEmpty.toList List1 Declaration
ds)

checkDeclarationsRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> Set Range
  -- ^ Ranges associated with parent record.
  -> AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsRecord :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range -> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsRecord Name
n Set Range
rs
  = forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n Set Range
rs)

checkDeclarationsTop
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsTop :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop
  = forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop

checkDeclarationsWith
  :: MonadError Error m
  => (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
  -> AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsWith :: forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
f AccessContext
c [Declaration]
ds = do
  (Fixities
fixities, Polarities
_)
    <- forall (m :: * -> *).
MonadFixityError m =>
DoWarn -> [Declaration] -> m (Fixities, Polarities)
fixitiesAndPolarities DoWarn
NoWarn [Declaration]
ds
  (Either DeclarationException [NiceDeclaration]
niceDeclsEither, NiceWarnings
_) 
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Nice a -> (Either DeclarationException a, NiceWarnings)
runNice (Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations Fixities
fixities [Declaration]
ds))
  [NiceDeclaration]
niceDecls
    <- forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft DeclarationException -> Error
ErrorDeclaration Either DeclarationException [NiceDeclaration]
niceDeclsEither)
  Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
f Fixities
fixities AccessContext
c [NiceDeclaration]
niceDecls

checkNiceDeclaration
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext
checkNiceDeclaration :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askGlobalMain
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext -> NiceDeclaration -> Bool -> m AccessContext
checkNiceDeclarationWith Fixities
fs AccessContext
c NiceDeclaration
d

checkNiceDeclarationWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> NiceDeclaration
  -> Bool
  -> m AccessContext
checkNiceDeclarationWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext -> NiceDeclaration -> Bool -> m AccessContext
checkNiceDeclarationWith Fixities
fs AccessContext
c NiceDeclaration
d Bool
False
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration' Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationWith Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceImport Range
_ QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_) Bool
True
  = forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localGlobal (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration' Fixities
fs AccessContext
c NiceDeclaration
d)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> m ()
touchAccessContext AccessContext
c'
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
c'
checkNiceDeclarationWith Fixities
_ AccessContext
_ NiceDeclaration
d Bool
True
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> Error
ErrorGlobal (forall a. HasRange a => a -> Range
getRange NiceDeclaration
d))

checkNiceDeclaration'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext

checkNiceDeclaration' :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration' Fixities
fs AccessContext
c (Axiom Range
_ Access
a IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangePostulate Name
n
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceField Range
r Access
_ IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedField Range
r))
checkNiceDeclaration' Fixities
fs AccessContext
c (PrimitiveFunction Range
_ Access
a IsAbstract
_ Name
n (Arg ArgInfo
_ Expr
e))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangeDefinition Name
n
checkNiceDeclaration' Fixities
_ AccessContext
c (NiceModule Range
r Access
a IsAbstract
_ (N.QName Name
n) [TypedBinding]
bs [Declaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c (Access -> Access
fromAccess Access
a) Range
r (Name -> Maybe Name
fromName Name
n) [TypedBinding]
bs [Declaration]
ds
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceModule Range
_ Access
_ IsAbstract
_ n :: QName
n@(N.Qual Name
_ QName
_) [TypedBinding]
_ [Declaration]
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n)))
checkNiceDeclaration' Fixities
_ AccessContext
c (NiceModuleMacro Range
r Access
a Name
n ModuleApplication
m OpenShortHand
o ImportDirective
i)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> m AccessContext
checkNiceModuleMacro AccessContext
c (Access -> Access
fromAccess Access
a) Range
r Name
n ModuleApplication
m OpenShortHand
o ImportDirective
i
checkNiceDeclaration' Fixities
_ AccessContext
_ (NicePragma Range
_ Pragma
_)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceRecSig Range
_ Access
a IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
bs Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
RangeRecord Name
n [LamBinding]
bs Expr
e
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceDataSig Range
_ Access
a IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
bs Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
RangeData Name
n [LamBinding]
bs Expr
e
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceFunClause Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedNiceFunClause Range
r))
checkNiceDeclaration' Fixities
fs AccessContext
c (FunSig Range
_ Access
a IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
n Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangeDefinition Name
n
checkNiceDeclaration' Fixities
_ AccessContext
c (FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
cs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses AccessContext
c [Clause]
cs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
bs [NiceDeclaration]
cs)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
checkNiceDataDef Bool
True Fixities
fs AccessContext
c Name
n [LamBinding]
bs [NiceDeclaration]
cs
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceLoneConstructor Range
r [NiceDeclaration]
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedLoneConstructor Range
r)
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n RecordDirectives
rs [LamBinding]
bs [Declaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
True Fixities
fs AccessContext
c Name
n RecordDirectives
rs [LamBinding]
bs [Declaration]
ds
checkNiceDeclaration' Fixities
_ AccessContext
c (NiceGeneralize Range
_ Access
_ ArgInfo
_ TacticAttribute
_ Name
_ Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedUnquote Range
r)
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedUnquote Range
r)

checkNiceDeclaration' Fixities
fs AccessContext
c
  (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
_
    (d :: NiceDeclaration
d@(NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
_ Expr
_) : NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n' RecordDirectives
rs [LamBinding]
bs [Declaration]
ds : []))
  | Name -> Range
nameRange Name
n forall a. Eq a => a -> a -> Bool
== Name -> Range
nameRange Name
n'
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
False Fixities
fs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Name
n' RecordDirectives
rs [LamBinding]
bs [Declaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')
checkNiceDeclaration' Fixities
fs AccessContext
c
  (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
_
    (d :: NiceDeclaration
d@(NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
_ Expr
_) : NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n' [LamBinding]
bs [NiceDeclaration]
cs : []))
  | Name -> Range
nameRange Name
n forall a. Eq a => a -> a -> Bool
== Name -> Range
nameRange Name
n'
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
checkNiceDataDef Bool
False Fixities
fs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Name
n' [LamBinding]
bs [NiceDeclaration]
cs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')
checkNiceDeclaration' Fixities
fs AccessContext
c
  (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
_
    ds :: [NiceDeclaration]
ds@(FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
_ Expr
_ : FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_ : []))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceMutual Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r RangeInfo
RangeMutual
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
MonadReader Environment m =>
Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll Range
r AccessContext
c'

checkNiceDeclaration' Fixities
_ AccessContext
c (NiceOpen Range
r QName
n ImportDirective
i)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Open Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')

checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceImport Range
r QName
n Maybe AsName
Nothing OpenShortHand
DontOpen ImportDirective
i)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Context -> AccessContext
accessContextImport QName
n' Context
c'')
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceImport Range
r QName
n Maybe AsName
Nothing OpenShortHand
DoOpen ImportDirective
i)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Context -> AccessContext
accessContextImport QName
n' Context
c'
    forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceImport Range
r QName
n (Just AsName
a) OpenShortHand
DontOpen ImportDirective
i)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
c'' Access
Public (forall a. HasRange a => a -> Range
getRange AsName
a) (AsName -> Maybe Name
fromAsName AsName
a)
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceImport Range
r QName
n (Just AsName
a) OpenShortHand
DoOpen ImportDirective
i)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
c' Access
Public (forall a. HasRange a => a -> Range
getRange AsName
a) (AsName -> Maybe Name
fromAsName AsName
a)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c''' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c''' forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')

checkNiceDeclaration' Fixities
fs AccessContext
c (NicePatternSyn Range
_ Access
a Name
n [Arg Name]
ns Pattern
p)
  = forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' Bool
False Access
Public RangeType
RangeVariable (forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Name]
ns))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Pattern
p
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
True Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangePatternSynonym Name
n

checkNiceDeclarationRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> Set Range
  -- ^ Ranges associated with parent record.
  -> Fixities
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext
checkNiceDeclarationRecord :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
_ Expr
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(PrimitiveFunction Range
_ Access
_ IsAbstract
_ Name
_ Arg Expr
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
n Set Range
rs Fixities
fs AccessContext
c (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n Set Range
rs Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceModule Range
_ Access
_ IsAbstract
_ QName
_ [TypedBinding]
_ [Declaration]
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceModuleMacro Range
_ Access
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceImport Range
_ QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NicePragma Range
_ Pragma
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
rs Fixities
fs AccessContext
c d :: NiceDeclaration
d@(FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
_ Expr
_)
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
_ AccessContext
_ (NiceLoneConstructor Range
r [NiceDeclaration]
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedLoneConstructor Range
r)
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NicePatternSyn Range
_ Access
_ Name
_ [Arg Name]
_ Pattern
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceGeneralize Range
_ Access
_ ArgInfo
_ TacticAttribute
_ Name
_ Expr
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord Name
_ Set Range
_ Fixities
fs AccessContext
c d :: NiceDeclaration
d@(NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d

checkNiceDeclarationRecord Name
n Set Range
rs Fixities
fs AccessContext
c (NiceField Range
_ Access
a IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
n' (Arg ArgInfo
_ Expr
e))
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (Name -> AccessContext -> AccessContext
accessContextDefine Name
n (AccessContext -> AccessContext
accessContextDefineFields AccessContext
c)) Expr
e
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty)
    (\Name
n'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextField Name
n'' (Access -> Access
fromAccess Access
a) Set Range
rs (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n'')))
    (Name -> Maybe Name
fromName Name
n')

checkNiceDeclarations
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarations :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs
  = forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs)

checkNiceDeclarationsRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> Set Range
  -- ^ Ranges associated with parent record.
  -> Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarationsRecord :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n Set Range
rs Fixities
fs
  = forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
checkNiceDeclarationRecord Name
n Set Range
rs Fixities
fs)

checkNiceDeclarationsTop
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarationsTop :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop Fixities
_ AccessContext
_ []
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkNiceDeclarationsTop Fixities
_ AccessContext
c (NiceModule Range
r Access
a IsAbstract
_ QName
_ [TypedBinding]
bs [Declaration]
ds : [NiceDeclaration]
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c (Access -> Access
fromAccess Access
a) Range
r forall a. Maybe a
Nothing [TypedBinding]
bs [Declaration]
ds
checkNiceDeclarationsTop Fixities
fs AccessContext
c (NiceDeclaration
d : [NiceDeclaration]
ds)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop Fixities
fs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [NiceDeclaration]
ds

checkNiceSig
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> Common.Access
  -> RangeType
  -> N.Name
  -> [LamBinding]
  -> Expr
  -> m AccessContext
checkNiceSig :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
t Name
n [LamBinding]
bs Expr
e
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
False AccessContext
c [LamBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
t Name
n

checkNiceDataDef
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names in lambda bindings.
  -> Fixities
  -> AccessContext
  -> N.Name
  -> [LamBinding]
  -> [NiceConstructor]
  -> m AccessContext
checkNiceDataDef :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
checkNiceDataDef Bool
b Fixities
fs AccessContext
c Name
n [LamBinding]
bs [NiceDeclaration]
cs
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Monoid a => a
mempty forall a. a -> a
id (QName -> AccessContext -> Either LookupError (Set Range)
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Set Range
rs -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
b AccessContext
c [LamBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> Set Range
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceConstructors Fixities
fs Set Range
rs (Name -> AccessContext -> AccessContext
accessContextDefine Name
n' AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [NiceDeclaration]
cs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> AccessContext -> AccessContext
accessContextModule' Name
n' Access
Public Set Range
rs AccessContext
c'' forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkNiceRecordDef
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names in lambda bindings.
  -> Fixities
  -> AccessContext
  -> N.Name
  -> RecordDirectives
  -> [LamBinding]
  -> [Declaration]
  -> m AccessContext
checkNiceRecordDef :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
b Fixities
fs AccessContext
c Name
n (RecordDirectives Maybe (Ranged Induction)
_ Maybe HasEta0
_ Maybe Range
_ Maybe (Name, IsInstance)
m) [LamBinding]
bs [Declaration]
ds
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty) forall a. a -> a
id (QName -> AccessContext -> Either LookupError (Set Range)
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Set Range
rs' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
b AccessContext
c [LamBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> Set Range -> Maybe (Range, Name) -> m AccessContext
checkNiceConstructorRecordMay Fixities
fs Set Range
rs' (Maybe (Name, IsInstance)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe (Range, Name)
fromNameRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> Set Range -> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsRecord Name
n' Set Range
rs' (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c''' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> AccessContext -> AccessContext
accessContextModule' Name
n' Access
Public Set Range
rs' (AccessContext
c'' forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkNiceConstructor
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> Set Range
  -- ^ Ranges associated with parent type.
  -> AccessContext
  -> NiceConstructor
  -> m AccessContext
checkNiceConstructor :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> Set Range -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceConstructor Fixities
fs Set Range
rs AccessContext
c (Axiom Range
_ Access
a IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
e)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty)
    (\Name
n'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextConstructor Name
n'' (Access -> Access
fromAccess Access
a) Set Range
rs
      (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n'')))
    (Name -> Maybe Name
fromName Name
n)
checkNiceConstructor Fixities
_ Set Range
_ AccessContext
_ NiceDeclaration
d
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorConstructor (forall a. HasRange a => a -> Range
getRange NiceDeclaration
d)))

checkNiceConstructors
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> Set Range
  -- ^ Ranges associated with parent type.
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceConstructors :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> Set Range
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceConstructors Fixities
fs Set Range
rs
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> Set Range -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceConstructor Fixities
fs Set Range
rs)

checkNiceConstructorRecord
  :: MonadReader Environment m
  => MonadState State m
  => Fixities
  -> Set Range
  -- ^ Ranges associated with record type.
  -> Range
  -> Name
  -> m AccessContext
checkNiceConstructorRecord :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> Set Range -> Range -> Name -> m AccessContext
checkNiceConstructorRecord Fixities
fs Set Range
rs Range
r Name
n
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
RangeRecordConstructor (Name -> QName
QName Name
n))
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextConstructor Name
n Access
Public (forall a. Ord a => a -> Set a -> Set a
Set.insert Range
r Set Range
rs) (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n))

checkNiceConstructorRecordMay
  :: MonadReader Environment m
  => MonadState State m
  => Fixities
  -> Set Range
  -- ^ Ranges associated with record type.
  -> Maybe (Range, Name)
  -> m AccessContext
checkNiceConstructorRecordMay :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> Set Range -> Maybe (Range, Name) -> m AccessContext
checkNiceConstructorRecordMay Fixities
_ Set Range
_ Maybe (Range, Name)
Nothing
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
checkNiceConstructorRecordMay Fixities
fs Set Range
rs (Just (Range
r, Name
n))
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> Set Range -> Range -> Name -> m AccessContext
checkNiceConstructorRecord Fixities
fs Set Range
rs Range
r Name
n

checkNiceModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Access
  -> Range
  -> Maybe Name
  -- ^ If `Nothing`, the module is anonymous.
  -> [TypedBinding]
  -> [Declaration]
  -> m AccessContext
checkNiceModule :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c Access
a Range
r Maybe Name
n [TypedBinding]
bs [Declaration]
ds
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> Context
toContext AccessContext
c'')
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Access -> Context -> AccessContext
fromContext Access
a Context
c''')) (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' Access
a Range
r) Maybe Name
n

checkNiceModuleMacro
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Access
  -> Range
  -> N.Name
  -> ModuleApplication
  -> OpenShortHand
  -> ImportDirective
  -> m AccessContext
checkNiceModuleMacro :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> m AccessContext
checkNiceModuleMacro AccessContext
c Access
a Range
_ Name
a' (SectionApp Range
r [TypedBinding]
bs Expr
e) OpenShortHand
o ImportDirective
i
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Name
-> [TypedBinding]
-> Maybe (QName, [Expr])
-> OpenShortHand
-> ImportDirective
-> m AccessContext
checkSectionApp AccessContext
c Access
a Range
r Name
a' [TypedBinding]
bs (Expr -> Maybe (QName, [Expr])
parseSectionApp Expr
e) OpenShortHand
o ImportDirective
i
checkNiceModuleMacro AccessContext
_ Access
_ Range
r Name
_ (RecordModuleInstance Range
_ QName
_) OpenShortHand
_ ImportDirective
_
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedMacro Range
r)

checkSectionApp
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Access
  -> Range
  -> N.Name
  -> [TypedBinding]
  -> Maybe (N.QName, [Expr])
  -> OpenShortHand
  -> ImportDirective
  -> m AccessContext
checkSectionApp :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Name
-> [TypedBinding]
-> Maybe (QName, [Expr])
-> OpenShortHand
-> ImportDirective
-> m AccessContext
checkSectionApp AccessContext
_ Access
_ Range
r Name
_ [TypedBinding]
_ Maybe (QName, [Expr])
Nothing OpenShortHand
_ ImportDirective
_
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorMacro Range
r))
checkSectionApp AccessContext
c Access
_ Range
r (N.NoName Range
_ NameId
_) [] (Just (QName
n, [Expr]
es)) OpenShortHand
DoOpen ImportDirective
i
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Open Range
r QName
n' Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i)
checkSectionApp AccessContext
c Access
a Range
r Name
a' [TypedBinding]
bs (Just (QName
n, [Expr]
es)) OpenShortHand
DontOpen ImportDirective
i
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
a'))) (Name -> Maybe Name
fromName Name
a')
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
a'' -> forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Module Range
r (Name -> QName
QName Name
a'') Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' Access
a Range
r Name
a''
checkSectionApp AccessContext
c Access
a Range
r Name
a' [TypedBinding]
bs (Just (QName
n, [Expr]
es)) OpenShortHand
DoOpen ImportDirective
i
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
a'))) (Name -> Maybe Name
fromName Name
a')
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
a'' -> forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Module Range
r (Name -> QName
QName Name
a'') Context
c' ImportDirective
i
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' Access
a Range
r Name
a''
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'''' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c'''' forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c''')

parseSectionApp
  :: Expr
  -> Maybe (N.QName, [Expr])
parseSectionApp :: Expr -> Maybe (QName, [Expr])
parseSectionApp (Ident QName
n)
  = forall a. a -> Maybe a
Just (QName
n, [])
parseSectionApp (RawApp Range
_ (List2 (Ident QName
n) Expr
e [Expr]
es))
  = forall a. a -> Maybe a
Just (QName
n, (Expr
e forall a. a -> [a] -> [a]
: [Expr]
es))
parseSectionApp Expr
_
  = forall a. Maybe a
Nothing

-- ## Imports

data DirectiveType where

  Import
    :: DirectiveType

  Module
    :: DirectiveType

  Open
    :: DirectiveType

  deriving Int -> DirectiveType -> ShowS
[DirectiveType] -> ShowS
DirectiveType -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [DirectiveType] -> ShowS
$cshowList :: [DirectiveType] -> ShowS
show :: DirectiveType -> FilePath
$cshow :: DirectiveType -> FilePath
showsPrec :: Int -> DirectiveType -> ShowS
$cshowsPrec :: Int -> DirectiveType -> ShowS
Show

directiveStatement
  :: DirectiveType
  -> Maybe RangeType
directiveStatement :: DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
Import
  = forall a. a -> Maybe a
Just RangeType
RangeImport
directiveStatement DirectiveType
Module
  = forall a. Maybe a
Nothing
directiveStatement DirectiveType
Open
  = forall a. a -> Maybe a
Just RangeType
RangeOpen

directiveItem
  :: DirectiveType
  -> RangeType
directiveItem :: DirectiveType -> RangeType
directiveItem DirectiveType
Import
  = RangeType
RangeImportItem
directiveItem DirectiveType
Module
  = RangeType
RangeModuleItem
directiveItem DirectiveType
Open
  = RangeType
RangeOpenItem

checkImportDirective
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Range
  -> QName
  -> Context
  -> ImportDirective
  -> m Context
checkImportDirective :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
dt Range
r QName
n Context
c (ImportDirective Range
_ Using' Name Name
UseEverything [ImportedName]
hs RenamingDirective' Name Name
rs Maybe Range
_)
  = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\RangeType
t -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t QName
n)) (DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
dt)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
MonadError Error m =>
Context -> [ImportedName] -> m Context
modifyHidings Context
c ([ImportedName]
hs forall a. Semigroup a => a -> a -> a
<> (forall n m. Renaming' n m -> ImportedName' n m
renFrom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RenamingDirective' Name Name
rs))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> RenamingDirective' Name Name -> m Context
checkRenamings DirectiveType
dt Context
c RenamingDirective' Name Name
rs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r (Context
c' forall a. Semigroup a => a -> a -> a
<> Context
c'')
checkImportDirective DirectiveType
dt Range
r QName
n Context
c (ImportDirective Range
_ (Using [ImportedName]
ns) [ImportedName]
_ RenamingDirective' Name Name
rs Maybe Range
_)
  = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\RangeType
t -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t QName
n)) (DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
dt)
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [ImportedName] -> m Context
checkImportedNames DirectiveType
dt Context
c [ImportedName]
ns
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> RenamingDirective' Name Name -> m Context
checkRenamings DirectiveType
dt Context
c RenamingDirective' Name Name
rs
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r (Context
c' forall a. Semigroup a => a -> a -> a
<> Context
c'')

checkRenaming
  :: MonadReader Environment m
  => MonadState State m
  => MonadError Error m
  => DirectiveType
  -> Context
  -> Renaming
  -> m Context
checkRenaming :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m,
 MonadError Error m) =>
DirectiveType -> Context -> Renaming -> m Context
checkRenaming DirectiveType
dt Context
c r :: Renaming
r@(Renaming ImportedName
n ImportedName
t Maybe Fixity
_ Range
_)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> (Range, ImportedName, ImportedName) -> m Context
checkImportedNamePair DirectiveType
dt Context
c (forall a. HasRange a => a -> Range
getRange Renaming
r, ImportedName
n, ImportedName
t)

checkRenamings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> [Renaming]
  -> m Context
checkRenamings :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> RenamingDirective' Name Name -> m Context
checkRenamings DirectiveType
dt
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m,
 MonadError Error m) =>
DirectiveType -> Context -> Renaming -> m Context
checkRenaming DirectiveType
dt)

checkImportedName
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> ImportedName
  -> m Context
checkImportedName :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> ImportedName -> m Context
checkImportedName DirectiveType
dt Context
c ImportedName
n
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> (Range, ImportedName, ImportedName) -> m Context
checkImportedNamePair DirectiveType
dt Context
c (forall a. HasRange a => a -> Range
getRange ImportedName
n, ImportedName
n, ImportedName
n)

checkImportedNamePair
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> (Range, ImportedName, ImportedName)
  -> m Context
checkImportedNamePair :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context -> (Range, ImportedName, ImportedName) -> m Context
checkImportedNamePair DirectiveType
dt Context
c (Range
_, ImportedName Name
n, ImportedName Name
t)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
t)))
    (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Range
r, Name
t') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (Name -> Item -> Context
contextItem Name
t') (QName -> Context -> Maybe Item
contextLookupItem (Name -> QName
QName Name
n') Context
c)
    forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair DirectiveType
dt Context
c (Range
_, ImportedModule Name
n, ImportedModule Name
t)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
t)))
    (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Range
r, Name
t') -> forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair DirectiveType
_ Context
_ (Range
r, ImportedName
_, ImportedName
_)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorRenaming Range
r))

checkImportedNames
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> [ImportedName]
  -> m Context
checkImportedNames :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [ImportedName] -> m Context
checkImportedNames DirectiveType
dt
  = forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> ImportedName -> m Context
checkImportedName DirectiveType
dt)

modifyHiding
  :: MonadError Error m
  => Context
  -> ImportedName
  -> m Context
modifyHiding :: forall (m :: * -> *).
MonadError Error m =>
Context -> ImportedName -> m Context
modifyHiding Context
c (ImportedName Name
n)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Context
contextDelete Context
c
modifyHiding Context
c (ImportedModule Name
n)
  = forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (forall a. HasRange a => a -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Context
contextDeleteModule Context
c

modifyHidings
  :: MonadError Error m
  => Context
  -> [ImportedName]
  -> m Context
modifyHidings :: forall (m :: * -> *).
MonadError Error m =>
Context -> [ImportedName] -> m Context
modifyHidings
  = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *).
MonadError Error m =>
Context -> ImportedName -> m Context
modifyHiding

touchModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m ()
touchModule :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchModule AccessContext
c Range
r QName
n
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Either LookupError Module -> Range -> QName -> m ()
touchModuleWith (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n AccessContext
c) Range
r QName
n

touchModuleWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Either LookupError C.Module
  -> Range
  -> QName
  -> m ()
touchModuleWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Either LookupError Module -> Range -> QName -> m ()
touchModuleWith (Left LookupError
LookupNotFound) Range
_ QName
_
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
touchModuleWith (Left LookupError
LookupAmbiguous) Range
r QName
n
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorAmbiguous Range
r QName
n)
touchModuleWith (Right Module
m) Range
_ QName
_
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete (Module -> Set Range
moduleRanges Module
m)

touchContext
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> m ()
touchContext :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> m ()
touchContext Context
c
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete (Context -> Set Range
contextRanges Context
c)

touchAccessContext
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> m ()
touchAccessContext :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> m ()
touchAccessContext AccessContext
c
  = forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete (AccessContext -> Set Range
accessContextRanges AccessContext
c)

importDirectiveAccess
  :: ImportDirective
  -> Access
importDirectiveAccess :: ImportDirective -> Access
importDirectiveAccess (ImportDirective Range
_ Using' Name Name
_ [ImportedName]
_ RenamingDirective' Name Name
_ Maybe Range
Nothing)
  = Access
Private
importDirectiveAccess (ImportDirective Range
_ Using' Name Name
_ [ImportedName]
_ RenamingDirective' Name Name
_ (Just Range
_))
  = Access
Public

-- ## Modules

checkModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => QName
  -> Module
  -> m Context
checkModule :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> Module -> m Context
checkModule QName
n (Mod [Pragma]
_ [Declaration]
ds) = do
  Bool
local
    <- forall (m :: * -> *). MonadReader Environment m => m Bool
askLocal
  ()
_
    <- forall (m :: * -> *). MonadState State m => QName -> m ()
modifyBlock QName
n
  Context
context
    <- AccessContext -> Context
toContext forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop forall a. Monoid a => a
mempty [Declaration]
ds
  ()
_
    <- forall (m :: * -> *).
MonadState State m =>
QName -> Context -> m ()
modifyCheck QName
n Context
context
  ()
_
    <- forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
local (forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> m ()
touchContext Context
context)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
context

-- ## Files

checkFile
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Range
  -> QName
  -> m Context
checkFile :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n
  = forall (m :: * -> *).
MonadState State m =>
QName -> m (Maybe ModuleState)
getModule QName
n
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> Maybe ModuleState -> m Context
checkFileWith Range
r QName
n

checkFileWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Range
  -> QName
  -> Maybe ModuleState
  -> m Context
checkFileWith :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> Maybe ModuleState -> m Context
checkFileWith Range
r QName
n Maybe ModuleState
Nothing
  = forall (m :: * -> *). MonadReader Environment m => m FilePath
askRoot
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \FilePath
p -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath
p FilePath -> ShowS
</> QName -> FilePath
qNamePath QName
n)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \FilePath
p' -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO Bool
doesFileExist FilePath
p')
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b -> forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> Maybe FilePath -> m Context
checkFileWith' Range
r QName
n (forall a. a -> a -> Bool -> a
bool forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just FilePath
p') Bool
b)
checkFileWith Range
r QName
n (Just ModuleState
Blocked)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorCyclic Range
r QName
n)
checkFileWith Range
_ QName
_ (Just (Checked Context
c))
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
c

checkFileWith'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Range
  -> QName
  -> Maybe FilePath
  -> m Context
checkFileWith' :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> Maybe FilePath -> m Context
checkFileWith' Range
r QName
n Maybe FilePath
Nothing
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFileExternal Range
r QName
n
checkFileWith' Range
_ QName
n (Just FilePath
p)
  = forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> FilePath -> m Context
checkFilePath QName
n FilePath
p

checkFileExternal
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Range
  -> QName
  -> m Context
checkFileExternal :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFileExternal Range
r QName
n = do
  [AbsolutePath]
includes
    <- forall (m :: * -> *). MonadReader Environment m => m [AbsolutePath]
askIncludes
  ModuleToSource
sources
    <- forall (m :: * -> *). MonadState State m => m ModuleToSource
getSources
  (Either FindError SourceFile
pathEither, ModuleToSource
sources') 
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
includes (QName -> TopLevelModuleName
toTopLevelModuleName (QName -> QName
toQName QName
n)) ModuleToSource
sources)
  SourceFile
path
    <- forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft (Range -> QName -> FindError -> Error
ErrorFind Range
r QName
n) Either FindError SourceFile
pathEither)
  ()
_
    <- forall (m :: * -> *). MonadState State m => ModuleToSource -> m ()
modifySources ModuleToSource
sources'
  Context
context
    <- forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> FilePath -> m Context
checkFilePath QName
n (AbsolutePath -> FilePath
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
path)))
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
context

checkFilePath
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => QName
  -> FilePath
  -> m Context
checkFilePath :: forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> FilePath -> m Context
checkFilePath QName
n FilePath
p
  = forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
FilePath -> m Module
readModule FilePath
p
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> Module -> m Context
checkModule QName
n

checkFileTop
  :: MonadError Error m
  => MonadIO m
  => Mode
  -> UnusedOptions
  -> FilePath
  -- ^ The file to check.
  -> m (FilePath, State)
  -- ^ The project root, along with the final state.
checkFileTop :: forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
Mode -> UnusedOptions -> FilePath -> m (FilePath, State)
checkFileTop Mode
m UnusedOptions
opts FilePath
p = do
  Module
module'
    <- forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
FilePath -> m Module
readModule FilePath
p
  TopLevelModuleName
moduleName
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module -> TopLevelModuleName
topLevelModuleName Module
module')
  QName
moduleQName
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (TopLevelModuleName -> QName
fromModuleName TopLevelModuleName
moduleName)
  AbsolutePath
absolutePath
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot (FilePath -> AbsolutePath
mkAbsolute FilePath
p) TopLevelModuleName
moduleName)
  FilePath
rootPath
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath -> FilePath
filePath AbsolutePath
absolutePath)
  Either TCErr [AbsolutePath]
includesEither
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. TCM a -> IO (Either TCErr a)
runTCMTop (UnusedOptions -> TCM ()
setOptions UnusedOptions
opts forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs))
  [AbsolutePath]
includes
    <- forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft (forall a b. a -> b -> a
const Error
ErrorInclude) Either TCErr [AbsolutePath]
includesEither)
  Environment
env
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (Mode -> FilePath -> [AbsolutePath] -> Environment
Environment Mode
m FilePath
rootPath [AbsolutePath]
includes)
  (Context
_, State
state)
    <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> Module -> m Context
checkModule QName
moduleQName Module
module') Environment
env) State
stateEmpty
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath
rootPath, State
state)

readModule
  :: MonadError Error m
  => MonadIO m
  => FilePath
  -> m Module
readModule :: forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
FilePath -> m Module
readModule FilePath
p = do
  Bool
exists
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO Bool
doesFileExist FilePath
p)
  ()
_
    <- forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (FilePath -> Error
ErrorFile FilePath
p))
  AbsolutePath
absolutePath
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath -> AbsolutePath
mkAbsolute FilePath
p)
  FilePath
contents
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO FilePath
readFile FilePath
p)
  (Either ParseError (Module, FileType)
parseResult, [ParseWarning]
_)
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO (forall a.
Show a =>
Parser a -> AbsolutePath -> FilePath -> PM (a, FileType)
parseFile Parser Module
moduleParser AbsolutePath
absolutePath FilePath
contents))
  (Module
module', FileType
_)
    <- forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft ParseError -> Error
ErrorParse Either ParseError (Module, FileType)
parseResult)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Module
module'

-- ## Paths

-- Look for unvisited modules.
checkPath
  :: Set QName
  -- ^ Visited modules.
  -> FilePath
  -- ^ A path to ignore.
  -> FilePath
  -- ^ The project root path.
  -> IO [FilePath]
checkPath :: Set QName -> FilePath -> FilePath -> IO [FilePath]
checkPath Set QName
ns FilePath
i FilePath
r
  = forall a. Set a -> [a]
Set.toAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set QName -> FilePath -> FilePath -> FilePath -> IO (Set FilePath)
checkPath' Set QName
ns FilePath
i FilePath
r FilePath
r

-- Look for unvisited modules at the given path.
checkPath'
  :: Set QName
  -- ^ Visited modules.
  -> FilePath
  -- ^ A path to ignore.
  -> FilePath
  -- ^ The project root path.
  -> FilePath
  -- ^ The path at which to look.
  -> IO (Set FilePath)
checkPath' :: Set QName -> FilePath -> FilePath -> FilePath -> IO (Set FilePath)
checkPath' Set QName
ns FilePath
i FilePath
r FilePath
p
  = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO Bool
doesDirectoryExist FilePath
p)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. a -> a -> Bool -> a
bool (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set QName -> FilePath -> FilePath -> FilePath -> Set FilePath
checkPathFile Set QName
ns FilePath
i FilePath
r FilePath
p)) (Set QName -> FilePath -> FilePath -> FilePath -> IO (Set FilePath)
checkPathDirectory Set QName
ns FilePath
i FilePath
r FilePath
p)

checkPathFile
  :: Set QName
  -- ^ Visited modules.
  -> FilePath
  -- ^ A path to ignore.
  -> FilePath
  -- ^ The project root path.
  -> FilePath
  -- ^ The path at which to look.
  -> Set FilePath
checkPathFile :: Set QName -> FilePath -> FilePath -> FilePath -> Set FilePath
checkPathFile Set QName
_ FilePath
i FilePath
_ FilePath
p | FilePath
i forall a. Eq a => a -> a -> Bool
== FilePath
p
  = forall a. Monoid a => a
mempty
checkPathFile Set QName
ns FilePath
_ FilePath
r FilePath
p
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (forall a. a -> a -> Bool -> a
bool (forall a. a -> Set a
Set.singleton FilePath
p) forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Set a -> Bool
Set.member Set QName
ns)
  forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> Maybe QName
pathQName FilePath
r FilePath
p

checkPathDirectory
  :: Set QName
  -- ^ Visited modules.
  -> FilePath
  -- ^ A path to ignore.
  -> FilePath
  -- ^ The project root path.
  -> FilePath
  -- ^ The path at which to look.
  -> IO (Set FilePath)
checkPathDirectory :: Set QName -> FilePath -> FilePath -> FilePath -> IO (Set FilePath)
checkPathDirectory Set QName
ns FilePath
i FilePath
r FilePath
p
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath
p FilePath -> ShowS
</>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO [FilePath]
listDirectory FilePath
p)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Set QName -> FilePath -> FilePath -> FilePath -> IO (Set FilePath)
checkPath' Set QName
ns FilePath
i FilePath
r)
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat

-- ## Main

-- | Check an Agda file and its dependencies for unused code, excluding public
-- items that could be imported elsewhere.
checkUnused
  :: UnusedOptions
  -- ^ Options to use.
  -> FilePath
  -- ^ Absolute path of the file to check.
  -> IO (Either Error UnusedItems)
checkUnused :: UnusedOptions -> FilePath -> IO (Either Error UnusedItems)
checkUnused
  = Mode -> UnusedOptions -> FilePath -> IO (Either Error UnusedItems)
checkUnusedWith Mode
Local

-- | Check an Agda file and its dependencies for unused code, using the
-- specified check mode.
checkUnusedWith
  :: Mode
  -- ^ The check mode to use.
  -> UnusedOptions
  -- ^ Options to use.
  -> FilePath
  -- ^ Absolute path of the file to check.
  -> IO (Either Error UnusedItems)
checkUnusedWith :: Mode -> UnusedOptions -> FilePath -> IO (Either Error UnusedItems)
checkUnusedWith Mode
m UnusedOptions
opts
  = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Range, RangeInfo)] -> UnusedItems
UnusedItems forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> [(Range, RangeInfo)]
stateItems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
Mode -> UnusedOptions -> FilePath -> m (FilePath, State)
checkFileTop Mode
m UnusedOptions
opts

-- | Check an Agda file and its dependencies for unused code, including public
-- items in dependencies, as well as files.
--
-- The given file should consist only of import statements; it serves as a
-- full description of the public interface of the project.
checkUnusedGlobal
  :: UnusedOptions
  -- ^ Options to use.
  -> FilePath
  -- ^ Absolute path of the file to check.
  -> IO (Either Error Unused)
checkUnusedGlobal :: UnusedOptions -> FilePath -> IO (Either Error Unused)
checkUnusedGlobal UnusedOptions
opts FilePath
p
  = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (UnusedOptions -> FilePath -> ExceptT Error IO Unused
checkUnusedGlobal' UnusedOptions
opts FilePath
p)

checkUnusedGlobal'
  :: UnusedOptions
  -> FilePath
  -> ExceptT Error IO Unused
checkUnusedGlobal' :: UnusedOptions -> FilePath -> ExceptT Error IO Unused
checkUnusedGlobal' UnusedOptions
opts FilePath
p = do
  (FilePath
rootPath, State
state)
    <- forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
Mode -> UnusedOptions -> FilePath -> m (FilePath, State)
checkFileTop Mode
GlobalMain UnusedOptions
opts FilePath
p
  [FilePath]
files
    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Set QName -> FilePath -> FilePath -> IO [FilePath]
checkPath (State -> Set QName
stateModules State
state) FilePath
p FilePath
rootPath)
  UnusedItems
items 
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Range, RangeInfo)] -> UnusedItems
UnusedItems (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> (Range, RangeInfo) -> Bool
inFile FilePath
p) (State -> [(Range, RangeInfo)]
stateItems State
state)))
  Unused
unused
    <- forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FilePath] -> UnusedItems -> Unused
Unused [FilePath]
files UnusedItems
items)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Unused
unused

setOptions
  :: UnusedOptions
  -> TCM ()
setOptions :: UnusedOptions -> TCM ()
setOptions UnusedOptions
opts
  = CommandLineOptions -> TCM ()
setCommandLineOptions
  forall a b. (a -> b) -> a -> b
$ CommandLineOptions
defaultOptions
  { optIncludePaths :: [FilePath]
optIncludePaths
    = UnusedOptions -> [FilePath]
unusedOptionsInclude UnusedOptions
opts
  , optLibraries :: [FilePath]
optLibraries
    = Text -> FilePath
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnusedOptions -> [Text]
unusedOptionsLibraries UnusedOptions
opts
  , optOverrideLibrariesFile :: Maybe FilePath
optOverrideLibrariesFile
    = UnusedOptions -> Maybe FilePath
unusedOptionsLibrariesFile UnusedOptions
opts
  , optDefaultLibs :: Bool
optDefaultLibs
    = UnusedOptions -> Bool
unusedOptionsUseDefaultLibraries UnusedOptions
opts
  , optUseLibs :: Bool
optUseLibs
    = UnusedOptions -> Bool
unusedOptionsUseLibraries UnusedOptions
opts
  }

inFile
  :: FilePath
  -> (Range, RangeInfo)
  -> Bool
inFile :: FilePath -> (Range, RangeInfo) -> Bool
inFile FilePath
p (Range
r, RangeInfo
_)
  = Range -> Maybe FilePath
rangePath Range
r forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just FilePath
p