module Agda.Compiler.Treeless.Compare (equalTerms) where
import Agda.Syntax.Treeless
import Agda.TypeChecking.Substitute
import Agda.Compiler.Treeless.Subst ()
equalTerms :: TTerm -> TTerm -> Bool
equalTerms u v =
case (evalPrims u, evalPrims v) of
(TLet s u@(TCase 0 _ _ _), TLet t v@(TCase 0 _ _ _)) ->
equalTerms s t && equalTerms u v
(TLet _ (TCase 0 _ _ _), _) -> False
(_, TLet _ (TCase 0 _ _ _)) -> False
(TLet t u, v) -> equalTerms (subst 0 t u) v
(u, TLet t v) -> equalTerms u (subst 0 t v)
(u, v) | u == v -> True
(TApp f us, TApp g vs) -> eqList equalTerms (f : us) (g : vs)
(TCase x _ d as, TCase y _ e bs) -> x == y && equalTerms d e && eqList equalAlts as bs
(TLam u, TLam v) -> equalTerms u v
_ -> False
equalAlts :: TAlt -> TAlt -> Bool
equalAlts (TACon c a b) (TACon c1 a1 b1) = (c, a) == (c1, a1) && equalTerms b b1
equalAlts (TALit l b) (TALit l1 b1) = l == l1 && equalTerms b b1
equalAlts (TAGuard g b) (TAGuard g1 b1) = equalTerms g g1 && equalTerms b b1
equalAlts _ _ = False
eqList :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList eq xs ys = length xs == length ys && and (zipWith eq xs ys)
evalPrims :: TTerm -> TTerm
evalPrims (TApp (TPrim op) [a, b])
| Just n <- intView (evalPrims a),
Just m <- intView (evalPrims b),
Just r <- applyPrim op n m = tInt r
evalPrims t = t
applyPrim :: TPrim -> Integer -> Integer -> Maybe Integer
applyPrim PAdd a b = Just (a + b)
applyPrim PSub a b = Just (a - b)
applyPrim PMul a b = Just (a * b)
applyPrim PQuot a b | b /= 0 = Just (quot a b)
| otherwise = Nothing
applyPrim PRem a b | b /= 0 = Just (rem a b)
| otherwise = Nothing
applyPrim PGeq _ _ = Nothing
applyPrim PLt _ _ = Nothing
applyPrim PEqI _ _ = Nothing
applyPrim PEqF _ _ = Nothing
applyPrim PEqC _ _ = Nothing
applyPrim PEqS _ _ = Nothing
applyPrim PEqQ _ _ = Nothing
applyPrim PIf _ _ = Nothing
applyPrim PSeq _ _ = Nothing
applyPrim PAdd64 _ _ = Nothing
applyPrim PSub64 _ _ = Nothing
applyPrim PMul64 _ _ = Nothing
applyPrim PQuot64 _ _ = Nothing
applyPrim PRem64 _ _ = Nothing
applyPrim PLt64 _ _ = Nothing
applyPrim PEq64 _ _ = Nothing
applyPrim PITo64 _ _ = Nothing
applyPrim P64ToI _ _ = Nothing