Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Base

Contents

- Type checking state
- st-prefixed lenses
- Fresh things
  - Managing file names
  - Interface
  - Closure
  - Constraints
- Open things
- Judgements
  - Generalizable variables
  - Meta variables
  - Interaction meta variables
  - Signature
  - Injectivity
  - Mutual blocks
  - Statistics
  - Trace
  - Instance table
  - Builtin things
- Highlighting levels
- Type checking environment
- e-prefixed lenses
  - Context
  - Let bindings
  - Abstract mode
  - Insertion of implicit arguments
- Type checking warnings (aka non-fatal errors)
- Type checking errors
- Accessing options
- The reduce monad
- Monad with read-only `TCEnv`
- Monad with mutable `TCState`
  - `TCState` accessors (no lenses)
  - `TCState` accessors via lenses
- Type checking monad transformer
- KillRange instances

Synopsis

- data TCState = TCSt {
  - stPreScopeState :: !PreScopeState
  - stPostScopeState :: !PostScopeState
  - stPersistentState :: !PersistentTCState
  }
- class Monad m => ReadTCState m where
  - getTCState :: m TCState
  - withTCState :: (TCState -> TCState) -> m a -> m a
- data PreScopeState = PreScopeState {
  - stPreTokens :: !CompressedFile
  - stPreImports :: !Signature
  - stPreImportedModules :: !(Set ModuleName)
  - stPreModuleToSource :: !ModuleToSource
  - stPreVisitedModules :: !VisitedModules
  - stPreScope :: !ScopeInfo
  - stPrePatternSyns :: !PatternSynDefns
  - stPrePatternSynImports :: !PatternSynDefns
  - stPreGeneralizedVars :: !(Maybe (Set QName))
  - stPrePragmaOptions :: !PragmaOptions
  - stPreImportedBuiltins :: !(BuiltinThings PrimFun)
  - stPreImportedDisplayForms :: !DisplayForms
  - stPreImportedInstanceDefs :: !InstanceTable
  - stPreForeignCode :: !(Map BackendName [ForeignCode])
  - stPreFreshInteractionId :: !InteractionId
  - stPreImportedUserWarnings :: !(Map QName String)
  - stPreLocalUserWarnings :: !(Map QName String)
  }
- type DisambiguatedNames = IntMap QName
- data PostScopeState = PostScopeState {
  - stPostSyntaxInfo :: !CompressedFile
  - stPostDisambiguatedNames :: !DisambiguatedNames
  - stPostMetaStore :: !MetaStore
  - stPostInteractionPoints :: !InteractionPoints
  - stPostAwakeConstraints :: !Constraints
  - stPostSleepingConstraints :: !Constraints
  - stPostDirty :: !Bool
  - stPostOccursCheckDefs :: !(Set QName)
  - stPostSignature :: !Signature
  - stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
  - stPostImportsDisplayForms :: !DisplayForms
  - stPostCurrentModule :: !(Maybe ModuleName)
  - stPostInstanceDefs :: !TempInstanceTable
  - stPostConcreteNames :: !(Map Name [Name])
  - stPostShadowingNames :: !(Map Name [Name])
  - stPostStatistics :: !Statistics
  - stPostTCWarnings :: ![TCWarning]
  - stPostMutualBlocks :: !(Map MutualId MutualBlock)
  - stPostLocalBuiltins :: !(BuiltinThings PrimFun)
  - stPostFreshMetaId :: !MetaId
  - stPostFreshMutualId :: !MutualId
  - stPostFreshProblemId :: !ProblemId
  - stPostFreshCheckpointId :: !CheckpointId
  - stPostFreshInt :: !Int
  - stPostFreshNameId :: !NameId
  - stPostAreWeCaching :: !Bool
  - stPostConsideringInstance :: !Bool
  }
- data MutualBlock = MutualBlock {
  - mutualInfo :: MutualInfo
  - mutualNames :: Set QName
  }
- data PersistentTCState = PersistentTCSt {
  - stDecodedModules :: DecodedModules
  - stPersistentOptions :: CommandLineOptions
  - stInteractionOutputCallback :: InteractionOutputCallback
  - stBenchmark :: !Benchmark
  - stAccumStatistics :: !Statistics
  - stLoadedFileCache :: !(Maybe LoadedFileCache)
  - stPersistBackends :: [Backend]
  }
- data LoadedFileCache = LoadedFileCache {
  - lfcCached :: !CachedTypeCheckLog
  - lfcCurrent :: !CurrentTypeCheckLog
  }
- type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- data TypeCheckAction
  - = EnterSection !ModuleInfo !ModuleName !Telescope
  - | LeaveSection !ModuleName
  - | Decl !Declaration
  - | Pragmas !PragmaOptions
- initPersistentState :: PersistentTCState
- initPreScopeState :: PreScopeState
- initPostScopeState :: PostScopeState
- initState :: TCState
- stTokens :: Lens' CompressedFile TCState
- stImports :: Lens' Signature TCState
- stImportedModules :: Lens' (Set ModuleName) TCState
- stModuleToSource :: Lens' ModuleToSource TCState
- stVisitedModules :: Lens' VisitedModules TCState
- stScope :: Lens' ScopeInfo TCState
- stPatternSyns :: Lens' PatternSynDefns TCState
- stPatternSynImports :: Lens' PatternSynDefns TCState
- stGeneralizedVars :: Lens' (Maybe (Set QName)) TCState
- stPragmaOptions :: Lens' PragmaOptions TCState
- stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState
- stFreshInteractionId :: Lens' InteractionId TCState
- stImportedUserWarnings :: Lens' (Map QName String) TCState
- stLocalUserWarnings :: Lens' (Map QName String) TCState
- getUserWarnings :: MonadTCState m => m (Map QName String)
- stBackends :: Lens' [Backend] TCState
- stFreshNameId :: Lens' NameId TCState
- stSyntaxInfo :: Lens' CompressedFile TCState
- stDisambiguatedNames :: Lens' DisambiguatedNames TCState
- stMetaStore :: Lens' MetaStore TCState
- stInteractionPoints :: Lens' InteractionPoints TCState
- stAwakeConstraints :: Lens' Constraints TCState
- stSleepingConstraints :: Lens' Constraints TCState
- stDirty :: Lens' Bool TCState
- stOccursCheckDefs :: Lens' (Set QName) TCState
- stSignature :: Lens' Signature TCState
- stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState
- stImportsDisplayForms :: Lens' DisplayForms TCState
- stImportedDisplayForms :: Lens' DisplayForms TCState
- stCurrentModule :: Lens' (Maybe ModuleName) TCState
- stImportedInstanceDefs :: Lens' InstanceTable TCState
- stInstanceDefs :: Lens' TempInstanceTable TCState
- stConcreteNames :: Lens' (Map Name [Name]) TCState
- stShadowingNames :: Lens' (Map Name [Name]) TCState
- stStatistics :: Lens' Statistics TCState
- stTCWarnings :: Lens' [TCWarning] TCState
- stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
- stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stFreshMetaId :: Lens' MetaId TCState
- stFreshMutualId :: Lens' MutualId TCState
- stFreshProblemId :: Lens' ProblemId TCState
- stFreshCheckpointId :: Lens' CheckpointId TCState
- stFreshInt :: Lens' Int TCState
- stAreWeCaching :: Lens' Bool TCState
- stConsideringInstance :: Lens' Bool TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- class Enum i => HasFresh i where
  - freshLens :: Lens' i TCState
  - nextFresh' :: i -> i
- nextFresh :: HasFresh i => TCState -> (i, TCState)
- fresh :: (HasFresh i, MonadTCState m) => m i
- newtype ProblemId = ProblemId Nat
- newtype CheckpointId = CheckpointId Int
- freshName :: MonadTCState m => Range -> String -> m Name
- freshNoName :: MonadTCState m => Range -> m Name
- freshNoName_ :: MonadTCState m => m Name
- freshRecordName :: MonadTCState m => m Name
- class FreshName a where
  - freshName_ :: MonadTCState m => a -> m Name
- type ModuleToSource = Map TopLevelModuleName AbsolutePath
- type SourceToModule = Map AbsolutePath TopLevelModuleName
- sourceToModule :: TCM SourceToModule
- lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
- data ModuleInfo = ModuleInfo {
  - miInterface :: Interface
  - miWarnings :: Bool
  - miPrimitive :: Bool
  }
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName Interface
- data ForeignCode = ForeignCode Range String
- 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 QName String
  - iBuiltin :: BuiltinThings (String, QName)
  - iForeignCode :: Map BackendName [ForeignCode]
  - iHighlighting :: HighlightingInfo
  - iPragmaOptions :: [OptionsPragma]
  - iOptionsUsed :: PragmaOptions
  - iPatternSyns :: PatternSynDefns
  - iWarnings :: [TCWarning]
  }
- iFullHash :: Interface -> Hash
- data Closure a = Closure {
  - clSignature :: Signature
  - clEnv :: TCEnv
  - clScope :: ScopeInfo
  - clModuleCheckpoints :: Map ModuleName CheckpointId
  - clValue :: a
  }
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {
  - constraintProblems :: Set ProblemId
  - theConstraint :: Closure Constraint
  }
- data Constraint
  - = ValueCmp Comparison Type Term Term
  - | ValueCmpOnFace Comparison Term Type Term Term
  - | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
  - | TypeCmp Comparison Type Type
  - | TelCmp Type Type Comparison Telescope Telescope
  - | SortCmp Comparison Sort Sort
  - | LevelCmp Comparison Level Level
  - | HasBiggerSort Sort
  - | HasPTSRule Sort (Abs Sort)
  - | UnBlock MetaId
  - | Guarded Constraint ProblemId
  - | IsEmpty Range Type
  - | CheckSizeLtSat Term
  - | FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])
  - | CheckFunDef Delayed DefInfo QName [Clause]
  - | UnquoteTactic (Maybe MetaId) Term Term Type
- data Comparison
  - = CmpEq
  - | CmpLeq
- data CompareDirection
  - = DirEq
  - | DirLeq
  - | DirGeq
- fromCmp :: Comparison -> CompareDirection
- flipCmp :: CompareDirection -> CompareDirection
- dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
- data Open a = OpenThing {
  - openThingCheckpoint :: CheckpointId
  - openThing :: a
  }
- data Judgement a
  - = HasType {
    - jMetaId :: a
    - jMetaType :: Type
    }
  - | IsSort {
    - jMetaId :: a
    - jMetaType :: Type
    }
- data DoGeneralize
  - = YesGeneralize
  - | NoGeneralize
- data GeneralizedValue = GeneralizedValue {
  - genvalCheckpoint :: CheckpointId
  - genvalTerm :: Term
  - genvalType :: Type
  }
- data MetaVariable = MetaVar {
  - mvInfo :: MetaInfo
  - mvPriority :: MetaPriority
  - mvPermutation :: Permutation
  - mvJudgement :: Judgement MetaId
  - mvInstantiation :: MetaInstantiation
  - mvListeners :: Set Listener
  - mvFrozen :: Frozen
  }
- data Listener
  - = EtaExpand MetaId
  - | CheckConstraint Nat ProblemConstraint
- data Frozen
  - = Frozen
  - | Instantiable
- 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 Expr Type
  - | CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term)
  - | CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonemptyList QName) Args Type Int Term Type
  - | CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type
  - | DoQuoteTerm Comparison Term Type
- newtype MetaPriority = MetaPriority Int
- data RunMetaOccursCheck
  - = RunMetaOccursCheck
  - | DontRunMetaOccursCheck
- data MetaInfo = MetaInfo {
  - miClosRange :: Closure Range
  - miMetaOccursCheck :: RunMetaOccursCheck
  - miNameSuggestion :: MetaNameSuggestion
  - miGeneralizable :: Arg DoGeneralize
  }
- type MetaNameSuggestion = String
- data NamedMeta = NamedMeta {
  - nmSuggestion :: MetaNameSuggestion
  - nmid :: MetaId
  }
- type MetaStore = IntMap MetaVariable
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaInfo :: MetaVariable -> Closure Range
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- getMetaRelevance :: MetaVariable -> Relevance
- getMetaModality :: MetaVariable -> Modality
- metaFrozen :: Lens' Frozen MetaVariable
- data InteractionPoint = InteractionPoint {
  - ipRange :: Range
  - ipMeta :: Maybe MetaId
  - ipSolved :: Bool
  - ipClause :: IPClause
  }
- type InteractionPoints = Map InteractionId InteractionPoint
- data IPClause
  - = IPClause {
    - ipcQName :: QName
    - ipcClauseNo :: Int
    - ipcClause :: RHS
    }
  - | IPNoClause
- data Signature = Sig {
  - _sigSections :: Sections
  - _sigDefinitions :: Definitions
  - _sigRewriteRules :: RewriteRuleMap
  }
- sigSections :: Lens' Sections Signature
- sigDefinitions :: Lens' Definitions Signature
- sigRewriteRules :: Lens' RewriteRuleMap Signature
- 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
  }
- secTelescope :: Lens' Telescope Section
- emptySignature :: Signature
- data DisplayForm = Display {
  - dfFreeVars :: Nat
  - dfPats :: Elims
  - dfRHS :: DisplayTerm
  }
