Safe Haskell | None |
---|---|

Language | Haskell2010 |

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' :: (MonadReduce m, MonadError TCErr m, MonadDebug m, HasBuiltins 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. (MonadReduce m, MonadError TCErr m, MonadDebug m, HasBuiltins m) => QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
- functionInverse :: (MonadReduce m, MonadError TCErr m, HasBuiltins m, HasConstInfo m) => Term -> m InvView
- data InvView
- useInjectivity :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
- invertFunction :: MonadConversion m => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m ()
- forcePiUsingInjectivity :: Type -> TCM Type

# Documentation

headSymbol' :: (MonadReduce m, MonadError TCErr m, MonadDebug m, HasBuiltins 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. (MonadReduce m, MonadError TCErr m, MonadDebug m, HasBuiltins 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 :: (MonadReduce m, MonadError TCErr m, HasBuiltins m, HasConstInfo m) => Term -> m InvView Source #

Argument should be in weak head normal form.

useInjectivity :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m () Source #

Precondition: The first argument must be blocked 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.