Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- headSymbol :: Term -> TCM (Maybe TermHead)
- headSymbol' :: Term -> TCM (Maybe TermHead)
- topLevelArg :: Clause -> Int -> Maybe TermHead
- joinHeadMaps :: [InversionMap c] -> InversionMap c
- updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c)
- checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
- checkOverapplication :: Elims -> InversionMap Clause -> TCM (InversionMap Clause)
- instantiateVarHeads :: QName -> Elims -> InversionMap c -> TCM (Maybe (InversionMap c))
- functionInverse :: Term -> TCM InvView
- data InvView
- data MaybeAbort
- useInjectivity :: CompareDirection -> Type -> Term -> Term -> TCM ()
- invertFunction :: Comparison -> Term -> InvView -> TermHead -> TCM () -> TCM () -> (Term -> TCM ()) -> TCM ()
- forcePiUsingInjectivity :: Type -> TCM Type
Documentation
headSymbol' :: Term -> TCM (Maybe TermHead) Source #
Do a full whnf and treat neutral terms as rigid. Used on the arguments to an injective functions and to the right-hand side.
topLevelArg :: Clause -> Int -> Maybe TermHead Source #
Does deBruijn variable i correspond to a top-level argument, and if so which one (index from the left).
joinHeadMaps :: [InversionMap c] -> InversionMap c Source #
Join a list of inversion maps.
updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c) Source #
Update the heads of an inversion map.
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse Source #
checkOverapplication :: Elims -> InversionMap Clause -> TCM (InversionMap Clause) Source #
If a clause is over-applied we can't trust the head (Issue 2944). For
instance, the clause might be `f ps = u , v` and the actual call `f vs
.fst`. In this case the head will be the head of u
rather than `_,_`.
instantiateVarHeads :: QName -> Elims -> InversionMap c -> TCM (Maybe (InversionMap c)) Source #
Turn variable heads, referring to top-level argument positions, into
proper heads. These might still be VarHead
, but in that case they refer to
deBruijn variables. Checks that the instantiated heads are still rigid and
distinct.
data MaybeAbort Source #
useInjectivity :: CompareDirection -> Type -> Term -> Term -> TCM () Source #
Precondition: The first argument must be blocked and the second must be neutral.