Safe Haskell | None |
---|---|
Language | Haskell98 |
- data OutputTypeName
- getOutputTypeName :: Type -> TCM OutputTypeName
- renameP :: Subst t => Permutation -> t -> t
- renaming :: Permutation -> Substitution
- renamingR :: Permutation -> Substitution
- flattenTel :: Telescope -> [Dom Type]
- reorderTel :: [Dom Type] -> Maybe Permutation
- reorderTel_ :: [Dom Type] -> Permutation
- unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
- teleNames :: Telescope -> [ArgName]
- teleArgNames :: Telescope -> [Arg ArgName]
- teleArgs :: Telescope -> Args
- data SplitTel = SplitTel {}
- splitTelescope :: VarSet -> Telescope -> SplitTel
- telView :: Type -> TCM TelView
- telViewUpTo :: Int -> Type -> TCM TelView
- telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView
- piApplyM :: Type -> Args -> TCM Type
- addTypedInstance :: QName -> Type -> TCM ()
- resolveUnknownInstanceDefs :: TCM ()
- getInstanceDefs :: TCM InstanceTable
Documentation
getOutputTypeName :: Type -> TCM OutputTypeName Source
Strips all Pi's and return the head definition name, if possible.
renameP :: Subst t => Permutation -> t -> t Source
The permutation should permute the corresponding telescope. (left-to-right list)
renaming :: Permutation -> Substitution Source
If permute π : [a]Γ -> [a]Δ
, then applySubst (renaming π) : Term Γ -> Term Δ
renamingR :: Permutation -> Substitution Source
If permute π : [a]Γ -> [a]Δ
, then substs (renamingR π) : Term Δ -> Term Γ
flattenTel :: Telescope -> [Dom Type] Source
Flatten telescope: (Γ : Tel) -> [Type Γ]
reorderTel :: [Dom Type] -> Maybe Permutation Source
Order a flattened telescope in the correct dependeny order: Γ -> Permutation (Γ -> Γ~)
Since reorderTel tel
uses free variable analysis of type in tel
,
the telescope should be normalise
d.
reorderTel_ :: [Dom Type] -> Permutation Source
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope Source
Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.
teleArgNames :: Telescope -> [Arg ArgName] Source
A telescope split in two.
SplitTel | |
|
:: VarSet | A set of de Bruijn indices. |
-> Telescope | Original telescope. |
-> SplitTel |
|
Split a telescope into the part that defines the given variables and the part that doesn't.
See prop_splitTelescope
.
telViewUpTo :: Int -> Type -> TCM TelView Source
telViewUpTo n t
takes off the first n
function types of t
.
Takes off all if n < 0
.
telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView Source
telViewUpTo' n p t
takes off $t$
the first n
(or arbitrary many if n < 0
) function domains
as long as they satify p
.
Instance definitions
addTypedInstance :: QName -> Type -> TCM () Source
getInstanceDefs :: TCM InstanceTable Source
Try to solve the instance definitions whose type is not yet known, report an error if it doesn't work and return the instance table otherwise.