Idris.Core.TT

TT is the core language of Idris. The language has:

• Full dependent types
• A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
• Pattern matching letrec binding
• (primitive types defined externally)

Some technical stuff:

• Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
• We have a simple collection of tactics which we use to elaborate source programs with implicit syntax into fully explicit terms.

Documentation

data AppStatus n

Constructors

Complete

MaybeHoles

Holes [n]

Instances

Functor AppStatus

Eq n => Eq (AppStatus n)

Data n => Data (AppStatus n)

Ord n => Ord (AppStatus n)

Show n => Show (AppStatus n)

data ArithTy

Constructors

ATInt IntTy

ATFloat

Instances

Eq ArithTy

Data ArithTy

Ord ArithTy

Show ArithTy

data Binder b

All binding forms are represented in a uniform fashion. This type only represents the types of bindings (and their values, if any); the attached identifiers are part of the Bind constructor for the TT type.

Constructors

Lam

A function binding

Fields

binderTy :: !b

type annotation for bound variable

Pi

A binding that occurs in a function type expression, e.g. (x:Int) -> ... The binderImpl flag says whether it was a scoped implicit (i.e. forall bound) in the high level Idris, but otherwise has no relevance in TT.

Fields

binderImpl :: Maybe ImplicitInfo

binderTy :: !b

type annotation for bound variable

binderKind :: !b

Let

A binding that occurs in a let expression

Fields

binderTy :: !b

type annotation for bound variable

binderVal :: b

value for bound variable

NLet

NLet is an intermediate product in the evaluator that's used for temporarily naming locals during reduction. It won't occur outside the evaluator.

Fields

binderTy :: !b

type annotation for bound variable

binderVal :: b

value for bound variable

Hole

A hole in a term under construction in the elaborator. If this is not filled during elaboration, it is an error.

Fields

binderTy :: !b

type annotation for bound variable

GHole

A saved TT hole that will later be converted to a top-level Idris metavariable applied to all elements of its local environment.

Fields

envlen :: Int

localnames :: [Name]

binderTy :: !b

type annotation for bound variable

Guess

A provided value for a hole. It will later be substituted - the guess is to keep it computationally inert while working on other things if necessary.

Fields

binderTy :: !b

type annotation for bound variable

binderVal :: b

value for bound variable

PVar

A pattern variable (these are bound around terms that make up pattern-match clauses)

Fields

binderTy :: !b

type annotation for bound variable

PVTy

The type of a pattern binding

Fields

binderTy :: !b

type annotation for bound variable

Instances

Functor Binder

Foldable Binder

Traversable Binder

Eq b => Eq (Binder b)

Data b => Data (Binder b)

Ord b => Ord (Binder b)

Show b => Show (Binder b)

data Const

Constructors

I Int

BI Integer

Fl Double

Ch Char

Str String

B8 Word8

B16 Word16

B32 Word32

B64 Word64

AType ArithTy

StrType

WorldType

TheWorld

VoidType

Forgot

Instances

Eq Const

Data Const

Ord Const

Show Const

type Ctxt a = Map Name (Map Name a)

Contexts allow us to map names to things. A root name maps to a collection of things in different namespaces with that name.

data ConstraintFC

Constructors

ConstraintFC

Fields

uconstraint :: UConstraint

ufc :: FC

Instances

Eq ConstraintFC

Data ConstraintFC

Ord ConstraintFC

Show ConstraintFC

data DataOpt

Data declaration options

Constructors

Codata

Set if the the data-type is coinductive

DefaultEliminator

Set if an eliminator should be generated for data type

DefaultCaseFun

Set if a case function should be generated for data type

DataErrRev

Instances

Eq DataOpt

Show DataOpt

type DataOpts = [DataOpt]

data Datatype n

Constructors

Data

Fields

d_typename :: n

d_typetag :: Int

d_type :: TT n

d_unique :: Bool

d_cons :: [(n, TT n)]

Instances

Functor Datatype

