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

Safe HaskellNone
LanguageHaskell98

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. During occurs check, we remove definitions from this set as soon we have checked them.

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

Counters to collect various statistics about meta variables etc.

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

Options which apply to all files, unless overridden.

Instances

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!

Instances

initPersistentState :: PersistentTCState Source

Empty persistent state.

data FreshThings Source

Constructors

Fresh 

Fields

fMeta :: MetaId
 
fInteraction :: InteractionId
 
fMutual :: MutualId
 
fName :: NameId
 
fCtx :: CtxId
 
fProblem :: ProblemId
 
fInt :: Int

Can be used for various things.

Instances

initState :: TCState Source

Empty state of type checker.

stBuiltinThings :: TCState -> BuiltinThings PrimFun Source

newtype ProblemId Source

Constructors

ProblemId Nat 

Instances

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.

Interface

data ModuleInfo Source

Constructors

ModuleInfo 

Fields

miInterface :: Interface
 
miWarnings :: Bool

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

type VisitedModules = Map TopLevelModuleName ModuleInfo Source

type DecodedModules = Map TopLevelModuleName Interface Source

data Interface Source

Constructors

Interface 

Fields

iSourceHash :: Hash

Hash of the source code.

iImportedModules :: [(ModuleName, Hash)]

Imported modules and their hashes.

iModuleName :: ModuleName

Module name of this interface.

iScope :: Map ModuleName Scope
 
iInsideScope :: ScopeInfo

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

iSignature :: Signature
 
iBuiltin :: BuiltinThings (String, QName)
 
iHaskellImports :: Set String

Haskell imports listed in (transitively) imported modules are not included here.

iHighlighting :: HighlightingInfo
 
iPragmaOptions :: [OptionsPragma]

Pragma options set in the file.

iPatternSyns :: PatternSynDefns
 

Instances

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
 
clValue :: a
 

Instances

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

Constraints

type Constraints = [ProblemConstraint] Source

data ProblemConstraint Source

Constructors

PConstr 

Fields

constraintProblem :: ProblemId
 
theConstraint :: Closure Constraint
 

Instances

data Constraint Source

Constructors

ValueCmp Comparison Type Term Term 
ElimCmp [Polarity] 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 
UnBlock MetaId 
Guarded Constraint ProblemId 
IsEmpty Range Type

the range is the one of the absurd pattern

FindInScope MetaId [(Term, Type)] 

Instances

data Comparison Source

Constructors

CmpEq 
CmpLeq 

Instances

data CompareDirection Source

An extension of Comparison to >=.

Constructors

DirEq 
DirLeq 
DirGeq 

Instances

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

openThingCtxIds :: [CtxId]
 
openThing :: a
 

Instances

Judgements

data Judgement t a Source

Constructors

HasType 

Fields

jMetaId :: a
 
jMetaType :: t
 
IsSort 

Fields

jMetaId :: a
 
jMetaType :: t
 

Instances

Functor (Judgement t) 
Foldable (Judgement t) 
Traversable (Judgement t) 
(Show t, Show a) => Show (Judgement t a) 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) 
Typeable (* -> * -> *) Judgement 
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') 

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?

Instances

data Listener Source

Constructors

EtaExpand MetaId 
CheckConstraint Nat ProblemConstraint 

Instances

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 TypeCheckingProblem) (TCM Bool) 

Instances

data TypeCheckingProblem Source

Constructors

CheckExpr Expr Type 
CheckArgs ExpandHidden ExpandInstances Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term) 

Instances

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

data RunMetaOccursCheck Source

Constructors

RunMetaOccursCheck 
DontRunMetaOccursCheck 

Instances

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.

Instances

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

type MetaStore = Map MetaId 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

getMetaColors :: MetaVariable -> [Color] 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.

Instances

type InteractionPoints = Map InteractionId InteractionPoint Source

Data structure managing the interaction points.

Signature

data Signature Source

Constructors

Sig 

Fields

sigSections :: Sections
 
sigDefinitions :: Definitions
 

Instances

type Sections = Map ModuleName Section Source

type Definitions = HashMap QName Definition Source

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.

Instances

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 :: [Term]

Left hand side patterns, where var 0 stands for a pattern variable. There should be n occurrences of var0 in dfPats.

dfRHS :: DisplayTerm

Right hand side, with n free variables.

Instances

data DisplayTerm Source

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Args

(f vs | ws) us. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Args are additional arguments us (possible in case the with-application is of function type).

DCon QName [Arg DisplayTerm]

c vs.

DDef QName [Arg DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

Instances

defaultDisplayForm :: QName -> [Open DisplayForm] Source

By default, we have no display form.

defRelevance :: Definition -> Relevance Source

defColors :: Definition -> [Color] 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]
 
defArgOccurrences :: [Occurrence]
 
defDisplay :: [Open DisplayForm]
 
defMutual :: MutualId
 
defCompiledRep :: CompiledRepresentation
 
theDef :: Defn
 

Instances

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

Create a definition with sensible defaults.

type HaskellCode = String Source

