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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Base

Contents

Synopsis

Type checking state

data TCState #

Constructors

TCSt 

Fields

Instances

Show TCState # 
LensPersistentVerbosity TCState # 
LensIncludePaths TCState # 
LensSafeMode TCState # 
LensCommandLineOptions TCState # 
LensVerbosity TCState # 
LensPragmaOptions TCState # 
MonadState TCState TerM 

Methods

get :: TerM TCState

put :: TCState -> TerM ()

state :: (TCState -> (a, TCState)) -> TerM a

MonadIO m => MonadState TCState (TCMT m) # 

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

state :: (TCState -> (a, TCState)) -> TCMT m a

class Monad m => ReadTCState m where #

Minimal complete definition

getTCState

Methods

getTCState :: m TCState #

data PreScopeState #

Constructors

PreScopeState 

Fields

data PostScopeState #

Constructors

PostScopeState 

Fields

data MutualBlock #

A mutual block of names in the signature.

Constructors

MutualBlock 

Fields

data PersistentTCState #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt 

Fields

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] #

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

data TypeCheckAction #

A complete log for a module will look like this:

  • Pragmas
  • EnterSection, entering the main module.
  • 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
  • LeaveSection, leaving the main module.

initPersistentState :: PersistentTCState #

Empty persistent state.

initPreScopeState :: PreScopeState #

Empty state of type checker.

st-prefixed lenses

Fresh things

fresh :: (HasFresh i, MonadState TCState m) => m i #

newtype ProblemId #

Constructors

ProblemId Nat 

Instances

Enum ProblemId # 
Eq ProblemId # 
Integral ProblemId # 
Num ProblemId # 
Ord ProblemId # 
Real ProblemId # 
Show ProblemId # 
Pretty ProblemId # 
HasFresh ProblemId # 
PrettyTCM ProblemId # 

Methods

prettyTCM :: ProblemId -> TCM Doc #

freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name #

freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name #

freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name #

class FreshName a where #

Create a fresh name from a.

Minimal complete definition

freshName_

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name #

Instances

FreshName () # 

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => () -> m Name #

FreshName String # 

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => String -> m Name #

FreshName Range # 

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => Range -> m Name #

FreshName (Range, String) # 

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => (Range, String) -> m Name #

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath #

Maps top-level module names to the corresponding source file names.

type SourceToModule = Map AbsolutePath TopLevelModuleName #

Maps source file names to the corresponding top-level module names.

sourceToModule :: TCM SourceToModule #

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

Interface

data ModuleInfo #

Constructors

ModuleInfo 

Fields

data Interface #

Constructors

Interface 

Fields

iFullHash :: Interface -> Hash #

Combines the source hash and the (full) hashes of the imported modules.

Closure

data Closure a #

Constructors

Closure 

Fields

Instances

Functor Closure # 

Methods

fmap :: (a -> b) -> Closure a -> Closure b #

(<$) :: a -> Closure b -> Closure a #

Foldable Closure # 

Methods

fold :: Monoid m => Closure m -> m #

foldMap :: Monoid m => (a -> m) -> Closure a -> m #

foldr :: (a -> b -> b) -> b -> Closure a -> b #

foldr' :: (a -> b -> b) -> b -> Closure a -> b #

foldl :: (b -> a -> b) -> b -> Closure a -> b #

foldl' :: (b -> a -> b) -> b -> Closure a -> b #

foldr1 :: (a -> a -> a) -> Closure a -> a #

foldl1 :: (a -> a -> a) -> Closure a -> a #

toList :: Closure a -> [a] #

null :: Closure a -> Bool #

length :: Closure a -> Int #

elem :: Eq a => a -> Closure a -> Bool #

maximum :: Ord a => Closure a -> a #

minimum :: Ord a => Closure a -> a #

sum :: Num a => Closure a -> a #

product :: Num a => Closure a -> a #

Show a => Show (Closure a) # 

