Agda.TypeChecking.Monad.Base

stFreshThings :: FreshThings
stMetaStore :: MetaStore
stInteractionPoints :: InteractionPoints
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stModuleToSource :: ModuleToSource
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe ModuleName	The current module is available after it has been type checked.
stScope :: ScopeInfo
stPersistentOptions :: CommandLineOptions	Options which apply to all files, unless overridden.
stPragmaOptions :: CommandLineOptions	Options applying to the current file. `OPTIONS` pragmas only affect this field.
stStatistics :: Statistics
stTrace :: CallTrace	record what is happening (for error msgs)
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: Set String	Imports 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 :: Integer	Can be used for various things.

initState :: TCState

Source

stBuiltinThings :: TCState -> BuiltinThings PrimFun

Source

Interface

data ModuleInfo

Source

Constructors

ModuleInfo

miInterface :: Interface
miWarnings :: Bool	`True` if warnings were encountered when the module was type checked.
miTimeStamp :: ClockTime	The 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 ModuleInfo

Source

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 String	Haskell imports listed in (transitively) imported modules are not included here.
iHighlighting :: HighlightingInfo

Closure

data Closure a

Source

Constructors

Closure

clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
clTrace :: CallTrace
clValue :: a

buildClosure :: MonadTCM tcm => a -> tcm (Closure a)

Source

Constraints

type ConstraintClosure = Closure Constraint

Source

data Constraint

Source

Constructors

ValueCmp Comparison Type Term Term
TypeCmp Comparison Type Type
TelCmp Comparison Telescope Telescope
SortCmp Comparison Sort Sort
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 :: MetaPriority	some metavariables are more eager to be instantiated
mvJudgement :: Judgement Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaId	metavariables 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 Range

Source

TODO: Not so nice.

type MetaStore = Map MetaId MetaVariable

Source

normalMetaPriority :: MetaPriority

Source

lowMetaPriority :: MetaPriority

Source

highMetaPriority :: MetaPriority

Source

getMetaInfo :: MetaVariable -> MetaInfo

Source

getMetaScope :: MetaVariable -> ScopeInfo

Source

getMetaEnv :: MetaVariable -> TCEnv

Source

getMetaSig :: MetaVariable -> Signature

Source

Interaction meta variables

type InteractionPoints = Map InteractionId MetaId

Source

newtype InteractionId

Source

Constructors

InteractionId Nat

Signature

data Signature

Source

Constructors

Sig

sigSections :: Sections
sigDefinitions :: Definitions

type Sections = Map ModuleName Section

Source

type Definitions = Map QName Definition

Source

data Section

Source

Constructors

Section

secTelescope :: Telescope
secFreeVars :: Nat	This 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 :: Signature

Source

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

defName :: QName
defType :: Type
defDisplay :: [Open DisplayForm]
defMutual :: MutualId
theDef :: Defn

type HaskellCode = String

Source

type HaskellType = String

Source

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

Function

funClauses :: [Clause]
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: Delayed	Are the clauses of this definition delayed?

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 :: Maybe QName	Constructor name.
recConType :: Type	The record constructor's type.
recFields :: [(Hiding, QName)]
recTel :: Telescope
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recAbstr :: IsAbstract

Constructor

conPars :: Nat
conSrcCon :: QName
conData :: QName
conHsCode :: Maybe (HaskellType, HaskellCode)
conAbstr :: IsAbstract
conInd :: Induction	Inductive or coinductive?

Primitive Primitive or builtin functions.

primAbstr :: IsAbstract
primName :: String
primClauses :: Maybe [Clause]	`Nothing` for primitive functions, `Just something` for builtin functions.

newtype Fields

Source

Constructors

Fields [(Name, Type)]

data Reduced no yes

Source

Constructors

NoReduction no
YesReduction yes

data PrimFun

Source

Constructors

PrimFun

primFunName :: QName
primFunArity :: Arity
primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term)

defClauses :: Definition -> [Clause]

Source

data Delayed

Source

Used to specify whether something should be delayed.

Constructors

Delayed
NotDelayed

defDelayed :: Definition -> Delayed

Source

Are the clauses of this definition delayed?

defAbstract :: Definition -> IsAbstract

Source

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 Int

Statistics

type Statistics = Map String Int

Source

Trace

type CallTrace = Trace (Closure Call)

Source

noTrace :: CallTrace

Source

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 MutualId	the current (if any) mutual block
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.
envReplace :: Bool	Coinductive 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 :: Bool	Sometimes we want to disable display forms.
envReifyInteractionPoints :: Bool	should we try to recover interaction points when reifying? disabled when generating types for with functions

initEnv :: TCEnv

Source

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, 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

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 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
DoesNotConstructAnElementOf QName Term	constructor, type
DifferentArities	Varying number of arguments for a function.
WrongHidingInLHS Type	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.
DependentPatternMatchingOnCodata
NotInductive Term	The 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 Type	The given type should have been a sort.
ShouldBePi Type	The given type should have been a pi.
ShouldBeRecordType Type
NotAProperTerm
UnequalTerms Comparison Term Term Type
UnequalTypes Comparison Type Type
UnequalTelescopes Comparison Telescope Telescope
UnequalHiding Type Type	The two function types have different hiding.
UnequalSorts Sort Sort
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
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	Module 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]
InvalidPattern Pattern
RepeatedVariablesInPattern [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
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 TCState	for pattern violations
AbortAssign TCState	used 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'