Safe Haskell | None |
---|
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.
- data Option
- data FC = FC {}
- newtype FC' = FC' {}
- emptyFC :: FC
- fileFC :: String -> FC
- data NameOutput
- data TextFormatting
- = BoldText
- | ItalicText
- | UnderlineText
- data OutputAnnotation
- = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
- | AnnBoundName Name Bool
- | AnnConst Const
- | AnnData String String
- | AnnType String String
- | AnnKeyword
- | AnnFC FC
- | AnnTextFmt TextFormatting
- | AnnTerm [(Name, Bool)] (TT Name)
- | AnnSearchResult Ordering
- | AnnErr Err
- data ErrorReportPart
- data Err' t
- = 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 [Name]
- | IncompleteTerm t
- | UniverseError
- | UniqueError Universe Name
- | UniqueKindError Universe Name
- | ProgramLineComment
- | Inaccessible Name
- | NonCollapsiblePostulate Name
- | AlreadyDefined Name
- | ProofSearchFail (Err' t)
- | NoRewriting t
- | At FC (Err' t)
- | Elaborating String Name (Err' t)
- | ElaboratingArg Name Name [(Name, Name)] (Err' t)
- | ProviderError String
- | LoadingFailed String (Err' t)
- | ReflectionError [[ErrorReportPart]] (Err' t)
- | ReflectionFailed String (Err' t)
- type Err = Err' Term
- score :: Err -> Int
- type TC = TC' Err
- tfail :: Err -> TC a
- failMsg :: String -> TC a
- trun :: FC -> TC a -> TC a
- discard :: Monad m => m a -> m ()
- showSep :: String -> [String] -> String
- pmap :: (t -> t1) -> (t, t) -> (t1, t1)
- traceWhen :: Bool -> String -> a -> a
- data Name
- txt :: String -> Text
- str :: Text -> String
- tnull :: Text -> Bool
- thead :: Text -> Char
- sUN :: String -> Name
- sNS :: Name -> [String] -> Name
- sMN :: Int -> String -> Name
- data SpecialName
- sInstanceN :: Name -> [String] -> SpecialName
- sParentN :: Name -> String -> SpecialName
- showCG :: Name -> String
- type Ctxt a = Map Name (Map Name a)
- emptyContext :: Map k a
- mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
- tcname :: Name -> Bool
- implicitable :: Name -> Bool
- nsroot :: Name -> Name
- addDef :: Name -> a -> Ctxt a -> Ctxt a
- lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
- lookupCtxt :: Name -> Ctxt a -> [a]
- lookupCtxtExact :: Name -> Ctxt a -> Maybe a
- deleteDefExact :: Name -> Ctxt a -> Ctxt a
- updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
- toAlist :: Ctxt a -> [(Name, a)]
- addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a
- data NativeTy
- data IntTy
- intTyName :: IntTy -> String
- data ArithTy
- nativeTyWidth :: NativeTy -> Int
- intTyWidth :: IntTy -> Int
- data Const
- constIsType :: Const -> Bool
- constDocs :: Const -> String
- data Universe
- = NullType
- | UniqueType
- | AllTypes
- data Raw
- data Binder b
- fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
- raw_apply :: Raw -> [Raw] -> Raw
- raw_unapply :: Raw -> (Raw, [Raw])
- data UExp
- data UConstraint
- type UCs = (Int, [UConstraint])
- data NameType
- data TT n
- class TermSize a where
- type EnvTT n = [(n, Binder (TT n))]
- data Datatype n = Data {}
- isInjective :: TT n -> Bool
- vinstances :: Int -> TT n -> Int
- instantiate :: TT n -> TT n -> TT n
- substV :: TT n -> TT n -> TT n
- explicitNames :: TT n -> TT n
- pToV :: Eq n => n -> TT n -> TT n
- pToV' :: Eq n => n -> Int -> TT n -> TT n
- addBinder :: TT n -> TT n
- pToVs :: Eq n => [n] -> TT n -> TT n
- vToP :: TT n -> TT n
- finalise :: Eq n => TT n -> TT n
- pEraseType :: TT n -> TT n
- subst :: Eq n => n -> TT n -> TT n -> TT n
- psubst :: Eq n => n -> TT n -> TT n -> TT n
- substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
- substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
- occurrences :: Eq n => n -> TT n -> Int
- noOccurrence :: Eq n => n -> TT n -> Bool
- freeNames :: Eq n => TT n -> [n]
- arity :: TT n -> Int
- unApply :: TT n -> (TT n, [TT n])
- mkApp :: TT n -> [TT n] -> TT n
- unList :: Term -> Maybe [Term]
- forget :: TT Name -> Raw
- forgetEnv :: [Name] -> TT Name -> Raw
- bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
- bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
- getArgTys :: TT n -> [(n, TT n)]
- getRetTy :: TT n -> TT n
- uniqueNameFrom :: [Name] -> [Name] -> Name
- uniqueName :: Name -> [Name] -> Name
- uniqueNameSet :: Name -> Set Name -> Name
- uniqueBinders :: [Name] -> TT Name -> TT Name
- nextName :: Name -> Name
- type Term = TT Name
- type Type = Term
- type Env = EnvTT Name
- newtype WkEnvTT n = Wk (EnvTT n)
- type WkEnv = WkEnvTT Name
- itBitsName :: NativeTy -> [Char]
- showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
- showEnvDbg :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> [Char]
- prettyEnv :: (Eq a1, Show a1, Pretty a1 a, Pretty NameType a, Pretty Const a) => [(a1, Binder (TT a1))] -> TT a1 -> Doc a
- showEnv' :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> Bool -> [Char]
- pureTerm :: TT Name -> Bool
- weakenTm :: Int -> TT n -> TT n
- weakenEnv :: EnvTT n -> EnvTT n
- weakenTmEnv :: Int -> EnvTT n -> EnvTT n
- orderPats :: Term -> Term
- liftPats :: Term -> Term
- allTTNames :: Eq n => TT n -> [n]
- module Idris.Core.TC
Documentation
data NameOutput Source
Output annotation for pretty-printed name - decides colour
data OutputAnnotation Source
Output annotations for pretty-printing
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 ErrorReportPart Source
Used for error reflection
Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.
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 [Name] | |
IncompleteTerm t | |
UniverseError | |
UniqueError Universe Name | |
UniqueKindError Universe Name | |
ProgramLineComment | |
Inaccessible Name | |
NonCollapsiblePostulate Name | |
AlreadyDefined Name | |
ProofSearchFail (Err' t) | |
NoRewriting t | |
At FC (Err' t) | |
Elaborating String Name (Err' t) | |
ElaboratingArg Name Name [(Name, Name)] (Err' t) | |
ProviderError String | |
LoadingFailed String (Err' t) | |
ReflectionError [[ErrorReportPart]] (Err' t) | |
ReflectionFailed String (Err' t) |
Names are hierarchies of strings, describing scope (so no danger of duplicate names, but need to be careful on lookup).
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) |
Eq Name | |
Ord Name | |
Show Name | |
Show Err | |
Binary Name | |
Binary CaseAlt | |
Binary SC | |
Error Err | |
NFData Name | |
NFData Err | |
TermSize CaseAlt | |
TermSize SC | |
SExpable Name | |
Apropos Name | |
Show a => Show (TC a) | |
Binary (TT Name) | |
TermSize (TT Name) | |
Optimisable (TT Name) | |
Optimisable (Binder (TT Name)) | |
Apropos (TT Name) | |
Apropos (Binder (TT Name)) |
data SpecialName Source
WhereN Int Name Name | |
WithN Int Name | |
InstanceN Name [Text] | |
ParentN Name Text | |
MethodN Name | |
CaseN Name | |
ElimN Name | |
InstanceCtorN Name |
Eq SpecialName | |
Ord SpecialName | |
Show SpecialName | |
Binary SpecialName | |
NFData SpecialName |
sInstanceN :: Name -> [String] -> SpecialNameSource
sParentN :: Name -> String -> SpecialNameSource
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
Return True if the argument Name
should be interpreted as the name of a
typeclass.
implicitable :: Name -> BoolSource
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
deleteDefExact :: Name -> Ctxt a -> Ctxt aSource
nativeTyWidth :: NativeTy -> IntSource
intTyWidth :: IntTy -> IntSource
Deprecated: Non-total function, use nativeTyWidth and appropriate casing
constIsType :: Const -> BoolSource
Determines whether the input constant represents a type
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.
Lam | |
| |
Pi | A binding that occurs in a function type expression, e.g. |
| |
Let | A binding that occurs in a |
NLet | |
Hole | |
| |
GHole | |
Guess | |
PVar | A pattern variable |
| |
PVTy | |
|
raw_unapply :: Raw -> (Raw, [Raw])Source
Universe expressions for universe checking
type UCs = (Int, [UConstraint])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
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) |
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)) |
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.
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
As instantiate
, but in addition to replacing
,
replace references to the given V
0Name
-like id.
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
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
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.
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.
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.
uniqueNameFrom :: [Name] -> [Name] -> NameSource
uniqueName :: Name -> [Name] -> NameSource
uniqueNameSet :: Name -> Set Name -> NameSource
an environment with de Bruijn indices normalised
so that they all refer to
this environment
itBitsName :: NativeTy -> [Char]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
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
allTTNames :: Eq n => TT n -> [n]Source
module Idris.Core.TC