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 :: 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