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

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 :: PragmaOptions
  - stStatistics :: Statistics
  - 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
  - iPragmaOptions :: [OptionsPragma]
  }
- data Closure a = Closure {
  - clSignature :: Signature
  - clEnv :: TCEnv
  - clScope :: ScopeInfo
  - clValue :: a
  }
- buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
- type ConstraintClosure = Closure Constraint
- data Constraint
  - = ValueCmp Comparison Type Term Term
  - | ArgsCmp [Polarity] Type Args Args
  - | TypeCmp Comparison Type Type
  - | TelCmp Comparison Telescope Telescope
  - | SortCmp Comparison Sort Sort
  - | LevelCmp Comparison Term Term
  - | 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
  - mvPermutation :: Permutation
  - 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 {
  - defRelevance :: Relevance
  - defName :: QName
  - defType :: Type
  - defDisplay :: [Open DisplayForm]
  - defMutual :: MutualId
  - theDef :: Defn
  }
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- data HaskellRepresentation
  - = HsDefn HaskellType HaskellCode
  - | HsType HaskellType
- data Polarity
  - = Covariant
  - | Contravariant
  - | Invariant
- data Occurrence
  - = Positive
  - | Negative
  - | Unused
- data Defn
  - = Axiom {
    - axHsDef :: Maybe HaskellRepresentation
    - axEpDef :: Maybe EpicCode
    }
  - | Function {
    - funClauses :: [Clauses]
    - funCompiled :: CompiledClauses
    - funInv :: FunctionInverse
    - funPolarity :: [Polarity]
    - funArgOccurrences :: [Occurrence]
    - funAbstr :: IsAbstract
    - funDelayed :: Delayed
    - funProjection :: Maybe Int
    }
  - | 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 :: QName
    - recNamedCon :: Bool
    - recConType :: Type
    - recFields :: [Arg QName]
    - recTel :: Telescope
    - recPolarity :: [Polarity]
    - recArgOccurrences :: [Occurrence]
    - recEtaEquality :: Bool
    - recAbstr :: IsAbstract
    }
  - | Constructor {
    - conPars :: Nat
    - conSrcCon :: QName
    - conData :: QName
    - conHsCode :: Maybe (HaskellType, HaskellCode)
    - conAbstr :: IsAbstract
    - conInd :: Induction
    }
  - | Primitive {
    - primAbstr :: IsAbstract
    - primName :: String
    - primClauses :: Maybe [Clauses]
    - primCompiled :: Maybe CompiledClauses
    }
- defIsRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Reduced no yes
  - = NoReduction no
  - | YesReduction yes
- data IsReduced
  - = NotReduced
  - | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
  - isReduced :: IsReduced
  - ignoreReduced :: a
  }
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked a -> MaybeReduced a
- data PrimFun = PrimFun {
  - primFunName :: QName
  - primFunArity :: Arity
  - primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced MaybeReducedArgs Term)
  }
- defClauses :: Definition -> [Clauses]
- defCompiled :: Definition -> Maybe CompiledClauses
- 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 Int32
- type Statistics = Map String Int
- 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
  - envIrrelevant :: Bool
  - envReplace :: Bool
  - envDisplayFormsEnabled :: Bool
  - envReifyInteractionPoints :: Bool
  - envEtaContractImplicit :: Bool
  - envRange :: Range
  - envCall :: Maybe (Closure Call)
  }
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {
  - ctxId :: CtxId
  - ctxEntry :: Arg (Name, Type)
  }
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Arg 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
  - | IndicesNotConstructorApplications [Arg Term]
  - | IndexVariablesNotDistinct [Arg Term]
  - | IndexFreeInParameter Nat [Arg Term]
  - | DoesNotConstructAnElementOf QName Term
  - | DifferentArities
  - | WrongHidingInLHS Type
  - | WrongHidingInLambda Type
  - | WrongHidingInApplication Type
  - | NotInductive Term
  - | UninstantiatedDotPattern Expr
  - | IlltypedPattern Pattern Type
  - | TooManyArgumentsInLHS Nat Type
  - | WrongNumberOfConstructorArguments QName Nat Nat
  - | ShouldBeEmpty Type [Pattern]
  - | ShouldBeASort Type
  - | ShouldBePi Type
  - | 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
  - | 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]
  - | DuplicateImports 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 :: TCState -> TCEnv -> m (a, TCState)
  }
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
  - liftTCM :: TCM a -> tcm a
- catchError_ :: TCM a -> (TCErr -> 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

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

Instances

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

data FreshThings

Constructors

Fresh |

Fields

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

stBuiltinThings :: TCState -> BuiltinThings PrimFun

## Interface

data ModuleInfo

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

type VisitedModules = Map TopLevelModuleName ModuleInfo

type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)

data Interface

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.

Instances

Data Interface |
Show Interface |
Typeable Interface |
EmbPrj Interface |
InstantiateFull Interface |

## Closure

data Closure a

Constructors

Closure |

Fields

clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
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)

## Constraints

type ConstraintClosure = Closure Constraint

data Constraint

Constructors

ValueCmp Comparison Type Term Term |
ArgsCmp [Polarity] Type Args Args |
TypeCmp Comparison Type Type |
TelCmp Comparison Telescope Telescope |
SortCmp Comparison Sort Sort |
LevelCmp Comparison Term Term |
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

