{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.TypeChecking.Monad.Base where
import Prelude hiding (null)
import qualified Control.Concurrent as C
import qualified Control.Exception as E
#if __GLASGOW_HASKELL__ >= 800
import qualified Control.Monad.Fail as Fail
#endif
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Maybe
import Control.Applicative hiding (empty)
import Data.Function
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Sequence (Seq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup ( Semigroup, (<>), Any(..) )
import Data.Data (Data, toConstr)
import Data.Foldable (Foldable)
import Data.String
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
import Data.Traversable
import Data.IORef
import qualified System.Console.Haskeline as Haskeline
import Agda.Benchmarking (Benchmark, Phase)
import Agda.Syntax.Concrete (TopLevelModuleName)
import Agda.Syntax.Common
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.Abstract (AllNames)
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern ()
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Literal
import Agda.Syntax.Parser (PM(..), ParseWarning, runPMIO)
import Agda.Syntax.Parser.Monad (parseWarningName)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Free.Lazy (Free(freeVars'), bind', bind)
import Agda.Termination.CutOff
import {-# SOURCE #-} Agda.Compiler.Backend
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Interaction.Response
(InteractionOutputCallback, defaultInteractionOutputCallback, Response(..))
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import Agda.Interaction.Library
import Agda.Utils.Except
( Error(strMsg)
, ExceptT
, MonadError(catchError, throwError)
, runExceptT
, mapExceptT
)
import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.FileName
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.NonemptyList
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty hiding ((<>))
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Functor
import Agda.Utils.Function
import Agda.Utils.WithDefault ( collapseDefault )
#include "undefined.h"
import Agda.Utils.Impossible
data TCState = TCSt
{ stPreScopeState :: !PreScopeState
, stPostScopeState :: !PostScopeState
, stPersistentState :: !PersistentTCState
}
class Monad m => ReadTCState m where
getTCState :: m TCState
withTCState :: (TCState -> TCState) -> m a -> m a
instance ReadTCState m => ReadTCState (MaybeT m) where
getTCState = lift getTCState
withTCState = mapMaybeT . withTCState
instance ReadTCState m => ReadTCState (ListT m) where
getTCState = lift getTCState
withTCState f = ListT . withTCState f . runListT
instance ReadTCState m => ReadTCState (ExceptT err m) where
getTCState = lift getTCState
withTCState = mapExceptT . withTCState
instance ReadTCState m => ReadTCState (ReaderT r m) where
getTCState = lift getTCState
withTCState = mapReaderT . withTCState
instance (Monoid w, ReadTCState m) => ReadTCState (WriterT w m) where
getTCState = lift getTCState
withTCState = mapWriterT . withTCState
instance ReadTCState m => ReadTCState (StateT s m) where
getTCState = lift getTCState
withTCState = mapStateT . withTCState
instance Show TCState where
show _ = "TCSt{}"
data PreScopeState = PreScopeState
{ stPreTokens :: !CompressedFile
, stPreImports :: !Signature
, stPreImportedModules :: !(Set ModuleName)
, stPreModuleToSource :: !ModuleToSource
, stPreVisitedModules :: !VisitedModules
, stPreScope :: !ScopeInfo
, stPrePatternSyns :: !A.PatternSynDefns
, stPrePatternSynImports :: !A.PatternSynDefns
, stPreGeneralizedVars :: !(Maybe (Set QName))
, stPrePragmaOptions :: !PragmaOptions
, stPreImportedBuiltins :: !(BuiltinThings PrimFun)
, stPreImportedDisplayForms :: !DisplayForms
, stPreImportedInstanceDefs :: !InstanceTable
, stPreForeignCode :: !(Map BackendName [ForeignCode])
, stPreFreshInteractionId :: !InteractionId
, stPreImportedUserWarnings :: !(Map A.QName String)
, stPreLocalUserWarnings :: !(Map A.QName String)
}
type DisambiguatedNames = IntMap A.QName
data PostScopeState = PostScopeState
{ stPostSyntaxInfo :: !CompressedFile
, stPostDisambiguatedNames :: !DisambiguatedNames
, stPostMetaStore :: !MetaStore
, stPostInteractionPoints :: !InteractionPoints
, stPostAwakeConstraints :: !Constraints
, stPostSleepingConstraints :: !Constraints
, stPostDirty :: !Bool
, stPostOccursCheckDefs :: !(Set QName)
, stPostSignature :: !Signature
, stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
, stPostImportsDisplayForms :: !DisplayForms
, stPostCurrentModule :: !(Maybe ModuleName)
, stPostInstanceDefs :: !TempInstanceTable
, stPostConcreteNames :: !(Map Name [C.Name])
, stPostShadowingNames :: !(Map Name [Name])
, stPostStatistics :: !Statistics
, stPostTCWarnings :: ![TCWarning]
, stPostMutualBlocks :: !(Map MutualId MutualBlock)
, stPostLocalBuiltins :: !(BuiltinThings PrimFun)
, stPostFreshMetaId :: !MetaId
, stPostFreshMutualId :: !MutualId
, stPostFreshProblemId :: !ProblemId
, stPostFreshCheckpointId :: !CheckpointId
, stPostFreshInt :: !Int
, stPostFreshNameId :: !NameId
, stPostAreWeCaching :: !Bool
, stPostConsideringInstance :: !Bool
}
data MutualBlock = MutualBlock
{ mutualInfo :: Info.MutualInfo
, mutualNames :: Set QName
} deriving (Show, Eq)
instance Null MutualBlock where
empty = MutualBlock empty empty
data PersistentTCState = PersistentTCSt
{ stDecodedModules :: DecodedModules
, stPersistentOptions :: CommandLineOptions
, stInteractionOutputCallback :: InteractionOutputCallback
, stBenchmark :: !Benchmark
, stAccumStatistics :: !Statistics
, stLoadedFileCache :: !(Maybe LoadedFileCache)
, stPersistBackends :: [Backend]
}
data LoadedFileCache = LoadedFileCache
{ lfcCached :: !CachedTypeCheckLog
, lfcCurrent :: !CurrentTypeCheckLog
}
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data TypeCheckAction
= EnterSection !Info.ModuleInfo !ModuleName !A.Telescope
| LeaveSection !ModuleName
| Decl !A.Declaration
| Pragmas !PragmaOptions
initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
{ stPersistentOptions = defaultOptions
, stDecodedModules = Map.empty
, stInteractionOutputCallback = defaultInteractionOutputCallback
, stBenchmark = empty
, stAccumStatistics = Map.empty
, stLoadedFileCache = Nothing
, stPersistBackends = []
}
initPreScopeState :: PreScopeState
initPreScopeState = PreScopeState
{ stPreTokens = mempty
, stPreImports = emptySignature
, stPreImportedModules = Set.empty
, stPreModuleToSource = Map.empty
, stPreVisitedModules = Map.empty
, stPreScope = emptyScopeInfo
, stPrePatternSyns = Map.empty
, stPrePatternSynImports = Map.empty
, stPreGeneralizedVars = mempty
, stPrePragmaOptions = defaultInteractionOptions
, stPreImportedBuiltins = Map.empty
, stPreImportedDisplayForms = HMap.empty
, stPreImportedInstanceDefs = Map.empty
, stPreForeignCode = Map.empty
, stPreFreshInteractionId = 0
, stPreImportedUserWarnings = Map.empty
, stPreLocalUserWarnings = Map.empty
}
initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
{ stPostSyntaxInfo = mempty
, stPostDisambiguatedNames = IntMap.empty
, stPostMetaStore = IntMap.empty
, stPostInteractionPoints = Map.empty
, stPostAwakeConstraints = []
, stPostSleepingConstraints = []
, stPostDirty = False
, stPostOccursCheckDefs = Set.empty
, stPostSignature = emptySignature
, stPostModuleCheckpoints = Map.empty
, stPostImportsDisplayForms = HMap.empty
, stPostCurrentModule = Nothing
, stPostInstanceDefs = (Map.empty , Set.empty)
, stPostConcreteNames = Map.empty
, stPostShadowingNames = Map.empty
, stPostStatistics = Map.empty
, stPostTCWarnings = []
, stPostMutualBlocks = Map.empty
, stPostLocalBuiltins = Map.empty
, stPostFreshMetaId = 0
, stPostFreshMutualId = 0
, stPostFreshProblemId = 1
, stPostFreshCheckpointId = 1
, stPostFreshInt = 0
, stPostFreshNameId = NameId 0 0
, stPostAreWeCaching = False
, stPostConsideringInstance = False
}
initState :: TCState
initState = TCSt
{ stPreScopeState = initPreScopeState
, stPostScopeState = initPostScopeState
, stPersistentState = initPersistentState
}
stTokens :: Lens' CompressedFile TCState
stTokens f s =
f (stPreTokens (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreTokens = x}}
stImports :: Lens' Signature TCState
stImports f s =
f (stPreImports (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImports = x}}
stImportedModules :: Lens' (Set ModuleName) TCState
stImportedModules f s =
f (stPreImportedModules (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedModules = x}}
stModuleToSource :: Lens' ModuleToSource TCState
stModuleToSource f s =
f (stPreModuleToSource (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreModuleToSource = x}}
stVisitedModules :: Lens' VisitedModules TCState
stVisitedModules f s =
f (stPreVisitedModules (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreVisitedModules = x}}
stScope :: Lens' ScopeInfo TCState
stScope f s =
f (stPreScope (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreScope = x}}
stPatternSyns :: Lens' A.PatternSynDefns TCState
stPatternSyns f s =
f (stPrePatternSyns (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSyns = x}}
stPatternSynImports :: Lens' A.PatternSynDefns TCState
stPatternSynImports f s =
f (stPrePatternSynImports (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSynImports = x}}
stGeneralizedVars :: Lens' (Maybe (Set QName)) TCState
stGeneralizedVars f s =
f (stPreGeneralizedVars (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreGeneralizedVars = x}}
stPragmaOptions :: Lens' PragmaOptions TCState
stPragmaOptions f s =
f (stPrePragmaOptions (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePragmaOptions = x}}
stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins f s =
f (stPreImportedBuiltins (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedBuiltins = x}}
stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState
stForeignCode f s =
f (stPreForeignCode (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreForeignCode = x}}
stFreshInteractionId :: Lens' InteractionId TCState
stFreshInteractionId f s =
f (stPreFreshInteractionId (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}
stImportedUserWarnings :: Lens' (Map A.QName String) TCState
stImportedUserWarnings f s =
f (stPreImportedUserWarnings (stPreScopeState s)) <&>
\ x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}}
stLocalUserWarnings :: Lens' (Map A.QName String) TCState
stLocalUserWarnings f s =
f (stPreLocalUserWarnings (stPreScopeState s)) <&>
\ x -> s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}}
getUserWarnings :: MonadTCState m => m (Map A.QName String)
getUserWarnings = do
iuw <- useTC stImportedUserWarnings
luw <- useTC stLocalUserWarnings
return $ iuw `Map.union` luw
stBackends :: Lens' [Backend] TCState
stBackends f s =
f (stPersistBackends (stPersistentState s)) <&>
\x -> s {stPersistentState = (stPersistentState s) {stPersistBackends = x}}
stFreshNameId :: Lens' NameId TCState
stFreshNameId f s =
f (stPostFreshNameId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshNameId = x}}
stSyntaxInfo :: Lens' CompressedFile TCState
stSyntaxInfo f s =
f (stPostSyntaxInfo (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSyntaxInfo = x}}
stDisambiguatedNames :: Lens' DisambiguatedNames TCState
stDisambiguatedNames f s =
f (stPostDisambiguatedNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostDisambiguatedNames = x}}
stMetaStore :: Lens' MetaStore TCState
stMetaStore f s =
f (stPostMetaStore (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostMetaStore = x}}
stInteractionPoints :: Lens' InteractionPoints TCState
stInteractionPoints f s =
f (stPostInteractionPoints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}}
stAwakeConstraints :: Lens' Constraints TCState
stAwakeConstraints f s =
f (stPostAwakeConstraints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostAwakeConstraints = x}}
stSleepingConstraints :: Lens' Constraints TCState
stSleepingConstraints f s =
f (stPostSleepingConstraints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSleepingConstraints = x}}
stDirty :: Lens' Bool TCState
stDirty f s =
f (stPostDirty (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostDirty = x}}
stOccursCheckDefs :: Lens' (Set QName) TCState
stOccursCheckDefs f s =
f (stPostOccursCheckDefs (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostOccursCheckDefs = x}}
stSignature :: Lens' Signature TCState
stSignature f s =
f (stPostSignature (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}}
stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints f s =
f (stPostModuleCheckpoints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostModuleCheckpoints = x}}
stImportsDisplayForms :: Lens' DisplayForms TCState
stImportsDisplayForms f s =
f (stPostImportsDisplayForms (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostImportsDisplayForms = x}}
stImportedDisplayForms :: Lens' DisplayForms TCState
stImportedDisplayForms f s =
f (stPreImportedDisplayForms (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}}
stCurrentModule :: Lens' (Maybe ModuleName) TCState
stCurrentModule f s =
f (stPostCurrentModule (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = x}}
stImportedInstanceDefs :: Lens' InstanceTable TCState
stImportedInstanceDefs f s =
f (stPreImportedInstanceDefs (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedInstanceDefs = x}}
stInstanceDefs :: Lens' TempInstanceTable TCState
stInstanceDefs f s =
f (stPostInstanceDefs (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostInstanceDefs = x}}
stConcreteNames :: Lens' (Map Name [C.Name]) TCState
stConcreteNames f s =
f (stPostConcreteNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostConcreteNames = x}}
stShadowingNames :: Lens' (Map Name [Name]) TCState
stShadowingNames f s =
f (stPostShadowingNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostShadowingNames = x}}
stStatistics :: Lens' Statistics TCState
stStatistics f s =
f (stPostStatistics (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}}
stTCWarnings :: Lens' [TCWarning] TCState
stTCWarnings f s =
f (stPostTCWarnings (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}}
stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks f s =
f (stPostMutualBlocks (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}}
stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins f s =
f (stPostLocalBuiltins (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostLocalBuiltins = x}}
stFreshMetaId :: Lens' MetaId TCState
stFreshMetaId f s =
f (stPostFreshMetaId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMetaId = x}}
stFreshMutualId :: Lens' MutualId TCState
stFreshMutualId f s =
f (stPostFreshMutualId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMutualId = x}}
stFreshProblemId :: Lens' ProblemId TCState
stFreshProblemId f s =
f (stPostFreshProblemId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshProblemId = x}}
stFreshCheckpointId :: Lens' CheckpointId TCState
stFreshCheckpointId f s =
f (stPostFreshCheckpointId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshCheckpointId = x}}
stFreshInt :: Lens' Int TCState
stFreshInt f s =
f (stPostFreshInt (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshInt = x}}
stAreWeCaching :: Lens' Bool TCState
stAreWeCaching f s =
f (stPostAreWeCaching (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostAreWeCaching = x}}
stConsideringInstance :: Lens' Bool TCState
stConsideringInstance f s =
f (stPostConsideringInstance (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostConsideringInstance = x}}
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings s = (s^.stLocalBuiltins) `Map.union` (s^.stImportedBuiltins)
class Enum i => HasFresh i where
freshLens :: Lens' i TCState
nextFresh' :: i -> i
nextFresh' = succ
nextFresh :: HasFresh i => TCState -> (i, TCState)
nextFresh s =
let !c = s^.freshLens
in (c, set freshLens (nextFresh' c) s)
fresh :: (HasFresh i, MonadTCState m) => m i
fresh =
do !s <- getTC
let (!c , !s') = nextFresh s
putTC s'
return c
instance HasFresh MetaId where
freshLens = stFreshMetaId
instance HasFresh MutualId where
freshLens = stFreshMutualId
instance HasFresh InteractionId where
freshLens = stFreshInteractionId
instance HasFresh NameId where
freshLens = stFreshNameId
nextFresh' = succ . succ
instance HasFresh Int where
freshLens = stFreshInt
newtype ProblemId = ProblemId Nat
deriving (Data, Eq, Ord, Enum, Real, Integral, Num)
instance Show ProblemId where
show (ProblemId n) = show n
instance Pretty ProblemId where
pretty (ProblemId n) = pretty n
instance HasFresh ProblemId where
freshLens = stFreshProblemId
newtype CheckpointId = CheckpointId Int
deriving (Data, Eq, Ord, Enum, Real, Integral, Num)
instance Show CheckpointId where
show (CheckpointId n) = show n
instance Pretty CheckpointId where
pretty (CheckpointId n) = pretty n
instance HasFresh CheckpointId where
freshLens = stFreshCheckpointId
freshName :: MonadTCState m => Range -> String -> m Name
freshName r s = do
i <- fresh
return $ mkName r i s
freshNoName :: MonadTCState m => Range -> m Name
freshNoName r =
do i <- fresh
return $ Name i (C.NoName noRange i) r noFixity' False
freshNoName_ :: MonadTCState m => m Name
freshNoName_ = freshNoName noRange
freshRecordName :: MonadTCState m => m Name
freshRecordName = do
i <- fresh
return $ Name i (C.Name noRange C.NotInScope [C.Id "r"]) noRange noFixity' True
class FreshName a where
freshName_ :: MonadTCState m => a -> m Name
instance FreshName (Range, String) where
freshName_ = uncurry freshName
instance FreshName String where
freshName_ = freshName noRange
instance FreshName Range where
freshName_ = freshNoName
instance FreshName () where
freshName_ () = freshNoName_
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
sourceToModule =
Map.fromList
. List.map (\(m, f) -> (f, m))
. Map.toList
<$> useTC stModuleToSource
lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
lookupModuleFromSource f =
fmap fst . List.find ((f ==) . snd) . Map.toList <$> useTC stModuleToSource
data ModuleInfo = ModuleInfo
{ miInterface :: Interface
, miWarnings :: Bool
, miPrimitive :: Bool
}
type VisitedModules = Map C.TopLevelModuleName ModuleInfo
type DecodedModules = Map C.TopLevelModuleName Interface
data ForeignCode = ForeignCode Range String
deriving Show
data Interface = Interface
{ iSourceHash :: Hash
, iSource :: Text
, iFileType :: FileType
, iImportedModules :: [(ModuleName, Hash)]
, iModuleName :: ModuleName
, iScope :: Map ModuleName Scope
, iInsideScope :: ScopeInfo
, iSignature :: Signature
, iDisplayForms :: DisplayForms
, iUserWarnings :: Map A.QName String
, iBuiltin :: BuiltinThings (String, QName)
, iForeignCode :: Map BackendName [ForeignCode]
, iHighlighting :: HighlightingInfo
, iPragmaOptions :: [OptionsPragma]
, iOptionsUsed :: PragmaOptions
, iPatternSyns :: A.PatternSynDefns
, iWarnings :: [TCWarning]
}
deriving Show
instance Pretty Interface where
pretty (Interface
sourceH source fileT importedM moduleN scope insideS signature
display userwarn builtin foreignCode highlighting pragmaO
oUsed patternS warnings) =
hang "Interface" 2 $ vcat
[ "source hash:" <+> (pretty . show) sourceH
, "source:" $$ nest 2 (text $ T.unpack source)
, "file type:" <+> (pretty . show) fileT
, "imported modules:" <+> (pretty . show) importedM
, "module name:" <+> pretty moduleN
, "scope:" <+> (pretty . show) scope
, "inside scope:" <+> (pretty . show) insideS
, "signature:" <+> (pretty . show) signature
, "display:" <+> (pretty . show) display
, "user warnings:" <+> (pretty . show) userwarn
, "builtin:" <+> (pretty . show) builtin
, "Foreign code:" <+> (pretty . show) foreignCode
, "highlighting:" <+> (pretty . show) highlighting
, "pragma options:" <+> (pretty . show) pragmaO
, "options used:" <+> (pretty . show) oUsed
, "pattern syns:" <+> (pretty . show) patternS
, "warnings:" <+> (pretty . show) warnings
]
iFullHash :: Interface -> Hash
iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i)
data Closure a = Closure
{ clSignature :: Signature
, clEnv :: TCEnv
, clScope :: ScopeInfo
, clModuleCheckpoints :: Map ModuleName CheckpointId
, clValue :: a
}
deriving (Data, Functor, Foldable)
instance Show a => Show (Closure a) where
show cl = "Closure { clValue = " ++ show (clValue cl) ++ " }"
instance HasRange a => HasRange (Closure a) where
getRange = getRange . clValue
buildClosure :: a -> TCM (Closure a)
buildClosure x = do
env <- askTC
sig <- useTC stSignature
scope <- useTC stScope
cps <- useTC stModuleCheckpoints
return $ Closure sig env scope cps x
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
{ constraintProblems :: Set ProblemId
, theConstraint :: Closure Constraint
}
deriving (Data, Show)
instance HasRange ProblemConstraint where
getRange = getRange . theConstraint
data Constraint
= ValueCmp Comparison Type Term Term
| ValueCmpOnFace Comparison Term Type Term Term
| ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
| TypeCmp Comparison Type Type
| TelCmp Type Type Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Level Level
| HasBiggerSort Sort
| HasPTSRule Sort (Abs Sort)
| UnBlock MetaId
| Guarded Constraint ProblemId
| IsEmpty Range Type
| CheckSizeLtSat Term
| FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])
| CheckFunDef Delayed Info.DefInfo QName [A.Clause]
| UnquoteTactic (Maybe MetaId) Term Term Type
deriving (Data, Show)
instance HasRange Constraint where
getRange (IsEmpty r t) = r
getRange _ = noRange
instance Free Constraint where
freeVars' c =
case c of
ValueCmp _ t u v -> freeVars' (t, (u, v))
ValueCmpOnFace _ p t u v -> freeVars' (p, (t, (u, v)))
ElimCmp _ _ t u es es' -> freeVars' ((t, u), (es, es'))
TypeCmp _ t t' -> freeVars' (t, t')
TelCmp _ _ _ tel tel' -> freeVars' (tel, tel')
SortCmp _ s s' -> freeVars' (s, s')
LevelCmp _ l l' -> freeVars' (l, l')
UnBlock _ -> mempty
Guarded c _ -> freeVars' c
IsEmpty _ t -> freeVars' t
CheckSizeLtSat u -> freeVars' u
FindInstance _ _ cs -> freeVars' cs
CheckFunDef _ _ _ _ -> mempty
HasBiggerSort s -> freeVars' s
HasPTSRule s1 s2 -> freeVars' (s1 , s2)
UnquoteTactic _ t h g -> freeVars' (t, (h, g))
instance TermLike Constraint where
foldTerm f = \case
ValueCmp _ t u v -> foldTerm f (t, u, v)
ValueCmpOnFace _ p t u v -> foldTerm f (p, t, u, v)
ElimCmp _ _ t u es es' -> foldTerm f (t, u, es, es')
TypeCmp _ t t' -> foldTerm f (t, t')
LevelCmp _ l l' -> foldTerm f (l, l')
IsEmpty _ t -> foldTerm f t
CheckSizeLtSat u -> foldTerm f u
UnquoteTactic _ t h g -> foldTerm f (t, h, g)
Guarded c _ -> foldTerm f c
TelCmp _ _ _ tel1 tel2 -> foldTerm f (tel1, tel2)
SortCmp _ s1 s2 -> foldTerm f (s1, s2)
UnBlock _ -> mempty
FindInstance _ _ _ -> mempty
CheckFunDef _ _ _ _ -> mempty
HasBiggerSort s -> foldTerm f s
HasPTSRule s1 s2 -> foldTerm f (s1, s2)
traverseTermM f c = __IMPOSSIBLE__
data Comparison = CmpEq | CmpLeq
deriving (Eq, Data, Show)
instance Pretty Comparison where
pretty CmpEq = "="
pretty CmpLeq = "=<"
data CompareDirection = DirEq | DirLeq | DirGeq
deriving (Eq, Show)
instance Pretty CompareDirection where
pretty = text . \case
DirEq -> "="
DirLeq -> "=<"
DirGeq -> ">="
fromCmp :: Comparison -> CompareDirection
fromCmp CmpEq = DirEq
fromCmp CmpLeq = DirLeq
flipCmp :: CompareDirection -> CompareDirection
flipCmp DirEq = DirEq
flipCmp DirLeq = DirGeq
flipCmp DirGeq = DirLeq
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp cont DirEq = cont CmpEq
dirToCmp cont DirLeq = cont CmpLeq
dirToCmp cont DirGeq = flip $ cont CmpLeq
data Open a = OpenThing { openThingCheckpoint :: CheckpointId, openThing :: a }
deriving (Data, Show, Functor, Foldable, Traversable)
instance Decoration Open where
traverseF f (OpenThing cp x) = OpenThing cp <$> f x
data Judgement a
= HasType { jMetaId :: a, jMetaType :: Type }
| IsSort { jMetaId :: a, jMetaType :: Type }
instance Show a => Show (Judgement a) where
show (HasType a t) = show a ++ " : " ++ show t
show (IsSort a t) = show a ++ " :sort " ++ show t
data DoGeneralize = YesGeneralize | NoGeneralize
deriving (Eq, Ord, Show, Data)
data GeneralizedValue = GeneralizedValue
{ genvalCheckpoint :: CheckpointId
, genvalTerm :: Term
, genvalType :: Type
} deriving (Show, Data)
data MetaVariable =
MetaVar { mvInfo :: MetaInfo
, mvPriority :: MetaPriority
, mvPermutation :: Permutation
, mvJudgement :: Judgement MetaId
, mvInstantiation :: MetaInstantiation
, mvListeners :: Set Listener
, mvFrozen :: Frozen
}
data Listener = EtaExpand MetaId
| CheckConstraint Nat ProblemConstraint
instance Eq Listener where
EtaExpand x == EtaExpand y = x == y
CheckConstraint x _ == CheckConstraint y _ = x == y
_ == _ = False
instance Ord Listener where
EtaExpand x `compare` EtaExpand y = x `compare` y
CheckConstraint x _ `compare` CheckConstraint y _ = x `compare` y
EtaExpand{} `compare` CheckConstraint{} = LT
CheckConstraint{} `compare` EtaExpand{} = GT
data Frozen
= Frozen
| Instantiable
deriving (Eq, Show)
data MetaInstantiation
= InstV [Arg String] Term
| Open
| OpenInstance
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
data CheckedTarget = CheckedTarget (Maybe ProblemId)
| NotCheckedTarget
data TypeCheckingProblem
= CheckExpr Comparison A.Expr Type
| CheckArgs ExpandHidden Range [NamedArg A.Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term)
| CheckProjAppToKnownPrincipalArg Comparison A.Expr ProjOrigin (NonemptyList QName) A.Args Type Int Term Type
| CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) A.Expr Type
| DoQuoteTerm Comparison Term Type
instance Show MetaInstantiation where
show (InstV tel t) = "InstV " ++ show tel ++ " (" ++ show t ++ ")"
show Open = "Open"
show OpenInstance = "OpenInstance"
show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")"
show (PostponedTypeCheckingProblem{}) = "PostponedTypeCheckingProblem (...)"
newtype MetaPriority = MetaPriority Int
deriving (Eq , Ord , Show)
data RunMetaOccursCheck
= RunMetaOccursCheck
| DontRunMetaOccursCheck
deriving (Eq , Ord , Show)
data MetaInfo = MetaInfo
{ miClosRange :: Closure Range
, miMetaOccursCheck :: RunMetaOccursCheck
, miNameSuggestion :: MetaNameSuggestion
, miGeneralizable :: Arg DoGeneralize
}
type MetaNameSuggestion = String
data NamedMeta = NamedMeta
{ nmSuggestion :: MetaNameSuggestion
, nmid :: MetaId
}
instance Pretty NamedMeta where
pretty (NamedMeta "" x) = pretty x
pretty (NamedMeta "_" x) = pretty x
pretty (NamedMeta s x) = text $ "_" ++ s ++ prettyShow x
type MetaStore = IntMap MetaVariable
instance HasRange MetaInfo where
getRange = clValue . miClosRange
instance HasRange MetaVariable where
getRange m = getRange $ getMetaInfo m
instance SetRange MetaInfo where
setRange r m = m { miClosRange = (miClosRange m) { clValue = r }}
instance SetRange MetaVariable where
setRange r m = m { mvInfo = setRange r (mvInfo m) }
normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0
lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (-10)
highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = miClosRange . mvInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope m = clScope $ getMetaInfo m
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv m = clEnv $ getMetaInfo m
getMetaSig :: MetaVariable -> Signature
getMetaSig m = clSignature $ getMetaInfo m
getMetaRelevance :: MetaVariable -> Relevance
getMetaRelevance = envRelevance . getMetaEnv
getMetaModality :: MetaVariable -> Modality
getMetaModality = envModality . getMetaEnv
metaFrozen :: Lens' Frozen MetaVariable
metaFrozen f mv = f (mvFrozen mv) <&> \ x -> mv { mvFrozen = x }
data InteractionPoint = InteractionPoint
{ ipRange :: Range
, ipMeta :: Maybe MetaId
, ipSolved:: Bool
, ipClause:: IPClause
}
instance Eq InteractionPoint where (==) = (==) `on` ipMeta
type InteractionPoints = Map InteractionId InteractionPoint
data IPClause = IPClause
{ ipcQName :: QName
, ipcClauseNo :: Int
, ipcClause :: A.RHS
}
| IPNoClause
deriving Data
instance Eq IPClause where
IPNoClause == IPNoClause = True
IPClause x i _ == IPClause x' i' _ = x == x' && i == i'
_ == _ = False
data Signature = Sig
{ _sigSections :: Sections
, _sigDefinitions :: Definitions
, _sigRewriteRules:: RewriteRuleMap
}
deriving (Data, Show)
sigSections :: Lens' Sections Signature
sigSections f s =
f (_sigSections s) <&>
\x -> s {_sigSections = x}
sigDefinitions :: Lens' Definitions Signature
sigDefinitions f s =
f (_sigDefinitions s) <&>
\x -> s {_sigDefinitions = x}
sigRewriteRules :: Lens' RewriteRuleMap Signature
sigRewriteRules f s =
f (_sigRewriteRules s) <&>
\x -> s {_sigRewriteRules = x}
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
type RewriteRuleMap = HashMap QName RewriteRules
type DisplayForms = HashMap QName [LocalDisplayForm]
newtype Section = Section { _secTelescope :: Telescope }
deriving (Data, Show)
instance Pretty Section where
pretty = pretty . _secTelescope
secTelescope :: Lens' Telescope Section
secTelescope f s =
f (_secTelescope s) <&>
\x -> s {_secTelescope = x}
emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty HMap.empty
data DisplayForm = Display
{ dfFreeVars :: Nat
, dfPats :: Elims
, dfRHS :: DisplayTerm
}
deriving (Data, Show)
type LocalDisplayForm = Open DisplayForm
data DisplayTerm
= DWithApp DisplayTerm [DisplayTerm] Elims
| DCon ConHead ConInfo [Arg DisplayTerm]
| DDef QName [Elim' DisplayTerm]
| DDot Term
| DTerm Term
deriving (Data, Show)
instance Free DisplayForm where
freeVars' (Display n ps t) = bind (freeVars' ps) `mappend` bind' n (freeVars' t)
instance Free DisplayTerm where
freeVars' (DWithApp t ws es) = freeVars' (t, (ws, es))
freeVars' (DCon _ _ vs) = freeVars' vs
freeVars' (DDef _ es) = freeVars' es
freeVars' (DDot v) = freeVars' v
freeVars' (DTerm v) = freeVars' v
instance Pretty DisplayTerm where
prettyPrec p v =
case v of
DTerm v -> prettyPrec p v
DDot v -> "." P.<> prettyPrec 10 v
DDef f es -> pretty f `pApp` es
DCon c _ vs -> pretty (conName c) `pApp` map Apply vs
DWithApp h ws es ->
mparens (p > 0)
(sep [ pretty h
, nest 2 $ fsep [ "|" <+> pretty w | w <- ws ] ])
`pApp` es
where
pApp d els = mparens (not (null els) && p > 9) $
sep [d, nest 2 $ fsep (map (prettyPrec 10) els)]
defaultDisplayForm :: QName -> [LocalDisplayForm]
defaultDisplayForm c = []
defRelevance :: Definition -> Relevance
defRelevance = getRelevance . defArgInfo
data NLPat
= PVar !Int [Arg Int]
| PWild
| PDef QName PElims
| PLam ArgInfo (Abs NLPat)
| PPi (Dom NLPType) (Abs NLPType)
| PBoundVar {-# UNPACK #-} !Int PElims
| PTerm Term
deriving (Data, Show)
type PElims = [Elim' NLPat]
data NLPType = NLPType
{ nlpTypeLevel :: NLPat
, nlpTypeUnEl :: NLPat
} deriving (Data, Show)
type RewriteRules = [RewriteRule]
data RewriteRule = RewriteRule
{ rewName :: QName
, rewContext :: Telescope
, rewHead :: QName
, rewPats :: PElims
, rewRHS :: Term
, rewType :: Type
}
deriving (Data, Show)
data Definition = Defn
{ defArgInfo :: ArgInfo
, defName :: QName
, defType :: Type
, defPolarity :: [Polarity]
, defArgOccurrences :: [Occurrence]
, defArgGeneralizable :: NumGeneralizableArgs
, defGeneralizedParams :: [Maybe Name]
, defDisplay :: [LocalDisplayForm]
, defMutual :: MutualId
, defCompiledRep :: CompiledRepresentation
, defInstance :: Maybe QName
, defCopy :: Bool
, defMatchable :: Bool
, defNoCompilation :: Bool
, defInjective :: Bool
, theDef :: Defn
}
deriving (Data, Show)
data NumGeneralizableArgs
= NoGeneralizableArgs
| SomeGeneralizableArgs Int
deriving (Data, Show)
theDefLens :: Lens' Defn Definition
theDefLens f d = f (theDef d) <&> \ df -> d { theDef = df }
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn info x t def = Defn
{ defArgInfo = info
, defName = x
, defType = t
, defPolarity = []
, defArgOccurrences = []
, defArgGeneralizable = NoGeneralizableArgs
, defGeneralizedParams = []
, defDisplay = defaultDisplayForm x
, defMutual = 0
, defCompiledRep = noCompiledRep
, defInstance = Nothing
, defCopy = False
, defMatchable = False
, defNoCompilation = False
, defInjective = False
, theDef = def
}
data Polarity
= Covariant
| Contravariant
| Invariant
| Nonvariant
deriving (Data, Show, Eq)
instance Pretty Polarity where
pretty = text . \case
Covariant -> "+"
Contravariant -> "-"
Invariant -> "*"
Nonvariant -> "_"
data IsForced
= Forced
| NotForced
deriving (Data, Show, Eq)
data CompilerPragma = CompilerPragma Range String
deriving (Data, Show, Eq)
instance HasRange CompilerPragma where
getRange (CompilerPragma r _) = r
type BackendName = String
jsBackendName, ghcBackendName :: BackendName
jsBackendName = "JS"
ghcBackendName = "GHC"
type CompiledRepresentation = Map BackendName [CompilerPragma]
noCompiledRep :: CompiledRepresentation
noCompiledRep = Map.empty
type Face = [(Term,Bool)]
data System = System
{ systemTel :: Telescope
, systemClauses :: [(Face,Term)]
} deriving (Data, Show)
data ExtLamInfo = ExtLamInfo
{ extLamModule :: ModuleName
, extLamSys :: !(Maybe System)
} deriving (Data, Show)
modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem f e = let !e' = e { extLamSys = f <$> extLamSys e } in e'
data Projection = Projection
{ projProper :: Maybe QName
, projOrig :: QName
, projFromType :: Arg QName
, projIndex :: Int
, projLams :: ProjLams
} deriving (Data, Show)
newtype ProjLams = ProjLams { getProjLams :: [Arg ArgName] }
deriving (Data, Show, Null)
projDropPars :: Projection -> ProjOrigin -> Term
projDropPars (Projection Just{} d _ _ lams) o =
case initLast $ getProjLams lams of
Nothing -> Def d []
Just (pars, Arg i y) ->
let core = Lam i $ Abs y $ Var 0 [Proj o d] in
List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) core pars
projDropPars (Projection Nothing _ _ _ lams) o | null lams = __IMPOSSIBLE__
projDropPars (Projection Nothing d _ _ lams) o =
List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (Def d []) $ init $ getProjLams lams
projArgInfo :: Projection -> ArgInfo
projArgInfo (Projection _ _ _ _ lams) =
maybe __IMPOSSIBLE__ getArgInfo $ lastMaybe $ getProjLams lams
data EtaEquality
= Specified { theEtaEquality :: !HasEta }
| Inferred { theEtaEquality :: !HasEta }
deriving (Data, Show, Eq)
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
setEtaEquality e@Specified{} _ = e
setEtaEquality _ b = Inferred b
data FunctionFlag
= FunStatic
| FunInline
| FunMacro
deriving (Data, Eq, Ord, Enum, Show)
data CompKit = CompKit
{ nameOfHComp :: Maybe QName
, nameOfTransp :: Maybe QName
}
deriving (Data, Eq, Ord, Show)
emptyCompKit :: CompKit
emptyCompKit = CompKit Nothing Nothing
data Defn = Axiom
| DataOrRecSig
{ datarecPars :: Int }
| GeneralizableVar
| AbstractDefn Defn
| Function
{ funClauses :: [Clause]
, funCompiled :: Maybe CompiledClauses
, funSplitTree :: Maybe SplitTree
, funTreeless :: Maybe Compiled
, funCovering :: [Closure Clause]
, funInv :: FunctionInverse
, funMutual :: Maybe [QName]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe Projection
, funFlags :: Set FunctionFlag
, funTerminates :: Maybe Bool
, funExtLam :: Maybe ExtLamInfo
, funWith :: Maybe QName
, funCopatternLHS :: Bool
}
| Datatype
{ dataPars :: Nat
, dataIxs :: Nat
, dataInduction :: Induction
, dataClause :: (Maybe Clause)
, dataCons :: [QName]
, dataSort :: Sort
, dataMutual :: Maybe [QName]
, dataAbstr :: IsAbstract
, dataPathCons :: [QName]
}
| Record
{ recPars :: Nat
, recClause :: Maybe Clause
, recConHead :: ConHead
, recNamedCon :: Bool
, recFields :: [Arg QName]
, recTel :: Telescope
, recMutual :: Maybe [QName]
, recEtaEquality' :: EtaEquality
, recInduction :: Maybe Induction
, recAbstr :: IsAbstract
, recComp :: CompKit
}
| Constructor
{ conPars :: Int
, conArity :: Int
, conSrcCon :: ConHead
, conData :: QName
, conAbstr :: IsAbstract
, conInd :: Induction
, conComp :: (CompKit, Maybe [QName])
, conForced :: [IsForced]
, conErased :: [Bool]
}
| Primitive
{ primAbstr :: IsAbstract
, primName :: String
, primClauses :: [Clause]
, primInv :: FunctionInverse
, primCompiled :: Maybe CompiledClauses
}
deriving (Data, Show)
instance Pretty Definition where
pretty Defn{..} =
"Defn {" <?> vcat
[ "defArgInfo =" <?> pshow defArgInfo
, "defName =" <?> pretty defName
, "defType =" <?> pretty defType
, "defPolarity =" <?> pshow defPolarity
, "defArgOccurrences =" <?> pshow defArgOccurrences
, "defGeneralizedParams =" <?> pshow defGeneralizedParams
, "defDisplay =" <?> pshow defDisplay
, "defMutual =" <?> pshow defMutual
, "defCompiledRep =" <?> pshow defCompiledRep
, "defInstance =" <?> pshow defInstance
, "defCopy =" <?> pshow defCopy
, "defMatchable =" <?> pshow defMatchable
, "defInjective =" <?> pshow defInjective
, "theDef =" <?> pretty theDef ] <+> "}"
instance Pretty Defn where
pretty Axiom = "Axiom"
pretty (DataOrRecSig n) = "DataOrRecSig" <+> pretty n
pretty GeneralizableVar{} = "GeneralizableVar"
pretty (AbstractDefn def) = "AbstractDefn" <?> parens (pretty def)
pretty Function{..} =
"Function {" <?> vcat
[ "funClauses =" <?> vcat (map pretty funClauses)
, "funCompiled =" <?> pshow funCompiled
, "funSplitTree =" <?> pshow funSplitTree
, "funTreeless =" <?> pshow funTreeless
, "funInv =" <?> pshow funInv
, "funMutual =" <?> pshow funMutual
, "funAbstr =" <?> pshow funAbstr
, "funDelayed =" <?> pshow funDelayed
, "funProjection =" <?> pshow funProjection
, "funFlags =" <?> pshow funFlags
, "funTerminates =" <?> pshow funTerminates
, "funWith =" <?> pshow funWith
, "funCopatternLHS =" <?> pshow funCopatternLHS ] <?> "}"
pretty Datatype{..} =
"Datatype {" <?> vcat
[ "dataPars =" <?> pshow dataPars
, "dataIxs =" <?> pshow dataIxs
, "dataInduction =" <?> pshow dataInduction
, "dataClause =" <?> pretty dataClause
, "dataCons =" <?> pshow dataCons
, "dataSort =" <?> pretty dataSort
, "dataMutual =" <?> pshow dataMutual
, "dataAbstr =" <?> pshow dataAbstr ] <?> "}"
pretty Record{..} =
"Record {" <?> vcat
[ "recPars =" <?> pshow recPars
, "recClause =" <?> pretty recClause
, "recConHead =" <?> pshow recConHead
, "recNamedCon =" <?> pshow recNamedCon
, "recFields =" <?> pshow recFields
, "recTel =" <?> pretty recTel
, "recMutual =" <?> pshow recMutual
, "recEtaEquality' =" <?> pshow recEtaEquality'
, "recInduction =" <?> pshow recInduction
, "recAbstr =" <?> pshow recAbstr ] <?> "}"
pretty Constructor{..} =
"Constructor {" <?> vcat
[ "conPars =" <?> pshow conPars
, "conArity =" <?> pshow conArity
, "conSrcCon =" <?> pshow conSrcCon
, "conData =" <?> pshow conData
, "conAbstr =" <?> pshow conAbstr
, "conInd =" <?> pshow conInd
, "conErased =" <?> pshow conErased ] <?> "}"
pretty Primitive{..} =
"Primitive {" <?> vcat
[ "primAbstr =" <?> pshow primAbstr
, "primName =" <?> pshow primName
, "primClauses =" <?> pshow primClauses
, "primCompiled =" <?> pshow primCompiled ] <?> "}"
recRecursive :: Defn -> Bool
recRecursive (Record { recMutual = Just qs }) = not $ null qs
recRecursive _ = __IMPOSSIBLE__
recEtaEquality :: Defn -> HasEta
recEtaEquality = theEtaEquality . recEtaEquality'
emptyFunction :: Defn
emptyFunction = Function
{ funClauses = []
, funCompiled = Nothing
, funSplitTree = Nothing
, funTreeless = Nothing
, funInv = NotInjective
, funMutual = Nothing
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Nothing
, funFlags = Set.empty
, funTerminates = Nothing
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = False
, funCovering = []
}
funFlag :: FunctionFlag -> Lens' Bool Defn
funFlag flag f def@Function{ funFlags = flags } =
f (Set.member flag flags) <&>
\ b -> def{ funFlags = (if b then Set.insert else Set.delete) flag flags }
funFlag _ f def = f False <&> const def
funStatic, funInline, funMacro :: Lens' Bool Defn
funStatic = funFlag FunStatic
funInline = funFlag FunInline
funMacro = funFlag FunMacro
isMacro :: Defn -> Bool
isMacro = (^. funMacro)
isEmptyFunction :: Defn -> Bool
isEmptyFunction def =
case def of
Function { funClauses = [] } -> True
_ -> False
isCopatternLHS :: [Clause] -> Bool
isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats)
recCon :: Defn -> QName
recCon Record{ recConHead } = conName recConHead
recCon _ = __IMPOSSIBLE__
defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _ = False
defIsDataOrRecord :: Defn -> Bool
defIsDataOrRecord Record{} = True
defIsDataOrRecord Datatype{} = True
defIsDataOrRecord _ = False
defConstructors :: Defn -> [QName]
defConstructors Datatype{dataCons = cs} = cs
defConstructors Record{recConHead = c} = [conName c]
defConstructors _ = __IMPOSSIBLE__
newtype Fields = Fields [(C.Name, Type)]
deriving Null
data Simplification = YesSimplification | NoSimplification
deriving (Data, Eq, Show)
instance Null Simplification where
empty = NoSimplification
null = (== NoSimplification)
instance Semigroup Simplification where
YesSimplification <> _ = YesSimplification
NoSimplification <> s = s
instance Monoid Simplification where
mempty = NoSimplification
mappend = (<>)
data Reduced no yes = NoReduction no | YesReduction Simplification yes
deriving Functor
data IsReduced
= NotReduced
| Reduced (Blocked ())
data MaybeReduced a = MaybeRed
{ isReduced :: IsReduced
, ignoreReduced :: a
}
deriving (Functor)
instance IsProjElim e => IsProjElim (MaybeReduced e) where
isProjElim = isProjElim . ignoreReduced
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
type MaybeReducedElims = [MaybeReduced Elim]
notReduced :: a -> MaybeReduced a
notReduced x = MaybeRed NotReduced x
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced b = case b of
NotBlocked _ (Arg _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
_ -> MaybeRed (Reduced $ () <$ b) v
where
v = ignoreBlocking b
data AllowedReduction
= ProjectionReductions
| InlineReductions
| CopatternReductions
| FunctionReductions
| RecursiveReductions
| LevelReductions
| UnconfirmedReductions
| NonTerminatingReductions
deriving (Show, Eq, Ord, Enum, Bounded, Data)
type AllowedReductions = [AllowedReduction]
allReductions :: AllowedReductions
allReductions = [minBound..pred maxBound]
data PrimFun = PrimFun
{ primFunName :: QName
, primFunArity :: Arity
, primFunImplementation :: [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
}
primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
primFun q ar imp = PrimFun q ar (\ args _ -> imp args)
defClauses :: Definition -> [Clause]
defClauses Defn{theDef = Function{funClauses = cs}} = cs
defClauses Defn{theDef = Primitive{primClauses = cs}} = cs
defClauses Defn{theDef = Datatype{dataClause = Just c}} = [c]
defClauses Defn{theDef = Record{recClause = Just c}} = [c]
defClauses _ = []
defCompiled :: Definition -> Maybe CompiledClauses
defCompiled Defn{theDef = Function {funCompiled = mcc}} = mcc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing
defParameters :: Definition -> Maybe Nat
defParameters Defn{theDef = Datatype{dataPars = n}} = Just n
defParameters Defn{theDef = Record {recPars = n}} = Just n
defParameters _ = Nothing
defInverse :: Definition -> FunctionInverse
defInverse Defn{theDef = Function { funInv = inv }} = inv
defInverse Defn{theDef = Primitive{ primInv = inv }} = inv
defInverse _ = NotInjective
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
defCompilerPragmas b = reverse . fromMaybe [] . Map.lookup b . defCompiledRep
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _ = NotDelayed
defNonterminating :: Definition -> Bool
defNonterminating Defn{theDef = Function{funTerminates = Just False}} = True
defNonterminating _ = False
defTerminationUnconfirmed :: Definition -> Bool
defTerminationUnconfirmed Defn{theDef = Function{funTerminates = Just True}} = False
defTerminationUnconfirmed Defn{theDef = Function{funTerminates = _ }} = True
defTerminationUnconfirmed _ = False
defAbstract :: Definition -> IsAbstract
defAbstract d = case theDef d of
Axiom{} -> ConcreteDef
DataOrRecSig{} -> ConcreteDef
GeneralizableVar{} -> ConcreteDef
AbstractDefn{} -> AbstractDef
Function{funAbstr = a} -> a
Datatype{dataAbstr = a} -> a
Record{recAbstr = a} -> a
Constructor{conAbstr = a} -> a
Primitive{primAbstr = a} -> a
defForced :: Definition -> [IsForced]
defForced d = case theDef d of
Constructor{conForced = fs} -> fs
Axiom{} -> []
DataOrRecSig{} -> []
GeneralizableVar{} -> []
AbstractDefn{} -> []
Function{} -> []
Datatype{} -> []
Record{} -> []
Primitive{} -> []
type FunctionInverse = FunctionInverse' Clause
type InversionMap c = Map TermHead [c]
data FunctionInverse' c
= NotInjective
| Inverse (InversionMap c)
deriving (Data, Show, Functor)
data TermHead = SortHead
| PiHead
| ConsHead QName
| VarHead Nat
| UnknownHead
deriving (Data, Eq, Ord, Show)
instance Pretty TermHead where
pretty = \ case
SortHead -> "SortHead"
PiHead -> "PiHead"
ConsHead q -> "ConsHead" <+> pretty q
VarHead i -> text ("VarHead " ++ show i)
UnknownHead -> "UnknownHead"
newtype MutualId = MutId Int32
deriving (Data, Eq, Ord, Show, Num, Enum)
type Statistics = Map String Integer
data Call = CheckClause Type A.SpineClause
| CheckPattern A.Pattern Telescope Type
| CheckLetBinding A.LetBinding
| InferExpr A.Expr
| CheckExprCall Comparison A.Expr Type
| CheckDotPattern A.Expr Term
| CheckPatternShadowing A.SpineClause
| CheckProjection Range QName Type
| IsTypeCall A.Expr Sort
| IsType_ A.Expr
| InferVar Name
| InferDef QName
| CheckArguments Range [NamedArg A.Expr] Type (Maybe Type)
| CheckTargetType Range Type Type
| CheckDataDef Range QName [A.LamBinding] [A.Constructor]
| CheckRecDef Range QName [A.LamBinding] [A.Constructor]
| CheckConstructor QName Telescope Sort A.Constructor
| CheckConstructorFitsIn QName Type Sort
| CheckFunDefCall Range QName [A.Clause]
| CheckPragma Range A.Pragma
| CheckPrimitive Range QName A.Expr
| CheckIsEmpty Range Type
| CheckWithFunctionType Type
| CheckSectionApplication Range ModuleName A.ModuleApplication
| CheckNamedWhere ModuleName
| ScopeCheckExpr C.Expr
| ScopeCheckDeclaration NiceDeclaration
| ScopeCheckLHS C.QName C.Pattern
| NoHighlighting
| ModuleContents
| SetRange Range
deriving Data
instance Pretty Call where
pretty CheckClause{} = "CheckClause"
pretty CheckPattern{} = "CheckPattern"
pretty InferExpr{} = "InferExpr"
pretty CheckExprCall{} = "CheckExprCall"
pretty CheckLetBinding{} = "CheckLetBinding"
pretty CheckProjection{} = "CheckProjection"
pretty IsTypeCall{} = "IsTypeCall"
pretty IsType_{} = "IsType_"
pretty InferVar{} = "InferVar"
pretty InferDef{} = "InferDef"
pretty CheckArguments{} = "CheckArguments"
pretty CheckTargetType{} = "CheckTargetType"
pretty CheckDataDef{} = "CheckDataDef"
pretty CheckRecDef{} = "CheckRecDef"
pretty CheckConstructor{} = "CheckConstructor"
pretty CheckConstructorFitsIn{} = "CheckConstructorFitsIn"
pretty CheckFunDefCall{} = "CheckFunDefCall"
pretty CheckPragma{} = "CheckPragma"
pretty CheckPrimitive{} = "CheckPrimitive"
pretty CheckWithFunctionType{} = "CheckWithFunctionType"
pretty CheckNamedWhere{} = "CheckNamedWhere"
pretty ScopeCheckExpr{} = "ScopeCheckExpr"
pretty ScopeCheckDeclaration{} = "ScopeCheckDeclaration"
pretty ScopeCheckLHS{} = "ScopeCheckLHS"
pretty CheckDotPattern{} = "CheckDotPattern"
pretty CheckPatternShadowing{} = "CheckPatternShadowing"
pretty SetRange{} = "SetRange"
pretty CheckSectionApplication{} = "CheckSectionApplication"
pretty CheckIsEmpty{} = "CheckIsEmpty"
pretty NoHighlighting{} = "NoHighlighting"
pretty ModuleContents{} = "ModuleContents"
instance HasRange Call where
getRange (CheckClause _ c) = getRange c
getRange (CheckPattern p _ _) = getRange p
getRange (InferExpr e) = getRange e
getRange (CheckExprCall _ e _) = getRange e
getRange (CheckLetBinding b) = getRange b
getRange (CheckProjection r _ _) = r
getRange (IsTypeCall e s) = getRange e
getRange (IsType_ e) = getRange e
getRange (InferVar x) = getRange x
getRange (InferDef f) = getRange f
getRange (CheckArguments r _ _ _) = r
getRange (CheckTargetType r _ _) = r
getRange (CheckDataDef i _ _ _) = getRange i
getRange (CheckRecDef i _ _ _) = getRange i
getRange (CheckConstructor _ _ _ c) = getRange c
getRange (CheckConstructorFitsIn c _ _) = getRange c
getRange (CheckFunDefCall i _ _) = getRange i
getRange (CheckPragma r _) = r
getRange (CheckPrimitive i _ _) = getRange i
getRange CheckWithFunctionType{} = noRange
getRange (CheckNamedWhere m) = getRange m
getRange (ScopeCheckExpr e) = getRange e
getRange (ScopeCheckDeclaration d) = getRange d
getRange (ScopeCheckLHS _ p) = getRange p
getRange (CheckDotPattern e _) = getRange e
getRange (CheckPatternShadowing c) = getRange c
getRange (SetRange r) = r
getRange (CheckSectionApplication r _ _) = r
getRange (CheckIsEmpty r _) = r
getRange NoHighlighting = noRange
getRange ModuleContents = noRange
type InstanceTable = Map QName (Set QName)
type TempInstanceTable = (InstanceTable , Set QName)
data BuiltinDescriptor
= BuiltinData (TCM Type) [String]
| BuiltinDataCons (TCM Type)
| BuiltinPrim String (Term -> TCM ())
| BuiltinPostulate Relevance (TCM Type)
| BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
data BuiltinInfo =
BuiltinInfo { builtinName :: String
, builtinDesc :: BuiltinDescriptor }
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
= Builtin Term
| Prim pf
deriving (Show, Functor, Foldable, Traversable)
data HighlightingLevel
= None
| NonInteractive
| Interactive
deriving (Eq, Ord, Show, Read, Data)
data HighlightingMethod
= Direct
| Indirect
deriving (Eq, Show, Read, Data)
ifTopLevelAndHighlightingLevelIsOr ::
MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIsOr l b m = do
e <- askTC
when (envModuleNestingLevel e == 0 &&
(envHighlightingLevel e >= l || b))
m
ifTopLevelAndHighlightingLevelIs ::
MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l =
ifTopLevelAndHighlightingLevelIsOr l False
data TCEnv =
TCEnv { envContext :: Context
, envLetBindings :: LetBindings
, envCurrentModule :: ModuleName
, envCurrentPath :: Maybe AbsolutePath
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envTerminationCheck :: TerminationCheck ()
, envSolvingConstraints :: Bool
, envCheckingWhere :: Bool
, envWorkingOnTypes :: Bool
, envAssignMetas :: Bool
, envActiveProblems :: Set ProblemId
, envAbstractMode :: AbstractMode
, envModality :: Modality
, envDisplayFormsEnabled :: Bool
, envRange :: Range
, envHighlightingRange :: Range
, envClause :: IPClause
, envCall :: Maybe (Closure Call)
, envHighlightingLevel :: HighlightingLevel
, envHighlightingMethod :: HighlightingMethod
, envModuleNestingLevel :: !Int
, envExpandLast :: ExpandHidden
, envAppDef :: Maybe QName
, envSimplification :: Simplification
, envAllowedReductions :: AllowedReductions
, envInjectivityDepth :: Int
, envCompareBlocked :: Bool
, envPrintDomainFreePi :: Bool
, envPrintMetasBare :: Bool
, envInsideDotPattern :: Bool
, envUnquoteFlags :: UnquoteFlags
, envInstanceDepth :: !Int
, envIsDebugPrinting :: Bool
, envPrintingPatternLambdas :: [QName]
, envCallByNeed :: Bool
, envCurrentCheckpoint :: CheckpointId
, envCheckpoints :: Map CheckpointId Substitution
, envGeneralizeMetas :: DoGeneralize
, envGeneralizedVars :: Map QName GeneralizedValue
, envCheckOptionConsistency :: Bool
}
deriving Data
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envCurrentPath = Nothing
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envTerminationCheck = TerminationCheck
, envSolvingConstraints = False
, envCheckingWhere = False
, envActiveProblems = Set.empty
, envWorkingOnTypes = False
, envAssignMetas = True
, envAbstractMode = ConcreteMode
, envModality = Modality Relevant Quantity1
, envDisplayFormsEnabled = True
, envRange = noRange
, envHighlightingRange = noRange
, envClause = IPNoClause
, envCall = Nothing
, envHighlightingLevel = None
, envHighlightingMethod = Indirect
, envModuleNestingLevel = -1
, envExpandLast = ExpandLast
, envAppDef = Nothing
, envSimplification = NoSimplification
, envAllowedReductions = allReductions
, envInjectivityDepth = 0
, envCompareBlocked = False
, envPrintDomainFreePi = False
, envPrintMetasBare = False
, envInsideDotPattern = False
, envUnquoteFlags = defaultUnquoteFlags
, envInstanceDepth = 0
, envIsDebugPrinting = False
, envPrintingPatternLambdas = []
, envCallByNeed = True
, envCurrentCheckpoint = 0
, envCheckpoints = Map.singleton 0 IdS
, envGeneralizeMetas = NoGeneralize
, envGeneralizedVars = Map.empty
, envCheckOptionConsistency = True
}
envRelevance :: TCEnv -> Relevance
envRelevance = modRelevance . envModality
data UnquoteFlags = UnquoteFlags
{ _unquoteNormalise :: Bool }
deriving Data
defaultUnquoteFlags :: UnquoteFlags
defaultUnquoteFlags = UnquoteFlags
{ _unquoteNormalise = False }
unquoteNormalise :: Lens' Bool UnquoteFlags
unquoteNormalise f e = f (_unquoteNormalise e) <&> \ x -> e { _unquoteNormalise = x }
eUnquoteNormalise :: Lens' Bool TCEnv
eUnquoteNormalise = eUnquoteFlags . unquoteNormalise
eContext :: Lens' Context TCEnv
eContext f e = f (envContext e) <&> \ x -> e { envContext = x }
eLetBindings :: Lens' LetBindings TCEnv
eLetBindings f e = f (envLetBindings e) <&> \ x -> e { envLetBindings = x }
eCurrentModule :: Lens' ModuleName TCEnv
eCurrentModule f e = f (envCurrentModule e) <&> \ x -> e { envCurrentModule = x }
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
eCurrentPath f e = f (envCurrentPath e) <&> \ x -> e { envCurrentPath = x }
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
eAnonymousModules f e = f (envAnonymousModules e) <&> \ x -> e { envAnonymousModules = x }
eImportPath :: Lens' [C.TopLevelModuleName] TCEnv
eImportPath f e = f (envImportPath e) <&> \ x -> e { envImportPath = x }
eMutualBlock :: Lens' (Maybe MutualId) TCEnv
eMutualBlock f e = f (envMutualBlock e) <&> \ x -> e { envMutualBlock = x }
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
eTerminationCheck f e = f (envTerminationCheck e) <&> \ x -> e { envTerminationCheck = x }
eSolvingConstraints :: Lens' Bool TCEnv
eSolvingConstraints f e = f (envSolvingConstraints e) <&> \ x -> e { envSolvingConstraints = x }
eCheckingWhere :: Lens' Bool TCEnv
eCheckingWhere f e = f (envCheckingWhere e) <&> \ x -> e { envCheckingWhere = x }
eWorkingOnTypes :: Lens' Bool TCEnv
eWorkingOnTypes f e = f (envWorkingOnTypes e) <&> \ x -> e { envWorkingOnTypes = x }
eAssignMetas :: Lens' Bool TCEnv
eAssignMetas f e = f (envAssignMetas e) <&> \ x -> e { envAssignMetas = x }
eActiveProblems :: Lens' (Set ProblemId) TCEnv
eActiveProblems f e = f (envActiveProblems e) <&> \ x -> e { envActiveProblems = x }
eAbstractMode :: Lens' AbstractMode TCEnv
eAbstractMode f e = f (envAbstractMode e) <&> \ x -> e { envAbstractMode = x }
eModality :: Lens' Modality TCEnv
eModality f e = f (envModality e) <&> \ x -> e { envModality = x }
eRelevance :: Lens' Relevance TCEnv
eRelevance = eModality . lModRelevance
eQuantity :: Lens' Quantity TCEnv
eQuantity = eModality . lModQuantity
eDisplayFormsEnabled :: Lens' Bool TCEnv
eDisplayFormsEnabled f e = f (envDisplayFormsEnabled e) <&> \ x -> e { envDisplayFormsEnabled = x }
eRange :: Lens' Range TCEnv
eRange f e = f (envRange e) <&> \ x -> e { envRange = x }
eHighlightingRange :: Lens' Range TCEnv
eHighlightingRange f e = f (envHighlightingRange e) <&> \ x -> e { envHighlightingRange = x }
eCall :: Lens' (Maybe (Closure Call)) TCEnv
eCall f e = f (envCall e) <&> \ x -> e { envCall = x }
eHighlightingLevel :: Lens' HighlightingLevel TCEnv
eHighlightingLevel f e = f (envHighlightingLevel e) <&> \ x -> e { envHighlightingLevel = x }
eHighlightingMethod :: Lens' HighlightingMethod TCEnv
eHighlightingMethod f e = f (envHighlightingMethod e) <&> \ x -> e { envHighlightingMethod = x }
eModuleNestingLevel :: Lens' Int TCEnv
eModuleNestingLevel f e = f (envModuleNestingLevel e) <&> \ x -> e { envModuleNestingLevel = x }
eExpandLast :: Lens' ExpandHidden TCEnv
eExpandLast f e = f (envExpandLast e) <&> \ x -> e { envExpandLast = x }
eAppDef :: Lens' (Maybe QName) TCEnv
eAppDef f e = f (envAppDef e) <&> \ x -> e { envAppDef = x }
eSimplification :: Lens' Simplification TCEnv
eSimplification f e = f (envSimplification e) <&> \ x -> e { envSimplification = x }
eAllowedReductions :: Lens' AllowedReductions TCEnv
eAllowedReductions f e = f (envAllowedReductions e) <&> \ x -> e { envAllowedReductions = x }
eInjectivityDepth :: Lens' Int TCEnv
eInjectivityDepth f e = f (envInjectivityDepth e) <&> \ x -> e { envInjectivityDepth = x }
eCompareBlocked :: Lens' Bool TCEnv
eCompareBlocked f e = f (envCompareBlocked e) <&> \ x -> e { envCompareBlocked = x }
ePrintDomainFreePi :: Lens' Bool TCEnv
ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x }
eInsideDotPattern :: Lens' Bool TCEnv
eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x }
eUnquoteFlags :: Lens' UnquoteFlags TCEnv
eUnquoteFlags f e = f (envUnquoteFlags e) <&> \ x -> e { envUnquoteFlags = x }
eInstanceDepth :: Lens' Int TCEnv
eInstanceDepth f e = f (envInstanceDepth e) <&> \ x -> e { envInstanceDepth = x }
eIsDebugPrinting :: Lens' Bool TCEnv
eIsDebugPrinting f e = f (envIsDebugPrinting e) <&> \ x -> e { envIsDebugPrinting = x }
ePrintingPatternLambdas :: Lens' [QName] TCEnv
ePrintingPatternLambdas f e = f (envPrintingPatternLambdas e) <&> \ x -> e { envPrintingPatternLambdas = x }
eCallByNeed :: Lens' Bool TCEnv
eCallByNeed f e = f (envCallByNeed e) <&> \ x -> e { envCallByNeed = x }
eCurrentCheckpoint :: Lens' CheckpointId TCEnv
eCurrentCheckpoint f e = f (envCurrentCheckpoint e) <&> \ x -> e { envCurrentCheckpoint = x }
eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv
eCheckpoints f e = f (envCheckpoints e) <&> \ x -> e { envCheckpoints = x }
eGeneralizeMetas :: Lens' DoGeneralize TCEnv
eGeneralizeMetas f e = f (envGeneralizeMetas e) <&> \ x -> e { envGeneralizeMetas = x }
eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv
eGeneralizedVars f e = f (envGeneralizedVars e) <&> \ x -> e { envGeneralizedVars = x }
type Context = [ContextEntry]
type ContextEntry = Dom (Name, Type)
type LetBindings = Map Name (Open (Term, Dom Type))
data AbstractMode
= AbstractMode
| ConcreteMode
| IgnoreAbstractMode
deriving (Data, Show, Eq)
aDefToMode :: IsAbstract -> AbstractMode
aDefToMode AbstractDef = AbstractMode
aDefToMode ConcreteDef = ConcreteMode
aModeToDef :: AbstractMode -> IsAbstract
aModeToDef AbstractMode = AbstractDef
aModeToDef ConcreteMode = ConcreteDef
aModeToDef _ = __IMPOSSIBLE__
data ExpandHidden
= ExpandLast
| DontExpandLast
deriving (Eq, Data)
data Candidate = Candidate { candidateTerm :: Term
, candidateType :: Type
, candidateOverlappable :: Bool
}
deriving (Show, Data)
instance Free Candidate where
freeVars' (Candidate t u _) = freeVars' (t, u)
data Warning
= NicifierIssue DeclarationWarning
| TerminationIssue [TerminationError]
| UnreachableClauses QName [[NamedArg DeBruijnPattern]]
| CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
| CoverageNoExactSplit QName [Clause]
| NotStrictlyPositive QName (Seq OccursWhere)
| UnsolvedMetaVariables [Range]
| UnsolvedInteractionMetas [Range]
| UnsolvedConstraints Constraints
| CantGeneralizeOverSorts [MetaId]
| AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
| OldBuiltin String String
| EmptyRewritePragma
| IllformedAsClause String
| UselessPublic
| UselessInline QName
| WrongInstanceDeclaration
| InstanceWithExplicitArg QName
| InstanceNoOutputTypeName Doc
| InstanceArgWithExplicitArg Doc
| InversionDepthReached QName
| GenericWarning Doc
| GenericNonFatalError Doc
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagNonTerminating
| SafeFlagTerminating
| SafeFlagWithoutKFlagPrimEraseEquality
| WithoutKFlagPrimEraseEquality
| SafeFlagNoPositivityCheck
| SafeFlagPolarity
| SafeFlagNoUniverseCheck
| ParseWarning ParseWarning
| LibraryWarning LibWarning
| DeprecationWarning String String String
| UserWarning String
| ModuleDoesntExport C.QName [C.ImportedName]
| InfectiveImport String ModuleName
| CoInfectiveImport String ModuleName
deriving (Show , Data)
warningName :: Warning -> WarningName
warningName w = case w of
NicifierIssue dw -> declarationWarningName dw
ParseWarning pw -> parseWarningName pw
LibraryWarning lw -> libraryWarningName lw
CantGeneralizeOverSorts{} -> CantGeneralizeOverSorts_
AbsurdPatternRequiresNoRHS{} -> AbsurdPatternRequiresNoRHS_
CoverageIssue{} -> CoverageIssue_
CoverageNoExactSplit{} -> CoverageNoExactSplit_
DeprecationWarning{} -> DeprecationWarning_
EmptyRewritePragma -> EmptyRewritePragma_
IllformedAsClause{} -> IllformedAsClause_
WrongInstanceDeclaration{} -> WrongInstanceDeclaration_
InstanceWithExplicitArg{} -> InstanceWithExplicitArg_
InstanceNoOutputTypeName{} -> InstanceNoOutputTypeName_
InstanceArgWithExplicitArg{} -> InstanceArgWithExplicitArg_
GenericNonFatalError{} -> GenericNonFatalError_
GenericWarning{} -> GenericWarning_
InversionDepthReached{} -> InversionDepthReached_
ModuleDoesntExport{} -> ModuleDoesntExport_
NotStrictlyPositive{} -> NotStrictlyPositive_
OldBuiltin{} -> OldBuiltin_
SafeFlagNoPositivityCheck -> SafeFlagNoPositivityCheck_
SafeFlagNonTerminating -> SafeFlagNonTerminating_
SafeFlagNoUniverseCheck -> SafeFlagNoUniverseCheck_
SafeFlagPolarity -> SafeFlagPolarity_
SafeFlagPostulate{} -> SafeFlagPostulate_
SafeFlagPragma{} -> SafeFlagPragma_
SafeFlagWithoutKFlagPrimEraseEquality -> SafeFlagWithoutKFlagPrimEraseEquality_
WithoutKFlagPrimEraseEquality -> WithoutKFlagPrimEraseEquality_
SafeFlagTerminating -> SafeFlagTerminating_
TerminationIssue{} -> TerminationIssue_
UnreachableClauses{} -> UnreachableClauses_
UnsolvedInteractionMetas{} -> UnsolvedInteractionMetas_
UnsolvedConstraints{} -> UnsolvedConstraints_
UnsolvedMetaVariables{} -> UnsolvedMetaVariables_
UselessInline{} -> UselessInline_
UselessPublic -> UselessPublic_
UserWarning{} -> UserWarning_
InfectiveImport{} -> InfectiveImport_
CoInfectiveImport{} -> CoInfectiveImport_
data TCWarning
= TCWarning
{ tcWarningRange :: Range
, tcWarning :: Warning
, tcWarningPrintedWarning :: Doc
, tcWarningCached :: Bool
}
deriving Show
tcWarningOrigin :: TCWarning -> SrcFile
tcWarningOrigin = rangeFile . tcWarningRange
instance HasRange TCWarning where
getRange = tcWarningRange
instance Eq TCWarning where
x == y = equalHeadConstructors (tcWarning x) (tcWarning y)
&& getRange x == getRange y
equalHeadConstructors :: Warning -> Warning -> Bool
equalHeadConstructors = (==) `on` toConstr
getPartialDefs :: ReadTCState tcm => tcm [QName]
getPartialDefs = do
tcst <- getTCState
return $ mapMaybe (extractQName . tcWarning)
$ tcst ^. stTCWarnings where
extractQName :: Warning -> Maybe QName
extractQName (CoverageIssue f _) = Just f
extractQName _ = Nothing
data CallInfo = CallInfo
{ callInfoTarget :: QName
, callInfoRange :: Range
, callInfoCall :: Closure Term
} deriving (Data, Show)
instance Pretty CallInfo where pretty = pretty . callInfoTarget
instance AllNames CallInfo where allNames = singleton . callInfoTarget
data TerminationError = TerminationError
{ termErrFunctions :: [QName]
, termErrCalls :: [CallInfo]
} deriving (Data, Show)
data SplitError
= NotADatatype (Closure Type)
| IrrelevantDatatype (Closure Type)
| ErasedDatatype (Closure Type)
| CoinductiveDatatype (Closure Type)
| UnificationStuck
{ cantSplitConName :: QName
, cantSplitTel :: Telescope
, cantSplitConIdx :: Args
, cantSplitGivenIdx :: Args
, cantSplitFailures :: [UnificationFailure]
}
| CosplitCatchall
| CosplitNoTarget
| CosplitNoRecordType (Closure Type)
| CannotCreateMissingClause QName (Telescope,[NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
| GenericSplitError String
deriving (Show)
data NegativeUnification
= UnifyConflict Telescope Term Term
| UnifyCycle Telescope Int Term
deriving (Show)
data UnificationFailure
= UnifyIndicesNotVars Telescope Type Term Term Args
| UnifyRecursiveEq Telescope Type Int Term
| UnifyReflexiveEq Telescope Type Term
deriving (Show)
data UnquoteError
= BadVisibility String (Arg I.Term)
| ConInsteadOfDef QName String String
| DefInsteadOfCon QName String String
| NonCanonical String I.Term
| BlockedOnMeta TCState MetaId
| UnquotePanic String
deriving (Show)
data TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
| DoesNotConstructAnElementOf QName Type
| WrongHidingInLHS
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| WrongNamedArgument (NamedArg A.Expr)
| WrongIrrelevanceInLambda
| WrongQuantityInLambda
| HidingMismatch Hiding Hiding
| RelevanceMismatch Relevance Relevance
| UninstantiatedDotPattern A.Expr
| ForcedConstructorNotInstantiated A.Pattern
| IlltypedPattern A.Pattern Type
| IllformedProjectionPattern A.Pattern
| CannotEliminateWithPattern (NamedArg A.Pattern) Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [DeBruijnPattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBePath Type
| ShouldBeRecordType Type
| ShouldBeRecordPattern DeBruijnPattern
| NotAProjectionPattern (NamedArg A.Pattern)
| NotAProperTerm
| InvalidTypeSort Sort
| InvalidType Term
| FunctionTypeInSizeUniv Term
| SplitOnIrrelevant (Dom Type)
| SplitOnNonVariable Term Type
| DefinitionIsIrrelevant QName
| VariableIsIrrelevant Name
| VariableIsErased Name
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalRelevance Comparison Term Term
| UnequalHiding Term Term
| UnequalSorts Sort Sort
| UnequalBecauseOfUniverseConflict Comparison Term Term
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| MetaOccursInItself MetaId
| MetaIrrelevantSolution MetaId Term
| GenericError String
| GenericDocError Doc
| BuiltinMustBeConstructor String A.Expr
| NoSuchBuiltinName String
| DuplicateBuiltinBinding String Term Term
| NoBindingForBuiltin String
| NoSuchPrimitiveFunction String
| DuplicatePrimitiveBinding String QName QName
| ShadowedModule C.Name [A.ModuleName]
| BuiltinInParameterisedModule String
| IllegalLetInTelescope C.TypedBinding
| NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
| TooManyFields QName [C.Name] [C.Name]
| DuplicateFields [C.Name]
| DuplicateConstructors [C.Name]
| WithOnFreeVariable A.Expr Term
| UnexpectedWithPatterns [A.Pattern]
| WithClausePatternMismatch A.Pattern (NamedArg DeBruijnPattern)
| FieldOutsideRecord
| ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
| GeneralizeCyclicDependency
| GeneralizeUnsolvedMeta
| SplitError SplitError
| ImpossibleConstructor QName NegativeUnification
| TooManyPolarities QName Int
| LocalVsImportedModuleClash ModuleName
| SolvedButOpenHoles
| CyclicModuleDependency [C.TopLevelModuleName]
| FileNotFound C.TopLevelModuleName [AbsolutePath]
| OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
| AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
| ModuleNameUnexpected C.TopLevelModuleName C.TopLevelModuleName
| ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath]
| ClashingFileNamesFor ModuleName [AbsolutePath]
| ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath
| BothWithAndRHS
| AbstractConstructorNotInScope A.QName
| NotInScope [C.QName]
| NoSuchModule C.QName
| AmbiguousName C.QName (NonemptyList A.QName)
| AmbiguousModule C.QName (NonemptyList A.ModuleName)
| ClashingDefinition C.QName A.QName
| ClashingModule A.ModuleName A.ModuleName
| ClashingImport C.Name A.QName
| ClashingModuleImport C.Name A.ModuleName
| PatternShadowsConstructor C.Name A.QName
| DuplicateImports C.QName [C.ImportedName]
| InvalidPattern C.Pattern
| RepeatedVariablesInPattern [C.Name]
| GeneralizeNotSupportedHere A.QName
| MultipleFixityDecls [(C.Name, [Fixity'])]
| MultiplePolarityPragmas [C.Name]
| NotAModuleExpr C.Expr
| NotAnExpression C.Expr
| NotAValidLetBinding NiceDeclaration
| NotValidBeforeField NiceDeclaration
| NothingAppliedToHiddenArg C.Expr
| NothingAppliedToInstanceArg C.Expr
| BadArgumentsToPatternSynonym A.AmbiguousQName
| TooFewArgumentsToPatternSynonym A.AmbiguousQName
| CannotResolveAmbiguousPatternSynonym (NonemptyList (A.QName, A.PatternSynDefn))
| UnusedVariableInPatternSynonym
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS LHSOrPatSyn C.Pattern
| AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
| OperatorInformation [NotationSection] TypeError
| InstanceNoCandidate Type [(Term, TCErr)]
| UnquoteFailed UnquoteError
| DeBruijnIndexOutOfScope Nat Telescope [Name]
| NeedOptionCopatterns
| NeedOptionRewriting
| NeedOptionProp
| NonFatalErrors [TCWarning]
| InstanceSearchDepthExhausted Term Type Int
| TriedToCopyConstrainedPrim QName
deriving Show
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, Show)
data TCErr
= TypeError
{ tcErrState :: TCState
, tcErrClosErr :: Closure TypeError
}
| Exception Range Doc
| IOException TCState Range E.IOException
| PatternErr
instance Error TCErr where
strMsg = Exception noRange . text . strMsg
instance Show TCErr where
show (TypeError _ e) = show (envRange $ clEnv e) ++ ": " ++ show (clValue e)
show (Exception r d) = show r ++ ": " ++ render d
show (IOException _ r e) = show r ++ ": " ++ show e
show PatternErr{} = "Pattern violation (you shouldn't see this)"
instance HasRange TCErr where
getRange (TypeError _ cl) = envRange $ clEnv cl
getRange (Exception r _) = r
getRange (IOException s r _) = r
getRange PatternErr{} = noRange
instance E.Exception TCErr
class (Functor m, Applicative m, Monad m) => HasOptions m where
pragmaOptions :: m PragmaOptions
commandLineOptions :: m CommandLineOptions
instance MonadIO m => HasOptions (TCMT m) where
pragmaOptions = useTC stPragmaOptions
commandLineOptions = do
p <- useTC stPragmaOptions
cl <- stPersistentOptions . stPersistentState <$> getTC
return $ cl { optPragmaOptions = p }
instance HasOptions m => HasOptions (ExceptT e m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
instance HasOptions m => HasOptions (ListT m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
instance HasOptions m => HasOptions (MaybeT m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
instance HasOptions m => HasOptions (ReaderT r m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
instance HasOptions m => HasOptions (StateT s m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
instance (HasOptions m, Monoid w) => HasOptions (WriterT w m) where
pragmaOptions = lift pragmaOptions
commandLineOptions = lift commandLineOptions
sizedTypesOption :: HasOptions m => m Bool
sizedTypesOption = collapseDefault . optSizedTypes <$> pragmaOptions
guardednessOption :: HasOptions m => m Bool
guardednessOption = collapseDefault . optGuardedness <$> pragmaOptions
withoutKOption :: HasOptions m => m Bool
withoutKOption = collapseDefault . optWithoutK <$> pragmaOptions
data ReduceEnv = ReduceEnv
{ redEnv :: TCEnv
, redSt :: TCState
}
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedEnv f s = s { redEnv = f (redEnv s) }
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedSt f s = s { redSt = f (redSt s) }
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv
-> ReduceEnv
mapRedEnvSt f g (ReduceEnv e s) = ReduceEnv (f e) (g s)
reduceEnv :: Lens' TCEnv ReduceEnv
reduceEnv f s = f (redEnv s) <&> \ e -> s { redEnv = e }
reduceSt :: Lens' TCState ReduceEnv
reduceSt f s = f (redSt s) <&> \ e -> s { redSt = e }
newtype ReduceM a = ReduceM { unReduceM :: ReduceEnv -> a }
onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
onReduceEnv f (ReduceM m) = ReduceM (m . f)
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
fmapReduce f (ReduceM m) = ReduceM $ \ e -> f $! m e
{-# INLINE fmapReduce #-}
apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
apReduce (ReduceM f) (ReduceM x) = ReduceM $ \ e -> f e $! x e
{-# INLINE apReduce #-}
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
bindReduce (ReduceM m) f = ReduceM $ \ e -> unReduceM (f $! m e) e
{-# INLINE bindReduce #-}
instance Functor ReduceM where
fmap = fmapReduce
instance Applicative ReduceM where
pure x = ReduceM (const x)
(<*>) = apReduce
instance Monad ReduceM where
return = pure
(>>=) = bindReduce
(>>) = (*>)
#if __GLASGOW_HASKELL__ >= 800
fail = Fail.fail
instance Fail.MonadFail ReduceM where
fail = error
#endif
instance ReadTCState ReduceM where
getTCState = ReduceM redSt
withTCState f = onReduceEnv $ mapRedSt f
runReduceM :: ReduceM a -> TCM a
runReduceM m = do
e <- askTC
s <- getTC
return $! unReduceM m (ReduceEnv e s)
runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
runReduceF f = do
e <- askTC
s <- getTC
return $ \x -> unReduceM (f x) (ReduceEnv e s)
instance MonadTCEnv ReduceM where
askTC = ReduceM redEnv
localTC = onReduceEnv . mapRedEnv
useR :: (ReadTCState m) => Lens' a TCState -> m a
useR l = (^.l) <$> getTCState
askR :: ReduceM ReduceEnv
askR = ReduceM ask
localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
localR f = ReduceM . local f . unReduceM
instance HasOptions ReduceM where
pragmaOptions = useR stPragmaOptions
commandLineOptions = do
p <- useR stPragmaOptions
cl <- stPersistentOptions . stPersistentState <$> getTCState
return $ cl{ optPragmaOptions = p }
class ( Applicative m
, MonadTCEnv m
, ReadTCState m
, HasOptions m
) => MonadReduce m where
liftReduce :: ReduceM a -> m a
instance MonadReduce m => MonadReduce (MaybeT m) where
liftReduce = lift . liftReduce
instance MonadReduce m => MonadReduce (ListT m) where
liftReduce = lift . liftReduce
instance MonadReduce m => MonadReduce (ExceptT err m) where
liftReduce = lift . liftReduce
instance MonadReduce m => MonadReduce (ReaderT r m) where
liftReduce = lift . liftReduce
instance (Monoid w, MonadReduce m) => MonadReduce (WriterT w m) where
liftReduce = lift . liftReduce
instance MonadReduce m => MonadReduce (StateT w m) where
liftReduce = lift . liftReduce
instance MonadReduce ReduceM where
liftReduce = id
class Monad m => MonadTCEnv m where
askTC :: m TCEnv
localTC :: (TCEnv -> TCEnv) -> m a -> m a
instance MonadTCEnv m => MonadTCEnv (MaybeT m) where
askTC = lift askTC
localTC = mapMaybeT . localTC
instance MonadTCEnv m => MonadTCEnv (ListT m) where
askTC = lift askTC
localTC = mapListT . localTC
instance MonadTCEnv m => MonadTCEnv (ExceptT err m) where
askTC = lift askTC
localTC = mapExceptT . localTC
instance MonadTCEnv m => MonadTCEnv (ReaderT r m) where
askTC = lift askTC
localTC = mapReaderT . localTC
instance (Monoid w, MonadTCEnv m) => MonadTCEnv (WriterT w m) where
askTC = lift askTC
localTC = mapWriterT . localTC
instance MonadTCEnv m => MonadTCEnv (StateT s m) where
askTC = lift askTC
localTC = mapStateT . localTC
asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
asksTC f = f <$> askTC
viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a
viewTC l = asksTC (^. l)
locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC l = localTC . over l
class Monad m => MonadTCState m where
getTC :: m TCState
putTC :: TCState -> m ()
modifyTC :: (TCState -> TCState) -> m ()
{-# MINIMAL getTC, (putTC | modifyTC) #-}
putTC = modifyTC . const
modifyTC f = putTC . f =<< getTC
instance MonadTCState m => MonadTCState (MaybeT m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance MonadTCState m => MonadTCState (ListT m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance MonadTCState m => MonadTCState (ExceptT err m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance MonadTCState m => MonadTCState (ReaderT r m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance (Monoid w, MonadTCState m) => MonadTCState (WriterT w m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance MonadTCState m => MonadTCState (StateT s m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
getsTC :: MonadTCState m => (TCState -> a) -> m a
getsTC f = f <$> getTC
modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
modifyTC' f = do
s' <- getTC
putTC $! f s'
useTC :: MonadTCState m => Lens' a TCState -> m a
useTC l = do
!x <- getsTC (^. l)
return x
infix 4 `setTCLens`
setTCLens :: MonadTCState m => Lens' a TCState -> a -> m ()
setTCLens l = modifyTC . set l
modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m ()
modifyTCLens l = modifyTC . over l
modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m ()
modifyTCLensM l f = putTC =<< l f =<< getTC
locallyTCState :: MonadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState l f k = do
old <- useTC l
modifyTCLens l f
x <- k
setTCLens l old
return x
newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }
instance MonadIO m => MonadTCEnv (TCMT m) where
askTC = TCM $ \ _ e -> return e
localTC f (TCM m) = TCM $ \ s e -> m s (f e)
instance MonadIO m => MonadTCState (TCMT m) where
getTC = TCM $ \ r _e -> liftIO (readIORef r)
putTC s = TCM $ \ r _e -> liftIO (writeIORef r s)
type TCM = TCMT IO
class ( Applicative tcm, MonadIO tcm
, MonadTCEnv tcm
, MonadTCState tcm
, HasOptions tcm
) => MonadTCM tcm where
liftTCM :: TCM a -> tcm a
instance MonadIO m => ReadTCState (TCMT m) where
getTCState = getTC
withTCState f m = __IMPOSSIBLE__
instance MonadError TCErr (TCMT IO) where
throwError = liftIO . E.throwIO
catchError m h = TCM $ \r e -> do
oldState <- liftIO (readIORef r)
unTCM m r e `E.catch` \err -> do
case err of
PatternErr -> return ()
_ ->
liftIO $ do
newState <- readIORef r
writeIORef r $ oldState { stPersistentState = stPersistentState newState }
unTCM (h err) r e
instance MonadIO m => MonadReduce (TCMT m) where
liftReduce = liftTCM . runReduceM
instance (IsString a, MonadIO m) => IsString (TCMT m a) where
fromString s = return (fromString s)
type IM = TCMT (Haskeline.InputT IO)
runIM :: IM a -> TCM a
runIM = mapTCMT (Haskeline.runInputT Haskeline.defaultSettings)
instance MonadError TCErr IM where
throwError = liftIO . E.throwIO
catchError m h = mapTCMT liftIO $ runIM m `catchError` (runIM . h)
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \r e ->
unTCM m r e
`E.catch` \err -> unTCM (h err) r e
finally_ :: TCM a -> TCM b -> TCM a
finally_ m f = do
x <- m `catchError_` \ err -> f >> throwError err
_ <- f
return x
{-# SPECIALIZE INLINE mapTCMT :: (forall a. IO a -> IO a) -> TCM a -> TCM a #-}
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
mapTCMT f (TCM m) = TCM $ \s e -> f (m s e)
pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \r e -> do
s <- liftIO $ readIORef r
return (f s e)
{-# RULES "liftTCM/id" liftTCM = id #-}
instance MonadIO m => MonadTCM (TCMT m) where
liftTCM = mapTCMT liftIO
instance MonadTCM tcm => MonadTCM (MaybeT tcm) where
liftTCM = lift . liftTCM
instance MonadTCM tcm => MonadTCM (ListT tcm) where
liftTCM = lift . liftTCM
instance MonadTCM tcm => MonadTCM (ExceptT err tcm) where
liftTCM = lift . liftTCM
instance (Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) where
liftTCM = lift . liftTCM
instance (MonadTCM tcm) => MonadTCM (StateT s tcm) where
liftTCM = lift . liftTCM
instance (MonadTCM tcm) => MonadTCM (ReaderT r tcm) where
liftTCM = lift . liftTCM
instance MonadTrans TCMT where
lift m = TCM $ \_ _ -> m
instance MonadIO m => Monad (TCMT m) where
return = pure
(>>=) = bindTCMT
(>>) = (*>)
#if __GLASGOW_HASKELL__ < 800
fail = internalError
#else
fail = Fail.fail
instance MonadIO m => Fail.MonadFail (TCMT m) where
fail = internalError
#endif
returnTCMT :: MonadIO m => a -> TCMT m a
returnTCMT = \x -> TCM $ \_ _ -> return x
{-# INLINE returnTCMT #-}
bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e
{-# INLINE bindTCMT #-}
thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
{-# INLINE thenTCMT #-}
instance MonadIO m => Functor (TCMT m) where
fmap = fmapTCMT
fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
{-# INLINE fmapTCMT #-}
instance MonadIO m => Applicative (TCMT m) where
pure = returnTCMT
(<*>) = apTCMT
apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
{-# INLINE apTCMT #-}
instance MonadIO m => MonadIO (TCMT m) where
liftIO m = TCM $ \s e -> do
let r = envRange e
liftIO $ wrap s r $ do
x <- m
x `seq` return x
where
wrap s r m = E.catch m $ \e -> do
s <- readIORef s
E.throwIO $ IOException s r e
instance MonadBench Phase TCM where
getBenchmark = liftIO $ getBenchmark
putBenchmark = liftIO . putBenchmark
finally = finally_
instance Null (TCM Doc) where
empty = return empty
null = __IMPOSSIBLE__
instance Semigroup (TCM Any) where
ma <> mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb)
instance Monoid (TCM Any) where
mempty = return mempty
mappend = (<>)
patternViolation :: TCM a
patternViolation = throwError PatternErr
internalError :: MonadTCM tcm => String -> tcm a
internalError s = typeError $ InternalError s
genericError :: MonadTCM tcm => String -> tcm a
genericError = typeError . GenericError
{-# SPECIALIZE genericDocError :: Doc -> TCM a #-}
genericDocError :: MonadTCM tcm => Doc -> tcm a
genericDocError = typeError . GenericDocError
{-# SPECIALIZE typeError :: TypeError -> TCM a #-}
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError err = liftTCM $ throwError =<< typeError_ err
{-# SPECIALIZE typeError_ :: TypeError -> TCM TCErr #-}
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
typeError_ err = liftTCM $ TypeError <$> getTC <*> buildClosure err
{-# SPECIALIZE runTCM :: TCEnv -> TCState -> TCM a -> IO (a, TCState) #-}
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM e s m = do
r <- liftIO $ newIORef s
a <- unTCM m r e
s <- liftIO $ readIORef r
return (a, s)
runTCMTop :: TCM a -> IO (Either TCErr a)
runTCMTop m = (Right <$> runTCMTop' m) `E.catch` (return . Left)
runTCMTop' :: MonadIO m => TCMT m a -> m a
runTCMTop' m = do
r <- liftIO $ newIORef initState
unTCM m r initEnv
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
runSafeTCM m st = runTCM initEnv st m `E.catch` (\ (e :: TCErr) -> __IMPOSSIBLE__)
forkTCM :: TCM a -> TCM ()
forkTCM m = do
s <- getTC
e <- askTC
liftIO $ void $ C.forkIO $ void $ runTCM e s m
extendedLambdaName :: String
extendedLambdaName = ".extendedlambda"
isExtendedLambdaName :: A.QName -> Bool
isExtendedLambdaName = (extendedLambdaName `List.isPrefixOf`) . prettyShow . nameConcrete . qnameName
absurdLambdaName :: String
absurdLambdaName = ".absurdlambda"
isAbsurdLambdaName :: QName -> Bool
isAbsurdLambdaName = (absurdLambdaName ==) . prettyShow . qnameName
generalizedFieldName :: String
generalizedFieldName = ".generalizedField-"
getGeneralizedFieldName :: A.QName -> Maybe String
getGeneralizedFieldName q
| List.isPrefixOf generalizedFieldName strName = Just (drop (length generalizedFieldName) strName)
| otherwise = Nothing
where strName = prettyShow $ nameConcrete $ qnameName q
instance KillRange Signature where
killRange (Sig secs defs rews) = killRange2 Sig secs defs rews
instance KillRange Sections where
killRange = fmap killRange
instance KillRange Definitions where
killRange = fmap killRange
instance KillRange RewriteRuleMap where
killRange = fmap killRange
instance KillRange Section where
killRange (Section tel) = killRange1 Section tel
instance KillRange Definition where
killRange (Defn ai name t pols occs gens gpars displ mut compiled inst copy ma nc inj def) =
killRange16 Defn ai name t pols occs gens gpars displ mut compiled inst copy ma nc inj def
instance KillRange NumGeneralizableArgs where
killRange = id
instance KillRange NLPat where
killRange (PVar x y) = killRange2 PVar x y
killRange (PWild) = PWild
killRange (PDef x y) = killRange2 PDef x y
killRange (PLam x y) = killRange2 PLam x y
killRange (PPi x y) = killRange2 PPi x y
killRange (PBoundVar x y) = killRange2 PBoundVar x y
killRange (PTerm x) = killRange1 PTerm x
instance KillRange NLPType where
killRange (NLPType s a) = killRange2 NLPType s a
instance KillRange RewriteRule where
killRange (RewriteRule q gamma f es rhs t) =
killRange6 RewriteRule q gamma f es rhs t
instance KillRange CompiledRepresentation where
killRange = id
instance KillRange EtaEquality where
killRange = id
instance KillRange System where
killRange (System tel sys) = System (killRange tel) (killRange sys)
instance KillRange ExtLamInfo where
killRange (ExtLamInfo m sys) = killRange2 ExtLamInfo m sys
instance KillRange FunctionFlag where
killRange = id
instance KillRange CompKit where
killRange = id
instance KillRange Defn where
killRange def =
case def of
Axiom -> Axiom
DataOrRecSig n -> DataOrRecSig n
GeneralizableVar -> GeneralizableVar
AbstractDefn{} -> __IMPOSSIBLE__
Function cls comp ct tt covering inv mut isAbs delayed proj flags term extlam with copat ->
killRange15 Function cls comp ct tt covering inv mut isAbs delayed proj flags term extlam with copat
Datatype a b c d e f g h i -> killRange8 Datatype a b c d e f g h i
Record a b c d e f g h i j k -> killRange11 Record a b c d e f g h i j k
Constructor a b c d e f g h i -> killRange9 Constructor a b c d e f g h i
Primitive a b c d e -> killRange5 Primitive a b c d e
instance KillRange MutualId where
killRange = id
instance KillRange c => KillRange (FunctionInverse' c) where
killRange NotInjective = NotInjective
killRange (Inverse m) = Inverse $ killRangeMap m
instance KillRange TermHead where
killRange SortHead = SortHead
killRange PiHead = PiHead
killRange (ConsHead q) = ConsHead $ killRange q
killRange h@VarHead{} = h
killRange UnknownHead = UnknownHead
instance KillRange Projection where
killRange (Projection a b c d e) = killRange5 Projection a b c d e
instance KillRange ProjLams where
killRange = id
instance KillRange a => KillRange (Open a) where
killRange = fmap killRange
instance KillRange DisplayForm where
killRange (Display n es dt) = killRange3 Display n es dt
instance KillRange Polarity where
killRange = id
instance KillRange IsForced where
killRange = id
instance KillRange DoGeneralize where
killRange = id
instance KillRange DisplayTerm where
killRange dt =
case dt of
DWithApp dt dts es -> killRange3 DWithApp dt dts es
DCon q ci dts -> killRange3 DCon q ci dts
DDef q dts -> killRange2 DDef q dts
DDot v -> killRange1 DDot v
DTerm v -> killRange1 DTerm v
instance KillRange a => KillRange (Closure a) where
killRange = id