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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Injectivity

Synopsis

- headSymbol :: Term -> TCM (Maybe TermHead)
- headSymbol' :: Term -> TCM (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
- checkOverapplication :: Elims -> InversionMap Clause -> TCM (InversionMap Clause)
- instantiateVarHeads :: QName -> Elims -> InversionMap c -> TCM (Maybe (InversionMap c))
- functionInverse :: Term -> TCM InvView
- data InvView
  - = Inv QName [Elim] (InversionMap Clause)
  - | NoInv
- data MaybeAbort
  - = Abort
  - | KeepGoing
- useInjectivity :: CompareDirection -> Type -> Term -> Term -> TCM ()
- invertFunction :: Comparison -> Term -> InvView -> TermHead -> TCM () -> TCM () -> (Term -> TCM ()) -> TCM ()
- forcePiUsingInjectivity :: Type -> TCM Type

# Documentation

headSymbol :: Term -> TCM (Maybe TermHead) Source #

headSymbol' :: Term -> TCM (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 #

checkOverapplication :: Elims -> InversionMap Clause -> TCM (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 :: QName -> Elims -> InversionMap c -> TCM (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 :: Term -> TCM InvView Source #

Argument should be in weak head normal form.

data InvView Source #

Constructors

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

data MaybeAbort Source #

Constructors

Abort |
KeepGoing |

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

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

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

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

forcePiUsingInjectivity :: Type -> TCM Type Source #