idris-0.9.15.1: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.TT

Contents

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

Instances

Eq FC

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

Show FC 
Binary FC 
NFData FC 
SExpable FC 

newtype FC' Source

FC with equality

Constructors

FC' 

Fields

unwrapFC :: FC
 

Instances

Eq FC' 

emptyFC :: FCSource

Empty source location

fileFC :: String -> FCSource

data NameOutput Source

Output annotation for pretty-printed name - decides colour

Instances

data TextFormatting Source

Text formatting output

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 
AnnTerm [(Name, Bool)] (TT Name)

pprint bound vars, original term

AnnSearchResult Ordering

more general, isomorphic, or more specific

AnnErr Err 

data Err' t Source

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

Instances

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

score :: Err -> IntSource

failMsg :: String -> TC aSource

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

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

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

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 something which is never used in scope

SN SpecialName

Decorated function names

SymRef Int

Reference to IBC file symbol table (used during serialisation)

txt :: String -> TextSource

str :: Text -> StringSource

tnull :: Text -> BoolSource

thead :: Text -> CharSource

sUN :: String -> NameSource

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

sMN :: Int -> String -> NameSource

showCG :: Name -> StringSource

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.

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

tcname :: Name -> BoolSource

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

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

data IntTy Source

Instances

Eq IntTy 
Ord IntTy 
Show IntTy 
NFData IntTy 

intTyName :: IntTy -> StringSource

data ArithTy Source

Constructors

ATInt IntTy 
ATFloat 

Instances

intTyWidth :: IntTy -> IntSource

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 
ManagedPtrType 
BufferType 
VoidType 
Forgot 

Instances

constIsType :: Const -> BoolSource

Determines whether the input constant represents a type

constDocs :: Const -> StringSource

Get the docstring for a Const

data Universe Source

Constructors

NullType 
UniqueType 
AllTypes 

Instances

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

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 

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 
Foldable Binder 
Traversable 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) 
Apropos (Binder (TT Name)) 

fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)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

type UCs = (Int, [UConstraint])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
 

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

UType Universe

Uniqueness type universe (disjoint from TType)

Instances

Functor TT 
Show Err 
Binary CaseAlt 
Binary SC 
Error Err 
NFData Err 
TermSize CaseAlt 
TermSize 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)) 
Apropos (TT Name) 
Apropos (Binder (TT Name)) 

class TermSize a whereSource

Methods

termsize :: Name -> a -> IntSource

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_unique :: Bool
 
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 -> BoolSource

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

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

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.

substSource

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

substTermSource

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.

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

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

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

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

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

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

newtype WkEnvTT n Source

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

Constructors

Wk (EnvTT n) 

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

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

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

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

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