{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Monad.Base where
import Prelude hiding (null)
import qualified Control.Concurrent as C
import qualified Control.Exception as E
import qualified Control.Monad.Fail as Fail
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Identity
import Control.Monad.Trans.Maybe
import Control.Applicative hiding (empty)
import Data.Array (Ix)
import Data.Function
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
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.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Semigroup ( Semigroup, (<>))
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.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.Generic (TermLike(..))
import Agda.Syntax.Parser (ParseWarning)
import Agda.Syntax.Parser.Monad (parseWarningName)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Notation
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'), underBinder', underBinder)
import {-# SOURCE #-} Agda.Compiler.Backend hiding (Args)
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import {-# SOURCE #-} Agda.Interaction.Response
(InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import Agda.Interaction.Library
import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.Except
( Error(strMsg)
, ExceptT
, MonadError(catchError, throwError)
, mapExceptT
)
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.SmallSet (SmallSet)
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Update
import Agda.Utils.WithDefault ( collapseDefault )
import Agda.Utils.Impossible
data TCState = TCSt
{ stPreScopeState :: !PreScopeState
, stPostScopeState :: !PostScopeState
, stPersistentState :: !PersistentTCState
}
class Monad m => ReadTCState m where
getTCState :: m TCState
locallyTCState :: Lens' a TCState -> (a -> a) -> m b -> m b
withTCState :: (TCState -> TCState) -> m a -> m a
withTCState = locallyTCState id
instance ReadTCState m => ReadTCState (MaybeT m) where
getTCState = lift getTCState
locallyTCState l = mapMaybeT . locallyTCState l
instance ReadTCState m => ReadTCState (ListT m) where
getTCState = lift getTCState
locallyTCState l f = ListT . locallyTCState l f . runListT
instance ReadTCState m => ReadTCState (ExceptT err m) where
getTCState = lift getTCState
locallyTCState l = mapExceptT . locallyTCState l
instance ReadTCState m => ReadTCState (ReaderT r m) where
getTCState = lift getTCState
locallyTCState l = mapReaderT . locallyTCState l
instance (Monoid w, ReadTCState m) => ReadTCState (WriterT w m) where
getTCState = lift getTCState
locallyTCState l = mapWriterT . locallyTCState l
instance ReadTCState m => ReadTCState (StateT s m) where
getTCState = lift getTCState
locallyTCState l = mapStateT . locallyTCState l
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 :: !(Strict.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)
, stPreWarningOnImport :: !(Strict.Maybe String)
, stPreImportedPartialDefs :: !(Set QName)
}
type DisambiguatedNames = IntMap A.QName
type ConcreteNames = Map Name [C.Name]
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 :: !(Strict.Maybe ModuleName)
, stPostInstanceDefs :: !TempInstanceTable
, stPostConcreteNames :: !ConcreteNames
, stPostUsedNames :: !(Map RawName [RawName])
, stPostShadowingNames :: !(Map Name [RawName])
, 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
, stPostPostponeInstanceSearch :: !Bool
, stPostConsideringInstance :: !Bool
, stPostInstantiateBlocking :: !Bool
, stPostLocalPartialDefs :: !(Set QName)
}
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
, stPersistLoadedFileCache :: !(Strict.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
, stPersistLoadedFileCache = empty
, 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
, stPreWarningOnImport = empty
, stPreImportedPartialDefs = Set.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 = empty
, stPostInstanceDefs = (Map.empty , Set.empty)
, stPostConcreteNames = Map.empty
, stPostUsedNames = 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
, stPostPostponeInstanceSearch = False
, stPostConsideringInstance = False
, stPostInstantiateBlocking = False
, stPostLocalPartialDefs = Set.empty
}
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 (Strict.toLazy $ stPreGeneralizedVars (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreGeneralizedVars = Strict.toStrict 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 :: ReadTCState m => m (Map A.QName String)
getUserWarnings = do
iuw <- useR stImportedUserWarnings
luw <- useR stLocalUserWarnings
return $ iuw `Map.union` luw
stWarningOnImport :: Lens' (Maybe String) TCState
stWarningOnImport f s =
f (Strict.toLazy $ stPreWarningOnImport (stPreScopeState s)) <&>
\ x -> s {stPreScopeState = (stPreScopeState s) {stPreWarningOnImport = Strict.toStrict x}}
stImportedPartialDefs :: Lens' (Set QName) TCState
stImportedPartialDefs f s =
f (stPreImportedPartialDefs (stPreScopeState s)) <&>
\ x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedPartialDefs = x}}
stLocalPartialDefs :: Lens' (Set QName) TCState
stLocalPartialDefs f s =
f (stPostLocalPartialDefs (stPostScopeState s)) <&>
\ x -> s {stPostScopeState = (stPostScopeState s) {stPostLocalPartialDefs = x}}
getPartialDefs :: ReadTCState m => m (Set QName)
getPartialDefs = do
ipd <- useR stImportedPartialDefs
lpd <- useR stLocalPartialDefs
return $ ipd `Set.union` lpd
stLoadedFileCache :: Lens' (Maybe LoadedFileCache) TCState
stLoadedFileCache f s =
f (Strict.toLazy $ stPersistLoadedFileCache (stPersistentState s)) <&>
\x -> s {stPersistentState = (stPersistentState s) {stPersistLoadedFileCache = Strict.toStrict x}}
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 (Strict.toLazy $ stPostCurrentModule (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = Strict.toStrict 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' ConcreteNames TCState
stConcreteNames f s =
f (stPostConcreteNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostConcreteNames = x}}
stUsedNames :: Lens' (Map RawName [RawName]) TCState
stUsedNames f s =
f (stPostUsedNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostUsedNames = x}}
stShadowingNames :: Lens' (Map Name [RawName]) 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}}
stPostponeInstanceSearch :: Lens' Bool TCState
stPostponeInstanceSearch f s =
f (stPostPostponeInstanceSearch (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostPostponeInstanceSearch = x}}
stConsideringInstance :: Lens' Bool TCState
stConsideringInstance f s =
f (stPostConsideringInstance (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostConsideringInstance = x}}
stInstantiateBlocking :: Lens' Bool TCState
stInstantiateBlocking f s =
f (stPostInstantiateBlocking (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostInstantiateBlocking = 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)
class Monad m => MonadFresh i m where
fresh :: m i
instance MonadFresh i m => MonadFresh i (ReaderT r m) where
fresh = lift fresh
instance MonadFresh i m => MonadFresh i (StateT s m) where
fresh = lift fresh
instance HasFresh i => MonadFresh i TCM where
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 :: MonadFresh NameId m => Range -> String -> m Name
freshName r s = do
i <- fresh
return $ mkName r i s
freshNoName :: MonadFresh NameId m => Range -> m Name
freshNoName r =
do i <- fresh
return $ Name i (C.NoName noRange i) r noFixity' False
freshNoName_ :: MonadFresh NameId m => m Name
freshNoName_ = freshNoName noRange
freshRecordName :: MonadFresh NameId 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_ :: MonadFresh NameId 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 :: ReadTCState m => AbsolutePath -> m (Maybe TopLevelModuleName)
lookupModuleFromSource f =
fmap fst . List.find ((f ==) . snd) . Map.toList <$> useR stModuleToSource
class Monad m => MonadStConcreteNames m where
runStConcreteNames :: StateT ConcreteNames m a -> m a
useConcreteNames :: m ConcreteNames
useConcreteNames = runStConcreteNames get
modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
modifyConcreteNames = runStConcreteNames . modify
instance MonadStConcreteNames TCM where
runStConcreteNames m = stateTCLensM stConcreteNames $ runStateT m
instance MonadStConcreteNames m => MonadStConcreteNames (ReaderT r m) where
runStConcreteNames m = ReaderT $ runStConcreteNames . StateT . (flip $ runReaderT . runStateT m)
instance MonadStConcreteNames m => MonadStConcreteNames (StateT s m) where
runStConcreteNames m = StateT $ \s -> runStConcreteNames $ StateT $ \ns -> do
((x,ns'),s') <- runStateT (runStateT m ns) s
return ((x,s'),ns')
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
, iImportWarning :: Maybe String
, iBuiltin :: BuiltinThings (String, QName)
, iForeignCode :: Map BackendName [ForeignCode]
, iHighlighting :: HighlightingInfo
, iPragmaOptions :: [OptionsPragma]
, iOptionsUsed :: PragmaOptions
, iPatternSyns :: A.PatternSynDefns
, iWarnings :: [TCWarning]
, iPartialDefs :: Set QName
}
deriving Show
instance Pretty Interface where
pretty (Interface
sourceH source fileT importedM moduleN scope insideS signature
display userwarn importwarn builtin foreignCode highlighting pragmaO
oUsed patternS warnings partialdefs) =
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
, "import warning:" <+> (pretty . show) importwarn
, "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
, "partial definitions:" <+> (pretty . show) partialdefs
]
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
class LensClosure a b | b -> a where
lensClosure :: Lens' (Closure a) b
instance LensClosure a (Closure a) where
lensClosure = id
instance LensTCEnv (Closure a) where
lensTCEnv f cl = (f $! clEnv cl) <&> \ env -> cl { clEnv = env }
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
buildClosure x = do
env <- askTC
sig <- useR stSignature
scope <- useR stScope
cps <- useR 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 CompareAs Term Term
| ValueCmpOnFace Comparison Term Type Term Term
| ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
| TelCmp Type Type Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Level Level
| HasBiggerSort Sort
| HasPTSRule (Dom Type) (Abs Sort)
| CheckMetaInst MetaId
| UnBlock MetaId
| Guarded Constraint ProblemId
| IsEmpty Range Type
| CheckSizeLtSat Term
| FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])
| CheckFunDef Delayed A.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'))
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 a s -> freeVars' (a , s)
UnquoteTactic _ t h g -> freeVars' (t, (h, g))
CheckMetaInst m -> mempty
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')
LevelCmp _ l l' -> foldTerm f (Level l, Level 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 (Sort s1, Sort s2)
UnBlock _ -> mempty
FindInstance _ _ _ -> mempty
CheckFunDef _ _ _ _ -> mempty
HasBiggerSort s -> foldTerm f s
HasPTSRule a s -> foldTerm f (a, Sort <$> s)
CheckMetaInst m -> mempty
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 CompareAs
= AsTermsOf Type
| AsSizes
| AsTypes
deriving (Data, Show)
instance Free CompareAs where
freeVars' (AsTermsOf a) = freeVars' a
freeVars' AsSizes = mempty
freeVars' AsTypes = mempty
instance TermLike CompareAs where
foldTerm f (AsTermsOf a) = foldTerm f a
foldTerm f AsSizes = mempty
foldTerm f AsTypes = mempty
traverseTermM f = \case
AsTermsOf a -> AsTermsOf <$> traverseTermM f a
AsSizes -> return AsSizes
AsTypes -> return AsTypes
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
, jComparison :: Comparison
, jMetaType :: Type
}
| IsSort
{ jMetaId :: a
, jMetaType :: Type
}
instance Show a => Show (Judgement a) where
show (HasType a cmp 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
, mvTwin :: Maybe MetaId
}
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 (NonEmpty 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 = getRelevance . getMetaEnv
getMetaModality :: MetaVariable -> Modality
getMetaModality = getModality . getMetaEnv
metaFrozen :: Lens' Frozen MetaVariable
metaFrozen f mv = f (mvFrozen mv) <&> \ x -> mv { mvFrozen = x }
_mvInfo :: Lens' MetaInfo MetaVariable
_mvInfo f mv = (f $! mvInfo mv) <&> \ mi -> mv { mvInfo = mi }
instance LensClosure Range MetaInfo where
lensClosure f mi = (f $! miClosRange mi) <&> \ cl -> mi { miClosRange = cl }
instance LensClosure Range MetaVariable where
lensClosure = _mvInfo . lensClosure
instance LensIsAbstract TCEnv where
lensIsAbstract f env =
(f $! fromMaybe __IMPOSSIBLE__ (aModeToDef $ envAbstractMode env))
<&> \ a -> env { envAbstractMode = aDefToMode a }
instance LensIsAbstract (Closure a) where
lensIsAbstract = lensTCEnv . lensIsAbstract
instance LensIsAbstract MetaInfo where
lensIsAbstract = lensClosure . lensIsAbstract
data InteractionPoint = InteractionPoint
{ ipRange :: Range
, ipMeta :: Maybe MetaId
, ipSolved:: Bool
, ipClause:: IPClause
}
instance Eq InteractionPoint where (==) = (==) `on` ipMeta
type InteractionPoints = Map InteractionId InteractionPoint
data Overapplied = Overapplied | NotOverapplied deriving (Eq, Show, Data)
data IPBoundary' t = IPBoundary
{ ipbEquations :: [(t,t)]
, ipbValue :: t
, ipbMetaApp :: t
, ipbOverapplied :: Overapplied
}
deriving (Show, Data, Functor, Foldable, Traversable)
type IPBoundary = IPBoundary' Term
data IPClause = IPClause
{ ipcQName :: QName
, ipcClauseNo :: Int
, ipcType :: Type
, ipcWithSub :: Maybe Substitution
, ipcClause :: A.SpineClause
, ipcClosure :: Closure ()
, ipcBoundary :: [Closure IPBoundary]
}
| 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) = underBinder (freeVars' ps) `mappend` underBinder' 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 -> "." <> 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 :: Pretty el => Doc -> [el] -> Doc
pApp d els = mparens (not (null els) && p > 9) $
sep [d, nest 2 $ fsep (map (prettyPrec 10) els)]
defaultDisplayForm :: QName -> [LocalDisplayForm]
defaultDisplayForm c = []
data NLPat
= PVar !Int [Arg Int]
| PDef QName PElims
| PLam ArgInfo (Abs NLPat)
| PPi (Dom NLPType) (Abs NLPType)
| PSort NLPSort
| PBoundVar {-# UNPACK #-} !Int PElims
| PTerm Term
deriving (Data, Show)
type PElims = [Elim' NLPat]
data NLPType = NLPType
{ nlpTypeSort :: NLPSort
, nlpTypeUnEl :: NLPat
} deriving (Data, Show)
data NLPSort
= PType NLPat
| PProp NLPat
| PInf
| PSizeUniv
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 :: Set QName
, defNoCompilation :: Bool
, defInjective :: Bool
, defCopatternLHS :: Bool
, defBlocked :: Blocked_
, theDef :: Defn
}
deriving (Data, Show)
instance LensArgInfo Definition where
getArgInfo = defArgInfo
mapArgInfo f def = def { defArgInfo = f $ defArgInfo def }
instance LensModality Definition where
instance LensQuantity Definition where
instance LensRelevance Definition where
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 = Set.empty
, defNoCompilation = False
, defInjective = False
, defCopatternLHS = False
, defBlocked = NotBlocked ReallyNotBlocked ()
, 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 :: !(Strict.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 :: [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
}
| Datatype
{ dataPars :: Nat
, dataIxs :: Nat
, 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 :: [Dom 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
, conProj :: Maybe [QName]
, conForced :: [IsForced]
, conErased :: Maybe [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 (Set.toList defMatchable)
, "defInjective =" <?> pshow defInjective
, "defCopatternLHS =" <?> pshow defCopatternLHS
, "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 ] <?> "}"
pretty Datatype{..} =
"Datatype {" <?> vcat
[ "dataPars =" <?> pshow dataPars
, "dataIxs =" <?> pshow dataIxs
, "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
, 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
redReturn :: a -> ReduceM (Reduced a' a)
redReturn = return . YesReduction YesSimplification
redBind :: ReduceM (Reduced a a') -> (a -> b) ->
(a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
redBind ma f k = do
r <- ma
case r of
NoReduction x -> return $ NoReduction $ f x
YesReduction _ y -> k y
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
| TypeLevelReductions
| UnconfirmedReductions
| NonTerminatingReductions
deriving (Show, Eq, Ord, Enum, Bounded, Ix, Data)
type AllowedReductions = SmallSet AllowedReduction
allReductions :: AllowedReductions
allReductions = SmallSet.delete NonTerminatingReductions reallyAllReductions
reallyAllReductions :: AllowedReductions
reallyAllReductions = SmallSet.total
data PrimitiveImpl = PrimImpl Type PrimFun
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
| CheckLHS A.SpineLHS
| CheckPattern A.Pattern Telescope Type
| CheckLetBinding A.LetBinding
| InferExpr A.Expr
| CheckExprCall Comparison A.Expr Type
| CheckDotPattern A.Expr Term
| CheckProjection Range QName Type
| IsTypeCall Comparison A.Expr Sort
| IsType_ A.Expr
| InferVar Name
| InferDef QName
| CheckArguments Range [NamedArg A.Expr] Type (Maybe Type)
| CheckMetaSolution Range MetaId Type Term
| 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
| CheckConfluence QName QName
| 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 CheckLHS{} = "CheckLHS"
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 CheckMetaSolution{} = "CheckMetaSolution"
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 SetRange{} = "SetRange"
pretty CheckSectionApplication{} = "CheckSectionApplication"
pretty CheckIsEmpty{} = "CheckIsEmpty"
pretty CheckConfluence{} = "CheckConfluence"
pretty NoHighlighting{} = "NoHighlighting"
pretty ModuleContents{} = "ModuleContents"
instance HasRange Call where
getRange (CheckClause _ c) = getRange c
getRange (CheckLHS lhs) = getRange lhs
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 cmp e s) = getRange e
getRange (IsType_ e) = getRange e
getRange (InferVar x) = getRange x
getRange (InferDef f) = getRange f
getRange (CheckArguments r _ _ _) = r
getRange (CheckMetaSolution 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 (SetRange r) = r
getRange (CheckSectionApplication r _ _) = r
getRange (CheckIsEmpty r _) = r
getRange (CheckConfluence rule1 rule2) = max (getRange rule1) (getRange rule2)
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 ()
, envCoverageCheck :: CoverageCheck
, envMakeCase :: Bool
, 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
, envActiveBackendName :: Maybe BackendName
}
deriving Data
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envCurrentPath = Nothing
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envTerminationCheck = TerminationCheck
, envCoverageCheck = YesCoverageCheck
, envMakeCase = False
, envSolvingConstraints = False
, envCheckingWhere = False
, envActiveProblems = Set.empty
, envWorkingOnTypes = False
, envAssignMetas = True
, envAbstractMode = ConcreteMode
, envModality = mempty
, 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
, envActiveBackendName = Nothing
}
class LensTCEnv a where
lensTCEnv :: Lens' TCEnv a
instance LensTCEnv TCEnv where
lensTCEnv = id
instance LensModality TCEnv where
getModality = setCohesion defaultCohesion . envModality
mapModality f e = e { envModality = setCohesion defaultCohesion $ f $ envModality e }
instance LensRelevance TCEnv where
instance LensQuantity TCEnv where
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 }
eCoverageCheck :: Lens' CoverageCheck TCEnv
eCoverageCheck f e = f (envCoverageCheck e) <&> \ x -> e { envCoverageCheck = x }
eMakeCase :: Lens' Bool TCEnv
eMakeCase f e = f (envMakeCase e) <&> \ x -> e { envMakeCase = 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 (getModality e) <&> \ x -> setModality x e
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 }
eActiveBackendName :: Lens' (Maybe BackendName) TCEnv
eActiveBackendName f e = f (envActiveBackendName e) <&> \ x -> e { envActiveBackendName = 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 -> Maybe IsAbstract
aModeToDef AbstractMode = Just AbstractDef
aModeToDef ConcreteMode = Just ConcreteDef
aModeToDef _ = Nothing
data ExpandHidden
= ExpandLast
| DontExpandLast
| ReallyDontExpandLast
deriving (Eq, Data)
isDontExpandLast :: ExpandHidden -> Bool
isDontExpandLast ExpandLast = False
isDontExpandLast DontExpandLast = True
isDontExpandLast ReallyDontExpandLast = True
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 [Range]
| 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
| ClashesViaRenaming NameOrModule [C.Name]
| 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
| SafeFlagNoCoverageCheck
| SafeFlagInjective
| SafeFlagEta
| ParseWarning ParseWarning
| LibraryWarning LibWarning
| DeprecationWarning String String String
| UserWarning String
| FixityInRenamingModule (NonEmpty Range)
| ModuleDoesntExport C.QName [C.ImportedName]
| InfectiveImport String ModuleName
| CoInfectiveImport String ModuleName
| RewriteNonConfluent Term Term Term Doc
| RewriteMaybeNonConfluent Term Term [Doc]
| PragmaCompileErased BackendName QName
| NotInScopeW [C.QName]
deriving (Show , Data)
warningName :: Warning -> WarningName
warningName = \case
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_
FixityInRenamingModule{} -> FixityInRenamingModule_
GenericNonFatalError{} -> GenericNonFatalError_
GenericWarning{} -> GenericWarning_
InversionDepthReached{} -> InversionDepthReached_
ModuleDoesntExport{} -> ModuleDoesntExport_
NotInScopeW{} -> NotInScope_
NotStrictlyPositive{} -> NotStrictlyPositive_
OldBuiltin{} -> OldBuiltin_
SafeFlagNoPositivityCheck -> SafeFlagNoPositivityCheck_
SafeFlagNonTerminating -> SafeFlagNonTerminating_
SafeFlagNoUniverseCheck -> SafeFlagNoUniverseCheck_
SafeFlagPolarity -> SafeFlagPolarity_
SafeFlagPostulate{} -> SafeFlagPostulate_
SafeFlagPragma{} -> SafeFlagPragma_
SafeFlagEta -> SafeFlagEta_
SafeFlagInjective -> SafeFlagInjective_
SafeFlagNoCoverageCheck -> SafeFlagNoCoverageCheck_
SafeFlagWithoutKFlagPrimEraseEquality -> SafeFlagWithoutKFlagPrimEraseEquality_
WithoutKFlagPrimEraseEquality -> WithoutKFlagPrimEraseEquality_
SafeFlagTerminating -> SafeFlagTerminating_
TerminationIssue{} -> TerminationIssue_
UnreachableClauses{} -> UnreachableClauses_
UnsolvedInteractionMetas{} -> UnsolvedInteractionMetas_
UnsolvedConstraints{} -> UnsolvedConstraints_
UnsolvedMetaVariables{} -> UnsolvedMetaVariables_
UselessInline{} -> UselessInline_
UselessPublic{} -> UselessPublic_
ClashesViaRenaming{} -> ClashesViaRenaming_
UserWarning{} -> UserWarning_
InfectiveImport{} -> InfectiveImport_
CoInfectiveImport{} -> CoInfectiveImport_
RewriteNonConfluent{} -> RewriteNonConfluent_
RewriteMaybeNonConfluent{} -> RewriteMaybeNonConfluent_
PragmaCompileErased{} -> PragmaCompileErased_
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
(==) = (==) `on` tcWarningPrintedWarning
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 Bool (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
| UnifyUnusableModality Telescope Type Int Term Modality
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) [NamedName]
| WrongIrrelevanceInLambda
| WrongQuantityInLambda
| WrongCohesionInLambda
| QuantityMismatch Quantity Quantity
| 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)
| SplitOnUnusableCohesion (Dom Type)
| SplitOnNonVariable Term Type
| DefinitionIsIrrelevant QName
| DefinitionIsErased QName
| VariableIsIrrelevant Name
| VariableIsErased Name
| VariableIsOfUnusableCohesion Name Cohesion
| UnequalLevel Comparison Level Level
| UnequalTerms Comparison Term Term CompareAs
| UnequalTypes Comparison Type Type
| UnequalRelevance Comparison Term Term
| UnequalQuantity Comparison Term Term
| UnequalCohesion Comparison Term Term
| UnequalHiding Term Term
| UnequalSorts Sort Sort
| UnequalBecauseOfUniverseConflict Comparison Term Term
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId Nat
| MetaOccursInItself MetaId
| MetaIrrelevantSolution MetaId Term
| MetaErasedSolution 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
| IllegalPatternInTelescope C.Binder
| 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 (NonEmpty A.QName)
| AmbiguousModule C.QName (NonEmpty 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 (NonEmpty (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
default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions
pragmaOptions = lift pragmaOptions
default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions
commandLineOptions = lift 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 (ChangeT m)
instance HasOptions m => HasOptions (ExceptT e m)
instance HasOptions m => HasOptions (IdentityT m)
instance HasOptions m => HasOptions (ListT m)
instance HasOptions m => HasOptions (MaybeT m)
instance HasOptions m => HasOptions (ReaderT r m)
instance HasOptions m => HasOptions (StateT s m)
instance (HasOptions m, Monoid w) => HasOptions (WriterT w m)
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
getIncludeDirs :: HasOptions m => m [AbsolutePath]
getIncludeDirs = do
incs <- optAbsoluteIncludePaths <$> commandLineOptions
case incs of
[] -> __IMPOSSIBLE__
_ -> return incs
enableCaching :: HasOptions m => m Bool
enableCaching = optCaching <$> 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__ < 808
fail = Fail.fail
#endif
instance Fail.MonadFail ReduceM where
fail = error
instance ReadTCState ReduceM where
getTCState = ReduceM redSt
locallyTCState l f = onReduceEnv $ mapRedSt $ over l 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 = do
!x <- (^.l) <$> getTCState
return x
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
instance MonadTCEnv m => MonadTCEnv (ChangeT m) where
askTC = lift askTC
localTC = mapChangeT . localTC
instance MonadTCEnv m => MonadTCEnv (IdentityT m) where
askTC = lift askTC
localTC = mapIdentityT . 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
instance MonadTCState m => MonadTCState (ChangeT m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
instance MonadTCState m => MonadTCState (IdentityT m) where
getTC = lift getTC
putTC = lift . putTC
modifyTC = lift . modifyTC
getsTC :: ReadTCState m => (TCState -> a) -> m a
getsTC f = f <$> getTCState
modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
modifyTC' f = do
s' <- getTC
putTC $! f s'
useTC :: ReadTCState 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
stateTCLens :: MonadTCState m => Lens' a TCState -> (a -> (r , a)) -> m r
stateTCLens l f = stateTCLensM l $ return . f
stateTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m (r , a)) -> m r
stateTCLensM l f = do
s <- getTC
(result , x) <- f $ s ^. l
putTC $ set l x s
return result
newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }
type TCM = TCMT IO
{-# 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)
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 MonadTrans TCMT where
lift m = TCM $ \_ _ -> m
instance MonadIO m => Monad (TCMT m) where
return = pure
(>>=) = bindTCMT
(>>) = (*>)
#if __GLASGOW_HASKELL__ < 808
fail = Fail.fail
#endif
instance MonadIO m => Fail.MonadFail (TCMT m) where
fail = internalError
instance MonadIO m => MonadIO (TCMT m) where
liftIO m = TCM $ \ s env -> do
liftIO $ wrap s (envRange env) $ do
x <- m
x `seq` return x
where
wrap s r m = E.catch m $ \ err -> do
s <- readIORef s
E.throwIO $ IOException s r err
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)
instance MonadIO m => ReadTCState (TCMT m) where
getTCState = getTC
locallyTCState l f = bracket_ (useTC l <* modifyTCLens l f) (setTCLens l)
instance MonadError TCErr TCM where
throwError = liftIO . E.throwIO
catchError m h = TCM $ \ r e -> do
oldState <- 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 CatchImpossible TCM where
catchImpossibleJust f m h = TCM $ \ r e -> do
s <- readIORef r
catchImpossibleJust f (unTCM m r e) $ \ err -> do
writeIORef r s
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)
instance {-# OVERLAPPABLE #-} (MonadIO m, Semigroup a) => Semigroup (TCMT m a) where
(<>) = liftA2 (<>)
instance {-# OVERLAPPABLE #-} (MonadIO m, Semigroup a, Monoid a) => Monoid (TCMT m a) where
mempty = pure mempty
mappend = (<>)
mconcat = mconcat <.> sequence
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 = liftTCM $ 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
class ( Applicative tcm, MonadIO tcm
, MonadTCEnv tcm
, MonadTCState tcm
, HasOptions tcm
) => MonadTCM tcm where
liftTCM :: TCM a -> tcm a
default liftTCM :: (MonadTCM m, MonadTrans t, tcm ~ t m) => TCM a -> tcm a
liftTCM = lift . liftTCM
{-# RULES "liftTCM/id" liftTCM = id #-}
instance MonadIO m => MonadTCM (TCMT m) where
liftTCM = mapTCMT liftIO
instance MonadTCM tcm => MonadTCM (ChangeT tcm)
instance MonadTCM tcm => MonadTCM (ExceptT err tcm)
instance MonadTCM tcm => MonadTCM (IdentityT tcm)
instance MonadTCM tcm => MonadTCM (ListT tcm)
instance MonadTCM tcm => MonadTCM (MaybeT tcm)
instance MonadTCM tcm => MonadTCM (ReaderT r tcm)
instance MonadTCM tcm => MonadTCM (StateT s tcm)
instance (Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm)
instance MonadBench Phase TCM where
getBenchmark = liftIO $ getBenchmark
putBenchmark = liftIO . putBenchmark
finally = finally_
instance Null (TCM Doc) where
empty = return empty
null = __IMPOSSIBLE__
patternViolation :: MonadError TCErr m => m a
patternViolation = throwError PatternErr
internalError :: MonadTCM tcm => String -> tcm a
internalError s = liftTCM $ typeError $ InternalError s
genericError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
=> String -> m a
genericError = typeError . GenericError
{-# SPECIALIZE genericDocError :: Doc -> TCM a #-}
genericDocError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
=> Doc -> m a
genericDocError = typeError . GenericDocError
{-# SPECIALIZE typeError :: TypeError -> TCM a #-}
typeError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
=> TypeError -> m a
typeError err = throwError =<< typeError_ err
{-# SPECIALIZE typeError_ :: TypeError -> TCM TCErr #-}
typeError_ :: (MonadTCEnv m, ReadTCState m) => TypeError -> m TCErr
typeError_ err = TypeError <$> getTCState <*> 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
patternInTeleName :: String
patternInTeleName = ".patternInTele"
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 copat blk def) =
killRange18 Defn ai name t pols occs gens gpars displ mut compiled inst copy ma nc inj copat blk def
instance KillRange NumGeneralizableArgs where
killRange = id
instance KillRange NLPat where
killRange (PVar x y) = killRange2 PVar x y
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 (PSort x) = killRange1 PSort x
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 NLPSort where
killRange (PType l) = killRange1 PType l
killRange (PProp l) = killRange1 PProp l
killRange PInf = PInf
killRange PSizeUniv = PSizeUniv
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 ->
killRange14 Function cls comp ct tt covering inv mut isAbs delayed proj flags term extlam with
Datatype a b c d e f g h -> killRange7 Datatype a b c d e f g h
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 j-> killRange10 Constructor a b c d e f g h i j
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