| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Base

Contents

Type checking state
  Interface
  Closure
  Constraints
Open things
Judgements
  Meta variables
  Interaction meta variables
  Signature
  Injectivity
  Mutual blocks
  Statistics
  Trace
  Builtin things
Type checking environment
  Context
  Let bindings
  Abstract mode
Type checking errors
Type checking monad transformer

Synopsis

data TCState = TCSt {

stFreshThings :: FreshThings
stMetaStore :: MetaStore
stInteractionPoints :: InteractionPoints
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stModuleToSource :: ModuleToSource
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe ModuleName
stScope :: ScopeInfo
stPersistentOptions :: CommandLineOptions
stPragmaOptions :: CommandLineOptions
stStatistics :: Statistics
stTrace :: CallTrace
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: Set String

}

data FreshThings = Fresh {

fMeta :: MetaId
fInteraction :: InteractionId
fMutual :: MutualId
fName :: NameId
fCtx :: CtxId
fInteger :: Integer

}

initState :: TCState
stBuiltinThings :: TCState -> BuiltinThings PrimFun

data ModuleInfo = ModuleInfo {

miInterface :: Interface
miWarnings :: Bool
miTimeStamp :: ClockTime

}

type VisitedModules = Map TopLevelModuleName ModuleInfo
type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)

data Interface = Interface {

iImportedModules :: [ModuleName]
iModuleName :: ModuleName
iScope :: Map ModuleName Scope
iInsideScope :: ScopeInfo
iSignature :: Signature
iBuiltin :: BuiltinThings String
iHaskellImports :: Set String
iHighlighting :: HighlightingInfo

}

data Closure a = Closure {

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

}

buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
type ConstraintClosure = Closure Constraint

data Constraint

= ValueCmp Comparison Type Term Term
| TypeCmp Comparison Type Type
| TelCmp Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| UnBlock MetaId
| Guarded Constraint Constraints
| IsEmpty Type

data Comparison

= CmpEq
| CmpLeq

type Constraints = [ConstraintClosure]
data Open a = OpenThing [CtxId] a

data Judgement t a

= HasType a t
| IsSort a

data MetaVariable = MetaVar {

mvInfo :: MetaInfo
mvPriority :: MetaPriority
mvJudgement :: Judgement Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaId

}

data MetaInstantiation

= InstV Term
| InstS Term
| Open
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))

newtype MetaPriority = MetaPriority Int
type MetaInfo = Closure Range
type MetaStore = Map MetaId MetaVariable
normalMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
getMetaInfo :: MetaVariable -> MetaInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
type InteractionPoints = Map InteractionId MetaId
newtype InteractionId = InteractionId Nat

data Signature = Sig {

sigSections :: Sections
sigDefinitions :: Definitions

}

type Sections = Map ModuleName Section
type Definitions = Map QName Definition

data Section = Section {

secTelescope :: Telescope
secFreeVars :: Nat

}

emptySignature :: Signature
data DisplayForm = Display Nat [Term] DisplayTerm

data DisplayTerm

= DWithApp [DisplayTerm] Args
| DTerm Term

defaultDisplayForm :: QName -> [Open DisplayForm]

data Definition = Defn {

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

}

type HaskellCode = String
type HaskellType = String

data HaskellRepresentation

= HsDefn HaskellType HaskellCode
| HsType HaskellType

data Polarity

= Covariant
| Contravariant
| Invariant

data Occurrence

= Positive
| Negative
| Unused

data Defn

= Axiom {

axHsDef :: Maybe HaskellRepresentation

}

| Function {

funClauses :: [Clause]
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: Delayed

}

| Datatype {

dataPars :: Nat
dataIxs :: Nat
dataInduction :: Induction
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataPolarity :: [Polarity]
dataArgOccurrences :: [Occurrence]
dataHsType :: Maybe HaskellType
dataAbstr :: IsAbstract

}