- type LocalDisplayForm = Open DisplayForm
- data DisplayTerm
  - = DWithApp DisplayTerm [DisplayTerm] Elims
  - | DCon ConHead ConInfo [Arg DisplayTerm]
  - | DDef QName [Elim' DisplayTerm]
  - | DDot Term
  - | DTerm Term
- defaultDisplayForm :: QName -> [LocalDisplayForm]
- defRelevance :: Definition -> Relevance
- data NLPat
  - = PVar !Int [Arg Int]
  - | PWild
  - | PDef QName PElims
  - | PLam ArgInfo (Abs NLPat)
  - | PPi (Dom NLPType) (Abs NLPType)
  - | PBoundVar !Int PElims
  - | PTerm Term
- type PElims = [Elim' NLPat]
- data NLPType = NLPType {
  - nlpTypeLevel :: NLPat
  - nlpTypeUnEl :: NLPat
  }
- type RewriteRules = [RewriteRule]
- data RewriteRule = RewriteRule {
  - rewName :: QName
  - rewContext :: Telescope
  - rewHead :: QName
  - rewPats :: PElims
  - rewRHS :: Term
  - rewType :: Type
  }
- data Definition = Defn {
  - defArgInfo :: ArgInfo
  - defName :: QName
  - defType :: Type
  - defPolarity :: [Polarity]
  - defArgOccurrences :: [Occurrence]
  - defArgGeneralizable :: NumGeneralizableArgs
  - defGeneralizedParams :: [Maybe Name]
  - defDisplay :: [LocalDisplayForm]
  - defMutual :: MutualId
  - defCompiledRep :: CompiledRepresentation
  - defInstance :: Maybe QName
  - defCopy :: Bool
  - defMatchable :: Bool
  - defNoCompilation :: Bool
  - defInjective :: Bool
  - theDef :: Defn
  }
- data NumGeneralizableArgs
  - = NoGeneralizableArgs
  - | SomeGeneralizableArgs Int
- theDefLens :: Lens' Defn Definition
- defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
- data Polarity
  - = Covariant
  - | Contravariant
  - | Invariant
  - | Nonvariant
- data IsForced
  - = Forced
  - | NotForced
- data CompilerPragma = CompilerPragma Range String
- type BackendName = String
- jsBackendName :: BackendName
- ghcBackendName :: BackendName
- type CompiledRepresentation = Map BackendName [CompilerPragma]
- noCompiledRep :: CompiledRepresentation
- type Face = [(Term, Bool)]
- data System = System {
  - systemTel :: Telescope
  - systemClauses :: [(Face, Term)]
  }
- data ExtLamInfo = ExtLamInfo {
  - extLamModule :: ModuleName
  - extLamSys :: !(Maybe System)
  }
- modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
- data Projection = Projection {
  - projProper :: Maybe QName
  - projOrig :: QName
  - projFromType :: Arg QName
  - projIndex :: Int
  - projLams :: ProjLams
  }
- newtype ProjLams = ProjLams {
  - getProjLams :: [Arg ArgName]
  }
- projDropPars :: Projection -> ProjOrigin -> Term
- projArgInfo :: Projection -> ArgInfo
- data EtaEquality
  - = Specified {
    - theEtaEquality :: !HasEta
    }
  - | Inferred {
    - theEtaEquality :: !HasEta
    }
- setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
- data FunctionFlag
  - = FunStatic
  - | FunInline
  - | FunMacro
- data CompKit = CompKit {
  - nameOfHComp :: Maybe QName
  - nameOfTransp :: Maybe QName
  }
- emptyCompKit :: CompKit
- data Defn
  - = Axiom
  - | DataOrRecSig {
    - datarecPars :: Int
    }
  - | GeneralizableVar
  - | AbstractDefn Defn
  - | Function {
    - funClauses :: [Clause]
    - funCompiled :: Maybe CompiledClauses
    - funSplitTree :: Maybe SplitTree
    - funTreeless :: Maybe Compiled
    - funCovering :: [Closure Clause]
    - funInv :: FunctionInverse
    - funMutual :: Maybe [QName]
    - funAbstr :: IsAbstract
    - funDelayed :: Delayed
    - funProjection :: Maybe Projection
    - funFlags :: Set FunctionFlag
    - funTerminates :: Maybe Bool
    - funExtLam :: Maybe ExtLamInfo
    - funWith :: Maybe QName
    - funCopatternLHS :: Bool
    }
  - | Datatype {
    - dataPars :: Nat
    - dataIxs :: Nat
    - dataInduction :: Induction
    - dataClause :: Maybe Clause
    - dataCons :: [QName]
    - dataSort :: Sort
    - dataMutual :: Maybe [QName]
    - dataAbstr :: IsAbstract
    - dataPathCons :: [QName]
    }
  - | Record {
    - recPars :: Nat
    - recClause :: Maybe Clause
    - recConHead :: ConHead
    - recNamedCon :: Bool
    - recFields :: [Arg QName]
    - recTel :: Telescope
    - recMutual :: Maybe [QName]
    - recEtaEquality' :: EtaEquality
    - recInduction :: Maybe Induction
    - recAbstr :: IsAbstract
    - recComp :: CompKit
    }
  - | Constructor {
    - conPars :: Int
    - conArity :: Int
    - conSrcCon :: ConHead
    - conData :: QName
    - conAbstr :: IsAbstract
    - conInd :: Induction
    - conComp :: (CompKit, Maybe [QName])
    - conForced :: [IsForced]
    - conErased :: [Bool]
    }
  - | Primitive {
    - primAbstr :: IsAbstract
    - primName :: String
    - primClauses :: [Clause]
    - primInv :: FunctionInverse
    - primCompiled :: Maybe CompiledClauses
    }
- recRecursive :: Defn -> Bool
- recEtaEquality :: Defn -> HasEta
- emptyFunction :: Defn
- funFlag :: FunctionFlag -> Lens' Bool Defn
- funStatic :: Lens' Bool Defn
- funInline :: Lens' Bool Defn
- funMacro :: Lens' Bool Defn
- isMacro :: Defn -> Bool
- isEmptyFunction :: Defn -> Bool
- isCopatternLHS :: [Clause] -> Bool
- recCon :: Defn -> QName
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- defConstructors :: Defn -> [QName]
- newtype Fields = Fields [(Name, Type)]
- data Simplification
  - = YesSimplification
  - | NoSimplification
- data Reduced no yes
  - = NoReduction no
  - | YesReduction Simplification yes
- data IsReduced
  - = NotReduced
  - | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
  - isReduced :: IsReduced
  - ignoreReduced :: a
  }
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- type MaybeReducedElims = [MaybeReduced Elim]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data AllowedReduction
  - = ProjectionReductions
  - | InlineReductions
  - | CopatternReductions
  - | FunctionReductions
  - | RecursiveReductions
  - | LevelReductions
  - | UnconfirmedReductions
  - | NonTerminatingReductions
- type AllowedReductions = [AllowedReduction]
- allReductions :: AllowedReductions
- 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
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defParameters :: Definition -> Maybe Nat
- defInverse :: Definition -> FunctionInverse
- defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
- defDelayed :: Definition -> Delayed
- defNonterminating :: Definition -> Bool
- defTerminationUnconfirmed :: Definition -> Bool
- defAbstract :: Definition -> IsAbstract
- defForced :: Definition -> [IsForced]
- type FunctionInverse = FunctionInverse' Clause
- type InversionMap c = Map TermHead [c]
- data FunctionInverse' c
  - = NotInjective
  - | Inverse (InversionMap c)
- data TermHead
  - = SortHead
  - | PiHead
  - | ConsHead QName
  - | VarHead Nat
  - | UnknownHead
- newtype MutualId = MutId Int32
- type Statistics = Map String Integer
- data Call
  - = CheckClause Type SpineClause
  - | CheckPattern Pattern Telescope Type
  - | CheckLetBinding LetBinding
  - | InferExpr Expr
  - | CheckExprCall Comparison Expr Type
  - | CheckDotPattern Expr Term
  - | CheckPatternShadowing SpineClause
  - | CheckProjection Range QName Type
  - | IsTypeCall Expr Sort
  - | IsType_ Expr
  - | InferVar Name
  - | InferDef QName
  - | CheckArguments Range [NamedArg Expr] Type (Maybe Type)
  - | CheckTargetType Range Type Type
  - | CheckDataDef Range QName [LamBinding] [Constructor]
  - | CheckRecDef Range QName [LamBinding] [Constructor]
  - | CheckConstructor QName Telescope Sort Constructor
  - | CheckConstructorFitsIn QName Type Sort
  - | CheckFunDefCall Range QName [Clause]
  - | CheckPragma Range Pragma
  - | CheckPrimitive Range QName Expr
  - | CheckIsEmpty Range Type
  - | CheckWithFunctionType Type
  - | CheckSectionApplication Range ModuleName ModuleApplication
  - | CheckNamedWhere ModuleName
  - | ScopeCheckExpr Expr
  - | ScopeCheckDeclaration NiceDeclaration
  - | ScopeCheckLHS QName Pattern
  - | NoHighlighting
  - | ModuleContents
  - | SetRange Range
- 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
- data HighlightingLevel
  - = None
  - | NonInteractive
  - | Interactive
- data HighlightingMethod
  - = Direct
  - | Indirect
- ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- data TCEnv = TCEnv {
  - envContext :: Context
  - envLetBindings :: LetBindings
  - envCurrentModule :: ModuleName
  - envCurrentPath :: Maybe AbsolutePath
  - envAnonymousModules :: [(ModuleName, Nat)]
  - envImportPath :: [TopLevelModuleName]
  - envMutualBlock :: Maybe MutualId
  - envTerminationCheck :: TerminationCheck ()
  - envSolvingConstraints :: Bool
  - envCheckingWhere :: Bool
  - envWorkingOnTypes :: Bool
  - envAssignMetas :: Bool
  - envActiveProblems :: Set ProblemId
  - envAbstractMode :: AbstractMode
  - envModality :: Modality
  - envDisplayFormsEnabled :: Bool
  - envRange :: Range
  - envHighlightingRange :: Range
  - envClause :: IPClause
  - envCall :: Maybe (Closure Call)
  - envHighlightingLevel :: HighlightingLevel
  - envHighlightingMethod :: HighlightingMethod
  - envModuleNestingLevel :: !Int
  - envExpandLast :: ExpandHidden
  - envAppDef :: Maybe QName
  - envSimplification :: Simplification
  - envAllowedReductions :: AllowedReductions
  - envInjectivityDepth :: Int
  - envCompareBlocked :: Bool
  - envPrintDomainFreePi :: Bool
  - envPrintMetasBare :: Bool
  - envInsideDotPattern :: Bool
  - envUnquoteFlags :: UnquoteFlags
  - envInstanceDepth :: !Int
  - envIsDebugPrinting :: Bool
  - envPrintingPatternLambdas :: [QName]
  - envCallByNeed :: Bool
  - envCurrentCheckpoint :: CheckpointId
  - envCheckpoints :: Map CheckpointId Substitution
  - envGeneralizeMetas :: DoGeneralize
  - envGeneralizedVars :: Map QName GeneralizedValue
  - envCheckOptionConsistency :: Bool
  }
- initEnv :: TCEnv
- envRelevance :: TCEnv -> Relevance
- data UnquoteFlags = UnquoteFlags {
  - _unquoteNormalise :: Bool
  }
- defaultUnquoteFlags :: UnquoteFlags
- unquoteNormalise :: Lens' Bool UnquoteFlags
- eUnquoteNormalise :: Lens' Bool TCEnv
- eContext :: Lens' Context TCEnv
- eLetBindings :: Lens' LetBindings TCEnv
- eCurrentModule :: Lens' ModuleName TCEnv
- eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
- eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
- eImportPath :: Lens' [TopLevelModuleName] TCEnv
- eMutualBlock :: Lens' (Maybe MutualId) TCEnv
- eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
- eSolvingConstraints :: Lens' Bool TCEnv
- eCheckingWhere :: Lens' Bool TCEnv
- eWorkingOnTypes :: Lens' Bool TCEnv
- eAssignMetas :: Lens' Bool TCEnv
- eActiveProblems :: Lens' (Set ProblemId) TCEnv
- eAbstractMode :: Lens' AbstractMode TCEnv
- eModality :: Lens' Modality TCEnv
- eRelevance :: Lens' Relevance TCEnv
- eQuantity :: Lens' Quantity TCEnv
- eDisplayFormsEnabled :: Lens' Bool TCEnv
- eRange :: Lens' Range TCEnv
- eHighlightingRange :: Lens' Range TCEnv
- eCall :: Lens' (Maybe (Closure Call)) TCEnv
- eHighlightingLevel :: Lens' HighlightingLevel TCEnv
- eHighlightingMethod :: Lens' HighlightingMethod TCEnv
- eModuleNestingLevel :: Lens' Int TCEnv
- eExpandLast :: Lens' ExpandHidden TCEnv
- eAppDef :: Lens' (Maybe QName) TCEnv
- eSimplification :: Lens' Simplification TCEnv
- eAllowedReductions :: Lens' AllowedReductions TCEnv
- eInjectivityDepth :: Lens' Int TCEnv
- eCompareBlocked :: Lens' Bool TCEnv
- ePrintDomainFreePi :: Lens' Bool TCEnv
- eInsideDotPattern :: Lens' Bool TCEnv
- eUnquoteFlags :: Lens' UnquoteFlags TCEnv
- eInstanceDepth :: Lens' Int TCEnv
- eIsDebugPrinting :: Lens' Bool TCEnv
- ePrintingPatternLambdas :: Lens' [QName] TCEnv
- eCallByNeed :: Lens' Bool TCEnv
- eCurrentCheckpoint :: Lens' CheckpointId TCEnv
- eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv
- eGeneralizeMetas :: Lens' DoGeneralize TCEnv
- eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv
- type Context = [ContextEntry]
- type ContextEntry = Dom (Name, Type)
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
  - = AbstractMode
  - | ConcreteMode
  - | IgnoreAbstractMode
- aDefToMode :: IsAbstract -> AbstractMode
- aModeToDef :: AbstractMode -> IsAbstract
- data ExpandHidden
  - = ExpandLast
  - | DontExpandLast
- data Candidate = Candidate {
  - candidateTerm :: Term
  - candidateType :: Type
  - candidateOverlappable :: Bool
  }
- data Warning
  - = NicifierIssue DeclarationWarning
  - | TerminationIssue [TerminationError]
  - | UnreachableClauses QName [[NamedArg DeBruijnPattern]]
  - | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
  - | CoverageNoExactSplit QName [Clause]
  - | NotStrictlyPositive QName (Seq OccursWhere)
  - | UnsolvedMetaVariables [Range]
  - | UnsolvedInteractionMetas [Range]
  - | UnsolvedConstraints Constraints
  - | CantGeneralizeOverSorts [MetaId]
  - | AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
  - | OldBuiltin String String
  - | EmptyRewritePragma
  - | IllformedAsClause String
  - | UselessPublic
  - | UselessInline QName
  - | WrongInstanceDeclaration
  - | InstanceWithExplicitArg QName
  - | InstanceNoOutputTypeName Doc
  - | InstanceArgWithExplicitArg Doc
  - | InversionDepthReached QName
  - | GenericWarning Doc
  - | GenericNonFatalError Doc
  - | SafeFlagPostulate Name
  - | SafeFlagPragma [String]
  - | SafeFlagNonTerminating
  - | SafeFlagTerminating
  - | SafeFlagWithoutKFlagPrimEraseEquality
  - | WithoutKFlagPrimEraseEquality
  - | SafeFlagNoPositivityCheck
  - | SafeFlagPolarity
  - | SafeFlagNoUniverseCheck
  - | ParseWarning ParseWarning
  - | LibraryWarning LibWarning
  - | DeprecationWarning String String String
  - | UserWarning String
  - | ModuleDoesntExport QName [ImportedName]
  - | InfectiveImport String ModuleName
  - | CoInfectiveImport String ModuleName
- warningName :: Warning -> WarningName
- data TCWarning = TCWarning {
  - tcWarningRange :: Range
  - tcWarning :: Warning
  - tcWarningPrintedWarning :: Doc
  - tcWarningCached :: Bool
  }
- tcWarningOrigin :: TCWarning -> SrcFile
- equalHeadConstructors :: Warning -> Warning -> Bool
- getPartialDefs :: ReadTCState tcm => tcm [QName]
- data CallInfo = CallInfo {
  - callInfoTarget :: QName
  - callInfoRange :: Range
  - callInfoCall :: Closure Term
  }
- data TerminationError = TerminationError {
  - termErrFunctions :: [QName]
  - termErrCalls :: [CallInfo]
  }
- data SplitError
  - = NotADatatype (Closure Type)
  - | IrrelevantDatatype (Closure Type)
  - | ErasedDatatype (Closure Type)
  - | CoinductiveDatatype (Closure Type)
  - | UnificationStuck {
    - cantSplitConName :: QName
    - cantSplitTel :: Telescope
    - cantSplitConIdx :: Args
    - cantSplitGivenIdx :: Args
    - cantSplitFailures :: [UnificationFailure]
    }
  - | CosplitCatchall
  - | CosplitNoTarget
  - | CosplitNoRecordType (Closure Type)
  - | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
  - | GenericSplitError String
- data NegativeUnification
  - = UnifyConflict Telescope Term Term
  - | UnifyCycle Telescope Int Term
- data UnificationFailure
  - = UnifyIndicesNotVars Telescope Type Term Term Args
  - | UnifyRecursiveEq Telescope Type Int Term
  - | UnifyReflexiveEq Telescope Type Term
- data UnquoteError
  - = BadVisibility String (Arg Term)
  - | ConInsteadOfDef QName String String
  - | DefInsteadOfCon QName String String
  - | NonCanonical String Term
  - | BlockedOnMeta TCState MetaId
  - | UnquotePanic String
- 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 Expr)
  - | WrongIrrelevanceInLambda
  - | WrongQuantityInLambda
  - | HidingMismatch Hiding Hiding
  - | RelevanceMismatch Relevance Relevance
  - | UninstantiatedDotPattern Expr
  - | ForcedConstructorNotInstantiated Pattern
  - | IlltypedPattern Pattern Type
  - | IllformedProjectionPattern Pattern
  - | CannotEliminateWithPattern (NamedArg Pattern) Type
  - | WrongNumberOfConstructorArguments QName Nat Nat
  - | ShouldBeEmpty Type [DeBruijnPattern]
  - | ShouldBeASort Type
  - | ShouldBePi Type
  - | ShouldBePath Type
  - | ShouldBeRecordType Type
  - | ShouldBeRecordPattern DeBruijnPattern
  - | NotAProjectionPattern (NamedArg Pattern)
  - | NotAProperTerm
  - | InvalidTypeSort Sort
  - | InvalidType Term
  - | FunctionTypeInSizeUniv Term
  - | SplitOnIrrelevant (Dom Type)
  - | SplitOnNonVariable Term Type
  - | DefinitionIsIrrelevant QName
  - | VariableIsIrrelevant Name
  - | VariableIsErased Name
  - | UnequalTerms Comparison Term Term Type
  - | UnequalTypes Comparison Type Type
  - | UnequalRelevance Comparison Term Term
  - | UnequalHiding Term Term
  - | UnequalSorts Sort Sort
  - | UnequalBecauseOfUniverseConflict Comparison Term Term
  - | NotLeqSort Sort Sort
  - | MetaCannotDependOn MetaId [Nat] Nat
  - | MetaOccursInItself MetaId
  - | MetaIrrelevantSolution MetaId Term
  - | GenericError String
  - | GenericDocError Doc
  - | BuiltinMustBeConstructor String Expr
  - | NoSuchBuiltinName String
  - | DuplicateBuiltinBinding String Term Term
  - | NoBindingForBuiltin String
  - | NoSuchPrimitiveFunction String
  - | DuplicatePrimitiveBinding String QName QName
  - | ShadowedModule Name [ModuleName]
  - | BuiltinInParameterisedModule String
  - | IllegalLetInTelescope TypedBinding
  - | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
  - | TooManyFields QName [Name] [Name]
  - | DuplicateFields [Name]
  - | DuplicateConstructors [Name]
  - | WithOnFreeVariable Expr Term
  - | UnexpectedWithPatterns [Pattern]
  - | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
  - | FieldOutsideRecord
  - | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
  - | GeneralizeCyclicDependency
  - | GeneralizeUnsolvedMeta
  - | SplitError SplitError
  - | ImpossibleConstructor QName NegativeUnification
  - | TooManyPolarities QName Int
  - | LocalVsImportedModuleClash ModuleName
  - | SolvedButOpenHoles
  - | CyclicModuleDependency [TopLevelModuleName]
  - | FileNotFound TopLevelModuleName [AbsolutePath]
  - | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
  - | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
  - | ModuleNameUnexpected TopLevelModuleName TopLevelModuleName
  - | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
  - | ClashingFileNamesFor ModuleName [AbsolutePath]
  - | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
  - | BothWithAndRHS
  - | AbstractConstructorNotInScope QName
  - | NotInScope [QName]
  - | NoSuchModule QName
  - | AmbiguousName QName (NonemptyList QName)
  - | AmbiguousModule QName (NonemptyList ModuleName)
  - | ClashingDefinition QName QName
  - | ClashingModule ModuleName ModuleName
  - | ClashingImport Name QName
  - | ClashingModuleImport Name ModuleName
  - | PatternShadowsConstructor Name QName
  - | DuplicateImports QName [ImportedName]
  - | InvalidPattern Pattern
  - | RepeatedVariablesInPattern [Name]
  - | GeneralizeNotSupportedHere QName
  - | MultipleFixityDecls [(Name, [Fixity'])]
  - | MultiplePolarityPragmas [Name]
  - | NotAModuleExpr Expr
  - | NotAnExpression Expr
  - | NotAValidLetBinding NiceDeclaration
  - | NotValidBeforeField NiceDeclaration
  - | NothingAppliedToHiddenArg Expr
  - | NothingAppliedToInstanceArg Expr
  - | BadArgumentsToPatternSynonym AmbiguousQName
  - | TooFewArgumentsToPatternSynonym AmbiguousQName
  - | CannotResolveAmbiguousPatternSynonym (NonemptyList (QName, PatternSynDefn))
  - | UnusedVariableInPatternSynonym
  - | NoParseForApplication [Expr]
  - | AmbiguousParseForApplication [Expr] [Expr]
  - | NoParseForLHS LHSOrPatSyn Pattern
  - | AmbiguousParseForLHS LHSOrPatSyn Pattern [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
- data LHSOrPatSyn
  - = IsLHS
  - | IsPatSyn
- data TCErr
  - = TypeError {
    - tcErrState :: TCState
    - tcErrClosErr :: Closure TypeError
    }
  - | Exception Range Doc
  - | IOException TCState Range IOException
  - | PatternErr
- class (Functor m, Applicative m, Monad m) => HasOptions m where
  - pragmaOptions :: m PragmaOptions
  - commandLineOptions :: m CommandLineOptions
- sizedTypesOption :: HasOptions m => m Bool
- guardednessOption :: HasOptions m => m Bool
- withoutKOption :: HasOptions m => m Bool
- data ReduceEnv = ReduceEnv {
  - redEnv :: TCEnv
  - redSt :: TCState
  }
- mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
- mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- reduceEnv :: Lens' TCEnv ReduceEnv
- reduceSt :: Lens' TCState ReduceEnv
- newtype ReduceM a = ReduceM {
  - unReduceM :: ReduceEnv -> a
  }
- onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
- apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
- bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
- runReduceM :: ReduceM a -> TCM a
- runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
- useR :: ReadTCState m => Lens' a TCState -> m a
- askR :: ReduceM ReduceEnv
- localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where
  - liftReduce :: ReduceM a -> m a
- class Monad m => MonadTCEnv m where
  - askTC :: m TCEnv
  - localTC :: (TCEnv -> TCEnv) -> m a -> m a
- asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
- viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a
- locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b
- class Monad m => MonadTCState m where
  - getTC :: m TCState
  - putTC :: TCState -> m ()
  - modifyTC :: (TCState -> TCState) -> m ()
- getsTC :: MonadTCState m => (TCState -> a) -> m a
- modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
- useTC :: MonadTCState m => Lens' a TCState -> m a
- setTCLens :: MonadTCState m => Lens' a TCState -> a -> m ()
- modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m ()
- modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m ()
- locallyTCState :: MonadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b
- newtype TCMT m a = TCM {
  - unTCM :: IORef TCState -> TCEnv -> m a
  }
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where
  - liftTCM :: TCM a -> tcm a
- type IM = TCMT (InputT IO)
- runIM :: IM a -> TCM a
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- finally_ :: TCM a -> TCM b -> TCM a
- mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
- pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
- returnTCMT :: MonadIO m => a -> TCMT m a
- bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
- thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
- fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
- apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
- patternViolation :: TCM a
- internalError :: MonadTCM tcm => String -> tcm a
- genericError :: MonadTCM tcm => String -> tcm a
- genericDocError :: MonadTCM tcm => Doc -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
- runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
- runTCMTop :: TCM a -> IO (Either TCErr a)
- runTCMTop' :: MonadIO m => TCMT m a -> m a
- runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
- forkTCM :: TCM a -> TCM ()
- extendedLambdaName :: String
- isExtendedLambdaName :: QName -> Bool
- absurdLambdaName :: String
- isAbsurdLambdaName :: QName -> Bool
- generalizedFieldName :: String
- getGeneralizedFieldName :: QName -> Maybe String

# Type checking state

data TCState Source #

Constructors

TCSt |

Fields

- stPreScopeState :: !PreScopeState

  The state which is frozen after scope checking.

- stPostScopeState :: !PostScopeState

  The state which is modified after scope checking.

- stPersistentState :: !PersistentTCState

  State which is forever, like a diamond.

Instances

Show TCState Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCState -> ShowS Source # show :: TCState -> String Source # showList :: [TCState] -> ShowS Source #
LensPersistentVerbosity TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: TCState -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCState -> TCState Source #
LensIncludePaths TCState Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: TCState -> [FilePath] Source #

setIncludePaths :: [FilePath] -> TCState -> TCState Source #

mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState Source #

getAbsoluteIncludePaths :: TCState -> [AbsolutePath] Source #

setAbsoluteIncludePaths :: [AbsolutePath] -> TCState -> TCState Source #

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState Source #

LensSafeMode TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: TCState -> SafeMode Source # setSafeMode :: SafeMode -> TCState -> TCState Source # mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState Source #
LensCommandLineOptions TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: TCState -> CommandLineOptions Source # setCommandLineOptions :: CommandLineOptions -> TCState -> TCState Source # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState Source #
LensVerbosity TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: TCState -> Verbosity Source # setVerbosity :: Verbosity -> TCState -> TCState Source # mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState Source #
LensPragmaOptions TCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: TCState -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> TCState -> TCState Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState Source # lensPragmaOptions :: Lens' PragmaOptions TCState Source #

class Monad m => ReadTCState m where Source #

Methods

getTCState :: m TCState Source #

withTCState :: (TCState -> TCState) -> m a -> m a Source #

Instances

ReadTCState ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ReduceM TCState Source # withTCState :: (TCState -> TCState) -> ReduceM a -> ReduceM a Source #
ReadTCState TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getTCState :: TerM TCState Source # withTCState :: (TCState -> TCState) -> TerM a -> TerM a Source #
ReadTCState m => ReadTCState (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: MaybeT m TCState Source # withTCState :: (TCState -> TCState) -> MaybeT m a -> MaybeT m a Source #
ReadTCState m => ReadTCState (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ListT m TCState Source # withTCState :: (TCState -> TCState) -> ListT m a -> ListT m a Source #
MonadIO m => ReadTCState (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: TCMT m TCState Source # withTCState :: (TCState -> TCState) -> TCMT m a -> TCMT m a Source #
ReadTCState m => ReadTCState (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getTCState :: NamesT m TCState Source # withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a Source #
ReadTCState m => ReadTCState (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ExceptT err m TCState Source # withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #
ReadTCState m => ReadTCState (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ReaderT r m TCState Source # withTCState :: (TCState -> TCState) -> ReaderT r m a -> ReaderT r m a Source #
ReadTCState m => ReadTCState (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: StateT s m TCState Source # withTCState :: (TCState -> TCState) -> StateT s m a -> StateT s m a Source #
(Monoid w, ReadTCState m) => ReadTCState (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: WriterT w m TCState Source # withTCState :: (TCState -> TCState) -> WriterT w m a -> WriterT w m a Source #

data PreScopeState Source #

Constructors

PreScopeState |

Fields

- stPreTokens :: !CompressedFile

  Highlighting info for tokens (but not those tokens for which highlighting exists in `stSyntaxInfo`).

- stPreImports :: !Signature

  Imported declared identifiers. Those most not be serialized!

- stPreImportedModules :: !(Set ModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns

  Pattern synonyms of the current file. Serialized.

- stPrePatternSynImports :: !PatternSynDefns

  Imported pattern synonyms. Must not be serialized!

- stPreGeneralizedVars :: !(Maybe (Set QName))

  Collected generalizable variables; used during scope checking of terms

- stPrePragmaOptions :: !PragmaOptions

  Options applying to the current file. `OPTIONS` pragmas only affect this field.

- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms

  Display forms added by someone else to imported identifiers

- stPreImportedInstanceDefs :: !InstanceTable
- stPreForeignCode :: !(Map BackendName [ForeignCode])

  `{-# FOREIGN #-}` code that should be included in the compiled output. Does not include code for imported modules.

- stPreFreshInteractionId :: !InteractionId
- stPreImportedUserWarnings :: !(Map QName String)

  Imported `UserWarning`s, not to be stored in the `Interface`

- stPreLocalUserWarnings :: !(Map QName String)

  Locally defined `UserWarning`s, to be stored in the `Interface`

type DisambiguatedNames = IntMap QName Source #

data PostScopeState Source #

Constructors

PostScopeState |

Fields

- stPostSyntaxInfo :: !CompressedFile

  Highlighting info.

- stPostDisambiguatedNames :: !DisambiguatedNames

  Disambiguation carried out by the type checker. Maps position of first name character to disambiguated ``QName`` for each ``AmbiguousQName`` already passed by the type checker.

- stPostMetaStore :: !MetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool

  Dirty when a constraint is added, used to prevent pointer update. Currently unused.

- stPostOccursCheckDefs :: !(Set QName)

  Definitions to be considered during occurs check. Initialized to the current mutual block before the check. During occurs check, we remove definitions from this set as soon we have checked them.

- stPostSignature :: !Signature

  Declared identifiers of the current file. These will be serialized after successful type checking.

- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)

  For each module remember the checkpoint corresponding to the orignal context of the module parameters.

- stPostImportsDisplayForms :: !DisplayForms

  Display forms we add for imported identifiers

- stPostCurrentModule :: !(Maybe ModuleName)

  The current module is available after it has been type checked.

- stPostInstanceDefs :: !TempInstanceTable
- stPostConcreteNames :: !(Map Name [Name])

  Map keeping track of concrete names assigned to each abstract name (can be more than one name in case the first one is shadowed)

- stPostShadowingNames :: !(Map Name [Name])

  Map keeping track of which names could maybe be shadowed by another name

- stPostStatistics :: !Statistics

  Counters to collect various statistics about meta variables etc. Only for current file.

- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostAreWeCaching :: !Bool
- stPostConsideringInstance :: !Bool

data MutualBlock Source #

A mutual block of names in the signature.

Constructors

MutualBlock |

Fields

- mutualInfo :: MutualInfo

  The original info of the mutual block.

- mutualNames :: Set QName

Instances

Eq MutualBlock Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MutualBlock -> MutualBlock -> Bool Source # (/=) :: MutualBlock -> MutualBlock -> Bool Source #
Show MutualBlock Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MutualBlock -> ShowS Source # show :: MutualBlock -> String Source # showList :: [MutualBlock] -> ShowS Source #
Null MutualBlock Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: MutualBlock Source # null :: MutualBlock -> Bool Source #

data PersistentTCState Source #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt |

Fields

- stDecodedModules :: DecodedModules
- stPersistentOptions :: CommandLineOptions
- stInteractionOutputCallback :: InteractionOutputCallback

  Callback function to call when there is a response to give to the interactive frontend. See the documentation of `InteractionOutputCallback`.

- stBenchmark :: !Benchmark

  Structure to track how much CPU time was spent on which Agda phase. Needs to be a strict field to avoid space leaks!

- stAccumStatistics :: !Statistics

  Should be strict field.

- stLoadedFileCache :: !(Maybe LoadedFileCache)

  Cached typechecking state from the last loaded file. Should be Nothing when checking imports.

- stPersistBackends :: [Backend]

  Current backends with their options

Instances

LensPersistentVerbosity PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PersistentTCState -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PersistentTCState -> PersistentTCState Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PersistentTCState -> PersistentTCState Source #
LensIncludePaths PersistentTCState Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: PersistentTCState -> [FilePath] Source #

setIncludePaths :: [FilePath] -> PersistentTCState -> PersistentTCState Source #

mapIncludePaths :: ([FilePath] -> [FilePath]) -> PersistentTCState -> PersistentTCState Source #

getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath] Source #

setAbsoluteIncludePaths :: [AbsolutePath] -> PersistentTCState -> PersistentTCState Source #

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> PersistentTCState -> PersistentTCState Source #

LensSafeMode PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PersistentTCState -> SafeMode Source # setSafeMode :: SafeMode -> PersistentTCState -> PersistentTCState Source # mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState Source #
LensCommandLineOptions PersistentTCState Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: PersistentTCState -> CommandLineOptions Source # setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState Source # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> PersistentTCState -> PersistentTCState Source #

data LoadedFileCache Source #

Constructors

LoadedFileCache |

Fields

- lfcCached :: !CachedTypeCheckLog
- lfcCurrent :: !CurrentTypeCheckLog

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

Like `CachedTypeCheckLog`, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

data TypeCheckAction Source #

A complete log for a module will look like this:

- `Pragmas`
- `EnterSection`, entering the main module.
- 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
- `LeaveSection`, leaving the main module.

Constructors

EnterSection !ModuleInfo !ModuleName !Telescope |
LeaveSection !ModuleName |
Decl !Declaration | Never a Section or ScopeDecl
Pragmas !PragmaOptions |

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

initPostScopeState :: PostScopeState Source #

initState :: TCState Source #

# st-prefixed lenses

stTokens :: Lens' CompressedFile TCState Source #

stImports :: Lens' Signature TCState Source #

stImportedModules :: Lens' (Set ModuleName) TCState Source #

stModuleToSource :: Lens' ModuleToSource TCState Source #

stVisitedModules :: Lens' VisitedModules TCState Source #

stScope :: Lens' ScopeInfo TCState Source #

stPatternSyns :: Lens' PatternSynDefns TCState Source #

stPatternSynImports :: Lens' PatternSynDefns TCState Source #

stGeneralizedVars :: Lens' (Maybe (Set QName)) TCState Source #

stPragmaOptions :: Lens' PragmaOptions TCState Source #

stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState Source #

stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState Source #

stFreshInteractionId :: Lens' InteractionId TCState Source #

stImportedUserWarnings :: Lens' (Map QName String) TCState Source #

stLocalUserWarnings :: Lens' (Map QName String) TCState Source #

getUserWarnings :: MonadTCState m => m (Map QName String) Source #

stBackends :: Lens' [Backend] TCState Source #

stFreshNameId :: Lens' NameId TCState Source #

stSyntaxInfo :: Lens' CompressedFile TCState Source #

stDisambiguatedNames :: Lens' DisambiguatedNames TCState Source #

stMetaStore :: Lens' MetaStore TCState Source #

stInteractionPoints :: Lens' InteractionPoints TCState Source #

stAwakeConstraints :: Lens' Constraints TCState Source #

stSleepingConstraints :: Lens' Constraints TCState Source #

stDirty :: Lens' Bool TCState Source #

stOccursCheckDefs :: Lens' (Set QName) TCState Source #

stSignature :: Lens' Signature TCState Source #

stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState Source #

stImportsDisplayForms :: Lens' DisplayForms TCState Source #

stImportedDisplayForms :: Lens' DisplayForms TCState Source #

stCurrentModule :: Lens' (Maybe ModuleName) TCState Source #

stImportedInstanceDefs :: Lens' InstanceTable TCState Source #

stInstanceDefs :: Lens' TempInstanceTable TCState Source #

stConcreteNames :: Lens' (Map Name [Name]) TCState Source #

stShadowingNames :: Lens' (Map Name [Name]) TCState Source #

stStatistics :: Lens' Statistics TCState Source #

stTCWarnings :: Lens' [TCWarning] TCState Source #

stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState Source #

stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState Source #

stFreshMetaId :: Lens' MetaId TCState Source #

stFreshMutualId :: Lens' MutualId TCState Source #

stFreshProblemId :: Lens' ProblemId TCState Source #

stFreshCheckpointId :: Lens' CheckpointId TCState Source #

stFreshInt :: Lens' Int TCState Source #

stAreWeCaching :: Lens' Bool TCState Source #

stConsideringInstance :: Lens' Bool TCState Source #

stBuiltinThings :: TCState -> BuiltinThings PrimFun Source #

# Fresh things

class Enum i => HasFresh i where Source #

Minimal complete definition

freshLens

Methods

freshLens :: Lens' i TCState Source #

nextFresh' :: i -> i Source #

Instances

HasFresh Int Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' Int TCState Source # nextFresh' :: Int -> Int Source #
HasFresh InteractionId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' InteractionId TCState Source # nextFresh' :: InteractionId -> InteractionId Source #
HasFresh MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState Source # nextFresh' :: MetaId -> MetaId Source #
HasFresh NameId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' NameId TCState Source # nextFresh' :: NameId -> NameId Source #
HasFresh MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MutualId TCState Source # nextFresh' :: MutualId -> MutualId Source #
HasFresh CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' CheckpointId TCState Source # nextFresh' :: CheckpointId -> CheckpointId Source #
HasFresh ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' ProblemId TCState Source # nextFresh' :: ProblemId -> ProblemId Source #

nextFresh :: HasFresh i => TCState -> (i, TCState) Source #

fresh :: (HasFresh i, MonadTCState m) => m i Source #

newtype ProblemId Source #

Constructors

ProblemId Nat |

Instances

Enum ProblemId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

succ :: ProblemId -> ProblemId Source #

pred :: ProblemId -> ProblemId Source #

toEnum :: Int -> ProblemId Source #

fromEnum :: ProblemId -> Int Source #

enumFrom :: ProblemId -> [ProblemId] Source #

enumFromThen :: ProblemId -> ProblemId -> [ProblemId] Source #

enumFromTo :: ProblemId -> ProblemId -> [ProblemId] Source #

enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] Source #

Eq ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ProblemId -> ProblemId -> Bool Source # (/=) :: ProblemId -> ProblemId -> Bool Source #
Integral ProblemId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

quot :: ProblemId -> ProblemId -> ProblemId Source #

rem :: ProblemId -> ProblemId -> ProblemId Source #

div :: ProblemId -> ProblemId -> ProblemId Source #

mod :: ProblemId -> ProblemId -> ProblemId Source #

quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source #

divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source #

toInteger :: ProblemId -> Integer Source #

Data ProblemId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId Source #

toConstr :: ProblemId -> Constr Source #

dataTypeOf :: ProblemId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) Source #

gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId Source #

Num ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: ProblemId -> ProblemId -> ProblemId Source # (-) :: ProblemId -> ProblemId -> ProblemId Source # (*) :: ProblemId -> ProblemId -> ProblemId Source # negate :: ProblemId -> ProblemId Source # abs :: ProblemId -> ProblemId Source # signum :: ProblemId -> ProblemId Source # fromInteger :: Integer -> ProblemId Source #
Ord ProblemId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: ProblemId -> ProblemId -> Ordering Source #

(<) :: ProblemId -> ProblemId -> Bool Source #

(<=) :: ProblemId -> ProblemId -> Bool Source #

(>) :: ProblemId -> ProblemId -> Bool Source #

(>=) :: ProblemId -> ProblemId -> Bool Source #

max :: ProblemId -> ProblemId -> ProblemId Source #

min :: ProblemId -> ProblemId -> ProblemId Source #

Real ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toRational :: ProblemId -> Rational Source #
Show ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProblemId -> ShowS Source # show :: ProblemId -> String Source # showList :: [ProblemId] -> ShowS Source #
Pretty ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
HasFresh ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' ProblemId TCState Source # nextFresh' :: ProblemId -> ProblemId Source #
PrettyTCM ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemId -> TCM Doc Source #

newtype CheckpointId Source #

Constructors

CheckpointId Int |

Instances

Enum CheckpointId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

succ :: CheckpointId -> CheckpointId Source #

pred :: CheckpointId -> CheckpointId Source #

toEnum :: Int -> CheckpointId Source #

fromEnum :: CheckpointId -> Int Source #

enumFrom :: CheckpointId -> [CheckpointId] Source #

enumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId] Source #

enumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId] Source #

enumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId] Source #

Eq CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CheckpointId -> CheckpointId -> Bool Source # (/=) :: CheckpointId -> CheckpointId -> Bool Source #
Integral CheckpointId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

quot :: CheckpointId -> CheckpointId -> CheckpointId Source #

rem :: CheckpointId -> CheckpointId -> CheckpointId Source #

div :: CheckpointId -> CheckpointId -> CheckpointId Source #

mod :: CheckpointId -> CheckpointId -> CheckpointId Source #

quotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId) Source #

divMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId) Source #

toInteger :: CheckpointId -> Integer Source #

Data CheckpointId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CheckpointId -> c CheckpointId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CheckpointId Source #

toConstr :: CheckpointId -> Constr Source #

dataTypeOf :: CheckpointId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CheckpointId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CheckpointId) Source #

gmapT :: (forall b. Data b => b -> b) -> CheckpointId -> CheckpointId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CheckpointId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CheckpointId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId Source #

Num CheckpointId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(+) :: CheckpointId -> CheckpointId -> CheckpointId Source #

(-) :: CheckpointId -> CheckpointId -> CheckpointId Source #

(*) :: CheckpointId -> CheckpointId -> CheckpointId Source #

negate :: CheckpointId -> CheckpointId Source #

abs :: CheckpointId -> CheckpointId Source #

signum :: CheckpointId -> CheckpointId Source #

fromInteger :: Integer -> CheckpointId Source #

Ord CheckpointId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: CheckpointId -> CheckpointId -> Ordering Source #

(<) :: CheckpointId -> CheckpointId -> Bool Source #

(<=) :: CheckpointId -> CheckpointId -> Bool Source #

(>) :: CheckpointId -> CheckpointId -> Bool Source #

(>=) :: CheckpointId -> CheckpointId -> Bool Source #

max :: CheckpointId -> CheckpointId -> CheckpointId Source #

min :: CheckpointId -> CheckpointId -> CheckpointId Source #

Real CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toRational :: CheckpointId -> Rational Source #
Show CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CheckpointId -> ShowS Source # show :: CheckpointId -> String Source # showList :: [CheckpointId] -> ShowS Source #
Pretty CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CheckpointId -> Doc Source # prettyPrec :: Int -> CheckpointId -> Doc Source # prettyList :: [CheckpointId] -> Doc Source #
HasFresh CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' CheckpointId TCState Source # nextFresh' :: CheckpointId -> CheckpointId Source #
EmbPrj CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Int32 Source # icod_ :: CheckpointId -> S Int32 Source # value :: Int32 -> R CheckpointId Source #
PrettyTCM CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: CheckpointId -> TCM Doc Source #

freshName :: MonadTCState m => Range -> String -> m Name Source #

freshNoName :: MonadTCState m => Range -> m Name Source #

freshNoName_ :: MonadTCState m => m Name Source #

freshRecordName :: MonadTCState m => m Name Source #

class FreshName a where Source #

Create a fresh name from `a`.

Methods

freshName_ :: MonadTCState m => a -> m Name Source #

Instances

FreshName () Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => () -> m Name Source #
FreshName String Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => String -> m Name Source #
FreshName Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => Range -> m Name Source #
FreshName (Range, String) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => (Range, String) -> m Name Source #

## Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

Maps top-level module names to the corresponding source file names.

type SourceToModule = Map AbsolutePath TopLevelModuleName Source #

Maps source file names to the corresponding top-level module names.

sourceToModule :: TCM SourceToModule Source #

Creates a `SourceToModule` map based on `stModuleToSource`.

O(n log n).

For a single reverse lookup in `stModuleToSource`, rather use `lookupModuleFromSourse`.

lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName) Source #

Lookup an `AbsolutePath` in `sourceToModule`.

O(n).

## Interface

data ModuleInfo Source #

Constructors

ModuleInfo |

Fields

- miInterface :: Interface
- miWarnings :: Bool

  `True` if warnings were encountered when the module was type checked.

- miPrimitive :: Bool

  `True` if the module is a primitive module, which should always be importable.

type VisitedModules = Map TopLevelModuleName ModuleInfo Source #

type DecodedModules = Map TopLevelModuleName Interface Source #

data ForeignCode Source #

Constructors

ForeignCode Range String |

Instances

Show ForeignCode Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ForeignCode -> ShowS Source # show :: ForeignCode -> String Source # showList :: [ForeignCode] -> ShowS Source #
EmbPrj ForeignCode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Int32 Source # icod_ :: ForeignCode -> S Int32 Source # value :: Int32 -> R ForeignCode Source #

data Interface Source #

Constructors

Interface |

Fields

- iSourceHash :: Hash

  Hash of the source code.

- iSource :: Text

  The source code. The source code is stored so that the HTML and LaTeX backends can generate their output without having to re-read the (possibly out of date) source code.

- iFileType :: FileType

  Source file type, determined from the file extension

- iImportedModules :: [(ModuleName, Hash)]

  Imported modules and their hashes.

- iModuleName :: ModuleName

  Module name of this interface.

- iScope :: Map ModuleName Scope

  Scope defined by this module.

  Andreas, AIM XX: Too avoid duplicate serialization, this field is not serialized, so if you deserialize an interface, `iScope` will be empty. But `constructIScope` constructs `iScope` from `iInsideScope`.

- iInsideScope :: ScopeInfo

  Scope after we loaded this interface. Used in `AtTopLevel` and `interactionLoop`.

- iSignature :: Signature
- iDisplayForms :: DisplayForms

  Display forms added for imported identifiers.

- iUserWarnings :: Map QName String

  User warnings for imported identifiers

- iBuiltin :: BuiltinThings (String, QName)
- iForeignCode :: Map BackendName [ForeignCode]
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]

  Pragma options set in the file.

- iOptionsUsed :: PragmaOptions

  Options/features used when checking the file (can be different from options set directly in the file).

- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]

