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