Constructors

CmpEq |
CmpLeq |

Instances

Eq Comparison |
Show Comparison |
Typeable Comparison |
PrettyTCM Comparison |

type Constraints = [ConstraintClosure]

# Open things

data Open a

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

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

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

Instances

Typeable MetaVariable |
SetRange MetaVariable |
HasRange MetaVariable |

data MetaInstantiation

Constructors

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

Instances

Show MetaInstantiation |
Typeable MetaInstantiation |

newtype MetaPriority

Constructors

MetaPriority Int |

Instances

Eq MetaPriority |
Ord MetaPriority |
Show MetaPriority |

type MetaInfo = Closure Range

TODO: Not so nice.

type MetaStore = Map MetaId MetaVariable

normalMetaPriority :: MetaPriority

lowMetaPriority :: MetaPriority

highMetaPriority :: MetaPriority

getMetaInfo :: MetaVariable -> MetaInfo

getMetaScope :: MetaVariable -> ScopeInfo

getMetaEnv :: MetaVariable -> TCEnv

getMetaSig :: MetaVariable -> Signature

## Interaction meta variables

type InteractionPoints = Map InteractionId MetaId

newtype InteractionId

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

Constructors

Sig |

Fields

sigSections :: Sections
sigDefinitions :: Definitions

Instances

Data Signature |
Show Signature |
Typeable Signature |
EmbPrj Signature |
InstantiateFull Signature |

type Sections = Map ModuleName Section

type Definitions = Map QName Definition

data Section

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

Data Section |
Show Section |
Typeable Section |
EmbPrj Section |
InstantiateFull Section |

emptySignature :: Signature

data DisplayForm

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

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]

data Definition

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

Instances

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

type HaskellCode = String

type HaskellType = String

type EpicCode = String

data HaskellRepresentation

Constructors

HsDefn HaskellType HaskellCode |
HsType HaskellType |

Instances

Data HaskellRepresentation |
Show HaskellRepresentation |
Typeable HaskellRepresentation |
EmbPrj HaskellRepresentation |

data Polarity

Constructors

Covariant |
Contravariant |
Invariant |

Instances

Eq Polarity |
Data Polarity |
Show Polarity |
Typeable Polarity |
EmbPrj Polarity |

data Occurrence

`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

Constructors

Axiom |

Fields

axHsDef :: Maybe HaskellRepresentation
axEpDef :: Maybe EpicCode

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 |

Fields

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

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

Instances

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

defIsRecord :: Defn -> Bool

newtype Fields

Constructors

Fields [(Name, Type)] |

Instances

Data Fields |
Typeable Fields |

data Reduced no yes

Constructors

NoReduction no |
YesReduction yes |

Instances

Typeable2 Reduced |

data IsReduced

Constructors

NotReduced |
Reduced (Blocked ()) |

data MaybeReduced a

Constructors

MaybeRed |

Fields

isReduced :: IsReduced
ignoreReduced :: a

Instances

Functor MaybeReduced |

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

notReduced :: a -> MaybeReduced a

reduced :: Blocked a -> MaybeReduced a

data PrimFun

Constructors

PrimFun |

Fields

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

Instances

Typeable PrimFun |
Abstract PrimFun |
Apply PrimFun |

defClauses :: Definition -> [Clauses]

defCompiled :: Definition -> Maybe CompiledClauses

data Delayed

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

Are the clauses of this definition delayed?

defAbstract :: Definition -> IsAbstract

## Injectivity

data FunctionInverse

Constructors

NotInjective |
Inverse (Map TermHead Clause) |

Instances

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

data TermHead

Constructors

SortHead |
PiHead |
ConHead QName |

Instances

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

## Mutual blocks

newtype MutualId

Constructors

MutId Int32 |

Instances

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

## Statistics

type Statistics = Map String Int

## Trace

data Call

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)

data Builtin pf

Constructors

Builtin Term |
Prim pf |

Instances

Functor Builtin |
Typeable1 Builtin |
Foldable Builtin |
Traversable 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

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

Instances

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

initEnv :: TCEnv

## Context

type Context = [ContextEntry]

data ContextEntry

Constructors

Ctx |

Fields

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

Instances

Data ContextEntry |
Typeable ContextEntry |
PrettyTCM Context |

newtype CtxId

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, Arg Type))

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

Instances

Data AbstractMode |
Typeable AbstractMode |

# Type checking errors

data Occ

Constructors

OccCon |

Fields

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

OccClause |

Fields

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

data OccPos

Constructors

NonPositively |
ArgumentTo Nat QName |

data TypeError

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

Instances

Show TypeError |
Typeable TypeError |
Error TypeError |
PrettyTCM TypeError |

data TCErr'

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

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'

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

Constructors

TCM |

Fields

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

Instances

MonadTrans TCMT |
MonadError TCErr IM |
MonadIO m => MonadState TCState (TCMT m) |
MonadIO m => MonadReader TCEnv (TCMT m) |
MonadError TCErr (TCMT IO) |
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

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

Methods

liftTCM :: TCM a -> tcm a

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

Running the type checking monad

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