    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 (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    0 TTerm
    SubstArg TTerm
    t TTerm
    u) TTerm
    v
        (TTerm
    u, TLet TTerm
    t TTerm
    v)                    -> TTerm -> TTerm -> Bool
    equalTerms TTerm
    u (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    0 TTerm
    SubstArg TTerm
    t TTerm
    v)
        (TTerm
    u, TTerm
    v) | TTerm
    u TTerm -> TTerm -> Bool
    forall a. Eq a => a -> a -> Bool
    == TTerm
    v                  -> Bool
    True
        (TApp TTerm
    f Args
    us, TApp TTerm
    g 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 Int
    x CaseInfo
    _ TTerm
    d [TAlt]
    as, TCase Int
    y CaseInfo
    _ TTerm
    e [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 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) (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 Literal
    l TTerm
    b)   (TALit Literal
    l1 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 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 = [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 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 = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer
    a Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    b)
    applyPrim TPrim
    PSub Integer
    a 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 TPrim
    PMul Integer
    a 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 TPrim
    PQuot Integer
    a Integer
    b | Integer
    b Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    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 TPrim
    PRem Integer
    a Integer
    b | Integer
    b Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    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 TPrim
    PGeq Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PLt  Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEqI Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEqF Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEqC Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEqS Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEqQ Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PIf  Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PSeq Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PAdd64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PSub64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PMul64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PQuot64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PRem64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PLt64  Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PEq64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    PITo64 Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing
    applyPrim TPrim
    P64ToI Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing