{-# LANGUAGE FlexibleInstances    #-}

-- Syntactic Equality of Types up to forall type renaming

module Language.Haskell.Liquid.Types.Equality where

import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RefType ()
import           Language.Haskell.Liquid.Types.Types
import qualified Liquid.GHC.API as Ghc

import Control.Monad (liftM2, zipWithM)
import Control.Monad.Writer.Lazy
import           Data.Function (on)
import qualified Data.List as L

instance REq SpecType where
  SpecType
t1 =*= :: SpecType -> SpecType -> Bool
=*= SpecType
t2 = SpecType -> SpecType -> Bool
compareRType SpecType
t1 SpecType
t2

compareRType :: SpecType -> SpecType -> Bool
compareRType :: SpecType -> SpecType -> Bool
compareRType SpecType
i1 SpecType
i2 = Bool
res Bool -> Bool -> Bool
&& [(RTyVar, RTyVar)] -> Bool
unify [(RTyVar, RTyVar)]
ys
  where
    unify :: [(RTyVar, RTyVar)] -> Bool
unify =
      ([(RTyVar, RTyVar)] -> Bool) -> [[(RTyVar, RTyVar)]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([RTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([RTyVar] -> Bool)
-> ([(RTyVar, RTyVar)] -> [RTyVar]) -> [(RTyVar, RTyVar)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [RTyVar] -> [RTyVar]
forall a. Int -> [a] -> [a]
drop Int
1 ([RTyVar] -> [RTyVar])
-> ([(RTyVar, RTyVar)] -> [RTyVar])
-> [(RTyVar, RTyVar)]
-> [RTyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RTyVar] -> [RTyVar]
forall a. Eq a => [a] -> [a]
L.nub ([RTyVar] -> [RTyVar])
-> ([(RTyVar, RTyVar)] -> [RTyVar])
-> [(RTyVar, RTyVar)]
-> [RTyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RTyVar, RTyVar) -> RTyVar) -> [(RTyVar, RTyVar)] -> [RTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (RTyVar, RTyVar) -> RTyVar
forall a b. (a, b) -> b
snd) ([[(RTyVar, RTyVar)]] -> Bool)
-> ([(RTyVar, RTyVar)] -> [[(RTyVar, RTyVar)]])
-> [(RTyVar, RTyVar)]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      ((RTyVar, RTyVar) -> (RTyVar, RTyVar) -> Bool)
-> [(RTyVar, RTyVar)] -> [[(RTyVar, RTyVar)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
(==) (RTyVar -> RTyVar -> Bool)
-> ((RTyVar, RTyVar) -> RTyVar)
-> (RTyVar, RTyVar)
-> (RTyVar, RTyVar)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (RTyVar, RTyVar) -> RTyVar
forall a b. (a, b) -> a
fst) ([(RTyVar, RTyVar)] -> [[(RTyVar, RTyVar)]])
-> ([(RTyVar, RTyVar)] -> [(RTyVar, RTyVar)])
-> [(RTyVar, RTyVar)]
-> [[(RTyVar, RTyVar)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      ((RTyVar, RTyVar) -> RTyVar)
-> [(RTyVar, RTyVar)] -> [(RTyVar, RTyVar)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (RTyVar, RTyVar) -> RTyVar
forall a b. (a, b) -> a
fst

    (Bool
res, [(RTyVar, RTyVar)]
ys) = Writer [(RTyVar, RTyVar)] Bool -> (Bool, [(RTyVar, RTyVar)])
forall w a. Writer w a -> (a, w)
runWriter (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
i1 SpecType
i2)
    go :: SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
    go :: SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go (RAllT RTVUV Symbol RTyCon RTyVar
x1 SpecType
t1 RReft
r1) (RAllT RTVUV Symbol RTyCon RTyVar
x2 SpecType
t2 RReft
r2)
      | RTV TyVar
v1 <- RTVUV Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVUV Symbol RTyCon RTyVar
x1
      , RTV TyVar
v2 <- RTVUV Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVUV Symbol RTyCon RTyVar
x2
      , RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2
      = SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t1 ((TyVar, Type) -> SpecType -> SpecType
forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (TyVar
v2, TyVar -> Type
Ghc.mkTyVarTy TyVar
v1) SpecType
t2)

    go (RVar RTyVar
v1 RReft
r1) (RVar RTyVar
v2 RReft
r2)
      = do [(RTyVar, RTyVar)] -> WriterT [(RTyVar, RTyVar)] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [(RTyVar
v1, RTyVar
v2)]
           Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2)
     -- = v1 == v2 && r1 =*= r2
    go (RFun Symbol
x1 RFInfo
_ SpecType
t11 SpecType
t12 RReft
r1) (RFun Symbol
x2 RFInfo
_ SpecType
t21 SpecType
t22 RReft
r2)
      | Symbol
x1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2 Bool -> Bool -> Bool
&& RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2
      = (Bool -> Bool -> Bool)
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t11 SpecType
t21) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t12 SpecType
t22)
    go (RAllP PVUV Symbol RTyCon RTyVar
x1 SpecType
t1) (RAllP PVUV Symbol RTyCon RTyVar
x2 SpecType
t2)
      | PVUV Symbol RTyCon RTyVar
x1 PVUV Symbol RTyCon RTyVar -> PVUV Symbol RTyCon RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== PVUV Symbol RTyCon RTyVar
x2
      = SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t1 SpecType
t2
    go (RApp RTyCon
x1 [SpecType]
ts1 [RTPropV Symbol RTyCon RTyVar RReft]
ps1 RReft
r1) (RApp RTyCon
x2 [SpecType]
ts2 [RTPropV Symbol RTyCon RTyVar RReft]
ps2 RReft
r2)
      | RTyCon
x1 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
x2 Bool -> Bool -> Bool
&&
        RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((RTPropV Symbol RTyCon RTyVar RReft
 -> RTPropV Symbol RTyCon RTyVar RReft -> Bool)
-> [RTPropV Symbol RTyCon RTyVar RReft]
-> [RTPropV Symbol RTyCon RTyVar RReft]
-> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RTPropV Symbol RTyCon RTyVar RReft
-> RTPropV Symbol RTyCon RTyVar RReft -> Bool
forall a. REq a => a -> a -> Bool
(=*=) [RTPropV Symbol RTyCon RTyVar RReft]
ps1 [RTPropV Symbol RTyCon RTyVar RReft]
ps2)
      = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> WriterT [(RTyVar, RTyVar)] Identity [Bool]
-> Writer [(RTyVar, RTyVar)] Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool)
-> [SpecType]
-> [SpecType]
-> WriterT [(RTyVar, RTyVar)] Identity [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go [SpecType]
ts1 [SpecType]
ts2
    go (RAllE Symbol
x1 SpecType
t11 SpecType
t12) (RAllE Symbol
x2 SpecType
t21 SpecType
t22) | Symbol
x1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
      = (Bool -> Bool -> Bool)
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t11 SpecType
t21) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t12 SpecType
t22)
    go (REx Symbol
x1 SpecType
t11 SpecType
t12) (REx Symbol
x2 SpecType
t21 SpecType
t22) | Symbol
x1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
      = (Bool -> Bool -> Bool)
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t11 SpecType
t21) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t12 SpecType
t22)
    go (RExprArg Located (ExprV Symbol)
e1) (RExprArg Located (ExprV Symbol)
e2)
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Located (ExprV Symbol)
e1 Located (ExprV Symbol) -> Located (ExprV Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= Located (ExprV Symbol)
e2)
    go (RAppTy SpecType
t11 SpecType
t12 RReft
r1) (RAppTy SpecType
t21 SpecType
t22 RReft
r2) | RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2
      = (Bool -> Bool -> Bool)
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
-> Writer [(RTyVar, RTyVar)] Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t11 SpecType
t21) (SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
go SpecType
t12 SpecType
t22)
    go (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
r1) (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
r2)
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
r1 SpecType -> SpecType -> Bool
forall a. REq a => a -> a -> Bool
=*= SpecType
r2)
    go (RHole RReft
r1) (RHole RReft
r2)
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RReft
r1 RReft -> RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RReft
r2)
    go SpecType
