Safe Haskell	None
Language	Haskell98

Idris.Core.TT

Description

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.

Synopsis

Documentation

data AppStatus n Source

Constructors

Complete
MaybeHoles
Holes [n]

Instances

Functor AppStatus Source
Eq n => Eq (AppStatus n) Source
Data n => Data (AppStatus n) Source
Ord n => Ord (AppStatus n) Source
Show n => Show (AppStatus n) Source

data ArithTy Source

Constructors

ATInt IntTy
ATFloat

Instances

Eq ArithTy Source
Data ArithTy Source
Ord ArithTy Source
Show ArithTy Source

data Binder b Source

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 Source
Foldable Binder Source
Traversable Binder Source
Eq b => Eq (Binder b) Source
Data b => Data (Binder b) Source
Ord b => Ord (Binder b) Source
Show b => Show (Binder b) Source

data Const Source

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 Source
Data Const Source
Ord Const Source
Show Const Source

type Ctxt a = Map Name (Map Name a) Source

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 Source

Constructors

ConstraintFC
Fields uconstraint :: UConstraint ufc :: FC

Instances

Eq ConstraintFC Source
Data ConstraintFC Source
Ord ConstraintFC Source
Show ConstraintFC Source

data DataOpt Source

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 Source
Show DataOpt Source

type DataOpts = [DataOpt] Source

data Datatype n Source

Constructors

Data
Fields d_typename :: n d_typetag :: Int d_type :: TT n d_unique :: Bool d_cons :: [(n, TT n)]

Instances

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

type Env = EnvTT Name Source

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

type Err = Err' Term Source