Instances

Show Interface Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Interface -> ShowS Source # show :: Interface -> String Source # showList :: [Interface] -> ShowS Source #
Pretty Interface Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Interface -> Doc Source # prettyPrec :: Int -> Interface -> Doc Source # prettyList :: [Interface] -> Doc Source #
EmbPrj Interface Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Int32 Source # icod_ :: Interface -> S Int32 Source # value :: Int32 -> R Interface Source #
InstantiateFull Interface Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Interface -> ReduceM Interface Source #

iFullHash :: Interface -> Hash Source #

Combines the source hash and the (full) hashes of the imported modules.

## Closure

data Closure a Source #

Constructors

Closure |

Fields

- clSignature :: Signature
- clEnv :: TCEnv
- clScope :: ScopeInfo
- clModuleCheckpoints :: Map ModuleName CheckpointId
- clValue :: a

Instances

Functor Closure Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Closure a -> Closure b Source # (<$) :: a -> Closure b -> Closure a Source #
Foldable Closure Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Closure m -> m Source #

foldMap :: Monoid m => (a -> m) -> Closure a -> m Source #

foldr :: (a -> b -> b) -> b -> Closure a -> b Source #

foldr' :: (a -> b -> b) -> b -> Closure a -> b Source #

foldl :: (b -> a -> b) -> b -> Closure a -> b Source #

foldl' :: (b -> a -> b) -> b -> Closure a -> b Source #

foldr1 :: (a -> a -> a) -> Closure a -> a Source #

foldl1 :: (a -> a -> a) -> Closure a -> a Source #

toList :: Closure a -> [a] Source #

null :: Closure a -> Bool Source #

length :: Closure a -> Int Source #

elem :: Eq a => a -> Closure a -> Bool Source #

maximum :: Ord a => Closure a -> a Source #

minimum :: Ord a => Closure a -> a Source #

sum :: Num a => Closure a -> a Source #

product :: Num a => Closure a -> a Source #

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #
Data a => Data (Closure a) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Closure a) Source #

toConstr :: Closure a -> Constr Source #

dataTypeOf :: Closure a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Closure a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Closure a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Closure a -> Closure a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Closure a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Closure a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) Source #