| Record {

recPars :: Nat
recClause :: Maybe Clause
recCon :: Maybe QName
recConType :: Type
recFields :: [(Hiding, QName)]
recTel :: Telescope
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recAbstr :: IsAbstract

}

| Constructor {

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

}

| Primitive {

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

}

newtype Fields = Fields [(Name, Type)]

data Reduced no yes

= NoReduction no
| YesReduction yes

data PrimFun = PrimFun {

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

}

defClauses :: Definition -> [Clause]

data Delayed

= Delayed
| NotDelayed

defDelayed :: Definition -> Delayed
defAbstract :: Definition -> IsAbstract

data FunctionInverse

= NotInjective
| Inverse (Map TermHead Clause)

data TermHead

= SortHead
| PiHead
| ConHead QName

newtype MutualId = MutId Int
type Statistics = Map String Int
type CallTrace = Trace (Closure Call)
noTrace :: CallTrace

data Call

= CheckClause Type Clause (Maybe Clause)
| forall a . CheckPattern Pattern Telescope Type (Maybe a)
| CheckLetBinding LetBinding (Maybe ())
| InferExpr Expr (Maybe (Term, Type))
| CheckExpr Expr Type (Maybe Term)
| CheckDotPattern Expr Term (Maybe Constraints)
| CheckPatternShadowing Clause (Maybe ())
| IsTypeCall Expr Sort (Maybe Type)
| IsType_ Expr (Maybe Type)
| InferVar Name (Maybe (Term, Type))
| InferDef Range QName (Maybe (Term, Type))
| CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type, Constraints))
| CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
| CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
| CheckConstructor QName Telescope Sort Constructor (Maybe ())
| CheckFunDef Range Name [Clause] (Maybe ())
| CheckPragma Range Pragma (Maybe ())
| CheckPrimitive Range Name Expr (Maybe ())
| CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
| ScopeCheckExpr Expr (Maybe Expr)
| ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
| ScopeCheckLHS Name Pattern (Maybe LHS)
| ScopeCheckDefinition NiceDefinition (Maybe Definition)
| forall a . TermFunDef Range Name [Clause] (Maybe a)
| forall a . SetRange Range (Maybe a)

type BuiltinThings pf = Map String (Builtin pf)

data Builtin pf

= Builtin Term
| Prim pf

data TCEnv = TCEnv {

envContext :: Context
envLetBindings :: LetBindings
envCurrentModule :: ModuleName
envAnonymousModules :: [(ModuleName, Nat)]
envImportPath :: [TopLevelModuleName]
envMutualBlock :: Maybe MutualId
envAbstractMode :: AbstractMode
envReplace :: Bool
envDisplayFormsEnabled :: Bool
envReifyInteractionPoints :: Bool

}

initEnv :: TCEnv
type Context = [ContextEntry]

data ContextEntry = Ctx {

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

}

newtype CtxId = CtxId Nat
type LetBindings = Map Name (Open (Term, Type))

data AbstractMode

= AbstractMode
| ConcreteMode
| IgnoreAbstractMode

data Occ

= OccCon {

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

}

| OccClause {

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

}

data OccPos

= NonPositively
| ArgumentTo Nat QName

data TypeError

= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [([QName], [Range])]
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| DependentPatternMatchingOnCodata
| NotInductive Term
| UninstantiatedDotPattern Expr
| IlltypedPattern Pattern Type
| TooManyArgumentsInLHS Nat Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| NotAProperTerm
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalHiding Type Type
| UnequalSorts Sort Sort
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| 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
| BothWithAndRHS
| NotInScope [QName]
| NoSuchModule QName
| AmbiguousName QName [QName]
| AmbiguousModule QName [ModuleName]
| UninstantiatedModule QName
| ClashingDefinition QName QName
| ClashingModule ModuleName ModuleName
| ClashingImport Name QName
| ClashingModuleImport Name ModuleName
| PatternShadowsConstructor Name QName
| ModuleDoesntExport QName [ImportedName]
| InvalidPattern Pattern
| RepeatedVariablesInPattern [Name]
| NotAModuleExpr Expr
| NotAnExpression Expr
| NotAValidLetBinding NiceDeclaration
| NothingAppliedToHiddenArg Expr
| NoParseForApplication [Expr]
| AmbiguousParseForApplication [Expr] [Expr]
| NoParseForLHS Pattern
| AmbiguousParseForLHS Pattern [Pattern]