Methods

showsPrec :: Int -> Closure a -> ShowS #

show :: Closure a -> String #

showList :: [Closure a] -> ShowS #

HasRange a => HasRange (Closure a) # 

Methods

getRange :: Closure a -> Range #

MentionsMeta a => MentionsMeta (Closure a) # 

Methods

mentionsMeta :: MetaId -> Closure a -> Bool #

PrettyTCM a => PrettyTCM (Closure a) # 

Methods

prettyTCM :: Closure a -> TCM Doc #

InstantiateFull a => InstantiateFull (Closure a) # 
Normalise a => Normalise (Closure a) # 

Methods

normalise' :: Closure a -> ReduceM (Closure a) #

Simplify a => Simplify (Closure a) # 

Methods

simplify' :: Closure a -> ReduceM (Closure a) #

Reduce a => Reduce (Closure a) # 
Instantiate a => Instantiate (Closure a) # 

Methods

instantiate' :: Closure a -> ReduceM (Closure a) #

Constraints

data Constraint #

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.

CheckSizeLtSat Term

Check that the Term is either not a SIZELT or a non-empty SIZELT.

FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])

the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)

flipCmp :: CompareDirection -> CompareDirection #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c #

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

Open things

data Open a #

A thing tagged with the context it came from.

Constructors

OpenThing 

Fields

Instances

Functor Open # 

Methods

fmap :: (a -> b) -> Open a -> Open b #

(<$) :: a -> Open b -> Open a #

Decoration Open # 

Methods

traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) #

distributeF :: Functor m => Open (m a) -> m (Open a) #

Show a => Show (Open a) # 

Methods

showsPrec :: Int -> Open a -> ShowS #

show :: Open a -> String #

showList :: [Open a] -> ShowS #

KillRange a => KillRange (Open a) # 

Methods

killRange :: KillRangeT (Open a) #

NamesIn a => NamesIn (Open a) # 

Methods

namesIn :: Open a -> Set QName #

InstantiateFull a => InstantiateFull (Open a) # 

Methods

instantiateFull' :: Open a -> ReduceM (Open a) #

data Local a #

Constructors

Local ModuleName a

Local to a given module, the value should have module parameters as free variables.

Global a

Global value, should be closed.

Instances

Functor Local # 

Methods

fmap :: (a -> b) -> Local a -> Local b #

(<$) :: a -> Local b -> Local a #

Foldable Local # 

Methods

fold :: Monoid m => Local m -> m #

foldMap :: Monoid m => (a -> m) -> Local a -> m #

foldr :: (a -> b -> b) -> b -> Local a -> b #

foldr' :: (a -> b -> b) -> b -> Local a -> b #

foldl :: (b -> a -> b) -> b -> Local a -> b #

foldl' :: (b -> a -> b) -> b -> Local a -> b #

foldr1 :: (a -> a -> a) -> Local a -> a #

foldl1 :: (a -> a -> a) -> Local a -> a #

toList :: Local a -> [a] #

null :: Local a -> Bool #

length :: Local a -> Int #

elem :: Eq a => a -> Local a -> Bool #

maximum :: Ord a => Local a -> a #

minimum :: Ord a => Local a -> a #

sum :: Num a => Local a -> a #

product :: Num a => Local a -> a #

Traversable Local # 

Methods

traverse :: Applicative f => (a -> f b) -> Local a -> f (Local b) #

sequenceA :: Applicative f => Local (f a) -> f (Local a) #

mapM :: Monad m => (a -> m b) -> Local a -> m (Local b) #

sequence :: Monad m => Local (m a) -> m (Local a) #

Decoration Local # 

Methods

traverseF :: Functor m => (a -> m b) -> Local a -> m (Local b) #

distributeF :: Functor m => Local (m a) -> m (Local a) #

Show a => Show (Local a) # 

Methods

showsPrec :: Int -> Local a -> ShowS #

show :: Local a -> String #