Show a => Show (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Closure a -> ShowS Source # show :: Closure a -> String Source # showList :: [Closure a] -> ShowS Source #
KillRange a => KillRange (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Closure a) Source #
HasRange a => HasRange (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Closure a -> Range Source #
PrettyTCM a => PrettyTCM (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Closure a -> TCM Doc Source #
MentionsMeta a => MentionsMeta (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Closure a -> Bool Source #
InstantiateFull a => InstantiateFull (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Closure a -> ReduceM (Closure a) Source #
Normalise a => Normalise (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Closure a -> ReduceM (Closure a) Source #
Simplify a => Simplify (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Closure a -> ReduceM (Closure a) Source #
Reduce a => Reduce (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Closure a -> ReduceM (Closure a) Source # reduceB' :: Closure a -> ReduceM (Blocked (Closure a)) Source #
Instantiate a => Instantiate (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Closure a -> ReduceM (Closure a) Source #

buildClosure :: a -> TCM (Closure a) Source #

## Constraints

type Constraints = [ProblemConstraint] Source #

data ProblemConstraint Source #

Constructors

PConstr |

Fields

- constraintProblems :: Set ProblemId
- theConstraint :: Closure Constraint

Instances

Data ProblemConstraint Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemConstraint -> c ProblemConstraint Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemConstraint Source #

toConstr :: ProblemConstraint -> Constr Source #

dataTypeOf :: ProblemConstraint -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemConstraint) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemConstraint) Source #

gmapT :: (forall b. Data b => b -> b) -> ProblemConstraint -> ProblemConstraint Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProblemConstraint -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemConstraint -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint Source #

Show ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProblemConstraint -> ShowS Source # show :: ProblemConstraint -> String Source # showList :: [ProblemConstraint] -> ShowS Source #
HasRange ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range Source #
PrettyTCM ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemConstraint -> TCM Doc Source #
MentionsMeta ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> ProblemConstraint -> Bool Source #
InstantiateFull ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
Normalise ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
Simplify ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #

data Constraint Source #

Constructors

ValueCmp Comparison Type Term Term |
ValueCmpOnFace Comparison Term Type Term Term |
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim] |
TypeCmp Comparison Type Type |
TelCmp Type Type Comparison Telescope Telescope | the two types are for the error message only
SortCmp Comparison Sort Sort |
LevelCmp Comparison Level Level |
HasBiggerSort Sort |
HasPTSRule Sort (Abs Sort) |
UnBlock MetaId |
Guarded Constraint ProblemId |
IsEmpty Range Type | The range is the one of the absurd pattern.
CheckSizeLtSat Term | Check that the `Term` is either not a SIZELT or a non-empty SIZELT.
FindInstance MetaId (Maybe MetaId) (Maybe [Candidate]) | the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)
CheckFunDef Delayed DefInfo QName [Clause] |
UnquoteTactic (Maybe MetaId) Term Term Type | First argument is computation and the others are hole and goal type

Instances

Eq Constraint Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Constraint -> Constraint -> Bool Source # (/=) :: Constraint -> Constraint -> Bool Source #
Data Constraint Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint Source #

toConstr :: Constraint -> Constr Source #

dataTypeOf :: Constraint -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint) Source #

gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint Source #

Show Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Constraint -> ShowS Source # show :: Constraint -> String Source # showList :: [Constraint] -> ShowS Source #
HasRange Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range Source #
Free Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Constraint -> FreeM c Source #
TermLike Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source # foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #
PrettyTCM Constraint Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Constraint -> TCM Doc Source #
MentionsMeta Constraint Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Constraint -> Bool Source #
InstantiateFull Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Constraint -> ReduceM Constraint Source #
Normalise Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Constraint -> ReduceM Constraint Source #
Simplify Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Constraint -> ReduceM Constraint Source #
Reduce Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Constraint -> ReduceM Constraint Source # reduceB' :: Constraint -> ReduceM (Blocked Constraint) Source #
Instantiate Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Constraint -> ReduceM Constraint Source #
Subst Term Constraint Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint Source #
Reify Constraint (OutputConstraint Expr Expr) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source #

data Comparison Source #

Constructors

CmpEq |
CmpLeq |

Instances

Eq Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Comparison -> Comparison -> Bool Source # (/=) :: Comparison -> Comparison -> Bool Source #
Data Comparison Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison Source #

toConstr :: Comparison -> Constr Source #

dataTypeOf :: Comparison -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) Source #

gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison Source #

Show Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS Source # show :: Comparison -> String Source # showList :: [Comparison] -> ShowS Source #
Pretty Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source #
PrettyTCM Comparison Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Comparison -> TCM Doc Source #

data CompareDirection Source #

An extension of `Comparison` to `>=`.

Constructors

DirEq |
DirLeq |
DirGeq |

Instances

Eq CompareDirection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompareDirection -> CompareDirection -> Bool Source # (/=) :: CompareDirection -> CompareDirection -> Bool Source #
Show CompareDirection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompareDirection -> ShowS Source # show :: CompareDirection -> String Source # showList :: [CompareDirection] -> ShowS Source #
Pretty CompareDirection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareDirection -> Doc Source # prettyPrec :: Int -> CompareDirection -> Doc Source # prettyList :: [CompareDirection] -> Doc Source #

fromCmp :: Comparison -> CompareDirection Source #

Embed `Comparison` into `CompareDirection`.

flipCmp :: CompareDirection -> CompareDirection Source #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source #

Turn a `Comparison` function into a `CompareDirection` function.

Property: `dirToCmp f (fromCmp cmp) = f cmp`

# Open things

data Open a Source #

A thing tagged with the context it came from.

Constructors

OpenThing |

Fields

- openThingCheckpoint :: CheckpointId
- openThing :: a

Instances

Functor Open Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Open a -> Open b Source # (<$) :: a -> Open b -> Open a Source #
Foldable Open Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Open m -> m Source #

foldMap :: Monoid m => (a -> m) -> Open a -> m Source #

foldr :: (a -> b -> b) -> b -> Open a -> b Source #

foldr' :: (a -> b -> b) -> b -> Open a -> b Source #

foldl :: (b -> a -> b) -> b -> Open a -> b Source #

foldl' :: (b -> a -> b) -> b -> Open a -> b Source #

foldr1 :: (a -> a -> a) -> Open a -> a Source #

foldl1 :: (a -> a -> a) -> Open a -> a Source #

toList :: Open a -> [a] Source #

null :: Open a -> Bool Source #

length :: Open a -> Int Source #

elem :: Eq a => a -> Open a -> Bool Source #

maximum :: Ord a => Open a -> a Source #

minimum :: Ord a => Open a -> a Source #

sum :: Num a => Open a -> a Source #

product :: Num a => Open a -> a Source #

Traversable Open Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverse :: Applicative f => (a -> f b) -> Open a -> f (Open b) Source # sequenceA :: Applicative f => Open (f a) -> f (Open a) Source # mapM :: Monad m => (a -> m b) -> Open a -> m (Open b) Source # sequence :: Monad m => Open (m a) -> m (Open a) Source #
Decoration Open Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) Source # distributeF :: Functor m => Open (m a) -> m (Open a) Source #
Data a => Data (Open a) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Open a) Source #

toConstr :: Open a -> Constr Source #

dataTypeOf :: Open a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Open a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Open a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Open a -> Open a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Open a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Open a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) Source #

Show a => Show (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Open a -> ShowS Source # show :: Open a -> String Source # showList :: [Open a] -> ShowS Source #
KillRange a => KillRange (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) Source #
EmbPrj a => EmbPrj (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Int32 Source # icod_ :: Open a -> S Int32 Source # value :: Int32 -> R (Open a) Source #
NamesIn a => NamesIn (Open a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Open a -> Set QName Source #
InstantiateFull a => InstantiateFull (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Open a -> ReduceM (Open a) Source #

# Judgements

data Judgement a Source #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType |

Fields

- jMetaId :: a
- jMetaType :: Type

IsSort |

Fields

- jMetaId :: a
- jMetaType :: Type

Instances

Show a => Show (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Judgement a -> ShowS Source # show :: Judgement a -> String Source # showList :: [Judgement a] -> ShowS Source #
PrettyTCM a => PrettyTCM (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Judgement a -> TCM Doc Source #

## Generalizable variables

data DoGeneralize Source #

Constructors

YesGeneralize |
NoGeneralize |

Instances

Eq DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: DoGeneralize -> DoGeneralize -> Bool Source # (/=) :: DoGeneralize -> DoGeneralize -> Bool Source #
Data DoGeneralize Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoGeneralize -> c DoGeneralize Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoGeneralize Source #

toConstr :: DoGeneralize -> Constr Source #

dataTypeOf :: DoGeneralize -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoGeneralize) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoGeneralize) Source #

gmapT :: (forall b. Data b => b -> b) -> DoGeneralize -> DoGeneralize Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DoGeneralize -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DoGeneralize -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize Source #

Ord DoGeneralize Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: DoGeneralize -> DoGeneralize -> Ordering Source #

(<) :: DoGeneralize -> DoGeneralize -> Bool Source #

(<=) :: DoGeneralize -> DoGeneralize -> Bool Source #

(>) :: DoGeneralize -> DoGeneralize -> Bool Source #

(>=) :: DoGeneralize -> DoGeneralize -> Bool Source #

max :: DoGeneralize -> DoGeneralize -> DoGeneralize Source #

min :: DoGeneralize -> DoGeneralize -> DoGeneralize Source #

Show DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DoGeneralize -> ShowS Source # show :: DoGeneralize -> String Source # showList :: [DoGeneralize] -> ShowS Source #
KillRange DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DoGeneralize Source #
EmbPrj DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DoGeneralize -> S Int32 Source # icod_ :: DoGeneralize -> S Int32 Source # value :: Int32 -> R DoGeneralize Source #

data GeneralizedValue Source #

The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.

Constructors

GeneralizedValue |

Fields

- genvalCheckpoint :: CheckpointId
- genvalTerm :: Term
- genvalType :: Type

Instances

Data GeneralizedValue Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizedValue -> c GeneralizedValue Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizedValue Source #

toConstr :: GeneralizedValue -> Constr Source #

dataTypeOf :: GeneralizedValue -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizedValue) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizedValue) Source #

gmapT :: (forall b. Data b => b -> b) -> GeneralizedValue -> GeneralizedValue Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> GeneralizedValue -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizedValue -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue Source #

Show GeneralizedValue Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> GeneralizedValue -> ShowS Source # show :: GeneralizedValue -> String Source # showList :: [GeneralizedValue] -> ShowS Source #

## Meta variables

data MetaVariable Source #

Constructors

MetaVar |

Fields

- mvInfo :: MetaInfo
- mvPriority :: MetaPriority

  some metavariables are more eager to be instantiated

- mvPermutation :: Permutation

  a metavariable doesn't have to depend on all variables in the context, this "permutation" will throw away the ones it does not depend on

- mvJudgement :: Judgement MetaId
- mvInstantiation :: MetaInstantiation
- mvListeners :: Set Listener

  meta variables scheduled for eta-expansion but blocked by this one

- mvFrozen :: Frozen

  are we past the point where we can instantiate this meta variable?

Instances

SetRange MetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable Source #
HasRange MetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range Source #

data Listener Source #

Constructors

EtaExpand MetaId |
CheckConstraint Nat ProblemConstraint |

Instances

Eq Listener Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Listener -> Listener -> Bool Source # (/=) :: Listener -> Listener -> Bool Source #
Ord Listener Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: Listener -> Listener -> Ordering Source # (<) :: Listener -> Listener -> Bool Source # (<=) :: Listener -> Listener -> Bool Source # (>) :: Listener -> Listener -> Bool Source # (>=) :: Listener -> Listener -> Bool Source # max :: Listener -> Listener -> Listener Source # min :: Listener -> Listener -> Listener Source #

data Frozen Source #

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen | Do not instantiate.
Instantiable |

Instances

Eq Frozen Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Frozen -> Frozen -> Bool Source # (/=) :: Frozen -> Frozen -> Bool Source #
Show Frozen Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Frozen -> ShowS Source # show :: Frozen -> String Source # showList :: [Frozen] -> ShowS Source #

data MetaInstantiation Source #

Constructors

InstV [Arg String] Term | solved by term (abstracted over some free variables)
Open | unsolved
OpenInstance | open, to be instantiated by instance search
BlockedConst Term | solution blocked by unsolved constraints
PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) |

Instances

Show MetaInstantiation Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaInstantiation -> ShowS Source # show :: MetaInstantiation -> String Source # showList :: [MetaInstantiation] -> ShowS Source #

data CheckedTarget Source #

Solving a `CheckArgs` constraint may or may not check the target type. If it did, it returns a handle to any unsolved constraints.

Constructors

CheckedTarget (Maybe ProblemId) |
NotCheckedTarget |

data TypeCheckingProblem Source #

Constructors

CheckExpr Comparison Expr Type |
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term) |
CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonemptyList QName) Args Type Int Term Type |
CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type | `(λ (xs : t₀) → e) : t` This is not an instance of `CheckExpr` as the domain type has already been checked. For example, when checking `(λ (x y : Fin _) → e) : (x : Fin n) → ?` we want to postpone `(λ (y : Fin n) → e) : ?` where `Fin n` is a `Type` rather than an `Expr`.
DoQuoteTerm Comparison Term Type | Quote the given term and check type against `Term`

Instances

PrettyTCM TypeCheckingProblem Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: TypeCheckingProblem -> TCM Doc Source #

newtype MetaPriority Source #

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.

Constructors

MetaPriority Int |

Instances

Eq MetaPriority Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MetaPriority -> MetaPriority -> Bool Source # (/=) :: MetaPriority -> MetaPriority -> Bool Source #
Ord MetaPriority Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: MetaPriority -> MetaPriority -> Ordering Source #

(<) :: MetaPriority -> MetaPriority -> Bool Source #

(<=) :: MetaPriority -> MetaPriority -> Bool Source #

(>) :: MetaPriority -> MetaPriority -> Bool Source #

(>=) :: MetaPriority -> MetaPriority -> Bool Source #

max :: MetaPriority -> MetaPriority -> MetaPriority Source #

min :: MetaPriority -> MetaPriority -> MetaPriority Source #

Show MetaPriority Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaPriority -> ShowS Source # show :: MetaPriority -> String Source # showList :: [MetaPriority] -> ShowS Source #

data RunMetaOccursCheck Source #

Constructors

RunMetaOccursCheck |
DontRunMetaOccursCheck |

Instances

Eq RunMetaOccursCheck Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source # (/=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source #
Ord RunMetaOccursCheck Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering Source #

(<) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source #

(<=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source #

(>) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source #

(>=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool Source #

max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck Source #

min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck Source #

Show RunMetaOccursCheck Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RunMetaOccursCheck -> ShowS Source # show :: RunMetaOccursCheck -> String Source # showList :: [RunMetaOccursCheck] -> ShowS Source #

data MetaInfo Source #

`MetaInfo` is cloned from one meta to the next during pruning.

Constructors

MetaInfo |

Fields

- miClosRange :: Closure Range
- miMetaOccursCheck :: RunMetaOccursCheck

  Run the extended occurs check that goes in definitions?

- miNameSuggestion :: MetaNameSuggestion

  Used for printing. `Just x` if meta-variable comes from omitted argument with name `x`.

- miGeneralizable :: Arg DoGeneralize

  Should this meta be generalized if unsolved? If so, at what ArgInfo?

Instances

SetRange MetaInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaInfo -> MetaInfo Source #
HasRange MetaInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaInfo -> Range Source #

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

Constructors

NamedMeta |

Fields

- nmSuggestion :: MetaNameSuggestion
- nmid :: MetaId

Instances

Pretty NamedMeta Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: NamedMeta -> Doc Source # prettyPrec :: Int -> NamedMeta -> Doc Source # prettyList :: [NamedMeta] -> Doc Source #
ToConcrete NamedMeta Expr Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: NamedMeta -> AbsToCon Expr Source # bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b Source #

type MetaStore = IntMap MetaVariable Source #

normalMetaPriority :: MetaPriority Source #

lowMetaPriority :: MetaPriority Source #

highMetaPriority :: MetaPriority Source #

getMetaInfo :: MetaVariable -> Closure Range Source #

getMetaScope :: MetaVariable -> ScopeInfo Source #

getMetaEnv :: MetaVariable -> TCEnv Source #

getMetaSig :: MetaVariable -> Signature Source #

getMetaRelevance :: MetaVariable -> Relevance Source #

getMetaModality :: MetaVariable -> Modality Source #

metaFrozen :: Lens' Frozen MetaVariable Source #

## Interaction meta variables

data InteractionPoint Source #

Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Constructors

InteractionPoint |

Fields

- ipRange :: Range

  The position of the interaction point.

- ipMeta :: Maybe MetaId

  The meta variable, if any, holding the type etc.

- ipSolved :: Bool

  Has this interaction point already been solved?

- ipClause :: IPClause

  The clause of the interaction point (if any). Used for case splitting.

Instances

Eq InteractionPoint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: InteractionPoint -> InteractionPoint -> Bool Source # (/=) :: InteractionPoint -> InteractionPoint -> Bool Source #

type InteractionPoints = Map InteractionId InteractionPoint Source #

Data structure managing the interaction points.

We never remove interaction points from this map, only set their `ipSolved` to `True`. (Issue #2368)

data IPClause Source #

Which clause is an interaction point located in?

Constructors

IPClause |

Fields

- ipcQName :: QName

  The name of the function.

- ipcClauseNo :: Int

  The number of the clause of this function.

- ipcClause :: RHS

  The original AST clause rhs.

IPNoClause | The interaction point is not in the rhs of a clause.

Instances

Eq IPClause Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: IPClause -> IPClause -> Bool Source # (/=) :: IPClause -> IPClause -> Bool Source #
Data IPClause Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPClause -> c IPClause Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IPClause Source #

toConstr :: IPClause -> Constr Source #

dataTypeOf :: IPClause -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IPClause) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IPClause) Source #

gmapT :: (forall b. Data b => b -> b) -> IPClause -> IPClause Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IPClause -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IPClause -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause Source #

## Signature

data Signature Source #

Constructors

Sig |

Fields

- _sigSections :: Sections
- _sigDefinitions :: Definitions
- _sigRewriteRules :: RewriteRuleMap

  The rewrite rules defined in this file.

Instances

Data Signature Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature Source #

toConstr :: Signature -> Constr Source #

dataTypeOf :: Signature -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature) Source #

gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature Source #

Show Signature Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Signature -> ShowS Source # show :: Signature -> String Source # showList :: [Signature] -> ShowS Source #
KillRange Signature Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Signature Source #
EmbPrj Signature Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Int32 Source # icod_ :: Signature -> S Int32 Source # value :: Int32 -> R Signature Source #
InstantiateFull Signature Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Signature -> ReduceM Signature Source #

sigSections :: Lens' Sections Signature Source #

sigDefinitions :: Lens' Definitions Signature Source #

sigRewriteRules :: Lens' RewriteRuleMap Signature Source #

type Sections = Map ModuleName Section Source #

type Definitions = HashMap QName Definition Source #

type RewriteRuleMap = HashMap QName RewriteRules Source #

type DisplayForms = HashMap QName [LocalDisplayForm] Source #

newtype Section Source #

Constructors

Section |

Fields

- _secTelescope :: Telescope

Instances

Eq Section Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Section -> Section -> Bool Source # (/=) :: Section -> Section -> Bool Source #
Data Section Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Section -> c Section Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Section Source #

toConstr :: Section -> Constr Source #

dataTypeOf :: Section -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Section) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Section) Source #

gmapT :: (forall b. Data b => b -> b) -> Section -> Section Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Section -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Section -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Section -> m Section Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section Source #

Show Section Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Section -> ShowS Source # show :: Section -> String Source # showList :: [Section] -> ShowS Source #
Pretty Section Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Section -> Doc Source # prettyPrec :: Int -> Section -> Doc Source # prettyList :: [Section] -> Doc Source #
KillRange Section Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Section Source #
KillRange Sections Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections Source #
EmbPrj Section Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Int32 Source # icod_ :: Section -> S Int32 Source # value :: Int32 -> R Section Source #
InstantiateFull Section Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Section -> ReduceM Section Source #

secTelescope :: Lens' Telescope Section Source #

emptySignature :: Signature Source #

data DisplayForm Source #

A `DisplayForm` is in essence a rewrite rule `q ts --> dt` for a defined symbol (could be a constructor as well) `q`. The right hand side is a `DisplayTerm` which is used to `reify` to a more readable `Syntax`.

The patterns `ts` are just terms, but `var 0` is interpreted as a hole. Each occurrence of `var 0` is a new hole (pattern var). For each *occurrence* of `var0` the rhs `dt` has a free variable. These are instantiated when matching a display form against a term `q vs` succeeds.

Constructors

Display |

Fields

- dfFreeVars :: Nat

  Number `n` of free variables in `dfRHS`.

- dfPats :: Elims

  Left hand side patterns, where `var 0` stands for a pattern variable. There should be `n` occurrences of `var0` in `dfPats`. The `ArgInfo` is ignored in these patterns.

- dfRHS :: DisplayTerm

  Right hand side, with `n` free variables.

Instances

Data DisplayForm Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayForm -> c DisplayForm Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayForm Source #

toConstr :: DisplayForm -> Constr Source #

dataTypeOf :: DisplayForm -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayForm) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayForm) Source #

gmapT :: (forall b. Data b => b -> b) -> DisplayForm -> DisplayForm Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DisplayForm -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayForm -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm Source #

Show DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DisplayForm -> ShowS Source # show :: DisplayForm -> String Source # showList :: [DisplayForm] -> ShowS Source #
KillRange DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayForm Source #
Free DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c Source #
EmbPrj DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Int32 Source # icod_ :: DisplayForm -> S Int32 Source # value :: Int32 -> R DisplayForm Source #
NamesIn DisplayForm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayForm -> Set QName Source #
InstantiateFull DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayForm -> ReduceM DisplayForm Source #
Normalise DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DisplayForm -> ReduceM DisplayForm Source #
Simplify DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: DisplayForm -> ReduceM DisplayForm Source #
Subst Term DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source #

type LocalDisplayForm = Open DisplayForm Source #

data DisplayTerm Source #

A structured presentation of a `Term` for reification into `Syntax`.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims | `(f vs | ws) es`. The first `DisplayTerm` is the parent function `f` with its args `vs`. The list of `DisplayTerm`s are the with expressions `ws`. The `Elims` are additional arguments `es` (possible in case the with-application is of function type) or projections (if it is of record type).
DCon ConHead ConInfo [Arg DisplayTerm] | `c vs`.
DDef QName [Elim' DisplayTerm] | `d vs`.
DDot Term | `.v`.
DTerm Term | `v`.

Instances

Data DisplayTerm Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayTerm -> c DisplayTerm Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayTerm Source #

toConstr :: DisplayTerm -> Constr Source #

dataTypeOf :: DisplayTerm -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayTerm) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayTerm) Source #

gmapT :: (forall b. Data b => b -> b) -> DisplayTerm -> DisplayTerm Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DisplayTerm -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayTerm -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm Source #

Show DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DisplayTerm -> ShowS Source # show :: DisplayTerm -> String Source # showList :: [DisplayTerm] -> ShowS Source #
Pretty DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: DisplayTerm -> Doc Source # prettyPrec :: Int -> DisplayTerm -> Doc Source # prettyList :: [DisplayTerm] -> Doc Source #
KillRange DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayTerm Source #
Free DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c Source #
Apply DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
EmbPrj DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Int32 Source # icod_ :: DisplayTerm -> S Int32 Source # value :: Int32 -> R DisplayTerm Source #
PrettyTCM DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DisplayTerm -> TCM Doc Source #
NamesIn DisplayTerm Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayTerm -> Set QName Source #
InstantiateFull DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm Source #
SubstWithOrigin DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm Source #
Subst Term DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm Source #
Reify DisplayTerm Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: DisplayTerm -> TCM Expr Source # reifyWhen :: Bool -> DisplayTerm -> TCM Expr Source #
PrettyTCM (Elim' DisplayTerm) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc Source #
SubstWithOrigin (Arg DisplayTerm) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm Source #

defaultDisplayForm :: QName -> [LocalDisplayForm] Source #

By default, we have no display form.

defRelevance :: Definition -> Relevance Source #

data NLPat Source #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar !Int [Arg Int] | Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.
PWild | Matches anything (e.g. irrelevant terms).
PDef QName PElims | Matches `f es`
PLam ArgInfo (Abs NLPat) | Matches `λ x → t`
PPi (Dom NLPType) (Abs NLPType) | Matches `(x : A) → B`
PBoundVar !Int PElims | Matches `x es` where x is a lambda-bound variable
PTerm Term | Matches the term modulo β (ideally βη).

Instances

Data NLPat Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPat -> c NLPat Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPat Source #

toConstr :: NLPat -> Constr Source #

dataTypeOf :: NLPat -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPat) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPat) Source #