data TCErr'

= TypeError TCState (Closure TypeError)
| Exception Range String
| IOException Range IOException
| PatternErr TCState
| AbortAssign TCState

data TCErr = TCErr {

errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
errError :: TCErr'

}

newtype TCMT m a = TCM {

unTCM :: StateT TCState (ReaderT TCEnv m) a

}

type TCM = TCMT IO
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where

liftTCM :: TCM a -> tcm a

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
patternViolation :: MonadTCM tcm => tcm a
internalError :: MonadTCM tcm => String -> tcm a
typeError :: MonadTCM tcm => TypeError -> tcm a
runTCM :: TCMT IO a -> IO (Either TCErr a)
runTCM' :: Monad m => TCMT m a -> m a

Type checking state

data TCState | Source

Constructors

TCSt |

stFreshThings :: FreshThings |
stMetaStore :: MetaStore |
stInteractionPoints :: InteractionPoints |
stConstraints :: Constraints |
stSignature :: Signature |
stImports :: Signature |
stImportedModules :: Set ModuleName |
stModuleToSource :: ModuleToSource |
stVisitedModules :: VisitedModules |
stDecodedModules :: DecodedModules |
stCurrentModule :: Maybe ModuleName | The current module is available after it has been type checked.
stScope :: ScopeInfo |
stPersistentOptions :: CommandLineOptions | Options which apply to all files, unless overridden.
stPragmaOptions :: CommandLineOptions | Options applying to the current file. `OPTIONS` pragmas only affect this field.
stStatistics :: Statistics |
stTrace :: CallTrace | record what is happening (for error msgs)
stMutualBlocks :: Map MutualId (Set QName) |
stLocalBuiltins :: BuiltinThings PrimFun |
stImportedBuiltins :: BuiltinThings PrimFun |
stHaskellImports :: Set String | Imports that should be generated by the compiler (this includes imports from imported modules).

Instances

MonadState TCState Unify
HasFresh i FreshThings => HasFresh i TCState
MonadIO m => MonadState TCState (TCMT m)

data FreshThings | Source

Constructors

Fresh |

fMeta :: MetaId |
fInteraction :: InteractionId |
fMutual :: MutualId |
fName :: NameId |
fCtx :: CtxId |
fInteger :: Integer | Can be used for various things.

Instances

Show FreshThings
HasFresh Integer FreshThings
HasFresh NameId FreshThings
HasFresh MetaId FreshThings
HasFresh CtxId FreshThings
HasFresh MutualId FreshThings
HasFresh InteractionId FreshThings

initState :: TCState | Source

stBuiltinThings :: TCState -> BuiltinThings PrimFun | Source

Interface

data ModuleInfo | Source

Constructors

ModuleInfo |

miInterface :: Interface |
miWarnings :: Bool | `True` if warnings were encountered when the module was type checked.
miTimeStamp :: ClockTime | The modification time stamp of the interface file when the interface was read or written. Alternatively, if warnings were encountered (in which case there may not be any up-to-date interface file), the time at which the interface was produced (approximately).

type VisitedModules = Map TopLevelModuleName ModuleInfo | Source

type DecodedModules = Map TopLevelModuleName (Interface, ClockTime) | Source

data Interface | Source

Constructors

Interface |

iImportedModules :: [ModuleName] |
iModuleName :: ModuleName |
iScope :: Map ModuleName Scope |
iInsideScope :: ScopeInfo |
iSignature :: Signature |
iBuiltin :: BuiltinThings String |
iHaskellImports :: Set String | Haskell imports listed in (transitively) imported modules are not included here.
iHighlighting :: HighlightingInfo |

