1module Agda.Compiler.Treeless.Compare (equalTerms) where
2
3import Agda.Syntax.Treeless
4import Agda.TypeChecking.Substitute
5import Agda.Compiler.Treeless.Subst () --instance only
6
7equalTerms :: TTerm -> TTerm -> Bool
8equalTerms u v =
9  case (evalPrims u, evalPrims v) of
10    (TLet s u@(TCase 0 _ _ _), TLet t v@(TCase 0 _ _ _)) ->
11      equalTerms s t && equalTerms u v
12    (TLet _ (TCase 0 _ _ _), _)      -> False
13    (_, TLet _ (TCase 0 _ _ _))      -> False
14    (TLet t u, v)                    -> equalTerms (subst 0 t u) v
15    (u, TLet t v)                    -> equalTerms u (subst 0 t v)
16    (u, v) | u == v                  -> True
17    (TApp f us, TApp g vs)           -> eqList equalTerms (f : us) (g : vs)
18    (TCase x _ d as, TCase y _ e bs) -> x == y && equalTerms d e && eqList equalAlts as bs
19    (TLam u, TLam v)                 -> equalTerms u v
20    _                                -> False
21
22equalAlts :: TAlt -> TAlt -> Bool
23equalAlts (TACon c a b) (TACon c1 a1 b1) = (c, a) == (c1, a1) && equalTerms b b1
24equalAlts (TALit l b)   (TALit l1 b1)    = l == l1 && equalTerms b b1
25equalAlts (TAGuard g b) (TAGuard g1 b1)  = equalTerms g g1 && equalTerms b b1
26equalAlts _ _ = False
27
28eqList :: (a -> a -> Bool) -> [a] -> [a] -> Bool
29eqList eq xs ys = length xs == length ys && and (zipWith eq xs ys)
30
31evalPrims :: TTerm -> TTerm
32evalPrims (TApp (TPrim op) [a, b])
33  | Just n <- intView (evalPrims a),
34    Just m <- intView (evalPrims b),
35    Just r <- applyPrim op n m = tInt r
36evalPrims t = t
37
38applyPrim :: TPrim -> Integer -> Integer -> Maybe Integer
39applyPrim PAdd a b = Just (a + b)
40applyPrim PSub a b = Just (a - b)
41applyPrim PMul a b = Just (a * b)
42applyPrim PQuot a b | b /= 0    = Just (quot a b)
43                   | otherwise = Nothing
44applyPrim PRem a b | b /= 0    = Just (rem a b)
45                   | otherwise = Nothing
46applyPrim PGeq _ _ = Nothing
47applyPrim PLt  _ _ = Nothing
48applyPrim PEqI _ _ = Nothing
49applyPrim PEqF _ _ = Nothing
50applyPrim PEqC _ _ = Nothing
51applyPrim PEqS _ _ = Nothing
52applyPrim PEqQ _ _ = Nothing
53applyPrim PIf  _ _ = Nothing
54applyPrim PSeq _ _ = Nothing
55applyPrim PAdd64 _ _ = Nothing
56applyPrim PSub64 _ _ = Nothing
57applyPrim PMul64 _ _ = Nothing
58applyPrim PQuot64 _ _ = Nothing
59applyPrim PRem64 _ _ = Nothing
60applyPrim PLt64  _ _ = Nothing
61applyPrim PEq64 _ _ = Nothing
62applyPrim PITo64 _ _ = Nothing
63applyPrim P64ToI _ _ = Nothing
64
65