gmapT :: (forall b. Data b => b -> b) -> NLPat -> NLPat Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NLPat -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPat -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat Source #

Show NLPat Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NLPat -> ShowS Source # show :: NLPat -> String Source # showList :: [NLPat] -> ShowS Source #
KillRange NLPat Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPat Source #
DeBruijn NLPat Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> NLPat Source # debruijnNamedVar :: String -> Int -> NLPat Source # deBruijnView :: NLPat -> Maybe Int Source #
Free NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPat -> FreeM c Source #
EmbPrj NLPat Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Int32 Source # icod_ :: NLPat -> S Int32 Source # value :: Int32 -> R NLPat Source #
PrettyTCM NLPat Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPat -> TCM Doc Source #
InstantiateFull NLPat Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPat -> ReduceM NLPat Source #
GetMatchables NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: NLPat -> [QName] Source #
NLPatVars NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPat -> IntSet Source # nlPatVars :: NLPat -> IntSet Source #
Subst NLPat RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule Source #
Subst NLPat NLPType Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType Source #
Subst NLPat NLPat Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPat -> NLPat Source #
Match () NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #
Match () NLPat Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Sort -> NLM () Source #
Match Type NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #
PatternFrom () Sort NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPat Source #
PatternFrom Type Term NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #
PrettyTCM (Type' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type' NLPat -> TCM Doc Source #
PrettyTCM (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' NLPat -> TCM Doc Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

type PElims = [Elim' NLPat] Source #

data NLPType Source #

Constructors

NLPType |

Fields

- nlpTypeLevel :: NLPat
- nlpTypeUnEl :: NLPat

Instances

Data NLPType Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPType -> c NLPType Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPType Source #

toConstr :: NLPType -> Constr Source #

dataTypeOf :: NLPType -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPType) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPType) Source #

gmapT :: (forall b. Data b => b -> b) -> NLPType -> NLPType Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NLPType -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPType -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType Source #

Show NLPType Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NLPType -> ShowS Source # show :: NLPType -> String Source # showList :: [NLPType] -> ShowS Source #
KillRange NLPType Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPType Source #
Free NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPType -> FreeM c Source #
EmbPrj NLPType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Int32 Source # icod_ :: NLPType -> S Int32 Source # value :: Int32 -> R NLPType Source #
PrettyTCM NLPType Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPType -> TCM Doc Source #
InstantiateFull NLPType Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPType -> ReduceM NLPType Source #
NLPatVars NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPType -> IntSet Source # nlPatVars :: NLPType -> IntSet Source #
Subst NLPat NLPType Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType Source #
Match () NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #
PatternFrom () Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #

type RewriteRules = [RewriteRule] Source #

data RewriteRule Source #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule |

Fields

- rewName :: QName

  Name of rewrite rule `q : Γ → f ps ≡ rhs` where `≡` is the rewrite relation.

- rewContext :: Telescope

  `Γ`.

- rewHead :: QName

  `f`.

- rewPats :: PElims

  `Γ ⊢ f ps : t`.

- rewRHS :: Term

  `Γ ⊢ rhs : t`.

- rewType :: Type

  `Γ ⊢ t`.

Instances

Data RewriteRule Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteRule -> c RewriteRule Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RewriteRule Source #

toConstr :: RewriteRule -> Constr Source #

dataTypeOf :: RewriteRule -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RewriteRule) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RewriteRule) Source #

gmapT :: (forall b. Data b => b -> b) -> RewriteRule -> RewriteRule Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> RewriteRule -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteRule -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule Source #

Show RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RewriteRule -> ShowS Source # show :: RewriteRule -> String Source # showList :: [RewriteRule] -> ShowS Source #
KillRange RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRule Source #
KillRange RewriteRuleMap Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap Source #
Abstract RewriteRule Source # | `tel ⊢ (Γ ⊢ lhs ↦ rhs : t)` becomes `tel, Γ ⊢ lhs ↦ rhs : t)` we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source #
Apply RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
EmbPrj RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Int32 Source # icod_ :: RewriteRule -> S Int32 Source # value :: Int32 -> R RewriteRule Source #
PrettyTCM RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: RewriteRule -> TCM Doc Source #
InstantiateFull RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: RewriteRule -> ReduceM RewriteRule Source #
GetMatchables RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: RewriteRule -> [QName] Source #
Subst NLPat RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule Source #

data Definition Source #

Constructors

Defn |

Fields

- defArgInfo :: ArgInfo

  Hiding should not be used.

- defName :: QName
- defType :: Type

  Type of the lifted definition.

- defPolarity :: [Polarity]

  Variance information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.

- defArgOccurrences :: [Occurrence]

  Positivity information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.

- defArgGeneralizable :: NumGeneralizableArgs

  How many arguments should be generalised.

- defGeneralizedParams :: [Maybe Name]

  Gives the name of the (bound variable) parameter for named generalized parameters. This is needed to bring it into scope when type checking the data/record definition corresponding to a type with generalized parameters.

- defDisplay :: [LocalDisplayForm]
- defMutual :: MutualId
- defCompiledRep :: CompiledRepresentation
- defInstance :: Maybe QName

  `Just q` when this definition is an instance of class q

- defCopy :: Bool

  Has this function been created by a module instantiation?

- defMatchable :: Bool

  Is the def matched against in a rewrite rule?

- defNoCompilation :: Bool

  should compilers skip this? Used for e.g. cubical's comp

- defInjective :: Bool

  Should the def be treated as injective by the pattern matching unifier?

- theDef :: Defn

Instances

Data Definition Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Definition -> c Definition Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Definition Source #

toConstr :: Definition -> Constr Source #

dataTypeOf :: Definition -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Definition) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Definition) Source #

gmapT :: (forall b. Data b => b -> b) -> Definition -> Definition Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Definition -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Definition -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Definition -> m Definition Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition Source #

Show Definition Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Definition -> ShowS Source # show :: Definition -> String Source # showList :: [Definition] -> ShowS Source #
Pretty Definition Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Definition -> Doc Source # prettyPrec :: Int -> Definition -> Doc Source # prettyList :: [Definition] -> Doc Source #
KillRange Definition Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definition Source #
KillRange Definitions Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
Abstract Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Definition -> Definition Source #
Apply Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
EmbPrj Definition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Int32 Source # icod_ :: Definition -> S Int32 Source # value :: Int32 -> R Definition Source #
NamesIn Definition Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Definition -> Set QName Source #
InstantiateFull Definition Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Definition -> ReduceM Definition Source #

data NumGeneralizableArgs Source #

Constructors

NoGeneralizableArgs |
SomeGeneralizableArgs Int | When lambda-lifting new args are generalizable if `SomeGeneralizableArgs`, also when the number is zero.

Instances

Data NumGeneralizableArgs Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NumGeneralizableArgs -> c NumGeneralizableArgs Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NumGeneralizableArgs Source #

toConstr :: NumGeneralizableArgs -> Constr Source #

dataTypeOf :: NumGeneralizableArgs -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NumGeneralizableArgs) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NumGeneralizableArgs) Source #

gmapT :: (forall b. Data b => b -> b) -> NumGeneralizableArgs -> NumGeneralizableArgs Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NumGeneralizableArgs -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NumGeneralizableArgs -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs Source #

Show NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NumGeneralizableArgs -> ShowS Source # show :: NumGeneralizableArgs -> String Source # showList :: [NumGeneralizableArgs] -> ShowS Source #
KillRange NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NumGeneralizableArgs Source #
Abstract NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Apply NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
EmbPrj NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NumGeneralizableArgs -> S Int32 Source # icod_ :: NumGeneralizableArgs -> S Int32 Source # value :: Int32 -> R NumGeneralizableArgs Source #

theDefLens :: Lens' Defn Definition Source #

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #

Create a definition with sensible defaults.

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant | monotone
Contravariant | antitone
Invariant | no information (mixed variance)
Nonvariant | constant

Instances

Eq Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Data Polarity Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity Source #

toConstr :: Polarity -> Constr Source #

dataTypeOf :: Polarity -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) Source #

gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity Source #

Show Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Polarity -> ShowS Source # show :: Polarity -> String Source # showList :: [Polarity] -> ShowS Source #
Pretty Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
KillRange Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity Source #
EmbPrj Polarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Int32 Source # icod_ :: Polarity -> S Int32 Source # value :: Int32 -> R Polarity Source #
PrettyTCM Polarity Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Polarity -> TCM Doc Source #
Abstract [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Apply [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #

data IsForced Source #

Information about whether an argument is forced by the type of a function.

Constructors

Forced |
NotForced |

Instances

Eq IsForced Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: IsForced -> IsForced -> Bool Source # (/=) :: IsForced -> IsForced -> Bool Source #
Data IsForced Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsForced -> c IsForced Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsForced Source #

toConstr :: IsForced -> Constr Source #

dataTypeOf :: IsForced -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsForced) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsForced) Source #

gmapT :: (forall b. Data b => b -> b) -> IsForced -> IsForced Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IsForced -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsForced -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced Source #

Show IsForced Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> IsForced -> ShowS Source # show :: IsForced -> String Source # showList :: [IsForced] -> ShowS Source #
KillRange IsForced Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT IsForced Source #
EmbPrj IsForced Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Int32 Source # icod_ :: IsForced -> S Int32 Source # value :: Int32 -> R IsForced Source #
PrettyTCM IsForced Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: IsForced -> TCM Doc Source #

data CompilerPragma Source #

The backends are responsible for parsing their own pragmas.

Constructors

CompilerPragma Range String |

Instances

Eq CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompilerPragma -> CompilerPragma -> Bool Source # (/=) :: CompilerPragma -> CompilerPragma -> Bool Source #
Data CompilerPragma Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompilerPragma -> c CompilerPragma Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompilerPragma Source #

toConstr :: CompilerPragma -> Constr Source #

dataTypeOf :: CompilerPragma -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompilerPragma) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompilerPragma) Source #

gmapT :: (forall b. Data b => b -> b) -> CompilerPragma -> CompilerPragma Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CompilerPragma -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompilerPragma -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma Source #

Show CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompilerPragma -> ShowS Source # show :: CompilerPragma -> String Source # showList :: [CompilerPragma] -> ShowS Source #
KillRange CompiledRepresentation Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompiledRepresentation Source #
HasRange CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range Source #
EmbPrj CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Int32 Source # icod_ :: CompilerPragma -> S Int32 Source # value :: Int32 -> R CompilerPragma Source #

type BackendName = String Source #

jsBackendName :: BackendName Source #

ghcBackendName :: BackendName Source #

type CompiledRepresentation = Map BackendName [CompilerPragma] Source #

noCompiledRep :: CompiledRepresentation Source #

type Face = [(Term, Bool)] Source #

data System Source #

An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).

Constructors

System |

Fields

- systemTel :: Telescope

  the telescope Δ, binding vars for the clauses, Γ ⊢ Δ

- systemClauses :: [(Face, Term)]

  a system [φ₁ u₁, ... , φₙ uₙ] where Γ, Δ ⊢ φᵢ and Γ, Δ, φᵢ ⊢ uᵢ

Instances

Data System Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> System -> c System Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c System Source #

toConstr :: System -> Constr Source #

dataTypeOf :: System -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c System) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c System) Source #

gmapT :: (forall b. Data b => b -> b) -> System -> System Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> System -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> System -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> System -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> System -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> System -> m System Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System Source #

Show System Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> System -> ShowS Source # show :: System -> String Source # showList :: [System] -> ShowS Source #
KillRange System Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT System Source #
Abstract System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> System -> System Source #
Apply System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
EmbPrj System Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: System -> S Int32 Source # icod_ :: System -> S Int32 Source # value :: Int32 -> R System Source #
InstantiateFull System Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: System -> ReduceM System Source #
Reify (QNamed System) [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed System -> TCM [Clause] Source # reifyWhen :: Bool -> QNamed System -> TCM [Clause] Source #

data ExtLamInfo Source #

Additional information for extended lambdas.

Constructors

ExtLamInfo |

Fields

- extLamModule :: ModuleName

  For complicated reasons the scope checker decides the QName of a pattern lambda, and thus its module. We really need to decide the module during type checking though, since if the lambda appears in a refined context the module picked by the scope checker has very much the wrong parameters.

- extLamSys :: !(Maybe System)

Instances

Data ExtLamInfo Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtLamInfo -> c ExtLamInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtLamInfo Source #

toConstr :: ExtLamInfo -> Constr Source #

dataTypeOf :: ExtLamInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExtLamInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLamInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ExtLamInfo -> ExtLamInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ExtLamInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLamInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo Source #

Show ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ExtLamInfo -> ShowS Source # show :: ExtLamInfo -> String Source # showList :: [ExtLamInfo] -> ShowS Source #
KillRange ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ExtLamInfo Source #
Apply ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
EmbPrj ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Int32 Source # icod_ :: ExtLamInfo -> S Int32 Source # value :: Int32 -> R ExtLamInfo Source #
InstantiateFull ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ExtLamInfo -> ReduceM ExtLamInfo Source #

modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo Source #

data Projection Source #

Additional information for projection `Function`s.

Constructors

Projection |

Fields

- projProper :: Maybe QName

  `Nothing` if only projection-like, `Just r` if record projection. The `r` is the name of the record type projected from. This field is updated by module application.

- projOrig :: QName

  The original projection name (current name could be from module application).

- projFromType :: Arg QName

  Type projected from. Original record type if `projProper = Just{}`. Also stores `ArgInfo` of the principal argument. This field is unchanged by module application.

- projIndex :: Int

  Index of the record argument. Start counting with 1, because 0 means that it is already applied to the record value. This can happen in module instantiation, but then either the record value is `var 0`, or `funProjection == Nothing`.

- projLams :: ProjLams

  Term `t` to be be applied to record parameters and record value. The parameters will be dropped. In case of a proper projection, a postfix projection application will be created: `t = pars r -> r .p` (Invariant: the number of abstractions equals `projIndex`.) In case of a projection-like function, just the function symbol is returned as `Def`: `t = pars -> f`.

Instances

Data Projection Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Projection -> c Projection Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Projection Source #

toConstr :: Projection -> Constr Source #

dataTypeOf :: Projection -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Projection) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Projection) Source #

gmapT :: (forall b. Data b => b -> b) -> Projection -> Projection Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Projection -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Projection -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Projection -> m Projection Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection Source #

Show Projection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Projection -> ShowS Source # show :: Projection -> String Source # showList :: [Projection] -> ShowS Source #
KillRange Projection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Projection Source #
Abstract Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Projection -> Projection Source #
Apply Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source #
EmbPrj Projection Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Int32 Source # icod_ :: Projection -> S Int32 Source # value :: Int32 -> R Projection Source #

newtype ProjLams Source #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams |

Fields

- getProjLams :: [Arg ArgName]

Instances

Data ProjLams Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjLams -> c ProjLams Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjLams Source #

toConstr :: ProjLams -> Constr Source #

dataTypeOf :: ProjLams -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjLams) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjLams) Source #

gmapT :: (forall b. Data b => b -> b) -> ProjLams -> ProjLams Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProjLams -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjLams -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams Source #

Show ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProjLams -> ShowS Source # show :: ProjLams -> String Source # showList :: [ProjLams] -> ShowS Source #
Null ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: ProjLams Source # null :: ProjLams -> Bool Source #
KillRange ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ProjLams Source #
Abstract ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Apply ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ProjLams -> Args -> ProjLams Source # applyE :: ProjLams -> Elims -> ProjLams Source #
EmbPrj ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Int32 Source # icod_ :: ProjLams -> S Int32 Source # value :: Int32 -> R ProjLams Source #

projDropPars :: Projection -> ProjOrigin -> Term Source #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo Source #

The info of the principal (record) argument.

data EtaEquality Source #

Should a record type admit eta-equality?

Constructors

Specified | User specifed 'eta-equality' or 'no-eta-equality'.

Fields

- theEtaEquality :: !HasEta

Inferred | Positivity checker inferred whether eta is safe.

Fields

- theEtaEquality :: !HasEta

Instances

Eq EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: EtaEquality -> EtaEquality -> Bool Source # (/=) :: EtaEquality -> EtaEquality -> Bool Source #
Data EtaEquality Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EtaEquality -> c EtaEquality Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EtaEquality Source #

toConstr :: EtaEquality -> Constr Source #

dataTypeOf :: EtaEquality -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EtaEquality) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EtaEquality) Source #

gmapT :: (forall b. Data b => b -> b) -> EtaEquality -> EtaEquality Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> EtaEquality -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> EtaEquality -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality Source #

Show EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> EtaEquality -> ShowS Source # show :: EtaEquality -> String Source # showList :: [EtaEquality] -> ShowS Source #
KillRange EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT EtaEquality Source #
EmbPrj EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Int32 Source # icod_ :: EtaEquality -> S Int32 Source # value :: Int32 -> R EtaEquality Source #

setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #

Make sure we do not overwrite a user specification.

data FunctionFlag Source #

Constructors

FunStatic | Should calls to this function be normalised at compile-time?
FunInline | Should calls to this function be inlined by the compiler?
FunMacro | Is this function a macro?

Instances

Enum FunctionFlag Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

succ :: FunctionFlag -> FunctionFlag Source #

pred :: FunctionFlag -> FunctionFlag Source #

toEnum :: Int -> FunctionFlag Source #

fromEnum :: FunctionFlag -> Int Source #

enumFrom :: FunctionFlag -> [FunctionFlag] Source #

enumFromThen :: FunctionFlag -> FunctionFlag -> [FunctionFlag] Source #

enumFromTo :: FunctionFlag -> FunctionFlag -> [FunctionFlag] Source #

enumFromThenTo :: FunctionFlag -> FunctionFlag -> FunctionFlag -> [FunctionFlag] Source #

Eq FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: FunctionFlag -> FunctionFlag -> Bool Source # (/=) :: FunctionFlag -> FunctionFlag -> Bool Source #
Data FunctionFlag Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctionFlag -> c FunctionFlag Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctionFlag Source #

toConstr :: FunctionFlag -> Constr Source #

dataTypeOf :: FunctionFlag -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctionFlag) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctionFlag) Source #

gmapT :: (forall b. Data b => b -> b) -> FunctionFlag -> FunctionFlag Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> FunctionFlag -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionFlag -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag Source #

Ord FunctionFlag Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: FunctionFlag -> FunctionFlag -> Ordering Source #

(<) :: FunctionFlag -> FunctionFlag -> Bool Source #

(<=) :: FunctionFlag -> FunctionFlag -> Bool Source #

(>) :: FunctionFlag -> FunctionFlag -> Bool Source #

(>=) :: FunctionFlag -> FunctionFlag -> Bool Source #

max :: FunctionFlag -> FunctionFlag -> FunctionFlag Source #

min :: FunctionFlag -> FunctionFlag -> FunctionFlag Source #

Show FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> FunctionFlag -> ShowS Source # show :: FunctionFlag -> String Source # showList :: [FunctionFlag] -> ShowS Source #
KillRange FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT FunctionFlag Source #
EmbPrj FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Int32 Source # icod_ :: FunctionFlag -> S Int32 Source # value :: Int32 -> R FunctionFlag Source #

data CompKit Source #

Constructors

CompKit |

Fields

- nameOfHComp :: Maybe QName
- nameOfTransp :: Maybe QName

Instances

Eq CompKit Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompKit -> CompKit -> Bool Source # (/=) :: CompKit -> CompKit -> Bool Source #
Data CompKit Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompKit -> c CompKit Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompKit Source #

toConstr :: CompKit -> Constr Source #

dataTypeOf :: CompKit -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompKit) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompKit) Source #

gmapT :: (forall b. Data b => b -> b) -> CompKit -> CompKit Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CompKit -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompKit -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit Source #

Ord CompKit Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: CompKit -> CompKit -> Ordering Source # (<) :: CompKit -> CompKit -> Bool Source # (<=) :: CompKit -> CompKit -> Bool Source # (>) :: CompKit -> CompKit -> Bool Source # (>=) :: CompKit -> CompKit -> Bool Source # max :: CompKit -> CompKit -> CompKit Source # min :: CompKit -> CompKit -> CompKit Source #
Show CompKit Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompKit -> ShowS Source # show :: CompKit -> String Source # showList :: [CompKit] -> ShowS Source #
KillRange CompKit Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompKit Source #
EmbPrj CompKit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompKit -> S Int32 Source # icod_ :: CompKit -> S Int32 Source # value :: Int32 -> R CompKit Source #
NamesIn CompKit Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompKit -> Set QName Source #

emptyCompKit :: CompKit Source #

data Defn Source #

Constructors

Axiom | Postulate
DataOrRecSig | Data or record type signature that doesn't yet have a definition

Fields

- datarecPars :: Int

GeneralizableVar | Generalizable variable (introduced in `generalize` block)
AbstractDefn Defn | Returned by `getConstInfo` if definition is abstract.
Function |

Fields

- funClauses :: [Clause]
- funCompiled :: Maybe CompiledClauses

  `Nothing` while function is still type-checked. `Just cc` after type and coverage checking and translation to case trees.

- funSplitTree :: Maybe SplitTree

  The split tree constructed by the coverage checker. Needed to re-compile the clauses after forcing translation.

- funTreeless :: Maybe Compiled

  Intermediate representation for compiler backends.

- funCovering :: [Closure Clause]

  Covering clauses computed by coverage checking. Erased by (IApply) confluence checking(?)

- funInv :: FunctionInverse
- funMutual :: Maybe [QName]

  Mutually recursive functions, `data`s and `record`s. Does include this function. Empty list if not recursive. `Nothing` if not yet computed (by positivity checker).

