{-# LANGUAGE FlexibleContexts #-}
module Language.Haskell.Liquid.LawInstances ( checkLawInstances ) where

import qualified Data.List                                  as L
import qualified Data.Maybe                                 as Mb
import           Text.PrettyPrint.HughesPJ                  hiding ((<>))

import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Types.Equality
import           Liquid.GHC.API            hiding ((<+>), text)
import qualified Language.Fixpoint.Types                    as F

checkLawInstances :: GhcSpecLaws -> Diagnostics
checkLawInstances :: GhcSpecLaws -> Diagnostics
checkLawInstances GhcSpecLaws
speclaws = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap LawInstance -> Diagnostics
go (GhcSpecLaws -> [LawInstance]
gsLawInst GhcSpecLaws
speclaws)
  where go :: LawInstance -> Diagnostics
go LawInstance
l = Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance (LawInstance -> Class
lilName LawInstance
l) (forall a. a -> Maybe a -> a
Mb.fromMaybe [] forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (LawInstance -> Class
lilName LawInstance
l) (GhcSpecLaws -> [(Class, [(Var, LocSpecType)])]
gsLawDefs GhcSpecLaws
speclaws)) LawInstance
l

checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance Class
c [(Var, LocSpecType)]
laws LawInstance
li
  = Class
-> LawInstance
-> [Var]
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> Diagnostics
checkExtra Class
c LawInstance
li ((forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, LocSpecType)]
laws) forall a. [a] -> [a] -> [a]
++ Class -> [Var]
classMethods Class
c) (LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li) forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Var, LocSpecType)
l -> Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw Class
c (Var, LocSpecType)
l LawInstance
li) [(Var, LocSpecType)]
laws

checkExtra :: Class
           -> LawInstance
           -> [Var]
           -> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
           -> Diagnostics
