Safe Haskell	None

Idris.Core.TT

Contents

A few handy operations on well typed terms:

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

Constructors

TTypeInTType
CheckConv

Instances

Eq Option

data FC Source

Source location. These are typically produced by the parser getFC

Constructors

FC
Fields fc_fname :: String Filename fc_line :: Int Line number fc_column :: Int Column number

Instances

Eq FC	Ignore source location equality (so deriving classes do not compare FCs)
Show FC
Binary FC
NFData FC

newtype FC' Source

FC with equality

Constructors

FC'
Fields unwrapFC :: FC

Instances

Eq FC'

emptyFC :: FC Source

Empty source location

fileFC :: String -> FC Source

Source location with file only

data NameOutput Source

Output annotation for pretty-printed name - decides colour

Constructors

TypeOutput
FunOutput
DataOutput

Instances

SExpable NameOutput

data OutputAnnotation Source

Output annotations for pretty-printing

Constructors

AnnName Name (Maybe NameOutput) (Maybe Type)
AnnBoundName Name Bool
AnnConstData
AnnConstType
AnnFC FC

Instances

SExpable OutputAnnotation
Show (Doc OutputAnnotation)

data ErrorReportPart Source

Used for error reflection

Constructors

TextPart String
NamePart Name
TermPart Term
SubReport [ErrorReportPart]

Instances