data Err' t Source

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' Source
Show Err Source
Eq t => Eq (Err' t) Source
Data t => Data (Err' t) Source

data ErrorReportPart Source

Used for error reflection

Constructors

TextPart String
NamePart Name
TermPart Term
RawPart Raw
SubReport [ErrorReportPart]

Instances

Eq ErrorReportPart Source
Data ErrorReportPart Source
Show ErrorReportPart Source

data FC Source

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 Source	Ignore source location equality (so deriving classes do not compare FCs)
Data FC Source
Ord FC Source
Show FC Source
SExpable FC Source

newtype FC' Source

FC with equality

Constructors

FC'
Fields unwrapFC :: FC

Instances

Eq FC' Source
Data FC' Source
Ord FC' Source
Show FC' Source

data ImplicitInfo Source

Constructors

Impl
Fields tcinstance :: Bool toplevel_imp :: Bool

Instances

Eq ImplicitInfo Source
Data ImplicitInfo Source
Ord ImplicitInfo Source
Show ImplicitInfo Source

data IntTy Source

Constructors

ITFixed NativeTy
ITNative
ITBig
ITChar

Instances

Eq IntTy Source
Data IntTy Source
Ord IntTy Source
Show IntTy Source

data Name Source

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 Source
Data Name Source
Ord Name Source
Show Name Source
Show Err Source
TermSize CaseAlt Source
TermSize SC Source
SExpable Name Source
TermSize (TT Name) Source

data NameOutput Source

Output annotation for pretty-printed name - decides colour

Constructors

TypeOutput
FunOutput
DataOutput
MetavarOutput
PostulateOutput

Instances

Eq NameOutput Source
Show NameOutput Source
SExpable NameOutput Source

data NameType Source

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 Source
Data NameType Source
Ord NameType Source
Show NameType Source

data NativeTy Source

Constructors

IT8
IT16
IT32
IT64

Instances

Enum NativeTy Source
Eq NativeTy Source
Data NativeTy Source
Ord NativeTy Source
Show NativeTy Source

data OutputAnnotation Source

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 Source
Show OutputAnnotation Source
SExpable OutputAnnotation Source

data Provenance Source

Constructors

ExpectedType
TooManyArgs Term
InferredVal
GivenVal
SourceTerm Term

Instances

Eq Provenance Source
Data Provenance Source
Show Provenance Source

data Raw Source

Constructors

Var Name
RBind Name (Binder Raw) Raw
RApp Raw Raw
RType
RUType Universe
RConstant Const

Instances

Eq Raw Source
Data Raw Source
Show Raw Source

data SpecialName Source

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 Source
Data SpecialName Source
Ord SpecialName Source
Show SpecialName Source

data TC a Source

Constructors

OK !a
Error Err

Instances

Monad TC Source
Functor TC Source
Applicative TC Source
Alternative TC Source
MonadPlus TC Source
Eq a => Eq (TC a) Source
Show a => Show (TC a) Source

type Term = TT Name Source

class TermSize a where Source

Methods

termsize :: Name -> a -> Int Source

Instances

TermSize CaseAlt Source
TermSize SC Source
TermSize a => TermSize [a] Source
TermSize (TT Name) Source

data TextFormatting Source

Text formatting output

Constructors

BoldText
ItalicText
UnderlineText

Instances

Eq TextFormatting Source
Show TextFormatting Source

data TT n Source

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 Source
Show Err Source
TermSize CaseAlt Source
TermSize SC Source
Eq n => Eq (TT n) Source
Data n => Data (TT n) Source
Ord n => Ord (TT n) Source
(Eq n, Show n) => Show (TT n) Source
TermSize (TT Name) Source

type Type = Term Source

data TypeInfo Source

Constructors

TI
Fields con_names :: [Name] codata :: Bool data_opts :: DataOpts param_pos :: [Int] mutual_types :: [Name]

Instances

Show TypeInfo Source

data UConstraint Source

Universe constraints

Constructors

ULT UExp UExp	Strictly less than
ULE UExp UExp	Less than or equal to

Instances

Eq UConstraint Source
Data UConstraint Source
Ord UConstraint Source
Show UConstraint Source

type UCs = (Int, [UConstraint]) Source

data UExp Source

Universe expressions for universe checking

Constructors

UVar Int	universe variable
UVal Int	explicit universe level

Instances

Eq UExp Source
Data UExp Source
Ord UExp Source
Show UExp Source

data Universe Source

Constructors

NullType
UniqueType
AllTypes

Instances

Eq Universe Source
Data Universe Source
Ord Universe Source
Show Universe Source

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

addBinder :: TT n -> TT n Source

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

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

arity :: TT n -> Int Source

Return the arity of a (normalised) type

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

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

bindingOf Source

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 Source

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.

constDocs :: Const -> String Source

Get the docstring for a Const

constIsType :: Const -> Bool Source

Determines whether the input constant represents a type

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

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

emptyContext :: Map k a Source

emptyFC :: FC Source

Empty source location

explicitNames :: TT n -> TT n Source

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

fc_end :: FC -> (Int, Int) Source

Give a notion of end location associated with an FC

fc_fname :: FC -> String Source

Give a notion of filename associated with an FC

fc_start :: FC -> (Int, Int) Source

Give a notion of start location associated with an FC

fcIn :: FC -> FC -> Bool Source

Determine whether the first argument is completely contained in the second

fileFC :: String -> FC Source

Source location with file only

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

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

forget :: TT Name -> Raw Source

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 Source

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

Returns all names used free in the term

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

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 Source

implicitable :: Name -> Bool Source

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

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

intTyName :: IntTy -> String Source

isInjective :: TT n -> Bool Source

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 Source

liftPats :: Term -> Term Source

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

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

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

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 Source

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

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

nativeTyWidth :: NativeTy -> Int Source

nextName :: Name -> Name Source

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

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

nsroot :: Name -> Name Source

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

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

orderPats :: Term -> Term Source

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

pEraseType :: TT n -> TT n Source

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

pprintRaw Source

Arguments

:: [Name]	Bound names, for highlighting
-> Raw	The term to pretty-print
-> Doc OutputAnnotation

Pretty-print a raw term.

pprintTT Source

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 Source

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

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

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

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

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

pureTerm :: TT Name -> Bool Source

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

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

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

refsIn :: TT Name -> [Name] Source

safeForget :: TT Name -> Maybe Raw Source

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

showCG :: Name -> String Source

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

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

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

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

sMN :: Int -> String -> Name Source

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

spanFC :: FC -> FC -> FC Source

Get the largest span containing the two FCs

str :: Text -> String Source

subst Source

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 Source

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

substTerm Source

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 Source

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 Source

tcname :: Name -> Bool Source

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

termSmallerThan :: Int -> Term -> Bool Source

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

tfail :: Err -> TC a Source

thead :: Text -> Char Source

tnull :: Text -> Bool Source

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

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

txt :: String -> Text Source

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

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

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

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

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

uniqueNameSet :: Name -> Set Name -> Name Source

unList :: Term -> Maybe [Term] Source

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

vToP :: TT n -> TT n Source

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 Source

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