showList :: [Local a] -> ShowS #

KillRange a => KillRange (Local a) # 

Methods

killRange :: KillRangeT (Local a) #

NamesIn a => NamesIn (Local a) # 

Methods

namesIn :: Local a -> Set QName #

InstantiateFull a => InstantiateFull (Local a) # 

Methods

instantiateFull' :: Local a -> ReduceM (Local a) #

Judgements

data Judgement a #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType 

Fields

IsSort 

Fields

Instances

Show a => Show (Judgement a) # 
PrettyTCM a => PrettyTCM (Judgement a) # 

Methods

prettyTCM :: Judgement a -> TCM Doc #

Meta variables

data MetaVariable #

Constructors

MetaVar 

Fields

data Frozen #

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

Eq Frozen # 

Methods

(==) :: Frozen -> Frozen -> Bool #

(/=) :: Frozen -> Frozen -> Bool #

Show Frozen # 

data MetaInstantiation #

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenIFS

open, to be instantiated as "implicit from scope"

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

data TypeCheckingProblem #

Constructors

CheckExpr Expr Type 
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term) 
CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type

(λ (xs : t₀) → e) : t This is not an instance of CheckExpr as the domain type has already been checked. For example, when checking (λ (x y : Fin _) → e) : (x : Fin n) → ? we want to postpone (λ (y : Fin n) → e) : ? where Fin n is a Type rather than an Expr.

UnquoteTactic Term Term Type

First argument is computation and the others are hole and goal type

newtype MetaPriority #

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 

data MetaInfo #

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo 

Fields

type MetaNameSuggestion = String #

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

data NamedMeta #

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

Interaction meta variables

data InteractionPoint #

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

type InteractionPoints = Map InteractionId InteractionPoint #

Data structure managing the interaction points.

data IPClause #

Which clause is an interaction point located in?

Constructors

IPClause 

Fields

IPNoClause

The interaction point is not in the rhs of a clause.

Instances

Signature

type Definitions = HashMap QName Definition #

data DisplayForm #

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

data DisplayTerm #

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims

(f vs | ws) es. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Elims are additional arguments es (possible in case the with-application is of function type) or projections (if it is of record type).

DCon ConHead ConInfo [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

defaultDisplayForm :: QName -> [LocalDisplayForm] #

By default, we have no display form.

data NLPat #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar (Maybe CtxId) !Int [Arg Int]

Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.

PWild

Matches anything (e.g. irrelevant terms).

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom NLPType) (Abs NLPType)

Matches (x : A) → B

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

