syntactic-0.8: Language/Syntactic/Interpretation/Equality.hs
module Language.Syntactic.Interpretation.Equality where
import Data.Hash
import Language.Syntactic.Syntax
-- | 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.
class ExprEq expr
where
exprEq :: expr a -> expr b -> Bool
-- | 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@
exprHash :: expr a -> Hash
instance ExprEq dom => ExprEq (AST dom)
where
exprEq (Sym a) (Sym b) = exprEq a b
exprEq (f1 :$ a1) (f2 :$ a2) = exprEq f1 f2 && exprEq a1 a2
exprEq _ _ = False
exprHash (Sym a) = hashInt 0 `combine` exprHash a
exprHash (f :$ a) = hashInt 1 `combine` exprHash f `combine` exprHash a
instance ExprEq dom => Eq (AST dom a)
where
(==) = exprEq
instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
where
exprEq (InjL a) (InjL b) = exprEq a b
exprEq (InjR a) (InjR b) = exprEq a b
exprEq _ _ = False
exprHash (InjL a) = hashInt 0 `combine` exprHash a
exprHash (InjR a) = hashInt 1 `combine` exprHash a
instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)
where
(==) = exprEq