idris-0.9.20.2: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

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] 

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

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

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

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

data Err' t Source

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

Instances

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
 

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)

data NameOutput Source

Output annotation for pretty-printed name - decides colour

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

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)

data TypeInfo Source

Constructors

TI 

Instances

data UConstraint Source

Universe constraints

Constructors

ULT UExp UExp

Strictly less than

ULE UExp UExp

Less than or equal to

data UExp Source

Universe expressions for universe checking

Constructors

UVar Int

universe variable

UVal Int

explicit universe level

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

discard :: Monad m => m a -> m () 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.

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

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

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

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.

lookupCtxt :: Name -> Ctxt a -> [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.

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

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

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

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

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

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

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

spanFC :: FC -> FC -> FC Source

Get the largest span containing the two FCs

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.

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

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

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

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

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

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)