Agda.TypeChecking.Injectivity

Documentation

headSymbol :: Term -> TCM (Maybe TermHead)

headSymbol' :: Term -> TCM (Maybe TermHead)

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

Does deBruijn variable i correspond to a top-level argument, and if so which one (index from the left).

joinHeadMaps :: [InversionMap c] -> InversionMap c

Join a list of inversion maps.

updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c)

Update the heads of an inversion map.

checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse

checkOverapplication :: Elims -> InversionMap Clause -> TCM (InversionMap Clause)

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

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.

functionInverse :: Term -> TCM InvView

Argument should be in weak head normal form.

data InvView

Constructors

Inv QName [Elim] (InversionMap Clause)

NoInv

data MaybeAbort

Constructors

Abort

KeepGoing

useInjectivity :: CompareDirection -> Type -> Term -> Term -> TCM ()

Precondition: The first argument must be blocked and the second must be neutral.

invertFunction :: Comparison -> Term -> InvView -> TermHead -> TCM () -> TCM () -> (Term -> TCM ()) -> TCM ()

The second argument should be a blocked application and the third argument the inverse of the applied function.

forcePiUsingInjectivity :: Type -> TCM Type