Instances

Data Interface
Show Interface
Typeable Interface
EmbPrj Interface
InstantiateFull Interface

Closure

data Closure a | Source

Constructors

Closure |

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

Instances

Typeable1 Closure
Data a => Data (Closure a)
Show a => Show (Closure a)
HasRange a => HasRange (Closure a)
InstantiateFull a => InstantiateFull (Closure a)
Normalise a => Normalise (Closure a)
Reduce a => Reduce (Closure a)
Instantiate a => Instantiate (Closure a)
PrettyTCM a => PrettyTCM (Closure a)

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

Constraints

type ConstraintClosure = Closure Constraint | Source

data Constraint | Source

Constructors

ValueCmp Comparison Type Term Term |
TypeCmp Comparison Type Type |
TelCmp Comparison Telescope Telescope |
SortCmp Comparison Sort Sort |
UnBlock MetaId |
Guarded Constraint Constraints |
IsEmpty Type |

Instances

Show Constraint
Typeable Constraint
InstantiateFull Constraint
Normalise Constraint
Reduce Constraint
Instantiate Constraint
PrettyTCM Constraint
Reify Constraint (OutputForm Expr Expr)

data Comparison | Source

Constructors

CmpEq |
CmpLeq |

Instances

Eq Comparison
Show Comparison
Typeable Comparison
PrettyTCM Comparison

type Constraints = [ConstraintClosure] | Source

Open things

data Open a | Source

A thing tagged with the context it came from.
Constructors

OpenThing [CtxId] a |

Instances

Typeable1 Open
Data a => Data (Open a)
Show a => Show (Open a)
EmbPrj a => EmbPrj (Open a)
InstantiateFull a => InstantiateFull (Open a)

Judgements

data Judgement t a | Source

Constructors

HasType a t |
IsSort a |

Instances

Typeable2 Judgement
Functor (Judgement t)
Traversable (Judgement t)
Foldable (Judgement t)
(Data t, Data a) => Data (Judgement t a)
(Show t, Show a) => Show (Judgement t a)
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a')

Meta variables

data MetaVariable | Source

Constructors

MetaVar |

mvInfo :: MetaInfo |
mvPriority :: MetaPriority | some metavariables are more eager to be instantiated
mvJudgement :: Judgement Type MetaId |
mvInstantiation :: MetaInstantiation |
mvListeners :: Set MetaId | metavariables interested in what happens to this guy

Instances

Typeable MetaVariable
SetRange MetaVariable
HasRange MetaVariable

data MetaInstantiation | Source

Constructors

InstV Term |
InstS Term |
Open |
BlockedConst Term |
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool)) |

Instances

Show MetaInstantiation
Typeable MetaInstantiation

newtype MetaPriority | Source

Constructors

MetaPriority Int |

Instances

Eq MetaPriority
Ord MetaPriority
Show MetaPriority

type MetaInfo = Closure Range | Source

TODO: Not so nice.

type MetaStore = Map MetaId MetaVariable | Source

normalMetaPriority :: MetaPriority | Source

lowMetaPriority :: MetaPriority | Source

highMetaPriority :: MetaPriority | Source

getMetaInfo :: MetaVariable -> MetaInfo | Source

getMetaScope :: MetaVariable -> ScopeInfo | Source

getMetaEnv :: MetaVariable -> TCEnv | Source

getMetaSig :: MetaVariable -> Signature | Source

Interaction meta variables

type InteractionPoints = Map InteractionId MetaId | Source

newtype InteractionId | Source

Constructors

InteractionId Nat |

Instances

Enum InteractionId
Eq InteractionId
Integral InteractionId
Num InteractionId
Ord InteractionId
Real InteractionId
Show InteractionId
HasFresh InteractionId FreshThings
ToConcrete InteractionId Expr

Signature

data Signature | Source

Constructors

Sig |

sigSections :: Sections |
sigDefinitions :: Definitions |

Instances