- funAbstr :: IsAbstract
- funDelayed :: Delayed

  Are the clauses of this definition delayed?

- funProjection :: Maybe Projection

  Is it a record projection? If yes, then return the name of the record type and index of the record argument. Start counting with 1, because 0 means that it is already applied to the record. (Can happen in module instantiation.) This information is used in the termination checker.

- funFlags :: Set FunctionFlag
- funTerminates :: Maybe Bool

  Has this function been termination checked? Did it pass?

- funExtLam :: Maybe ExtLamInfo

  Is this function generated from an extended lambda? If yes, then return the number of hidden and non-hidden lambda-lifted arguments

- funWith :: Maybe QName

  Is this a generated with-function? If yes, then what's the name of the parent function.

- funCopatternLHS :: Bool

  Is this a function defined by copatterns?

Datatype |

Fields

- dataPars :: Nat

  Number of parameters.

- dataIxs :: Nat

  Number of indices.

- dataInduction :: Induction

  `data` or `codata` (legacy).

- dataClause :: Maybe Clause

  This might be in an instantiated module.

- dataCons :: [QName]

  Constructor names , ordered according to the order of their definition.

- dataSort :: Sort
- dataMutual :: Maybe [QName]

  Mutually recursive functions, `data`s and `record`s. Does include this data type. Empty if not recursive. `Nothing` if not yet computed (by positivity checker).

- dataAbstr :: IsAbstract
- dataPathCons :: [QName]

  Path constructor names (subset of dataCons)

Record |

Fields

- recPars :: Nat

  Number of parameters.

- recClause :: Maybe Clause

  Was this record type created by a module application? If yes, the clause is its definition (linking back to the original record type).

- recConHead :: ConHead

  Constructor name and fields.

- recNamedCon :: Bool

  Does this record have a `constructor`?

- recFields :: [Arg QName]

  The record field names.

- recTel :: Telescope

  The record field telescope. (Includes record parameters.) Note: `TelV recTel _ == telView' recConType`. Thus, `recTel` is redundant.

- recMutual :: Maybe [QName]

  Mutually recursive functions, `data`s and `record`s. Does include this record. Empty if not recursive. `Nothing` if not yet computed (by positivity checker).

- recEtaEquality' :: EtaEquality

  Eta-expand at this record type? `False` for unguarded recursive records and coinductive records unless the user specifies otherwise.

- recInduction :: Maybe Induction

  `Inductive` or `CoInductive`? Matters only for recursive records. `Nothing` means that the user did not specify it, which is an error for recursive records.

- recAbstr :: IsAbstract
- recComp :: CompKit

Constructor |

Fields

- conPars :: Int

  Number of parameters.

- conArity :: Int

  Number of arguments (excluding parameters).

- conSrcCon :: ConHead

  Name of (original) constructor and fields. (This might be in a module instance.)

- conData :: QName

  Name of datatype or record type.

- conAbstr :: IsAbstract
- conInd :: Induction

  Inductive or coinductive?

- conComp :: (CompKit, Maybe [QName])

  (cubical composition, projections)

- conForced :: [IsForced]

  Which arguments are forced (i.e. determined by the type of the constructor)?

- conErased :: [Bool]

  Which arguments are erased at runtime (computed during compilation to treeless)

Primitive | Primitive or builtin functions.

Fields

- primAbstr :: IsAbstract
- primName :: String
- primClauses :: [Clause]

  `null` for primitive functions, `not null` for builtin functions.

- primInv :: FunctionInverse

  Builtin functions can have inverses. For instance, natural number addition.

- primCompiled :: Maybe CompiledClauses

  `Nothing` for primitive functions, ``Just` something` for builtin functions.

Instances

Data Defn Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn Source #

toConstr :: Defn -> Constr Source #

dataTypeOf :: Defn -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn) Source #

gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source #

Show Defn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Defn -> ShowS Source # show :: Defn -> String Source # showList :: [Defn] -> ShowS Source #
Pretty Defn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Defn -> Doc Source # prettyPrec :: Int -> Defn -> Doc Source # prettyList :: [Defn] -> Doc Source #
KillRange Defn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Defn Source #
Abstract Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Defn -> Defn Source #
Apply Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
EmbPrj Defn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Int32 Source # icod_ :: Defn -> S Int32 Source # value :: Int32 -> R Defn Source #
NamesIn Defn Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Defn -> Set QName Source #
InstantiateFull Defn Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Defn -> ReduceM Defn Source #
Occurs Defn Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Defn -> TCM Defn Source # metaOccurs :: MetaId -> Defn -> TCM () Source #

recRecursive :: Defn -> Bool Source #

Is the record type recursive?

recEtaEquality :: Defn -> HasEta Source #

emptyFunction :: Defn Source #

A template for creating `Function` definitions, with sensible defaults.

funFlag :: FunctionFlag -> Lens' Bool Defn Source #

funStatic :: Lens' Bool Defn Source #

funInline :: Lens' Bool Defn Source #

funMacro :: Lens' Bool Defn Source #

isMacro :: Defn -> Bool Source #

isEmptyFunction :: Defn -> Bool Source #

Checking whether we are dealing with a function yet to be defined.

isCopatternLHS :: [Clause] -> Bool Source #

recCon :: Defn -> QName Source #

defIsRecord :: Defn -> Bool Source #

defIsDataOrRecord :: Defn -> Bool Source #

defConstructors :: Defn -> [QName] Source #

newtype Fields Source #

Constructors

Fields [(Name, Type)] |

Instances

Null Fields Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Fields Source # null :: Fields -> Bool Source #

data Simplification Source #

Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?

Constructors

YesSimplification |
NoSimplification |

Instances

Eq Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Simplification -> Simplification -> Bool Source # (/=) :: Simplification -> Simplification -> Bool Source #
Data Simplification Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Simplification -> c Simplification Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Simplification Source #

toConstr :: Simplification -> Constr Source #

dataTypeOf :: Simplification -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Simplification) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Simplification) Source #

gmapT :: (forall b. Data b => b -> b) -> Simplification -> Simplification Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Simplification -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Simplification -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification Source #

Show Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Simplification -> ShowS Source # show :: Simplification -> String Source # showList :: [Simplification] -> ShowS Source #
Semigroup Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: Simplification -> Simplification -> Simplification Source # sconcat :: NonEmpty Simplification -> Simplification Source # stimes :: Integral b => b -> Simplification -> Simplification Source #
Monoid Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods mempty :: Simplification Source # mappend :: Simplification -> Simplification -> Simplification Source # mconcat :: [Simplification] -> Simplification Source #
Null Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Simplification Source # null :: Simplification -> Bool Source #

data Reduced no yes Source #

Constructors

NoReduction no |
YesReduction Simplification yes |

Instances

Functor (Reduced no) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Reduced no a -> Reduced no b Source # (<$) :: a -> Reduced no b -> Reduced no a Source #

data IsReduced Source #

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.

Constructors

NotReduced |
Reduced (Blocked ()) |

data MaybeReduced a Source #

Constructors

MaybeRed |

Fields

- isReduced :: IsReduced
- ignoreReduced :: a

Instances

Functor MaybeReduced Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> MaybeReduced a -> MaybeReduced b Source # (<$) :: a -> MaybeReduced b -> MaybeReduced a Source #
IsProjElim e => IsProjElim (MaybeReduced e) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source #
PrettyTCM a => PrettyTCM (MaybeReduced a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MaybeReduced a -> TCM Doc Source #

type MaybeReducedArgs = [MaybeReduced (Arg Term)] Source #

type MaybeReducedElims = [MaybeReduced Elim] Source #

notReduced :: a -> MaybeReduced a Source #

reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term) Source #

data AllowedReduction Source #

Controlling `reduce`.

Constructors

ProjectionReductions | (Projection and) projection-like functions may be reduced.
InlineReductions | Functions marked INLINE may be reduced.
CopatternReductions | Copattern definitions may be reduced.
FunctionReductions | Non-recursive functions and primitives may be reduced.
RecursiveReductions | Even recursive functions may be reduced.
LevelReductions | Reduce ``Term`` terms.
UnconfirmedReductions | Functions whose termination has not (yet) been confirmed.
NonTerminatingReductions | Functions that have failed termination checking.

Instances

Bounded AllowedReduction Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods minBound :: AllowedReduction Source # maxBound :: AllowedReduction Source #
Enum AllowedReduction Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

succ :: AllowedReduction -> AllowedReduction Source #

pred :: AllowedReduction -> AllowedReduction Source #

toEnum :: Int -> AllowedReduction Source #

fromEnum :: AllowedReduction -> Int Source #

enumFrom :: AllowedReduction -> [AllowedReduction] Source #

enumFromThen :: AllowedReduction -> AllowedReduction -> [AllowedReduction] Source #

enumFromTo :: AllowedReduction -> AllowedReduction -> [AllowedReduction] Source #

enumFromThenTo :: AllowedReduction -> AllowedReduction -> AllowedReduction -> [AllowedReduction] Source #

Eq AllowedReduction Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: AllowedReduction -> AllowedReduction -> Bool Source # (/=) :: AllowedReduction -> AllowedReduction -> Bool Source #
Data AllowedReduction Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AllowedReduction -> c AllowedReduction Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AllowedReduction Source #

toConstr :: AllowedReduction -> Constr Source #

dataTypeOf :: AllowedReduction -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AllowedReduction) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AllowedReduction) Source #

gmapT :: (forall b. Data b => b -> b) -> AllowedReduction -> AllowedReduction Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AllowedReduction -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AllowedReduction -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction Source #

Ord AllowedReduction Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: AllowedReduction -> AllowedReduction -> Ordering Source #

(<) :: AllowedReduction -> AllowedReduction -> Bool Source #

(<=) :: AllowedReduction -> AllowedReduction -> Bool Source #

(>) :: AllowedReduction -> AllowedReduction -> Bool Source #

(>=) :: AllowedReduction -> AllowedReduction -> Bool Source #

max :: AllowedReduction -> AllowedReduction -> AllowedReduction Source #

min :: AllowedReduction -> AllowedReduction -> AllowedReduction Source #

Show AllowedReduction Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AllowedReduction -> ShowS Source # show :: AllowedReduction -> String Source # showList :: [AllowedReduction] -> ShowS Source #

type AllowedReductions = [AllowedReduction] Source #

allReductions :: AllowedReductions Source #

Not quite all reductions (skip non-terminating reductions)

data PrimFun Source #

Constructors

PrimFun |

Fields

- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)

Instances

Abstract PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Apply PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun Source #

primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun Source #

defClauses :: Definition -> [Clause] Source #

defCompiled :: Definition -> Maybe CompiledClauses Source #

defParameters :: Definition -> Maybe Nat Source #

defInverse :: Definition -> FunctionInverse Source #

defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma] Source #

defDelayed :: Definition -> Delayed Source #

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool Source #

Has the definition failed the termination checker?

defTerminationUnconfirmed :: Definition -> Bool Source #

Has the definition not termination checked or did the check fail?

defAbstract :: Definition -> IsAbstract Source #

defForced :: Definition -> [IsForced] Source #

## Injectivity

type FunctionInverse = FunctionInverse' Clause Source #

type InversionMap c = Map TermHead [c] Source #

data FunctionInverse' c Source #

Constructors

NotInjective |
Inverse (InversionMap c) |

Instances

Functor FunctionInverse' Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> FunctionInverse' a -> FunctionInverse' b Source # (<$) :: a -> FunctionInverse' b -> FunctionInverse' a Source #
Abstract FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Apply FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
DropArgs FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #
InstantiateFull FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #
Data c => Data (FunctionInverse' c) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> FunctionInverse' c -> c0 (FunctionInverse' c) Source #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (FunctionInverse' c) Source #

toConstr :: FunctionInverse' c -> Constr Source #

dataTypeOf :: FunctionInverse' c -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (FunctionInverse' c)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (FunctionInverse' c)) Source #

gmapT :: (forall b. Data b => b -> b) -> FunctionInverse' c -> FunctionInverse' c Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> FunctionInverse' c -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionInverse' c -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) Source #

Show c => Show (FunctionInverse' c) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> FunctionInverse' c -> ShowS Source # show :: FunctionInverse' c -> String Source # showList :: [FunctionInverse' c] -> ShowS Source #
KillRange c => KillRange (FunctionInverse' c) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) Source #
EmbPrj a => EmbPrj (FunctionInverse' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Int32 Source # icod_ :: FunctionInverse' a -> S Int32 Source # value :: Int32 -> R (FunctionInverse' a) Source #

data TermHead Source #

Constructors

SortHead |
PiHead |
ConsHead QName |
VarHead Nat |
UnknownHead |

Instances

Eq TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: TermHead -> TermHead -> Bool Source # (/=) :: TermHead -> TermHead -> Bool Source #
Data TermHead Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermHead -> c TermHead Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermHead Source #

toConstr :: TermHead -> Constr Source #

dataTypeOf :: TermHead -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermHead) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermHead) Source #

gmapT :: (forall b. Data b => b -> b) -> TermHead -> TermHead Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TermHead -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TermHead -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead Source #

Ord TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: TermHead -> TermHead -> Ordering Source # (<) :: TermHead -> TermHead -> Bool Source # (<=) :: TermHead -> TermHead -> Bool Source # (>) :: TermHead -> TermHead -> Bool Source # (>=) :: TermHead -> TermHead -> Bool Source # max :: TermHead -> TermHead -> TermHead Source # min :: TermHead -> TermHead -> TermHead Source #
Show TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TermHead -> ShowS Source # show :: TermHead -> String Source # showList :: [TermHead] -> ShowS Source #
Pretty TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: TermHead -> Doc Source # prettyPrec :: Int -> TermHead -> Doc Source # prettyList :: [TermHead] -> Doc Source #
KillRange TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT TermHead Source #
EmbPrj TermHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Int32 Source # icod_ :: TermHead -> S Int32 Source # value :: Int32 -> R TermHead Source #

## Mutual blocks

newtype MutualId Source #

Constructors

MutId Int32 |

Instances

Enum MutualId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

succ :: MutualId -> MutualId Source #

pred :: MutualId -> MutualId Source #

toEnum :: Int -> MutualId Source #

fromEnum :: MutualId -> Int Source #

enumFrom :: MutualId -> [MutualId] Source #

enumFromThen :: MutualId -> MutualId -> [MutualId] Source #

enumFromTo :: MutualId -> MutualId -> [MutualId] Source #

enumFromThenTo :: MutualId -> MutualId -> MutualId -> [MutualId] Source #

Eq MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MutualId -> MutualId -> Bool Source # (/=) :: MutualId -> MutualId -> Bool Source #
Data MutualId Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualId -> c MutualId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualId Source #

toConstr :: MutualId -> Constr Source #

dataTypeOf :: MutualId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualId) Source #

gmapT :: (forall b. Data b => b -> b) -> MutualId -> MutualId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MutualId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId Source #

Num MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: MutualId -> MutualId -> MutualId Source # (-) :: MutualId -> MutualId -> MutualId Source # (*) :: MutualId -> MutualId -> MutualId Source # negate :: MutualId -> MutualId Source # abs :: MutualId -> MutualId Source # signum :: MutualId -> MutualId Source # fromInteger :: Integer -> MutualId Source #
Ord MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: MutualId -> MutualId -> Ordering Source # (<) :: MutualId -> MutualId -> Bool Source # (<=) :: MutualId -> MutualId -> Bool Source # (>) :: MutualId -> MutualId -> Bool Source # (>=) :: MutualId -> MutualId -> Bool Source # max :: MutualId -> MutualId -> MutualId Source # min :: MutualId -> MutualId -> MutualId Source #
Show MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MutualId -> ShowS Source # show :: MutualId -> String Source # showList :: [MutualId] -> ShowS Source #
KillRange MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT MutualId Source #
HasFresh MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MutualId TCState Source # nextFresh' :: MutualId -> MutualId Source #
EmbPrj MutualId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Int32 Source # icod_ :: MutualId -> S Int32 Source # value :: Int32 -> R MutualId Source #

## Statistics

type Statistics = Map String Integer Source #

## Trace

data Call Source #

Constructors

CheckClause Type SpineClause |
CheckPattern Pattern Telescope Type |
CheckLetBinding LetBinding |
InferExpr Expr |
CheckExprCall Comparison Expr Type |
CheckDotPattern Expr Term |
CheckPatternShadowing SpineClause |
CheckProjection Range QName Type |
IsTypeCall Expr Sort |
IsType_ Expr |
InferVar Name |
InferDef QName |
CheckArguments Range [NamedArg Expr] Type (Maybe Type) |
CheckTargetType Range Type Type |
CheckDataDef Range QName [LamBinding] [Constructor] |
CheckRecDef Range QName [LamBinding] [Constructor] |
CheckConstructor QName Telescope Sort Constructor |
CheckConstructorFitsIn QName Type Sort |
CheckFunDefCall Range QName [Clause] |
CheckPragma Range Pragma |
CheckPrimitive Range QName Expr |
CheckIsEmpty Range Type |
CheckWithFunctionType Type |
CheckSectionApplication Range ModuleName ModuleApplication |
CheckNamedWhere ModuleName |
ScopeCheckExpr Expr |
ScopeCheckDeclaration NiceDeclaration |
ScopeCheckLHS QName Pattern |
NoHighlighting |
ModuleContents | Interaction command: show module contents.
SetRange Range | used by `setCurrentRange`

Instances

Data Call Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Call -> c Call Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Call Source #

toConstr :: Call -> Constr Source #

dataTypeOf :: Call -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Call) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Call) Source #

gmapT :: (forall b. Data b => b -> b) -> Call -> Call Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Call -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Call -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Call -> m Call Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call Source #

Pretty Call Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Call -> Doc Source # prettyPrec :: Int -> Call -> Doc Source # prettyList :: [Call] -> Doc Source #
HasRange Call Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Call -> Range Source #
PrettyTCM Call Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Call -> TCM Doc Source #

## Instance table

type InstanceTable = Map QName (Set QName) Source #

The instance table is a `Map` associating to every name of recorddata typepostulate its list of instances

type TempInstanceTable = (InstanceTable, Set QName) Source #

When typechecking something of the following form:

instance x : _ x = y

it's not yet known where to add `x`, so we add it to a list of unresolved instances and we'll deal with it later.

## Builtin things

data BuiltinDescriptor Source #

Constructors

BuiltinData (TCM Type) [String] |
BuiltinDataCons (TCM Type) |
BuiltinPrim String (Term -> TCM ()) |
BuiltinPostulate Relevance (TCM Type) |
BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ()) | Builtin of any kind. Type can be checked (`Just t`) or inferred (`Nothing`). The second argument is the hook for the verification function.

data BuiltinInfo Source #

Constructors

BuiltinInfo |

Fields

- builtinName :: String
- builtinDesc :: BuiltinDescriptor

type BuiltinThings pf = Map String (Builtin pf) Source #

data Builtin pf Source #

Constructors

Builtin Term |
Prim pf |

Instances

Functor Builtin Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Builtin a -> Builtin b Source # (<$) :: a -> Builtin b -> Builtin a Source #
Foldable Builtin Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Builtin m -> m Source #

foldMap :: Monoid m => (a -> m) -> Builtin a -> m Source #

foldr :: (a -> b -> b) -> b -> Builtin a -> b Source #

foldr' :: (a -> b -> b) -> b -> Builtin a -> b Source #

foldl :: (b -> a -> b) -> b -> Builtin a -> b Source #

foldl' :: (b -> a -> b) -> b -> Builtin a -> b Source #

foldr1 :: (a -> a -> a) -> Builtin a -> a Source #

foldl1 :: (a -> a -> a) -> Builtin a -> a Source #

toList :: Builtin a -> [a] Source #

null :: Builtin a -> Bool Source #

length :: Builtin a -> Int Source #

elem :: Eq a => a -> Builtin a -> Bool Source #

maximum :: Ord a => Builtin a -> a Source #

minimum :: Ord a => Builtin a -> a Source #

sum :: Num a => Builtin a -> a Source #

product :: Num a => Builtin a -> a Source #

Traversable Builtin Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b) Source # sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a) Source # mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b) Source # sequence :: Monad m => Builtin (m a) -> m (Builtin a) Source #
Show pf => Show (Builtin pf) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Builtin pf -> ShowS Source # show :: Builtin pf -> String Source # showList :: [Builtin pf] -> ShowS Source #
EmbPrj a => EmbPrj (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Int32 Source # icod_ :: Builtin a -> S Int32 Source # value :: Int32 -> R (Builtin a) Source #
InstantiateFull a => InstantiateFull (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Builtin a -> ReduceM (Builtin a) Source #

# Highlighting levels

data HighlightingLevel Source #

How much highlighting should be sent to the user interface?

Constructors

None |
NonInteractive |
Interactive | This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Instances

Eq HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: HighlightingLevel -> HighlightingLevel -> Bool Source # (/=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #
Data HighlightingLevel Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingLevel -> c HighlightingLevel Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingLevel Source #

toConstr :: HighlightingLevel -> Constr Source #

dataTypeOf :: HighlightingLevel -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingLevel) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingLevel) Source #

gmapT :: (forall b. Data b => b -> b) -> HighlightingLevel -> HighlightingLevel Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> HighlightingLevel -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingLevel -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel Source #

Ord HighlightingLevel Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: HighlightingLevel -> HighlightingLevel -> Ordering Source #

