Agda.TypeChecking.SyntacticEquality

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.

Documentation

class SynEq a

Instantiate full as long as things are equal

Minimal complete definition

synEq

Instances

SynEq ArgInfo

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Level -> Level -> SynEqM (Level, Level)

synEq' :: Level -> Level -> SynEqM (Level, Level)

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)

synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Sort -> Sort -> SynEqM (Sort, Sort)

synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)

SynEq Term

Syntactic term equality ignores DontCare stuff.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Term -> Term -> SynEqM (Term, Term)

synEq' :: Term -> Term -> SynEqM (Term, Term)

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Type -> Type -> SynEqM (Type, Type)

synEq' :: Type -> Type -> SynEqM (Type, Type)

SynEq Bool

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Bool -> Bool -> SynEqM (Bool, Bool)

synEq' :: Bool -> Bool -> SynEqM (Bool, Bool)

SynEq a => SynEq (Arg a)

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)

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)

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)

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]

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)

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

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'

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

Does the syntactic equality check have any remaining fuel?