Data Signature
Show Signature
Typeable Signature
EmbPrj Signature
InstantiateFull Signature

type Sections = Map ModuleName Section | Source

type Definitions = Map QName Definition | Source

data Section | Source

Constructors

Section |

secTelescope :: Telescope |
secFreeVars :: Nat | This is the number of parameters when we're inside the section and 0 outside. It's used to know how much of the context to apply function from the section to when translating from abstract to internal syntax.

Instances

Data Section
Show Section
Typeable Section
EmbPrj Section
InstantiateFull Section

emptySignature :: Signature | Source

data DisplayForm | Source

Constructors

Display Nat [Term] DisplayTerm

The three arguments are:

- `n`: number of free variables;
- Patterns for arguments, one extra free var which represents pattern vars. There should `n` of them.
- Display form. `n` free variables.

Instances

Data DisplayForm
Show DisplayForm
Typeable DisplayForm
Raise DisplayForm
EmbPrj DisplayForm
InstantiateFull DisplayForm
Normalise DisplayForm

data DisplayTerm | Source

Constructors

DWithApp [DisplayTerm] Args |
DTerm Term |

Instances

Data DisplayTerm
Show DisplayTerm
Typeable DisplayTerm
Raise DisplayTerm
Subst DisplayTerm
Apply DisplayTerm
EmbPrj DisplayTerm
InstantiateFull DisplayTerm
PrettyTCM DisplayTerm
Reify DisplayTerm Expr

defaultDisplayForm :: QName -> [Open DisplayForm] | Source

data Definition | Source

Constructors

Defn |

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

Instances

Data Definition
Show Definition
Typeable Definition
Abstract Definition
Apply Definition
EmbPrj Definition
InstantiateFull Definition

type HaskellCode = String | Source

type HaskellType = String | Source

data HaskellRepresentation | Source

Constructors

HsDefn HaskellType HaskellCode |
HsType HaskellType |

Instances

Data HaskellRepresentation
Show HaskellRepresentation
Typeable HaskellRepresentation
EmbPrj HaskellRepresentation

data Polarity | Source

Constructors

Covariant |
Contravariant |
Invariant |

Instances

Eq Polarity
Data Polarity
Show Polarity
Typeable Polarity
EmbPrj Polarity

data Occurrence | Source

`Positive` means strictly positive and `Negative` means not strictly positive.
Constructors

Positive |
Negative |
Unused |

Instances

Eq Occurrence
Data Occurrence
Ord Occurrence
Show Occurrence
Typeable Occurrence
SemiRing Occurrence
EmbPrj Occurrence

data Defn | Source

Constructors

Axiom |

axHsDef :: Maybe HaskellRepresentation |

Function |

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

Datatype |

dataPars :: Nat |
dataIxs :: Nat |
dataInduction :: Induction |
dataClause :: Maybe Clause |
dataCons :: [QName] |
dataSort :: Sort |
dataPolarity :: [Polarity] |
dataArgOccurrences :: [Occurrence] |
dataHsType :: Maybe HaskellType |
dataAbstr :: IsAbstract |

Record |

recPars :: Nat |
recClause :: Maybe Clause |
recCon :: Maybe QName | Constructor name.
recConType :: Type | The record constructor's type.
recFields :: [(Hiding, QName)] |
recTel :: Telescope |
recPolarity :: [Polarity] |
recArgOccurrences :: [Occurrence] |
recAbstr :: IsAbstract |

Constructor |

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

Primitive | Primitive or builtin functions.

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

Instances

Data Defn
Show Defn
Typeable Defn
Abstract Defn
Apply Defn
EmbPrj Defn
InstantiateFull Defn

newtype Fields | Source

Constructors

Fields [(Name, Type)] |

Instances

Data Fields
Typeable Fields

data Reduced no yes | Source

Constructors

NoReduction no |
YesReduction yes |

Instances

Typeable2 Reduced

data PrimFun | Source

Constructors

PrimFun |

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

Instances

