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

Safe HaskellNone

Agda.TypeChecking.Monad.Base

Contents

Synopsis

Type checking state

data TCState Source

Constructors

TCSt 

Fields

stFreshThings :: FreshThings
 
stSyntaxInfo :: CompressedFile

Highlighting info.

stTokens :: CompressedFile

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

stTermErrs :: Seq TerminationError
 
stMetaStore :: MetaStore
 
stInteractionPoints :: InteractionPoints
 
stAwakeConstraints :: Constraints
 
stSleepingConstraints :: Constraints
 
stDirty :: Bool
 
stOccursCheckDefs :: Set QName

Definitions to be considered during occurs check. Initialized to the current mutual block before the check.

stSignature :: Signature
 
stImports :: Signature
 
stImportedModules :: Set ModuleName
 
stModuleToSource :: ModuleToSource
 
stVisitedModules :: VisitedModules
 
stCurrentModule :: Maybe ModuleName

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

stScope :: ScopeInfo
 
stPatternSyns :: PatternSynDefns
 
stPatternSynImports :: PatternSynDefns
 
stPragmaOptions :: PragmaOptions

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

stStatistics :: Statistics
 
stExtLambdaTele :: Map QName (Int, Int)
 
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).

stPersistent :: PersistentTCState
 
stInteractionOutputCallback :: InteractionOutputCallback

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

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

Options which apply to all files, unless overridden.

Interface

data ModuleInfo Source

Constructors

ModuleInfo 

Fields

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).

Closure

Constraints

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 

Fields

jMetaId :: a
 
jMetaType :: t
 
IsSort 

Fields

jMetaId :: a
 
jMetaType :: t
 

Instances

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 Type 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?

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

data MetaInstantiation Source

Constructors

InstV Term

solved by term

InstS Term

solved by Lam .. Sort s

Open

unsolved

OpenIFS

open, to be instantiated as implicit from scope

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool)) 

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.

type MetaNameSuggestion = StringSource

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

data NamedMeta Source

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

Interaction meta variables

Signature

data Section Source

Constructors

Section 

Fields

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.

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 Polarity Source

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

data Occurrence Source

Subterm occurrences for positivity checking. The constructors are listed in increasing information they provide: Mixed <= JustPos <= StrictPos <= GuardPos <= Unused Mixed <= JustNeg <= Unused.

Constructors

Mixed

Arbitrary occurrence (positive and negative).

JustNeg

Negative occurrence.

JustPos

Positive occurrence, but not strictly positive.

StrictPos

Strictly positive occurrence.

GuardPos

Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records.

Unused 

Instances

Eq Occurrence 
Ord Occurrence 
Show Occurrence 
Typeable Occurrence 
NFData Occurrence 
SemiRing Occurrence

Occurrence is a complete lattice with least element Mixed and greatest element Unused.

It forms a commutative semiring where oplus is meet (glb) and otimes is composition. Both operations are idempotent.

For oplus, Unused is neutral (zero) and Mixed is dominant. For otimes, StrictPos is neutral (one) and Unused is dominant.

PrettyTCM Occurrence 
EmbPrj Occurrence 
Abstract [Occurrence] 
Apply [Occurrence] 
PrettyTCM n => PrettyTCM (n, Occurrence) 

data Defn Source

Constructors

Axiom 
Function 

Fields

funClauses :: [Clause]
 
funCompiled :: CompiledClauses
 
funInv :: FunctionInverse
 
funMutual :: [QName]

Mutually recursive functions, datas and records.

funAbstr :: IsAbstract
 
funDelayed :: Delayed

Are the clauses of this definition delayed?

funProjection :: Maybe (QName, Int)

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.

funStatic :: Bool

Should calls to this function be normalised at compile-time?

funCopy :: Bool

Has this function been created by a module instantiation?

funTerminates :: Maybe Bool

Has this function been termination checked? Did it pass?

Datatype 

Fields

dataPars :: Nat
 
dataIxs :: Nat
 
dataInduction :: Induction
 
dataClause :: Maybe Clause
 
dataCons :: [QName]
 
dataSort :: Sort
 
dataMutual :: [QName]

Mutually recursive functions, datas and records.

dataAbstr :: IsAbstract
 
Record 

Fields

recPars :: Nat

Number of parameters.

recClause :: Maybe Clause
 
recCon :: QName

Constructor name.

recNamedCon :: Bool
 
recConType :: Type

The record constructor's type.

recFields :: [Arg QName]
 
recTel :: Telescope

The record field telescope

recMutual :: [QName]

Mutually recursive functions, datas and records.

recEtaEquality :: Bool

Eta-expand at this record type. False for unguarded recursive records.

recInduction :: Induction

Inductive or Coinductive? Matters only for recursive records.

recRecursive :: Bool

Recursive record. Implies recEtaEquality = False. Projections are not size-preserving.

recAbstr :: IsAbstract
 
Constructor 

Fields

conPars :: Nat
 
conSrcCon :: QName
 
conData :: QName
 
conAbstr :: IsAbstract
 
conInd :: Induction

Inductive or coinductive?

Primitive

Primitive or builtin functions.

Fields

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

Nothing for primitive functions, Just something for builtin functions.

primCompiled :: Maybe CompiledClauses

Nothing for primitive functions, Just something for builtin functions.

newtype Fields Source

Constructors

Fields [(Name, Type)] 

Instances

