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

Agda.TypeChecking.Monad.Base

Contents

Synopsis

Type checking state

data TCState Source

Constructors

TCSt 

Fields

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

Options 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 String

Imports that should be generated by the compiler (this includes imports from imported modules).

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

data Interface Source

Constructors

Interface 

Fields

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
 
iPragmaOptions :: [OptionsPragma]

Pragma options set in the file.

Closure

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

Constraints

Open things

data Open a Source

A thing tagged with the context it came from.

Constructors

OpenThing [CtxId] a 

Instances

Judgements

data Judgement t a Source

Constructors

HasType a t 
IsSort a 

Instances

Typeable2 Judgement 
Functor (Judgement t) 
Foldable (Judgement t) 
Traversable (Judgement t) 
(Data t, Data a) => Data (Judgement t a) 
(Show t, Show a) => Show (Judgement t a) 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) 
(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 MetaId

metavariables interested in what happens to this guy

type MetaInfo = Closure RangeSource

TODO: Not so nice.

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

Constructors

Defn 

Fields

defRelevance :: Relevance

Some defs can be irrelevant (but not hidden).

defName :: QName
 
defType :: Type

Type of the lifted definition.

defDisplay :: [Open DisplayForm]
 
defMutual :: MutualId
 
theDef :: Defn
 

data Occurrence Source

Positive means strictly positive and Negative means not strictly positive.

Constructors

Positive 
Negative 
Unused 

data Defn Source

Constructors

Axiom 
Function 

Fields

funClauses :: [Clauses]
 
funCompiled :: CompiledClauses
 
funInv :: FunctionInverse
 
funPolarity :: [Polarity]
 
funArgOccurrences :: [Occurrence]
 
funAbstr :: IsAbstract
 
funDelayed :: Delayed

Are the clauses of this definition delayed?

funProjection :: Maybe Int

Is 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 
Record 

Fields

recPars :: Nat
 
recClause :: Maybe Clause
 
recCon :: QName

Constructor name.

recNamedCon :: Bool
 
recConType :: Type

The record constructor's type.

recFields :: [Arg QName]
 
recTel :: Telescope
 
recPolarity :: [Polarity]
 
recArgOccurrences :: [Occurrence]
 
recEtaEquality :: Bool
 
recAbstr :: IsAbstract
 
Constructor

Note that, currently, the sharp constructor is represented as a definition (Def), but if you look up the name you will get a Constructor.

Fields

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

Inductive or coinductive?

Primitive

Primitive or builtin functions.

Fields

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

Nothing for primitive functions, Just something for builtin functions.

primCompiled :: Maybe CompiledClauses
 

newtype Fields Source

Constructors

Fields [(Name, Type)] 

data Reduced no yes Source

Constructors

NoReduction no 
YesReduction yes 

Instances

data MaybeReduced a Source

Constructors

MaybeRed 

data Delayed Source

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

defDelayed :: Definition -> DelayedSource

Are the clauses of this definition delayed?

Injectivity

Mutual blocks

Statistics

Trace

Builtin things

Type checking environment

data TCEnv Source

Constructors

TCEnv 

Fields

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.

envIrrelevant :: Bool

Are we checking an irrelevant argument? Then top-level irrelevant declarations are enabled.

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

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
 
envCall :: Maybe (Closure Call)

what we're doing at the moment

Context

data ContextEntry Source

Constructors

Ctx 

Fields

ctxId :: CtxId
 
ctxEntry :: Arg (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

Type checking errors

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

IndicesNotConstructorApplications [Arg Term]

Indices.

IndexVariablesNotDistinct [Arg Term]

Indices.

IndexFreeInParameter Nat [Arg Term]

Index (a variable), 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.

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

The two function types have different relevance.

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

Fields

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 

Fields

unTCM :: TCState -> TCEnv -> m (a, TCState)
 

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

Methods

liftTCM :: TCM a -> tcm aSource

Instances

MonadTCM RecPatM 
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

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

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

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

Running the type checking monad

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