Language.Syntactic.Analysis.Equality

Documentation

class ExprEq expr where

Equality for expressions. The difference between Eq and ExprEq is that ExprEq allows comparison of expressions with different value types. It is assumed that when the types differ, the expressions also differ. The reason for allowing comparison of different types is that this is convenient when the types are existentially quantified.

Methods

exprEq :: expr a -> expr b -> Bool

exprHash :: expr a -> Hash

Computes a Hash for an expression. Expressions that are equal according to exprEq must result in the same hash:

exprEq a b  ==>  exprHash a == exprHash b

Instances

ExprEq Sym

ExprEq dom => ExprEq (AST dom)

ExprEq (Literal ctx)

ExprEq (Condition ctx)

ExprEq (Select ctx)

ExprEq (Tuple ctx)

ExprEq (Lambda ctx)

exprEq does strict identifier comparison; i.e. no alpha equivalence.

exprHash assigns the same hash to all Lambda bindings. This is a valid over-approximation that enables the following property:

alphaEq a b  ==>  exprHash a == exprHash b

ExprEq (Variable ctx)

exprEq does strict identifier comparison; i.e. no alpha equivalence.

exprHash assigns the same hash to all variables. This is a valid over-approximation that enables the following property:

alphaEq a b  ==>  exprHash a == exprHash b

(ExprEq expr1, ExprEq expr2) => ExprEq (:+: expr1 expr2)

ExprEq expr => ExprEq (Ann info expr)

ExprEq (Let ctxa ctxb)