| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Injectivity
Description
Injectivity, or more precisely, "constructor headedness", is a property of functions defined by pattern matching that helps us solve constraints involving blocked applications of such functions. Blocked shall mean here that pattern matching is blocked on a meta variable, and constructor headedness lets us learn more about that meta variable.
Consider the simple example:
isZero : Nat -> Bool
isZero zero = true
isZero (suc n) = false
This function is constructor-headed, meaning that all rhss are headed
by a distinct constructor. Thus, on a constraint like
isZero ?X = false : Bool
involving an application of isZero that is blocked on meta variable ?X,
we can exploit injectivity and learn that ?X = suc ?Y for a new
meta-variable ?Y.
Which functions qualify for injectivity?
- The function needs to have at least one non-absurd clause that has a proper match, meaning that the function can actually be blocked on a meta. Proper matches are these patterns:
- data constructor (
ConP, but not record constructor) - literal (
LitP) - HIT-patterns (
DefP)
Projection patterns (ProjP) are excluded because metas cannot occupy their place!
- All the clauses that satisfy (1.) need to be headed by a distinct constructor.
Synopsis
- headSymbol :: Term -> TCM (Maybe TermHead)
- headSymbol' :: (PureTCM m, MonadError TCErr m) => Term -> m (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
- checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse
- checkOverapplication :: forall m. HasConstInfo m => Elims -> InversionMap Clause -> m (InversionMap Clause)
- instantiateVarHeads :: forall m c. (PureTCM m, MonadError TCErr m) => QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
- functionInverse :: (PureTCM m, MonadError TCErr m) => Term -> m InvView
- data InvView
- useInjectivity :: MonadConversion m => CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
- invertFunction :: MonadConversion m => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m ()
- forcePiUsingInjectivity :: Type -> TCM Type
Documentation
headSymbol' :: (PureTCM m, MonadError TCErr m) => Term -> m (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 #
checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse Source #
Precondition: all the given clauses are non-absurd and contain a proper match.
checkOverapplication :: forall m. HasConstInfo m => Elims -> InversionMap Clause -> m (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 :: forall m c. (PureTCM m, MonadError TCErr m) => QName -> Elims -> InversionMap c -> m (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.
functionInverse :: (PureTCM m, MonadError TCErr m) => Term -> m InvView Source #
Argument should be in weak head normal form.
useInjectivity :: MonadConversion m => CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m () Source #
Precondition: The first term must be blocked on the given meta and the second must be neutral.
invertFunction :: MonadConversion m => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m () Source #
The second argument should be a blocked application and the third argument the inverse of the applied function.