type PElims = [Elim' NLPat] #

data RewriteRule #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule 

Fields

data Definition #

Constructors

Defn 

Fields

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

Create a definition with sensible defaults.

type JSCode = String #

data CoreRepresentation #

Constructors

CrDefn CoreExpr

Core code for functions.

CrType CoreType

Core type for agda type.

CrConstr CoreConstr

Core constructor for agda constructor.

data Polarity #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

data Projection #

Additional information for projection Functions.

Constructors

Projection 

Fields

  • projProper :: Bool

    False if only projection-like, True if record projection.

  • projOrig :: QName

    The original projection name (current name could be from module application).

  • projFromType :: Arg QName

    Type projected from. Record type if projProper = Just{}. Also stores ArgInfo of the principal argument.

  • projIndex :: Int

    Index of the record argument. Start counting with 1, because 0 means that it is already applied to the record value. This can happen in module instantiation, but then either the record value is var 0, or funProjection == Nothing.

  • projLams :: ProjLams

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

newtype ProjLams #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams 

Fields

projDropPars :: Projection -> ProjOrigin -> Term #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo #

The info of the principal (record) argument.

data EtaEquality #

Should a record type admit eta-equality?

Constructors

Specified !Bool

User specifed 'eta-equality' or 'no-eta-equality'

Inferred !Bool

Positivity checker inferred whether eta is safe/

setEtaEquality :: EtaEquality -> Bool -> EtaEquality #

Make sure we do not overwrite a user specification.

data Defn #

Constructors

Axiom

Postulate.

AbstractDefn

Returned by getConstInfo if definition is abstract.

Function 

Fields

Datatype 

Fields

Record 

Fields

Constructor 

Fields

Primitive

Primitive or builtin functions.

Fields

emptyFunction :: Defn #

A template for creating Function definitions, with sensible defaults.

isEmptyFunction :: Defn -> Bool #

Checking whether we are dealing with a function yet to be defined.

newtype Fields #

Constructors

Fields [(Name, Type)] 

Instances

Null Fields # 

Methods

empty :: Fields #

null :: Fields -> Bool #

data Simplification #

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?

data Reduced no yes #

Instances

Functor (Reduced no) # 

Methods

fmap :: (a -> b) -> Reduced no a -> Reduced no b #

(<$) :: a -> Reduced no b -> Reduced no a #

data IsReduced #

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.

Constructors

NotReduced 
Reduced (Blocked ()) 

data MaybeReduced a #

Constructors

MaybeRed 

data AllowedReduction #

Controlling reduce.

Constructors

ProjectionReductions

(Projection and) projection-like functions may be reduced.

InlineReductions

Functions marked INLINE may be reduced.

CopatternReductions

Copattern definitions may be reduced.

FunctionReductions

Functions which are not projections may be reduced.

LevelReductions

Reduce Level terms.

NonTerminatingReductions

Functions that have not passed termination checking.

allReductions :: AllowedReductions #

Not quite all reductions (skip non-terminating reductions)

defDelayed :: Definition -> Delayed #

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool #

Has the definition failed the termination checker?

Injectivity

Mutual blocks

Statistics

Trace

Instance table

type InstanceTable = Map QName (Set QName) #

The instance table is a Map associating to every name of recorddata typepostulate its list of instances

type TempInstanceTable = (InstanceTable, Set QName) #

When typechecking something of the following form:

instance x : _ x = y

it's not yet known where to add x, so we add it to a list of unresolved instances and we'll deal with it later.

Builtin things

data BuiltinDescriptor #

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 Builtin pf #

Constructors

Builtin Term 
Prim pf 

Instances

Functor Builtin # 

Methods

fmap :: (a -> b) -> Builtin a -> Builtin b #

(<$) :: a -> Builtin b -> Builtin a #

Foldable Builtin # 

Methods

fold :: Monoid m => Builtin m -> m #

foldMap :: Monoid m => (a -> m) -> Builtin a -> m #

foldr :: (a -> b -> b) -> b -> Builtin a -> b #

foldr' :: (a -> b -> b) -> b -> Builtin a -> b #

foldl :: (b -> a -> b) -> b -> Builtin a -> b #

foldl' :: (b -> a -> b) -> b -> Builtin a -> b #

foldr1 :: (a -> a -> a) -> Builtin a -> a #

foldl1 :: (a -> a -> a) -> Builtin a -> a #

toList :: Builtin a -> [a] #

null :: Builtin a -> Bool #

length :: Builtin a -> Int #

elem :: Eq a => a -> Builtin a -> Bool #

maximum :: Ord a => Builtin a -> a #

minimum :: Ord a => Builtin a -> a #

sum :: Num a => Builtin a -> a #

product :: Num a => Builtin a -> a #

Traversable Builtin # 

Methods

traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b) #

sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a) #

mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b) #

sequence :: Monad m => Builtin (m a) -> m (Builtin a) #

Show pf => Show (Builtin pf) # 

Methods

showsPrec :: Int -> Builtin pf -> ShowS #

show :: Builtin pf -> String #

showList :: [Builtin pf] -> ShowS #

InstantiateFull a => InstantiateFull (Builtin a) # 

Highlighting levels

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () #

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

Constructors

ModuleParams 

Fields

type ModuleParamDict #

Arguments

 = Map ModuleName ModuleParameters

