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

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

eqList :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList :: forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqList a -> a -> Bool
eq [a]
xs [a]
ys = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (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 TPrim
op) [TTerm
a, TTerm
b])
  | Just Integer
n <- TTerm -> Maybe Integer
intView (TTerm -> TTerm
evalPrims TTerm
a),
    Just Integer
m <- TTerm -> Maybe Integer
intView (TTerm -> TTerm
evalPrims TTerm
b),
    Just Integer
r <- TPrim -> Integer -> Integer -> Maybe Integer
applyPrim TPrim
op Integer
n Integer
m = Integer -> TTerm
tInt Integer
r
evalPrims TTerm
t = TTerm
t

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