{-# 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
  RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1 =*= :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Bool
=*= RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2 = RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Bool
compareRType RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2

compareRType :: SpecType -> SpecType -> Bool
compareRType :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Bool
compareRType RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
i1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
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 (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
i1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
i2)
    go :: SpecType -> SpecType -> Writer [(RTyVar, RTyVar)] Bool
    go :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
x1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
x2 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
      | RTV Var
v1 <- RTVUBV Symbol Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVUBV Symbol Symbol RTyCon RTyVar
x1
      , RTV Var
v2 <- RTVUBV Symbol Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVUBV Symbol Symbol RTyCon RTyVar
x2
      , UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2
      = RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1 ((Var, Type)
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Var
v2, Var -> Type
Ghc.mkTyVarTy Var
v1) RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2)

    go (RVar RTyVar
v1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RVar RTyVar
v2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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 (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
     -- = v1 == v2 && r1 =*= r2
    go (RFun Symbol
x1 RFInfo
_ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RFun Symbol
x2 RFInfo
_ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
      | Symbol
x1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2 Bool -> Bool -> Bool
&& UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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
(&&) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22)
    go (RAllP PVarBV
  Symbol
  Symbol
  (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
x1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1) (RAllP PVarBV
  Symbol
  Symbol
  (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
x2 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2)
      | PVarBV
  Symbol
  Symbol
  (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
x1 PVarBV
  Symbol
  Symbol
  (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
-> PVarBV
     Symbol
     Symbol
     (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
-> Bool
forall a. Eq a => a -> a -> Bool
== PVarBV
  Symbol
  Symbol
  (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
x2
      = RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t2
    go (RApp RTyCon
x1 [RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts1 [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RApp RTyCon
x2 [RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts2 [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
      | RTyCon
x1 RTyCon -> RTyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon
x2 Bool -> Bool -> Bool
&&
        UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> Bool)
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RTPropBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Bool
forall a. REq a => a -> a -> Bool
(=*=) [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps1 [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
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
<$> (RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> Writer [(RTyVar, RTyVar)] Bool)
-> [RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTypeBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> WriterT [(RTyVar, RTyVar)] Identity [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go [RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts1 [RTypeBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts2
    go (RAllE Symbol
x1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12) (RAllE Symbol
x2 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
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
(&&) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22)
    go (REx Symbol
x1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12) (REx Symbol
x2 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
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
(&&) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22)
    go (RExprArg Located (ExprBV Symbol Symbol)
e1) (RExprArg Located (ExprBV Symbol 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 (ExprBV Symbol Symbol)
e1 Located (ExprBV Symbol Symbol)
-> Located (ExprBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= Located (ExprBV Symbol Symbol)
e2)
    go (RAppTy RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RAppTy RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2) | UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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
(&&) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t11 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t21) (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Writer [(RTyVar, RTyVar)] Bool
go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t12 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t22)
    go (RRTy [(Symbol,
  RTypeBV
    Symbol
    Symbol
    RTyCon
    RTyVar
    (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_ Oblig
_ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r1) (RRTy [(Symbol,
  RTypeBV
    Symbol
    Symbol
    RTyCon
    RTyVar
    (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_ Oblig
_ RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r2)
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Bool
forall a. REq a => a -> a -> Bool
=*= RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r2)
    go (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1) (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
      = Bool -> Writer [(RTyVar, RTyVar)] Bool
forall a. a -> WriterT [(RTyVar, RTyVar)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r1 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
forall a. REq a => a -> a -> Bool
=*= UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2)
    go RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
_t1 RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
_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 ReftBV Symbol Symbol
r1 PredicateBV Symbol Symbol
p1) =*= :: UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> Bool
=*= (MkUReft ReftBV Symbol Symbol
r2 PredicateBV Symbol Symbol
p2)
     = ReftBV Symbol Symbol
r1 ReftBV Symbol Symbol -> ReftBV Symbol Symbol -> Bool
forall a. REq a => a -> a -> Bool
=*= ReftBV Symbol Symbol
r2 Bool -> Bool -> Bool
&& PredicateBV Symbol Symbol
p1 PredicateBV Symbol Symbol -> PredicateBV Symbol Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PredicateBV Symbol Symbol
p2

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

instance REq F.Expr where
  ExprBV Symbol Symbol
e1 =*= :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
=*= ExprBV Symbol Symbol
e2 = ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
forall {a}. (Fixpoint a, Eq a) => a -> a -> Bool
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Fixpoint a => a -> a
F.simplify ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Fixpoint a => a -> a
F.simplify ExprBV Symbol 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