The map contains for each ModuleName M with module telescope Γ_M a substitution Γ ⊢ ρ_M : Γ_M from the current context Γ = envContext (clEnv).

data TCEnv #

Constructors

TCEnv 

Fields

Instances

MonadReader TCEnv ReduceM # 

Methods

ask :: ReduceM TCEnv

local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a

reader :: (TCEnv -> a) -> ReduceM a

MonadReader TCEnv TerM 

Methods

ask :: TerM TCEnv

local :: (TCEnv -> TCEnv) -> TerM a -> TerM a

reader :: (TCEnv -> a) -> TerM a

MonadIO m => MonadReader TCEnv (TCMT m) # 

Methods

ask :: TCMT m TCEnv

local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a

reader :: (TCEnv -> a) -> TCMT m a

data UnquoteFlags #

Constructors

UnquoteFlags 

e-prefixed lenses

Context

type Context = [ContextEntry] #

The Context is a stack of ContextEntrys.

data ContextEntry #

Constructors

Ctx 

Fields

Instances

newtype CtxId #

Constructors

CtxId Nat 

Instances

Let bindings

Abstract mode

data AbstractMode #

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 #

Constructors

ExpandLast

Add implicit arguments in the end until type is no longer hidden Pi.

DontExpandLast

Do not append implicit arguments.

data Candidate #

A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.

Type checking warnings (aka non-fatal errors)

data Warning #

A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.

Constructors

TerminationIssue [TerminationError] 
NotStrictlyPositive QName OccursWhere 
UnsolvedMetaVariables [Range]

Do not use directly with warning

UnsolvedInteractionMetas [Range]

Do not use directly with warning

UnsolvedConstraints Constraints

Do not use directly with warning

OldBuiltin String String

In `OldBuiltin old new`, the BUILTIN old has been replaced by new

EmptyRewritePragma

If the user wrote just {--}.

ParseWarning ParseWarning 

Instances

data TCWarning #

Constructors

TCWarning 

Fields

Type checking errors

data CallInfo #

Information about a call.

Constructors

CallInfo 

Fields

Instances

Show CallInfo #

We only show the name of the callee.

Pretty CallInfo # 

Methods

pretty :: CallInfo -> Doc #

prettyPrec :: Int -> CallInfo -> Doc #

AllNames CallInfo # 

Methods

allNames :: CallInfo -> Seq QName #

data TerminationError #

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError 

Fields

data SplitError #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)

Neither data type nor record.

IrrelevantDatatype (Closure Type)

Data type, but in irrelevant position.

CoinductiveDatatype (Closure Type)

Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor

CantSplit 

Fields

GenericSplitError String 

data TypeError #

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.

WrongInstanceDeclaration

A term is declared as an instance but it’s not allowed

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.

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 [DeBruijnPattern] 
ShouldBeASort Type

The given type should have been a sort.

ShouldBePi Type

The given type should have been a pi.

ShouldBeRecordType Type 
ShouldBeRecordPattern DeBruijnPattern 
NotAProjectionPattern (NamedArg Pattern) 
NotAProperTerm 
SetOmegaNotValidType 
InvalidTypeSort Sort

This sort is not a type expression.

InvalidType Term

This term is not a type expression.

FunctionTypeInSizeUniv Term

This term, a function type constructor, lives in SizeUniv, which is not allowed.

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.

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] 
WithOnFreeVariable Expr Term 
UnexpectedWithPatterns [Pattern] 
WithClausePatternMismatch Pattern Pattern 
FieldOutsideRecord 
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] 
IncompletePatternMatching Term [Elim] 
CoverageFailure QName [[NamedArg DeBruijnPattern]] 
UnreachableClauses QName [[NamedArg DeBruijnPattern]] 
CoverageCantSplitOn QName Telescope Args Args 
CoverageCantSplitIrrelevantType Type 
CoverageCantSplitType Type 
CoverageNoExactSplit QName Clause 
WithoutKError Type Term Term 
UnifyConflict ConHead ConHead 
UnifyCycle Int Term 
UnifyIndicesNotVars Type Term Term Args 
UnificationRecursiveEq Type Int Term 
UnificationStuck Telescope [Term] [Term] 
SplitError SplitError 
TooManyPolarities QName Integer 
LocalVsImportedModuleClash ModuleName 
SolvedButOpenHoles