type HaskellType = String Source

type EpicCode = String Source

type JSCode = Exp Source

data HaskellRepresentation Source

Constructors

HsDefn HaskellType HaskellCode 
HsType HaskellType 

Instances

data HaskellExport Source

Constructors

HsExport HaskellType String 

Instances

data Polarity Source

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances

data CompiledRepresentation Source

Constructors

CompiledRep 

Fields

compiledHaskell :: Maybe HaskellRepresentation
 
exportHaskell :: Maybe HaskellExport
 
compiledEpic :: Maybe EpicCode
 
compiledJS :: Maybe JSCode
 

Instances

noCompiledRep :: CompiledRepresentation Source

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

KillRange Occurrence 
PrettyTCM Occurrence 
EmbPrj Occurrence 
Typeable * Occurrence 
Abstract [Occurrence] 
Apply [Occurrence] 
PrettyTCM n => PrettyTCM (WithNode n Occurrence) 

data Projection Source

Additional information for projection Functions.

Constructors

Projection 

Fields

projProper :: Maybe QName

Nothing if only projection-like, Just q if record projection, where q is the original projection name (current name could be from module app).

projFromType :: QName

Type projected from. Record type if projProper = Just{}.

projIndex :: Int

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

projDropPars :: Term

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 In case of a projection-like function, just the function symbol is returned as Def: t = pars -> f.

projArgInfo :: ArgInfo

The info of the principal (record) argument.

Instances

data Defn Source

Constructors

Axiom

Postulate.

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.

funInv :: FunctionInverse
 
funMutual :: [QName]

Mutually recursive functions, datas and records. Does not include this function.

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.

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?

funExtLam :: Maybe (Int, Int)

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.

Datatype 

Fields

dataPars :: Nat

Number of parameters.

dataSmallPars :: Permutation

Parameters that are maybe small.

dataNonLinPars :: Drop Permutation

Parameters that appear in indices.

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.

dataSort :: Sort
 
dataMutual :: [QName]

Mutually recursive functions, datas and records. Does not include this data type.

dataAbstr :: IsAbstract
 
Record 

Fields

recPars :: Nat

Number of parameters.

recClause :: Maybe Clause
 
recConHead :: ConHead

Constructor name and fields.

recNamedCon :: Bool
 
recConType :: Type

The record constructor's type. (Includes record parameters.)

recFields :: [Arg QName]
 
recTel :: Telescope

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

recMutual :: [QName]

Mutually recursive functions, datas and records. Does not include this record.

recEtaEquality :: Bool

Eta-expand at this record type. False for unguarded recursive records and coinductive 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

Number of 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?

Primitive

Primitive or builtin functions.

Fields

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

null for primitive functions, not null for builtin functions.

primCompiled :: Maybe CompiledClauses

Nothing for primitive functions, Just something for builtin functions.

Instances

emptyFunction :: Defn Source

A template for creating Function definitions, with sensible defaults.

recCon :: Defn -> QName Source

defIsRecord :: Defn -> Bool Source

defIsDataOrRecord :: Defn -> Bool Source

newtype Fields Source

Constructors

Fields [(Name, Type)] 

Instances

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

data Reduced no yes Source

Constructors

NoReduction no 
YesReduction Simplification yes 

Instances

Functor (Reduced no) 
Typeable (* -> * -> *) Reduced 

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

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.

FunctionReductions

Functions which are not projections may be reduced.

LevelReductions

Reduce Level terms.

Instances

type AllowedReductions = [AllowedReduction] Source

allReductions :: [AllowedReduction] Source

data PrimFun Source

Constructors

PrimFun 

Fields

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

Instances

defClauses :: Definition -> [Clause] Source

defCompiled :: Definition -> Maybe CompiledClauses Source

defJSDef :: Definition -> Maybe JSCode Source

defEpicDef :: Definition -> Maybe EpicCode Source

defDelayed :: Definition -> Delayed Source

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool Source

Has the definition failed the termination checker?

defCopy :: Definition -> Bool Source

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

defAbstract :: Definition -> IsAbstract Source

Injectivity

type FunctionInverse = FunctionInverse' Clause Source

data FunctionInverse' c Source

Constructors

NotInjective 
Inverse (Map TermHead c) 

Instances

Functor FunctionInverse' 
Abstract FunctionInverse 
Apply FunctionInverse 
EmbPrj FunctionInverse 
DropArgs FunctionInverse 
InstantiateFull FunctionInverse 
Show c => Show (FunctionInverse' c) 
KillRange c => KillRange (FunctionInverse' c) 
Typeable (* -> *) FunctionInverse' 

data TermHead Source

Constructors

SortHead 
PiHead 
ConsHead QName 

Instances

Mutual blocks

newtype MutualId Source

Constructors

MutId Int32 

Instances

Statistics

type Statistics = Map String Integer Source

Trace

data Call Source

Constructors

CheckClause Type SpineClause (Maybe Clause) 
forall a . CheckPattern Pattern Telescope Type (Maybe a) 
CheckLetBinding LetBinding (Maybe ()) 
InferExpr Expr (Maybe (Term, Type)) 
CheckExprCall Expr Type (Maybe Term) 
CheckDotPattern Expr Term (Maybe Constraints) 
CheckPatternShadowing SpineClause (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)) 
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 ()) 
CheckIsEmpty Range Type (Maybe ()) 
CheckWithFunctionType Expr (Maybe ()) 
CheckSectionApplication Range ModuleName ModuleApplication (Maybe ()) 
ScopeCheckExpr Expr (Maybe Expr) 
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration]) 
ScopeCheckLHS Name Pattern (Maybe LHS) 
forall a . NoHighlighting (Maybe a) 
forall a . SetRange Range (Maybe a)