Typeable PrimFun
Abstract PrimFun
Apply PrimFun

defClauses :: Definition -> [Clause] | Source

data Delayed | Source

Used to specify whether something should be delayed.
Constructors

Delayed |
NotDelayed |

Instances

Eq Delayed
Data Delayed
Show Delayed
Typeable Delayed
EmbPrj Delayed

defDelayed :: Definition -> Delayed | Source

Are the clauses of this definition delayed?

defAbstract :: Definition -> IsAbstract | Source

Injectivity

data FunctionInverse | Source

Constructors

NotInjective |
Inverse (Map TermHead Clause) |

Instances

Data FunctionInverse
Show FunctionInverse
Typeable FunctionInverse
Abstract FunctionInverse
Apply FunctionInverse
EmbPrj FunctionInverse
InstantiateFull FunctionInverse

data TermHead | Source

Constructors

SortHead |
PiHead |
ConHead QName |

Instances

Eq TermHead
Data TermHead
Ord TermHead
Show TermHead
Typeable TermHead
EmbPrj TermHead

Mutual blocks

newtype MutualId | Source

Constructors

MutId Int |

Instances

Eq MutualId
Data MutualId
Num MutualId
Ord MutualId
Show MutualId
Typeable MutualId
EmbPrj MutualId
HasFresh MutualId FreshThings

Statistics

type Statistics = Map String Int | Source

Trace

type CallTrace = Trace (Closure Call) | Source

noTrace :: CallTrace | Source

data Call | Source

Constructors

CheckClause Type Clause (Maybe Clause) |
forall a . CheckPattern Pattern Telescope Type (Maybe a) |
CheckLetBinding LetBinding (Maybe ()) |
InferExpr Expr (Maybe (Term, Type)) |
CheckExpr Expr Type (Maybe Term) |
CheckDotPattern Expr Term (Maybe Constraints) |
CheckPatternShadowing Clause (Maybe ()) |
IsTypeCall Expr Sort (Maybe Type) |
IsType_ Expr (Maybe Type) |
InferVar Name (Maybe (Term, Type)) |
InferDef Range QName (Maybe (Term, Type)) |
CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type, Constraints)) |
CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckConstructor QName Telescope Sort Constructor (Maybe ()) |
CheckFunDef Range Name [Clause] (Maybe ()) |
CheckPragma Range Pragma (Maybe ()) |
CheckPrimitive Range Name Expr (Maybe ()) |
CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ()) |
ScopeCheckExpr Expr (Maybe Expr) |
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration]) |
ScopeCheckLHS Name Pattern (Maybe LHS) |
ScopeCheckDefinition NiceDefinition (Maybe Definition) |
forall a . TermFunDef Range Name [Clause] (Maybe a) |
forall a . SetRange Range (Maybe a) | used by setCurrentRange actually, a is Agda.Termination.TermCheck.CallGraph but I was to lazy to import the stuff here --Andreas,2007-5-29

Instances

Data Call
Typeable Call
HasRange Call
PrettyTCM Call

Builtin things

type BuiltinThings pf = Map String (Builtin pf) | Source

data Builtin pf | Source

Constructors

Builtin Term |
Prim pf |

Instances

Functor Builtin
Typeable1 Builtin
Traversable Builtin
Foldable Builtin
Data pf => Data (Builtin pf)
Show pf => Show (Builtin pf)
EmbPrj a => EmbPrj (Builtin a)
InstantiateFull a => InstantiateFull (Builtin a)

Type checking environment

data TCEnv | Source

Constructors

TCEnv |

envContext :: Context |
envLetBindings :: LetBindings |
envCurrentModule :: ModuleName |
envAnonymousModules :: [(ModuleName, Nat)] | anonymous modules and their number of free variables
envImportPath :: [TopLevelModuleName] | to detect import cycles
envMutualBlock :: Maybe MutualId | the current (if any) mutual block
envAbstractMode :: AbstractMode | When checking the typesignature of a public definition or the body of a non-abstract definition this is true. To prevent information about abstract things leaking outside the module.

