module Agda.Compiler.Treeless.Compare (equalTerms) where

import Agda.Syntax.Treeless
import Agda.TypeChecking.Substitute
import Agda.Compiler.Treeless.Subst () --instance only

equalTerms :: TTerm -> TTerm -> Bool
equalTerms :: TTerm -> TTerm -> Bool
equalTerms u :: TTerm
u v :: TTerm
v =
  case (TTerm -> TTerm
evalPrims TTerm
u, TTerm -> TTerm
evalPrims TTerm
v) of
    (TLet s :: TTerm
s u :: TTerm
u@(TCase 0 _ _ _), TLet t :: TTerm
t v :: TTerm
v@(TCase 0 _ _ _)) ->
      TTerm -> TTerm -> Bool
equalTerms TTerm
s TTerm
t Bool -> Bool -> Bool
&& TTerm -> TTerm -> Bool
equalTerms TTerm
u TTerm
v
    (TLet _ (TCase 0 _ _ _), _)      -> Bool
False
    (_, TLet _ (TCase 0 _ _ _))      -> Bool
False
    (TLet t :: TTerm
t u :: TTerm
u, v :: TTerm
v)                    -> TTerm -> TTerm -> Bool
equalTerms (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst 0 TTerm
t TTerm
u) TTerm
v
    (u :: TTerm
u, TLet t :: TTerm
t v :: TTerm
v)                    -> TTerm -> TTerm -> Bool
equalTerms TTerm
u (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst 0 TTerm
t TTerm
v)
    (u :: TTerm
u, v :: TTerm
v) | TTerm
u TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
v                  -> Bool
True
    (TApp f :: TTerm
f us :: Args
us, TApp g :: TTerm
g vs :: Args
vs)           -> (TTerm -> TTerm -> Bool) -> Args -> Args -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList TTerm -> TTerm -> Bool
equalTerms (TTerm
f TTerm -> Args -> Args
forall a. a -> [a] -> [a]
: Args
us) (TTerm
g TTerm -> Args -> Args
forall a. a -> [a] -> [a]
: Args
vs)
    (TCase x :: Int
x _ d :: TTerm
d as :: [TAlt]
as, TCase y :: Int
y _ e :: TTerm
e bs :: [TAlt]
bs) -> Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y Bool -> Bool -> Bool
&& TTerm -> TTerm -> Bool
equalTerms TTerm
d TTerm
e Bool -> Bool -> Bool
&& (TAlt -> TAlt -> Bool) -> [TAlt] -> [TAlt] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList TAlt -> TAlt -> Bool
equalAlts [TAlt]
as [TAlt]
bs
    (TLam u :: TTerm
u, TLam v :: TTerm
v)                 -> TTerm -> TTerm -> Bool
equalTerms TTerm
u TTerm
v
    _                                -> Bool
False

equalAlts :: TAlt -> TAlt -> Bool
equalAlts :: TAlt -> TAlt -> Bool
equalAlts (TACon c :: QName
c a :: Int
a b :: TTerm
b) (TACon c1 :: QName
c1 a1 :: Int
a1 b1 :: TTerm
b1) = (QName
c, Int
a) (QName, Int) -> (QName, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (QName
c1, Int
a1) Bool -> Bool -> Bool
&& TTerm -> TTerm -> Bool
equalTerms TTerm
b TTerm
b1
equalAlts (TALit l :: Literal
l b :: TTerm
b)   (TALit l1 :: Literal
l1 b1 :: TTerm
b1)    = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l1 Bool -> Bool -> Bool
&& TTerm -> TTerm -> Bool
equalTerms TTerm
b TTerm
b1
equalAlts (TAGuard g :: TTerm
g b :: TTerm
b) (TAGuard g1 :: TTerm
g1 b1 :: TTerm
b1)  = TTerm -> TTerm -> Bool
equalTerms TTerm
g TTerm
g1 Bool -> Bool -> Bool
&& TTerm -> TTerm -> Bool
equalTerms TTerm
b TTerm
b1
equalAlts _ _ = Bool
False

eqList :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList eq :: a -> a -> Bool
eq xs :: [a]
xs ys :: [a]
ys = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((a -> a -> Bool) -> [a] -> [a] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> Bool
eq [a]
xs [a]
ys)

evalPrims :: TTerm -> TTerm
evalPrims :: TTerm -> TTerm
evalPrims (TApp (TPrim op :: TPrim
op) [a :: TTerm
a, b :: TTerm
b])
  | Just n :: Integer
n <- TTerm -> Maybe Integer
intView (TTerm -> TTerm
evalPrims TTerm
a),
    Just m :: Integer
m <- TTerm -> Maybe Integer
intView (TTerm -> TTerm
evalPrims TTerm
b),
    Just r :: Integer
r <- TPrim -> Integer -> Integer -> Maybe Integer
applyPrim TPrim
op Integer
n Integer
m = Integer -> TTerm
tInt Integer
r
evalPrims t :: TTerm
t = TTerm
t

applyPrim :: TPrim -> Integer -> Integer -> Maybe Integer
applyPrim :: TPrim -> Integer -> Integer -> Maybe Integer
applyPrim PAdd a :: Integer
a b :: Integer
b = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)
applyPrim PSub a :: Integer
a b :: Integer
b = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b)
applyPrim PMul a :: Integer
a b :: Integer
b = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b)
applyPrim PQuot a :: Integer
a b :: Integer
b | Integer
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0    = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
quot Integer
a Integer
b)
                   | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PRem a :: Integer
a b :: Integer
b | Integer
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0    = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
rem Integer
a Integer
b)
                   | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PGeq _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PLt  _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEqI _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEqF _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEqC _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEqS _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEqQ _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PIf  _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PSeq _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PAdd64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PSub64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PMul64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PQuot64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PRem64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PLt64  _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PEq64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim PITo64 _ _ = Maybe Integer
forall a. Maybe a
Nothing
applyPrim P64ToI _ _ = Maybe Integer
forall a. Maybe a
Nothing