{-# LANGUAGE CPP #-}
{-# LANGUAGE RecursiveDo #-}
module Agda.TypeChecking.Monad.Base
( module Agda.TypeChecking.Monad.Base
, module Agda.TypeChecking.Monad.Base.Types
, HasOptions (..)
, RecordFieldWarning
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import qualified Control.Concurrent as C
import Control.DeepSeq
import qualified Control.Exception as E
import qualified Control.Monad.Fail as Fail
import Control.Monad ( void )
import Control.Monad.Except
import Control.Monad.Fix
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.State ( MonadState(..), modify, StateT(..), runStateT )
import Control.Monad.Reader ( MonadReader(..), ReaderT(..), runReaderT )
import Control.Monad.Writer ( WriterT )
import Control.Monad.Trans ( MonadTrans(..), lift )
import Control.Monad.Trans.Control ( MonadTransControl(..), liftThrough )
import Control.Monad.Trans.Identity ( IdentityT(..), runIdentityT )
import Control.Monad.Trans.Maybe ( MaybeT(..) )
import Control.Parallel ( pseq )
import Data.Array (Ix)
import Data.DList (DList)
import Data.Function (on)
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Sequence (Seq)
import Data.Set (Set, toList, fromList)
import qualified Data.Set as Set
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import qualified Data.HashSet as HashSet
import Data.Hashable
import Data.HashSet (HashSet)
import Data.Semigroup ( Semigroup, (<>))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String
import Data.Text (Text)
import qualified Data.Text.Lazy as TL
import Data.IORef
import GHC.Generics (Generic)
import System.IO (hFlush, stdout)
import Agda.Benchmarking (Benchmark, Phase)
import {-# SOURCE #-} Agda.Compiler.Treeless.Pretty ()
import Agda.Syntax.Common
import Agda.Syntax.Builtin (SomeBuiltin, BuiltinId, PrimitiveId)
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Definitions
(NiceDeclaration, DeclarationWarning, declarationWarningName)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Parser (ParseWarning)
import Agda.Syntax.Parser.Monad (parseWarningName)
import Agda.Syntax.TopLevelModuleName
(RawTopLevelModuleName, TopLevelModuleName)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Notation
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Info ( MetaKind(InstanceMeta, UnificationMeta), MetaNameSuggestion, MutualInfo )
import Agda.TypeChecking.Monad.Base.Types
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import Agda.TypeChecking.Monad.Base.Warning (RecordFieldWarning)
import Agda.TypeChecking.SizedTypes.Syntax (HypSizeConstraint)
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Free.Lazy (Free(freeVars'), underBinder', underBinder)
import Agda.TypeChecking.DiscrimTree.Types
import Agda.Compiler.Backend.Base
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Interaction.Response.Base (Response_boot(..))
import Agda.Interaction.Highlighting.Precise
(HighlightingInfo, NameKind)
import Agda.Interaction.Library
import Agda.Interaction.Library.Base (LibErrors)
import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.BiMap (BiMap, HasTag(..))
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Boolean ( fromBool, toBool )
import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Hash
import Agda.Utils.IO ( showIOException )
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List2 (List2, pattern List2)
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty
import Agda.Utils.SmallSet (SmallSet, SmallSetElement)
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Singleton
import Agda.Utils.Update
import Agda.Utils.Impossible
data TCState = TCSt
{ TCState -> PreScopeState
stPreScopeState :: !PreScopeState
, TCState -> PostScopeState
stPostScopeState :: !PostScopeState
, TCState -> PersistentTCState
stPersistentState :: !PersistentTCState
}
deriving (forall x. TCState -> Rep TCState x)
-> (forall x. Rep TCState x -> TCState) -> Generic TCState
forall x. Rep TCState x -> TCState
forall x. TCState -> Rep TCState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TCState -> Rep TCState x
from :: forall x. TCState -> Rep TCState x
$cto :: forall x. Rep TCState x -> TCState
to :: forall x. Rep TCState x -> TCState
Generic
class Monad m => ReadTCState m where
getTCState :: m TCState
locallyTCState :: Lens' TCState a -> (a -> a) -> m b -> m b
withTCState :: (TCState -> TCState) -> m a -> m a
withTCState = Lens' TCState TCState -> (TCState -> TCState) -> m a -> m a
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (TCState -> f TCState) -> TCState -> f TCState
forall a. a -> a
Lens' TCState TCState
id
default getTCState :: (MonadTrans t, ReadTCState n, t n ~ m) => m TCState
getTCState = n TCState -> t n TCState
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
default locallyTCState
:: (MonadTransControl t, ReadTCState n, t n ~ m)
=> Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState Lens' TCState a
l = (n (StT t b) -> n (StT t b)) -> m b -> m b
(n (StT t b) -> n (StT t b)) -> t n b -> t n b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t b) -> n (StT t b)) -> m b -> m b)
-> ((a -> a) -> n (StT t b) -> n (StT t b))
-> (a -> a)
-> m b
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCState a -> (a -> a) -> n (StT t b) -> n (StT t b)
forall a b. Lens' TCState a -> (a -> a) -> n b -> n b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (a -> f a) -> TCState -> f TCState
Lens' TCState a
l
instance ReadTCState m => ReadTCState (ListT m) where
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ListT m b -> ListT m b
locallyTCState Lens' TCState a
l = (m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
-> ListT m b -> ListT m b
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> ListT m a -> ListT n b
mapListT ((m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
-> ListT m b -> ListT m b)
-> ((a -> a)
-> m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
-> (a -> a)
-> ListT m b
-> ListT m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCState a
-> (a -> a) -> m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b))
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (a -> f a) -> TCState -> f TCState
Lens' TCState a
l
instance ReadTCState m => ReadTCState (ChangeT m)
instance ReadTCState m => ReadTCState (ExceptT err m)
instance ReadTCState m => ReadTCState (IdentityT m)
instance ReadTCState m => ReadTCState (MaybeT m)
instance ReadTCState m => ReadTCState (ReaderT r m)
instance ReadTCState m => ReadTCState (StateT s m)
instance (Monoid w, ReadTCState m) => ReadTCState (WriterT w m)
instance Show TCState where
show :: TCState -> String
show TCState
_ = String
"TCSt{}"
data PreScopeState = PreScopeState
{ PreScopeState -> HighlightingInfo
stPreTokens :: !HighlightingInfo
, PreScopeState -> Signature
stPreImports :: !Signature
, PreScopeState -> Set TopLevelModuleName
stPreImportedModules :: !(Set TopLevelModuleName)
, PreScopeState -> ModuleToSource
stPreModuleToSource :: !ModuleToSource
, PreScopeState -> VisitedModules
stPreVisitedModules :: !VisitedModules
, PreScopeState -> ScopeInfo
stPreScope :: !ScopeInfo
, PreScopeState -> PatternSynDefns
stPrePatternSyns :: !A.PatternSynDefns
, PreScopeState -> PatternSynDefns
stPrePatternSynImports :: !A.PatternSynDefns
, PreScopeState -> Maybe (Set QName)
stPreGeneralizedVars :: !(Strict.Maybe (Set QName))
, PreScopeState -> PragmaOptions
stPrePragmaOptions :: !PragmaOptions
, PreScopeState -> BuiltinThings PrimFun
stPreImportedBuiltins :: !(BuiltinThings PrimFun)
, PreScopeState -> DisplayForms
stPreImportedDisplayForms :: !DisplayForms
, PreScopeState -> InteractionId
stPreFreshInteractionId :: !InteractionId
, PreScopeState -> Map QName Text
stPreImportedUserWarnings :: !(Map A.QName Text)
, PreScopeState -> Map QName Text
stPreLocalUserWarnings :: !(Map A.QName Text)
, PreScopeState -> Maybe Text
stPreWarningOnImport :: !(Strict.Maybe Text)
, PreScopeState -> Set QName
stPreImportedPartialDefs :: !(Set QName)
, PreScopeState -> Map String ProjectConfig
stPreProjectConfigs :: !(Map FilePath ProjectConfig)
, PreScopeState -> Map String AgdaLibFile
stPreAgdaLibFiles :: !(Map FilePath AgdaLibFile)
, PreScopeState -> RemoteMetaStore
stPreImportedMetaStore :: !RemoteMetaStore
, PreScopeState -> HashMap QName QName
stPreCopiedNames :: !(HashMap A.QName A.QName)
, PreScopeState -> HashMap QName (HashSet QName)
stPreNameCopies :: !(HashMap A.QName (HashSet A.QName))
}
deriving (forall x. PreScopeState -> Rep PreScopeState x)
-> (forall x. Rep PreScopeState x -> PreScopeState)
-> Generic PreScopeState
forall x. Rep PreScopeState x -> PreScopeState
forall x. PreScopeState -> Rep PreScopeState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PreScopeState -> Rep PreScopeState x
from :: forall x. PreScopeState -> Rep PreScopeState x
$cto :: forall x. Rep PreScopeState x -> PreScopeState
to :: forall x. Rep PreScopeState x -> PreScopeState
Generic
data DisambiguatedName = DisambiguatedName NameKind A.QName
deriving (forall x. DisambiguatedName -> Rep DisambiguatedName x)
-> (forall x. Rep DisambiguatedName x -> DisambiguatedName)
-> Generic DisambiguatedName
forall x. Rep DisambiguatedName x -> DisambiguatedName
forall x. DisambiguatedName -> Rep DisambiguatedName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DisambiguatedName -> Rep DisambiguatedName x
from :: forall x. DisambiguatedName -> Rep DisambiguatedName x
$cto :: forall x. Rep DisambiguatedName x -> DisambiguatedName
to :: forall x. Rep DisambiguatedName x -> DisambiguatedName
Generic
type DisambiguatedNames = IntMap DisambiguatedName
type ConcreteNames = Map Name [C.Name]
data PostScopeState = PostScopeState
{ PostScopeState -> HighlightingInfo
stPostSyntaxInfo :: !HighlightingInfo
, PostScopeState -> DisambiguatedNames
stPostDisambiguatedNames :: !DisambiguatedNames
, PostScopeState -> LocalMetaStore
stPostOpenMetaStore :: !LocalMetaStore
, PostScopeState -> LocalMetaStore
stPostSolvedMetaStore :: !LocalMetaStore
, PostScopeState -> InteractionPoints
stPostInteractionPoints :: !InteractionPoints
, PostScopeState -> Constraints
stPostAwakeConstraints :: !Constraints
, PostScopeState -> Constraints
stPostSleepingConstraints :: !Constraints
, PostScopeState -> Bool
stPostDirty :: !Bool
, PostScopeState -> Set QName
stPostOccursCheckDefs :: !(Set QName)
, PostScopeState -> Signature
stPostSignature :: !Signature
, PostScopeState -> Map ModuleName CheckpointId
stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
, PostScopeState -> DisplayForms
stPostImportsDisplayForms :: !DisplayForms
, PostScopeState -> Map String ForeignCodeStack
stPostForeignCode :: !(Map BackendName ForeignCodeStack)
, PostScopeState -> Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule ::
!(Maybe (ModuleName, TopLevelModuleName))
, PostScopeState -> Set QName
stPostPendingInstances :: !(Set QName)
, PostScopeState -> Set QName
stPostTemporaryInstances :: !(Set QName)
, PostScopeState -> ConcreteNames
stPostConcreteNames :: !ConcreteNames
, PostScopeState -> Map String (DList String)
stPostUsedNames :: !(Map RawName (DList RawName))
, PostScopeState -> Map Name (DList String)
stPostShadowingNames :: !(Map Name (DList RawName))
, PostScopeState -> Statistics
stPostStatistics :: !Statistics
, PostScopeState -> [TCWarning]
stPostTCWarnings :: ![TCWarning]
, PostScopeState -> Map MutualId MutualBlock
stPostMutualBlocks :: !(Map MutualId MutualBlock)
, PostScopeState -> BuiltinThings PrimFun
stPostLocalBuiltins :: !(BuiltinThings PrimFun)
, PostScopeState -> MetaId
stPostFreshMetaId :: !MetaId
, PostScopeState -> MutualId
stPostFreshMutualId :: !MutualId
, PostScopeState -> ProblemId
stPostFreshProblemId :: !ProblemId
, PostScopeState -> CheckpointId
stPostFreshCheckpointId :: !CheckpointId
, PostScopeState -> Int
stPostFreshInt :: !Int
, PostScopeState -> NameId
stPostFreshNameId :: !NameId
, PostScopeState -> OpaqueId
stPostFreshOpaqueId :: !OpaqueId
, PostScopeState -> Bool
stPostAreWeCaching :: !Bool
, PostScopeState -> Bool
stPostPostponeInstanceSearch :: !Bool
, PostScopeState -> Bool
stPostConsideringInstance :: !Bool
, PostScopeState -> Bool
stPostInstantiateBlocking :: !Bool
, PostScopeState -> Set QName
stPostLocalPartialDefs :: !(Set QName)
, PostScopeState -> Map OpaqueId OpaqueBlock
stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
, PostScopeState -> Map QName OpaqueId
stPostOpaqueIds :: Map QName OpaqueId
}
deriving ((forall x. PostScopeState -> Rep PostScopeState x)
-> (forall x. Rep PostScopeState x -> PostScopeState)
-> Generic PostScopeState
forall x. Rep PostScopeState x -> PostScopeState
forall x. PostScopeState -> Rep PostScopeState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PostScopeState -> Rep PostScopeState x
from :: forall x. PostScopeState -> Rep PostScopeState x
$cto :: forall x. Rep PostScopeState x -> PostScopeState
to :: forall x. Rep PostScopeState x -> PostScopeState
Generic)
data MutualBlock = MutualBlock
{ MutualBlock -> MutualInfo
mutualInfo :: MutualInfo
, MutualBlock -> Set QName
mutualNames :: Set QName
} deriving (Int -> MutualBlock -> ShowS
[MutualBlock] -> ShowS
MutualBlock -> String
(Int -> MutualBlock -> ShowS)
-> (MutualBlock -> String)
-> ([MutualBlock] -> ShowS)
-> Show MutualBlock
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MutualBlock -> ShowS
showsPrec :: Int -> MutualBlock -> ShowS
$cshow :: MutualBlock -> String
show :: MutualBlock -> String
$cshowList :: [MutualBlock] -> ShowS
showList :: [MutualBlock] -> ShowS
Show, MutualBlock -> MutualBlock -> Bool
(MutualBlock -> MutualBlock -> Bool)
-> (MutualBlock -> MutualBlock -> Bool) -> Eq MutualBlock
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MutualBlock -> MutualBlock -> Bool
== :: MutualBlock -> MutualBlock -> Bool
$c/= :: MutualBlock -> MutualBlock -> Bool
/= :: MutualBlock -> MutualBlock -> Bool
Eq, (forall x. MutualBlock -> Rep MutualBlock x)
-> (forall x. Rep MutualBlock x -> MutualBlock)
-> Generic MutualBlock
forall x. Rep MutualBlock x -> MutualBlock
forall x. MutualBlock -> Rep MutualBlock x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MutualBlock -> Rep MutualBlock x
from :: forall x. MutualBlock -> Rep MutualBlock x
$cto :: forall x. Rep MutualBlock x -> MutualBlock
to :: forall x. Rep MutualBlock x -> MutualBlock
Generic)
instance Null MutualBlock where
empty :: MutualBlock
empty = MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
forall a. Null a => a
empty Set QName
forall a. Null a => a
empty
data PersistentTCState = PersistentTCSt
{ PersistentTCState -> VisitedModules
stDecodedModules :: !DecodedModules
, PersistentTCState -> BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames ::
!(BiMap RawTopLevelModuleName ModuleNameHash)
, PersistentTCState -> CommandLineOptions
stPersistentOptions :: CommandLineOptions
, PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback :: InteractionOutputCallback
, PersistentTCState -> Benchmark
stBenchmark :: !Benchmark
, PersistentTCState -> Statistics
stAccumStatistics :: !Statistics
, PersistentTCState -> Maybe LoadedFileCache
stPersistLoadedFileCache :: !(Strict.Maybe LoadedFileCache)
, PersistentTCState -> [Backend_boot (TCMT IO)]
stPersistBackends :: [Backend_boot TCM]
}
deriving (forall x. PersistentTCState -> Rep PersistentTCState x)
-> (forall x. Rep PersistentTCState x -> PersistentTCState)
-> Generic PersistentTCState
forall x. Rep PersistentTCState x -> PersistentTCState
forall x. PersistentTCState -> Rep PersistentTCState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PersistentTCState -> Rep PersistentTCState x
from :: forall x. PersistentTCState -> Rep PersistentTCState x
$cto :: forall x. Rep PersistentTCState x -> PersistentTCState
to :: forall x. Rep PersistentTCState x -> PersistentTCState
Generic
data LoadedFileCache = LoadedFileCache
{ LoadedFileCache -> CachedTypeCheckLog
lfcCached :: !CachedTypeCheckLog
, LoadedFileCache -> CachedTypeCheckLog
lfcCurrent :: !CurrentTypeCheckLog
}
deriving (forall x. LoadedFileCache -> Rep LoadedFileCache x)
-> (forall x. Rep LoadedFileCache x -> LoadedFileCache)
-> Generic LoadedFileCache
forall x. Rep LoadedFileCache x -> LoadedFileCache
forall x. LoadedFileCache -> Rep LoadedFileCache x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LoadedFileCache -> Rep LoadedFileCache x
from :: forall x. LoadedFileCache -> Rep LoadedFileCache x
$cto :: forall x. Rep LoadedFileCache x -> LoadedFileCache
to :: forall x. Rep LoadedFileCache x -> LoadedFileCache
Generic
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data TypeCheckAction
= EnterSection !Erased !ModuleName !A.Telescope
| LeaveSection !ModuleName
| Decl !A.Declaration
| Pragmas !PragmaOptions
deriving ((forall x. TypeCheckAction -> Rep TypeCheckAction x)
-> (forall x. Rep TypeCheckAction x -> TypeCheckAction)
-> Generic TypeCheckAction
forall x. Rep TypeCheckAction x -> TypeCheckAction
forall x. TypeCheckAction -> Rep TypeCheckAction x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TypeCheckAction -> Rep TypeCheckAction x
from :: forall x. TypeCheckAction -> Rep TypeCheckAction x
$cto :: forall x. Rep TypeCheckAction x -> TypeCheckAction
to :: forall x. Rep TypeCheckAction x -> TypeCheckAction
Generic)
initPersistentState :: PersistentTCState
initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
{ stPersistentOptions :: CommandLineOptions
stPersistentOptions = CommandLineOptions
defaultOptions
, stPersistentTopLevelModuleNames :: BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames = BiMap RawTopLevelModuleName ModuleNameHash
forall a. Null a => a
empty
, stDecodedModules :: VisitedModules
stDecodedModules = VisitedModules
forall k a. Map k a
Map.empty
, stInteractionOutputCallback :: InteractionOutputCallback
stInteractionOutputCallback = InteractionOutputCallback
defaultInteractionOutputCallback
, stBenchmark :: Benchmark
stBenchmark = Benchmark
forall a. Null a => a
empty
, stAccumStatistics :: Statistics
stAccumStatistics = Statistics
forall k a. Map k a
Map.empty
, stPersistLoadedFileCache :: Maybe LoadedFileCache
stPersistLoadedFileCache = Maybe LoadedFileCache
forall a. Null a => a
empty
, stPersistBackends :: [Backend_boot (TCMT IO)]
stPersistBackends = []
}
initialMetaId :: MetaId
initialMetaId :: MetaId
initialMetaId = MetaId
{ metaId :: Word64
metaId = Word64
0
, metaModule :: ModuleNameHash
metaModule = ModuleNameHash
noModuleNameHash
}
initPreScopeState :: PreScopeState
initPreScopeState :: PreScopeState
initPreScopeState = PreScopeState
{ stPreTokens :: HighlightingInfo
stPreTokens = HighlightingInfo
forall a. Monoid a => a
mempty
, stPreImports :: Signature
stPreImports = Signature
emptySignature
, stPreImportedModules :: Set TopLevelModuleName
stPreImportedModules = Set TopLevelModuleName
forall a. Null a => a
empty
, stPreModuleToSource :: ModuleToSource
stPreModuleToSource = ModuleToSource
forall k a. Map k a
Map.empty
, stPreVisitedModules :: VisitedModules
stPreVisitedModules = VisitedModules
forall k a. Map k a
Map.empty
, stPreScope :: ScopeInfo
stPreScope = ScopeInfo
emptyScopeInfo
, stPrePatternSyns :: PatternSynDefns
stPrePatternSyns = PatternSynDefns
forall k a. Map k a
Map.empty
, stPrePatternSynImports :: PatternSynDefns
stPrePatternSynImports = PatternSynDefns
forall k a. Map k a
Map.empty
, stPreGeneralizedVars :: Maybe (Set QName)
stPreGeneralizedVars = Maybe (Set QName)
forall a. Monoid a => a
mempty
, stPrePragmaOptions :: PragmaOptions
stPrePragmaOptions = PragmaOptions
defaultInteractionOptions
, stPreImportedBuiltins :: BuiltinThings PrimFun
stPreImportedBuiltins = BuiltinThings PrimFun
forall k a. Map k a
Map.empty
, stPreImportedDisplayForms :: DisplayForms
stPreImportedDisplayForms = DisplayForms
forall k v. HashMap k v
HMap.empty
, stPreFreshInteractionId :: InteractionId
stPreFreshInteractionId = InteractionId
0
, stPreImportedUserWarnings :: Map QName Text
stPreImportedUserWarnings = Map QName Text
forall k a. Map k a
Map.empty
, stPreLocalUserWarnings :: Map QName Text
stPreLocalUserWarnings = Map QName Text
forall k a. Map k a
Map.empty
, stPreWarningOnImport :: Maybe Text
stPreWarningOnImport = Maybe Text
forall a. Null a => a
empty
, stPreImportedPartialDefs :: Set QName
stPreImportedPartialDefs = Set QName
forall a. Set a
Set.empty
, stPreProjectConfigs :: Map String ProjectConfig
stPreProjectConfigs = Map String ProjectConfig
forall k a. Map k a
Map.empty
, stPreAgdaLibFiles :: Map String AgdaLibFile
stPreAgdaLibFiles = Map String AgdaLibFile
forall k a. Map k a
Map.empty
, stPreImportedMetaStore :: RemoteMetaStore
stPreImportedMetaStore = RemoteMetaStore
forall k v. HashMap k v
HMap.empty
, stPreCopiedNames :: HashMap QName QName
stPreCopiedNames = HashMap QName QName
forall k v. HashMap k v
HMap.empty
, stPreNameCopies :: HashMap QName (HashSet QName)
stPreNameCopies = HashMap QName (HashSet QName)
forall k v. HashMap k v
HMap.empty
}
initPostScopeState :: PostScopeState
initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
{ stPostSyntaxInfo :: HighlightingInfo
stPostSyntaxInfo = HighlightingInfo
forall a. Monoid a => a
mempty
, stPostDisambiguatedNames :: DisambiguatedNames
stPostDisambiguatedNames = DisambiguatedNames
forall a. IntMap a
IntMap.empty
, stPostOpenMetaStore :: LocalMetaStore
stPostOpenMetaStore = LocalMetaStore
forall k a. Map k a
Map.empty
, stPostSolvedMetaStore :: LocalMetaStore
stPostSolvedMetaStore = LocalMetaStore
forall k a. Map k a
Map.empty
, stPostInteractionPoints :: InteractionPoints
stPostInteractionPoints = InteractionPoints
forall a. Null a => a
empty
, stPostAwakeConstraints :: Constraints
stPostAwakeConstraints = []
, stPostSleepingConstraints :: Constraints
stPostSleepingConstraints = []
, stPostDirty :: Bool
stPostDirty = Bool
False
, stPostOccursCheckDefs :: Set QName
stPostOccursCheckDefs = Set QName
forall a. Set a
Set.empty
, stPostSignature :: Signature
stPostSignature = Signature
emptySignature
, stPostModuleCheckpoints :: Map ModuleName CheckpointId
stPostModuleCheckpoints = Map ModuleName CheckpointId
forall k a. Map k a
Map.empty
, stPostImportsDisplayForms :: DisplayForms
stPostImportsDisplayForms = DisplayForms
forall k v. HashMap k v
HMap.empty
, stPostCurrentModule :: Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule = Maybe (ModuleName, TopLevelModuleName)
forall a. Null a => a
empty
, stPostPendingInstances :: Set QName
stPostPendingInstances = Set QName
forall a. Set a
Set.empty
, stPostTemporaryInstances :: Set QName
stPostTemporaryInstances = Set QName
forall a. Set a
Set.empty
, stPostConcreteNames :: ConcreteNames
stPostConcreteNames = ConcreteNames
forall k a. Map k a
Map.empty
, stPostUsedNames :: Map String (DList String)
stPostUsedNames = Map String (DList String)
forall k a. Map k a
Map.empty
, stPostShadowingNames :: Map Name (DList String)
stPostShadowingNames = Map Name (DList String)
forall k a. Map k a
Map.empty
, stPostStatistics :: Statistics
stPostStatistics = Statistics
forall k a. Map k a
Map.empty
, stPostTCWarnings :: [TCWarning]
stPostTCWarnings = []
, stPostMutualBlocks :: Map MutualId MutualBlock
stPostMutualBlocks = Map MutualId MutualBlock
forall k a. Map k a
Map.empty
, stPostLocalBuiltins :: BuiltinThings PrimFun
stPostLocalBuiltins = BuiltinThings PrimFun
forall k a. Map k a
Map.empty
, stPostFreshMetaId :: MetaId
stPostFreshMetaId = MetaId
initialMetaId
, stPostFreshMutualId :: MutualId
stPostFreshMutualId = MutualId
0
, stPostFreshProblemId :: ProblemId
stPostFreshProblemId = ProblemId
1
, stPostFreshCheckpointId :: CheckpointId
stPostFreshCheckpointId = CheckpointId
1
, stPostFreshInt :: Int
stPostFreshInt = Int
0
, stPostFreshNameId :: NameId
stPostFreshNameId = Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
noModuleNameHash
, stPostFreshOpaqueId :: OpaqueId
stPostFreshOpaqueId = Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
0 ModuleNameHash
noModuleNameHash
, stPostAreWeCaching :: Bool
stPostAreWeCaching = Bool
False
, stPostPostponeInstanceSearch :: Bool
stPostPostponeInstanceSearch = Bool
False
, stPostConsideringInstance :: Bool
stPostConsideringInstance = Bool
False
, stPostInstantiateBlocking :: Bool
stPostInstantiateBlocking = Bool
False
, stPostLocalPartialDefs :: Set QName
stPostLocalPartialDefs = Set QName
forall a. Set a
Set.empty
, stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
stPostOpaqueBlocks = Map OpaqueId OpaqueBlock
forall k a. Map k a
Map.empty
, stPostOpaqueIds :: Map QName OpaqueId
stPostOpaqueIds = Map QName OpaqueId
forall k a. Map k a
Map.empty
, stPostForeignCode :: Map String ForeignCodeStack
stPostForeignCode = Map String ForeignCodeStack
forall k a. Map k a
Map.empty
}
initState :: TCState
initState :: TCState
initState = TCSt
{ stPreScopeState :: PreScopeState
stPreScopeState = PreScopeState
initPreScopeState
, stPostScopeState :: PostScopeState
stPostScopeState = PostScopeState
initPostScopeState
, stPersistentState :: PersistentTCState
stPersistentState = PersistentTCState
initPersistentState
}
stTokens :: Lens' TCState HighlightingInfo
stTokens :: Lens' TCState HighlightingInfo
stTokens HighlightingInfo -> f HighlightingInfo
f TCState
s =
HighlightingInfo -> f HighlightingInfo
f (PreScopeState -> HighlightingInfo
stPreTokens (TCState -> PreScopeState
stPreScopeState TCState
s)) f HighlightingInfo -> (HighlightingInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\HighlightingInfo
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreTokens = x}}
stImports :: Lens' TCState Signature
stImports :: Lens' TCState Signature
stImports Signature -> f Signature
f TCState
s =
Signature -> f Signature
f (PreScopeState -> Signature
stPreImports (TCState -> PreScopeState
stPreScopeState TCState
s)) f Signature -> (Signature -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Signature
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImports = x}}
stImportedModules ::
Lens' TCState (Set TopLevelModuleName)
stImportedModules :: Lens' TCState (Set TopLevelModuleName)
stImportedModules Set TopLevelModuleName -> f (Set TopLevelModuleName)
f TCState
s =
Set TopLevelModuleName -> f (Set TopLevelModuleName)
f (PreScopeState -> Set TopLevelModuleName
stPreImportedModules (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Set TopLevelModuleName)
-> (Set TopLevelModuleName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Set TopLevelModuleName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedModules = x}}
stModuleToSource :: Lens' TCState ModuleToSource
stModuleToSource :: Lens' TCState ModuleToSource
stModuleToSource ModuleToSource -> f ModuleToSource
f TCState
s =
ModuleToSource -> f ModuleToSource
f (PreScopeState -> ModuleToSource
stPreModuleToSource (TCState -> PreScopeState
stPreScopeState TCState
s)) f ModuleToSource -> (ModuleToSource -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ModuleToSource
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreModuleToSource = x}}
stVisitedModules :: Lens' TCState VisitedModules
stVisitedModules :: Lens' TCState VisitedModules
stVisitedModules VisitedModules -> f VisitedModules
f TCState
s =
VisitedModules -> f VisitedModules
f (PreScopeState -> VisitedModules
stPreVisitedModules (TCState -> PreScopeState
stPreScopeState TCState
s)) f VisitedModules -> (VisitedModules -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\VisitedModules
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreVisitedModules = x}}
stScope :: Lens' TCState ScopeInfo
stScope :: Lens' TCState ScopeInfo
stScope ScopeInfo -> f ScopeInfo
f TCState
s =
ScopeInfo -> f ScopeInfo
f (PreScopeState -> ScopeInfo
stPreScope (TCState -> PreScopeState
stPreScopeState TCState
s)) f ScopeInfo -> (ScopeInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ScopeInfo
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreScope = x}}
stPatternSyns :: Lens' TCState A.PatternSynDefns
stPatternSyns :: Lens' TCState PatternSynDefns
stPatternSyns PatternSynDefns -> f PatternSynDefns
f TCState
s =
PatternSynDefns -> f PatternSynDefns
f (PreScopeState -> PatternSynDefns
stPrePatternSyns (TCState -> PreScopeState
stPreScopeState TCState
s)) f PatternSynDefns -> (PatternSynDefns -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\PatternSynDefns
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePatternSyns = x}}
stPatternSynImports :: Lens' TCState A.PatternSynDefns
stPatternSynImports :: Lens' TCState PatternSynDefns
stPatternSynImports PatternSynDefns -> f PatternSynDefns
f TCState
s =
PatternSynDefns -> f PatternSynDefns
f (PreScopeState -> PatternSynDefns
stPrePatternSynImports (TCState -> PreScopeState
stPreScopeState TCState
s)) f PatternSynDefns -> (PatternSynDefns -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\PatternSynDefns
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePatternSynImports = x}}
stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
stGeneralizedVars Maybe (Set QName) -> f (Maybe (Set QName))
f TCState
s =
Maybe (Set QName) -> f (Maybe (Set QName))
f (Maybe (Set QName) -> Maybe (Set QName)
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe (Set QName) -> Maybe (Set QName))
-> Maybe (Set QName) -> Maybe (Set QName)
forall a b. (a -> b) -> a -> b
$ PreScopeState -> Maybe (Set QName)
stPreGeneralizedVars (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Maybe (Set QName))
-> (Maybe (Set QName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Maybe (Set QName)
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreGeneralizedVars = Strict.toStrict x}}
stPragmaOptions :: Lens' TCState PragmaOptions
stPragmaOptions :: Lens' TCState PragmaOptions
stPragmaOptions PragmaOptions -> f PragmaOptions
f TCState
s =
PragmaOptions -> f PragmaOptions
f (PreScopeState -> PragmaOptions
stPrePragmaOptions (TCState -> PreScopeState
stPreScopeState TCState
s)) f PragmaOptions -> (PragmaOptions -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\PragmaOptions
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePragmaOptions = x}}
stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f TCState
s =
BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f (PreScopeState -> BuiltinThings PrimFun
stPreImportedBuiltins (TCState -> PreScopeState
stPreScopeState TCState
s)) f (BuiltinThings PrimFun)
-> (BuiltinThings PrimFun -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\BuiltinThings PrimFun
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedBuiltins = x}}
stForeignCode :: Lens' TCState (Map BackendName ForeignCodeStack)
stForeignCode :: Lens' TCState (Map String ForeignCodeStack)
stForeignCode Map String ForeignCodeStack -> f (Map String ForeignCodeStack)
f TCState
s =
Map String ForeignCodeStack -> f (Map String ForeignCodeStack)
f (PostScopeState -> Map String ForeignCodeStack
stPostForeignCode (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map String ForeignCodeStack)
-> (Map String ForeignCodeStack -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map String ForeignCodeStack
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostForeignCode = x}}
stFreshInteractionId :: Lens' TCState InteractionId
stFreshInteractionId :: Lens' TCState InteractionId
stFreshInteractionId InteractionId -> f InteractionId
f TCState
s =
InteractionId -> f InteractionId
f (PreScopeState -> InteractionId
stPreFreshInteractionId (TCState -> PreScopeState
stPreScopeState TCState
s)) f InteractionId -> (InteractionId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\InteractionId
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}
stImportedUserWarnings :: Lens' TCState (Map A.QName Text)
stImportedUserWarnings :: Lens' TCState (Map QName Text)
stImportedUserWarnings Map QName Text -> f (Map QName Text)
f TCState
s =
Map QName Text -> f (Map QName Text)
f (PreScopeState -> Map QName Text
stPreImportedUserWarnings (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map QName Text) -> (Map QName Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Map QName Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}}
stLocalUserWarnings :: Lens' TCState (Map A.QName Text)
stLocalUserWarnings :: Lens' TCState (Map QName Text)
stLocalUserWarnings Map QName Text -> f (Map QName Text)
f TCState
s =
Map QName Text -> f (Map QName Text)
f (PreScopeState -> Map QName Text
stPreLocalUserWarnings (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map QName Text) -> (Map QName Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Map QName Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}}
getUserWarnings :: ReadTCState m => m (Map A.QName Text)
getUserWarnings :: forall (m :: * -> *). ReadTCState m => m (Map QName Text)
getUserWarnings = do
Map QName Text
iuw <- Lens' TCState (Map QName Text) -> m (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map QName Text -> f (Map QName Text)) -> TCState -> f TCState
Lens' TCState (Map QName Text)
stImportedUserWarnings
Map QName Text
luw <- Lens' TCState (Map QName Text) -> m (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map QName Text -> f (Map QName Text)) -> TCState -> f TCState
Lens' TCState (Map QName Text)
stLocalUserWarnings
Map QName Text -> m (Map QName Text)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map QName Text -> m (Map QName Text))
-> Map QName Text -> m (Map QName Text)
forall a b. (a -> b) -> a -> b
$ Map QName Text
iuw Map QName Text -> Map QName Text -> Map QName Text
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map QName Text
luw
stWarningOnImport :: Lens' TCState (Maybe Text)
stWarningOnImport :: Lens' TCState (Maybe Text)
stWarningOnImport Maybe Text -> f (Maybe Text)
f TCState
s =
Maybe Text -> f (Maybe Text)
f (Maybe Text -> Maybe Text
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe Text -> Maybe Text) -> Maybe Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ PreScopeState -> Maybe Text
stPreWarningOnImport (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Maybe Text) -> (Maybe Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Maybe Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreWarningOnImport = Strict.toStrict x}}
stImportedPartialDefs :: Lens' TCState (Set QName)
stImportedPartialDefs :: Lens' TCState (Set QName)
stImportedPartialDefs Set QName -> f (Set QName)
f TCState
s =
Set QName -> f (Set QName)
f (PreScopeState -> Set QName
stPreImportedPartialDefs (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Set QName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedPartialDefs = x}}
stLocalPartialDefs :: Lens' TCState (Set QName)
stLocalPartialDefs :: Lens' TCState (Set QName)
stLocalPartialDefs Set QName -> f (Set QName)
f TCState
s =
Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostLocalPartialDefs (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Set QName
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostLocalPartialDefs = x}}
getPartialDefs :: ReadTCState m => m (Set QName)
getPartialDefs :: forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs = do
Set QName
ipd <- Lens' TCState (Set QName) -> m (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stImportedPartialDefs
Set QName
lpd <- Lens' TCState (Set QName) -> m (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stLocalPartialDefs
Set QName -> m (Set QName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set QName -> m (Set QName)) -> Set QName -> m (Set QName)
forall a b. (a -> b) -> a -> b
$ Set QName
ipd Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set QName
lpd
stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
stLoadedFileCache Maybe LoadedFileCache -> f (Maybe LoadedFileCache)
f TCState
s =
Maybe LoadedFileCache -> f (Maybe LoadedFileCache)
f (Maybe LoadedFileCache -> Maybe LoadedFileCache
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> Maybe LoadedFileCache -> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> Maybe LoadedFileCache
stPersistLoadedFileCache (TCState -> PersistentTCState
stPersistentState TCState
s)) f (Maybe LoadedFileCache)
-> (Maybe LoadedFileCache -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Maybe LoadedFileCache
x -> TCState
s {stPersistentState = (stPersistentState s) {stPersistLoadedFileCache = Strict.toStrict x}}
stBackends :: Lens' TCState [Backend_boot TCM]
stBackends :: Lens' TCState [Backend_boot (TCMT IO)]
stBackends [Backend_boot (TCMT IO)] -> f [Backend_boot (TCMT IO)]
f TCState
s =
[Backend_boot (TCMT IO)] -> f [Backend_boot (TCMT IO)]
f (PersistentTCState -> [Backend_boot (TCMT IO)]
stPersistBackends (TCState -> PersistentTCState
stPersistentState TCState
s)) f [Backend_boot (TCMT IO)]
-> ([Backend_boot (TCMT IO)] -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\[Backend_boot (TCMT IO)]
x -> TCState
s {stPersistentState = (stPersistentState s) {stPersistBackends = x}}
stProjectConfigs :: Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs :: Lens' TCState (Map String ProjectConfig)
stProjectConfigs Map String ProjectConfig -> f (Map String ProjectConfig)
f TCState
s =
Map String ProjectConfig -> f (Map String ProjectConfig)
f (PreScopeState -> Map String ProjectConfig
stPreProjectConfigs (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map String ProjectConfig)
-> (Map String ProjectConfig -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Map String ProjectConfig
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreProjectConfigs = x}}
stAgdaLibFiles :: Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles :: Lens' TCState (Map String AgdaLibFile)
stAgdaLibFiles Map String AgdaLibFile -> f (Map String AgdaLibFile)
f TCState
s =
Map String AgdaLibFile -> f (Map String AgdaLibFile)
f (PreScopeState -> Map String AgdaLibFile
stPreAgdaLibFiles (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map String AgdaLibFile)
-> (Map String AgdaLibFile -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ Map String AgdaLibFile
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreAgdaLibFiles = x}}
stTopLevelModuleNames ::
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames :: Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames BiMap RawTopLevelModuleName ModuleNameHash
-> f (BiMap RawTopLevelModuleName ModuleNameHash)
f TCState
s =
BiMap RawTopLevelModuleName ModuleNameHash
-> f (BiMap RawTopLevelModuleName ModuleNameHash)
f (PersistentTCState -> BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames (TCState -> PersistentTCState
stPersistentState TCState
s)) f (BiMap RawTopLevelModuleName ModuleNameHash)
-> (BiMap RawTopLevelModuleName ModuleNameHash -> TCState)
-> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ BiMap RawTopLevelModuleName ModuleNameHash
x -> TCState
s {stPersistentState =
(stPersistentState s) {stPersistentTopLevelModuleNames = x}}
stImportedMetaStore :: Lens' TCState RemoteMetaStore
stImportedMetaStore :: Lens' TCState RemoteMetaStore
stImportedMetaStore RemoteMetaStore -> f RemoteMetaStore
f TCState
s =
RemoteMetaStore -> f RemoteMetaStore
f (PreScopeState -> RemoteMetaStore
stPreImportedMetaStore (TCState -> PreScopeState
stPreScopeState TCState
s)) f RemoteMetaStore -> (RemoteMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\RemoteMetaStore
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedMetaStore = x}}
stCopiedNames :: Lens' TCState (HashMap QName QName)
stCopiedNames :: Lens' TCState (HashMap QName QName)
stCopiedNames HashMap QName QName -> f (HashMap QName QName)
f TCState
s =
HashMap QName QName -> f (HashMap QName QName)
f (PreScopeState -> HashMap QName QName
stPreCopiedNames (TCState -> PreScopeState
stPreScopeState TCState
s)) f (HashMap QName QName)
-> (HashMap QName QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\HashMap QName QName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreCopiedNames = x}}
stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
stNameCopies HashMap QName (HashSet QName) -> f (HashMap QName (HashSet QName))
f TCState
s =
HashMap QName (HashSet QName) -> f (HashMap QName (HashSet QName))
f (PreScopeState -> HashMap QName (HashSet QName)
stPreNameCopies (TCState -> PreScopeState
stPreScopeState TCState
s)) f (HashMap QName (HashSet QName))
-> (HashMap QName (HashSet QName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\HashMap QName (HashSet QName)
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreNameCopies = x}}
stFreshNameId :: Lens' TCState NameId
stFreshNameId :: Lens' TCState NameId
stFreshNameId NameId -> f NameId
f TCState
s =
NameId -> f NameId
f (PostScopeState -> NameId
stPostFreshNameId (TCState -> PostScopeState
stPostScopeState TCState
s)) f NameId -> (NameId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\NameId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshNameId = x}}
stFreshOpaqueId :: Lens' TCState OpaqueId
stFreshOpaqueId :: Lens' TCState OpaqueId
stFreshOpaqueId OpaqueId -> f OpaqueId
f TCState
s =
OpaqueId -> f OpaqueId
f (PostScopeState -> OpaqueId
stPostFreshOpaqueId (TCState -> PostScopeState
stPostScopeState TCState
s)) f OpaqueId -> (OpaqueId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\OpaqueId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshOpaqueId = x}}
stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock)
f TCState
s =
Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock)
f (PostScopeState -> Map OpaqueId OpaqueBlock
stPostOpaqueBlocks (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map OpaqueId OpaqueBlock)
-> (Map OpaqueId OpaqueBlock -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map OpaqueId OpaqueBlock
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpaqueBlocks = x}}
stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
stOpaqueIds Map QName OpaqueId -> f (Map QName OpaqueId)
f TCState
s =
Map QName OpaqueId -> f (Map QName OpaqueId)
f (PostScopeState -> Map QName OpaqueId
stPostOpaqueIds (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map QName OpaqueId)
-> (Map QName OpaqueId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map QName OpaqueId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpaqueIds = x}}
stSyntaxInfo :: Lens' TCState HighlightingInfo
stSyntaxInfo :: Lens' TCState HighlightingInfo
stSyntaxInfo HighlightingInfo -> f HighlightingInfo
f TCState
s =
HighlightingInfo -> f HighlightingInfo
f (PostScopeState -> HighlightingInfo
stPostSyntaxInfo (TCState -> PostScopeState
stPostScopeState TCState
s)) f HighlightingInfo -> (HighlightingInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\HighlightingInfo
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSyntaxInfo = x}}
stDisambiguatedNames :: Lens' TCState DisambiguatedNames
stDisambiguatedNames :: Lens' TCState DisambiguatedNames
stDisambiguatedNames DisambiguatedNames -> f DisambiguatedNames
f TCState
s =
DisambiguatedNames -> f DisambiguatedNames
f (PostScopeState -> DisambiguatedNames
stPostDisambiguatedNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f DisambiguatedNames
-> (DisambiguatedNames -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\DisambiguatedNames
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostDisambiguatedNames = x}}
stOpenMetaStore :: Lens' TCState LocalMetaStore
stOpenMetaStore :: Lens' TCState LocalMetaStore
stOpenMetaStore LocalMetaStore -> f LocalMetaStore
f TCState
s =
LocalMetaStore -> f LocalMetaStore
f (PostScopeState -> LocalMetaStore
stPostOpenMetaStore (TCState -> PostScopeState
stPostScopeState TCState
s)) f LocalMetaStore -> (LocalMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\LocalMetaStore
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpenMetaStore = x}}
stSolvedMetaStore :: Lens' TCState LocalMetaStore
stSolvedMetaStore :: Lens' TCState LocalMetaStore
stSolvedMetaStore LocalMetaStore -> f LocalMetaStore
f TCState
s =
LocalMetaStore -> f LocalMetaStore
f (PostScopeState -> LocalMetaStore
stPostSolvedMetaStore (TCState -> PostScopeState
stPostScopeState TCState
s)) f LocalMetaStore -> (LocalMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\LocalMetaStore
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSolvedMetaStore = x}}
stInteractionPoints :: Lens' TCState InteractionPoints
stInteractionPoints :: Lens' TCState InteractionPoints
stInteractionPoints InteractionPoints -> f InteractionPoints
f TCState
s =
InteractionPoints -> f InteractionPoints
f (PostScopeState -> InteractionPoints
stPostInteractionPoints (TCState -> PostScopeState
stPostScopeState TCState
s)) f InteractionPoints -> (InteractionPoints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\InteractionPoints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}}
stAwakeConstraints :: Lens' TCState Constraints
stAwakeConstraints :: Lens' TCState Constraints
stAwakeConstraints Constraints -> f Constraints
f TCState
s =
Constraints -> f Constraints
f (PostScopeState -> Constraints
stPostAwakeConstraints (TCState -> PostScopeState
stPostScopeState TCState
s)) f Constraints -> (Constraints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Constraints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostAwakeConstraints = x}}
stSleepingConstraints :: Lens' TCState Constraints
stSleepingConstraints :: Lens' TCState Constraints
stSleepingConstraints Constraints -> f Constraints
f TCState
s =
Constraints -> f Constraints
f (PostScopeState -> Constraints
stPostSleepingConstraints (TCState -> PostScopeState
stPostScopeState TCState
s)) f Constraints -> (Constraints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Constraints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSleepingConstraints = x}}
stDirty :: Lens' TCState Bool
stDirty :: Lens' TCState Bool
stDirty Bool -> f Bool
f TCState
s =
Bool -> f Bool
f (PostScopeState -> Bool
stPostDirty (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostDirty = x}}
stOccursCheckDefs :: Lens' TCState (Set QName)
stOccursCheckDefs :: Lens' TCState (Set QName)
stOccursCheckDefs Set QName -> f (Set QName)
f TCState
s =
Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostOccursCheckDefs (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Set QName
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOccursCheckDefs = x}}
stSignature :: Lens' TCState Signature
stSignature :: Lens' TCState Signature
stSignature Signature -> f Signature
f TCState
s =
Signature -> f Signature
f (PostScopeState -> Signature
stPostSignature (TCState -> PostScopeState
stPostScopeState TCState
s)) f Signature -> (Signature -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Signature
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}}
stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId)
f TCState
s =
Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId)
f (PostScopeState -> Map ModuleName CheckpointId
stPostModuleCheckpoints (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map ModuleName CheckpointId)
-> (Map ModuleName CheckpointId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map ModuleName CheckpointId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostModuleCheckpoints = x}}
stImportsDisplayForms :: Lens' TCState DisplayForms
stImportsDisplayForms :: Lens' TCState DisplayForms
stImportsDisplayForms DisplayForms -> f DisplayForms
f TCState
s =
DisplayForms -> f DisplayForms
f (PostScopeState -> DisplayForms
stPostImportsDisplayForms (TCState -> PostScopeState
stPostScopeState TCState
s)) f DisplayForms -> (DisplayForms -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\DisplayForms
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostImportsDisplayForms = x}}
stImportedDisplayForms :: Lens' TCState DisplayForms
stImportedDisplayForms :: Lens' TCState DisplayForms
stImportedDisplayForms DisplayForms -> f DisplayForms
f TCState
s =
DisplayForms -> f DisplayForms
f (PreScopeState -> DisplayForms
stPreImportedDisplayForms (TCState -> PreScopeState
stPreScopeState TCState
s)) f DisplayForms -> (DisplayForms -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\DisplayForms
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}}
stCurrentModule ::
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule :: Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName))
f TCState
s =
Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName))
f (PostScopeState -> Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Maybe (ModuleName, TopLevelModuleName))
-> (Maybe (ModuleName, TopLevelModuleName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Maybe (ModuleName, TopLevelModuleName)
x -> TCState
s {stPostScopeState =
(stPostScopeState s)
{stPostCurrentModule = case x of
Maybe (ModuleName, TopLevelModuleName)
Nothing -> Maybe (ModuleName, TopLevelModuleName)
forall a. Maybe a
Nothing
Just (!ModuleName
m, !TopLevelModuleName
top) -> (ModuleName, TopLevelModuleName)
-> Maybe (ModuleName, TopLevelModuleName)
forall a. a -> Maybe a
Just (ModuleName
m, TopLevelModuleName
top)}}
stInstanceDefs :: Lens' TCState TempInstanceTable
stInstanceDefs :: Lens' TCState TempInstanceTable
stInstanceDefs TempInstanceTable -> f TempInstanceTable
f TCState
s =
TempInstanceTable -> f TempInstanceTable
f ( TCState
s TCState -> Lens' TCState InstanceTable -> InstanceTable
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> (InstanceTable -> f InstanceTable)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances
, PostScopeState -> Set QName
stPostPendingInstances (TCState -> PostScopeState
stPostScopeState TCState
s)
)
f TempInstanceTable -> (TempInstanceTable -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(InstanceTable
t, Set QName
x) ->
Lens' TCState InstanceTable -> LensSet TCState InstanceTable
forall o i. Lens' o i -> LensSet o i
set ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> (InstanceTable -> f InstanceTable)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances) InstanceTable
t
(TCState
s { stPostScopeState = (stPostScopeState s) { stPostPendingInstances = x }})
stTemporaryInstances :: Lens' TCState (Set QName)
stTemporaryInstances :: Lens' TCState (Set QName)
stTemporaryInstances Set QName -> f (Set QName)
f TCState
s = Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostTemporaryInstances (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Set QName
x -> TCState
s {
stPostScopeState = (stPostScopeState s) { stPostTemporaryInstances = x } }
stInstanceTree :: Lens' TCState (DiscrimTree QName)
stInstanceTree :: Lens' TCState (DiscrimTree QName)
stInstanceTree = (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((DiscrimTree QName -> f (DiscrimTree QName))
-> Signature -> f Signature)
-> (DiscrimTree QName -> f (DiscrimTree QName))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> ((DiscrimTree QName -> f (DiscrimTree QName))
-> InstanceTable -> f InstanceTable)
-> (DiscrimTree QName -> f (DiscrimTree QName))
-> Signature
-> f Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DiscrimTree QName -> f (DiscrimTree QName))
-> InstanceTable -> f InstanceTable
Lens' InstanceTable (DiscrimTree QName)
itableTree
stConcreteNames :: Lens' TCState ConcreteNames
stConcreteNames :: Lens' TCState ConcreteNames
stConcreteNames ConcreteNames -> f ConcreteNames
f TCState
s =
ConcreteNames -> f ConcreteNames
f (PostScopeState -> ConcreteNames
stPostConcreteNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f ConcreteNames -> (ConcreteNames -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ConcreteNames
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostConcreteNames = x}}
stUsedNames :: Lens' TCState (Map RawName (DList RawName))
stUsedNames :: Lens' TCState (Map String (DList String))
stUsedNames Map String (DList String) -> f (Map String (DList String))
f TCState
s =
Map String (DList String) -> f (Map String (DList String))
f (PostScopeState -> Map String (DList String)
stPostUsedNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map String (DList String))
-> (Map String (DList String) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map String (DList String)
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostUsedNames = x}}
stShadowingNames :: Lens' TCState (Map Name (DList RawName))
stShadowingNames :: Lens' TCState (Map Name (DList String))
stShadowingNames Map Name (DList String) -> f (Map Name (DList String))
f TCState
s =
Map Name (DList String) -> f (Map Name (DList String))
f (PostScopeState -> Map Name (DList String)
stPostShadowingNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map Name (DList String))
-> (Map Name (DList String) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map Name (DList String)
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostShadowingNames = x}}
stStatistics :: Lens' TCState Statistics
stStatistics :: Lens' TCState Statistics
stStatistics Statistics -> f Statistics
f TCState
s =
Statistics -> f Statistics
f (PostScopeState -> Statistics
stPostStatistics (TCState -> PostScopeState
stPostScopeState TCState
s)) f Statistics -> (Statistics -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Statistics
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}}
stTCWarnings :: Lens' TCState [TCWarning]
stTCWarnings :: Lens' TCState [TCWarning]
stTCWarnings [TCWarning] -> f [TCWarning]
f TCState
s =
[TCWarning] -> f [TCWarning]
f (PostScopeState -> [TCWarning]
stPostTCWarnings (TCState -> PostScopeState
stPostScopeState TCState
s)) f [TCWarning] -> ([TCWarning] -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\[TCWarning]
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}}
stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks Map MutualId MutualBlock -> f (Map MutualId MutualBlock)
f TCState
s =
Map MutualId MutualBlock -> f (Map MutualId MutualBlock)
f (PostScopeState -> Map MutualId MutualBlock
stPostMutualBlocks (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map MutualId MutualBlock)
-> (Map MutualId MutualBlock -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Map MutualId MutualBlock
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}}
stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f TCState
s =
BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f (PostScopeState -> BuiltinThings PrimFun
stPostLocalBuiltins (TCState -> PostScopeState
stPostScopeState TCState
s)) f (BuiltinThings PrimFun)
-> (BuiltinThings PrimFun -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\BuiltinThings PrimFun
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostLocalBuiltins = x}}
stFreshMetaId :: Lens' TCState MetaId
stFreshMetaId :: Lens' TCState MetaId
stFreshMetaId MetaId -> f MetaId
f TCState
s =
MetaId -> f MetaId
f (PostScopeState -> MetaId
stPostFreshMetaId (TCState -> PostScopeState
stPostScopeState TCState
s)) f MetaId -> (MetaId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\MetaId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshMetaId = x}}
stFreshMutualId :: Lens' TCState MutualId
stFreshMutualId :: Lens' TCState MutualId
stFreshMutualId MutualId -> f MutualId
f TCState
s =
MutualId -> f MutualId
f (PostScopeState -> MutualId
stPostFreshMutualId (TCState -> PostScopeState
stPostScopeState TCState
s)) f MutualId -> (MutualId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\MutualId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshMutualId = x}}
stFreshProblemId :: Lens' TCState ProblemId
stFreshProblemId :: Lens' TCState ProblemId
stFreshProblemId ProblemId -> f ProblemId
f TCState
s =
ProblemId -> f ProblemId
f (PostScopeState -> ProblemId
stPostFreshProblemId (TCState -> PostScopeState
stPostScopeState TCState
s)) f ProblemId -> (ProblemId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\ProblemId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshProblemId = x}}
stFreshCheckpointId :: Lens' TCState CheckpointId
stFreshCheckpointId :: Lens' TCState CheckpointId
stFreshCheckpointId CheckpointId -> f CheckpointId
f TCState
s =
CheckpointId -> f CheckpointId
f (PostScopeState -> CheckpointId
stPostFreshCheckpointId (TCState -> PostScopeState
stPostScopeState TCState
s)) f CheckpointId -> (CheckpointId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\CheckpointId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshCheckpointId = x}}
stFreshInt :: Lens' TCState Int
stFreshInt :: Lens' TCState Int
stFreshInt Int -> f Int
f TCState
s =
Int -> f Int
f (PostScopeState -> Int
stPostFreshInt (TCState -> PostScopeState
stPostScopeState TCState
s)) f Int -> (Int -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Int
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshInt = x}}
stAreWeCaching :: Lens' TCState Bool
stAreWeCaching :: Lens' TCState Bool
stAreWeCaching Bool -> f Bool
f TCState
s =
Bool -> f Bool
f (PostScopeState -> Bool
stPostAreWeCaching (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostAreWeCaching = x}}
stPostponeInstanceSearch :: Lens' TCState Bool
stPostponeInstanceSearch :: Lens' TCState Bool
stPostponeInstanceSearch Bool -> f Bool
f TCState
s =
Bool -> f Bool
f (PostScopeState -> Bool
stPostPostponeInstanceSearch (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostPostponeInstanceSearch = x}}
stConsideringInstance :: Lens' TCState Bool
stConsideringInstance :: Lens' TCState Bool
stConsideringInstance Bool -> f Bool
f TCState
s =
Bool -> f Bool
f (PostScopeState -> Bool
stPostConsideringInstance (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostConsideringInstance = x}}
stInstantiateBlocking :: Lens' TCState Bool
stInstantiateBlocking :: Lens' TCState Bool
stInstantiateBlocking Bool -> f Bool
f TCState
s =
Bool -> f Bool
f (PostScopeState -> Bool
stPostInstantiateBlocking (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostInstantiateBlocking = x}}
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings TCState
s = (Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
-> BuiltinThings PrimFun
-> BuiltinThings PrimFun
-> BuiltinThings PrimFun
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin (TCState
s TCState
-> Lens' TCState (BuiltinThings PrimFun) -> BuiltinThings PrimFun
forall o i. o -> Lens' o i -> i
^. (BuiltinThings PrimFun -> f (BuiltinThings PrimFun))
-> TCState -> f TCState
Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins) (TCState
s TCState
-> Lens' TCState (BuiltinThings PrimFun) -> BuiltinThings PrimFun
forall o i. o -> Lens' o i -> i
^. (BuiltinThings PrimFun -> f (BuiltinThings PrimFun))
-> TCState -> f TCState
Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins)
unionBuiltin :: Builtin a -> Builtin a -> Builtin a
unionBuiltin :: forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin = ((Builtin a, Builtin a) -> Builtin a)
-> Builtin a -> Builtin a -> Builtin a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Builtin a, Builtin a) -> Builtin a)
-> Builtin a -> Builtin a -> Builtin a)
-> ((Builtin a, Builtin a) -> Builtin a)
-> Builtin a
-> Builtin a
-> Builtin a
forall a b. (a -> b) -> a -> b
$ \case
(BuiltinRewriteRelations Set QName
xs, BuiltinRewriteRelations Set QName
ys) -> Set QName -> Builtin a
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations (Set QName -> Builtin a) -> Set QName -> Builtin a
forall a b. (a -> b) -> a -> b
$ Set QName
xs Set QName -> Set QName -> Set QName
forall a. Semigroup a => a -> a -> a
<> Set QName
ys
(Builtin a, Builtin a)
_ -> Builtin a
forall a. HasCallStack => a
__IMPOSSIBLE__
class Enum i => HasFresh i where
freshLens :: Lens' TCState i
nextFresh' :: i -> i
nextFresh' = i -> i
forall a. Enum a => a -> a
succ
{-# INLINE nextFresh #-}
nextFresh :: HasFresh i => TCState -> (i, TCState)
nextFresh :: forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
s =
let !c :: i
c = TCState
s TCState -> Lens' TCState i -> i
forall o i. o -> Lens' o i -> i
^. (i -> f i) -> TCState -> f TCState
forall i. HasFresh i => Lens' TCState i
Lens' TCState i
freshLens
!next :: TCState
next = Lens' TCState i -> LensSet TCState i
forall o i. Lens' o i -> LensSet o i
set (i -> f i) -> TCState -> f TCState
forall i. HasFresh i => Lens' TCState i
Lens' TCState i
freshLens (i -> i
forall i. HasFresh i => i -> i
nextFresh' i
c) TCState
s
in (i
c, TCState
next)
class Monad m => MonadFresh i m where
fresh :: m i
default fresh :: (MonadTrans t, MonadFresh i n, t n ~ m) => m i
fresh = n i -> t n i
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n i
forall i (m :: * -> *). MonadFresh i m => m i
fresh
instance MonadFresh i m => MonadFresh i (ReaderT r m)
instance MonadFresh i m => MonadFresh i (StateT s m)
instance MonadFresh i m => MonadFresh i (ListT m)
instance MonadFresh i m => MonadFresh i (IdentityT m)
instance HasFresh i => MonadFresh i TCM where
fresh :: TCM i
fresh = do
!TCState
s <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
let (!i
c , !TCState
s') = TCState -> (i, TCState)
forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
s
TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s'
i -> TCM i
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return i
c
{-# INLINE fresh #-}
instance HasFresh MetaId where
freshLens :: Lens' TCState MetaId
freshLens = (MetaId -> f MetaId) -> TCState -> f TCState
Lens' TCState MetaId
stFreshMetaId
instance HasFresh MutualId where
freshLens :: Lens' TCState MutualId
freshLens = (MutualId -> f MutualId) -> TCState -> f TCState
Lens' TCState MutualId
stFreshMutualId
instance HasFresh InteractionId where
freshLens :: Lens' TCState InteractionId
freshLens = (InteractionId -> f InteractionId) -> TCState -> f TCState
Lens' TCState InteractionId
stFreshInteractionId
instance HasFresh NameId where
freshLens :: Lens' TCState NameId
freshLens = (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId
nextFresh' :: NameId -> NameId
nextFresh' = NameId -> NameId
forall a. Enum a => a -> a
succ (NameId -> NameId) -> (NameId -> NameId) -> NameId -> NameId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameId -> NameId
forall a. Enum a => a -> a
succ
instance HasFresh OpaqueId where
freshLens :: Lens' TCState OpaqueId
freshLens = (OpaqueId -> f OpaqueId) -> TCState -> f TCState
Lens' TCState OpaqueId
stFreshOpaqueId
instance HasFresh Int where
freshLens :: Lens' TCState Int
freshLens = (Int -> f Int) -> TCState -> f TCState
Lens' TCState Int
stFreshInt
instance HasFresh ProblemId where
freshLens :: Lens' TCState ProblemId
freshLens = (ProblemId -> f ProblemId) -> TCState -> f TCState
Lens' TCState ProblemId
stFreshProblemId
newtype CheckpointId = CheckpointId Int
deriving (CheckpointId -> CheckpointId -> Bool
(CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool) -> Eq CheckpointId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckpointId -> CheckpointId -> Bool
== :: CheckpointId -> CheckpointId -> Bool
$c/= :: CheckpointId -> CheckpointId -> Bool
/= :: CheckpointId -> CheckpointId -> Bool
Eq, Eq CheckpointId
Eq CheckpointId =>
(CheckpointId -> CheckpointId -> Ordering)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> Ord CheckpointId
CheckpointId -> CheckpointId -> Bool
CheckpointId -> CheckpointId -> Ordering
CheckpointId -> CheckpointId -> CheckpointId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CheckpointId -> CheckpointId -> Ordering
compare :: CheckpointId -> CheckpointId -> Ordering
$c< :: CheckpointId -> CheckpointId -> Bool
< :: CheckpointId -> CheckpointId -> Bool
$c<= :: CheckpointId -> CheckpointId -> Bool
<= :: CheckpointId -> CheckpointId -> Bool
$c> :: CheckpointId -> CheckpointId -> Bool
> :: CheckpointId -> CheckpointId -> Bool
$c>= :: CheckpointId -> CheckpointId -> Bool
>= :: CheckpointId -> CheckpointId -> Bool
$cmax :: CheckpointId -> CheckpointId -> CheckpointId
max :: CheckpointId -> CheckpointId -> CheckpointId
$cmin :: CheckpointId -> CheckpointId -> CheckpointId
min :: CheckpointId -> CheckpointId -> CheckpointId
Ord, Int -> CheckpointId
CheckpointId -> Int
CheckpointId -> [CheckpointId]
CheckpointId -> CheckpointId
CheckpointId -> CheckpointId -> [CheckpointId]
CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
(CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (Int -> CheckpointId)
-> (CheckpointId -> Int)
-> (CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId])
-> Enum CheckpointId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: CheckpointId -> CheckpointId
succ :: CheckpointId -> CheckpointId
$cpred :: CheckpointId -> CheckpointId
pred :: CheckpointId -> CheckpointId
$ctoEnum :: Int -> CheckpointId
toEnum :: Int -> CheckpointId
$cfromEnum :: CheckpointId -> Int
fromEnum :: CheckpointId -> Int
$cenumFrom :: CheckpointId -> [CheckpointId]
enumFrom :: CheckpointId -> [CheckpointId]
$cenumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId]
enumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId]
$cenumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId]
enumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId]
$cenumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
enumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
Enum, Num CheckpointId
Ord CheckpointId
(Num CheckpointId, Ord CheckpointId) =>
(CheckpointId -> Rational) -> Real CheckpointId
CheckpointId -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
$ctoRational :: CheckpointId -> Rational
toRational :: CheckpointId -> Rational
Real, Enum CheckpointId
Real CheckpointId
(Real CheckpointId, Enum CheckpointId) =>
(CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId))
-> (CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId))
-> (CheckpointId -> Integer)
-> Integral CheckpointId
CheckpointId -> Integer
CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
CheckpointId -> CheckpointId -> CheckpointId
forall a.
(Real a, Enum a) =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: CheckpointId -> CheckpointId -> CheckpointId
quot :: CheckpointId -> CheckpointId -> CheckpointId
$crem :: CheckpointId -> CheckpointId -> CheckpointId
rem :: CheckpointId -> CheckpointId -> CheckpointId
$cdiv :: CheckpointId -> CheckpointId -> CheckpointId
div :: CheckpointId -> CheckpointId -> CheckpointId
$cmod :: CheckpointId -> CheckpointId -> CheckpointId
mod :: CheckpointId -> CheckpointId -> CheckpointId
$cquotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
quotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
$cdivMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
divMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
$ctoInteger :: CheckpointId -> Integer
toInteger :: CheckpointId -> Integer
Integral, Integer -> CheckpointId
CheckpointId -> CheckpointId
CheckpointId -> CheckpointId -> CheckpointId
(CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (Integer -> CheckpointId)
-> Num CheckpointId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: CheckpointId -> CheckpointId -> CheckpointId
+ :: CheckpointId -> CheckpointId -> CheckpointId
$c- :: CheckpointId -> CheckpointId -> CheckpointId
- :: CheckpointId -> CheckpointId -> CheckpointId
$c* :: CheckpointId -> CheckpointId -> CheckpointId
* :: CheckpointId -> CheckpointId -> CheckpointId
$cnegate :: CheckpointId -> CheckpointId
negate :: CheckpointId -> CheckpointId
$cabs :: CheckpointId -> CheckpointId
abs :: CheckpointId -> CheckpointId
$csignum :: CheckpointId -> CheckpointId
signum :: CheckpointId -> CheckpointId
$cfromInteger :: Integer -> CheckpointId
fromInteger :: Integer -> CheckpointId
Num, CheckpointId -> ()
(CheckpointId -> ()) -> NFData CheckpointId
forall a. (a -> ()) -> NFData a
$crnf :: CheckpointId -> ()
rnf :: CheckpointId -> ()
NFData)
instance Show CheckpointId where
show :: CheckpointId -> String
show (CheckpointId Int
n) = Int -> String
forall a. Show a => a -> String
show Int
n
instance Pretty CheckpointId where
pretty :: CheckpointId -> Doc
pretty (CheckpointId Int
n) = Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n
instance HasFresh CheckpointId where
freshLens :: Lens' TCState CheckpointId
freshLens = (CheckpointId -> f CheckpointId) -> TCState -> f TCState
Lens' TCState CheckpointId
stFreshCheckpointId
freshName :: MonadFresh NameId m => Range -> String -> m Name
freshName :: forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName Range
r String
s = do
NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ Range -> NameId -> String -> Name
forall a. MkName a => Range -> NameId -> a -> Name
mkName Range
r NameId
i String
s
freshNoName :: MonadFresh NameId m => Range -> m Name
freshNoName :: forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName Range
r =
do NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i (Range -> NameId -> Name
C.NoName Range
forall a. Range' a
noRange NameId
i) Range
r Fixity'
noFixity' Bool
False
freshNoName_ :: MonadFresh NameId m => m Name
freshNoName_ :: forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_ = Range -> m Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName Range
forall a. Range' a
noRange
freshRecordName :: MonadFresh NameId m => m Name
freshRecordName :: forall (m :: * -> *). MonadFresh NameId m => m Name
freshRecordName = do
NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i (Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> Name
C.simpleName String
"r") Range
forall a. Range' a
noRange Fixity'
noFixity' Bool
True
class FreshName a where
freshName_ :: MonadFresh NameId m => a -> m Name
instance FreshName (Range, String) where
freshName_ :: forall (m :: * -> *).
MonadFresh NameId m =>
(Range, String) -> m Name
freshName_ = (Range -> String -> m Name) -> (Range, String) -> m Name
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Range -> String -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName
instance FreshName String where
freshName_ :: forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ = Range -> String -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName Range
forall a. Range' a
noRange
instance FreshName Range where
freshName_ :: forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshName_ = Range -> m Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName
instance FreshName () where
freshName_ :: forall (m :: * -> *). MonadFresh NameId m => () -> m Name
freshName_ () = m Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_
type ModuleToSource = Map TopLevelModuleName AbsolutePath
class Monad m => MonadStConcreteNames m where
runStConcreteNames :: StateT ConcreteNames m a -> m a
useConcreteNames :: m ConcreteNames
useConcreteNames = StateT ConcreteNames m ConcreteNames -> m ConcreteNames
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames StateT ConcreteNames m ConcreteNames
forall s (m :: * -> *). MonadState s m => m s
get
modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
modifyConcreteNames = StateT ConcreteNames m () -> m ()
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m () -> m ())
-> ((ConcreteNames -> ConcreteNames) -> StateT ConcreteNames m ())
-> (ConcreteNames -> ConcreteNames)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> ConcreteNames) -> StateT ConcreteNames m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
instance MonadStConcreteNames TCM where
runStConcreteNames :: forall a. StateT ConcreteNames (TCMT IO) a -> TCM a
runStConcreteNames StateT ConcreteNames (TCMT IO) a
m = Lens' TCState ConcreteNames
-> (ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a
forall (m :: * -> *) a r.
MonadTCState m =>
Lens' TCState a -> (a -> m (r, a)) -> m r
stateTCLensM (ConcreteNames -> f ConcreteNames) -> TCState -> f TCState
Lens' TCState ConcreteNames
stConcreteNames ((ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a)
-> (ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames (TCMT IO) a
-> ConcreteNames -> TCMT IO (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (TCMT IO) a
m
instance MonadStConcreteNames m => MonadStConcreteNames (IdentityT m) where
runStConcreteNames :: forall a. StateT ConcreteNames (IdentityT m) a -> IdentityT m a
runStConcreteNames StateT ConcreteNames (IdentityT m) a
m = m a -> IdentityT m a
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames m a -> m a
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m a -> m a)
-> StateT ConcreteNames m a -> m a
forall a b. (a -> b) -> a -> b
$ (ConcreteNames -> m (a, ConcreteNames)) -> StateT ConcreteNames m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m (a, ConcreteNames))
-> StateT ConcreteNames m a)
-> (ConcreteNames -> m (a, ConcreteNames))
-> StateT ConcreteNames m a
forall a b. (a -> b) -> a -> b
$ IdentityT m (a, ConcreteNames) -> m (a, ConcreteNames)
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT m (a, ConcreteNames) -> m (a, ConcreteNames))
-> (ConcreteNames -> IdentityT m (a, ConcreteNames))
-> ConcreteNames
-> m (a, ConcreteNames)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ConcreteNames (IdentityT m) a
-> ConcreteNames -> IdentityT m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (IdentityT m) a
m
instance MonadStConcreteNames m => MonadStConcreteNames (ReaderT r m) where
runStConcreteNames :: forall a. StateT ConcreteNames (ReaderT r m) a -> ReaderT r m a
runStConcreteNames StateT ConcreteNames (ReaderT r m) a
m = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames m a -> m a
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m a -> m a)
-> (r -> StateT ConcreteNames m a) -> r -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> m (a, ConcreteNames)) -> StateT ConcreteNames m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m (a, ConcreteNames))
-> StateT ConcreteNames m a)
-> (r -> ConcreteNames -> m (a, ConcreteNames))
-> r
-> StateT ConcreteNames m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> r -> m (a, ConcreteNames))
-> r -> ConcreteNames -> m (a, ConcreteNames)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ReaderT r m (a, ConcreteNames) -> r -> m (a, ConcreteNames)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT r m (a, ConcreteNames) -> r -> m (a, ConcreteNames))
-> (ConcreteNames -> ReaderT r m (a, ConcreteNames))
-> ConcreteNames
-> r
-> m (a, ConcreteNames)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ConcreteNames (ReaderT r m) a
-> ConcreteNames -> ReaderT r m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (ReaderT r m) a
m)
instance MonadStConcreteNames m => MonadStConcreteNames (StateT s m) where
runStConcreteNames :: forall a. StateT ConcreteNames (StateT s m) a -> StateT s m a
runStConcreteNames StateT ConcreteNames (StateT s m) a
m = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> StateT ConcreteNames m (a, s) -> m (a, s)
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m (a, s) -> m (a, s))
-> StateT ConcreteNames m (a, s) -> m (a, s)
forall a b. (a -> b) -> a -> b
$ (ConcreteNames -> m ((a, s), ConcreteNames))
-> StateT ConcreteNames m (a, s)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m ((a, s), ConcreteNames))
-> StateT ConcreteNames m (a, s))
-> (ConcreteNames -> m ((a, s), ConcreteNames))
-> StateT ConcreteNames m (a, s)
forall a b. (a -> b) -> a -> b
$ \ConcreteNames
ns -> do
((a
x,ConcreteNames
ns'),s
s') <- StateT s m (a, ConcreteNames) -> s -> m ((a, ConcreteNames), s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateT ConcreteNames (StateT s m) a
-> ConcreteNames -> StateT s m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (StateT s m) a
m ConcreteNames
ns) s
s
((a, s), ConcreteNames) -> m ((a, s), ConcreteNames)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x,s
s'),ConcreteNames
ns')
data ModuleCheckMode
= ModuleScopeChecked
| ModuleTypeChecked
deriving (ModuleCheckMode -> ModuleCheckMode -> Bool
(ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> Eq ModuleCheckMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleCheckMode -> ModuleCheckMode -> Bool
== :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c/= :: ModuleCheckMode -> ModuleCheckMode -> Bool
/= :: ModuleCheckMode -> ModuleCheckMode -> Bool
Eq, Eq ModuleCheckMode
Eq ModuleCheckMode =>
(ModuleCheckMode -> ModuleCheckMode -> Ordering)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode)
-> (ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode)
-> Ord ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> Bool
ModuleCheckMode -> ModuleCheckMode -> Ordering
ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ModuleCheckMode -> ModuleCheckMode -> Ordering
compare :: ModuleCheckMode -> ModuleCheckMode -> Ordering
$c< :: ModuleCheckMode -> ModuleCheckMode -> Bool
< :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c<= :: ModuleCheckMode -> ModuleCheckMode -> Bool
<= :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c> :: ModuleCheckMode -> ModuleCheckMode -> Bool
> :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c>= :: ModuleCheckMode -> ModuleCheckMode -> Bool
>= :: ModuleCheckMode -> ModuleCheckMode -> Bool
$cmax :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
max :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
$cmin :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
min :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
Ord, ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> Bounded ModuleCheckMode
forall a. a -> a -> Bounded a
$cminBound :: ModuleCheckMode
minBound :: ModuleCheckMode
$cmaxBound :: ModuleCheckMode
maxBound :: ModuleCheckMode
Bounded, Int -> ModuleCheckMode
ModuleCheckMode -> Int
ModuleCheckMode -> [ModuleCheckMode]
ModuleCheckMode -> ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
(ModuleCheckMode -> ModuleCheckMode)
-> (ModuleCheckMode -> ModuleCheckMode)
-> (Int -> ModuleCheckMode)
-> (ModuleCheckMode -> Int)
-> (ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> Enum ModuleCheckMode
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ModuleCheckMode -> ModuleCheckMode
succ :: ModuleCheckMode -> ModuleCheckMode
$cpred :: ModuleCheckMode -> ModuleCheckMode
pred :: ModuleCheckMode -> ModuleCheckMode
$ctoEnum :: Int -> ModuleCheckMode
toEnum :: Int -> ModuleCheckMode
$cfromEnum :: ModuleCheckMode -> Int
fromEnum :: ModuleCheckMode -> Int
$cenumFrom :: ModuleCheckMode -> [ModuleCheckMode]
enumFrom :: ModuleCheckMode -> [ModuleCheckMode]
$cenumFromThen :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromThen :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
$cenumFromTo :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromTo :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
$cenumFromThenTo :: ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromThenTo :: ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
Enum, Int -> ModuleCheckMode -> ShowS
[ModuleCheckMode] -> ShowS
ModuleCheckMode -> String
(Int -> ModuleCheckMode -> ShowS)
-> (ModuleCheckMode -> String)
-> ([ModuleCheckMode] -> ShowS)
-> Show ModuleCheckMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModuleCheckMode -> ShowS
showsPrec :: Int -> ModuleCheckMode -> ShowS
$cshow :: ModuleCheckMode -> String
show :: ModuleCheckMode -> String
$cshowList :: [ModuleCheckMode] -> ShowS
showList :: [ModuleCheckMode] -> ShowS
Show, (forall x. ModuleCheckMode -> Rep ModuleCheckMode x)
-> (forall x. Rep ModuleCheckMode x -> ModuleCheckMode)
-> Generic ModuleCheckMode
forall x. Rep ModuleCheckMode x -> ModuleCheckMode
forall x. ModuleCheckMode -> Rep ModuleCheckMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModuleCheckMode -> Rep ModuleCheckMode x
from :: forall x. ModuleCheckMode -> Rep ModuleCheckMode x
$cto :: forall x. Rep ModuleCheckMode x -> ModuleCheckMode
to :: forall x. Rep ModuleCheckMode x -> ModuleCheckMode
Generic)
data ModuleInfo = ModuleInfo
{ ModuleInfo -> Interface
miInterface :: Interface
, ModuleInfo -> [TCWarning]
miWarnings :: [TCWarning]
, ModuleInfo -> Bool
miPrimitive :: Bool
, ModuleInfo -> ModuleCheckMode
miMode :: ModuleCheckMode
}
deriving (forall x. ModuleInfo -> Rep ModuleInfo x)
-> (forall x. Rep ModuleInfo x -> ModuleInfo) -> Generic ModuleInfo
forall x. Rep ModuleInfo x -> ModuleInfo
forall x. ModuleInfo -> Rep ModuleInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModuleInfo -> Rep ModuleInfo x
from :: forall x. ModuleInfo -> Rep ModuleInfo x
$cto :: forall x. Rep ModuleInfo x -> ModuleInfo
to :: forall x. Rep ModuleInfo x -> ModuleInfo
Generic
type VisitedModules = Map TopLevelModuleName ModuleInfo
type DecodedModules = Map TopLevelModuleName ModuleInfo
data ForeignCode = ForeignCode Range String
deriving (Int -> ForeignCode -> ShowS
[ForeignCode] -> ShowS
ForeignCode -> String
(Int -> ForeignCode -> ShowS)
-> (ForeignCode -> String)
-> ([ForeignCode] -> ShowS)
-> Show ForeignCode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForeignCode -> ShowS
showsPrec :: Int -> ForeignCode -> ShowS
$cshow :: ForeignCode -> String
show :: ForeignCode -> String
$cshowList :: [ForeignCode] -> ShowS
showList :: [ForeignCode] -> ShowS
Show, (forall x. ForeignCode -> Rep ForeignCode x)
-> (forall x. Rep ForeignCode x -> ForeignCode)
-> Generic ForeignCode
forall x. Rep ForeignCode x -> ForeignCode
forall x. ForeignCode -> Rep ForeignCode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ForeignCode -> Rep ForeignCode x
from :: forall x. ForeignCode -> Rep ForeignCode x
$cto :: forall x. Rep ForeignCode x -> ForeignCode
to :: forall x. Rep ForeignCode x -> ForeignCode
Generic)
newtype ForeignCodeStack = ForeignCodeStack
{ ForeignCodeStack -> [ForeignCode]
getForeignCodeStack :: [ForeignCode]
} deriving (Int -> ForeignCodeStack -> ShowS
[ForeignCodeStack] -> ShowS
ForeignCodeStack -> String
(Int -> ForeignCodeStack -> ShowS)
-> (ForeignCodeStack -> String)
-> ([ForeignCodeStack] -> ShowS)
-> Show ForeignCodeStack
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForeignCodeStack -> ShowS
showsPrec :: Int -> ForeignCodeStack -> ShowS
$cshow :: ForeignCodeStack -> String
show :: ForeignCodeStack -> String
$cshowList :: [ForeignCodeStack] -> ShowS
showList :: [ForeignCodeStack] -> ShowS
Show, (forall x. ForeignCodeStack -> Rep ForeignCodeStack x)
-> (forall x. Rep ForeignCodeStack x -> ForeignCodeStack)
-> Generic ForeignCodeStack
forall x. Rep ForeignCodeStack x -> ForeignCodeStack
forall x. ForeignCodeStack -> Rep ForeignCodeStack x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ForeignCodeStack -> Rep ForeignCodeStack x
from :: forall x. ForeignCodeStack -> Rep ForeignCodeStack x
$cto :: forall x. Rep ForeignCodeStack x -> ForeignCodeStack
to :: forall x. Rep ForeignCodeStack x -> ForeignCodeStack
Generic, ForeignCodeStack -> ()
(ForeignCodeStack -> ()) -> NFData ForeignCodeStack
forall a. (a -> ()) -> NFData a
$crnf :: ForeignCodeStack -> ()
rnf :: ForeignCodeStack -> ()
NFData)
data Interface = Interface
{ Interface -> Word64
iSourceHash :: !Hash
, Interface -> Text
iSource :: TL.Text
, Interface -> FileType
iFileType :: FileType
, Interface -> [(TopLevelModuleName, Word64)]
iImportedModules :: [(TopLevelModuleName, Hash)]
, Interface -> ModuleName
iModuleName :: ModuleName
, Interface -> TopLevelModuleName
iTopLevelModuleName :: TopLevelModuleName
, Interface -> Map ModuleName Scope
iScope :: Map ModuleName Scope
, Interface -> ScopeInfo
iInsideScope :: ScopeInfo
, Interface -> Signature
iSignature :: Signature
, Interface -> RemoteMetaStore
iMetaBindings :: RemoteMetaStore
, Interface -> DisplayForms
iDisplayForms :: DisplayForms
, Interface -> Map QName Text
iUserWarnings :: Map A.QName Text
, Interface -> Maybe Text
iImportWarning :: Maybe Text
, Interface -> BuiltinThings (PrimitiveId, QName)
iBuiltin :: BuiltinThings (PrimitiveId, QName)
, Interface -> Map String ForeignCodeStack
iForeignCode :: Map BackendName ForeignCodeStack
, Interface -> HighlightingInfo
iHighlighting :: HighlightingInfo
, Interface -> [OptionsPragma]
iDefaultPragmaOptions :: [OptionsPragma]
, Interface -> [OptionsPragma]
iFilePragmaOptions :: [OptionsPragma]
, Interface -> PragmaOptions
iOptionsUsed :: PragmaOptions
, Interface -> PatternSynDefns
iPatternSyns :: A.PatternSynDefns
, Interface -> [TCWarning]
iWarnings :: [TCWarning]
, Interface -> Set QName
iPartialDefs :: Set QName
, Interface -> Map OpaqueId OpaqueBlock
iOpaqueBlocks :: Map OpaqueId OpaqueBlock
, Interface -> Map QName OpaqueId
iOpaqueNames :: Map QName OpaqueId
}
deriving (Int -> Interface -> ShowS
[Interface] -> ShowS
Interface -> String
(Int -> Interface -> ShowS)
-> (Interface -> String)
-> ([Interface] -> ShowS)
-> Show Interface
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Interface -> ShowS
showsPrec :: Int -> Interface -> ShowS
$cshow :: Interface -> String
show :: Interface -> String
$cshowList :: [Interface] -> ShowS
showList :: [Interface] -> ShowS
Show, (forall x. Interface -> Rep Interface x)
-> (forall x. Rep Interface x -> Interface) -> Generic Interface
forall x. Rep Interface x -> Interface
forall x. Interface -> Rep Interface x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Interface -> Rep Interface x
from :: forall x. Interface -> Rep Interface x
$cto :: forall x. Rep Interface x -> Interface
to :: forall x. Rep Interface x -> Interface
Generic)
instance Pretty Interface where
pretty :: Interface -> Doc
pretty (Interface
Word64
sourceH Text
source FileType
fileT [(TopLevelModuleName, Word64)]
importedM ModuleName
moduleN TopLevelModuleName
topModN Map ModuleName Scope
scope ScopeInfo
insideS
Signature
signature RemoteMetaStore
metas DisplayForms
display Map QName Text
userwarn Maybe Text
importwarn BuiltinThings (PrimitiveId, QName)
builtin
Map String ForeignCodeStack
foreignCode HighlightingInfo
highlighting [OptionsPragma]
libPragmaO [OptionsPragma]
filePragmaO PragmaOptions
oUsed
PatternSynDefns
patternS [TCWarning]
warnings Set QName
partialdefs Map OpaqueId OpaqueBlock
oblocks Map QName OpaqueId
onames) =
Doc -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
hang Doc
"Interface" Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"source hash:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Word64 -> String) -> Word64 -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> String
forall a. Show a => a -> String
show) Word64
sourceH
, Doc
"source:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> String
TL.unpack Text
source)
, Doc
"file type:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (FileType -> String) -> FileType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FileType -> String
forall a. Show a => a -> String
show) FileType
fileT
, Doc
"imported modules:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([(TopLevelModuleName, Word64)] -> String)
-> [(TopLevelModuleName, Word64)]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TopLevelModuleName, Word64)] -> String
forall a. Show a => a -> String
show) [(TopLevelModuleName, Word64)]
importedM
, Doc
"module name:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty ModuleName
moduleN
, Doc
"top-level module name:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
topModN
, Doc
"scope:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map ModuleName Scope -> String) -> Map ModuleName Scope -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName Scope -> String
forall a. Show a => a -> String
show) Map ModuleName Scope
scope
, Doc
"inside scope:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (ScopeInfo -> String) -> ScopeInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> String
forall a. Show a => a -> String
show) ScopeInfo
insideS
, Doc
"signature:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Signature -> String) -> Signature -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> String
forall a. Show a => a -> String
show) Signature
signature
, Doc
"meta-variables:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (RemoteMetaStore -> String) -> RemoteMetaStore -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemoteMetaStore -> String
forall a. Show a => a -> String
show) RemoteMetaStore
metas
, Doc
"display:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (DisplayForms -> String) -> DisplayForms -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForms -> String
forall a. Show a => a -> String
show) DisplayForms
display
, Doc
"user warnings:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map QName Text -> String) -> Map QName Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map QName Text -> String
forall a. Show a => a -> String
show) Map QName Text
userwarn
, Doc
"import warning:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Maybe Text -> String) -> Maybe Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Text -> String
forall a. Show a => a -> String
show) Maybe Text
importwarn
, Doc
"builtin:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (BuiltinThings (PrimitiveId, QName) -> String)
-> BuiltinThings (PrimitiveId, QName)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinThings (PrimitiveId, QName) -> String
forall a. Show a => a -> String
show) BuiltinThings (PrimitiveId, QName)
builtin
, Doc
"Foreign code:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map String ForeignCodeStack -> String)
-> Map String ForeignCodeStack
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String ForeignCodeStack -> String
forall a. Show a => a -> String
show) Map String ForeignCodeStack
foreignCode
, Doc
"highlighting:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (HighlightingInfo -> String) -> HighlightingInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighlightingInfo -> String
forall a. Show a => a -> String
show) HighlightingInfo
highlighting
, Doc
"library pragma options:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([OptionsPragma] -> String) -> [OptionsPragma] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OptionsPragma] -> String
forall a. Show a => a -> String
show) [OptionsPragma]
libPragmaO
, Doc
"file pragma options:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([OptionsPragma] -> String) -> [OptionsPragma] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OptionsPragma] -> String
forall a. Show a => a -> String
show) [OptionsPragma]
filePragmaO
, Doc
"options used:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (PragmaOptions -> String) -> PragmaOptions -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> String
forall a. Show a => a -> String
show) PragmaOptions
oUsed
, Doc
"pattern syns:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (PatternSynDefns -> String) -> PatternSynDefns -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternSynDefns -> String
forall a. Show a => a -> String
show) PatternSynDefns
patternS
, Doc
"warnings:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> ([TCWarning] -> String) -> [TCWarning] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> String
forall a. Show a => a -> String
show) [TCWarning]
warnings
, Doc
"partial definitions:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Set QName -> String) -> Set QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set QName -> String
forall a. Show a => a -> String
show) Set QName
partialdefs
, Doc
"opaque blocks:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Map OpaqueId OpaqueBlock -> Doc
forall a. Pretty a => a -> Doc
pretty Map OpaqueId OpaqueBlock
oblocks
, Doc
"opaque names" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Map QName OpaqueId -> Doc
forall a. Pretty a => a -> Doc
pretty Map QName OpaqueId
onames
]
iFullHash :: Interface -> Hash
iFullHash :: Interface -> Word64
iFullHash Interface
i = [Word64] -> Word64
combineHashes ([Word64] -> Word64) -> [Word64] -> Word64
forall a b. (a -> b) -> a -> b
$ Interface -> Word64
iSourceHash Interface
i Word64 -> [Word64] -> [Word64]
forall a. a -> [a] -> [a]
: ((TopLevelModuleName, Word64) -> Word64)
-> [(TopLevelModuleName, Word64)] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
List.map (TopLevelModuleName, Word64) -> Word64
forall a b. (a, b) -> b
snd (Interface -> [(TopLevelModuleName, Word64)]
iImportedModules Interface
i)
intSignature :: Lens' Interface Signature
intSignature :: Lens' Interface Signature
intSignature Signature -> f Signature
f Interface
i = Signature -> f Signature
f (Interface -> Signature
iSignature Interface
i) f Signature -> (Signature -> Interface) -> f Interface
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Signature
s -> Interface
i { iSignature = s }
data Closure a = Closure
{ forall a. Closure a -> Signature
clSignature :: Signature
, forall a. Closure a -> TCEnv
clEnv :: TCEnv
, forall a. Closure a -> ScopeInfo
clScope :: ScopeInfo
, forall a. Closure a -> Map ModuleName CheckpointId
clModuleCheckpoints :: Map ModuleName CheckpointId
, forall a. Closure a -> a
clValue :: a
}
deriving ((forall a b. (a -> b) -> Closure a -> Closure b)
-> (forall a b. a -> Closure b -> Closure a) -> Functor Closure
forall a b. a -> Closure b -> Closure a
forall a b. (a -> b) -> Closure a -> Closure b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Closure a -> Closure b
fmap :: forall a b. (a -> b) -> Closure a -> Closure b
$c<$ :: forall a b. a -> Closure b -> Closure a
<$ :: forall a b. a -> Closure b -> Closure a
Functor, (forall m. Monoid m => Closure m -> m)
-> (forall m a. Monoid m => (a -> m) -> Closure a -> m)
-> (forall m a. Monoid m => (a -> m) -> Closure a -> m)
-> (forall a b. (a -> b -> b) -> b -> Closure a -> b)
-> (forall a b. (a -> b -> b) -> b -> Closure a -> b)
-> (forall b a. (b -> a -> b) -> b -> Closure a -> b)
-> (forall b a. (b -> a -> b) -> b -> Closure a -> b)
-> (forall a. (a -> a -> a) -> Closure a -> a)
-> (forall a. (a -> a -> a) -> Closure a -> a)
-> (forall a. Closure a -> [a])
-> (forall a. Closure a -> Bool)
-> (forall a. Closure a -> Int)
-> (forall a. Eq a => a -> Closure a -> Bool)
-> (forall a. Ord a => Closure a -> a)
-> (forall a. Ord a => Closure a -> a)
-> (forall a. Num a => Closure a -> a)
-> (forall a. Num a => Closure a -> a)
-> Foldable Closure
forall a. Eq a => a -> Closure a -> Bool
forall a. Num a => Closure a -> a
forall a. Ord a => Closure a -> a
forall m. Monoid m => Closure m -> m
forall a. Closure a -> Bool
forall a. Closure a -> Int
forall a. Closure a -> [a]
forall a. (a -> a -> a) -> Closure a -> a
forall m a. Monoid m => (a -> m) -> Closure a -> m
forall b a. (b -> a -> b) -> b -> Closure a -> b
forall a b. (a -> b -> b) -> b -> Closure a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Closure m -> m
fold :: forall m. Monoid m => Closure m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Closure a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Closure a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Closure a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Closure a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Closure a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Closure a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Closure a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Closure a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Closure a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Closure a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Closure a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Closure a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Closure a -> a
foldr1 :: forall a. (a -> a -> a) -> Closure a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Closure a -> a
foldl1 :: forall a. (a -> a -> a) -> Closure a -> a
$ctoList :: forall a. Closure a -> [a]
toList :: forall a. Closure a -> [a]
$cnull :: forall a. Closure a -> Bool
null :: forall a. Closure a -> Bool
$clength :: forall a. Closure a -> Int
length :: forall a. Closure a -> Int
$celem :: forall a. Eq a => a -> Closure a -> Bool
elem :: forall a. Eq a => a -> Closure a -> Bool
$cmaximum :: forall a. Ord a => Closure a -> a
maximum :: forall a. Ord a => Closure a -> a
$cminimum :: forall a. Ord a => Closure a -> a
minimum :: forall a. Ord a => Closure a -> a
$csum :: forall a. Num a => Closure a -> a
sum :: forall a. Num a => Closure a -> a
$cproduct :: forall a. Num a => Closure a -> a
product :: forall a. Num a => Closure a -> a
Foldable, (forall x. Closure a -> Rep (Closure a) x)
-> (forall x. Rep (Closure a) x -> Closure a)
-> Generic (Closure a)
forall x. Rep (Closure a) x -> Closure a
forall x. Closure a -> Rep (Closure a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Closure a) x -> Closure a
forall a x. Closure a -> Rep (Closure a) x
$cfrom :: forall a x. Closure a -> Rep (Closure a) x
from :: forall x. Closure a -> Rep (Closure a) x
$cto :: forall a x. Rep (Closure a) x -> Closure a
to :: forall x. Rep (Closure a) x -> Closure a
Generic)
instance Show a => Show (Closure a) where
show :: Closure a -> String
show Closure a
cl = String
"Closure { clValue = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Closure a -> a
forall a. Closure a -> a
clValue Closure a
cl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" }"
instance HasRange a => HasRange (Closure a) where
getRange :: Closure a -> Range
getRange = a -> Range
forall a. HasRange a => a -> Range
getRange (a -> Range) -> (Closure a -> a) -> Closure a -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure a -> a
forall a. Closure a -> a
clValue
class LensClosure b a | b -> a where
lensClosure :: Lens' b (Closure a)
instance LensClosure (Closure a) a where
lensClosure :: Lens' (Closure a) (Closure a)
lensClosure = (Closure a -> f (Closure a)) -> Closure a -> f (Closure a)
forall a. a -> a
id
instance LensTCEnv (Closure a) where
lensTCEnv :: Lens' (Closure a) TCEnv
lensTCEnv TCEnv -> f TCEnv
f Closure a
cl = (TCEnv -> f TCEnv
f (TCEnv -> f TCEnv) -> TCEnv -> f TCEnv
forall a b. (a -> b) -> a -> b
$! Closure a -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure a
cl) f TCEnv -> (TCEnv -> Closure a) -> f (Closure a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ TCEnv
env -> Closure a
cl { clEnv = env }
{-# SPECIALIZE buildClosure :: a -> TCM (Closure a) #-}
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
buildClosure :: forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure a
x = do
TCEnv
env <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
Signature
sig <- Lens' TCState Signature -> m Signature
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature
ScopeInfo
scope <- Lens' TCState ScopeInfo -> m ScopeInfo
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope
Map ModuleName CheckpointId
cps <- Lens' TCState (Map ModuleName CheckpointId)
-> m (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints
Closure a -> m (Closure a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure a -> m (Closure a)) -> Closure a -> m (Closure a)
forall a b. (a -> b) -> a -> b
$ Signature
-> TCEnv
-> ScopeInfo
-> Map ModuleName CheckpointId
-> a
-> Closure a
forall a.
Signature
-> TCEnv
-> ScopeInfo
-> Map ModuleName CheckpointId
-> a
-> Closure a
Closure Signature
sig TCEnv
env ScopeInfo
scope Map ModuleName CheckpointId
cps a
x
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
{ ProblemConstraint -> Set ProblemId
constraintProblems :: Set ProblemId
, ProblemConstraint -> Blocker
constraintUnblocker :: Blocker
, ProblemConstraint -> Closure Constraint
theConstraint :: Closure Constraint
}
deriving (Int -> ProblemConstraint -> ShowS
Constraints -> ShowS
ProblemConstraint -> String
(Int -> ProblemConstraint -> ShowS)
-> (ProblemConstraint -> String)
-> (Constraints -> ShowS)
-> Show ProblemConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProblemConstraint -> ShowS
showsPrec :: Int -> ProblemConstraint -> ShowS
$cshow :: ProblemConstraint -> String
show :: ProblemConstraint -> String
$cshowList :: Constraints -> ShowS
showList :: Constraints -> ShowS
Show, (forall x. ProblemConstraint -> Rep ProblemConstraint x)
-> (forall x. Rep ProblemConstraint x -> ProblemConstraint)
-> Generic ProblemConstraint
forall x. Rep ProblemConstraint x -> ProblemConstraint
forall x. ProblemConstraint -> Rep ProblemConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProblemConstraint -> Rep ProblemConstraint x
from :: forall x. ProblemConstraint -> Rep ProblemConstraint x
$cto :: forall x. Rep ProblemConstraint x -> ProblemConstraint
to :: forall x. Rep ProblemConstraint x -> ProblemConstraint
Generic)
instance HasRange ProblemConstraint where
getRange :: ProblemConstraint -> Range
getRange = Closure Constraint -> Range
forall a. HasRange a => a -> Range
getRange (Closure Constraint -> Range)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint
data WhyCheckModality
= ConstructorType
| IndexedClause
| IndexedClauseArg Name Name
| GeneratedClause
deriving (Int -> WhyCheckModality -> ShowS
[WhyCheckModality] -> ShowS
WhyCheckModality -> String
(Int -> WhyCheckModality -> ShowS)
-> (WhyCheckModality -> String)
-> ([WhyCheckModality] -> ShowS)
-> Show WhyCheckModality
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhyCheckModality -> ShowS
showsPrec :: Int -> WhyCheckModality -> ShowS
$cshow :: WhyCheckModality -> String
show :: WhyCheckModality -> String
$cshowList :: [WhyCheckModality] -> ShowS
showList :: [WhyCheckModality] -> ShowS
Show, (forall x. WhyCheckModality -> Rep WhyCheckModality x)
-> (forall x. Rep WhyCheckModality x -> WhyCheckModality)
-> Generic WhyCheckModality
forall x. Rep WhyCheckModality x -> WhyCheckModality
forall x. WhyCheckModality -> Rep WhyCheckModality x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhyCheckModality -> Rep WhyCheckModality x
from :: forall x. WhyCheckModality -> Rep WhyCheckModality x
$cto :: forall x. Rep WhyCheckModality x -> WhyCheckModality
to :: forall x. Rep WhyCheckModality x -> WhyCheckModality
Generic)
data Constraint
= ValueCmp Comparison CompareAs Term Term
| ValueCmpOnFace Comparison Term Type Term Term
| ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Level Level
| HasBiggerSort Sort
| HasPTSRule (Dom Type) (Abs Sort)
| CheckDataSort QName Sort
| CheckMetaInst MetaId
| CheckType Type
| UnBlock MetaId
| IsEmpty Range Type
| CheckSizeLtSat Term
| FindInstance MetaId (Maybe [Candidate])
| ResolveInstanceHead QName
| CheckFunDef A.DefInfo QName [A.Clause] TCErr
| UnquoteTactic Term Term Type
| CheckLockedVars Term Type (Arg Term) Type
| UsableAtModality WhyCheckModality (Maybe Sort) Modality Term
deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show, (forall x. Constraint -> Rep Constraint x)
-> (forall x. Rep Constraint x -> Constraint) -> Generic Constraint
forall x. Rep Constraint x -> Constraint
forall x. Constraint -> Rep Constraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Constraint -> Rep Constraint x
from :: forall x. Constraint -> Rep Constraint x
$cto :: forall x. Rep Constraint x -> Constraint
to :: forall x. Rep Constraint x -> Constraint
Generic)
instance HasRange Constraint where
getRange :: Constraint -> Range
getRange (IsEmpty Range
r Type
t) = Range
r
getRange Constraint
_ = Range
forall a. Range' a
noRange
instance Free Constraint where
freeVars' :: forall a c. IsVarSet a c => Constraint -> FreeM a c
freeVars' Constraint
c =
case Constraint
c of
ValueCmp Comparison
_ CompareAs
t Term
u Term
v -> (CompareAs, (Term, Term)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (CompareAs, (Term, Term)) -> FreeM a c
freeVars' (CompareAs
t, (Term
u, Term
v))
ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v -> (Term, (Type, (Term, Term))) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
(Term, (Type, (Term, Term))) -> FreeM a c
freeVars' (Term
p, (Type
t, (Term
u, Term
v)))
ElimCmp [Polarity]
_ [IsForced]
_ Type
t Term
u [Elim]
es [Elim]
es' -> ((Type, Term), ([Elim], [Elim])) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
((Type, Term), ([Elim], [Elim])) -> FreeM a c
freeVars' ((Type
t, Term
u), ([Elim]
es, [Elim]
es'))
SortCmp Comparison
_ Sort
s Sort
s' -> (Sort, Sort) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, Sort) -> FreeM a c
freeVars' (Sort
s, Sort
s')
LevelCmp Comparison
_ Level
l Level
l' -> (Level, Level) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Level, Level) -> FreeM a c
freeVars' (Level
l, Level
l')
UnBlock MetaId
_ -> FreeM a c
forall a. Monoid a => a
mempty
IsEmpty Range
_ Type
t -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
CheckSizeLtSat Term
u -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
u
FindInstance MetaId
_ Maybe [Candidate]
cs -> Maybe [Candidate] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Maybe [Candidate] -> FreeM a c
freeVars' Maybe [Candidate]
cs
ResolveInstanceHead QName
q -> FreeM a c
forall a. Monoid a => a
mempty
CheckFunDef{} -> FreeM a c
forall a. Monoid a => a
mempty
HasBiggerSort Sort
s -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
HasPTSRule Dom Type
a Abs Sort
s -> (Dom Type, Abs Sort) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Dom Type, Abs Sort) -> FreeM a c
freeVars' (Dom Type
a , Abs Sort
s)
CheckLockedVars Term
a Type
b Arg Term
c Type
d -> ((Term, Type), (Arg Term, Type)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
((Term, Type), (Arg Term, Type)) -> FreeM a c
freeVars' ((Term
a,Type
b),(Arg Term
c,Type
d))
UnquoteTactic Term
t Term
h Type
g -> (Term, (Term, Type)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Term, (Term, Type)) -> FreeM a c
freeVars' (Term
t, (Term
h, Type
g))
CheckDataSort QName
_ Sort
s -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
CheckMetaInst MetaId
m -> FreeM a c
forall a. Monoid a => a
mempty
CheckType Type
t -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
mod Term
t -> (Maybe Sort, Term) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Maybe Sort, Term) -> FreeM a c
freeVars' (Maybe Sort
ms, Term
t)
instance TermLike Constraint where
foldTerm :: forall m. Monoid m => (Term -> m) -> Constraint -> m
foldTerm Term -> m
f = \case
ValueCmp Comparison
_ CompareAs
t Term
u Term
v -> (Term -> m) -> (CompareAs, Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (CompareAs, Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (CompareAs
t, Term
u, Term
v)
ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v -> (Term -> m) -> (Term, Type, Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Type, Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
p, Type
t, Term
u, Term
v)
ElimCmp [Polarity]
_ [IsForced]
_ Type
t Term
u [Elim]
es [Elim]
es' -> (Term -> m) -> (Type, Term, [Elim], [Elim]) -> m
forall m.
Monoid m =>
(Term -> m) -> (Type, Term, [Elim], [Elim]) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Type
t, Term
u, [Elim]
es, [Elim]
es')
LevelCmp Comparison
_ Level
l Level
l' -> (Term -> m) -> (Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
IsEmpty Range
_ Type
t -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
CheckSizeLtSat Term
u -> (Term -> m) -> Term -> m
forall m. Monoid m => (Term -> m) -> Term -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
u
UnquoteTactic Term
t Term
h Type
g -> (Term -> m) -> (Term, Term, Type) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term, Type) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
t, Term
h, Type
g)
SortCmp Comparison
_ Sort
s1 Sort
s2 -> (Term -> m) -> (Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
UnBlock MetaId
_ -> m
forall a. Monoid a => a
mempty
CheckLockedVars Term
a Type
b Arg Term
c Type
d -> (Term -> m) -> (Term, Type, Arg Term, Type) -> m
forall m.
Monoid m =>
(Term -> m) -> (Term, Type, Arg Term, Type) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
a, Type
b, Arg Term
c, Type
d)
FindInstance MetaId
_ Maybe [Candidate]
_ -> m
forall a. Monoid a => a
mempty
ResolveInstanceHead QName
q -> m
forall a. Monoid a => a
mempty
CheckFunDef{} -> m
forall a. Monoid a => a
mempty
HasBiggerSort Sort
s -> (Term -> m) -> Sort -> m
forall m. Monoid m => (Term -> m) -> Sort -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
s
HasPTSRule Dom Type
a Abs Sort
s -> (Term -> m) -> (Dom Type, Abs Term) -> m
forall m. Monoid m => (Term -> m) -> (Dom Type, Abs Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Dom Type
a, Sort -> Term
Sort (Sort -> Term) -> Abs Sort -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Sort
s)
CheckDataSort QName
_ Sort
s -> (Term -> m) -> Sort -> m
forall m. Monoid m => (Term -> m) -> Sort -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
s
CheckMetaInst MetaId
m -> m
forall a. Monoid a => a
mempty
CheckType Type
t -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
m Term
t -> (Term -> m) -> (Maybe Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Maybe Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Sort -> Term
Sort (Sort -> Term) -> Maybe Sort -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Sort
ms, Term
t)
traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Constraint -> m Constraint
traverseTermM Term -> m Term
f Constraint
c = m Constraint
forall a. HasCallStack => a
__IMPOSSIBLE__
instance AllMetas Constraint
data Comparison = CmpEq | CmpLeq
deriving (Comparison -> Comparison -> Bool
(Comparison -> Comparison -> Bool)
-> (Comparison -> Comparison -> Bool) -> Eq Comparison
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Comparison -> Comparison -> Bool
== :: Comparison -> Comparison -> Bool
$c/= :: Comparison -> Comparison -> Bool
/= :: Comparison -> Comparison -> Bool
Eq, Int -> Comparison -> ShowS
[Comparison] -> ShowS
Comparison -> String
(Int -> Comparison -> ShowS)
-> (Comparison -> String)
-> ([Comparison] -> ShowS)
-> Show Comparison
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Comparison -> ShowS
showsPrec :: Int -> Comparison -> ShowS
$cshow :: Comparison -> String
show :: Comparison -> String
$cshowList :: [Comparison] -> ShowS
showList :: [Comparison] -> ShowS
Show, (forall x. Comparison -> Rep Comparison x)
-> (forall x. Rep Comparison x -> Comparison) -> Generic Comparison
forall x. Rep Comparison x -> Comparison
forall x. Comparison -> Rep Comparison x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Comparison -> Rep Comparison x
from :: forall x. Comparison -> Rep Comparison x
$cto :: forall x. Rep Comparison x -> Comparison
to :: forall x. Rep Comparison x -> Comparison
Generic)
instance Pretty Comparison where
pretty :: Comparison -> Doc
pretty Comparison
CmpEq = Doc
"="
pretty Comparison
CmpLeq = Doc
"=<"
data CompareDirection = DirEq | DirLeq | DirGeq
deriving (CompareDirection -> CompareDirection -> Bool
(CompareDirection -> CompareDirection -> Bool)
-> (CompareDirection -> CompareDirection -> Bool)
-> Eq CompareDirection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompareDirection -> CompareDirection -> Bool
== :: CompareDirection -> CompareDirection -> Bool
$c/= :: CompareDirection -> CompareDirection -> Bool
/= :: CompareDirection -> CompareDirection -> Bool
Eq, Int -> CompareDirection -> ShowS
[CompareDirection] -> ShowS
CompareDirection -> String
(Int -> CompareDirection -> ShowS)
-> (CompareDirection -> String)
-> ([CompareDirection] -> ShowS)
-> Show CompareDirection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompareDirection -> ShowS
showsPrec :: Int -> CompareDirection -> ShowS
$cshow :: CompareDirection -> String
show :: CompareDirection -> String
$cshowList :: [CompareDirection] -> ShowS
showList :: [CompareDirection] -> ShowS
Show)
instance Pretty CompareDirection where
pretty :: CompareDirection -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc)
-> (CompareDirection -> String) -> CompareDirection -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
CompareDirection
DirEq -> String
"="
CompareDirection
DirLeq -> String
"=<"
CompareDirection
DirGeq -> String
">="
fromCmp :: Comparison -> CompareDirection
fromCmp :: Comparison -> CompareDirection
fromCmp Comparison
CmpEq = CompareDirection
DirEq
fromCmp Comparison
CmpLeq = CompareDirection
DirLeq
flipCmp :: CompareDirection -> CompareDirection
flipCmp :: CompareDirection -> CompareDirection
flipCmp CompareDirection
DirEq = CompareDirection
DirEq
flipCmp CompareDirection
DirLeq = CompareDirection
DirGeq
flipCmp CompareDirection
DirGeq = CompareDirection
DirLeq
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp :: forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirEq = Comparison -> a -> a -> c
cont Comparison
CmpEq
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirLeq = Comparison -> a -> a -> c
cont Comparison
CmpLeq
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirGeq = (a -> a -> c) -> a -> a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> a -> c) -> a -> a -> c) -> (a -> a -> c) -> a -> a -> c
forall a b. (a -> b) -> a -> b
$ Comparison -> a -> a -> c
cont Comparison
CmpLeq
data CompareAs
= AsTermsOf Type
| AsSizes
| AsTypes
deriving (Int -> CompareAs -> ShowS
[CompareAs] -> ShowS
CompareAs -> String
(Int -> CompareAs -> ShowS)
-> (CompareAs -> String)
-> ([CompareAs] -> ShowS)
-> Show CompareAs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompareAs -> ShowS
showsPrec :: Int -> CompareAs -> ShowS
$cshow :: CompareAs -> String
show :: CompareAs -> String
$cshowList :: [CompareAs] -> ShowS
showList :: [CompareAs] -> ShowS
Show, (forall x. CompareAs -> Rep CompareAs x)
-> (forall x. Rep CompareAs x -> CompareAs) -> Generic CompareAs
forall x. Rep CompareAs x -> CompareAs
forall x. CompareAs -> Rep CompareAs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CompareAs -> Rep CompareAs x
from :: forall x. CompareAs -> Rep CompareAs x
$cto :: forall x. Rep CompareAs x -> CompareAs
to :: forall x. Rep CompareAs x -> CompareAs
Generic)
instance Free CompareAs where
freeVars' :: forall a c. IsVarSet a c => CompareAs -> FreeM a c
freeVars' (AsTermsOf Type
a) = Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
a
freeVars' CompareAs
AsSizes = FreeM a c
forall a. Monoid a => a
mempty
freeVars' CompareAs
AsTypes = FreeM a c
forall a. Monoid a => a
mempty
instance TermLike CompareAs where
foldTerm :: forall m. Monoid m => (Term -> m) -> CompareAs -> m
foldTerm Term -> m
f (AsTermsOf Type
a) = (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
a
foldTerm Term -> m
f CompareAs
AsSizes = m
forall a. Monoid a => a
mempty
foldTerm Term -> m
f CompareAs
AsTypes = m
forall a. Monoid a => a
mempty
traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> CompareAs -> m CompareAs
traverseTermM Term -> m Term
f = \case
AsTermsOf Type
a -> Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> m Type -> m CompareAs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Term) -> Type -> m Type
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
traverseTermM Term -> m Term
f Type
a
CompareAs
AsSizes -> CompareAs -> m CompareAs
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
CompareAs
AsTypes -> CompareAs -> m CompareAs
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsTypes
instance AllMetas CompareAs
instance Pretty CompareAs where
pretty :: CompareAs -> Doc
pretty (AsTermsOf Type
a) = Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
a
pretty CompareAs
AsSizes = Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text String
"Size"
pretty CompareAs
AsTypes = Doc
forall a. Null a => a
empty
data Open a = OpenThing { forall a. Open a -> CheckpointId
openThingCheckpoint :: CheckpointId
, forall a. Open a -> Map CheckpointId Substitution
openThingCheckpointMap :: Map CheckpointId Substitution
, forall a. Open a -> ModuleNameHash
openThingModule :: ModuleNameHash
, forall a. Open a -> a
openThing :: a }
deriving (Int -> Open a -> ShowS
[Open a] -> ShowS
Open a -> String
(Int -> Open a -> ShowS)
-> (Open a -> String) -> ([Open a] -> ShowS) -> Show (Open a)
forall a. Show a => Int -> Open a -> ShowS
forall a. Show a => [Open a] -> ShowS
forall a. Show a => Open a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Open a -> ShowS
showsPrec :: Int -> Open a -> ShowS
$cshow :: forall a. Show a => Open a -> String
show :: Open a -> String
$cshowList :: forall a. Show a => [Open a] -> ShowS
showList :: [Open a] -> ShowS
Show, (forall a b. (a -> b) -> Open a -> Open b)
-> (forall a b. a -> Open b -> Open a) -> Functor Open
forall a b. a -> Open b -> Open a
forall a b. (a -> b) -> Open a -> Open b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Open a -> Open b
fmap :: forall a b. (a -> b) -> Open a -> Open b
$c<$ :: forall a b. a -> Open b -> Open a
<$ :: forall a b. a -> Open b -> Open a
Functor, (forall m. Monoid m => Open m -> m)
-> (forall m a. Monoid m => (a -> m) -> Open a -> m)
-> (forall m a. Monoid m => (a -> m) -> Open a -> m)
-> (forall a b. (a -> b -> b) -> b -> Open a -> b)
-> (forall a b. (a -> b -> b) -> b -> Open a -> b)
-> (forall b a. (b -> a -> b) -> b -> Open a -> b)
-> (forall b a. (b -> a -> b) -> b -> Open a -> b)
-> (forall a. (a -> a -> a) -> Open a -> a)
-> (forall a. (a -> a -> a) -> Open a -> a)
-> (forall a. Open a -> [a])
-> (forall a. Open a -> Bool)
-> (forall a. Open a -> Int)
-> (forall a. Eq a => a -> Open a -> Bool)
-> (forall a. Ord a => Open a -> a)
-> (forall a. Ord a => Open a -> a)
-> (forall a. Num a => Open a -> a)
-> (forall a. Num a => Open a -> a)
-> Foldable Open
forall a. Eq a => a -> Open a -> Bool
forall a. Num a => Open a -> a
forall a. Ord a => Open a -> a
forall m. Monoid m => Open m -> m
forall a. Open a -> Bool
forall a. Open a -> Int
forall a. Open a -> [a]
forall a. (a -> a -> a) -> Open a -> a
forall m a. Monoid m => (a -> m) -> Open a -> m
forall b a. (b -> a -> b) -> b -> Open a -> b
forall a b. (a -> b -> b) -> b -> Open a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Open m -> m
fold :: forall m. Monoid m => Open m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Open a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Open a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Open a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Open a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Open a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Open a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Open a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Open a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Open a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Open a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Open a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Open a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Open a -> a
foldr1 :: forall a. (a -> a -> a) -> Open a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Open a -> a
foldl1 :: forall a. (a -> a -> a) -> Open a -> a
$ctoList :: forall a. Open a -> [a]
toList :: forall a. Open a -> [a]
$cnull :: forall a. Open a -> Bool
null :: forall a. Open a -> Bool
$clength :: forall a. Open a -> Int
length :: forall a. Open a -> Int
$celem :: forall a. Eq a => a -> Open a -> Bool
elem :: forall a. Eq a => a -> Open a -> Bool
$cmaximum :: forall a. Ord a => Open a -> a
maximum :: forall a. Ord a => Open a -> a
$cminimum :: forall a. Ord a => Open a -> a
minimum :: forall a. Ord a => Open a -> a
$csum :: forall a. Num a => Open a -> a
sum :: forall a. Num a => Open a -> a
$cproduct :: forall a. Num a => Open a -> a
product :: forall a. Num a => Open a -> a
Foldable, Functor Open
Foldable Open
(Functor Open, Foldable Open) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b))
-> (forall (f :: * -> *) a.
Applicative f =>
Open (f a) -> f (Open a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b))
-> (forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a))
-> Traversable Open
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
$csequence :: forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
sequence :: forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
Traversable, (forall x. Open a -> Rep (Open a) x)
-> (forall x. Rep (Open a) x -> Open a) -> Generic (Open a)
forall x. Rep (Open a) x -> Open a
forall x. Open a -> Rep (Open a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Open a) x -> Open a
forall a x. Open a -> Rep (Open a) x
$cfrom :: forall a x. Open a -> Rep (Open a) x
from :: forall x. Open a -> Rep (Open a) x
$cto :: forall a x. Rep (Open a) x -> Open a
to :: forall x. Rep (Open a) x -> Open a
Generic)
instance Decoration Open where
traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Open a -> m (Open b)
traverseF a -> m b
f (OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
m a
x) = CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> b -> Open b
forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
m (b -> Open b) -> m b -> m (Open b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
x
instance Pretty a => Pretty (Open a) where
prettyPrec :: Int -> Open a -> Doc
prettyPrec Int
p (OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
_ a
x) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc
"OpenThing" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc
forall a. Pretty a => a -> Doc
pretty CheckpointId
cp Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [(CheckpointId, Substitution)] -> Doc
forall a. Pretty a => a -> Doc
pretty (Map CheckpointId Substitution -> [(CheckpointId, Substitution)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
env) Doc -> Doc -> Doc
<?> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 a
x
data Judgement a
= HasType
{ forall a. Judgement a -> a
jMetaId :: a
, forall a. Judgement a -> Comparison
jComparison :: Comparison
, forall a. Judgement a -> Type
jMetaType :: Type
}
| IsSort
{ jMetaId :: a
, jMetaType :: Type
}
deriving (Int -> Judgement a -> ShowS
[Judgement a] -> ShowS
Judgement a -> String
(Int -> Judgement a -> ShowS)
-> (Judgement a -> String)
-> ([Judgement a] -> ShowS)
-> Show (Judgement a)
forall a. Show a => Int -> Judgement a -> ShowS
forall a. Show a => [Judgement a] -> ShowS
forall a. Show a => Judgement a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Judgement a -> ShowS
showsPrec :: Int -> Judgement a -> ShowS
$cshow :: forall a. Show a => Judgement a -> String
show :: Judgement a -> String
$cshowList :: forall a. Show a => [Judgement a] -> ShowS
showList :: [Judgement a] -> ShowS
Show, (forall x. Judgement a -> Rep (Judgement a) x)
-> (forall x. Rep (Judgement a) x -> Judgement a)
-> Generic (Judgement a)
forall x. Rep (Judgement a) x -> Judgement a
forall x. Judgement a -> Rep (Judgement a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Judgement a) x -> Judgement a
forall a x. Judgement a -> Rep (Judgement a) x
$cfrom :: forall a x. Judgement a -> Rep (Judgement a) x
from :: forall x. Judgement a -> Rep (Judgement a) x
$cto :: forall a x. Rep (Judgement a) x -> Judgement a
to :: forall x. Rep (Judgement a) x -> Judgement a
Generic)
instance Pretty a => Pretty (Judgement a) where
pretty :: Judgement a -> Doc
pretty (HasType a
a Comparison
cmp Type
t) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a, Doc
":" , Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t ]
pretty (IsSort a
a Type
t) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a, Doc
":sort", Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t ]
data DoGeneralize
= YesGeneralizeVar
| YesGeneralizeMeta
| NoGeneralize
deriving (DoGeneralize -> DoGeneralize -> Bool
(DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool) -> Eq DoGeneralize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DoGeneralize -> DoGeneralize -> Bool
== :: DoGeneralize -> DoGeneralize -> Bool
$c/= :: DoGeneralize -> DoGeneralize -> Bool
/= :: DoGeneralize -> DoGeneralize -> Bool
Eq, Eq DoGeneralize
Eq DoGeneralize =>
(DoGeneralize -> DoGeneralize -> Ordering)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> DoGeneralize)
-> (DoGeneralize -> DoGeneralize -> DoGeneralize)
-> Ord DoGeneralize
DoGeneralize -> DoGeneralize -> Bool
DoGeneralize -> DoGeneralize -> Ordering
DoGeneralize -> DoGeneralize -> DoGeneralize
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DoGeneralize -> DoGeneralize -> Ordering
compare :: DoGeneralize -> DoGeneralize -> Ordering
$c< :: DoGeneralize -> DoGeneralize -> Bool
< :: DoGeneralize -> DoGeneralize -> Bool
$c<= :: DoGeneralize -> DoGeneralize -> Bool
<= :: DoGeneralize -> DoGeneralize -> Bool
$c> :: DoGeneralize -> DoGeneralize -> Bool
> :: DoGeneralize -> DoGeneralize -> Bool
$c>= :: DoGeneralize -> DoGeneralize -> Bool
>= :: DoGeneralize -> DoGeneralize -> Bool
$cmax :: DoGeneralize -> DoGeneralize -> DoGeneralize
max :: DoGeneralize -> DoGeneralize -> DoGeneralize
$cmin :: DoGeneralize -> DoGeneralize -> DoGeneralize
min :: DoGeneralize -> DoGeneralize -> DoGeneralize
Ord, Int -> DoGeneralize -> ShowS
[DoGeneralize] -> ShowS
DoGeneralize -> String
(Int -> DoGeneralize -> ShowS)
-> (DoGeneralize -> String)
-> ([DoGeneralize] -> ShowS)
-> Show DoGeneralize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DoGeneralize -> ShowS
showsPrec :: Int -> DoGeneralize -> ShowS
$cshow :: DoGeneralize -> String
show :: DoGeneralize -> String
$cshowList :: [DoGeneralize] -> ShowS
showList :: [DoGeneralize] -> ShowS
Show, (forall x. DoGeneralize -> Rep DoGeneralize x)
-> (forall x. Rep DoGeneralize x -> DoGeneralize)
-> Generic DoGeneralize
forall x. Rep DoGeneralize x -> DoGeneralize
forall x. DoGeneralize -> Rep DoGeneralize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DoGeneralize -> Rep DoGeneralize x
from :: forall x. DoGeneralize -> Rep DoGeneralize x
$cto :: forall x. Rep DoGeneralize x -> DoGeneralize
to :: forall x. Rep DoGeneralize x -> DoGeneralize
Generic)
data GeneralizedValue = GeneralizedValue
{ GeneralizedValue -> CheckpointId
genvalCheckpoint :: CheckpointId
, GeneralizedValue -> Term
genvalTerm :: Term
, GeneralizedValue -> Type
genvalType :: Type
} deriving (Int -> GeneralizedValue -> ShowS
[GeneralizedValue] -> ShowS
GeneralizedValue -> String
(Int -> GeneralizedValue -> ShowS)
-> (GeneralizedValue -> String)
-> ([GeneralizedValue] -> ShowS)
-> Show GeneralizedValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GeneralizedValue -> ShowS
showsPrec :: Int -> GeneralizedValue -> ShowS
$cshow :: GeneralizedValue -> String
show :: GeneralizedValue -> String
$cshowList :: [GeneralizedValue] -> ShowS
showList :: [GeneralizedValue] -> ShowS
Show, (forall x. GeneralizedValue -> Rep GeneralizedValue x)
-> (forall x. Rep GeneralizedValue x -> GeneralizedValue)
-> Generic GeneralizedValue
forall x. Rep GeneralizedValue x -> GeneralizedValue
forall x. GeneralizedValue -> Rep GeneralizedValue x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GeneralizedValue -> Rep GeneralizedValue x
from :: forall x. GeneralizedValue -> Rep GeneralizedValue x
$cto :: forall x. Rep GeneralizedValue x -> GeneralizedValue
to :: forall x. Rep GeneralizedValue x -> GeneralizedValue
Generic)
data MetaVariable =
MetaVar { MetaVariable -> MetaInfo
mvInfo :: MetaInfo
, MetaVariable -> MetaPriority
mvPriority :: MetaPriority
, MetaVariable -> Permutation
mvPermutation :: Permutation
, MetaVariable -> Judgement MetaId
mvJudgement :: Judgement MetaId
, MetaVariable -> MetaInstantiation
mvInstantiation :: MetaInstantiation
, MetaVariable -> Set Listener
mvListeners :: Set Listener
, MetaVariable -> Frozen
mvFrozen :: Frozen
, MetaVariable -> Maybe MetaId
mvTwin :: Maybe MetaId
}
deriving (forall x. MetaVariable -> Rep MetaVariable x)
-> (forall x. Rep MetaVariable x -> MetaVariable)
-> Generic MetaVariable
forall x. Rep MetaVariable x -> MetaVariable
forall x. MetaVariable -> Rep MetaVariable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaVariable -> Rep MetaVariable x
from :: forall x. MetaVariable -> Rep MetaVariable x
$cto :: forall x. Rep MetaVariable x -> MetaVariable
to :: forall x. Rep MetaVariable x -> MetaVariable
Generic
data Listener = EtaExpand MetaId
| CheckConstraint Nat ProblemConstraint
deriving (forall x. Listener -> Rep Listener x)
-> (forall x. Rep Listener x -> Listener) -> Generic Listener
forall x. Rep Listener x -> Listener
forall x. Listener -> Rep Listener x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Listener -> Rep Listener x
from :: forall x. Listener -> Rep Listener x
$cto :: forall x. Rep Listener x -> Listener
to :: forall x. Rep Listener x -> Listener
Generic
instance Eq Listener where
EtaExpand MetaId
x == :: Listener -> Listener -> Bool
== EtaExpand MetaId
y = MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y
CheckConstraint Int
x ProblemConstraint
_ == CheckConstraint Int
y ProblemConstraint
_ = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y
Listener
_ == Listener
_ = Bool
False
instance Ord Listener where
EtaExpand MetaId
x compare :: Listener -> Listener -> Ordering
`compare` EtaExpand MetaId
y = MetaId
x MetaId -> MetaId -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` MetaId
y
CheckConstraint Int
x ProblemConstraint
_ `compare` CheckConstraint Int
y ProblemConstraint
_ = Int
x Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
y
EtaExpand{} `compare` CheckConstraint{} = Ordering
LT
CheckConstraint{} `compare` EtaExpand{} = Ordering
GT
data Frozen
= Frozen
| Instantiable
deriving (Frozen -> Frozen -> Bool
(Frozen -> Frozen -> Bool)
-> (Frozen -> Frozen -> Bool) -> Eq Frozen
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Frozen -> Frozen -> Bool
== :: Frozen -> Frozen -> Bool
$c/= :: Frozen -> Frozen -> Bool
/= :: Frozen -> Frozen -> Bool
Eq, Int -> Frozen -> ShowS
[Frozen] -> ShowS
Frozen -> String
(Int -> Frozen -> ShowS)
-> (Frozen -> String) -> ([Frozen] -> ShowS) -> Show Frozen
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Frozen -> ShowS
showsPrec :: Int -> Frozen -> ShowS
$cshow :: Frozen -> String
show :: Frozen -> String
$cshowList :: [Frozen] -> ShowS
showList :: [Frozen] -> ShowS
Show, (forall x. Frozen -> Rep Frozen x)
-> (forall x. Rep Frozen x -> Frozen) -> Generic Frozen
forall x. Rep Frozen x -> Frozen
forall x. Frozen -> Rep Frozen x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Frozen -> Rep Frozen x
from :: forall x. Frozen -> Rep Frozen x
$cto :: forall x. Rep Frozen x -> Frozen
to :: forall x. Rep Frozen x -> Frozen
Generic)
data MetaInstantiation
= InstV Instantiation
| OpenMeta MetaKind
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure TypeCheckingProblem)
deriving (forall x. MetaInstantiation -> Rep MetaInstantiation x)
-> (forall x. Rep MetaInstantiation x -> MetaInstantiation)
-> Generic MetaInstantiation
forall x. Rep MetaInstantiation x -> MetaInstantiation
forall x. MetaInstantiation -> Rep MetaInstantiation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInstantiation -> Rep MetaInstantiation x
from :: forall x. MetaInstantiation -> Rep MetaInstantiation x
$cto :: forall x. Rep MetaInstantiation x -> MetaInstantiation
to :: forall x. Rep MetaInstantiation x -> MetaInstantiation
Generic
data Instantiation = Instantiation
{ Instantiation -> [Arg String]
instTel :: [Arg String]
, Instantiation -> Term
instBody :: Term
}
deriving (Int -> Instantiation -> ShowS
[Instantiation] -> ShowS
Instantiation -> String
(Int -> Instantiation -> ShowS)
-> (Instantiation -> String)
-> ([Instantiation] -> ShowS)
-> Show Instantiation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Instantiation -> ShowS
showsPrec :: Int -> Instantiation -> ShowS
$cshow :: Instantiation -> String
show :: Instantiation -> String
$cshowList :: [Instantiation] -> ShowS
showList :: [Instantiation] -> ShowS
Show, (forall x. Instantiation -> Rep Instantiation x)
-> (forall x. Rep Instantiation x -> Instantiation)
-> Generic Instantiation
forall x. Rep Instantiation x -> Instantiation
forall x. Instantiation -> Rep Instantiation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Instantiation -> Rep Instantiation x
from :: forall x. Instantiation -> Rep Instantiation x
$cto :: forall x. Rep Instantiation x -> Instantiation
to :: forall x. Rep Instantiation x -> Instantiation
Generic)
data RemoteMetaVariable = RemoteMetaVariable
{ RemoteMetaVariable -> Instantiation
rmvInstantiation :: Instantiation
, RemoteMetaVariable -> Modality
rmvModality :: Modality
, RemoteMetaVariable -> Judgement MetaId
rmvJudgement :: Judgement MetaId
}
deriving (Int -> RemoteMetaVariable -> ShowS
[RemoteMetaVariable] -> ShowS
RemoteMetaVariable -> String
(Int -> RemoteMetaVariable -> ShowS)
-> (RemoteMetaVariable -> String)
-> ([RemoteMetaVariable] -> ShowS)
-> Show RemoteMetaVariable
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RemoteMetaVariable -> ShowS
showsPrec :: Int -> RemoteMetaVariable -> ShowS
$cshow :: RemoteMetaVariable -> String
show :: RemoteMetaVariable -> String
$cshowList :: [RemoteMetaVariable] -> ShowS
showList :: [RemoteMetaVariable] -> ShowS
Show, (forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x)
-> (forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable)
-> Generic RemoteMetaVariable
forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
from :: forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
$cto :: forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
to :: forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
Generic)
data CheckedTarget = CheckedTarget (Maybe ProblemId)
| NotCheckedTarget
data PrincipalArgTypeMetas = PrincipalArgTypeMetas
{ PrincipalArgTypeMetas -> Args
patmMetas :: Args
, PrincipalArgTypeMetas -> Type
patmRemainder :: Type
}
deriving (forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x)
-> (forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas)
-> Generic PrincipalArgTypeMetas
forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
from :: forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
$cto :: forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
to :: forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
Generic
data TypeCheckingProblem
= CheckExpr Comparison A.Expr Type
| CheckArgs Comparison ExpandHidden Range [NamedArg A.Expr] Type Type (ArgsCheckState CheckedTarget -> TCM Term)
| CheckProjAppToKnownPrincipalArg Comparison A.Expr ProjOrigin (List1 QName) A.Args Type Int Term Type PrincipalArgTypeMetas
| CheckLambda Comparison (Arg (List1 (WithHiding Name), Maybe Type)) A.Expr Type
| DoQuoteTerm Comparison Term Type
deriving (forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x)
-> (forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem)
-> Generic TypeCheckingProblem
forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
from :: forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
$cto :: forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
to :: forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
Generic
instance Pretty MetaInstantiation where
pretty :: MetaInstantiation -> Doc
pretty = \case
OpenMeta MetaKind
UnificationMeta -> Doc
"Open"
OpenMeta MetaKind
InstanceMeta -> Doc
"OpenInstance"
PostponedTypeCheckingProblem{} -> Doc
"PostponedTypeCheckingProblem (...)"
BlockedConst Term
t -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"BlockedConst", Doc -> Doc
parens (Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t) ]
InstV Instantiation{ [Arg String]
instTel :: Instantiation -> [Arg String]
instTel :: [Arg String]
instTel, Term
instBody :: Instantiation -> Term
instBody :: Term
instBody } -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"InstV", [Arg String] -> Doc
forall a. Pretty a => a -> Doc
pretty [Arg String]
instTel, Doc -> Doc
parens (Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
instBody) ]
newtype MetaPriority = MetaPriority Int
deriving (MetaPriority -> MetaPriority -> Bool
(MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool) -> Eq MetaPriority
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaPriority -> MetaPriority -> Bool
== :: MetaPriority -> MetaPriority -> Bool
$c/= :: MetaPriority -> MetaPriority -> Bool
/= :: MetaPriority -> MetaPriority -> Bool
Eq, Eq MetaPriority
Eq MetaPriority =>
(MetaPriority -> MetaPriority -> Ordering)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> MetaPriority)
-> (MetaPriority -> MetaPriority -> MetaPriority)
-> Ord MetaPriority
MetaPriority -> MetaPriority -> Bool
MetaPriority -> MetaPriority -> Ordering
MetaPriority -> MetaPriority -> MetaPriority
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MetaPriority -> MetaPriority -> Ordering
compare :: MetaPriority -> MetaPriority -> Ordering
$c< :: MetaPriority -> MetaPriority -> Bool
< :: MetaPriority -> MetaPriority -> Bool
$c<= :: MetaPriority -> MetaPriority -> Bool
<= :: MetaPriority -> MetaPriority -> Bool
$c> :: MetaPriority -> MetaPriority -> Bool
> :: MetaPriority -> MetaPriority -> Bool
$c>= :: MetaPriority -> MetaPriority -> Bool
>= :: MetaPriority -> MetaPriority -> Bool
$cmax :: MetaPriority -> MetaPriority -> MetaPriority
max :: MetaPriority -> MetaPriority -> MetaPriority
$cmin :: MetaPriority -> MetaPriority -> MetaPriority
min :: MetaPriority -> MetaPriority -> MetaPriority
Ord, Int -> MetaPriority -> ShowS
[MetaPriority] -> ShowS
MetaPriority -> String
(Int -> MetaPriority -> ShowS)
-> (MetaPriority -> String)
-> ([MetaPriority] -> ShowS)
-> Show MetaPriority
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaPriority -> ShowS
showsPrec :: Int -> MetaPriority -> ShowS
$cshow :: MetaPriority -> String
show :: MetaPriority -> String
$cshowList :: [MetaPriority] -> ShowS
showList :: [MetaPriority] -> ShowS
Show, MetaPriority -> ()
(MetaPriority -> ()) -> NFData MetaPriority
forall a. (a -> ()) -> NFData a
$crnf :: MetaPriority -> ()
rnf :: MetaPriority -> ()
NFData)
data RunMetaOccursCheck
= RunMetaOccursCheck
| DontRunMetaOccursCheck
deriving (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
(RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> Eq RunMetaOccursCheck
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
== :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c/= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
/= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
Eq, Eq RunMetaOccursCheck
Eq RunMetaOccursCheck =>
(RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck)
-> Ord RunMetaOccursCheck
RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
$c< :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
< :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c<= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
<= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c> :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
> :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c>= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
>= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$cmax :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
$cmin :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
Ord, Int -> RunMetaOccursCheck -> ShowS
[RunMetaOccursCheck] -> ShowS
RunMetaOccursCheck -> String
(Int -> RunMetaOccursCheck -> ShowS)
-> (RunMetaOccursCheck -> String)
-> ([RunMetaOccursCheck] -> ShowS)
-> Show RunMetaOccursCheck
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RunMetaOccursCheck -> ShowS
showsPrec :: Int -> RunMetaOccursCheck -> ShowS
$cshow :: RunMetaOccursCheck -> String
show :: RunMetaOccursCheck -> String
$cshowList :: [RunMetaOccursCheck] -> ShowS
showList :: [RunMetaOccursCheck] -> ShowS
Show, (forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x)
-> (forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck)
-> Generic RunMetaOccursCheck
forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
from :: forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
$cto :: forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
to :: forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
Generic)
data MetaInfo = MetaInfo
{ MetaInfo -> Closure Range
miClosRange :: Closure Range
, MetaInfo -> Modality
miModality :: Modality
, MetaInfo -> RunMetaOccursCheck
miMetaOccursCheck :: RunMetaOccursCheck
, MetaInfo -> String
miNameSuggestion :: MetaNameSuggestion
, MetaInfo -> Arg DoGeneralize
miGeneralizable :: Arg DoGeneralize
}
deriving (forall x. MetaInfo -> Rep MetaInfo x)
-> (forall x. Rep MetaInfo x -> MetaInfo) -> Generic MetaInfo
forall x. Rep MetaInfo x -> MetaInfo
forall x. MetaInfo -> Rep MetaInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInfo -> Rep MetaInfo x
from :: forall x. MetaInfo -> Rep MetaInfo x
$cto :: forall x. Rep MetaInfo x -> MetaInfo
to :: forall x. Rep MetaInfo x -> MetaInfo
Generic
instance LensModality MetaInfo where
getModality :: MetaInfo -> Modality
getModality = MetaInfo -> Modality
miModality
setModality :: Modality -> MetaInfo -> MetaInfo
setModality Modality
mod MetaInfo
mi = MetaInfo
mi { miModality = mod }
mapModality :: (Modality -> Modality) -> MetaInfo -> MetaInfo
mapModality Modality -> Modality
f MetaInfo
mi = MetaInfo
mi { miModality = f $ miModality mi }
instance LensQuantity MetaInfo where
getQuantity :: MetaInfo -> Quantity
getQuantity = Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity)
-> (MetaInfo -> Modality) -> MetaInfo -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Modality
forall a. LensModality a => a -> Modality
getModality
mapQuantity :: (Quantity -> Quantity) -> MetaInfo -> MetaInfo
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> MetaInfo -> MetaInfo
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)
instance LensRelevance MetaInfo where
mapRelevance :: (Relevance -> Relevance) -> MetaInfo -> MetaInfo
mapRelevance Relevance -> Relevance
f = (Modality -> Modality) -> MetaInfo -> MetaInfo
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Relevance -> Relevance) -> Modality -> Modality
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)
data NamedMeta = NamedMeta
{ NamedMeta -> String
nmSuggestion :: MetaNameSuggestion
, NamedMeta -> MetaId
nmid :: MetaId
}
suffixNameSuggestion :: MetaNameSuggestion -> ArgName -> MetaNameSuggestion
suffixNameSuggestion :: String -> ShowS
suffixNameSuggestion String
"_" String
field = String
field
suffixNameSuggestion String
"" String
field = String
field
suffixNameSuggestion String
record String
field = String
record String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
field
instance Pretty NamedMeta where
pretty :: NamedMeta -> Doc
pretty (NamedMeta String
"" MetaId
x) = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
pretty (NamedMeta String
"_" MetaId
x) = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
pretty (NamedMeta String
s MetaId
x) = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
x
type LocalMetaStore = Map MetaId MetaVariable
{-# SPECIALIZE Map.insert :: MetaId -> v -> Map MetaId v -> Map MetaId v #-}
{-# SPECIALIZE Map.lookup :: MetaId -> Map MetaId v -> Maybe v #-}
type RemoteMetaStore = HashMap MetaId RemoteMetaVariable
instance HasRange MetaInfo where
getRange :: MetaInfo -> Range
getRange = Closure Range -> Range
forall a. Closure a -> a
clValue (Closure Range -> Range)
-> (MetaInfo -> Closure Range) -> MetaInfo -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Closure Range
miClosRange
instance HasRange MetaVariable where
getRange :: MetaVariable -> Range
getRange MetaVariable
m = Closure Range -> Range
forall a. HasRange a => a -> Range
getRange (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m
instance SetRange MetaInfo where
setRange :: Range -> MetaInfo -> MetaInfo
setRange Range
r MetaInfo
m = MetaInfo
m { miClosRange = (miClosRange m) { clValue = r }}
instance SetRange MetaVariable where
setRange :: Range -> MetaVariable -> MetaVariable
setRange Range
r MetaVariable
m = MetaVariable
m { mvInfo = setRange r (mvInfo m) }
instance LensModality MetaVariable where
getModality :: MetaVariable -> Modality
getModality = MetaInfo -> Modality
forall a. LensModality a => a -> Modality
getModality (MetaInfo -> Modality)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Modality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo
setModality :: Modality -> MetaVariable -> MetaVariable
setModality Modality
mod MetaVariable
mv = MetaVariable
mv { mvInfo = setModality mod $ mvInfo mv }
mapModality :: (Modality -> Modality) -> MetaVariable -> MetaVariable
mapModality Modality -> Modality
f MetaVariable
mv = MetaVariable
mv { mvInfo = mapModality f $ mvInfo mv }
instance LensRelevance MetaVariable where
setRelevance :: Relevance -> MetaVariable -> MetaVariable
setRelevance Relevance
mod MetaVariable
mv = MetaVariable
mv { mvInfo = setRelevance mod $ mvInfo mv }
instance LensQuantity MetaVariable where
getQuantity :: MetaVariable -> Quantity
getQuantity = Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity)
-> (MetaVariable -> Modality) -> MetaVariable -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality
mapQuantity :: (Quantity -> Quantity) -> MetaVariable -> MetaVariable
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> MetaVariable -> MetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)
instance LensModality RemoteMetaVariable where
getModality :: RemoteMetaVariable -> Modality
getModality = RemoteMetaVariable -> Modality
rmvModality
mapModality :: (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
mapModality Modality -> Modality
f RemoteMetaVariable
mv = RemoteMetaVariable
mv { rmvModality = f $ rmvModality mv }
instance LensRelevance RemoteMetaVariable where
mapRelevance :: (Relevance -> Relevance)
-> RemoteMetaVariable -> RemoteMetaVariable
mapRelevance Relevance -> Relevance
f = (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Relevance -> Relevance) -> Modality -> Modality
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)
instance LensQuantity RemoteMetaVariable where
mapQuantity :: (Quantity -> Quantity) -> RemoteMetaVariable -> RemoteMetaVariable
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)
normalMetaPriority :: MetaPriority
normalMetaPriority :: MetaPriority
normalMetaPriority = Int -> MetaPriority
MetaPriority Int
0
lowMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
lowMetaPriority = Int -> MetaPriority
MetaPriority (-Int
10)
highMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
highMetaPriority = Int -> MetaPriority
MetaPriority Int
10
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Closure Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope MetaVariable
m = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv MetaVariable
m = Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Range -> TCEnv) -> Closure Range -> TCEnv
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m
getMetaSig :: MetaVariable -> Signature
getMetaSig :: MetaVariable -> Signature
getMetaSig MetaVariable
m = Closure Range -> Signature
forall a. Closure a -> Signature
clSignature (Closure Range -> Signature) -> Closure Range -> Signature
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m
metaFrozen :: Lens' MetaVariable Frozen
metaFrozen :: Lens' MetaVariable Frozen
metaFrozen Frozen -> f Frozen
f MetaVariable
mv = Frozen -> f Frozen
f (MetaVariable -> Frozen
mvFrozen MetaVariable
mv) f Frozen -> (Frozen -> MetaVariable) -> f MetaVariable
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Frozen
x -> MetaVariable
mv { mvFrozen = x }
_mvInfo :: Lens' MetaVariable MetaInfo