_t1 SpecType
_t2
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

class REq a where
  (=*=) :: a -> a -> Bool

instance REq t2 => REq (Ref t1 t2) where
    (RProp [(Symbol, t1)]
_ t2
t1) =*= :: Ref t1 t2 -> Ref t1 t2 -> Bool
=*= (RProp [(Symbol, t1)]
_ t2
t2) = t2
t1 t2 -> t2 -> Bool
forall a. REq a => a -> a -> Bool
=*= t2
t2

instance REq (UReft F.Reft) where
  (MkUReft Reft
r1 PredicateV Symbol
p1) =*= :: RReft -> RReft -> Bool
=*= (MkUReft Reft
r2 PredicateV Symbol
p2)
     = Reft
r1 Reft -> Reft -> Bool
forall a. REq a => a -> a -> Bool
=*= Reft
r2 Bool -> Bool -> Bool
&& PredicateV Symbol
p1 PredicateV Symbol -> PredicateV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PredicateV Symbol
p2

instance REq F.Reft where
  F.Reft (Symbol
v1, ExprV Symbol
e1) =*= :: Reft -> Reft -> Bool
=*= F.Reft (Symbol
v2, ExprV Symbol
e2) = ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 ExprV Symbol
e1 (Symbol
v1, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
v2) ExprV Symbol -> ExprV Symbol -> Bool
forall a. REq a => a -> a -> Bool
=*= ExprV Symbol
e2

instance REq F.Expr where
  ExprV Symbol
e1 =*= :: ExprV Symbol -> ExprV Symbol -> Bool
=*= ExprV Symbol
e2 = ExprV Symbol -> ExprV Symbol -> Bool
forall {a}. (Eq a, Fixpoint a) => a -> a -> Bool
go (ExprV Symbol -> ExprV Symbol
forall a. Fixpoint a => a -> a
F.simplify ExprV Symbol
e1) (ExprV Symbol -> ExprV Symbol
forall a. Fixpoint a => a -> a
F.simplify ExprV Symbol
e2)
    where go :: a -> a -> Bool
go a
r1 a
r2 = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp (String
"comparing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Doc, Doc) -> String
forall a. PPrint a => a -> String
showpp (a -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix a
r1, a -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix a
r2)) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
r1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
r2

instance REq r => REq (Located r) where
  Located r
t1 =*= :: Located r -> Located r -> Bool
=*= Located r
t2 = Located r -> r
forall a. Located a -> a
val Located r
t1 r -> r -> Bool
forall a. REq a => a -> a -> Bool
=*= Located r -> r
forall a. Located a -> a
val Located r
t2