checkExtra :: Class
-> LawInstance
-> [Var]
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> Diagnostics
checkExtra Class
c LawInstance
li [Var]
_laws [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts =
    let allMsgs :: [Doc]
allMsgs = {- (msgExtra <$> extra) ++ -} (forall {a}. PPrint a => a -> Doc
msgUnfoundLaw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
unfoundLaws) forall a. [a] -> [a] -> [a]
++ (forall {a}. PPrint a => a -> Doc
msgUnfoundInstance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
unfoundInstances)
    in [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty (forall {t}. Doc -> TError t
mkError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
allMsgs)
    where
        unfoundInstances :: [LocSymbol]
unfoundInstances = [ LocSymbol
x | (VarOrLocSymbol
_, (Right LocSymbol
x,Maybe LocSpecType
_)) <- [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts]
        unfoundLaws :: [LocSymbol]
unfoundLaws = [ LocSymbol
x | (Right LocSymbol
x, (VarOrLocSymbol, Maybe LocSpecType)
_) <- [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts]
        _extra :: [a]
_extra = [] -- this breaks on extra super requirements [ (x,i) | (Left x, (Left i, _)) <- insts, not (x `L.elem` laws)] 
        mkError :: Doc -> TError t
mkError = forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrILaw (LawInstance -> SrcSpan
lilPos LawInstance
li) (forall {a}. PPrint a => a -> Doc
pprint Class
c) (forall {a}. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)
        _msgExtra :: (a, b) -> Doc
_msgExtra (a
x,b
_)      = forall {a}. PPrint a => a -> Doc
pprint a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined law."
        msgUnfoundLaw :: a -> Doc
msgUnfoundLaw a
i      = forall {a}. PPrint a => a -> Doc
pprint a
i Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined law."
        msgUnfoundInstance :: a -> Doc
msgUnfoundInstance a
i = forall {a}. PPrint a => a -> Doc
pprint a
i Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined instance."

checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw Class
c (Var
x, LocSpecType
t) LawInstance
li
  | Just (Left Var
_, Just LocSpecType
ti) <- Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix
  = (Doc -> Error)
-> Class
-> LawInstance
-> LocSpecType
-> LocSpecType
-> Diagnostics
unify forall {t}. Doc -> TError t
mkError Class
c LawInstance
li LocSpecType
t LocSpecType
ti
  | Just (Right LocSymbol
_l, Maybe LocSpecType
_) <- Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix
  = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [forall {t}. Doc -> TError t
mkError (String -> Doc
text String
"is not found.")]
  | Bool
otherwise
  = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [forall {t}. Doc -> TError t
mkError (String -> Doc
text String
"is not defined.")]
  where
    lix :: Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix = forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (forall a b. a -> Either a b
Left Var
x) (LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li)
    mkError :: Doc -> TError t
mkError Doc
txt = forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrILaw (LawInstance -> SrcSpan
lilPos LawInstance
li) (forall {a}. PPrint a => a -> Doc
pprint Class
c) (forall {a}. PPrint a => [a] -> Doc
pprintXs forall a b. (a -> b) -> a -> b
$ LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)
                          (String -> Doc
text String
"The instance for the law" Doc -> Doc -> Doc
<+> forall {a}. PPrint a => a -> Doc
pprint Var
x Doc -> Doc -> Doc
<+> Doc
txt)
    pprintXs :: [a] -> Doc
pprintXs [a
l] = forall {a}. PPrint a => a -> Doc
pprint a
l
    pprintXs [a]
xs  = forall {a}. PPrint a => a -> Doc
pprint [a]
xs

unify :: (Doc -> Error) -> Class -> LawInstance -> LocSpecType -> LocSpecType -> Diagnostics
unify :: (Doc -> Error)
-> Class
-> LawInstance
-> LocSpecType
-> LocSpecType
-> Diagnostics
unify Doc -> Error
mkError Class
c LawInstance
li LocSpecType
t1 LocSpecType
t2
  = if RType RTyCon RTyVar (UReft Reft)
t11 forall a. REq a => a -> a -> Bool
=*= RType RTyCon RTyVar (UReft Reft)
t22 then Diagnostics
emptyDiagnostics else Diagnostics
err
  where
    err :: Diagnostics
err = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [Doc -> Error
mkError (String -> Doc
text String
"is invalid:\nType" Doc -> Doc -> Doc
<+> forall {a}. PPrint a => a -> Doc
pprint LocSpecType
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"\nis different than\n" Doc -> Doc -> Doc
<+> forall {a}. PPrint a => a -> Doc
pprint LocSpecType
t2
       --  text "\nesubt1 = " <+> pprint esubst1  
       -- text "\nesubt = " <+> pprint esubst  
       -- text "\ncompared\n" <+> pprint t11 <+> text "\nWITH\n" <+> pprint t22 
           )]

    t22 :: RType RTyCon RTyVar (UReft Reft)
t22 = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar (UReft Reft)
trep2 {ty_vars :: [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
ty_vars = [], ty_binds :: [Symbol]
ty_binds = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args2, ty_args :: [RType RTyCon RTyVar (UReft Reft)]
ty_args = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args2, ty_refts :: [UReft Reft]
ty_refts = forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar (UReft Reft))]
tc2) (forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar (UReft Reft)
trep2)})
    t11 :: RType RTyCon RTyVar (UReft Reft)
t11 = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar (UReft Reft)
trep1 { ty_vars :: [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
ty_vars = []
                              , ty_binds :: [Symbol]
ty_binds = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args2
                              , ty_args :: [RType RTyCon RTyVar (UReft Reft)]
ty_args = RType RTyCon RTyVar (UReft Reft)
-> RType RTyCon RTyVar (UReft Reft)
tx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args1
                              , ty_refts :: [UReft Reft]
ty_refts = forall a. Subable a => Subst -> a -> a
F.subst Subst
esubst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar (UReft Reft))]
tc1) (forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar (UReft Reft)
trep1)
                              , ty_res :: RType RTyCon RTyVar (UReft Reft)
ty_res = RType RTyCon RTyVar (UReft Reft)
-> RType RTyCon RTyVar (UReft Reft)
tx forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar (UReft Reft)
trep1})
    tx :: RType RTyCon RTyVar (UReft Reft)
-> RType RTyCon RTyVar (UReft Reft)
tx = [(Var, Type)]
-> RType RTyCon RTyVar (UReft Reft)
-> RType RTyCon RTyVar (UReft Reft)
subtsSpec [(Var, Type)]
tsubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => Subst -> a -> a
F.subst Subst
esubst
    subtsSpec :: [(Var, Type)]
-> RType RTyCon RTyVar (UReft Reft)
-> RType RTyCon RTyVar (UReft Reft)
subtsSpec = forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts :: ([(TyVar, Type)] -> SpecType -> SpecType)

    trep1 :: RTypeRep RTyCon RTyVar (UReft Reft)
trep1 = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t1 
    trep2 :: RTypeRep RTyCon RTyVar (UReft Reft)
