Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- 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 :: DeBruijn a => Telescope -> [Arg a]
- withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
- teleNamedArgs :: DeBruijn a => Telescope -> [NamedArg a]
- tele2NamedArgs :: DeBruijn a => Telescope -> Telescope -> [NamedArg a]
- splitTelescopeAt :: Int -> Telescope -> (Telescope, Telescope)
- permuteTel :: Permutation -> Telescope -> Telescope
- varDependencies :: Telescope -> IntSet -> IntSet
- data SplitTel = SplitTel {}
- splitTelescope :: VarSet -> Telescope -> SplitTel
- splitTelescopeExact :: [Int] -> Telescope -> Maybe SplitTel
- instantiateTelescope :: Telescope -> Int -> Term -> Maybe (Telescope, PatternSubstitution, Permutation)
- expandTelescopeVar :: Telescope -> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
- telView :: Type -> TCM TelView
- telViewUpTo :: Int -> Type -> TCM TelView
- telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView
- mustBePi :: MonadTCM tcm => Type -> tcm (Dom Type, Abs Type)
- ifPi :: MonadTCM tcm => Term -> (Dom Type -> Abs Type -> tcm a) -> (Term -> tcm a) -> tcm a
- ifPiType :: MonadTCM tcm => Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a
- ifNotPi :: MonadTCM tcm => Term -> (Term -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
- ifNotPiType :: MonadTCM tcm => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
- piApplyM :: Type -> Args -> TCM Type
- piApply1 :: MonadTCM tcm => Type -> Term -> tcm Type
- typeArity :: Type -> TCM Nat
- data OutputTypeName
- getOutputTypeName :: Type -> TCM OutputTypeName
- addTypedInstance :: QName -> Type -> TCM ()
- resolveUnknownInstanceDefs :: TCM ()
- getInstanceDefs :: TCM InstanceTable
Documentation
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.
withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a] Source #
tele2NamedArgs :: DeBruijn a => Telescope -> Telescope -> [NamedArg a] Source #
A variant of teleNamedArgs
which takes the argument names (and the argument info)
from the first telescope and the variable names from the second telescope.
Precondition: the two telescopes have the same length.
splitTelescopeAt :: Int -> Telescope -> (Telescope, Telescope) Source #
Split the telescope at the specified position.
permuteTel :: Permutation -> Telescope -> Telescope Source #
Permute telescope: permutes or drops the types in the telescope according to the given permutation. Assumes that the permutation preserves the dependencies in the telescope.
For example (Andreas, 2016-12-18, issue #2344):
tel = (A : Set) (X : _18 A) (i : Fin (_m_23 A X))
tel (de Bruijn) = 2:Set, 1:_18
0, 0:Fin(_m_23 1
0)
flattenTel tel = 2:Set, 1:_18 0, 0:Fin(_m_23
1 0) |- [ Set, _18
2, Fin (_m_23 2
1) ]
perm = 0,1,2 -> 0,1 (picks the first two)
renaming _ perm = [var 0, var 1, error] -- THE WRONG RENAMING!
renaming _ (flipP perm) = [error, var 1, var 0] -- The correct renaming!
apply to flattened tel = ... |- [ Set, _18 1, Fin (_m_23
1 0) ]
permute perm it = ... |- [ Set, _18
1 ]
unflatten (de Bruijn) = 1:Set, 0: _18 0
unflatten = (A : Set) (X : _18 A)
varDependencies :: Telescope -> IntSet -> IntSet Source #
Recursively computes dependencies of a set of variables in a given telescope. Any dependencies outside of the telescope are ignored.
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
.
:: [Int] | A list of de Bruijn indices |
-> Telescope | The telescope to split |
-> Maybe SplitTel |
|
As splitTelescope, but fails if any additional variables or reordering would be needed to make the first part well-typed.
:: Telescope | ⊢ Γ |
-> Int | Γ ⊢ var k : A |
-> Term | Γ ⊢ u : A |
-> Maybe (Telescope, PatternSubstitution, Permutation) |
Try to instantiate one variable in the telescope (given by its de Bruijn level) with the given value, returning the new telescope and a substitution to the old one. Returns Nothing if the given value depends (directly or indirectly) on the variable.
expandTelescopeVar :: Telescope -> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution) Source #
Try to eta-expand one variable in the telescope (given by its de Bruijn level)
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
.
ifPi :: MonadTCM tcm => Term -> (Dom Type -> Abs Type -> tcm a) -> (Term -> tcm a) -> tcm a Source #
If the given type is a Pi
, pass its parts to the first continuation.
If not (or blocked), pass the reduced type to the second continuation.
ifPiType :: MonadTCM tcm => Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a Source #
If the given type is a Pi
, pass its parts to the first continuation.
If not (or blocked), pass the reduced type to the second continuation.
ifNotPi :: MonadTCM tcm => Term -> (Term -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a Source #
If the given type is blocked or not a Pi
, pass it reduced to the first continuation.
If it is a Pi
, pass its parts to the second continuation.
ifNotPiType :: MonadTCM tcm => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a Source #
If the given type is blocked or not a Pi
, pass it reduced to the first continuation.
If it is a Pi
, pass its parts to the second continuation.
Instance definitions
data OutputTypeName Source #
getOutputTypeName :: Type -> TCM OutputTypeName Source #
Strips all Pi's and return the head definition name, if possible.
resolveUnknownInstanceDefs :: 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.