|
| 1 | +{-# LANGUAGE FlexibleContexts #-} |
| 2 | +module Language.Haskell.Liquid.LawInstances ( checkLawInstances ) where |
| 3 | + |
| 4 | +import qualified Data.List as L |
| 5 | +import qualified Data.Maybe as Mb |
| 6 | +import Text.PrettyPrint.HughesPJ |
| 7 | + |
| 8 | +import Language.Haskell.Liquid.Types |
| 9 | +import Language.Haskell.Liquid.Types.Equality |
| 10 | +import Language.Haskell.Liquid.GHC.API |
| 11 | +import qualified Language.Fixpoint.Types as F |
| 12 | + |
| 13 | +checkLawInstances :: GhcSpecLaws -> [Error] |
| 14 | +checkLawInstances speclaws = concatMap go (gsLawInst speclaws) |
| 15 | + where go l = checkOneInstance (lilName l) (Mb.fromMaybe [] $ L.lookup (lilName l) (gsLawDefs speclaws)) l |
| 16 | + |
| 17 | +checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> [Error] |
| 18 | +checkOneInstance c laws li |
| 19 | + = checkExtra c li ((fst <$> laws) ++ classMethods c) (lilEqus li) ++ concatMap (\l -> checkOneLaw c l li) laws |
| 20 | + |
| 21 | +checkExtra :: Class -> LawInstance -> [Var] -> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))] -> [Error] |
| 22 | +checkExtra c li laws insts = mkError <$> ({- (msgExtra <$> extra) ++ -} (msgUnfoundLaw <$> unfoundLaws) ++ (msgUnfoundInstance <$> unfoundInstances)) |
| 23 | + where |
| 24 | + |
| 25 | + unfoundInstances = [ x | (_, (Right x,_)) <- insts] |
| 26 | + unfoundLaws = [ x | (Right x, _) <- insts] |
| 27 | + extra = [] -- this breaks on extra super requirements [ (x,i) | (Left x, (Left i, _)) <- insts, not (x `L.elem` laws)] |
| 28 | + mkError = ErrILaw (lilPos li) (pprint c) (pprint $ lilTyArgs li) |
| 29 | + msgExtra (x,_) = pprint x <+> text "is not a defined law." |
| 30 | + msgUnfoundLaw i = pprint i <+> text "is not a defined law." |
| 31 | + msgUnfoundInstance i = pprint i <+> text "is not a defined instance." |
| 32 | + |
| 33 | +checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> [Error] |
| 34 | +checkOneLaw c (x, t) li |
| 35 | + | Just (Left _, Just ti) <- lix |
| 36 | + = unify mkError c li t ti |
| 37 | + | Just (Right l, _) <- lix |
| 38 | + = [mkError (text "is not found.")] |
| 39 | + | otherwise |
| 40 | + = [mkError (text "is not defined.")] |
| 41 | + where |
| 42 | + lix = L.lookup (Left x) (lilEqus li) |
| 43 | + mkError txt = ErrILaw (lilPos li) (pprint c) (pprintXs $ lilTyArgs li) |
| 44 | + (text "The instance for the law" <+> pprint x <+> txt) |
| 45 | + pprintXs [l] = pprint l |
| 46 | + pprintXs xs = pprint xs |
| 47 | + |
| 48 | +unify :: (Doc -> Error) -> Class -> LawInstance -> LocSpecType -> LocSpecType -> [Error] |
| 49 | +unify mkError c li t1 t2 |
| 50 | + = if t11 =*= t22 then [] else err |
| 51 | + where |
| 52 | + err = [mkError (text "is invalid:\nType" <+> pprint t1 <+> text "\nis different than\n" <+> pprint t2 |
| 53 | + -- <+> text "\nesubt1 = " <+> pprint esubst1 |
| 54 | + -- <+> text "\nesubt = " <+> pprint esubst |
| 55 | + -- <+> text "\ncompared\n" <+> pprint t11 <+> text "\nWITH\n" <+> pprint t22 |
| 56 | + )] |
| 57 | + |
| 58 | + t22 = fromRTypeRep (trep2 {ty_vars = [], ty_binds = fst <$> args2, ty_args = snd <$> args2, ty_refts = drop (length tc2) (ty_refts trep2)}) |
| 59 | + t11 = fromRTypeRep (trep1 { ty_vars = [] |
| 60 | + , ty_binds = fst <$> args2 |
| 61 | + , ty_args = (tx . snd) <$> args1 |
| 62 | + , ty_refts = F.subst esubst <$> drop (length tc1) (ty_refts trep1) |
| 63 | + , ty_res = tx $ ty_res trep1}) |
| 64 | + tx = subtsSpec tsubst . F.subst esubst |
| 65 | + subtsSpec = subts :: ([(TyVar, Type)] -> SpecType -> SpecType) |
| 66 | + |
| 67 | + trep1 = toRTypeRep $ val t1 |
| 68 | + trep2 = toRTypeRep $ val t2 |
| 69 | + (tc1, args1) = splitTypeConstraints $ zip (ty_binds trep1) (ty_args trep1) |
| 70 | + (tc2, args2) = splitTypeConstraints $ zip (ty_binds trep2) (ty_args trep2) |
| 71 | + esubst = F.mkSubst (esubst1 |
| 72 | + ++ [(F.symbol x, F.EVar (F.symbol y)) | (Left x, (Left y, _)) <- lilEqus li] |
| 73 | + ) |
| 74 | + esubst1 = zip (fst <$> args1) ((F.EVar . fst) <$> args2) |
| 75 | + |
| 76 | + tsubst = reverse $ zip ((\(RTV v) -> v) <$> (findTyVars tc1 ++ (ty_var_value <$> concat argVars))) |
| 77 | + (toType <$> (argBds ++ (((`RVar` mempty) . ty_var_value) <$>ty_vars trep2))) |
| 78 | + |
| 79 | + (argVars, argBds) = unzip (splitForall [] . val <$> lilTyArgs li) |
| 80 | + |
| 81 | + splitForall vs (RAllT v t) = splitForall (v:vs) t |
| 82 | + splitForall vs t = (vs, t) |
| 83 | + |
| 84 | + findTyVars ((b@(x,RApp cc as _ _):ts)) | rtc_tc cc == classTyCon c |
| 85 | + = [v | RVar v _ <- as ] |
| 86 | + findTyVars (_:ts) = findTyVars ts |
| 87 | + findTyVars [] = [] |
| 88 | + |
| 89 | + |
| 90 | +splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)]) |
| 91 | +splitTypeConstraints = go [] |
| 92 | + where |
| 93 | + go cs (b@(x,RApp c _ _ _):ts) |
| 94 | + | isClass c |
| 95 | + = go (b:cs) ts |
| 96 | + go cs r = (reverse cs, map (\(x, t) -> (x, shiftVV t x)) r) |
0 commit comments