Eq n => Eq (Datatype n)

(Eq n, Show n) => Show (Datatype n)

type Env = EnvTT Name

type EnvTT n = [(n, Binder (TT n))]

type Err = Err' Term

data Err' t

Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.

Constructors

Msg String

InternalMsg String

CantUnify Bool (t, Maybe Provenance) (t, Maybe Provenance) (Err' t) [(Name, t)] Int

InfiniteUnify Name t [(Name, t)]

CantConvert t t [(Name, t)]

CantSolveGoal t [(Name, t)]

UnifyScope Name Name t [(Name, t)]

CantInferType String

NonFunctionType t t

NotEquality t t

TooManyArguments Name

CantIntroduce t

NoSuchVariable Name

WithFnType t

NoTypeDecl Name

NotInjective t t t

CantResolve Bool t (Err' t)

InvalidTCArg Name t

CantResolveAlts [Name]

NoValidAlts [Name]

IncompleteTerm t

NoEliminator String t

UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

Location, bad universe, old domain, new domain, suspects

UniqueError Universe Name

UniqueKindError Universe Name

ProgramLineComment

Inaccessible Name

UnknownImplicit Name Name

CantMatch t

NonCollapsiblePostulate Name

AlreadyDefined Name

ProofSearchFail (Err' t)

NoRewriting t

At FC (Err' t)

Elaborating String Name (Maybe t) (Err' t)

ElaboratingArg Name Name [(Name, Name)] (Err' t)

ProviderError String

LoadingFailed String (Err' t)

ReflectionError [[ErrorReportPart]] (Err' t)

ReflectionFailed String (Err' t)

ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]

User-specified message, proof term, goals with context (first goal is focused)

ElabScriptStuck t

RunningElabScript (Err' t)

The error occurred during a top-level elaboration script

ElabScriptStaging Name

FancyMsg [ErrorReportPart]

Instances

Functor Err'

Show Err

Eq t => Eq (Err' t)

Data t => Data (Err' t)

data ErrorReportPart

Used for error reflection

Constructors

TextPart String

NamePart Name

TermPart Term

RawPart Raw

SubReport [ErrorReportPart]

Instances

Eq ErrorReportPart

Data ErrorReportPart

Show ErrorReportPart

data FC

Source location. These are typically produced by the parser getFC

Constructors

FC

Fields

_fc_fname :: String

Filename

_fc_start :: (Int, Int)

Line and column numbers for the start of the location span

_fc_end :: (Int, Int)

Line and column numbers for the end of the location span

NoFC

Locations for machine-generated terms

FileFC

Locations with file only

Fields

_fc_fname :: String

Filename

Instances

Eq FC

Ignore source location equality (so deriving classes do not compare FCs)

Data FC

Ord FC

Show FC

SExpable FC

newtype FC'

FC with equality

Constructors

FC'

Fields

unwrapFC :: FC

Instances

Eq FC'

Data FC'

Ord FC'

Show FC'

data ImplicitInfo

Constructors

Impl

Fields

tcinstance :: Bool

toplevel_imp :: Bool

Instances

Eq ImplicitInfo

Data ImplicitInfo

Ord ImplicitInfo

Show ImplicitInfo

data IntTy

Constructors

ITFixed NativeTy

ITNative

ITBig

ITChar

Instances

Eq IntTy

Data IntTy

Ord IntTy

Show IntTy

data Name

Names are hierarchies of strings, describing scope (so no danger of duplicate names, but need to be careful on lookup).

Constructors

UN !Text

User-provided name

NS !Name [Text]

Root, namespaces

MN !Int !Text

Machine chosen names

SN !SpecialName

Decorated function names

SymRef Int

Reference to IBC file symbol table (used during serialisation)

Instances

Eq Name

Data Name

Ord Name

Show Name

Show Err

TermSize CaseAlt

TermSize SC

SExpable Name

TermSize (TT Name)

data NameOutput

Output annotation for pretty-printed name - decides colour

Constructors

TypeOutput

FunOutput

DataOutput

MetavarOutput

PostulateOutput

Instances

Eq NameOutput

Show NameOutput

SExpable NameOutput

data NameType

Constructors

Bound

Ref

DCon

Data constructor

Fields

nt_tag :: Int

nt_arity :: Int

nt_unique :: Bool

TCon

Type constructor

Fields

nt_tag :: Int

nt_arity :: Int

Instances

Eq NameType

Data NameType

Ord NameType

Show NameType

data NativeTy

Constructors

IT8

IT16

IT32

IT64

Instances

Enum NativeTy

Eq NativeTy

Data NativeTy

Ord NativeTy

Show NativeTy

data OutputAnnotation

Output annotations for pretty-printing

Constructors

AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

^ The name, classification, docs overview, and pretty-printed type

AnnBoundName Name Bool

^ The name and whether it is implicit

AnnConst Const

AnnData String String

type, doc overview

AnnType String String

name, doc overview

AnnKeyword

AnnFC FC

AnnTextFmt TextFormatting

AnnLink String

A link to this URL

AnnTerm [(Name, Bool)] (TT Name)

pprint bound vars, original term

AnnSearchResult Ordering

more general, isomorphic, or more specific

AnnErr Err

AnnNamespace [Text] (Maybe FilePath)

A namespace (e.g. on an import line or in a namespace declaration). Stored starting at the root, with the hierarchy fully resolved. If a file path is present, then the namespace represents a module imported from that file.

AnnQuasiquote

AnnAntiquote

Instances

Eq OutputAnnotation

Show OutputAnnotation

SExpable OutputAnnotation

data Provenance

Constructors

ExpectedType

TooManyArgs Term

InferredVal

GivenVal

SourceTerm Term

Instances

Eq Provenance

Data Provenance

Show Provenance

data Raw

Constructors

Var Name

RBind Name (Binder Raw) Raw

RApp Raw Raw

RType

RUType Universe

RConstant Const

Instances

Eq Raw

Data Raw

Show Raw

data SpecialName

Constructors

WhereN !Int !Name !Name

WithN !Int !Name

InstanceN !Name [Text]

ParentN !Name !Text

MethodN !Name

CaseN !FC' !Name

ElimN !Name

InstanceCtorN !Name

MetaN !Name !Name

Instances

Eq SpecialName

Data SpecialName

Ord SpecialName

Show SpecialName

data TC a

Constructors

OK !a

Error Err

Instances

Monad TC

Functor TC

Applicative TC

Alternative TC

MonadPlus TC

Eq a => Eq (TC a)

Show a => Show (TC a)

type Term = TT Name

class TermSize a where

Methods

termsize :: Name -> a -> Int

Instances

TermSize CaseAlt

TermSize SC

TermSize a => TermSize [a]

TermSize (TT Name)

data TextFormatting

Text formatting output

Constructors

BoldText

ItalicText

UnderlineText

Instances

Eq TextFormatting

Show TextFormatting

data TT n

Terms in the core language. The type parameter is the type of identifiers used for bindings and explicit named references; usually we use TT Name.

Constructors

P NameType n (TT n)

named references with type (P for Parameter, motivated by McKinna and Pollack's Pure Type Systems Formalized)

V !Int

a resolved de Bruijn-indexed variable

Bind n !(Binder (TT n)) (TT n)

a binding

App (AppStatus n) !(TT n) (TT n)

function, function type, arg

Constant Const

constant

Proj (TT n) !Int

argument projection; runtime only (-1) is a special case for 'subtract one from BI'

Erased

an erased term

Impossible

special case for totality checking

TType UExp

the type of types at some level

UType Universe

Uniqueness type universe (disjoint from TType)

Instances

Functor TT

Show Err

TermSize CaseAlt

TermSize SC

Eq n => Eq (TT n)

Data n => Data (TT n)

Ord n => Ord (TT n)

(Eq n, Show n) => Show (TT n)

TermSize (TT Name)

type Type = Term

data TypeInfo

Constructors

TI

Fields

con_names :: [Name]

codata :: Bool

data_opts :: DataOpts

param_pos :: [Int]

mutual_types :: [Name]

Instances

Show TypeInfo

data UConstraint

Universe constraints

Constructors

ULT UExp UExp

Strictly less than

ULE UExp UExp

Less than or equal to

Instances

Eq UConstraint

Data UConstraint

Ord UConstraint

Show UConstraint

type UCs = (Int, [UConstraint])

data UExp

Universe expressions for universe checking

Constructors

UVar Int

universe variable

UVal Int

explicit universe level

Instances

Eq UExp

Data UExp

Ord UExp

Show UExp

data Universe

Constructors

NullType

UniqueType

AllTypes

Instances

Eq Universe

Data Universe

Ord Universe

Show Universe

addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

addBinder :: TT n -> TT n

addDef :: Name -> a -> Ctxt a -> Ctxt a

allTTNames :: Eq n => TT n -> [n]

arity :: TT n -> Int

Return the arity of a (normalised) type

bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

Introduce a Bind into the given term for each element of the given list of (name, binder) pairs.

bindingOf

Arguments

:: Name

^ the bound name

-> Bool

^ whether the name is implicit

-> Doc OutputAnnotation

Pretty-printer helper for the binding site of a name

bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n

Like bindAll, but the Binders are TT terms instead. The first argument is a function to map TT terms to Binders. This function might often be something like Lam, which directly constructs a Binder from a TT term.

caseName :: Name -> Bool

constDocs :: Const -> String

Get the docstring for a Const

constIsType :: Const -> Bool

Determines whether the input constant represents a type

deleteDefExact :: Name -> Ctxt a -> Ctxt a

discard :: Monad m => m a -> m ()

emptyContext :: Map k a

emptyFC :: FC

Empty source location

explicitNames :: TT n -> TT n

Replace all non-free de Bruijn references in the given term with references to the name of their binding.

fc_end :: FC -> (Int, Int)

Give a notion of end location associated with an FC

fc_fname :: FC -> String

Give a notion of filename associated with an FC

fc_start :: FC -> (Int, Int)

Give a notion of start location associated with an FC

fcIn :: FC -> FC -> Bool

Determine whether the first argument is completely contained in the second

fileFC :: String -> FC

Source location with file only

finalise :: Eq n => TT n -> TT n

Replace every non-free reference to the name of a binding in the given term with a de Bruijn index.

fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

forget :: TT Name -> Raw

Cast a TT term to a Raw value, discarding universe information and the types of named references and replacing all de Bruijn indices with the corresponding name. It is an error if there are free de Bruijn indices.

forgetEnv :: [Name] -> TT Name -> Raw

freeNames :: Eq n => TT n -> [n]

Returns all names used free in the term

getArgTys :: TT n -> [(n, TT n)]

Return a list of pairs of the names of the outermost Pi-bound variables in the given term, together with their types.

getRetTy :: TT n -> TT n

implicitable :: Name -> Bool

instantiate :: TT n -> TT n -> TT n

Replace the outermost (index 0) de Bruijn variable with the given term

intTyName :: IntTy -> String

isInjective :: TT n -> Bool

A term is injective iff it is a data constructor, type constructor, constant, the type Type, pi-binding, or an application of an injective term.

isTypeConst :: Const -> Bool

liftPats :: Term -> Term

lookupCtxt :: Name -> Ctxt a -> [a]

lookupCtxtExact :: Name -> Ctxt a -> Maybe a

lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]

Look up a name in the context, given an optional namespace. The name (n) may itself have a (partial) namespace given.

Rules for resolution:

• if an explicit namespace is given, return the names which match it. If none match, return all names.
• if the name has has explicit namespace given, return the names which match it and ignore the given namespace.
• otherwise, return all names.

mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

mkApp :: TT n -> [TT n] -> TT n

Returns a term representing the application of the first argument (a function) to every element of the second argument.

nativeTyWidth :: NativeTy -> Int

nextName :: Name -> Name

noOccurrence :: Eq n => n -> TT n -> Bool

Returns true if V 0 and bound name n do not occur in the term

nsroot :: Name -> Name

occurrences :: Eq n => n -> TT n -> Int

Return number of occurrences of V 0 or bound name i the term

orderPats :: Term -> Term

Gather up all the outer PVars and Holes in an expression and reintroduce them in a canonical order

pEraseType :: TT n -> TT n

pmap :: (t -> t1) -> (t, t) -> (t1, t1)

pprintRaw

Arguments

:: [Name]

Bound names, for highlighting

-> Raw

The term to pretty-print

-> Doc OutputAnnotation

Pretty-print a raw term.

pprintTT

Arguments

:: [Name]

The bound names (for highlighting and de Bruijn indices)

-> TT Name

The term to be printed

-> Doc OutputAnnotation

Pretty-print a term

prettyEnv :: Env -> Term -> Doc OutputAnnotation

psubst :: Eq n => n -> TT n -> TT n -> TT n

pToV :: Eq n => n -> TT n -> TT n

Replace references to the given Name-like id with references to de Bruijn index 0.

pToVs :: Eq n => [n] -> TT n -> TT n

Convert several names. First in the list comes out as V 0

pureTerm :: TT Name -> Bool

Check whether a term has any hole bindings in it - impure if so

raw_apply :: Raw -> [Raw] -> Raw

raw_unapply :: Raw -> (Raw, [Raw])

refsIn :: TT Name -> [Name]

safeForget :: TT Name -> Maybe Raw

safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

showCG :: Name -> String

showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String

showEnvDbg :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> [Char]

showSep :: String -> [String] -> String

sInstanceN :: Name -> [String] -> SpecialName

sMN :: Int -> String -> Name

sNS :: Name -> [String] -> Name

spanFC :: FC -> FC -> FC

Get the largest span containing the two FCs

str :: Text -> String

subst

Arguments

:: Eq n

=> n

The id to replace

-> TT n

The replacement term

-> TT n

The term to replace in

-> TT n

As instantiate, but in addition to replacing V 0, replace references to the given Name-like id.

substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

As subst, but takes a list of (name, substitution) pairs instead of a single name and substitution

substTerm

Arguments

:: Eq n

=> TT n

Old term

-> TT n

New term

-> TT n

template term

-> TT n

Replaces all terms equal (in the sense of (==)) to the old term with the new term.

substV :: TT n -> TT n -> TT n

As instantiate, but also decrement the indices of all de Bruijn variables remaining in the term, so that there are no more references to the variable that has been substituted.

sUN :: String -> Name

tcname :: Name -> Bool

Return True if the argument Name should be interpreted as the name of a typeclass.

termSmallerThan :: Int -> Term -> Bool

Hard-code a heuristic maximum term size, to prevent attempts to serialize or force infinite or just gigantic terms

tfail :: Err -> TC a

thead :: Text -> Char

tnull :: Text -> Bool

toAlist :: Ctxt a -> [(Name, a)]

traceWhen :: Bool -> String -> a -> a

txt :: String -> Text

unApply :: TT n -> (TT n, [TT n])

Deconstruct an application; returns the function and a list of arguments

uniqueBinders :: [Name] -> TT Name -> TT Name

uniqueName :: Name -> [Name] -> Name

uniqueNameFrom :: [Name] -> [Name] -> Name

uniqueNameSet :: Name -> Set Name -> Name

unList :: Term -> Maybe [Term]

updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

vToP :: TT n -> TT n

Replace de Bruijn indices in the given term with explicit references to the names of the bindings they refer to. It is an error if the given term contains free de Bruijn indices.

weakenTm :: Int -> TT n -> TT n

Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)