{- |
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
  (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'(..),
    IsInstance, Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..),
    Using'(..), namedThing, unArg, whThing)
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, 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, getRange)
import Agda.TypeChecking.Monad.Base
  (TCM, getIncludeDirs, runTCMTop)
import Agda.TypeChecking.Monad.Options
  (setCommandLineOptions)
import Agda.Utils.FileName
  (filePath, mkAbsolute)
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.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 :: Range -> Context -> m Context
contextInsertRangeAll Range
r Context
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Bool -> Context) -> Bool -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context -> Bool -> Context
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 :: Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll Range
r AccessContext
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> m AccessContext)
-> (Bool -> AccessContext) -> Bool -> m AccessContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AccessContext -> AccessContext -> Bool -> AccessContext
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 [NamePart]
ps)
  = Name -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Range -> NameInScope -> [NamePart] -> Name
N.Name Range
forall a. Range' a
NoRange NameInScope
InScope [NamePart]
ps) Fixities
fs Maybe Fixity' -> (Fixity' -> Maybe Name) -> Maybe Name
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
_ [] Range
_)
  = Maybe Name
forall a. Maybe a
Nothing
fromFixity (Fixity' Fixity
_ ps :: [GenPart]
ps@(GenPart
_ : [GenPart]
_) Range
_)
  = Name -> Maybe Name
forall a. a -> Maybe a
Just ([NamePart] -> Name
Name (GenPart -> NamePart
fromGenPart (GenPart -> NamePart) -> [GenPart] -> [NamePart]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GenPart]
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
_ RawName
s))
  = RawName -> NamePart
Id RawName
s

-- ## Lists

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

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

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

checkFoldUnion
  :: Monad m
  => (AccessContext -> b -> m AccessContext)
  -> AccessContext
  -> [b]
  -> m AccessContext
checkFoldUnion :: (AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion
  = AccessContext
-> (AccessContext -> AccessContext -> AccessContext)
-> (AccessContext -> b -> m AccessContext)
-> AccessContext
-> [b]
-> m AccessContext
forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith AccessContext
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 :: 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
  = (a -> b -> m a) -> a -> [b] -> m a
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'' (a -> a) -> m a -> m a
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 :: Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
_ Fixities
_ Access
_ RangeType
_ Range
NoRange Name
_
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkName Bool
_ Fixities
_ Access
_ RangeType
_ Range
_ (Name [NamePart
Hole])
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkName Bool
p Fixities
fs Access
a RangeType
t r :: Range
r@(Range SrcFile
_ Seq IntervalWithoutFile
_) Name
n
  = Range -> RangeInfo -> m ()
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))
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Name -> Access -> Set Range -> Maybe Name -> AccessContext)
-> (Name -> Access -> Set Range -> Maybe Name -> AccessContext)
-> Bool
-> Name
-> Access
-> Set Range
-> Maybe Name
-> AccessContext
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 (Range -> Set Range
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' :: Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
p Fixities
fs Access
a RangeType
t Name
n
  = m AccessContext
-> ((Range, Name) -> m AccessContext)
-> Maybe (Range, Name)
-> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty) ((Range -> Name -> m AccessContext)
-> (Range, Name) -> m AccessContext
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
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' :: Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' Bool
p Access
a
  = (RangeType -> Name -> m AccessContext)
-> RangeType -> [Name] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
p Fixities
forall a. Monoid a => a
mempty Access
a)

checkQNameP
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m AccessContext
checkQNameP :: AccessContext -> Range -> QName -> m AccessContext
checkQNameP AccessContext
c Range
r QName
n
  = Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
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 :: Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
checkQNamePWith Maybe Bool
Nothing AccessContext
_ Range
r QName
n
  = Access -> RangeType -> Range -> QName -> m AccessContext
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
_
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkQNamePWith (Just Bool
True) AccessContext
c Range
r QName
n
  = AccessContext -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c Range
r QName
n m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty

checkQNameP'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> N.QName
  -> m AccessContext
checkQNameP' :: AccessContext -> QName -> m AccessContext
checkQNameP' AccessContext
c QName
n
  = m AccessContext