(<) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(<=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(>) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(>=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel Source #

min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel Source #

Read HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods readsPrec :: Int -> ReadS HighlightingLevel Source # readList :: ReadS [HighlightingLevel] Source # readPrec :: ReadPrec HighlightingLevel Source # readListPrec :: ReadPrec [HighlightingLevel] Source #
Show HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> HighlightingLevel -> ShowS Source # show :: HighlightingLevel -> String Source # showList :: [HighlightingLevel] -> ShowS Source #

data HighlightingMethod Source #

How should highlighting be sent to the user interface?

Constructors

Direct | Via stdout.
Indirect | Both via files and via stdout.

Instances

Eq HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: HighlightingMethod -> HighlightingMethod -> Bool Source # (/=) :: HighlightingMethod -> HighlightingMethod -> Bool Source #
Data HighlightingMethod Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingMethod -> c HighlightingMethod Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingMethod Source #

toConstr :: HighlightingMethod -> Constr Source #

dataTypeOf :: HighlightingMethod -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingMethod) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingMethod) Source #

gmapT :: (forall b. Data b => b -> b) -> HighlightingMethod -> HighlightingMethod Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> HighlightingMethod -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingMethod -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod Source #

Read HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods readsPrec :: Int -> ReadS HighlightingMethod Source # readList :: ReadS [HighlightingMethod] Source # readPrec :: ReadPrec HighlightingMethod Source # readListPrec :: ReadPrec [HighlightingMethod] Source #
Show HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> HighlightingMethod -> ShowS Source # show :: HighlightingMethod -> String Source # showList :: [HighlightingMethod] -> ShowS Source #

ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm () Source #

`ifTopLevelAndHighlightingLevelIs l b m` runs `m` when we're type-checking the top-level module and either the highlighting level is at least `l` or `b` is `True`.

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source #

`ifTopLevelAndHighlightingLevelIs l m` runs `m` when we're type-checking the top-level module and the highlighting level is at least `l`.

# Type checking environment

data TCEnv Source #

Constructors

TCEnv |

Fields

- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath

  The path to the file that is currently being type-checked. `Nothing` if we do not have a file (like in interactive mode see `CommandLine`).

- envAnonymousModules :: [(ModuleName, Nat)]

  anonymous modules and their number of free variables

- envImportPath :: [TopLevelModuleName]

  to detect import cycles

- envMutualBlock :: Maybe MutualId

  the current (if any) mutual block

- envTerminationCheck :: TerminationCheck ()

  are we inside the scope of a termination pragma

- envSolvingConstraints :: Bool

  Are we currently in the process of solving active constraints?

- envCheckingWhere :: Bool

  Have we stepped into the where-declarations of a clause? Everything under a `where` will be checked with this flag on.

- envWorkingOnTypes :: Bool

  Are we working on types? Turned on by `workOnTypes`.

- envAssignMetas :: Bool

  Are we allowed to assign metas?

- envActiveProblems :: Set ProblemId
- envAbstractMode :: AbstractMode

  When checking the typesignature of a public definition or the body of a non-abstract definition this is true. To prevent information about abstract things leaking outside the module.

- envModality :: Modality

  `Relevance` component: Are we checking an irrelevant argument? (=`Irrelevant`) Then top-level irrelevant declarations are enabled. Other value: `Relevant`, then only relevant decls. are available.

  `Quantity` component: Are we checking a runtime-irrelevant thing? (=`Quantity0`) Then runtime-irrelevant things are usable. Other value: `Quantity1`, runtime relevant. `Quantityω` is not allowed here, see Bob Atkey, LiCS 2018.

- envDisplayFormsEnabled :: Bool

  Sometimes we want to disable display forms.

- envRange :: Range
- envHighlightingRange :: Range

  Interactive highlighting uses this range rather than `envRange`.

- envClause :: IPClause

  What is the current clause we are type-checking? Will be recorded in interaction points in this clause.

- envCall :: Maybe (Closure Call)

  what we're doing at the moment

- envHighlightingLevel :: HighlightingLevel

  Set to `None` when imported modules are type-checked.

- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: !Int

  This number indicates how far away from the top-level module Agda has come when chasing modules. The level of a given module is not necessarily the same as the length, in the module dependency graph, of the shortest path from the top-level module; it depends on in which order Agda chooses to chase dependencies.

- envExpandLast :: ExpandHidden

  When type-checking an alias f=e, we do not want to insert hidden arguments in the end, because these will become unsolved metas.

- envAppDef :: Maybe QName

  We are reducing an application of this function. (For debugging of incomplete matches only.)

- envSimplification :: Simplification

  Did we encounter a simplification (proper match) during the current reduction process?

- envAllowedReductions :: AllowedReductions
- envInjectivityDepth :: Int

  Injectivity can cause non-termination for unsolvable contraints (3067). Keep a limit on the nesting depth of injectivity uses.

- envCompareBlocked :: Bool

  Can we compare blocked things during conversion? No by default. Yes for rewriting feature.

- envPrintDomainFreePi :: Bool

  When `True`, types will be omitted from printed pi types if they can be inferred.

- envPrintMetasBare :: Bool

  When `True`, throw away meta numbers and meta elims. This is used for reifying terms for feeding into the user's source code, e.g., for the interaction tactics `solveAll`.

- envInsideDotPattern :: Bool

  Used by the scope checker to make sure that certain forms of expressions are not used inside dot patterns: extended lambdas and let-expressions.

- envUnquoteFlags :: UnquoteFlags
- envInstanceDepth :: !Int

  Until we get a termination checker for instance search (#1743) we limit the search depth to ensure termination.

- envIsDebugPrinting :: Bool
- envPrintingPatternLambdas :: [QName]

  #3004: pattern lambdas with copatterns may refer to themselves. We don't have a good story for what to do in this case, but at least printing shouldn't loop. Here we keep track of which pattern lambdas we are currently in the process of printing.

- envCallByNeed :: Bool

  Use call-by-need evaluation for reductions.

- envCurrentCheckpoint :: CheckpointId

  Checkpoints track the evolution of the context as we go under binders or refine it by pattern matching.

- envCheckpoints :: Map CheckpointId Substitution

  Keeps the substitution from each previous checkpoint to the current context.

- envGeneralizeMetas :: DoGeneralize

  Should new metas generalized over.

- envGeneralizedVars :: Map QName GeneralizedValue

  Values for used generalizable variables.

- envCheckOptionConsistency :: Bool

  Do we check that options in imported files are consistent with each other?

Instances

Data TCEnv Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEnv -> c TCEnv Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCEnv Source #

toConstr :: TCEnv -> Constr Source #

dataTypeOf :: TCEnv -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCEnv) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCEnv) Source #

gmapT :: (forall b. Data b => b -> b) -> TCEnv -> TCEnv Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TCEnv -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEnv -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv Source #

initEnv :: TCEnv Source #

envRelevance :: TCEnv -> Relevance Source #

Project `Relevance` component of `TCEnv`.

data UnquoteFlags Source #

Constructors

UnquoteFlags |

Fields

- _unquoteNormalise :: Bool

Instances

Data UnquoteFlags Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnquoteFlags -> c UnquoteFlags Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnquoteFlags Source #

toConstr :: UnquoteFlags -> Constr Source #

dataTypeOf :: UnquoteFlags -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnquoteFlags) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnquoteFlags) Source #

gmapT :: (forall b. Data b => b -> b) -> UnquoteFlags -> UnquoteFlags Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> UnquoteFlags -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnquoteFlags -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags Source #

defaultUnquoteFlags :: UnquoteFlags Source #

unquoteNormalise :: Lens' Bool UnquoteFlags Source #

eUnquoteNormalise :: Lens' Bool TCEnv Source #

# e-prefixed lenses

eContext :: Lens' Context TCEnv Source #

eLetBindings :: Lens' LetBindings TCEnv Source #

eCurrentModule :: Lens' ModuleName TCEnv Source #

eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv Source #

eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv Source #

eImportPath :: Lens' [TopLevelModuleName] TCEnv Source #

eMutualBlock :: Lens' (Maybe MutualId) TCEnv Source #

eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv Source #

eSolvingConstraints :: Lens' Bool TCEnv Source #

eCheckingWhere :: Lens' Bool TCEnv Source #

eWorkingOnTypes :: Lens' Bool TCEnv Source #

eAssignMetas :: Lens' Bool TCEnv Source #

eActiveProblems :: Lens' (Set ProblemId) TCEnv Source #

eAbstractMode :: Lens' AbstractMode TCEnv Source #

eModality :: Lens' Modality TCEnv Source #

eRelevance :: Lens' Relevance TCEnv Source #

eQuantity :: Lens' Quantity TCEnv Source #

eDisplayFormsEnabled :: Lens' Bool TCEnv Source #

eRange :: Lens' Range TCEnv Source #

eHighlightingRange :: Lens' Range TCEnv Source #

eCall :: Lens' (Maybe (Closure Call)) TCEnv Source #

eHighlightingLevel :: Lens' HighlightingLevel TCEnv Source #

eHighlightingMethod :: Lens' HighlightingMethod TCEnv Source #

eModuleNestingLevel :: Lens' Int TCEnv Source #

eExpandLast :: Lens' ExpandHidden TCEnv Source #

eAppDef :: Lens' (Maybe QName) TCEnv Source #

eSimplification :: Lens' Simplification TCEnv Source #

eAllowedReductions :: Lens' AllowedReductions TCEnv Source #

eInjectivityDepth :: Lens' Int TCEnv Source #

eCompareBlocked :: Lens' Bool TCEnv Source #

ePrintDomainFreePi :: Lens' Bool TCEnv Source #

eInsideDotPattern :: Lens' Bool TCEnv Source #

eUnquoteFlags :: Lens' UnquoteFlags TCEnv Source #

eInstanceDepth :: Lens' Int TCEnv Source #

eIsDebugPrinting :: Lens' Bool TCEnv Source #

ePrintingPatternLambdas :: Lens' [QName] TCEnv Source #

eCallByNeed :: Lens' Bool TCEnv Source #

eCurrentCheckpoint :: Lens' CheckpointId TCEnv Source #

eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv Source #

eGeneralizeMetas :: Lens' DoGeneralize TCEnv Source #

eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv Source #

## Context

type Context = [ContextEntry] Source #

The `Context` is a stack of `ContextEntry`s.

type ContextEntry = Dom (Name, Type) Source #

## Let bindings

type LetBindings = Map Name (Open (Term, Dom Type)) Source #

## Abstract mode

data AbstractMode Source #

Constructors

AbstractMode | Abstract things in the current module can be accessed.
ConcreteMode | No abstract things can be accessed.
IgnoreAbstractMode | All abstract things can be accessed.

Instances

Eq AbstractMode Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: AbstractMode -> AbstractMode -> Bool Source # (/=) :: AbstractMode -> AbstractMode -> Bool Source #
Data AbstractMode Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractMode -> c AbstractMode Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractMode Source #

toConstr :: AbstractMode -> Constr Source #

dataTypeOf :: AbstractMode -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractMode) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractMode) Source #

gmapT :: (forall b. Data b => b -> b) -> AbstractMode -> AbstractMode Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AbstractMode -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractMode -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode Source #

Show AbstractMode Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AbstractMode -> ShowS Source # show :: AbstractMode -> String Source # showList :: [AbstractMode] -> ShowS Source #

aDefToMode :: IsAbstract -> AbstractMode Source #

aModeToDef :: AbstractMode -> IsAbstract Source #

## Insertion of implicit arguments

data ExpandHidden Source #

Constructors

ExpandLast | Add implicit arguments in the end until type is no longer hidden `Pi`.
DontExpandLast | Do not append implicit arguments.

Instances

Eq ExpandHidden Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ExpandHidden -> ExpandHidden -> Bool Source # (/=) :: ExpandHidden -> ExpandHidden -> Bool Source #
Data ExpandHidden Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandHidden -> c ExpandHidden Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandHidden Source #

toConstr :: ExpandHidden -> Constr Source #

dataTypeOf :: ExpandHidden -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandHidden) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandHidden) Source #

gmapT :: (forall b. Data b => b -> b) -> ExpandHidden -> ExpandHidden Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ExpandHidden -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandHidden -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden Source #

data Candidate Source #

A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.

Constructors

Candidate |

Fields

- candidateTerm :: Term
- candidateType :: Type
- candidateOverlappable :: Bool

Instances

Eq Candidate Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Candidate -> Candidate -> Bool Source # (/=) :: Candidate -> Candidate -> Bool Source #
Data Candidate Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Candidate -> c Candidate Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Candidate Source #

toConstr :: Candidate -> Constr Source #

dataTypeOf :: Candidate -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Candidate) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Candidate) Source #

gmapT :: (forall b. Data b => b -> b) -> Candidate -> Candidate Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Candidate -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Candidate -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate Source #

Show Candidate Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Candidate -> ShowS Source # show :: Candidate -> String Source # showList :: [Candidate] -> ShowS Source #
Free Candidate Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Candidate -> FreeM c Source #
InstantiateFull Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Candidate -> ReduceM Candidate Source #
Normalise Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Candidate -> ReduceM Candidate Source #
Simplify Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Candidate -> ReduceM Candidate Source #
Reduce Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Candidate -> ReduceM Candidate Source # reduceB' :: Candidate -> ReduceM (Blocked Candidate) Source #
Instantiate Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Candidate -> ReduceM Candidate Source #
Subst Term Candidate Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source #

# Type checking warnings (aka non-fatal errors)

data Warning Source #

A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.

Constructors

NicifierIssue DeclarationWarning |
TerminationIssue [TerminationError] |
UnreachableClauses QName [[NamedArg DeBruijnPattern]] |
CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])] | `CoverageIssue f pss` means that `pss` are not covered in `f`
CoverageNoExactSplit QName [Clause] |
NotStrictlyPositive QName (Seq OccursWhere) |
UnsolvedMetaVariables [Range] | Do not use directly with `warning`
UnsolvedInteractionMetas [Range] | Do not use directly with `warning`
UnsolvedConstraints Constraints | Do not use directly with `warning`
CantGeneralizeOverSorts [MetaId] |
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern] |
OldBuiltin String String | In `OldBuiltin old new`, the BUILTIN old has been replaced by new
EmptyRewritePragma | If the user wrote just `{-# REWRITE #-}`.
IllformedAsClause String | If the user wrote something other than an unqualified name in the `as` clause of an `import` statement. The `String` gives optionally extra explanation.
UselessPublic | If the user opens a module public before the module header. (See issue #2377.)
UselessInline QName |
WrongInstanceDeclaration |
InstanceWithExplicitArg QName | An instance was declared with an implicit argument, which means it will never actually be considered by instance search.
InstanceNoOutputTypeName Doc | The type of an instance argument doesn't end in a named or variable type, so it will never be considered by instance search.
InstanceArgWithExplicitArg Doc | As InstanceWithExplicitArg, but for local bindings rather than top-level instances.
InversionDepthReached QName | The --inversion-max-depth was reached. Generic warnings for one-off things
GenericWarning Doc | Harmless generic warning (not an error)
GenericNonFatalError Doc | Generic error which doesn't abort proceedings (not a warning) Safe flag errors
SafeFlagPostulate Name |
SafeFlagPragma [String] |
SafeFlagNonTerminating |
SafeFlagTerminating |
SafeFlagWithoutKFlagPrimEraseEquality |
WithoutKFlagPrimEraseEquality |
SafeFlagNoPositivityCheck |
SafeFlagPolarity |
SafeFlagNoUniverseCheck |
ParseWarning ParseWarning |
LibraryWarning LibWarning |
DeprecationWarning String String String | `DeprecationWarning old new version`: `old` is deprecated, use `new` instead. This will be an error in Agda `version`.
UserWarning String | User-defined warning (e.g. to mention that a name is deprecated)
ModuleDoesntExport QName [ImportedName] | Some imported names are not actually exported by the source module
InfectiveImport String ModuleName | Importing a file using an infective option into one which doesn't
CoInfectiveImport String ModuleName | Importing a file not using a coinfective option from one which does

Instances

Data Warning Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Warning -> c Warning Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Warning Source #

toConstr :: Warning -> Constr Source #

dataTypeOf :: Warning -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Warning) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Warning) Source #

gmapT :: (forall b. Data b => b -> b) -> Warning -> Warning Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Warning -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Warning -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Warning -> m Warning Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning Source #

Show Warning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Warning -> ShowS Source # show :: Warning -> String Source # showList :: [Warning] -> ShowS Source #
EmbPrj Warning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Int32 Source # icod_ :: Warning -> S Int32 Source # value :: Int32 -> R Warning Source #
PrettyTCM Warning Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Warning -> TCM Doc Source #

warningName :: Warning -> WarningName Source #

data TCWarning Source #

Constructors

TCWarning |

Fields

- tcWarningRange :: Range

  Range where the warning was raised

- tcWarning :: Warning

  The warning itself

- tcWarningPrintedWarning :: Doc

  The warning printed in the state and environment where it was raised

- tcWarningCached :: Bool

  Should the warning be affected by caching.

Instances

Eq TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: TCWarning -> TCWarning -> Bool Source # (/=) :: TCWarning -> TCWarning -> Bool Source #
Show TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCWarning -> ShowS Source # show :: TCWarning -> String Source # showList :: [TCWarning] -> ShowS Source #
HasRange TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCWarning -> Range Source #
EmbPrj TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Int32 Source # icod_ :: TCWarning -> S Int32 Source # value :: Int32 -> R TCWarning Source #
PrettyTCM TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCWarning -> TCM Doc Source #

tcWarningOrigin :: TCWarning -> SrcFile Source #

equalHeadConstructors :: Warning -> Warning -> Bool Source #

getPartialDefs :: ReadTCState tcm => tcm [QName] Source #

# Type checking errors

data CallInfo Source #

Information about a call.

Constructors

CallInfo |

Fields

- callInfoTarget :: QName

  Target function name.

- callInfoRange :: Range

  Range of the target function.

- callInfoCall :: Closure Term

  To be formatted representation of the call.

Instances

Data CallInfo Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CallInfo -> c CallInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CallInfo Source #

toConstr :: CallInfo -> Constr Source #

dataTypeOf :: CallInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CallInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CallInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> CallInfo -> CallInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CallInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CallInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo Source #

Show CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CallInfo -> ShowS Source # show :: CallInfo -> String Source # showList :: [CallInfo] -> ShowS Source #
Pretty CallInfo Source # | We only `show` the name of the callee.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CallInfo -> Doc Source # prettyPrec :: Int -> CallInfo -> Doc Source # prettyList :: [CallInfo] -> Doc Source #
AllNames CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allNames :: CallInfo -> Seq QName Source #
PrettyTCM CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: CallInfo -> TCM Doc Source #

data TerminationError Source #

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError |

Fields

- termErrFunctions :: [QName]

  The functions which failed to check. (May not include automatically generated functions.)

- termErrCalls :: [CallInfo]

  The problematic call sites.

Instances

Data TerminationError Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationError -> c TerminationError Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TerminationError Source #

toConstr :: TerminationError -> Constr Source #

dataTypeOf :: TerminationError -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TerminationError) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TerminationError) Source #

gmapT :: (forall b. Data b => b -> b) -> TerminationError -> TerminationError Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TerminationError -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationError -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError Source #

Show TerminationError Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TerminationError -> ShowS Source # show :: TerminationError -> String Source # showList :: [TerminationError] -> ShowS Source #

data SplitError Source #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type) | Neither data type nor record.
IrrelevantDatatype (Closure Type) | Data type, but in irrelevant position.
ErasedDatatype (Closure Type) | Data type, but in erased position.
CoinductiveDatatype (Closure Type) | Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor
UnificationStuck |

Fields

- cantSplitConName :: QName

  Constructor.

- cantSplitTel :: Telescope

  Context for indices.

- cantSplitConIdx :: Args

  Inferred indices (from type of constructor).

- cantSplitGivenIdx :: Args

  Expected indices (from checking pattern).

- cantSplitFailures :: [UnificationFailure]

  Reason(s) why unification got stuck.

CosplitCatchall | Copattern split with a catchall
CosplitNoTarget | We do not know the target type of the clause.
CosplitNoRecordType (Closure Type) | Target type is not a record type.
CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type)) |
GenericSplitError String |

Instances

Show SplitError Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> SplitError -> ShowS Source # show :: SplitError -> String Source # showList :: [SplitError] -> ShowS Source #
PrettyTCM SplitError Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: SplitError -> TCM Doc Source #

data NegativeUnification Source #

Constructors

UnifyConflict Telescope Term Term |
UnifyCycle Telescope Int Term |

Instances

Show NegativeUnification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NegativeUnification -> ShowS Source # show :: NegativeUnification -> String Source # showList :: [NegativeUnification] -> ShowS Source #
PrettyTCM NegativeUnification Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: NegativeUnification -> TCM Doc Source #

data UnificationFailure Source #

Constructors

UnifyIndicesNotVars Telescope Type Term Term Args | Failed to apply injectivity to constructor of indexed datatype
UnifyRecursiveEq Telescope Type Int Term | Can't solve equation because variable occurs in (type of) lhs
UnifyReflexiveEq Telescope Type Term | Can't solve reflexive equation because --without-K is enabled

Instances

Show UnificationFailure Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnificationFailure -> ShowS Source # show :: UnificationFailure -> String Source # showList :: [UnificationFailure] -> ShowS Source #
PrettyTCM UnificationFailure Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: UnificationFailure -> TCM Doc Source #

data UnquoteError Source #

Constructors

BadVisibility String (Arg Term) |
ConInsteadOfDef QName String String |
DefInsteadOfCon QName String String |
NonCanonical String Term |
BlockedOnMeta TCState MetaId |
UnquotePanic String |

Instances

Show UnquoteError Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnquoteError -> ShowS Source # show :: UnquoteError -> String Source # showList :: [UnquoteError] -> ShowS Source #

data TypeError Source #

Constructors