Eq ErrorReportPart
Show ErrorReportPart

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 t (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
NoTypeDecl Name
NotInjective t t t
CantResolve t
CantResolveAlts [String]
IncompleteTerm t
UniverseError
ProgramLineComment
Inaccessible Name
NonCollapsiblePostulate Name
AlreadyDefined Name
ProofSearchFail (Err' t)
NoRewriting t
At FC (Err' t)
Elaborating String Name (Err' t)
ProviderError String
LoadingFailed String (Err' t)
ReflectionError [[ErrorReportPart]] (Err' t)
ReflectionFailed String (Err' t)

Instances

Functor Err'
Show Err
NFData Err
Error Err
Eq t => Eq (Err' t)
Show a => Show (TC a)

type Err = Err' Term Source

score :: Err -> Int Source

type TC = TC' Err Source

tfail :: Err -> TC aSource

failMsg :: String -> TC aSource

trun :: FC -> TC a -> TC aSource

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

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

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

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

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
NErased	Name of somethng which is never used in scope
SN SpecialName	Decorated function names
SymRef Int	Reference to IBC file symbol table (used during serialisation)

Instances

Eq Name
Ord Name
Show Name
Show Err
Binary Name
Binary CaseAlt
Binary SC
NFData Name
NFData Err
Error Err
TermSize CaseAlt
TermSize SC
SExpable Name
ToIR SC
Transform CaseAlt
Transform SC
Show a => Show (TC a)
Binary (TT Name)
TermSize (TT Name)
Optimisable (TT Name)
Optimisable (Binder (TT Name))
ToIR (TT Name)
Transform (TT Name)
ToIR ([Name], SC)

txt :: String -> Text Source

str :: Text -> String Source

tnull :: Text -> Bool Source

thead :: Text -> Char Source

sUN :: String -> Name Source

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

sMN :: Int -> String -> Name Source

data SpecialName Source

Constructors

WhereN Int Name Name
InstanceN Name [Text]
ParentN Name Text
MethodN Name
CaseN Name
ElimN Name

Instances

Eq SpecialName
Ord SpecialName
Show SpecialName
Binary SpecialName
NFData SpecialName

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

sParentN :: Name -> String -> SpecialName Source

showCG :: Name -> String 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.

emptyContext :: Map k aSource

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

tcname :: Name -> Bool Source

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

implicitable :: Name -> Bool Source

nsroot :: Name -> Name Source

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

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.

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

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

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

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

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

data NativeTy Source

Constructors

IT8
IT16
IT32
IT64

Instances

Enum NativeTy
Eq NativeTy
Ord NativeTy
Show NativeTy
NFData NativeTy

data IntTy Source

Constructors

ITFixed NativeTy
ITNative
ITBig
ITChar
ITVec NativeTy Int

Instances

Eq IntTy
Ord IntTy
Show IntTy
NFData IntTy

intTyName :: IntTy -> String Source

data ArithTy Source

Constructors

ATInt IntTy
ATFloat

Instances

Eq ArithTy
Ord ArithTy
Show ArithTy
NFData ArithTy

nativeTyWidth :: NativeTy -> Int Source

intTyWidth :: IntTy -> Int Source

Deprecated: Non-total function, use nativeTyWidth and appropriate casing

data Const Source

Constructors

I Int
BI Integer
Fl Double
Ch Char
Str String
B8 Word8
B16 Word16
B32 Word32
B64 Word64
B8V (Vector Word8)
B16V (Vector Word16)
B32V (Vector Word32)
B64V (Vector Word64)
AType ArithTy
StrType
PtrType
BufferType
VoidType
Forgot

Instances

Eq Const
Ord Const
Show Const
Binary Const

data Raw Source

Constructors

Var Name
RBind Name (Binder Raw) Raw
RApp Raw Raw
RType
RForce Raw
RConstant Const

Instances

Eq Raw
Show Raw
Binary Raw
NFData Raw
Optimisable Raw
Optimisable (Binder Raw)

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
Fields binderTy :: !b type annotation for bound variable
Pi	A binding that occurs in a function type expression, e.g. `(x:Int) -> ...`
Fields binderTy :: !b type annotation for bound variable
Let	A binding that occurs in a `let` expression
Fields binderTy :: !b type annotation for bound variable binderVal :: b value for bound variable
NLet
Fields binderTy :: !b type annotation for bound variable binderVal :: b value for bound variable
Hole
Fields binderTy :: !b type annotation for bound variable
GHole
Fields envlen :: Int binderTy :: !b type annotation for bound variable
Guess
Fields binderTy :: !b type annotation for bound variable binderVal :: b value for bound variable
PVar	A pattern variable
Fields binderTy :: !b type annotation for bound variable
PVTy
Fields binderTy :: !b type annotation for bound variable

Instances

Functor Binder
Eq b => Eq (Binder b)
Ord b => Ord (Binder b)
Show b => Show (Binder b)
Binary b => Binary (Binder b)
NFData b => NFData (Binder b)
Optimisable (Binder (TT Name))
Optimisable (Binder Raw)
Transform a => Transform (Binder a)

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

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

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

data UExp Source

Universe expressions for universe checking

Constructors

UVar Int	universe variable
UVal Int	explicit universe level

Instances

Eq UExp
Ord UExp
Show UExp
Binary UExp
NFData UExp

data UConstraint Source

Universe constraints

Constructors

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

Instances

Eq UConstraint
Show UConstraint

type UCs = (Int, [UConstraint])Source

data NameType Source

Constructors

Bound
Ref
DCon	Data constructor
Fields nt_tag :: Int nt_arity :: Int
TCon	Type constructor
Fields nt_tag :: Int nt_arity :: Int

Instances

Eq NameType
Ord NameType
Show NameType
Binary NameType
NFData NameType

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 !(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

Instances

Functor TT
Show Err
Binary CaseAlt
Binary SC
NFData Err
Error Err
TermSize CaseAlt
TermSize SC
ToIR SC
Transform CaseAlt
Transform SC
Eq n => Eq (TT n)
Ord n => Ord (TT n)
(Eq n, Show n) => Show (TT n)
Show a => Show (TC a)
Binary (TT Name)
NFData n => NFData (TT n)
TermSize (TT Name)
Optimisable (TT Name)
Optimisable (Binder (TT Name))
ToIR (TT Name)
Transform (TT Name)
ToIR ([Name], SC)

class TermSize a whereSource

Methods

termsize :: Name -> a -> Int Source

Instances

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

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

data Datatype n Source

Constructors

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

Instances

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

A few handy operations on well typed terms:

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.

vinstances :: Int -> TT n -> Int Source

Count the number of instances of a de Bruijn index in a term

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

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

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

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.

explicitNames :: TT n -> TT nSource

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

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

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

pToV' :: Eq n => n -> Int -> TT n -> TT nSource

addBinder :: TT n -> TT nSource

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

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

vToP :: TT n -> TT nSource

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.

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

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

pEraseType :: TT n -> TT nSource

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.

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

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

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.

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

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

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

Returns all names used free in the term

arity :: TT n -> Int Source

Return the arity of a (normalised) type

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

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

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

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

unList :: Term -> Maybe [Term]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.

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

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

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

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.

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 nSource

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

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

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

nextName :: Name -> Name Source

type Term = TT Name Source

type Type = Term Source

type Env = EnvTT Name Source

newtype WkEnvTT n Source

an environment with de Bruijn indices normalised so that they all refer to this environment

Constructors

Wk (EnvTT n)

type WkEnv = WkEnvTT Name Source

itBitsName :: NativeTy -> [Char]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

prettyEnv :: (Eq a1, Show a1, Pretty a1 a, Pretty NameType a, Pretty Const a) => [(a1, Binder (TT a1))] -> TT a1 -> Doc aSource

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

pureTerm :: TT Name -> Bool Source

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

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

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

weakenEnv :: EnvTT n -> EnvTT nSource

Weaken an environment so that all the de Bruijn indices are correct according to the latest bound variable

weakenTmEnv :: Int -> EnvTT n -> EnvTT nSource

Weaken every term in the environment by the given amount

orderPats :: Term -> Term Source

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

module Idris.Core.TC