-> ((Range, QName) -> m AccessContext)
-> Maybe (Range, QName)
-> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty) ((Range -> QName -> m AccessContext)
-> (Range, QName) -> m AccessContext
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AccessContext -> Range -> QName -> m AccessContext
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 :: Access -> RangeType -> Range -> QName -> m AccessContext
checkQName Access
a RangeType
t Range
r (QName Name
n)
  = Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
False Fixities
forall a. Monoid a => a
mempty Access
a RangeType
t Range
r Name
n
checkQName Access
_ RangeType
_ Range
_ (Qual Name
_ QName
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty

checkModuleName
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> Access
  -> Range
  -> Name
  -> m AccessContext
checkModuleName :: Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c Access
a Range
r Name
n
  = Range -> RangeInfo -> m ()
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))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r Context
c
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> AccessModule -> AccessContext
accessContextModule Name
n (Access -> Set Range -> Context -> AccessModule
AccessModule Access
a (Range -> Set Range
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 :: Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
_ Access
_ Range
_ Maybe Name
Nothing
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkModuleNameMay Context
c Access
a Range
r (Just Name
n)
  = Context -> Access -> Range -> Name -> m AccessContext
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 :: AccessContext -> Name -> m ()
touchName AccessContext
c Name
n
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either LookupError (Bool, Set Range) -> Bool -> m ()
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 :: Either LookupError (Bool, Set Range) -> Bool -> m ()
touchNameWith (Right (Bool
False, Set Range
rs)) Bool
False
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
touchNameWith Either LookupError (Bool, Set Range)
_ Bool
_
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

touchNames
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> [Name]
  -> m ()
touchNames :: AccessContext -> [Name] -> m ()
touchNames
  = (AccessContext -> Name -> m ()) -> AccessContext -> [Name] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> Name -> m ()
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 :: AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c Range
r QName
n
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range
-> QName -> Either LookupError (Bool, Set Range) -> Bool -> m ()
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 :: Range
-> QName -> Either LookupError (Bool, Set Range) -> Bool -> m ()
touchQNameWith Range
r QName
n (Left LookupError
LookupAmbiguous) Bool
False
  = Error -> m ()
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
  = Either LookupError (Bool, Set Range) -> Bool -> m ()
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' :: AccessContext -> QName -> m ()
touchQName' AccessContext
c QName
n
  = ((Range, QName) -> m ()) -> Maybe (Range, QName) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Range -> QName -> m ()) -> (Range, QName) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AccessContext -> Range -> QName -> m ()
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 :: Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b AccessContext
c (Binder Maybe Pattern
p (BName Name
n Fixity'
_ TacticAttribute
_))
  = (m AccessContext -> m AccessContext)
-> (m AccessContext -> m AccessContext)
-> Bool
-> m AccessContext
-> m AccessContext
forall a. a -> a -> Bool -> a
bool m AccessContext -> m AccessContext
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip m AccessContext -> m AccessContext
forall a. a -> a
id Bool
b (Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> Maybe Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay AccessContext
c Maybe Pattern
p
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkBinders
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [Binder]
  -> m AccessContext
checkBinders :: Bool -> AccessContext -> [Binder] -> m AccessContext
checkBinders Bool
b
  = (AccessContext -> Binder -> m AccessContext)
-> AccessContext -> [Binder] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Bool -> AccessContext -> Binder -> m AccessContext
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 :: Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding Bool
b AccessContext
c (DomainFree (Arg ArgInfo
_ (Named Maybe NamedName
_ Binder
b')))
  = Bool -> AccessContext -> Binder -> m AccessContext
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')
  = Bool -> AccessContext -> TypedBinding -> m AccessContext
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 :: Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
b
  = (AccessContext -> LamBinding -> m AccessContext)
-> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (Bool -> AccessContext -> LamBinding -> m AccessContext
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 :: Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b AccessContext
c (TBind Range
_ [Arg (Named_ Binder)]
bs Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [Binder] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [Binder] -> m AccessContext
checkBinders Bool
b AccessContext
c (Named_ Binder -> Binder
forall name a. Named name a -> a
namedThing (Named_ Binder -> Binder)
-> (Arg (Named_ Binder) -> Named_ Binder)
-> Arg (Named_ Binder)
-> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Binder) -> Named_ Binder
forall e. Arg e -> e
unArg (Arg (Named_ Binder) -> Binder)
-> [Arg (Named_ Binder)] -> [Binder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg (Named_ Binder)]
bs)
checkTypedBinding Bool
_ AccessContext
c (TLet Range
_ [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [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 :: Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
b
  = (AccessContext -> TypedBinding -> m AccessContext)
-> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (Bool -> AccessContext -> TypedBinding -> m AccessContext
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 :: AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c (IdentP QName
n)
  = AccessContext -> QName -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m AccessContext
checkQNameP' AccessContext
c QName
n
checkPattern AccessContext
_ (QuoteP Range
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
c (RawAppP Range
_ [Pattern]
ps)
  = AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkRawAppP AccessContext
c [Pattern]
ps
checkPattern AccessContext
_ (OpAppP Range
r QName
_ Set Name
_ [NamedArg Pattern]
_)
  = Error -> m AccessContext
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))
  = AccessContext -> Pattern -> m AccessContext
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))
  = AccessContext -> Pattern -> m AccessContext
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)
  = AccessContext -> Pattern -> m AccessContext
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
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (AbsurdP Range
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
c (DotP Range
_ Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (LitP Literal
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
c (RecP Range
_ [FieldAssignment' Pattern]
as)
  = AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c (FieldAssignment' Pattern -> Pattern
forall a. FieldAssignment' a -> a
_exprFieldA (FieldAssignment' Pattern -> Pattern)
-> [FieldAssignment' Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldAssignment' Pattern]
as)
checkPattern AccessContext
c (EqualP Range
_ [(Expr, Expr)]
es)
  = AccessContext -> [(Expr, Expr)] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs AccessContext
c [(Expr, Expr)]
es m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
_ (EllipsisP Range
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern AccessContext
c (WithP Range
_ Pattern
p)
  = AccessContext -> Pattern -> m AccessContext
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')))
  = AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
(<>)
  (AccessContext -> AccessContext -> AccessContext)
-> m AccessContext -> m (AccessContext -> AccessContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  m (AccessContext -> AccessContext)
-> m AccessContext -> m AccessContext
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AccessContext -> Pattern -> m AccessContext
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)
  = AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
(<>)
  (AccessContext -> AccessContext -> AccessContext)
-> m AccessContext -> m (AccessContext -> AccessContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n
  m (AccessContext -> AccessContext)
-> m AccessContext -> m AccessContext
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AccessContext -> Pattern -> m AccessContext
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 :: AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay AccessContext
_ Maybe Pattern
Nothing
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPatternMay AccessContext
c (Just Pattern
p)
  = AccessContext -> Pattern -> m AccessContext
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 :: AccessContext -> [Pattern] -> m AccessContext
checkPatterns
  = (AccessContext -> Pattern -> m AccessContext)
-> AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence AccessContext -> Pattern -> m AccessContext
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 :: AccessContext -> [Pattern] -> m AccessContext
checkRawAppP AccessContext
c [Pattern]
ps
  = [Name] -> m [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([RawName] -> AccessContext -> [Name]
accessContextMatch ([Pattern] -> [RawName]
patternNames [Pattern]
ps) AccessContext
c)
  m [Name] -> ([Name] -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[Name]
ns -> AccessContext -> [Name] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c [Name]
ns
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Pattern] -> m AccessContext
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
  = Bool -> (RawName -> Bool) -> Maybe RawName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((RawName -> [RawName] -> Bool) -> [RawName] -> RawName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip RawName -> [RawName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ([[RawName]] -> [RawName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Name -> [RawName]
nameIds (Name -> [RawName]) -> [Name] -> [[RawName]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ns))) (Pattern -> Maybe RawName
patternName Pattern
p)

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

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

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

-- ## Expressions

checkExpr
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Expr
  -> m ()
checkExpr :: AccessContext -> Expr -> m ()
checkExpr AccessContext
c (Ident QName
n)
  = AccessContext -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m ()
touchQName' AccessContext
c QName
n
checkExpr AccessContext
_ (Lit Literal
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (QuestionMark Range
_ Maybe Int
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (Underscore Range
_ Maybe RawName
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (RawApp Range
_ [Expr]
es)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkRawApp AccessContext
c [Expr]
es
checkExpr AccessContext
c (App Range
_ Expr
e (Arg ArgInfo
_ (Named Maybe NamedName
_ Expr
e')))
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
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
_ [NamedArg (MaybePlaceholder (OpApp Expr))]
_)
  = Error -> m ()
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)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
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))
  = AccessContext -> Expr -> m ()
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))
  = AccessContext -> Expr -> m ()
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
_ [LamBinding]
bs Expr
e)
  = Bool -> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
True AccessContext
c [LamBinding]
bs m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr AccessContext
_ (AbsurdLam Range
_ Hiding
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (ExtendedLam Range
_ [LamClause]
ls)
  = AccessContext -> [LamClause] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [LamClause] -> m ()
checkLamClauses_ AccessContext
c [LamClause]
ls
checkExpr AccessContext
c (Fun Range
_ (Arg ArgInfo
_ Expr
e) Expr
e')
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
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 [TypedBinding]
bs Expr
e)
  = Bool -> AccessContext -> [TypedBinding] -> m AccessContext
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 m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr AccessContext
_ (Set Range
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (Prop Range
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (SetN Range
_ Integer
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (PropN Range
_ Integer
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (Rec Range
_ RecordAssignments
rs)
  = AccessContext -> RecordAssignments -> m ()
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)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [FieldAssignment] -> m ()
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)
  = AccessContext -> Expr -> m ()
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)
  = AccessContext -> [Expr] -> m ()
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
_ [DoStmt]
ss)
  = m AccessContext -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (AccessContext -> [DoStmt] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [DoStmt] -> m AccessContext
checkDoStmts AccessContext
c [DoStmt]
ss)
checkExpr AccessContext
_ (Absurd Range
r)
  = Error -> m ()
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
_)
  = Error -> m ()
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)
  = AccessContext -> Expr -> m ()
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)
  = AccessContext -> Expr -> m ()
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]
_)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedETel (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e)))
checkExpr AccessContext
_ (Quote Range
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ (QuoteTerm Range
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
c (Tactic Range
_ Expr
e)
  = AccessContext -> Expr -> m ()
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
_)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr AccessContext
_ e :: Expr
e@(DontCare Expr
_)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (UnexpectedError -> Range -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedDontCare (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e)))
checkExpr AccessContext
_ (Equal Range
r Expr
_ Expr
_)
  = Error -> m ()
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)
  = Error -> m ()
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)
  = AccessContext -> Expr -> m ()
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
_ [Declaration]
ds TacticAttribute
e)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> (Expr -> m ()) -> TacticAttribute -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
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 :: AccessContext -> [Expr] -> m ()
checkExprs
  = (AccessContext -> Expr -> m ()) -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> Expr -> m ()
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 :: AccessContext -> (Expr, Expr) -> m ()
checkExprPair AccessContext
c (Expr
e1, Expr
e2)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e1 m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
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 :: AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs
  = (AccessContext -> (Expr, Expr) -> m ())
-> AccessContext -> [(Expr, Expr)] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> (Expr, Expr) -> m ()
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 :: AccessContext -> [Expr] -> m ()
checkRawApp AccessContext
c [Expr]
es
  = AccessContext -> [Name] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c ([RawName] -> AccessContext -> [Name]
accessContextMatch ([Expr] -> [RawName]
exprNames [Expr]
es) AccessContext
c)
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
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 RawName
exprName (Ident (N.QName (N.Name Range
_ NameInScope
_ [Id RawName
n])))
  = RawName -> Maybe RawName
forall a. a -> Maybe a
Just RawName
n
exprName Expr
_
  = Maybe RawName
forall a. Maybe a
Nothing

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

-- ## Assignments

checkRecordAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RecordAssignment
  -> m ()
checkRecordAssignment :: AccessContext -> RecordAssignment -> m ()
checkRecordAssignment AccessContext
c (Left FieldAssignment
f)
  = AccessContext -> FieldAssignment -> m ()
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)
  = AccessContext -> 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 :: AccessContext -> RecordAssignments -> m ()
checkRecordAssignments
  = (AccessContext -> RecordAssignment -> m ())
-> AccessContext -> RecordAssignments -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> RecordAssignment -> m ()
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 :: AccessContext -> FieldAssignment -> m ()
checkFieldAssignment AccessContext
c (FieldAssignment Name
_ Expr
e)
  = AccessContext -> Expr -> m ()
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 :: AccessContext -> [FieldAssignment] -> m ()
checkFieldAssignments
  = (AccessContext -> FieldAssignment -> m ())
-> AccessContext -> [FieldAssignment] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> FieldAssignment -> m ()
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 :: AccessContext -> ModuleAssignment -> m ()
checkModuleAssignment AccessContext
c a :: ModuleAssignment
a@(ModuleAssignment QName
n [Expr]
es ImportDirective
_)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (QName -> m ()) -> Maybe QName -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (AccessContext -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchModule AccessContext
c (ModuleAssignment -> Range
forall t. HasRange t => t -> 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 :: AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c (LHS Pattern
p [RewriteEqn]
rs [WithHiding Expr]
ws ExpandedEllipsis
_)
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> [RewriteEqn] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [RewriteEqn] -> m AccessContext
checkRewriteEqns (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [RewriteEqn]
rs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') (WithHiding Expr -> Expr
forall a. WithHiding a -> a
whThing (WithHiding Expr -> Expr) -> [WithHiding Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [WithHiding Expr]
ws)
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
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 :: AccessContext -> RHS -> m ()
checkRHS AccessContext
_ RHS
AbsurdRHS
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkRHS AccessContext
c (RHS Expr
e)
  = AccessContext -> Expr -> m ()
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 :: AccessContext -> Clause -> m AccessContext
checkClause AccessContext
c (Clause Name
n Bool
_ LHS
l RHS
r WhereClause
w [Clause]
cs)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((AccessContext -> AccessContext)
-> (Name -> AccessContext -> AccessContext)
-> Maybe Name
-> AccessContext
-> AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe AccessContext -> AccessContext
forall a. a -> a
id Name -> AccessContext -> AccessContext
accessContextDefine (Name -> Maybe Name
fromName Name
n) AccessContext
c)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> LHS -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c' LHS
l
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> WhereClause -> m (AccessContext, AccessContext)
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') WhereClause
w
  m (AccessContext, AccessContext)
-> ((AccessContext, AccessContext) -> m AccessContext)
-> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(AccessContext
m, AccessContext
c''') -> AccessContext -> RHS -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') RHS
r
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') [Clause]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
m' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
m AccessContext -> AccessContext -> AccessContext
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 :: AccessContext -> [Clause] -> m AccessContext
checkClauses
  = (AccessContext -> Clause -> m AccessContext)
-> AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence AccessContext -> Clause -> m AccessContext
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 :: AccessContext -> LamClause -> m AccessContext
checkLamClause AccessContext
c (LamClause LHS
l RHS
r WhereClause
_ Bool
_)
  = AccessContext -> LHS -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c LHS
l
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> RHS -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') RHS
r
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
c'

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

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

-- Do not propogate context from one clause to the next.
checkLamClauses_
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [LamClause]
  -> m ()
checkLamClauses_ :: AccessContext -> [LamClause] -> m ()
checkLamClauses_
  = (AccessContext -> LamClause -> m ())
-> AccessContext -> [LamClause] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> LamClause -> m ()
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 :: AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause AccessContext
_ WhereClause
NoWhere
  = (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
forall a. Monoid a => a
mempty, AccessContext
forall a. Monoid a => a
mempty)
checkWhereClause AccessContext
c (AnyWhere [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
forall a. Monoid a => a
mempty, AccessContext
c')
checkWhereClause AccessContext
c (SomeWhere Name
n Access
a [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Context -> Access -> Range -> Maybe Name -> m AccessContext
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) (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)
    (Name -> Maybe Name
fromName Name
n)
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
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 :: AccessContext -> RewriteEqn -> m AccessContext
checkRewriteEqn AccessContext
c (Rewrite [((), Expr)]
rs)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c (((), Expr) -> Expr
forall a b. (a, b) -> b
snd (((), Expr) -> Expr) -> [((), Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((), Expr)]
rs) m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkRewriteEqn AccessContext
c (Invert ()
_ [(Pattern, Expr)]
ws)
  = AccessContext -> [(Pattern, Expr)] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Pattern, Expr)] -> m AccessContext
checkIrrefutableWiths AccessContext
c [(Pattern, Expr)]
ws

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

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

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

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

bind
  :: Name
bind :: Name
bind
  = [NamePart] -> Name
Name
  [ NamePart
Hole
  , RawName -> NamePart
Id RawName
">>="
  , NamePart
Hole
  ]

bind_
  :: Name
bind_ :: Name
bind_
  = [NamePart] -> Name
Name
  [ NamePart
Hole
  , RawName -> NamePart
Id RawName
">>"
  , NamePart
Hole
  ]

-- ## Declarations

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

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 :: Name
-> Set Range -> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsRecord Name
n Set Range
rs
  = (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith (Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
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 :: AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop
  = (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
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 :: (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
f AccessContext
c [Declaration]
ds = do
  (Fixities
fixities, Polarities
_)
    <- DoWarn -> [Declaration] -> m (Fixities, Polarities)
forall (m :: * -> *).
MonadFixityError m =>
DoWarn -> [Declaration] -> m (Fixities, Polarities)
fixitiesAndPolarities DoWarn
NoWarn [Declaration]
ds
  (Either DeclarationException [NiceDeclaration]
niceDeclsEither, NiceWarnings
_) 
    <- (Either DeclarationException [NiceDeclaration], NiceWarnings)
-> m (Either DeclarationException [NiceDeclaration], NiceWarnings)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nice [NiceDeclaration]
-> (Either DeclarationException [NiceDeclaration], NiceWarnings)
forall a. Nice a -> (Either DeclarationException a, NiceWarnings)
runNice (Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations Fixities
fixities [Declaration]
ds))
  [NiceDeclaration]
niceDecls
    <- Either Error [NiceDeclaration] -> m [NiceDeclaration]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((DeclarationException -> Error)
-> Either DeclarationException [NiceDeclaration]
-> Either Error [NiceDeclaration]
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 :: Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askGlobalMain
  m Bool -> (Bool -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fixities
-> AccessContext -> NiceDeclaration -> Bool -> m AccessContext
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 :: Fixities
-> AccessContext -> NiceDeclaration -> Bool -> m AccessContext
checkNiceDeclarationWith Fixities
fs AccessContext
c NiceDeclaration
d Bool
False
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
  = m AccessContext -> m AccessContext
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localGlobal (Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> m ()
touchAccessContext AccessContext
c'
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
c'
checkNiceDeclarationWith Fixities
_ AccessContext
_ NiceDeclaration
d Bool
True
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> Error
ErrorGlobal (NiceDeclaration -> Range
forall t. HasRange t => t -> Range
getRange NiceDeclaration
d))

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

checkNiceDeclaration' :: Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration' Fixities
fs AccessContext
c (Axiom Range
_ Access
a IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
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
_)
  = Error -> m AccessContext
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 Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
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)
  = AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
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]
_)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)))
checkNiceDeclaration' Fixities
_ AccessContext
_ (NicePragma Range
_ Pragma
_)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceRecSig Range
_ Access
a IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
bs Expr
e)
  = Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
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)
  = Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
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
_)
  = Error -> m AccessContext
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)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
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)
  = AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses AccessContext
c [Clause]
cs m AccessContext -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
fs AccessContext
c (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
bs [NiceDeclaration]
cs)
  = Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
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
fs AccessContext
c (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n Maybe (Ranged Induction)
_ Maybe HasEta
_ Maybe (Name, IsInstance)
m [LamBinding]
bs [Declaration]
ds)
  = Bool
-> Fixities
-> AccessContext
-> Name
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
True Fixities
fs AccessContext
c Name
n Maybe (Name, IsInstance)
m [LamBinding]
bs [Declaration]
ds
checkNiceDeclaration' Fixities
_ AccessContext
c (NiceGeneralize Range
_ Access
_ ArgInfo
_ TacticAttribute
_ Name
_ Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration' Fixities
_ AccessContext
_ (NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)
  = Error -> m AccessContext
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
_)
  = Error -> m AccessContext
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' Maybe (Ranged Induction)
_ Maybe HasEta
_ Maybe (Name, IsInstance)
m [LamBinding]
bs [Declaration]
ds : []))
  | Name -> Range
nameRange Name
n Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
nameRange Name
n'
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Bool
-> Fixities
-> AccessContext
-> Name
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool
-> Fixities
-> AccessContext
-> Name
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
False Fixities
fs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Name
n' Maybe (Name, IsInstance)
m [LamBinding]
bs [Declaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
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 Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
nameRange Name
n'
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
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 AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Name
n' [LamBinding]
bs [NiceDeclaration]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
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]
_ : []))
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
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)
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r RangeInfo
RangeMutual
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Range -> AccessContext -> m AccessContext
forall (m :: * -> *).
MonadReader Environment m =>
Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll Range
r AccessContext
c'

checkNiceDeclaration' Fixities
_ AccessContext
c
  (NiceModuleMacro Range
r Access
_ (N.NoName Range
_ NameId
_)
    (SectionApp Range
_ [] (RawApp Range
_ (Ident QName
n : [Expr]
es))) OpenShortHand
DoOpen ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> Either LookupError Module -> m Module
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)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> m AccessContext)
-> (Context -> AccessContext) -> Context -> m AccessContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i)
checkNiceDeclaration' Fixities
_ AccessContext
c
  (NiceModuleMacro Range
r Access
a Name
a'
    (SectionApp Range
_ [TypedBinding]
bs (RawApp Range
_ (Ident QName
n : [Expr]
es))) OpenShortHand
DontOpen ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
a'))) (Name -> Maybe Name
fromName Name
a')
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
a'' -> Range -> QName -> Either LookupError Module -> m Module
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)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [TypedBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' (Access -> Access
fromAccess Access
a) Range
r Name
a''
checkNiceDeclaration' Fixities
_ AccessContext
c
  (NiceModuleMacro Range
r Access
a Name
a'
    (SectionApp Range
_ [TypedBinding]
bs (RawApp Range
_ (Ident QName
n : [Expr]
es))) OpenShortHand
DoOpen ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
a'))) (Name -> Maybe Name
fromName Name
a')
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
a'' -> Range -> QName -> Either LookupError Module -> m Module
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)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [TypedBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' (Access -> Access
fromAccess Access
a) Range
r Name
a''
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'''' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c'''' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c''')
checkNiceDeclaration' Fixities
_ AccessContext
_
  (NiceModuleMacro Range
_ Access
_ Name
_
    (SectionApp Range
r [TypedBinding]
_ Expr
_) OpenShortHand
_ ImportDirective
_)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorMacro Range
r))
checkNiceDeclaration' Fixities
_ AccessContext
_
  (NiceModuleMacro Range
r Access
_ Name
_
    (RecordModuleInstance Range
_ QName
_) OpenShortHand
_ ImportDirective
_)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedMacro Range
r)

checkNiceDeclaration' Fixities
_ AccessContext
c (NiceOpen Range
r QName
n ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> Either LookupError Module -> m Module
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)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module Set Range
rs Context
c') -> Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> AccessContext -> m AccessContext
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)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> AccessContext -> m AccessContext
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)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Context -> AccessContext
accessContextImport QName
n' Context
c'
    AccessContext -> AccessContext -> AccessContext
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)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> Context -> Access -> Range -> Maybe Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
c'' Access
Public (AsName -> Range
forall t. HasRange t => t -> 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)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \QName
n' -> Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> m Context
checkFile Range
r QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
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
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> Context -> Access -> Range -> Maybe Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Maybe Name -> m AccessContext
checkModuleNameMay Context
c' Access
Public (AsName -> Range
forall t. HasRange t => t -> Range
getRange AsName
a) (AsName -> Maybe Name
fromAsName AsName
a)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c''' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c''' AccessContext -> AccessContext -> AccessContext
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)
  = m AccessContext -> m AccessContext
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (Bool -> Access -> RangeType -> [Name] -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' Bool
False Access
Public RangeType
RangeVariable (Arg Name -> Name
forall e. Arg e -> e
unArg (Arg Name -> Name) -> [Arg Name] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Name]
ns))
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Pattern
p
  m AccessContext -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
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 :: 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
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_ Expr
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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)
  = Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
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]
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Set Range -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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]
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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]
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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@(NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ Maybe (Ranged Induction)
_ Maybe HasEta
_ Maybe (Name, IsInstance)
_ [LamBinding]
_ [Declaration]
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
_)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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))
  = AccessContext -> Expr -> m ()
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
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty)
    (\Name
n'' -> AccessContext -> m AccessContext
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 :: Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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 :: Name
-> Set Range
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n Set Range
rs Fixities
fs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (Name
-> Set Range
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
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 :: Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop Fixities
_ AccessContext
_ []
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclarationsTop Fixities
_ AccessContext
c (NiceModule Range
r Access
a IsAbstract
_ QName
_ [TypedBinding]
bs [Declaration]
ds : [NiceDeclaration]
_)
  = AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
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 Maybe Name
forall a. Maybe a
Nothing [TypedBinding]
bs [Declaration]
ds
checkNiceDeclarationsTop Fixities
fs AccessContext
c (NiceDeclaration
d : [NiceDeclaration]
ds)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop Fixities
fs (AccessContext
c AccessContext -> AccessContext -> AccessContext
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 :: Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
t Name
n [LamBinding]
bs Expr
e
  = Bool -> AccessContext -> [LamBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
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 :: Bool
-> Fixities
-> AccessContext
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> m AccessContext
checkNiceDataDef Bool
b Fixities
fs AccessContext
c Name
n [LamBinding]
bs [NiceDeclaration]
cs
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> Set Range -> m (Set Range)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LookupError -> Set Range)
-> (Set Range -> Set Range)
-> Either LookupError (Set Range)
-> Set Range
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either LookupError -> Set Range
forall a. Monoid a => a
mempty Set Range -> Set Range
forall a. a -> a
id (QName -> AccessContext -> Either LookupError (Set Range)
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  m (Set Range) -> (Set Range -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Set Range
rs -> Bool -> AccessContext -> [LamBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Fixities
-> Set Range
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
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 AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [NiceDeclaration]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> AccessContext -> m AccessContext
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'' AccessContext -> AccessContext -> AccessContext
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
  -> Maybe (N.Name, IsInstance)
  -> [LamBinding]
  -> [Declaration]
  -> m AccessContext
checkNiceRecordDef :: Bool
-> Fixities
-> AccessContext
-> Name
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> m AccessContext
checkNiceRecordDef Bool
b Fixities
fs AccessContext
c Name
n Maybe (Name, IsInstance)
m [LamBinding]
bs [Declaration]
ds
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> Set Range -> m (Set Range)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LookupError -> Set Range)
-> (Set Range -> Set Range)
-> Either LookupError (Set Range)
-> Set Range
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Set Range -> LookupError -> Set Range
forall a b. a -> b -> a
const Set Range
forall a. Monoid a => a
mempty) Set Range -> Set Range
forall a. a -> a
id (QName -> AccessContext -> Either LookupError (Set Range)
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  m (Set Range) -> (Set Range -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Set Range
rs -> Bool -> AccessContext -> [LamBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> Fixities -> Set Range -> Maybe (Range, Name) -> m AccessContext
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 Maybe (Name, IsInstance)
-> ((Name, IsInstance) -> Maybe (Range, Name))
-> Maybe (Range, Name)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe (Range, Name)
fromNameRange (Name -> Maybe (Range, Name))
-> ((Name, IsInstance) -> Name)
-> (Name, IsInstance)
-> Maybe (Range, Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> Name
-> Set Range -> AccessContext -> [Declaration] -> m AccessContext
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 AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c''' -> AccessContext -> m AccessContext
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'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') AccessContext -> AccessContext -> AccessContext
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 :: 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)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty)
    (\Name
n'' -> AccessContext -> m AccessContext
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
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorConstructor (NiceDeclaration -> Range
forall t. HasRange t => t -> 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 :: Fixities
-> Set Range
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceConstructors Fixities
fs Set Range
rs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Fixities
-> Set Range -> AccessContext -> NiceDeclaration -> m AccessContext
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 :: Fixities -> Set Range -> Range -> Name -> m AccessContext
checkNiceConstructorRecord Fixities
fs Set Range
rs Range
r Name
n
  = Range -> RangeInfo -> m ()
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))
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Set Range -> Maybe Name -> AccessContext
accessContextConstructor Name
n Access
Public (Range -> Set Range -> Set Range
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 :: Fixities -> Set Range -> Maybe (Range, Name) -> m AccessContext
checkNiceConstructorRecordMay Fixities
_ Set Range
_ Maybe (Range, Name)
Nothing
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceConstructorRecordMay Fixities
fs Set Range
rs (Just (Range
r, Name
n))
  = Fixities -> Set Range -> Range -> Name -> m AccessContext
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 :: AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c Access
a Range
r Maybe Name
n [TypedBinding]
bs [Declaration]
ds
  = Bool -> AccessContext -> [TypedBinding] -> m AccessContext
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
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c' -> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \AccessContext
c'' -> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> Context
toContext AccessContext
c'')
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c''' -> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Access -> Context -> AccessContext
fromContext Access
a Context
c''')) (Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' Access
a Range
r) Maybe Name
n

-- ## Imports

data DirectiveType where

  Import
    :: DirectiveType

  Module
    :: DirectiveType

  Open
    :: DirectiveType

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

directiveStatement
  :: DirectiveType
  -> Maybe RangeType
directiveStatement :: DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
Import
  = RangeType -> Maybe RangeType
forall a. a -> Maybe a
Just RangeType
RangeImport
directiveStatement DirectiveType
Module
  = Maybe RangeType
forall a. Maybe a
Nothing
directiveStatement DirectiveType
Open
  = RangeType -> Maybe RangeType
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 :: DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
dt Range
r QName
n Context
c (ImportDirective Range
_ Using' Name Name
UseEverything [ImportedName' Name Name]
hs [Renaming' Name Name]
rs Maybe Range
_)
  = (RangeType -> m ()) -> Maybe RangeType -> m (Maybe ())
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\RangeType
t -> Range -> RangeInfo -> m ()
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)
  m (Maybe ()) -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *).
MonadError Error m =>
Context -> [ImportedName' Name Name] -> m Context
modifyHidings Context
c ([ImportedName' Name Name]
hs [ImportedName' Name Name]
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall a. Semigroup a => a -> a -> a
<> (Renaming' Name Name -> ImportedName' Name Name
forall n m. Renaming' n m -> ImportedName' n m
renFrom (Renaming' Name Name -> ImportedName' Name Name)
-> [Renaming' Name Name] -> [ImportedName' Name Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Renaming' Name Name]
rs))
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType -> Context -> [Renaming' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [Renaming' Name Name] -> m Context
checkRenamings DirectiveType
dt Context
c [Renaming' Name Name]
rs
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r (Context
c' Context -> Context -> Context
forall a. Semigroup a => a -> a -> a
<> Context
c'')
checkImportDirective DirectiveType
dt Range
r QName
n Context
c (ImportDirective Range
_ (Using [ImportedName' Name Name]
ns) [ImportedName' Name Name]
_ [Renaming' Name Name]
rs Maybe Range
_)
  = (RangeType -> m ()) -> Maybe RangeType -> m (Maybe ())
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\RangeType
t -> Range -> RangeInfo -> m ()
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)
  m (Maybe ()) -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
checkImportedNames DirectiveType
dt Context
c [ImportedName' Name Name]
ns
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c' -> DirectiveType -> Context -> [Renaming' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [Renaming' Name Name] -> m Context
checkRenamings DirectiveType
dt Context
c [Renaming' Name Name]
rs
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Context
c'' -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r (Context
c' Context -> Context -> Context
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 :: DirectiveType -> Context -> Renaming' Name Name -> m Context
checkRenaming DirectiveType
dt Context
c r :: Renaming' Name Name
r@(Renaming ImportedName' Name Name
n ImportedName' Name Name
t Maybe Fixity
_ Range
_)
  = DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
checkImportedNamePair DirectiveType
dt Context
c (Renaming' Name Name -> Range
forall t. HasRange t => t -> Range
getRange Renaming' Name Name
r, ImportedName' Name Name
n, ImportedName' Name Name
t)

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

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

checkImportedNamePair
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> (Range, ImportedName, ImportedName)
  -> m Context
checkImportedNamePair :: DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
checkImportedNamePair DirectiveType
dt Context
c (Range
_, ImportedName Name
n, ImportedName Name
t)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)))
    (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Range
r, Name
t') -> Range -> RangeInfo -> m ()
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'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> (Item -> Context) -> Maybe Item -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Item -> Context
contextItem Name
t') (QName -> Context -> Maybe Item
contextLookupItem (Name -> QName
QName Name
n') Context
c)
    Context -> Context -> Context
forall a. Semigroup a => a -> a -> a
<> Context -> (Module -> Context) -> Maybe Module -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair DirectiveType
dt Context
c (Range
_, ImportedModule Name
n, ImportedModule Name
t)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)))
    (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Range
r, Name
t') -> Range -> RangeInfo -> m ()
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'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> (Module -> Context) -> Maybe Module -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair DirectiveType
_ Context
_ (Range
r, ImportedName' Name Name
_, ImportedName' Name Name
_)
  = Error -> m Context
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 :: DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
checkImportedNames DirectiveType
dt
  = (Context -> ImportedName' Name Name -> m Context)
-> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (DirectiveType -> Context -> ImportedName' Name Name -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> ImportedName' Name Name -> m Context
checkImportedName DirectiveType
dt)

modifyHiding
  :: MonadError Error m
  => Context
  -> ImportedName
  -> m Context
modifyHiding :: Context -> ImportedName' Name Name -> m Context
modifyHiding Context
c (ImportedName Name
n)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Name -> Context) -> Name -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Context -> Context) -> Context -> Name -> Context
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Context
contextDelete Context
c
modifyHiding Context
c (ImportedModule Name
n)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (Range -> InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n))) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Name -> Context) -> Name -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Context -> Context) -> Context -> Name -> Context
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 :: Context -> [ImportedName' Name Name] -> m Context
modifyHidings
  = (Context -> ImportedName' Name Name -> m Context)
-> Context -> [ImportedName' Name Name] -> m Context
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Context -> ImportedName' Name Name -> m Context
forall (m :: * -> *).
MonadError Error m =>
Context -> ImportedName' Name Name -> m Context
modifyHiding

touchModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m ()
touchModule :: AccessContext -> Range -> QName -> m ()
touchModule AccessContext
c Range
r QName
n
  = Either LookupError Module -> Range -> QName -> m ()
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 :: Either LookupError Module -> Range -> QName -> m ()
touchModuleWith (Left LookupError
LookupNotFound) Range
_ QName
_
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
touchModuleWith (Left LookupError
LookupAmbiguous) Range
r QName
n
  = Error -> m ()
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
_
  = Set Range -> m ()
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 :: Context -> m ()
touchContext Context
c
  = Set Range -> m ()
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 :: AccessContext -> m ()
touchAccessContext AccessContext
c
  = Set Range -> m ()
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' Name Name]
_ [Renaming' Name Name]
_ Maybe Range
Nothing)
  = Access
Private
importDirectiveAccess (ImportDirective Range
_ Using' Name Name
_ [ImportedName' Name Name]
_ [Renaming' Name Name]
_ (Just Range
_))
  = Access
Public

-- ## Modules

checkModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => QName
  -> Module
  -> m Context
checkModule :: QName -> Module -> m Context
checkModule QName
n ([Pragma]
_, [Declaration]
ds) = do
  Bool
local
    <- m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askLocal
  ()
_
    <- QName -> m ()
forall (m :: * -> *). MonadState State m => QName -> m ()
modifyBlock QName
n
  Context
context
    <- AccessContext -> Context
toContext (AccessContext -> Context) -> m AccessContext -> m Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop AccessContext
forall a. Monoid a => a
mempty [Declaration]
ds
  ()
_
    <- QName -> Context -> m ()
forall (m :: * -> *).
MonadState State m =>
QName -> Context -> m ()
modifyCheck QName
n Context
context
  ()
_
    <- Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
local (Context -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> m ()
touchContext Context
context)
  Context -> m 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 :: Range -> QName -> m Context
checkFile Range
r QName
n
  = QName -> m (Maybe ModuleState)
forall (m :: * -> *).
MonadState State m =>
QName -> m (Maybe ModuleState)
getModule QName
n
  m (Maybe ModuleState)
-> (Maybe ModuleState -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> QName -> Maybe ModuleState -> m Context
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 :: Range -> QName -> Maybe ModuleState -> m Context
checkFileWith Range
r QName
n Maybe ModuleState
Nothing
  = m RawName
forall (m :: * -> *). MonadReader Environment m => m RawName
askRoot
  m RawName -> (RawName -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \RawName
p -> RawName -> m RawName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RawName
p RawName -> ShowS
</> QName -> RawName
qNamePath QName
n)
  m RawName -> (RawName -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \RawName
p' -> IO Bool -> m Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO Bool
doesFileExist RawName
p')
  m Bool -> (Bool -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b -> Range -> QName -> Maybe RawName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Range -> QName -> Maybe RawName -> m Context
checkFileWith' Range
r QName
n (Maybe RawName -> Maybe RawName -> Bool -> Maybe RawName
forall a. a -> a -> Bool -> a
bool Maybe RawName
forall a. Maybe a
Nothing (RawName -> Maybe RawName
forall a. a -> Maybe a
Just RawName
p') Bool
b)
checkFileWith Range
r QName
n (Just ModuleState
Blocked)
  = Error -> m Context
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))
  = Context -> m Context
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' :: Range -> QName -> Maybe RawName -> m Context
checkFileWith' Range
r QName
n Maybe RawName
Nothing
  = Range -> QName -> m Context
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 RawName
p)
  = QName -> RawName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> RawName -> m Context
checkFilePath QName
n RawName
p

checkFileExternal
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Range
  -> QName
  -> m Context
checkFileExternal :: Range -> QName -> m Context
checkFileExternal Range
r QName
n = do
  [AbsolutePath]
includes
    <- m [AbsolutePath]
forall (m :: * -> *). MonadReader Environment m => m [AbsolutePath]
askIncludes
  ModuleToSource
sources
    <- m ModuleToSource
forall (m :: * -> *). MonadState State m => m ModuleToSource
getSources
  (Either FindError SourceFile
pathEither, ModuleToSource
sources') 
    <- IO (Either FindError SourceFile, ModuleToSource)
-> m (Either FindError SourceFile, ModuleToSource)
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
    <- Either Error SourceFile -> m SourceFile
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((FindError -> Error)
-> Either FindError SourceFile -> Either Error SourceFile
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)
  ()
_
    <- ModuleToSource -> m ()
forall (m :: * -> *). MonadState State m => ModuleToSource -> m ()
modifySources ModuleToSource
sources'
  Context
context
    <- m Context -> m Context
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (QName -> RawName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
QName -> RawName -> m Context
checkFilePath QName
n (AbsolutePath -> RawName
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
path)))
  Context -> m Context
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 :: QName -> RawName -> m Context
checkFilePath QName
n RawName
p
  = RawName -> m Module
forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
RawName -> m Module
readModule RawName
p
  m Module -> (Module -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QName -> Module -> m Context
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 :: Mode -> UnusedOptions -> RawName -> m (RawName, State)
checkFileTop Mode
m UnusedOptions
opts RawName
p = do
  Module
module'
    <- RawName -> m Module
forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
RawName -> m Module
readModule RawName
p
  TopLevelModuleName
moduleName
    <- TopLevelModuleName -> m TopLevelModuleName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module -> TopLevelModuleName
topLevelModuleName Module
module')
  QName
moduleQName
    <- Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Error
ErrorInternal (RawName -> InternalError
ErrorModuleName RawName
p)) (TopLevelModuleName -> Maybe QName
fromModuleName TopLevelModuleName
moduleName)
  AbsolutePath
absolutePath
    <- AbsolutePath -> m AbsolutePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot (RawName -> AbsolutePath
mkAbsolute RawName
p) TopLevelModuleName
moduleName)
  RawName
rootPath
    <- RawName -> m RawName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath -> RawName
filePath AbsolutePath
absolutePath)
  Either TCErr [AbsolutePath]
includesEither
    <- IO (Either TCErr [AbsolutePath]) -> m (Either TCErr [AbsolutePath])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (TCM [AbsolutePath] -> IO (Either TCErr [AbsolutePath])
forall a. TCM a -> IO (Either TCErr a)
runTCMTop (UnusedOptions -> TCM ()
setOptions UnusedOptions
opts TCM () -> TCM [AbsolutePath] -> TCM [AbsolutePath]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCM [AbsolutePath]
forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs))
  [AbsolutePath]
includes
    <- Either Error [AbsolutePath] -> m [AbsolutePath]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((TCErr -> Error)
-> Either TCErr [AbsolutePath] -> Either Error [AbsolutePath]
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft (Error -> TCErr -> Error
forall a b. a -> b -> a
const Error
ErrorInclude) Either TCErr [AbsolutePath]
includesEither)
  Environment
env
    <- Environment -> m Environment
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Mode -> RawName -> [AbsolutePath] -> Environment
Environment Mode
m RawName
rootPath [AbsolutePath]
includes)
  (Context
_, State
state)
    <- StateT State m Context -> State -> m (Context, State)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ReaderT Environment (StateT State m) Context
-> Environment -> StateT State m Context
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (QName -> Module -> ReaderT Environment (StateT State m) Context
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
  (RawName, State) -> m (RawName, State)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RawName
rootPath, State
state)

readModule
  :: MonadError Error m
  => MonadIO m
  => FilePath
  -> m Module
readModule :: RawName -> m Module
readModule RawName
p = do
  Bool
exists
    <- IO Bool -> m Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO Bool
doesFileExist RawName
p)
  ()
_
    <- Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists (Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (RawName -> Error
ErrorFile RawName
p))
  AbsolutePath
absolutePath
    <- AbsolutePath -> m AbsolutePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RawName -> AbsolutePath
mkAbsolute RawName
p)
  RawName
contents
    <- IO RawName -> m RawName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO RawName
readFile RawName
p)
  (Either ParseError (Module, FileType)
parseResult, [ParseWarning]
_)
    <- IO (Either ParseError (Module, FileType), [ParseWarning])
-> m (Either ParseError (Module, FileType), [ParseWarning])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PM (Module, FileType)
-> IO (Either ParseError (Module, FileType), [ParseWarning])
forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO (Parser Module -> AbsolutePath -> RawName -> PM (Module, FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> RawName -> PM (a, FileType)
parseFile Parser Module
moduleParser AbsolutePath
absolutePath RawName
contents))
  (Module
module', FileType
_)
    <- Either Error (Module, FileType) -> m (Module, FileType)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((ParseError -> Error)
-> Either ParseError (Module, FileType)
-> Either Error (Module, FileType)
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft ParseError -> Error
ErrorParse Either ParseError (Module, FileType)
parseResult)
  Module -> m Module
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 -> RawName -> RawName -> IO [RawName]
checkPath Set QName
ns RawName
i RawName
r
  = Set RawName -> [RawName]
forall a. Set a -> [a]
Set.toAscList (Set RawName -> [RawName]) -> IO (Set RawName) -> IO [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set QName -> RawName -> RawName -> RawName -> IO (Set RawName)
checkPath' Set QName
ns RawName
i RawName
r RawName
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 -> RawName -> RawName -> RawName -> IO (Set RawName)
checkPath' Set QName
ns RawName
i RawName
r RawName
p
  = IO Bool -> IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO Bool
doesDirectoryExist RawName
p)
  IO Bool -> (Bool -> IO (Set RawName)) -> IO (Set RawName)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (Set RawName) -> IO (Set RawName) -> Bool -> IO (Set RawName)
forall a. a -> a -> Bool -> a
bool (Set RawName -> IO (Set RawName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set QName -> RawName -> RawName -> RawName -> Set RawName
checkPathFile Set QName
ns RawName
i RawName
r RawName
p)) (Set QName -> RawName -> RawName -> RawName -> IO (Set RawName)
checkPathDirectory Set QName
ns RawName
i RawName
r RawName
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 -> RawName -> RawName -> RawName -> Set RawName
checkPathFile Set QName
_ RawName
i RawName
_ RawName
p | RawName
i RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
p
  = Set RawName
forall a. Monoid a => a
mempty
checkPathFile Set QName
ns RawName
_ RawName
r RawName
p
  = Set RawName -> (QName -> Set RawName) -> Maybe QName -> Set RawName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set RawName
forall a. Monoid a => a
mempty (Set RawName -> Set RawName -> Bool -> Set RawName
forall a. a -> a -> Bool -> a
bool (RawName -> Set RawName
forall a. a -> Set a
Set.singleton RawName
p) Set RawName
forall a. Monoid a => a
mempty (Bool -> Set RawName) -> (QName -> Bool) -> QName -> Set RawName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Set QName -> Bool) -> Set QName -> QName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set QName
ns)
  (Maybe QName -> Set RawName) -> Maybe QName -> Set RawName
forall a b. (a -> b) -> a -> b
$ RawName -> RawName -> Maybe QName
pathQName RawName
r RawName
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 -> RawName -> RawName -> RawName -> IO (Set RawName)
checkPathDirectory Set QName
ns RawName
i RawName
r RawName
p
  = ShowS -> [RawName] -> [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RawName
p RawName -> ShowS
</>) ([RawName] -> [RawName]) -> IO [RawName] -> IO [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [RawName] -> IO [RawName]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO [RawName]
listDirectory RawName
p)
  IO [RawName] -> ([RawName] -> IO [Set RawName]) -> IO [Set RawName]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (RawName -> IO (Set RawName)) -> [RawName] -> IO [Set RawName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Set QName -> RawName -> RawName -> RawName -> IO (Set RawName)
checkPath' Set QName
ns RawName
i RawName
r)
  IO [Set RawName]
-> ([Set RawName] -> IO (Set RawName)) -> IO (Set RawName)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set RawName -> IO (Set RawName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set RawName -> IO (Set RawName))
-> ([Set RawName] -> Set RawName)
-> [Set RawName]
-> IO (Set RawName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set RawName] -> Set RawName
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 -> RawName -> IO (Either Error UnusedItems)
checkUnused
  = Mode -> UnusedOptions -> RawName -> 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 -> RawName -> IO (Either Error UnusedItems)
checkUnusedWith Mode
m UnusedOptions
opts
  = ExceptT Error IO UnusedItems -> IO (Either Error UnusedItems)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  (ExceptT Error IO UnusedItems -> IO (Either Error UnusedItems))
-> (RawName -> ExceptT Error IO UnusedItems)
-> RawName
-> IO (Either Error UnusedItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RawName, State) -> UnusedItems)
-> ExceptT Error IO (RawName, State)
-> ExceptT Error IO UnusedItems
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Range, RangeInfo)] -> UnusedItems
UnusedItems ([(Range, RangeInfo)] -> UnusedItems)
-> ((RawName, State) -> [(Range, RangeInfo)])
-> (RawName, State)
-> UnusedItems
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> [(Range, RangeInfo)]
stateItems (State -> [(Range, RangeInfo)])
-> ((RawName, State) -> State)
-> (RawName, State)
-> [(Range, RangeInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RawName, State) -> State
forall a b. (a, b) -> b
snd)
  (ExceptT Error IO (RawName, State) -> ExceptT Error IO UnusedItems)
-> (RawName -> ExceptT Error IO (RawName, State))
-> RawName
-> ExceptT Error IO UnusedItems
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mode
-> UnusedOptions -> RawName -> ExceptT Error IO (RawName, State)
forall (m :: * -> *).
(MonadError Error m, MonadIO m) =>
Mode -> UnusedOptions -> RawName -> m (RawName, 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 -> RawName -> IO (Either Error Unused)
checkUnusedGlobal UnusedOptions
opts RawName
p
  = ExceptT Error IO Unused -> IO (Either Error Unused)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (UnusedOptions -> RawName -> ExceptT Error IO Unused
checkUnusedGlobal' UnusedOptions
opts RawName
p)

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

setOptions
  :: UnusedOptions
  -> TCM ()
setOptions :: UnusedOptions -> TCM ()
setOptions UnusedOptions
opts
  = CommandLineOptions -> TCM ()
setCommandLineOptions
  (CommandLineOptions -> TCM ()) -> CommandLineOptions -> TCM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
defaultOptions
  { optIncludePaths :: [RawName]
optIncludePaths
    = UnusedOptions -> [RawName]
unusedOptionsInclude UnusedOptions
opts
  , optLibraries :: [RawName]
optLibraries
    = Text -> RawName
T.unpack (Text -> RawName) -> [Text] -> [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnusedOptions -> [Text]
unusedOptionsLibraries UnusedOptions
opts
  , optOverrideLibrariesFile :: Maybe RawName
optOverrideLibrariesFile
    = UnusedOptions -> Maybe RawName
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 :: RawName -> (Range, RangeInfo) -> Bool
inFile RawName
p (Range
r, RangeInfo
_)
  = Range -> Maybe RawName
rangePath Range
r Maybe RawName -> Maybe RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName -> Maybe RawName
forall a. a -> Maybe a
Just RawName
p