Some interaction points (holes) have not been filled by user. There are not UnsolvedMetas since unification solved them. This is an error, since interaction points are never filled without user interaction.

CyclicModuleDependency [TopLevelModuleName] 
FileNotFound TopLevelModuleName [AbsolutePath] 
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName 
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] 
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName

Found module name, expected module name.

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 
NotValidBeforeField NiceDeclaration 
NothingAppliedToHiddenArg Expr 
NothingAppliedToInstanceArg Expr 
BadArgumentsToPatternSynonym QName 
TooFewArgumentsToPatternSynonym QName 
UnusedVariableInPatternSynonym 
NoParseForApplication [Expr] 
AmbiguousParseForApplication [Expr] [Expr] 
NoParseForLHS LHSOrPatSyn Pattern 
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] 
OperatorInformation [NotationSection] TypeError 
OperatorChangeMessage TypeError 
IFSNoCandidateInScope Type 
UnquoteFailed UnquoteError 
DeBruijnIndexOutOfScope Nat Telescope [Name] 
SafeFlagPostulate Name 
SafeFlagPragma [String] 
SafeFlagNonTerminating 
SafeFlagTerminating 
SafeFlagPrimTrustMe 
SafeFlagNoPositivityCheck 
SafeFlagPolarity 
NeedOptionCopatterns 
NeedOptionRewriting 
NonFatalErrors [TCWarning] 
InstanceSearchDepthExhausted Term Type Int 

data LHSOrPatSyn #

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

Constructors

IsLHS 
IsPatSyn 

data TCErr #

Type-checking errors.

Constructors

TypeError 

Fields

Exception Range Doc 
IOException Range IOException 
PatternErr

The exception which is usually caught. Raised for pattern violations during unification (assignV) but also in other situations where we want to backtrack.

The reduce monad

data ReduceEnv #

Environment of the reduce monad.

Constructors

ReduceEnv 

Fields

newtype ReduceM a #

Constructors

ReduceM 

Fields

Instances

Monad ReduceM # 

Methods

(>>=) :: ReduceM a -> (a -> ReduceM b) -> ReduceM b #

(>>) :: ReduceM a -> ReduceM b -> ReduceM b #

return :: a -> ReduceM a #

fail :: String -> ReduceM a #

Functor ReduceM # 

Methods

fmap :: (a -> b) -> ReduceM a -> ReduceM b #

(<$) :: a -> ReduceM b -> ReduceM a #

Applicative ReduceM # 

Methods

pure :: a -> ReduceM a #

(<*>) :: ReduceM (a -> b) -> ReduceM a -> ReduceM b #

(*>) :: ReduceM a -> ReduceM b -> ReduceM b #

(<*) :: ReduceM a -> ReduceM b -> ReduceM a #

ReadTCState ReduceM # 
HasOptions NLM # 
MonadReader TCEnv ReduceM # 

Methods

ask :: ReduceM TCEnv

local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a

reader :: (TCEnv -> a) -> ReduceM a

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b #

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b #

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b #

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) #

Type checking monad transformer

newtype TCMT m a #

Constructors

TCM 

Fields

Instances

MonadTrans TCMT # 

Methods

lift :: Monad m => m a -> TCMT m a #

MonadError TCErr IM # 

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadBench Phase TCM #

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

MonadIO m => MonadReader TCEnv (TCMT m) # 

Methods

ask :: TCMT m TCEnv

local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a

reader :: (TCEnv -> a) -> TCMT m a

