Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Monad.Base
Contents
Type checking state
Interface
Closure
Constraints
Open things
Judgements
Meta variables
Interaction meta variables
Signature
Injectivity
Mutual blocks
Statistics
Trace
Builtin things
Type checking environment
Context
Let bindings
Abstract mode
Type checking errors
Type checking monad transformer
Synopsis
data TCState = TCSt {
stFreshThings :: FreshThings
stMetaStore :: MetaStore
stInteractionPoints :: InteractionPoints
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stModuleToSource :: ModuleToSource
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe ModuleName
stScope :: ScopeInfo
stPersistentOptions :: CommandLineOptions
stPragmaOptions :: PragmaOptions
stStatistics :: Statistics
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: Set String
}
data FreshThings = Fresh {
fMeta :: MetaId
fInteraction :: InteractionId
fMutual :: MutualId
fName :: NameId
fCtx :: CtxId
fInteger :: Integer
}
initState :: TCState
stBuiltinThings :: TCState -> BuiltinThings PrimFun
data ModuleInfo = ModuleInfo {
miInterface :: Interface
miWarnings :: Bool
miTimeStamp :: ClockTime
}
type VisitedModules = Map TopLevelModuleName ModuleInfo
type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)
data Interface = Interface {
iImportedModules :: [ModuleName]
iModuleName :: ModuleName
iScope :: Map ModuleName Scope
iInsideScope :: ScopeInfo
iSignature :: Signature
iBuiltin :: BuiltinThings String
iHaskellImports :: Set String
iHighlighting :: HighlightingInfo
iPragmaOptions :: [OptionsPragma]
}
data Closure a = Closure {
clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
clValue :: a
}
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
type ConstraintClosure = Closure Constraint
data Constraint
= ValueCmp Comparison Type Term Term
| ArgsCmp [Polarity] Type Args Args
| TypeCmp Comparison Type Type
| TelCmp Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Term Term
| UnBlock MetaId
| Guarded Constraint Constraints
| IsEmpty Type
data Comparison
= CmpEq
| CmpLeq
type Constraints = [ConstraintClosure]
data Open a = OpenThing [CtxId] a
data Judgement t a
= HasType a t
| IsSort a
data MetaVariable = MetaVar {
mvInfo :: MetaInfo
mvPriority :: MetaPriority
mvPermutation :: Permutation
mvJudgement :: Judgement Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaId
}
data MetaInstantiation
= InstV Term
| InstS Term
| Open
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))
newtype MetaPriority = MetaPriority Int
type MetaInfo = Closure Range
type MetaStore = Map MetaId MetaVariable
normalMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
getMetaInfo :: MetaVariable -> MetaInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
type InteractionPoints = Map InteractionId MetaId
newtype InteractionId = InteractionId Nat
data Signature = Sig {
sigSections :: Sections
sigDefinitions :: Definitions
}
type Sections = Map ModuleName Section
type Definitions = Map QName Definition
data Section = Section {
secTelescope :: Telescope
secFreeVars :: Nat
}
emptySignature :: Signature
data DisplayForm = Display Nat [Term] DisplayTerm
data DisplayTerm
= DWithApp [DisplayTerm] Args
| DTerm Term
defaultDisplayForm :: QName -> [Open DisplayForm]
data Definition = Defn {
defRelevance :: Relevance
defName :: QName
defType :: Type
defDisplay :: [Open DisplayForm]
defMutual :: MutualId
theDef :: Defn
}
type HaskellCode = String
type HaskellType = String
type EpicCode = String
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
data Polarity
= Covariant
| Contravariant
| Invariant
data Occurrence
= Positive
| Negative
| Unused
data Defn
= Axiom {
axHsDef :: Maybe HaskellRepresentation
axEpDef :: Maybe EpicCode
}
| Function {
funClauses :: [Clauses]
funCompiled :: CompiledClauses
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: Delayed
funProjection :: Maybe Int
}
| Datatype {
dataPars :: Nat
dataIxs :: Nat
dataInduction :: Induction
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataPolarity :: [Polarity]
dataArgOccurrences :: [Occurrence]
dataHsType :: Maybe HaskellType
dataAbstr :: IsAbstract
}
| Record {
recPars :: Nat
recClause :: Maybe Clause
recCon :: QName
recNamedCon :: Bool
recConType :: Type
recFields :: [Arg QName]
recTel :: Telescope
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recEtaEquality :: Bool
recAbstr :: IsAbstract
}
| Constructor {
conPars :: Nat
conSrcCon :: QName
conData :: QName
conHsCode :: Maybe (HaskellType, HaskellCode)
conAbstr :: IsAbstract
conInd :: Induction
}
| Primitive {
primAbstr :: IsAbstract
primName :: String
primClauses :: Maybe [Clauses]
primCompiled :: Maybe CompiledClauses
}
defIsRecord :: Defn -> Bool
newtype Fields = Fields [(Name, Type)]
data Reduced no yes
= NoReduction no
| YesReduction yes
data IsReduced
= NotReduced
| Reduced (Blocked ())
data MaybeReduced a = MaybeRed {
isReduced :: IsReduced
ignoreReduced :: a
}
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
notReduced :: a -> MaybeReduced a
reduced :: Blocked a -> MaybeReduced a
data PrimFun = PrimFun {
primFunName :: QName
primFunArity :: Arity
primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced MaybeReducedArgs Term)
}
defClauses :: Definition -> [Clauses]
defCompiled :: Definition -> Maybe CompiledClauses
data Delayed
= Delayed
| NotDelayed
defDelayed :: Definition -> Delayed
defAbstract :: Definition -> IsAbstract
data FunctionInverse
= NotInjective
| Inverse (Map TermHead Clause)
data TermHead
= SortHead
| PiHead
| ConHead QName
newtype MutualId = MutId Int32
type Statistics = Map String Int
data Call
= CheckClause Type Clause (Maybe Clause)
| forall a . CheckPattern Pattern Telescope Type (Maybe a)
| CheckLetBinding LetBinding (Maybe ())
| InferExpr Expr (Maybe (Term, Type))
| CheckExpr Expr Type (Maybe Term)
| CheckDotPattern Expr Term (Maybe Constraints)
| CheckPatternShadowing Clause (Maybe ())
| IsTypeCall Expr Sort (Maybe Type)
| IsType_ Expr (Maybe Type)
| InferVar Name (Maybe (Term, Type))
| InferDef Range QName (Maybe (Term, Type))
| CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type, Constraints))
| CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
| CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
| CheckConstructor QName Telescope Sort Constructor (Maybe ())
| CheckFunDef Range Name [Clause] (Maybe ())
| CheckPragma Range Pragma (Maybe ())
| CheckPrimitive Range Name Expr (Maybe ())
| CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
| ScopeCheckExpr Expr (Maybe Expr)
| ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
| ScopeCheckLHS Name Pattern (Maybe LHS)
| ScopeCheckDefinition NiceDefinition (Maybe Definition)
| forall a . TermFunDef Range Name [Clause] (Maybe a)
| forall a . SetRange Range (Maybe a)
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
= Builtin Term
| Prim pf
data TCEnv = TCEnv {
envContext :: Context
envLetBindings :: LetBindings
envCurrentModule :: ModuleName
envAnonymousModules :: [(ModuleName, Nat)]
envImportPath :: [TopLevelModuleName]
envMutualBlock :: Maybe MutualId
envAbstractMode :: AbstractMode
envIrrelevant :: Bool
envReplace :: Bool
envDisplayFormsEnabled :: Bool
envReifyInteractionPoints :: Bool
envEtaContractImplicit :: Bool
envRange :: Range
envCall :: Maybe (Closure Call)
}
initEnv :: TCEnv
type Context = [ContextEntry]
data ContextEntry = Ctx {
ctxId :: CtxId
ctxEntry :: Arg (Name, Type)
}
newtype CtxId = CtxId Nat
type LetBindings = Map Name (Open (Term, Arg Type))
data AbstractMode
= AbstractMode
| ConcreteMode
| IgnoreAbstractMode
data Occ
= OccCon {
occDatatype :: QName
occConstructor :: QName
occPosition :: OccPos
}
| OccClause {
occFunction :: QName
occClause :: Int
occPosition :: OccPos
}
data OccPos
= NonPositively
| ArgumentTo Nat QName
data TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [([QName], [Range])]
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| IndicesNotConstructorApplications [Arg Term]
| IndexVariablesNotDistinct [Arg Term]
| IndexFreeInParameter Nat [Arg Term]
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| NotInductive Term
| UninstantiatedDotPattern Expr
| IlltypedPattern Pattern Type
| TooManyArgumentsInLHS Nat Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| NotAProperTerm
| SplitOnIrrelevant Pattern (Arg Type)
| DefinitionIsIrrelevant QName
| VariableIsIrrelevant Name
| UnequalLevel Comparison Term Term
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalRelevance Type Type
| UnequalHiding Type Type
| UnequalSorts Sort Sort
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| MetaOccursInItself MetaId
| GenericError String
| BuiltinMustBeConstructor String Expr
| NoSuchBuiltinName String
| DuplicateBuiltinBinding String Term Term
| NoBindingForBuiltin String
| NoSuchPrimitiveFunction String
| ShadowedModule [ModuleName]
| BuiltinInParameterisedModule String
| NoRHSRequiresAbsurdPattern [NamedArg Pattern]
| AbsurdPatternRequiresNoRHS [NamedArg Pattern]
| TooFewFields QName [Name]
| TooManyFields QName [Name]
| DuplicateFields [Name]
| DuplicateConstructors [Name]
| UnexpectedWithPatterns [Pattern]
| WithClausePatternMismatch Pattern Pattern
| FieldOutsideRecord
| ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
| IncompletePatternMatching Term Args
| CoverageFailure QName [[Arg Pattern]]
| UnreachableClauses QName [[Arg Pattern]]
| CoverageCantSplitOn QName
| CoverageCantSplitType Type
| NotStrictlyPositive QName [Occ]
| LocalVsImportedModuleClash ModuleName
| UnsolvedMetas [Range]
| UnsolvedConstraints Constraints
| CyclicModuleDependency [TopLevelModuleName]
| FileNotFound TopLevelModuleName [AbsolutePath]
| OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
| AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
| ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
| ClashingFileNamesFor ModuleName [AbsolutePath]
| ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
| BothWithAndRHS
| NotInScope [QName]
| NoSuchModule QName
| AmbiguousName QName [QName]
| AmbiguousModule QName [ModuleName]
| UninstantiatedModule QName
| ClashingDefinition QName QName
| ClashingModule ModuleName ModuleName
| ClashingImport Name QName
| ClashingModuleImport Name ModuleName
| PatternShadowsConstructor Name QName
| ModuleDoesntExport QName [ImportedName]
| DuplicateImports QName [ImportedName]
| InvalidPattern Pattern
| RepeatedVariablesInPattern [Name]
| NotAModuleExpr Expr
| NotAnExpression Expr
| NotAValidLetBinding NiceDeclaration
| NothingAppliedToHiddenArg Expr
| NoParseForApplication [Expr]
| AmbiguousParseForApplication [Expr] [Expr]
| NoParseForLHS Pattern
| AmbiguousParseForLHS Pattern [Pattern]
data TCErr'
= TypeError TCState (Closure TypeError)
| Exception Range String
| IOException Range IOException
| PatternErr TCState
| AbortAssign TCState
data TCErr = TCErr {
errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
errError :: TCErr'
}
newtype TCMT m a = TCM {
unTCM :: TCState -> TCEnv -> m (a, TCState)
}
type TCM = TCMT IO
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
liftTCM :: TCM a -> tcm a
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
patternViolation :: MonadTCM tcm => tcm a
internalError :: MonadTCM tcm => String -> tcm a
typeError :: MonadTCM tcm => TypeError -> tcm a
runTCM :: TCMT IO a -> IO (Either TCErr a)
runTCM' :: Monad m => TCMT m a -> m a
Type checking state
data TCState Source
Constructors
TCSt
stFreshThings :: FreshThings
stMetaStore :: MetaStore
stInteractionPoints :: InteractionPoints
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stModuleToSource :: ModuleToSource
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe ModuleNameThe current module is available after it has been type checked.
stScope :: ScopeInfo
stPersistentOptions :: CommandLineOptionsOptions which apply to all files, unless overridden.
stPragmaOptions :: PragmaOptionsOptions applying to the current file. OPTIONS pragmas only affect this field.
stStatistics :: Statistics
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: Set StringImports that should be generated by the compiler (this includes imports from imported modules).
data FreshThings Source
Constructors
Fresh
fMeta :: MetaId
fInteraction :: InteractionId
fMutual :: MutualId
fName :: NameId
fCtx :: CtxId
fInteger :: IntegerCan be used for various things.
initState :: TCStateSource
stBuiltinThings :: TCState -> BuiltinThings PrimFunSource
Interface
data ModuleInfo Source
Constructors
ModuleInfo
miInterface :: Interface
miWarnings :: BoolTrue if warnings were encountered when the module was type checked.
miTimeStamp :: ClockTimeThe modification time stamp of the interface file when the interface was read or written. Alternatively, if warnings were encountered (in which case there may not be any up-to-date interface file), the time at which the interface was produced (approximately).
type VisitedModules = Map TopLevelModuleName ModuleInfoSource
type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)Source
data Interface Source
Constructors
Interface
iImportedModules :: [ModuleName]
iModuleName :: ModuleName
iScope :: Map ModuleName Scope
iInsideScope :: ScopeInfo
iSignature :: Signature
iBuiltin :: BuiltinThings String
iHaskellImports :: Set StringHaskell imports listed in (transitively) imported modules are not included here.
iHighlighting :: HighlightingInfo
iPragmaOptions :: [OptionsPragma]Pragma options set in the file.
Closure
data Closure a Source
Constructors
Closure
clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
clValue :: a
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)Source
Constraints
type ConstraintClosure = Closure ConstraintSource
data Constraint Source
Constructors
ValueCmp Comparison Type Term Term
ArgsCmp [Polarity] Type Args Args
TypeCmp Comparison Type Type
TelCmp Comparison Telescope Telescope
SortCmp Comparison Sort Sort
LevelCmp Comparison Term Term
UnBlock MetaId
Guarded Constraint Constraints
IsEmpty Type
data Comparison Source
Constructors
CmpEq
CmpLeq
type Constraints = [ConstraintClosure]Source
Open things
data Open a Source
A thing tagged with the context it came from.
Constructors
OpenThing [CtxId] a
Judgements
data Judgement t a Source
Constructors
HasType a t
IsSort a
Meta variables
data MetaVariable Source
Constructors
MetaVar
mvInfo :: MetaInfo
mvPriority :: MetaPrioritysome metavariables are more eager to be instantiated
mvPermutation :: Permutationa 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 Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaIdmetavariables interested in what happens to this guy
data MetaInstantiation Source
Constructors
InstV Term
InstS Term
Open
BlockedConst Term
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))
newtype MetaPriority Source
Constructors
MetaPriority Int
type MetaInfo = Closure RangeSource
TODO: Not so nice.
type MetaStore = Map MetaId MetaVariableSource
normalMetaPriority :: MetaPrioritySource
lowMetaPriority :: MetaPrioritySource
highMetaPriority :: MetaPrioritySource
getMetaInfo :: MetaVariable -> MetaInfoSource
getMetaScope :: MetaVariable -> ScopeInfoSource
getMetaEnv :: MetaVariable -> TCEnvSource
getMetaSig :: MetaVariable -> SignatureSource
Interaction meta variables
type InteractionPoints = Map InteractionId MetaIdSource
newtype InteractionId Source
Constructors
InteractionId Nat
Signature
data Signature Source
Constructors
Sig
sigSections :: Sections
sigDefinitions :: Definitions
type Sections = Map ModuleName SectionSource
type Definitions = Map QName DefinitionSource
data Section Source
Constructors
Section
secTelescope :: Telescope
secFreeVars :: NatThis is the number of parameters when we're inside the section and 0 outside. It's used to know how much of the context to apply function from the section to when translating from abstract to internal syntax.
emptySignature :: SignatureSource
data DisplayForm Source
Constructors
Display Nat [Term] DisplayTerm

