Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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?

  1. 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!

  1. All the clauses that satisfy (1.) need to be headed by a distinct constructor.
Synopsis

Documentation

isUnstableDef :: PureTCM m => QName -> m Bool Source #

Is this a matchable definition, or constructor, which reduces based on interval substitutions?

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. Only returns heads which are stable under interval substitution, i.e. NOT path constructors or generated hcomp/transp!

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 #

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.