MonadIO m => MonadState TCState (TCMT m) # 

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

state :: (TCState -> (a, TCState)) -> TCMT m a

MonadError TCErr (TCMT IO) # 

Methods

throwError :: TCErr -> TCMT IO a #

catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a #

MonadIO m => Monad (TCMT m) # 

Methods

(>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b #

(>>) :: TCMT m a -> TCMT m b -> TCMT m b #

return :: a -> TCMT m a #

fail :: String -> TCMT m a #

MonadIO m => Functor (TCMT m) # 

Methods

fmap :: (a -> b) -> TCMT m a -> TCMT m b #

(<$) :: a -> TCMT m b -> TCMT m a #

MonadIO m => Applicative (TCMT m) # 

Methods

pure :: a -> TCMT m a #

(<*>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b #

(*>) :: TCMT m a -> TCMT m b -> TCMT m b #

(<*) :: TCMT m a -> TCMT m b -> TCMT m a #

Semigroup (TCM Any) #

Short-cutting disjunction forms a monoid.

Methods

(<>) :: TCM Any -> TCM Any -> TCM Any #

sconcat :: NonEmpty (TCM Any) -> TCM Any #

stimes :: Integral b => b -> TCM Any -> TCM Any #

Monoid (TCM Any) # 

Methods

mempty :: TCM Any #

mappend :: TCM Any -> TCM Any -> TCM Any #

mconcat :: [TCM Any] -> TCM Any #

MonadIO m => MonadIO (TCMT m) # 

Methods

liftIO :: IO a -> TCMT m a #

Null (TCM Doc) # 

Methods

empty :: TCM Doc #

null :: TCM Doc -> Bool #

MonadIO m => MonadTCM (TCMT m) # 

Methods

liftTCM :: TCM a -> TCMT m a #

MonadIO m => ReadTCState (TCMT m) # 

Methods

getTCState :: TCMT m TCState #

MonadIO m => HasOptions (TCMT m) # 
MonadIO m => HasBuiltins (TCMT m) # 
HasConstInfo (TCMT IO) # 

type TCM = TCMT IO #

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

Minimal complete definition

liftTCM

Methods

liftTCM :: TCM a -> tcm a #

Instances

MonadTCM TerM # 

Methods

liftTCM :: TCM a -> TerM a #

MonadTCM tcm => MonadTCM (MaybeT tcm) # 

Methods

liftTCM :: TCM a -> MaybeT tcm a #

MonadTCM tcm => MonadTCM (ListT tcm) # 

Methods

liftTCM :: TCM a -> ListT tcm a #

MonadIO m => MonadTCM (TCMT m) # 

Methods

liftTCM :: TCM a -> TCMT m a #

MonadTCM m => MonadTCM (CompileT m) # 

Methods

liftTCM :: TCM a -> CompileT m a #

(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) # 

Methods

liftTCM :: TCM a -> WriterT w tcm a #

MonadTCM tcm => MonadTCM (ExceptT err tcm) # 

Methods

liftTCM :: TCM a -> ExceptT err tcm a #

(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) # 

Methods

liftTCM :: TCM a -> ExceptionT err tcm a #

runPM :: PM a -> TCM a #

Parse monad

type IM = TCMT (InputT IO) #

Interaction monad.

runIM :: IM a -> TCM a #

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

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a #

Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.

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

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

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

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

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

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

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

internalError :: MonadTCM tcm => String -> tcm a #

genericError :: MonadTCM tcm => String -> tcm a #

genericDocError :: MonadTCM tcm => Doc -> tcm a #

typeError :: MonadTCM tcm => TypeError -> tcm a #

warning :: MonadTCM tcm => Warning -> tcm () #

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) #

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) #

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a #

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) #

runSafeTCM runs a safe TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () #

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.

extendedLambdaName :: String #

Base name for extended lambda patterns

absurdLambdaName :: String #

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool #

Check whether we have an definition from an absurd lambda.

KillRange instances