The three arguments are:

  • n: number of free variables;
  • Patterns for arguments, one extra free var which represents pattern vars. There should n of them.
  • Display form. n free variables.
data DisplayTerm Source
Constructors
DWithApp [DisplayTerm] Args
DTerm Term
defaultDisplayForm :: QName -> [Open DisplayForm]Source
data Definition Source
Constructors
Defn
defRelevance :: RelevanceSome defs can be irrelevant (but not hidden).
defName :: QName
defType :: TypeType of the lifted definition.
defDisplay :: [Open DisplayForm]
defMutual :: MutualId
theDef :: Defn
type HaskellCode = StringSource
type HaskellType = StringSource
type EpicCode = StringSource
data HaskellRepresentation Source
Constructors
HsDefn HaskellType HaskellCode
HsType HaskellType
data Polarity Source
Constructors
Covariant
Contravariant
Invariant
data Occurrence Source
Positive means strictly positive and Negative means not strictly positive.
Constructors
Positive
Negative
Unused
data Defn Source
Constructors
Axiom
axHsDef :: Maybe HaskellRepresentation
axEpDef :: Maybe EpicCode
Function
funClauses :: [Clauses]
funCompiled :: CompiledClauses
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: DelayedAre the clauses of this definition delayed?
funProjection :: Maybe IntIs it a record projection? If yes, then return the 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.
Datatype
dataPars :: Nat
dataIxs :: Nat
dataInduction :: Induction
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataPolarity :: [Polarity]
dataArgOccurrences :: [Occurrence]
dataHsType :: Maybe HaskellType
dataAbstr :: IsAbstract
Record
recPars :: Nat
recClause :: Maybe Clause
recCon :: QNameConstructor name.
recNamedCon :: Bool
recConType :: TypeThe record constructor's type.
recFields :: [Arg QName]
recTel :: Telescope
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recEtaEquality :: Bool
recAbstr :: IsAbstract
ConstructorNote that, currently, the sharp constructor is represented as a definition (Def), but if you look up the name you will get a Constructor.
conPars :: Nat
conSrcCon :: QName
conData :: QName
conHsCode :: Maybe (HaskellType, HaskellCode)
conAbstr :: IsAbstract
conInd :: InductionInductive or coinductive?
PrimitivePrimitive or builtin functions.
primAbstr :: IsAbstract
primName :: String
primClauses :: Maybe [Clauses]Nothing for primitive functions, Just something for builtin functions.
primCompiled :: Maybe CompiledClauses
defIsRecord :: Defn -> BoolSource
newtype Fields Source
Constructors
Fields [(Name, Type)]
data Reduced no yes Source
Constructors
NoReduction no
YesReduction yes
data IsReduced Source
Constructors
NotReduced
Reduced (Blocked ())
data MaybeReduced a Source
Constructors
MaybeRed
isReduced :: IsReduced
ignoreReduced :: a
type MaybeReducedArgs = [MaybeReduced (Arg Term)]Source
notReduced :: a -> MaybeReduced aSource
reduced :: Blocked a -> MaybeReduced aSource
data PrimFun Source
Constructors
PrimFun
primFunName :: QName
primFunArity :: Arity
primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced MaybeReducedArgs Term)
defClauses :: Definition -> [Clauses]Source
defCompiled :: Definition -> Maybe CompiledClausesSource
data Delayed Source
Used to specify whether something should be delayed.
Constructors
Delayed
NotDelayed
defDelayed :: Definition -> DelayedSource
Are the clauses of this definition delayed?
defAbstract :: Definition -> IsAbstractSource
Injectivity
data FunctionInverse Source
Constructors
NotInjective
Inverse (Map TermHead Clause)
data TermHead Source
Constructors
SortHead
PiHead
ConHead QName
Mutual blocks
newtype MutualId Source
Constructors
MutId Int32
Statistics
type Statistics = Map String IntSource
Trace
data Call Source
Constructors
CheckClause Type Clause (Maybe Clause)
forall a . CheckPattern Pattern Telescope Type (Maybe a)
CheckLetBinding LetBinding (Maybe ())
InferExpr Expr (Maybe (Term, Type))
CheckExpr Expr Type (Maybe Term)
CheckDotPattern Expr Term (Maybe Constraints)
CheckPatternShadowing Clause (Maybe ())
IsTypeCall Expr Sort (Maybe Type)
IsType_ Expr (Maybe Type)
InferVar Name (Maybe (Term, Type))
InferDef Range QName (Maybe (Term, Type))
CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type, Constraints))
CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
CheckConstructor QName Telescope Sort Constructor (Maybe ())
CheckFunDef Range Name [Clause] (Maybe ())
CheckPragma Range Pragma (Maybe ())
CheckPrimitive Range Name Expr (Maybe ())
CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
ScopeCheckExpr Expr (Maybe Expr)
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
ScopeCheckLHS Name Pattern (Maybe LHS)
ScopeCheckDefinition NiceDefinition (Maybe Definition)
forall a . TermFunDef Range Name [Clause] (Maybe a)
forall a . SetRange Range (Maybe a)used by setCurrentRange actually, a is Agda.Termination.TermCheck.CallGraph but I was to lazy to import the stuff here --Andreas,2007-5-29
Builtin things
type BuiltinThings pf = Map String (Builtin pf)Source
data Builtin pf Source
Constructors
Builtin Term
Prim pf
Type checking environment
data TCEnv Source
Constructors
TCEnv
envContext :: Context
envLetBindings :: LetBindings
envCurrentModule :: ModuleName
envAnonymousModules :: [(ModuleName, Nat)]anonymous modules and their number of free variables
envImportPath :: [TopLevelModuleName]to detect import cycles
envMutualBlock :: Maybe MutualIdthe current (if any) mutual block
envAbstractMode :: AbstractModeWhen 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.
envIrrelevant :: BoolAre we checking an irrelevant argument? Then top-level irrelevant declarations are enabled.
envReplace :: BoolCoinductive constructor applications c args get replaced by a function application f tel, where tel corresponds to the current telescope and f is defined as f tel = c args. The initial occurrence of c in the body of f should not be replaced by yet another function application, though. To avoid that this happens the envReplace flag is set to False when f is checked.
envDisplayFormsEnabled :: BoolSometimes we want to disable display forms.
envReifyInteractionPoints :: Boolshould we try to recover interaction points when reifying? disabled when generating types for with functions
envEtaContractImplicit :: Boolit's safe to eta contract implicit lambdas as long as we're not going to reify and retypecheck (like when doing with abstraction)
envRange :: Range
envCall :: Maybe (Closure Call)what we're doing at the moment
initEnv :: TCEnvSource
Context
type Context = [ContextEntry]Source
data ContextEntry Source
Constructors
Ctx
ctxId :: CtxId
ctxEntry :: Arg (Name, Type)
newtype CtxId Source
Constructors
CtxId Nat
Let bindings
type LetBindings = Map Name (Open (Term, Arg Type))Source
Abstract mode
data AbstractMode Source
Constructors
AbstractModeabstract things in the current module can be accessed
ConcreteModeno abstract things can be accessed
IgnoreAbstractModeall abstract things can be accessed
Type checking errors
data Occ Source
Constructors
OccCon
occDatatype :: QName
occConstructor :: QName
occPosition :: OccPos
OccClause
occFunction :: QName
occClause :: Int
occPosition :: OccPos
data OccPos Source
Constructors
NonPositively
ArgumentTo Nat QName
data TypeError Source
Constructors
InternalError String
NotImplemented String
NotSupported String
CompilationError String
TerminationCheckFailed [([QName], [Range])]Parameterised on functions which failed to termination check (grouped if they are mutual), along with ranges for problematic call sites.
PropMustBeSingleton
DataMustEndInSort Term
ShouldEndInApplicationOfTheDatatype TypeThe target of a constructor isn't an application of its datatype. The Type records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term TermThe 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 QNameExpected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QNameconstructor, datatype
IndicesNotConstructorApplications [Arg Term]Indices.
IndexVariablesNotDistinct [Arg Term]Indices.
IndexFreeInParameter Nat [Arg Term]Index (a variable), parameters.
DoesNotConstructAnElementOf QName Termconstructor, type
DifferentAritiesVarying number of arguments for a function.
WrongHidingInLHS TypeThe left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda TypeExpected a non-hidden function and found a hidden lambda.
WrongHidingInApplication TypeA function is applied to a hidden argument where a non-hidden was expected.
NotInductive TermThe term does not correspond to an inductive data type.
UninstantiatedDotPattern Expr
IlltypedPattern Pattern Type
TooManyArgumentsInLHS Nat Type
WrongNumberOfConstructorArguments QName Nat Nat
ShouldBeEmpty Type [Pattern]
ShouldBeASort TypeThe given type should have been a sort.
ShouldBePi TypeThe given type should have been a pi.
ShouldBeRecordType Type
NotAProperTerm
SplitOnIrrelevant Pattern (Arg Type)
DefinitionIsIrrelevant QName
VariableIsIrrelevant Name
UnequalLevel Comparison Term Term
UnequalTerms Comparison Term Term Type
UnequalTypes Comparison Type Type
UnequalTelescopes Comparison Telescope Telescope
UnequalRelevance Type TypeThe two function types have different relevance.
UnequalHiding Type TypeThe two function types have different hiding.
UnequalSorts Sort Sort
NotLeqSort Sort Sort
MetaCannotDependOn MetaId [Nat] NatThe arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.
MetaOccursInItself MetaId
GenericError String
BuiltinMustBeConstructor String Expr
NoSuchBuiltinName String
DuplicateBuiltinBinding String Term Term
NoBindingForBuiltin String
NoSuchPrimitiveFunction String
ShadowedModule [ModuleName]
BuiltinInParameterisedModule String
NoRHSRequiresAbsurdPattern [NamedArg Pattern]
AbsurdPatternRequiresNoRHS [NamedArg Pattern]
TooFewFields QName [Name]
TooManyFields QName [Name]
DuplicateFields [Name]
DuplicateConstructors [Name]
UnexpectedWithPatterns [Pattern]
WithClausePatternMismatch Pattern Pattern
FieldOutsideRecord
ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
IncompletePatternMatching Term Args
CoverageFailure QName [[Arg Pattern]]
UnreachableClauses QName [[Arg Pattern]]
CoverageCantSplitOn QName
CoverageCantSplitType Type
NotStrictlyPositive QName [Occ]
LocalVsImportedModuleClash ModuleName
UnsolvedMetas [Range]
UnsolvedConstraints Constraints
CyclicModuleDependency [TopLevelModuleName]
FileNotFound TopLevelModuleName [AbsolutePath]
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
ClashingFileNamesFor ModuleName [AbsolutePath]
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePathModule name, file from which it was loaded, file which the include path says contains the module. Scope errors
BothWithAndRHS
NotInScope [QName]
NoSuchModule QName
AmbiguousName QName [QName]
AmbiguousModule QName [ModuleName]
UninstantiatedModule QName
ClashingDefinition QName QName
ClashingModule ModuleName ModuleName
ClashingImport Name QName
ClashingModuleImport Name ModuleName
PatternShadowsConstructor Name QName
ModuleDoesntExport QName [ImportedName]
DuplicateImports QName [ImportedName]
InvalidPattern Pattern
RepeatedVariablesInPattern [Name]
NotAModuleExpr ExprThe 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
NothingAppliedToHiddenArg Expr
NoParseForApplication [Expr]
AmbiguousParseForApplication [Expr] [Expr]
NoParseForLHS Pattern
AmbiguousParseForLHS Pattern [Pattern]
data TCErr' Source
Type-checking errors.
Constructors
TypeError TCState (Closure TypeError)
Exception Range String
IOException Range IOException
PatternErr TCStatefor pattern violations
AbortAssign TCStateused to abort assignment to meta when there are instantiations
data TCErr Source
Type-checking errors, potentially paired with relevant syntax highlighting information.
Constructors
TCErr
errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)The ModuleToSource can be used to map the module names in the HighlightingInfo to file names.
errError :: TCErr'
Type checking monad transformer
newtype TCMT m a Source
Constructors
TCM
unTCM :: TCState -> TCEnv -> m (a, TCState)
type TCM = TCMT IOSource
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm whereSource
Methods
liftTCM :: TCM a -> tcm aSource
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM aSource
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n aSource
pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m aSource
patternViolation :: MonadTCM tcm => tcm aSource
internalError :: MonadTCM tcm => String -> tcm aSource
typeError :: MonadTCM tcm => TypeError -> tcm aSource
runTCM :: TCMT IO a -> IO (Either TCErr a)Source
Running the type checking monad
runTCM' :: Monad m => TCMT m a -> m aSource
Produced by Haddock version 2.6.1