    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