used by setCurrentRange

Instances

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

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

data HighlightingMethod Source

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

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.

envColors :: [Color]
 
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

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.

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
 
envPrintDomainFreePi :: Bool

When True types will be omitted from printed pi types if they can be inferred

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.

Instances

initEnv :: TCEnv Source

Context

type Context = [ContextEntry] Source

The Context is a stack of ContextEntrys.

data ContextEntry Source

Constructors

Ctx 

Fields

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

Instances

newtype CtxId Source

Constructors

CtxId Nat 

Instances

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

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

data ExpandInstances Source

Constructors

ExpandInstanceArguments 
DontExpandInstanceArguments 

Instances

Type checking errors

data Occ Source

Constructors

OccCon 

Fields

occDatatype :: QName
 
occConstructor :: QName
 
occPosition :: OccPos
 
OccClause 

Fields

occFunction :: QName
 
occClause :: Int
 
occPosition :: OccPos
 

Instances

data OccPos Source

Constructors

NonPositively 
ArgumentTo Nat QName 

Instances

data CallInfo Source

Information about a call.

Constructors

CallInfo 

Fields

callInfoTarget :: QName

Target function name pretty-printed.

callInfoRange :: Range

Range of the target function.

callInfoCall :: Closure Term

To be formatted representation of the call.

Instances

Show CallInfo

We only show the name of the callee.

Pretty CallInfo 
PrettyTCM CallInfo 
Typeable * CallInfo 

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

Constructors

NotADatatype (Closure Type)

neither data type nor record

IrrelevantDatatype (Closure Type)

data type, but in irrelevant position

CoinductiveDatatype (Closure Type)

coinductive data type

CantSplit QName Telescope Args Args [Term] 
GenericSplitError String 

Instances

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.

CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]

Datatype, constructors.

DoesNotConstructAnElementOf QName Type

constructor, type

DifferentArities

Varying number of arguments for a function.

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 Type

Expected a relevant function and found an irrelevant 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.

ColorMismatch [Color] [Color]

The given color does not correspond to the expected color.

NotInductive Term

The term does not correspond to an inductive data type.

UninstantiatedDotPattern Expr 
IlltypedPattern Pattern Type 
IllformedProjectionPattern Pattern 
CannotEliminateWithPattern (NamedArg 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 
NotAProjectionPattern (NamedArg Pattern) 
NotAProperTerm 
SetOmegaNotValidType 
InvalidType Term

This term is not a type expression.

SplitOnIrrelevant Pattern (Dom Type) 
DefinitionIsIrrelevant QName 
VariableIsIrrelevant 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.

UnequalColors Term Term

The two function types have different color.

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 
IllegalLetInTelescope TypedBinding 
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 [Elim] 
CoverageFailure QName [[Arg Pattern]] 
UnreachableClauses QName [[Arg Pattern]] 
CoverageCantSplitOn QName Telescope Args Args 
CoverageCantSplitIrrelevantType Type 
CoverageCantSplitType Type 
WithoutKError Type Term Term 
SplitError SplitError 
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 

Instances

data LHSOrPatSyn Source

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

Constructors

IsLHS 
IsPatSyn 

Instances

data TCErr Source

Type-checking errors.

Constructors

TypeError TCState (Closure TypeError) 
Exception Range String 
IOException Range IOException 
PatternErr TCState

for pattern violations

Instances

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

newtype ReduceM a Source

Constructors

ReduceM 

Fields

unReduceM :: Reader ReduceEnv a
 

Instances

runReduceM :: ReduceM a -> TCM a Source

Type checking monad transformer

newtype TCMT m a Source

Constructors

TCM 

Fields

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

Instances

type TCM = TCMT IO Source

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

Methods

liftTCM :: TCM a -> tcm a Source

Instances

MonadTCM TerM 
MonadTCM Unify 
MonadTCM tcm => MonadTCM (MaybeT tcm) 
MonadIO m => MonadTCM (TCMT m) 
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) 
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) 
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) 

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

Preserve the state of the failing computation.

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

typeError :: MonadTCM tcm => TypeError -> tcm a 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 TCM action (a TCM 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.

extendlambdaname :: [Char] Source

Base name for extended lambda patterns

absurdLambdaName :: [Char] Source

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool Source

Check whether we have an definition from an absurd lambda.