Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
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?

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

- 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
  - = Inv QName [Elim] (InversionMap Clause)
  - | NoInv
- 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 :: Term -> TCM (Maybe TermHead) Source #

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.

data InvView Source #

Constructors

Inv QName [Elim] (InversionMap Clause) |
NoInv |

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.

forcePiUsingInjectivity :: Type -> TCM Type Source #