trep2 = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t2 
    ([(Symbol, RType RTyCon RTyVar (UReft Reft))]
tc1, [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args1) = [(Symbol, RType RTyCon RTyVar (UReft Reft))]
-> ([(Symbol, RType RTyCon RTyVar (UReft Reft))],
    [(Symbol, RType RTyCon RTyVar (UReft Reft))])
splitTypeConstraints forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar (UReft Reft)
trep1) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep1)
    ([(Symbol, RType RTyCon RTyVar (UReft Reft))]
tc2, [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args2) = [(Symbol, RType RTyCon RTyVar (UReft Reft))]
-> ([(Symbol, RType RTyCon RTyVar (UReft Reft))],
    [(Symbol, RType RTyCon RTyVar (UReft Reft))])
splitTypeConstraints forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar (UReft Reft)
trep2) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep2)
    esubst :: Subst
esubst = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)]
esubst1
                 forall a. [a] -> [a] -> [a]
++  [(forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Symbol -> Expr
F.EVar (forall a. Symbolic a => a -> Symbol
F.symbol Var
y)) | (Left Var
x, (Left Var
y, Maybe LocSpecType
_)) <- LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li]
                     )
    esubst1 :: [(Symbol, Expr)]
esubst1 = forall a b. [a] -> [b] -> [(a, b)]
zip  (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args1) (Symbol -> Expr
F.EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar (UReft Reft))]
args2)

    tsubst :: [(Var, Type)]
tsubst = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip ((\(RTV Var
v) -> Var
v) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {a} {a} {r}. [(a, RType RTyCon a r)] -> [a]
findTyVars [(Symbol, RType RTyCon RTyVar (UReft Reft))]
tc1 forall a. [a] -> [a] -> [a]
++ (forall tv s. RTVar tv s -> tv
ty_var_value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[RTVar RTyVar (RType RTyCon RTyVar ())]]
argVars)))
                 (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([RType RTyCon RTyVar (UReft Reft)]
argBds forall a. [a] -> [a] -> [a]
++ ((forall c tv r. tv -> r -> RType c tv r
`RVar` forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv s. RTVar tv s -> tv
ty_var_value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars RTypeRep RTyCon RTyVar (UReft Reft)
trep2))))

    ([[RTVar RTyVar (RType RTyCon RTyVar ())]]
argVars, [RType RTyCon RTyVar (UReft Reft)]
argBds) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall {c} {tv} {r}.
[RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)

    splitForall :: [RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall [RTVU c tv]
vs (RAllT RTVU c tv
v RType c tv r
t r
_) = [RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall (RTVU c tv
vforall a. a -> [a] -> [a]
:[RTVU c tv]
vs) RType c tv r
t 
    splitForall [RTVU c tv]
vs  RType c tv r
t            = ([RTVU c tv]
vs, RType c tv r
t) 

    findTyVars :: [(a, RType RTyCon a r)] -> [a]
findTyVars (((a
_x, RApp RTyCon
cc [RType RTyCon a r]
as [RTProp RTyCon a r]
_ r
_):[(a, RType RTyCon a r)]
_ts)) | RTyCon -> TyCon
rtc_tc RTyCon
cc forall a. Eq a => a -> a -> Bool
== Class -> TyCon
classTyCon Class
c 
      = [a
v | RVar a
v r
_ <- [RType RTyCon a r]
as ]
    findTyVars ((a, RType RTyCon a r)
_:[(a, RType RTyCon a r)]
ts) = [(a, RType RTyCon a r)] -> [a]
findTyVars [(a, RType RTyCon a r)]
ts 
    findTyVars [] = [] 


splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
splitTypeConstraints :: [(Symbol, RType RTyCon RTyVar (UReft Reft))]
-> ([(Symbol, RType RTyCon RTyVar (UReft Reft))],
    [(Symbol, RType RTyCon RTyVar (UReft Reft))])
splitTypeConstraints = forall {c} {f :: * -> *} {tv}.
(TyConable c, Reftable (f Reft), Functor f) =>
[(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go []  
  where  
    go :: [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go [(Symbol, RType c tv (f Reft))]
cs (b :: (Symbol, RType c tv (f Reft))
b@(Symbol
_x, RApp c
c [RType c tv (f Reft)]
_ [RTProp c tv (f Reft)]
_ f Reft
_):[(Symbol, RType c tv (f Reft))]
ts) 
      | forall c. TyConable c => c -> Bool
isClass c
c
      = [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go ((Symbol, RType c tv (f Reft))
bforall a. a -> [a] -> [a]
:[(Symbol, RType c tv (f Reft))]
cs) [(Symbol, RType c tv (f Reft))]
ts 
    go [(Symbol, RType c tv (f Reft))]
cs [(Symbol, RType c tv (f Reft))]
r = (forall a. [a] -> [a]
reverse [(Symbol, RType c tv (f Reft))]
cs, forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
x, RType c tv (f Reft)
t) -> (Symbol
x, forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV RType c tv (f Reft)
t Symbol
x)) [(Symbol, RType c tv (f Reft))]
r)