InternalError String |
NotImplemented String |
NotSupported String |
CompilationError String |
PropMustBeSingleton |
DataMustEndInSort Term |
ShouldEndInApplicationOfTheDatatype Type | The target of a constructor isn't an application of its datatype. The `Type` records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term Term | The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.
ShouldBeApplicationOf Type QName | Expected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QName | constructor, datatype
CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName] | Datatype, constructors.
DoesNotConstructAnElementOf QName Type | constructor, type
WrongHidingInLHS | The left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda Type | Expected a non-hidden function and found a hidden lambda.
WrongHidingInApplication Type | A function is applied to a hidden argument where a non-hidden was expected.
WrongNamedArgument (NamedArg Expr) | A function is applied to a hidden named argument it does not have.
WrongIrrelevanceInLambda | Wrong user-given relevance annotation in lambda.
WrongQuantityInLambda | Wrong user-given quantity annotation in lambda.
HidingMismatch Hiding Hiding | The given hiding does not correspond to the expected hiding.
RelevanceMismatch Relevance Relevance | The given relevance does not correspond to the expected relevane.
UninstantiatedDotPattern Expr |
ForcedConstructorNotInstantiated Pattern |
IlltypedPattern Pattern Type |
IllformedProjectionPattern Pattern |
CannotEliminateWithPattern (NamedArg Pattern) Type |
WrongNumberOfConstructorArguments QName Nat Nat |
ShouldBeEmpty Type [DeBruijnPattern] |
ShouldBeASort Type | The given type should have been a sort.
ShouldBePi Type | The given type should have been a pi.
ShouldBePath Type |
ShouldBeRecordType Type |
ShouldBeRecordPattern DeBruijnPattern |
NotAProjectionPattern (NamedArg Pattern) |
NotAProperTerm |
InvalidTypeSort Sort | This sort is not a type expression.
InvalidType Term | This term is not a type expression.
FunctionTypeInSizeUniv Term | This term, a function type constructor, lives in `SizeUniv`, which is not allowed.
SplitOnIrrelevant (Dom Type) |
SplitOnNonVariable Term Type |
DefinitionIsIrrelevant QName |
VariableIsIrrelevant Name |
VariableIsErased Name |
UnequalTerms Comparison Term Term Type |
UnequalTypes Comparison Type Type |
UnequalRelevance Comparison Term Term | The two function types have different relevance.
UnequalHiding Term Term | The two function types have different hiding.
UnequalSorts Sort Sort |
UnequalBecauseOfUniverseConflict Comparison Term Term |
NotLeqSort Sort Sort |
MetaCannotDependOn MetaId [Nat] Nat | The arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.
MetaOccursInItself MetaId |
MetaIrrelevantSolution MetaId Term |
GenericError String |
GenericDocError Doc |
BuiltinMustBeConstructor String Expr |
NoSuchBuiltinName String |
DuplicateBuiltinBinding String Term Term |
NoBindingForBuiltin String |
NoSuchPrimitiveFunction String |
DuplicatePrimitiveBinding String QName QName |
ShadowedModule Name [ModuleName] |
BuiltinInParameterisedModule String |
IllegalLetInTelescope TypedBinding |
NoRHSRequiresAbsurdPattern [NamedArg Pattern] |
TooManyFields QName [Name] [Name] | Record type, fields not supplied by user, non-fields not supplied.
DuplicateFields [Name] |
DuplicateConstructors [Name] |
WithOnFreeVariable Expr Term |
UnexpectedWithPatterns [Pattern] |
WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern) |
FieldOutsideRecord |
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] |
GeneralizeCyclicDependency |
GeneralizeUnsolvedMeta |
SplitError SplitError |
ImpossibleConstructor QName NegativeUnification |
TooManyPolarities QName Int |
LocalVsImportedModuleClash ModuleName |
SolvedButOpenHoles | Some interaction points (holes) have not been filled by user. There are not `UnsolvedMetas` since unification solved them. This is an error, since interaction points are never filled without user interaction.
CyclicModuleDependency [TopLevelModuleName] |
FileNotFound TopLevelModuleName [AbsolutePath] |
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName |
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] |
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName | Found module name, expected module name.
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] |
ClashingFileNamesFor ModuleName [AbsolutePath] |
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath | Module name, file from which it was loaded, file which the include path says contains the module. Scope errors
BothWithAndRHS |
AbstractConstructorNotInScope QName |
NotInScope [QName] |
NoSuchModule QName |
AmbiguousName QName (NonemptyList QName) |
AmbiguousModule QName (NonemptyList ModuleName) |
ClashingDefinition QName QName |
ClashingModule ModuleName ModuleName |
ClashingImport Name QName |
ClashingModuleImport Name ModuleName |
PatternShadowsConstructor Name QName |
DuplicateImports QName [ImportedName] |
InvalidPattern Pattern |
RepeatedVariablesInPattern [Name] |
GeneralizeNotSupportedHere QName |
MultipleFixityDecls [(Name, [Fixity'])] |
MultiplePolarityPragmas [Name] |
NotAModuleExpr Expr | The expr was used in the right hand side of an implicit module definition, but it wasn't of the form `m Delta`.
NotAnExpression Expr |
NotAValidLetBinding NiceDeclaration |
NotValidBeforeField NiceDeclaration |
NothingAppliedToHiddenArg Expr |
NothingAppliedToInstanceArg Expr |
BadArgumentsToPatternSynonym AmbiguousQName |
TooFewArgumentsToPatternSynonym AmbiguousQName |
CannotResolveAmbiguousPatternSynonym (NonemptyList (QName, PatternSynDefn)) |
UnusedVariableInPatternSynonym |
NoParseForApplication [Expr] |
AmbiguousParseForApplication [Expr] [Expr] |
NoParseForLHS LHSOrPatSyn Pattern |
AmbiguousParseForLHS LHSOrPatSyn Pattern [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 |

Instances

Show TypeError Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TypeError -> ShowS Source # show :: TypeError -> String Source # showList :: [TypeError] -> ShowS Source #
PrettyTCM TypeError Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TypeError -> TCM Doc Source #

data LHSOrPatSyn Source #

Distinguish error message when parsing lhs or pattern synonym, resp.

Constructors

IsLHS |
IsPatSyn |

Instances

Eq LHSOrPatSyn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool Source # (/=) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool Source #
Show LHSOrPatSyn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> LHSOrPatSyn -> ShowS Source # show :: LHSOrPatSyn -> String Source # showList :: [LHSOrPatSyn] -> ShowS Source #

data TCErr Source #

Type-checking errors.

Constructors

TypeError |

Fields

- tcErrState :: TCState

  The state in which the error was raised.

- tcErrClosErr :: Closure TypeError

  The environment in which the error as raised plus the error.

Exception Range Doc |
IOException TCState Range IOException | The first argument is the state in which the error was raised.
PatternErr | The exception which is usually caught. Raised for pattern violations during unification (`assignV`) but also in other situations where we want to backtrack.

Instances

Show TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCErr -> ShowS Source # show :: TCErr -> String Source # showList :: [TCErr] -> ShowS Source #
Exception TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toException :: TCErr -> SomeException Source # fromException :: SomeException -> Maybe TCErr Source # displayException :: TCErr -> String Source #
Error TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods noMsg :: TCErr Source # strMsg :: String -> TCErr Source #
HasRange TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCErr -> Range Source #
PrettyTCM TCErr Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCErr -> TCM Doc Source #
MonadError TCErr IM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> IM a Source # catchError :: IM a -> (TCErr -> IM a) -> IM a Source #
MonadError TCErr TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods throwError :: TCErr -> TerM a Source # catchError :: TerM a -> (TCErr -> TerM a) -> TerM a Source #
MonadError TCErr (TCMT IO) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a Source # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a Source #

# Accessing options

class (Functor m, Applicative m, Monad m) => HasOptions m where Source #

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

Instances

HasOptions ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReduceM PragmaOptions Source # commandLineOptions :: ReduceM CommandLineOptions Source #
HasOptions TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions Source # commandLineOptions :: TerM CommandLineOptions Source #
HasOptions m => HasOptions (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: MaybeT m PragmaOptions Source # commandLineOptions :: MaybeT m CommandLineOptions Source #
HasOptions m => HasOptions (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ListT m PragmaOptions Source # commandLineOptions :: ListT m CommandLineOptions Source #
MonadIO m => HasOptions (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions Source # commandLineOptions :: TCMT m CommandLineOptions Source #
HasOptions m => HasOptions (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods pragmaOptions :: NamesT m PragmaOptions Source # commandLineOptions :: NamesT m CommandLineOptions Source #
HasOptions m => HasOptions (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source #
HasOptions m => HasOptions (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReaderT r m PragmaOptions Source # commandLineOptions :: ReaderT r m CommandLineOptions Source #
HasOptions m => HasOptions (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: StateT s m PragmaOptions Source # commandLineOptions :: StateT s m CommandLineOptions Source #
(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: WriterT w m PragmaOptions Source # commandLineOptions :: WriterT w m CommandLineOptions Source #

sizedTypesOption :: HasOptions m => m Bool Source #

guardednessOption :: HasOptions m => m Bool Source #

withoutKOption :: HasOptions m => m Bool Source #

# The reduce monad

data ReduceEnv Source #

Environment of the reduce monad.

Constructors

ReduceEnv |

Fields

- redEnv :: TCEnv

  Read only access to environment.

- redSt :: TCState

  Read only access to state (signature, metas...).

mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv Source #

mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv Source #

mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv Source #

reduceEnv :: Lens' TCEnv ReduceEnv Source #

reduceSt :: Lens' TCState ReduceEnv Source #

newtype ReduceM a Source #

Constructors

ReduceM |

Fields

- unReduceM :: ReduceEnv -> a

Instances

Monad ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (>>=) :: ReduceM a -> (a -> ReduceM b) -> ReduceM b Source # (>>) :: ReduceM a -> ReduceM b -> ReduceM b Source # return :: a -> ReduceM a Source # fail :: String -> ReduceM a Source #
Functor ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> ReduceM a -> ReduceM b Source # (<$) :: a -> ReduceM b -> ReduceM a Source #
MonadFail ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fail :: String -> ReduceM a Source #
Applicative ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pure :: a -> ReduceM a Source # (<*>) :: ReduceM (a -> b) -> ReduceM a -> ReduceM b Source # liftA2 :: (a -> b -> c) -> ReduceM a -> ReduceM b -> ReduceM c Source # (*>) :: ReduceM a -> ReduceM b -> ReduceM b Source # (<*) :: ReduceM a -> ReduceM b -> ReduceM a Source #
MonadTCEnv ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ReduceM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a Source #
MonadReduce ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ReduceM a Source #
HasOptions ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReduceM PragmaOptions Source # commandLineOptions :: ReduceM CommandLineOptions Source #
ReadTCState ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ReduceM TCState Source # withTCState :: (TCState -> TCState) -> ReduceM a -> ReduceM a Source #
MonadDebug ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods displayDebugMessage :: Int -> String -> ReduceM () Source # traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String Source #
HasConstInfo ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getConstInfo :: QName -> ReduceM Definition Source # getConstInfo' :: QName -> ReduceM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ReduceM RewriteRules Source #
HasBuiltins ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #

onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a Source #

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b Source #

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b Source #

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b Source #

runReduceM :: ReduceM a -> TCM a Source #

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source #

useR :: ReadTCState m => Lens' a TCState -> m a Source #

askR :: ReduceM ReduceEnv Source #

localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a Source #

class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where Source #

Methods

liftReduce :: ReduceM a -> m a Source #

Instances

MonadReduce ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ReduceM a Source #
MonadReduce TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods liftReduce :: ReduceM a -> TerM a Source #
MonadReduce m => MonadReduce (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> MaybeT m a Source #
MonadReduce m => MonadReduce (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ListT m a Source #
MonadIO m => MonadReduce (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> TCMT m a Source #
MonadReduce m => MonadReduce (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods liftReduce :: ReduceM a -> NamesT m a Source #
MonadReduce m => MonadReduce (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ExceptT err m a Source #
MonadReduce m => MonadReduce (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ReaderT r m a Source #
MonadReduce m => MonadReduce (StateT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> StateT w m a Source #
(Monoid w, MonadReduce m) => MonadReduce (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> WriterT w m a Source #

# Monad with read-only `TCEnv`

class Monad m => MonadTCEnv m where Source #

`MonadTCEnv` made into its own dedicated service class. This allows us to use `MonadReader` for `ReaderT` extensions of `TCM`.

Methods

askTC :: m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> m a -> m a Source #

Instances

MonadTCEnv ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ReduceM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a Source #
MonadTCEnv TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods askTC :: TerM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #
MonadTCEnv m => MonadTCEnv (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: MaybeT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> MaybeT m a -> MaybeT m a Source #
MonadTCEnv m => MonadTCEnv (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ListT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ListT m a -> ListT m a Source #
MonadIO m => MonadTCEnv (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: TCMT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #
MonadTCEnv m => MonadTCEnv (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods askTC :: NamesT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a Source #
MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ExceptT err m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ExceptT err m a -> ExceptT err m a Source #
MonadTCEnv m => MonadTCEnv (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: ReaderT r m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> ReaderT r m a -> ReaderT r m a Source #
MonadTCEnv m => MonadTCEnv (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: StateT s m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> StateT s m a -> StateT s m a Source #
(Monoid w, MonadTCEnv m) => MonadTCEnv (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: WriterT w m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> WriterT w m a -> WriterT w m a Source #

asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a Source #

viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a Source #

locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b Source #

Modify the lens-indicated part of the `TCEnv` in a subcomputation.

# Monad with mutable `TCState`

class Monad m => MonadTCState m where Source #

`MonadTCState` made into its own dedicated service class. This allows us to use `MonadState` for `StateT` extensions of `TCM`.

Minimal complete definition

getTC, (putTC | modifyTC)

Methods

getTC :: m TCState Source #

putTC :: TCState -> m () Source #

modifyTC :: (TCState -> TCState) -> m () Source #

Instances

MonadTCState TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getTC :: TerM TCState Source # putTC :: TCState -> TerM () Source # modifyTC :: (TCState -> TCState) -> TerM () Source #
MonadTCState m => MonadTCState (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: MaybeT m TCState Source # putTC :: TCState -> MaybeT m () Source # modifyTC :: (TCState -> TCState) -> MaybeT m () Source #
MonadTCState m => MonadTCState (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: ListT m TCState Source # putTC :: TCState -> ListT m () Source # modifyTC :: (TCState -> TCState) -> ListT m () Source #
MonadIO m => MonadTCState (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: TCMT m TCState Source # putTC :: TCState -> TCMT m () Source # modifyTC :: (TCState -> TCState) -> TCMT m () Source #
MonadTCState m => MonadTCState (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getTC :: NamesT m TCState Source # putTC :: TCState -> NamesT m () Source # modifyTC :: (TCState -> TCState) -> NamesT m () Source #
MonadTCState m => MonadTCState (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: ExceptT err m TCState Source # putTC :: TCState -> ExceptT err m () Source # modifyTC :: (TCState -> TCState) -> ExceptT err m () Source #
MonadTCState m => MonadTCState (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: ReaderT r m TCState Source # putTC :: TCState -> ReaderT r m () Source # modifyTC :: (TCState -> TCState) -> ReaderT r m () Source #
MonadTCState m => MonadTCState (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: StateT s m TCState Source # putTC :: TCState -> StateT s m () Source # modifyTC :: (TCState -> TCState) -> StateT s m () Source #
(Monoid w, MonadTCState m) => MonadTCState (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: WriterT w m TCState Source # putTC :: TCState -> WriterT w m () Source # modifyTC :: (TCState -> TCState) -> WriterT w m () Source #

## `TCState` accessors (no lenses)

getsTC :: MonadTCState m => (TCState -> a) -> m a Source #

modifyTC' :: MonadTCState m => (TCState -> TCState) -> m () Source #

A variant of `modifyTC` in which the computation is strict in the new state.

## `TCState` accessors via lenses

useTC :: MonadTCState m => Lens' a TCState -> m a Source #

setTCLens :: MonadTCState m => Lens' a TCState -> a -> m () infix 4 Source #

Overwrite the part of the `TCState` focused on by the lens.

modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m () Source #

Modify the part of the `TCState` focused on by the lens.

modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m () Source #

Modify a part of the state monadically.

locallyTCState :: MonadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b Source #

Modify the lens-indicated part of the `TCState` locally.

# Type checking monad transformer

newtype TCMT m a Source #

The type checking monad transformer. Adds readonly `TCEnv` and mutable `TCState`.

Constructors

TCM |

Fields

- unTCM :: IORef TCState -> TCEnv -> m a

Instances

MonadTrans TCMT Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lift :: Monad m => m a -> TCMT m a Source #
MonadFixityError ScopeM Source # |

Instance details

Defined in Agda.Syntax.Scope.Monad

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> ScopeM a Source #

throwMultiplePolarityPragmas :: [Name] -> ScopeM a Source #

warnUnknownNamesInFixityDecl :: [Name] -> ScopeM () Source #

warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM () Source #

warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM () Source #

warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM () Source #

MonadError TCErr IM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> IM a Source # catchError :: IM a -> (TCErr -> IM a) -> IM a Source #
MonadBench Phase TCM Source # | We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getBenchmark :: TCM (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> TCM c Source # putBenchmark :: Benchmark Phase -> TCM () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM () Source # finally :: TCM b -> TCM c -> TCM b Source #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
MonadError TCErr (TCMT IO) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a Source # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg a -> TOM (Hiding, b) Source #
MonadIO m => Monad (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b Source # (>>) :: TCMT m a -> TCMT m b -> TCMT m b Source # return :: a -> TCMT m a Source # fail :: String -> TCMT m a Source #
MonadIO m => Functor (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> TCMT m a -> TCMT m b Source # (<$) :: a -> TCMT m b -> TCMT m a Source #
MonadIO m => MonadFail (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fail :: String -> TCMT m a Source #
MonadIO m => Applicative (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pure :: a -> TCMT m a Source # (<*>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b Source # liftA2 :: (a -> b -> c) -> TCMT m a -> TCMT m b -> TCMT m c Source # (*>) :: TCMT m a -> TCMT m b -> TCMT m b Source # (<*) :: TCMT m a -> TCMT m b -> TCMT m a Source #
Semigroup (TCM Any) Source # | Short-cutting disjunction forms a monoid.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: TCM Any -> TCM Any -> TCM Any Source # sconcat :: NonEmpty (TCM Any) -> TCM Any Source # stimes :: Integral b => b -> TCM Any -> TCM Any Source #
Monoid (TCM Any) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods mempty :: TCM Any Source # mappend :: TCM Any -> TCM Any -> TCM Any Source # mconcat :: [TCM Any] -> TCM Any Source #
MonadIO m => MonadIO (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftIO :: IO a -> TCMT m a Source #
Null (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
MonadIO m => MonadTCM (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> TCMT m a Source #
MonadIO m => MonadTCState (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTC :: TCMT m TCState Source # putTC :: TCState -> TCMT m () Source # modifyTC :: (TCState -> TCState) -> TCMT m () Source #
MonadIO m => MonadTCEnv (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods askTC :: TCMT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #
MonadIO m => MonadReduce (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> TCMT m a Source #
MonadIO m => HasOptions (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions Source # commandLineOptions :: TCMT m CommandLineOptions Source #
MonadIO m => ReadTCState (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: TCMT m TCState Source # withTCState :: (TCState -> TCState) -> TCMT m a -> TCMT m a Source #
MonadIO m => MonadDebug (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> TCMT m () Source # traceDebugMessage :: Int -> String -> TCMT m a -> TCMT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TCMT m String Source #
HasConstInfo (TCMT IO) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> TCMT IO Definition Source # getConstInfo' :: QName -> TCMT IO (Either SigError Definition) Source # getRewriteRulesFor :: QName -> TCMT IO RewriteRules Source #
MonadIO m => HasBuiltins (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #
(IsString a, MonadIO m) => IsString (TCMT m a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fromString :: String -> TCMT m a Source #

type TCM = TCMT IO Source #

class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where Source #

Methods

liftTCM :: TCM a -> tcm a Source #

Instances

MonadTCM TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods liftTCM :: TCM a -> TerM a Source #
MonadTCM tcm => MonadTCM (MaybeT tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> MaybeT tcm a Source #
MonadTCM tcm => MonadTCM (ListT tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ListT tcm a Source #
MonadIO m => MonadTCM (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> TCMT m a Source #
MonadTCM m => MonadTCM (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods liftTCM :: TCM a -> NamesT m a Source #
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ExceptT err tcm a Source #
MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ReaderT r tcm a Source #
MonadTCM tcm => MonadTCM (StateT s tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> StateT s tcm a Source #
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> WriterT w tcm a Source #

type IM = TCMT (InputT IO) Source #

Interaction monad.

runIM :: IM a -> TCM a Source #

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source #

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a Source #

Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a Source #

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a Source #

returnTCMT :: MonadIO m => a -> TCMT m a Source #

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b Source #

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b Source #

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b Source #

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b Source #

patternViolation :: TCM a Source #

internalError :: MonadTCM tcm => String -> tcm a Source #

genericError :: MonadTCM tcm => String -> tcm a Source #

genericDocError :: MonadTCM tcm => Doc -> tcm a Source #

typeError :: MonadTCM tcm => TypeError -> tcm a Source #

typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr Source #

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source #

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) Source #

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a Source #

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source #

`runSafeTCM` runs a safe `TCMT` action (a `TCMT` action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () Source #

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to `forkTCM` tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The `forkTCM` function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

extendedLambdaName :: String Source #

Base name for extended lambda patterns

isExtendedLambdaName :: QName -> Bool Source #

Check whether we have an definition from an extended lambda.

absurdLambdaName :: String Source #

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool Source #

Check whether we have an definition from an absurd lambda.

generalizedFieldName :: String Source #

Base name for generalized variable projections

getGeneralizedFieldName :: QName -> Maybe String Source #

Check whether we have a generalized variable field

# KillRange instances