| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.SyntacticEquality
Description
A syntactic equality check that takes meta instantiations into account,
but does not reduce. It replaces
(v, v') <- instantiateFull (v, v')
v == v'
by a more efficient routine which only traverses and instantiates the terms
as long as they are equal.
Synopsis
- class SynEq a
- checkSyntacticEquality :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
- checkSyntacticEquality' :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
- syntacticEqualityFuelRemains :: MonadReduce m => m Bool
Documentation
Instantiate full as long as things are equal
Minimal complete definition
synEq
Instances
| SynEq ArgInfo Source # | |
| SynEq Level Source # | |
| SynEq PlusLevel Source # | |
| SynEq Sort Source # | |
| SynEq Term Source # | Syntactic term equality ignores |
| SynEq Type Source # | Syntactic equality ignores sorts. |
| SynEq Bool Source # | |
Defined in Agda.TypeChecking.SyntacticEquality | |
| SynEq a => SynEq (Arg a) Source # | |
| (Subst a, SynEq a) => SynEq (Abs a) Source # | |
| SynEq a => SynEq (Dom a) Source # | |
| SynEq a => SynEq (Elim' a) Source # | |
| SynEq a => SynEq [a] Source # | |
Defined in Agda.TypeChecking.SyntacticEquality | |
| (SynEq a, SynEq b) => SynEq (a, b) Source # | |
Defined in Agda.TypeChecking.SyntacticEquality | |
checkSyntacticEquality Source #
Arguments
| :: (Instantiate a, SynEq a, MonadReduce m) | |
| => a | |
| -> a | |
| -> (a -> a -> m b) | Continuation used upon success. |
| -> (a -> a -> m b) | Continuation used upon failure, or if syntactic equality checking has been turned off. |
| -> m b |
Syntactic equality check for terms. If syntactic equality
checking has fuel left, then checkSyntacticEquality behaves as if
it were implemented in the following way (which does not match the
given type signature), only that v and v' are only fully
instantiated to the depth where they are equal (and the amount of
fuel is reduced by one unit in the failure branch):
checkSyntacticEquality v v' s f = do
(v, v') <- instantiateFull (v, v')
if v == v' then s v v' else f v v'
If syntactic equality checking does not have fuel left, then
checkSyntacticEquality instantiates the two terms and takes the
failure branch.
Note that in either case the returned values v and v' cannot be
MetaVs that are instantiated.
checkSyntacticEquality' Source #
Arguments
| :: (Instantiate a, SynEq a, MonadReduce m) | |
| => a | |
| -> a | |
| -> (a -> a -> m b) | Continuation used upon success. |
| -> (a -> a -> m b) | Continuation used upon failure. |
| -> m b |
Syntactic equality check for terms without checking remaining fuel.
syntacticEqualityFuelRemains :: MonadReduce m => m Bool Source #
Does the syntactic equality check have any remaining fuel?