module Language.Syntactic.Analysis.Equality where
import Language.Syntactic.Syntax
class ExprEq expr
where
exprEq :: expr a -> expr b -> Bool
instance ExprEq dom => ExprEq (AST dom)
where
exprEq (Symbol a) (Symbol b) = exprEq a b
exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2
exprEq _ _ = False
instance ExprEq dom => Eq (AST dom a)
where
(==) = exprEq
instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
where
exprEq (InjectL a) (InjectL b) = exprEq a b
exprEq (InjectR a) (InjectR b) = exprEq a b
exprEq _ _ = False
instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)
where
(==) = exprEq
eqSyn :: (Syntactic a dom, ExprEq dom) => a -> a -> Bool
eqSyn a b = desugar a `exprEq` desugar b