data Reduced no yes Source

Constructors

NoReduction no 
YesReduction yes 

Instances

data IsReduced Source

Constructors

NotReduced 
Reduced (Blocked ()) 

data MaybeReduced a Source

Constructors

MaybeRed 

defDelayed :: Definition -> DelayedSource

Are the clauses of this definition delayed?

defCopy :: Definition -> BoolSource

Is the definition just a copy created by a module instantiation?

Injectivity

Mutual blocks

Statistics

Trace

Builtin things

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.

data HighlightingMethod Source

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

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 :: AbsolutePath

The path to the file that is currently being type-checked.

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

envSolvingConstraints :: Bool

Are we currently in the process of solving active constraints?

envAssignMetas :: Bool

Are we allowed to assign metas?

envActiveProblems :: [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.

envRelevance :: Relevance

Are we checking an irrelevant argument? (=Irrelevant) Then top-level irrelevant declarations are enabled. Other value: Relevant, then only relevant decls. are avail.

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

envEtaContractImplicit :: Bool

it'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
 
envHighlightingRange :: Range

Interactive highlighting uses this range rather than envRange.

envCall :: Maybe (Closure Call)

what we're doing at the moment

envEmacs :: Bool

True when called from the Emacs mode.

envHighlightingLevel :: HighlightingLevel

Set to None when imported modules are type-checked.

envHighlightingMethod :: HighlightingMethod
 
envModuleNestingLevel :: Integer

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.

envAllowDestructiveUpdate :: Bool

When True, allows destructively shared updating terms during evaluation or unification. This is disabled when doing speculative checking, like solve instance metas, or when updating might break abstraction, as is the case when checking abstract definitions.

Context

type Context = [ContextEntry]Source

The Context is a stack of ContextEntrys.

data ContextEntry Source

Constructors

Ctx 

Fields

ctxId :: CtxId
 
ctxEntry :: Dom (Name, Type)
 

Let bindings

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

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.

Type checking errors

data OccPos Source

Instances

data CallInfo Source

Information about a call.

Constructors

CallInfo 

Fields

callInfoRange :: Range

Range of the head identifier.

callInfoCall :: String

Formatted representation of the call.

(Doc would perhaps be better here, but Doc doesn't come with an Ord instance.)

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.

data TypeError Source

Constructors

InternalError String 
NotImplemented String 
NotSupported String 
CompilationError String 
TerminationCheckFailed [TerminationError] 
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

IndicesNotConstructorApplications [Arg Term]

Indices.

IndexVariablesNotDistinct [Nat] [Arg Term]

Variables, indices.

IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]

Indices (variables), index expressions (with constructors applied to reconstructed parameters), parameters.

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.

WrongIrrelevanceInLambda Type

Expected a relevant function and found an irrelevant lambda.

NotInductive Term

The term does not correspond to an inductive data type.

UninstantiatedDotPattern Expr 
IlltypedPattern Pattern Type 
TooManyArgumentsInLHS 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 
ShouldBeRecordPattern Pattern 
NotAProperTerm 
SetOmegaNotValidType 
SplitOnIrrelevant Pattern (Dom Type) 
DefinitionIsIrrelevant QName 
VariableIsIrrelevant Name 
UnequalLevel Comparison Term Term 
UnequalTerms Comparison Term Term Type 
UnequalTypes Comparison Type Type 
UnequalTelescopes Comparison Telescope Telescope 
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 
HeterogeneousEquality Term Type Term Type

We ended up with an equality constraint where the terms have different types. This is not supported.

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 
GenericDocError Doc 
BuiltinMustBeConstructor String Expr 
NoSuchBuiltinName String 
DuplicateBuiltinBinding String Term Term 
NoBindingForBuiltin String 
NoSuchPrimitiveFunction String 
ShadowedModule Name [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 Telescope Args Args 
CoverageCantSplitIrrelevantType Type 
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] 
DuplicateImports 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 
NothingAppliedToInstanceArg Expr 
UnusedVariableInPatternSynonym 
PatternSynonymArityMismatch QName 
NoParseForApplication [Expr] 
AmbiguousParseForApplication [Expr] [Expr] 
NoParseForLHS LHSOrPatSyn Pattern 
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] 
IFSNoCandidateInScope Type 
SafeFlagPostulate Name 
SafeFlagPragma [String] 
SafeFlagNoTerminationCheck 
SafeFlagPrimTrustMe 
NeedOptionCopatterns 

data LHSOrPatSyn Source

Distinguish error message when parsing lhs or pattern synonym, resp.

Constructors

IsLHS 
IsPatSyn 

Type checking monad transformer

newtype TCMT m a Source

Constructors

TCM 

Fields

unTCM :: IORef TCState -> TCEnv -> m a
 

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm whereSource

Methods

liftTCM :: TCM a -> tcm aSource

Instances

MonadTCM Unify 
MonadIO m => MonadTCM (TCMT m) 
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) 
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) 

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM aSource

Preserve the state of the failing computation.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n aSource

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m aSource

returnTCMT :: MonadIO m => a -> TCMT m aSource

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m bSource

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m bSource

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m bSource

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m bSource

runTCM :: TCMT IO a -> IO (Either TCErr a)Source

Running the type checking monad

runTCM' :: MonadIO m => TCMT m a -> m aSource

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.

extendlambdaname :: [Char]Source

Base name for extended lambda patterns