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

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

class SynEq a Source #

Instantiate full as long as things are equal

Minimal complete definition

synEq

#### Instances

Instances details

SynEq ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo) synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)
SynEq Level Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
SynEq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
SynEq Sort Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
SynEq Term Source # | Syntactic term equality ignores `DontCare` stuff.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Term -> Term -> SynEqM (Term, Term) synEq' :: Term -> Term -> SynEqM (Term, Term)
SynEq Type Source # | Syntactic equality ignores sorts.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
SynEq Bool Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Bool -> Bool -> SynEqM (Bool, Bool) synEq' :: Bool -> Bool -> SynEqM (Bool, Bool)
SynEq a => SynEq (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a) synEq' :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)
(Subst a, SynEq a) => SynEq (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a) synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
SynEq a => SynEq (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a) synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
SynEq a => SynEq (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a) synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
SynEq a => SynEq [a] Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: [a] -> [a] -> SynEqM ([a], [a]) synEq' :: [a] -> [a] -> SynEqM ([a], [a])
(SynEq a, SynEq b) => SynEq (a, b) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: (a, b) -> (a, b) -> SynEqM ((a, b), (a, b)) synEq' :: (a, b) -> (a, b) -> SynEqM ((a, b), (a, b))

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 `MetaV`s 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?