envReplace :: Bool

Coinductive constructor applications `c args` get replaced by a function application `f tel`, where tel corresponds to the current telescope and `f` is defined as `f tel = c args`. The initial occurrence of `c` in the body of `f` should not be replaced by yet another function application, though. To avoid that this happens the `envReplace` flag is set to `False` when `f` is checked.

envDisplayFormsEnabled :: Bool | Sometimes we want to disable display forms.
envReifyInteractionPoints :: Bool | should we try to recover interaction points when reifying? disabled when generating types for with functions

Instances

Data TCEnv
Typeable TCEnv
MonadReader TCEnv Unify
MonadIO m => MonadReader TCEnv (TCMT m)

initEnv :: TCEnv | Source

Context

type Context = [ContextEntry] | Source

data ContextEntry | Source

Constructors

Ctx |

ctxId :: CtxId |
ctxEntry :: Arg (Name, Type) |

Instances

Data ContextEntry
Typeable ContextEntry

newtype CtxId | Source

Constructors

CtxId Nat |

Instances

Enum CtxId
Eq CtxId
Integral CtxId
Data CtxId
Num CtxId
Ord CtxId
Real CtxId
Show CtxId
Typeable CtxId
EmbPrj CtxId
HasFresh CtxId FreshThings

Let bindings

type LetBindings = Map Name (Open (Term, Type)) | Source

Abstract mode

data AbstractMode | Source

Constructors

AbstractMode | abstract things in the current module can be accessed
ConcreteMode | no abstract things can be accessed
IgnoreAbstractMode | all abstract things can be accessed

Instances

Data AbstractMode
Typeable AbstractMode

Type checking errors

data Occ | Source

Constructors

OccCon |

occDatatype :: QName |
occConstructor :: QName |
occPosition :: OccPos |

OccClause |

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

data OccPos | Source

Constructors

NonPositively |
ArgumentTo Nat QName |

data TypeError | Source

Constructors

