LawInstances.hs

{-# 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 

import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Types.Equality
import           Language.Haskell.Liquid.GHC.API            
import qualified Language.Fixpoint.Types                     as F

checkLawInstances :: GhcSpecLaws -> [Error]    
checkLawInstances speclaws = concatMap go (gsLawInst speclaws) 
  where go l = checkOneInstance (lilName l) (Mb.fromMaybe [] $ L.lookup (lilName l) (gsLawDefs speclaws)) l 

checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> [Error]
checkOneInstance c laws li 
  = checkExtra c li ((fst <$> laws) ++ classMethods c) (lilEqus li) ++ concatMap (\l -> checkOneLaw c l li) laws

checkExtra :: Class  -> LawInstance -> [Var] -> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))] -> [Error]
checkExtra c li _laws insts = mkError <$> ({- (msgExtra <$> extra) ++ -}  (msgUnfoundLaw <$> unfoundLaws) ++ (msgUnfoundInstance <$> unfoundInstances))
    where 
        unfoundInstances = [ x | (_, (Right x,_)) <- insts] 
        unfoundLaws = [ x | (Right x, _) <- insts] 
        _extra = [] -- this breaks on extra super requirements [ (x,i) | (Left x, (Left i, _)) <- insts, not (x `L.elem` laws)] 
        mkError = ErrILaw (lilPos li) (pprint c) (pprint $ lilTyArgs li) 
        _msgExtra (x,_)      = pprint x <+> text "is not a defined law."
        msgUnfoundLaw i      = pprint i <+> text "is not a defined law."
        msgUnfoundInstance i = pprint i <+> text "is not a defined instance."

checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> [Error]
checkOneLaw c (x, t) li 
  | Just (Left _, Just ti) <- lix 
  = unify mkError c li t ti
  | Just (Right _l, _) <- lix
  = [mkError (text "is not found.")]
  | otherwise
  = [mkError (text "is not defined.")]
  where 
    lix = L.lookup (Left x) (lilEqus li)
    mkError txt = ErrILaw (lilPos li) (pprint c) (pprintXs $ lilTyArgs li)
                          (text "The instance for the law" <+> pprint x <+> txt)
    pprintXs [l] = pprint l 
    pprintXs xs  = pprint xs 

unify :: (Doc -> Error) -> Class -> LawInstance -> LocSpecType -> LocSpecType -> [Error]
unify mkError c li t1 t2 
  = if t11 =*= t22 then [] else err
  where 
    err = [mkError (text "is invalid:\nType" <+> pprint t1 <+> text "\nis different than\n" <+> pprint t2
       --  text "\nesubt1 = " <+> pprint esubst1  
       -- text "\nesubt = " <+> pprint esubst  
       -- text "\ncompared\n" <+> pprint t11 <+> text "\nWITH\n" <+> pprint t22 
           )]

    t22 = fromRTypeRep (trep2 {ty_vars = [], ty_binds = fst <$> args2, ty_args = snd <$> args2, ty_refts = drop (length tc2) (ty_refts trep2)})
    t11 = fromRTypeRep (trep1 { ty_vars = []
                              , ty_binds = fst <$> args2
                              , ty_args = (tx . snd) <$> args1
                              , ty_refts = F.subst esubst <$> drop (length tc1) (ty_refts trep1)
                              , ty_res = tx $ ty_res trep1})
    tx = subtsSpec tsubst . F.subst esubst
    subtsSpec = subts :: ([(TyVar, Type)] -> SpecType -> SpecType)

    trep1 = toRTypeRep $ val t1 
    trep2 = toRTypeRep $ val t2 
    (tc1, args1) = splitTypeConstraints $ zip (ty_binds trep1) (ty_args trep1)
    (tc2, args2) = splitTypeConstraints $ zip (ty_binds trep2) (ty_args trep2)
    esubst = F.mkSubst (esubst1
                 ++  [(F.symbol x, F.EVar (F.symbol y)) | (Left x, (Left y, _)) <- lilEqus li]
                     )
    esubst1 = zip  (fst <$> args1) ((F.EVar . fst) <$> args2)

    tsubst = reverse $ zip ((\(RTV v) -> v) <$> (findTyVars tc1 ++ (ty_var_value <$> concat argVars)))
                 (toType <$> (argBds ++ (((`RVar` mempty) . ty_var_value) <$>ty_vars trep2)))

    (argVars, argBds) = unzip (splitForall [] . val <$> lilTyArgs li)

    splitForall vs (RAllT v t) = splitForall (v:vs) t 
    splitForall vs  t           = (vs, t) 

    findTyVars (((_x, RApp cc as _ _):_ts)) | rtc_tc cc == classTyCon c 
      = [v | RVar v _ <- as ]
    findTyVars (_:ts) = findTyVars ts 
    findTyVars [] = [] 


splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
splitTypeConstraints = go []  
  where  
    go cs (b@(_x, RApp c _ _ _):ts) 
      | isClass c
      = go (b:cs) ts 
    go cs r = (reverse cs, map (\(x, t) -> (x, shiftVV t x)) r)