Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

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

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 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?