InternalError String |
NotImplemented String |
NotSupported String |
CompilationError String |
TerminationCheckFailed [([QName], [Range])] | Parameterised on functions which failed to termination check (grouped if they are mutual), along with ranges for problematic call sites.
PropMustBeSingleton |
DataMustEndInSort Term |
ShouldEndInApplicationOfTheDatatype Type | The target of a constructor isn't an application of its datatype. The `Type` records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term Term | The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.
ShouldBeApplicationOf Type QName | Expected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QName | constructor, datatype
DoesNotConstructAnElementOf QName Term | constructor, type
DifferentArities | Varying number of arguments for a function.
WrongHidingInLHS Type | The left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda Type | Expected a non-hidden function and found a hidden lambda.
WrongHidingInApplication Type | A function is applied to a hidden argument where a non-hidden was expected.
DependentPatternMatchingOnCodata |
NotInductive Term | The term does not correspond to an inductive data type.
UninstantiatedDotPattern Expr |
IlltypedPattern Pattern Type |
TooManyArgumentsInLHS Nat Type |
WrongNumberOfConstructorArguments QName Nat Nat |
ShouldBeEmpty Type [Pattern] |
ShouldBeASort Type | The given type should have been a sort.
ShouldBePi Type | The given type should have been a pi.
ShouldBeRecordType Type |
NotAProperTerm |
UnequalTerms Comparison Term Term Type |
UnequalTypes Comparison Type Type |
UnequalTelescopes Comparison Telescope Telescope |
UnequalHiding Type Type | The two function types have different hiding.
UnequalSorts Sort Sort |
NotLeqSort Sort Sort |
MetaCannotDependOn MetaId [Nat] Nat | The arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.
MetaOccursInItself MetaId |
GenericError String |
BuiltinMustBeConstructor String Expr |
NoSuchBuiltinName String |
DuplicateBuiltinBinding String Term Term |
NoBindingForBuiltin String |
NoSuchPrimitiveFunction String |
ShadowedModule [ModuleName] |
BuiltinInParameterisedModule String |
NoRHSRequiresAbsurdPattern [NamedArg Pattern] |
AbsurdPatternRequiresNoRHS [NamedArg Pattern] |
TooFewFields QName [Name] |
TooManyFields QName [Name] |
DuplicateFields [Name] |
DuplicateConstructors [Name] |
UnexpectedWithPatterns [Pattern] |
WithClausePatternMismatch Pattern Pattern |
FieldOutsideRecord |
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] |
IncompletePatternMatching Term Args |
CoverageFailure QName [[Arg Pattern]] |
UnreachableClauses QName [[Arg Pattern]] |
CoverageCantSplitOn QName |
CoverageCantSplitType Type |
NotStrictlyPositive QName [Occ] |
LocalVsImportedModuleClash ModuleName |
UnsolvedMetas [Range] |
UnsolvedConstraints Constraints |
CyclicModuleDependency [TopLevelModuleName] |
FileNotFound TopLevelModuleName [AbsolutePath] |
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName |
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] |
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] |
ClashingFileNamesFor ModuleName [AbsolutePath] |
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath | Module name, file from which it was loaded, file which the include path says contains the module. Scope errors
BothWithAndRHS |
NotInScope [QName] |
NoSuchModule QName |
AmbiguousName QName [QName] |
AmbiguousModule QName [ModuleName] |
UninstantiatedModule QName |
ClashingDefinition QName QName |
ClashingModule ModuleName ModuleName |
ClashingImport Name QName |
ClashingModuleImport Name ModuleName |
PatternShadowsConstructor Name QName |
ModuleDoesntExport QName [ImportedName] |
InvalidPattern Pattern |
RepeatedVariablesInPattern [Name] |
NotAModuleExpr Expr | The expr was used in the right hand side of an implicit module definition, but it wasn't of the form `m Delta`.
NotAnExpression Expr |
NotAValidLetBinding NiceDeclaration |
NothingAppliedToHiddenArg Expr |
NoParseForApplication [Expr] |
AmbiguousParseForApplication [Expr] [Expr] |
NoParseForLHS Pattern |
AmbiguousParseForLHS Pattern [Pattern] |

Instances

Show TypeError
Typeable TypeError
Error TypeError
PrettyTCM TypeError

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

Instances

Show TCErr'
Typeable TCErr'
HasRange TCErr'

data TCErr | Source

Type-checking errors, potentially paired with relevant syntax highlighting information.
Constructors

TCErr |

errHighlighting :: Maybe (HighlightingInfo, ModuleToSource) | The `ModuleToSource` can be used to map the module names in the `HighlightingInfo` to file names.
errError :: TCErr' |

Instances

Show TCErr
Typeable TCErr
Exception TCErr
Error TCErr
HasRange TCErr
PrettyTCM TCErr
MonadError TCErr IM
MonadError TCErr (TCMT IO)

Type checking monad transformer

newtype TCMT m a | Source

Constructors

TCM |

unTCM :: StateT TCState (ReaderT TCEnv m) a |

Instances

MonadTrans TCMT
MonadError TCErr IM
MonadError TCErr (TCMT IO)
MonadIO m => MonadReader TCEnv (TCMT m)
MonadIO m => MonadState TCState (TCMT m)
MonadIO m => Monad (TCMT m)
MonadIO m => Functor (TCMT m)
MonadIO m => Applicative (TCMT m)
MonadIO m => MonadIO (TCMT m)
MonadIO m => MonadTCM (TCMT m)

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 Unify
MonadIO m => MonadTCM (TCMT m)
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm)
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm)

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

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

patternViolation :: MonadTCM tcm => tcm a | Source

internalError :: MonadTCM tcm => String -> tcm a | Source

typeError :: MonadTCM tcm => TypeError -> tcm a | Source

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

Running the type checking monad

runTCM' :: Monad m => TCMT m a -> m a | Source

Produced by Haddock version 2.4.2