{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Bare.Check ( checkTargetSpec , checkBareSpec , checkTargetSrc ) where import Language.Haskell.Liquid.Constraint.ToFixpoint import Liquid.GHC.API as Ghc hiding ( Located , text , (<+>) , panic , ($+$) , empty ) import Control.Applicative ((<|>)) import Control.Arrow ((&&&)) import Data.Maybe import Data.Function (on) import Text.PrettyPrint.HughesPJ hiding ((<>)) import qualified Data.List as L import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import Data.Hashable import qualified Language.Fixpoint.Misc as Misc import Language.Fixpoint.SortCheck (checkSorted, checkSortedReftFull, checkSortFull) import qualified Language.Fixpoint.Types as F import qualified Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.GHC.Play (getNonPositivesTyCon) import Language.Haskell.Liquid.Misc (condNull, thd5) import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.WiredIn import Language.Haskell.Liquid.LawInstances (checkLawInstances) import qualified Language.Haskell.Liquid.Measure as Ms import qualified Language.Haskell.Liquid.Bare.Types as Bare import qualified Language.Haskell.Liquid.Bare.Resolve as Bare ---------------------------------------------------------------------------------------------- -- | Checking TargetSrc ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics () checkTargetSrc cfg spec | nopositivity cfg || nopositives == emptyDiagnostics = Right () | otherwise = Left nopositives where nopositives = checkPositives (gsTcs spec) checkPositives :: [TyCon] -> Diagnostics checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys) mkNonPosError :: [(TyCon, [DataCon])] -> [Error] mkNonPosError tcs = [ ErrPosTyCon (getSrcSpan tc) (pprint tc) (pprint dc <+> ":" <+> pprint (dataConRepType dc)) | (tc, dc:_) <- tcs] ---------------------------------------------------------------------------------------------- -- | Checking BareSpec ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- checkBareSpec :: ModName -> Ms.BareSpec -> Either Diagnostics () checkBareSpec _ sp | allChecks == emptyDiagnostics = Right () | otherwise = Left allChecks where allChecks = mconcat [ checkUnique "measure" measures , checkUnique "field" fields , checkDisjoints [ inlines , hmeasures , S.fromList measures , reflects , S.fromList fields ] ] inlines = Ms.inlines sp hmeasures = Ms.hmeas sp reflects = Ms.reflects sp measures = msName <$> Ms.measures sp fields = concatMap dataDeclFields (Ms.dataDecls sp) dataDeclFields :: DataDecl -> [F.LocSymbol] dataDeclFields = filter (not . GM.isTmpSymbol . F.val) . Misc.hashNubWith val . concatMap dataCtorFields . fromMaybe [] . tycDCons dataCtorFields :: DataCtor -> [F.LocSymbol] dataCtorFields c | isGadt c = [] | otherwise = F.atLoc c <$> [ f | (f,_) <- dcFields c ] isGadt :: DataCtor -> Bool isGadt = isJust . dcResult checkUnique :: String -> [F.LocSymbol] -> Diagnostics checkUnique _ = mkDiagnostics mempty . checkUnique' F.val GM.fSrcSpan checkUnique' :: (PPrint a, Eq a, Hashable a) => (t -> a) -> (t -> Ghc.SrcSpan) -> [t] -> [Error] checkUnique' nameF locF ts = [ErrDupSpecs l (pprint n) ls | (n, ls@(l:_)) <- dups] where dups = [ z | z@(_, _:_:_) <- Misc.groupList nts ] nts = [ (n, l) | t <- ts, let n = nameF t, let l = locF t ] checkDisjoints :: [S.HashSet F.LocSymbol] -> Diagnostics checkDisjoints [] = emptyDiagnostics checkDisjoints [_] = emptyDiagnostics checkDisjoints (s:ss) = checkDisjoint s (S.unions ss) <> checkDisjoints ss checkDisjoint :: S.HashSet F.LocSymbol -> S.HashSet F.LocSymbol -> Diagnostics checkDisjoint s1 s2 = checkUnique "disjoint" (S.toList s1 ++ S.toList s2) ---------------------------------------------------------------------------------------------- -- | Checking TargetSpec ---------------------------------------------------------------------------------------------- checkTargetSpec :: [Ms.BareSpec] -> TargetSrc -> F.SEnv F.SortedReft -> [CoreBind] -> TargetSpec -> Either Diagnostics () checkTargetSpec specs src env cbs tsp | diagnostics == emptyDiagnostics = Right () | otherwise = Left diagnostics where diagnostics :: Diagnostics diagnostics = foldMap (checkBind allowHO bsc "measure" emb tcEnv env) (gsMeas (gsData tsp)) <> condNull noPrune (foldMap (checkBind allowHO bsc "constructor" emb tcEnv env) (txCtors $ gsCtors (gsData tsp))) <> foldMap (checkBind allowHO bsc "assume" emb tcEnv env) (gsAsmSigs (gsSig tsp)) <> foldMap (checkBind allowHO bsc "reflect" emb tcEnv env . (\sig@(_,s) -> F.notracepp (show (ty_info (toRTypeRep (F.val s)))) sig)) (gsRefSigs (gsSig tsp)) <> checkTySigs allowHO bsc cbs emb tcEnv env (gsSig tsp) -- ++ mapMaybe (checkTerminationExpr emb env) (gsTexprs (gsSig sp)) <> foldMap (checkBind allowHO bsc "class method" emb tcEnv env) (clsSigs (gsSig tsp)) <> foldMap (checkInv allowHO bsc emb tcEnv env) (gsInvariants (gsData tsp)) <> checkIAl allowHO bsc emb tcEnv env (gsIaliases (gsData tsp)) <> checkMeasures emb env ms <> checkClassMeasures (gsMeasures (gsData tsp)) <> checkClassMethods (gsCls src) (gsCMethods (gsVars tsp)) (gsTySigs (gsSig tsp)) -- <> foldMap checkMismatch sigs <> foldMap checkMismatch (L.filter (\(v,_) -> not (GM.isSCSel v || GM.isMethod v)) sigs) <> checkDuplicate (gsTySigs (gsSig tsp)) -- TODO-REBARE ++ checkQualifiers env (gsQualifiers (gsQual sp)) <> checkDuplicate (gsAsmSigs (gsSig tsp)) <> checkDupIntersect (gsTySigs (gsSig tsp)) (gsAsmSigs (gsSig tsp)) <> checkRTAliases "Type Alias" env tAliases <> checkRTAliases "Pred Alias" env eAliases -- ++ _checkDuplicateFieldNames (gsDconsP sp) -- NV TODO: allow instances of refined classes to be refined -- but make sure that all the specs are checked. -- ++ checkRefinedClasses rClasses rInsts <> checkSizeFun emb env (gsTconsP (gsName tsp)) <> checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig tsp) ]) <> checkLawInstances (gsLaws tsp) <> checkRewrites tsp _rClasses = concatMap Ms.classes specs _rInsts = concatMap Ms.rinstance specs tAliases = concat [Ms.aliases sp | sp <- specs] eAliases = concat [Ms.ealiases sp | sp <- specs] emb = gsTcEmbeds (gsName tsp) tcEnv = gsTyconEnv (gsName tsp) ms = gsMeasures (gsData tsp) clsSigs sp = [ (v, t) | (v, t) <- gsTySigs sp, isJust (isClassOpId_maybe v) ] sigs = gsTySigs (gsSig tsp) ++ gsAsmSigs (gsSig tsp) ++ gsCtors (gsData tsp) -- allowTC = typeclass (getConfig sp) allowHO = higherOrderFlag tsp bsc = bscope (getConfig tsp) noPrune = not (pruneFlag tsp) txCtors ts = [(v, fmap (fmap (fmap (F.filterUnMatched temps))) t) | (v, t) <- ts] temps = F.makeTemplates $ gsUnsorted $ gsData tsp -- env' = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms checkPlugged :: PPrint v => [(v, LocSpecType)] -> Diagnostics checkPlugged xs = mkDiagnostics mempty (map mkError (filter (hasHoleTy . val . snd) xs)) where mkError (x,t) = ErrBadData (GM.sourcePosSrcSpan $ loc t) (pprint x) msg msg = "Cannot resolve type hole `_`. Use explicit type instead." -------------------------------------------------------------------------------- checkTySigs :: Bool -> BScope -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> GhcSpecSig -> Diagnostics -------------------------------------------------------------------------------- checkTySigs allowHO bsc cbs emb tcEnv senv sig = mconcat (map (check senv) topTs) -- = concatMap (check env) topTs -- (mapMaybe (checkT env) [ (x, t) | (x, (t, _)) <- topTs]) -- ++ (mapMaybe (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs]) <> coreVisitor checkVisitor senv emptyDiagnostics cbs -- ++ coreVisitor checkVisitor env [] cbs where check env = checkSigTExpr allowHO bsc emb tcEnv env locTm = M.fromList locTs (locTs, topTs) = Bare.partitionLocalBinds vtes vtes = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs] vExprs = M.fromList [ (x, es) | (x, _, es) <- gsTexprs sig ] checkVisitor :: CoreVisitor (F.SEnv F.SortedReft) Diagnostics checkVisitor = CoreVisitor { envF = \env v -> F.insertSEnv (F.symbol v) (vSort v) env , bindF = \env acc v -> errs env v <> acc , exprF = \_ acc _ -> acc } vSort = Bare.varSortedReft emb errs env v = case M.lookup v locTm of Nothing -> emptyDiagnostics Just t -> check env (v, t) checkSigTExpr :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Var, (LocSpecType, Maybe [Located F.Expr])) -> Diagnostics checkSigTExpr allowHO bsc emb tcEnv env (x, (t, es)) = mbErr1 <> mbErr2 where mbErr1 = checkBind allowHO bsc empty emb tcEnv env (x, t) mbErr2 = maybe emptyDiagnostics (checkTerminationExpr emb env . (x, t,)) es -- mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es _checkQualifiers :: F.SEnv F.SortedReft -> [F.Qualifier] -> [Error] _checkQualifiers = mapMaybe . checkQualifier checkQualifier :: F.SEnv F.SortedReft -> F.Qualifier -> Maybe Error checkQualifier env q = mkE <$> checkSortFull (F.srcSpan q) γ F.boolSort (F.qBody q) where γ = L.foldl' (\e (x, s) -> F.insertSEnv x (F.RR s mempty) e) env (F.qualBinds q ++ wiredSortedSyms) mkE = ErrBadQual (GM.fSrcSpan q) (pprint $ F.qName q) -- | Used for termination checking. If we have no \"len\" defined /yet/ (for example we are checking -- 'GHC.Prim') then we want to skip this check. checkSizeFun :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [TyConP] -> Diagnostics checkSizeFun emb env tys = mkDiagnostics mempty (map mkError (mapMaybe go tys)) where mkError ((f, tcp), msg) = ErrTyCon (GM.sourcePosSrcSpan $ tcpLoc tcp) (text "Size function" <+> pprint (f x) <+> text "should have type int, but it was " <+> pprint (tcpCon tcp) <+> text "." $+$ msg) (pprint (tcpCon tcp)) go tcp = case tcpSizeFun tcp of Nothing -> Nothing Just f | isWiredInLenFn f -> Nothing -- Skip the check. Just f -> checkWFSize (szFun f) tcp checkWFSize f tcp = ((f, tcp),) <$> checkSortFull (F.srcSpan tcp) (F.insertSEnv x (mkTySort (tcpCon tcp)) env) F.intSort (f x) x = "x" :: F.Symbol mkTySort tc = rTypeSortedReft emb (ofType $ TyConApp tc (TyVarTy <$> tyConTyVars tc) :: RRType ()) isWiredInLenFn :: SizeFun -> Bool isWiredInLenFn IdSizeFun = False isWiredInLenFn (SymSizeFun locSym) = isWiredIn locSym _checkRefinedClasses :: [RClass LocBareType] -> [RInstance LocBareType] -> [Error] _checkRefinedClasses definitions instances = mkError <$> duplicates where duplicates = mapMaybe (checkCls . rcName) definitions checkCls cls = case findConflicts cls of [] -> Nothing conflicts -> Just (cls, conflicts) findConflicts cls = filter ((== cls) . riclass) instances mkError (cls, conflicts) = ErrRClass (GM.sourcePosSrcSpan $ loc $ btc_tc cls) (pprint cls) (ofConflict <$> conflicts) ofConflict = GM.sourcePosSrcSpan . loc . btc_tc . riclass &&& pprint . ritype _checkDuplicateFieldNames :: [(DataCon, DataConP)] -> [Error] _checkDuplicateFieldNames = mapMaybe go where go (d, dts) = checkNoDups (dcpLoc dts) d (fst <$> dcpTyArgs dts) checkNoDups l d xs = mkError l d <$> _firstDuplicate xs mkError l d x = ErrBadData (GM.sourcePosSrcSpan l) (pprint d) (text "Multiple declarations of record selector" <+> pprintSymbol x) _firstDuplicate :: Ord a => [a] -> Maybe a _firstDuplicate = go . L.sort where go (y:x:xs) | x == y = Just x | otherwise = go (x:xs) go _ = Nothing checkInv :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Diagnostics checkInv allowHO bsc emb tcEnv env (_, t) = checkTy allowHO bsc err emb tcEnv env t where err = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t) checkIAl :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> Diagnostics checkIAl allowHO bsc emb tcEnv env = mconcat . map (checkIAlOne allowHO bsc emb tcEnv env) checkIAlOne :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (LocSpecType, LocSpecType) -> Diagnostics checkIAlOne allowHO bsc emb tcEnv env (t1, t2) = mconcat $ checkEq : (tcheck <$> [t1, t2]) where tcheck t = checkTy allowHO bsc (err t) emb tcEnv env t err t = ErrIAl (GM.sourcePosSrcSpan $ loc t) (val t) t1' :: RSort t1' = toRSort $ val t1 t2' :: RSort t2' = toRSort $ val t2 checkEq = if t1' == t2' then emptyDiagnostics else mkDiagnostics mempty [errmis] errmis = ErrIAlMis (GM.sourcePosSrcSpan $ loc t1) (val t1) (val t2) emsg emsg = pprint t1 <+> text "does not match with" <+> pprint t2 -- FIXME: Should _ be removed if it isn't used? checkRTAliases :: String -> t -> [Located (RTAlias s a)] -> Diagnostics checkRTAliases msg _ as = err1s where err1s = checkDuplicateRTAlias msg as checkBind :: (PPrint v) => Bool -> BScope -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Diagnostics checkBind allowHO bsc s emb tcEnv env (v, t) = checkTy allowHO bsc msg emb tcEnv env t where msg = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t) checkTerminationExpr :: (Eq v, PPrint v) => F.TCEmb TyCon -> F.SEnv F.SortedReft -> (v, LocSpecType, [F.Located F.Expr]) -> Diagnostics checkTerminationExpr emb env (v, Loc l _ st, les) = mkError "ill-sorted" (go les) <> mkError "non-numeric" (go' les) where -- es = val <$> les mkError :: Doc -> Maybe (F.Expr, Doc) -> Diagnostics mkError _ Nothing = emptyDiagnostics mkError k (Just expr') = mkDiagnostics mempty [(\ (e, d) -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) k e st d) expr'] -- mkErr = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d) -- mkErr' = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d) go :: [F.Located F.Expr] -> Maybe (F.Expr, Doc) go = L.foldl' (\err e -> err <|> (val e,) <$> checkSorted (F.srcSpan e) env' (val e)) Nothing go' :: [F.Located F.Expr] -> Maybe (F.Expr, Doc) go' = L.foldl' (\err e -> err <|> (val e,) <$> checkSorted (F.srcSpan e) env' (cmpZero e)) Nothing env' = F.sr_sort <$> L.foldl' (\e (x,s) -> F.insertSEnv x s e) env xts xts = concatMap mkClss $ zip (ty_binds trep) (ty_args trep) trep = toRTypeRep st mkClss (_, RApp c ts _ _) | isClass c = classBinds emb (rRCls c ts) mkClss (x, t) = [(x, rSort t)] rSort = rTypeSortedReft emb cmpZero e = F.PAtom F.Le (F.expr (0 :: Int)) (val e) checkTy :: Bool -> BScope -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Diagnostics checkTy allowHO bsc mkE emb tcEnv env t = case checkRType allowHO bsc emb env (Bare.txRefSort tcEnv emb t) of Nothing -> emptyDiagnostics Just d -> mkDiagnostics mempty [mkE d] where _msg = "CHECKTY: " ++ showpp (val t) checkDupIntersect :: [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics checkDupIntersect xts asmSigs = mkDiagnostics (map mkWrn {- trace msg -} dups) mempty where mkWrn (x, t) = mkWarning (GM.sourcePosSrcSpan $ loc t) (pprWrn x) dups = L.intersectBy ((==) `on` fst) asmSigs xts pprWrn v = text $ "Assume Overwrites Specifications for " ++ show v -- msg = "CHECKDUPINTERSECT:" ++ msg1 ++ msg2 -- msg1 = "\nCheckd-SIGS:\n" ++ showpp (M.fromList xts) -- msg2 = "\nAssume-SIGS:\n" ++ showpp (M.fromList asmSigs) checkDuplicate :: [(Var, LocSpecType)] -> Diagnostics checkDuplicate = mkDiagnostics mempty . checkUnique' fst (GM.fSrcSpan . snd) checkClassMethods :: Maybe [ClsInst] -> [Var] -> [(Var, LocSpecType)] -> Diagnostics checkClassMethods Nothing _ _ = emptyDiagnostics checkClassMethods (Just clsis) cms xts = mkDiagnostics mempty [ErrMClass (GM.sourcePosSrcSpan $ loc t) (pprint x)| (x,t) <- dups ] where dups = F.notracepp "DPS" $ filter ((`elem` ms) . fst) xts' ms = F.notracepp "MS" $ concatMap (classMethods . is_cls) clsis xts' = F.notracepp "XTS" $ filter (not . (`elem` cls) . fst) xts cls = F.notracepp "CLS" cms checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> Diagnostics checkDuplicateRTAlias s tas = mkDiagnostics mempty (map mkError dups) where mkError xs@(x:_) = ErrDupAlias (GM.fSrcSpan x) (text s) (pprint . rtName . val $ x) (GM.fSrcSpan <$> xs) mkError [] = panic Nothing "mkError: called on empty list" dups = [z | z@(_:_:_) <- L.groupBy ((==) `on` (rtName . val)) tas] checkMismatch :: (Var, LocSpecType) -> Diagnostics checkMismatch (x, t) = if ok then emptyDiagnostics else mkDiagnostics mempty [err] where ok = tyCompat x (val t) err = errTypeMismatch x t tyCompat :: Var -> RType RTyCon RTyVar r -> Bool tyCompat x t = lqT == hsT where lqT :: RSort = toRSort t hsT :: RSort = ofType (varType x) _msg = "TY-COMPAT: " ++ GM.showPpr x ++ ": hs = " ++ F.showpp hsT ++ " :lq = " ++ F.showpp lqT errTypeMismatch :: Var -> Located SpecType -> Error errTypeMismatch x t = ErrMismatch lqSp (pprint x) (text "Checked") d1 d2 Nothing hsSp where d1 = pprint $ varType x d2 = pprint $ toType False $ val t lqSp = GM.fSrcSpan t hsSp = getSrcSpan x ------------------------------------------------------------------------------------------------ -- | @checkRType@ determines if a type is malformed in a given environment --------------------- ------------------------------------------------------------------------------------------------ checkRType :: Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc ------------------------------------------------------------------------------------------------ checkRType allowHO bsc emb senv lt = checkAppTys st <|> checkAbstractRefs st <|> efoldReft farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv senv Nothing st where -- isErasable = if allowTC then isEmbeddedDict else isClass st = val lt cb c ts = classBinds emb (rRCls c ts) farg _ t = allowHO || isBase t -- NOTE: this check should be the same as the one in addCGEnv f env me r err = err <|> checkReft (F.srcSpan lt) env emb me r insertPEnv p γ = insertsSEnv γ (Misc.mapSnd (rTypeSortedReft emb) <$> pbinds p) pbinds p = (pname p, pvarRType p :: RSort) : [(x, tx) | (tx, x, _) <- pargs p] tyToBind :: F.TCEmb TyCon -> RTVar RTyVar RSort -> [(F.Symbol, F.SortedReft)] tyToBind emb = go . ty_var_info where go RTVInfo{..} = [(rtv_name, rTypeSortedReft emb rtv_kind)] go RTVNoInfo{} = [] checkAppTys :: RType RTyCon t t1 -> Maybe Doc checkAppTys = go where go (RAllT _ t _) = go t go (RAllP _ t) = go t go (RApp rtc ts _ _) = checkTcArity rtc (length ts) <|> L.foldl' (\merr t -> merr <|> go t) Nothing ts go (RFun _ _ t1 t2 _) = go t1 <|> go t2 go (RVar _ _) = Nothing go (RAllE _ t1 t2) = go t1 <|> go t2 go (REx _ t1 t2) = go t1 <|> go t2 go (RAppTy t1 t2 _) = go t1 <|> go t2 go (RRTy _ _ _ t) = go t go (RExprArg _) = Just $ text "Logical expressions cannot appear inside a Haskell type" go (RHole _) = Nothing checkTcArity :: RTyCon -> Arity -> Maybe Doc checkTcArity RTyCon{ rtc_tc = tc } givenArity | expectedArity < givenArity = Just $ text "Type constructor" <+> pprint tc <+> text "expects a maximum" <+> pprint expectedArity <+> text "arguments but was given" <+> pprint givenArity <+> text "arguments" | otherwise = Nothing where expectedArity = tyConRealArity tc checkAbstractRefs :: (PPrint t, F.Reftable t, SubsTy RTyVar RSort t, F.Reftable (RTProp RTyCon RTyVar (UReft t))) => RType RTyCon RTyVar (UReft t) -> Maybe Doc checkAbstractRefs rt = go rt where penv = mkPEnv rt go t@(RAllT _ t1 r) = check (toRSort t :: RSort) r <|> go t1 go (RAllP _ t) = go t go t@(RApp c ts rs r) = check (toRSort t :: RSort) r <|> efold go ts <|> go' c rs go t@(RFun _ _ t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2 go t@(RVar _ r) = check (toRSort t :: RSort) r go (RAllE _ t1 t2) = go t1 <|> go t2 go (REx _ t1 t2) = go t1 <|> go t2 go t@(RAppTy t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2 go (RRTy xts _ _ t) = efold go (snd <$> xts) <|> go t go (RExprArg _) = Nothing go (RHole _) = Nothing go' c rs = L.foldl' (\acc (x, y) -> acc <|> checkOne' x y) Nothing (zip rs (rTyConPVs c)) checkOne' (RProp xs (RHole _)) p | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)] = Just $ text "Wrong Arguments in" <+> pprint p | length xs /= length (pargs p) = Just $ text "Wrong Number of Arguments in" <+> pprint p | otherwise = Nothing checkOne' (RProp xs t) p | pvType p /= toRSort t = Just $ text "Unexpected Sort in" <+> pprint p | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)] = Just $ text "Wrong Arguments in" <+> pprint p | length xs /= length (pargs p) = Just $ text "Wrong Number of Arguments in" <+> pprint p | otherwise = go t efold f = L.foldl' (\acc x -> acc <|> f x) Nothing check s (MkUReft _ (Pr ps)) = L.foldl' (\acc pp -> acc <|> checkOne s pp) Nothing ps checkOne s p | pvType' p /= s = Just $ text "Incorrect Sort:\n\t" <+> text "Abstract refinement with type" <+> pprint (pvType' p) <+> text "is applied to" <+> pprint s <+> text "\n\t In" <+> pprint p | otherwise = Nothing mkPEnv (RAllT _ t _) = mkPEnv t mkPEnv (RAllP p t) = p:mkPEnv t mkPEnv _ = [] pvType' p = Misc.safeHead (showpp p ++ " not in env of " ++ showpp rt) [pvType q | q <- penv, pname p == pname q] checkReft :: (PPrint r, F.Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, F.Reftable (RTProp RTyCon RTyVar (UReft r))) => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc checkReft _ _ _ Nothing _ = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet. checkReft sp env emb (Just t) _ = (\z -> dr $+$ z) <$> checkSortedReftFull sp env r where r = rTypeSortedReft emb t dr = text "Sort Error in Refinement:" <+> pprint r -- DONT DELETE the below till we've added pred-checking as well -- checkReft env emb (Just t) _ = checkSortedReft env xs (rTypeSortedReft emb t) -- where xs = fromMaybe [] $ params <$> stripRTypeBase t -- checkSig env (x, t) -- = case filter (not . (`S.member` env)) (freeSymbols t) of -- [] -> TrueNGUAGE ScopedTypeVariables #-} -- ys -> errorstar (msg ys) -- where -- msg ys = printf "Unkown free symbols: %s in specification for %s \n%s\n" (showpp ys) (showpp x) (showpp t) --------------------------------------------------------------------------------------------------- -- | @checkMeasures@ determines if a measure definition is wellformed ----------------------------- --------------------------------------------------------------------------------------------------- checkMeasures :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [Measure SpecType DataCon] -> Diagnostics --------------------------------------------------------------------------------------------------- checkMeasures emb env = foldMap (checkMeasure emb env) checkMeasure :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> Measure SpecType DataCon -> Diagnostics checkMeasure emb γ (M name@(Loc src _ n) sort body _ _) = mkDiagnostics mempty [ txerror e | Just e <- checkMBody γ emb name sort <$> body ] where txerror = ErrMeas (GM.sourcePosSrcSpan src) (pprint n) checkMBody :: (PPrint r, F.Reftable r,SubsTy RTyVar RSort r, F.Reftable (RTProp RTyCon RTyVar r)) => F.SEnv F.SortedReft -> F.TCEmb TyCon -> t -> SpecType -> Def (RRType r) DataCon -> Maybe Doc checkMBody senv emb _ sort (Def m c _ bs body) = checkMBody' emb sort γ' sp body where sp = F.srcSpan m γ' = L.foldl' (\γ (x, t) -> F.insertSEnv x t γ) senv xts xts = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVarsMeet su <$> filter keep (ty_args trep) keep | allowTC = not . isEmbeddedClass | otherwise = not . isClassType -- YL: extract permitTC information from sort allowTC = or $ fmap (fromMaybe False . permitTC) (ty_info $ toRTypeRep sort) trep = toRTypeRep ct su = checkMBodyUnify (ty_res trep) (last txs) txs = thd5 $ bkArrowDeep sort ct = ofType $ dataConWrapperType c :: SpecType checkMBodyUnify :: RType t t2 t1 -> RType c tv r -> [(t2,RType c tv (),RType c tv r)] checkMBodyUnify = go where go (RVar tv _) t = [(tv, toRSort t, t)] go t@RApp{} t'@RApp{} = concat $ zipWith go (rt_args t) (rt_args t') go _ _ = [] checkMBody' :: (PPrint r, F.Reftable r,SubsTy RTyVar RSort r, F.Reftable (RTProp RTyCon RTyVar r)) => F.TCEmb TyCon -> RType RTyCon RTyVar r -> F.SEnv F.SortedReft -> F.SrcSpan -> Body -> Maybe Doc checkMBody' emb sort γ sp body = case body of E e -> checkSortFull sp γ (rTypeSort emb sort') e P p -> checkSortFull sp γ F.boolSort p R s p -> checkSortFull sp (F.insertSEnv s sty γ) F.boolSort p where sty = rTypeSortedReft emb sort' sort' = dropNArgs 1 sort dropNArgs :: Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r dropNArgs i t = fromRTypeRep $ trep {ty_binds = xs, ty_info = is, ty_args = ts, ty_refts = rs} where xs = drop i $ ty_binds trep ts = drop i $ ty_args trep rs = drop i $ ty_refts trep is = drop i $ ty_info trep trep = toRTypeRep t getRewriteErrors :: (Var, Located SpecType) -> [TError t] getRewriteErrors (rw, t) | null $ refinementEQs t = [ErrRewrite (GM.fSrcSpan t) $ text $ "Unable to use " ++ show rw ++ " as a rewrite because it does not prove an equality, or the equality it proves is trivial." ] | otherwise = refErrs ++ [ ErrRewrite (GM.fSrcSpan t) $ text $ "Could not generate any rewrites from equality. Likely causes: " ++ "\n - There are free (uninstantiatable) variables on both sides of the " ++ "equality\n - The rewrite would diverge" | cannotInstantiate] where refErrs = map getInnerRefErr (filter (hasInnerRefinement . fst) (zip tyArgs syms)) allowedRWs = [ (lhs, rhs) | (lhs , rhs) <- refinementEQs t , canRewrite (S.fromList syms) lhs rhs || canRewrite (S.fromList syms) rhs lhs ] cannotInstantiate = null allowedRWs tyArgs = ty_args tRep syms = ty_binds tRep tRep = toRTypeRep $ val t getInnerRefErr (_, sym) = ErrRewrite (GM.fSrcSpan t) $ text $ "Unable to use " ++ show rw ++ " as a rewrite. Functions whose parameters have inner refinements cannot be used as rewrites, but parameter " ++ show sym ++ " contains an inner refinement." isRefined :: F.Reftable r => RType c tv r -> Bool isRefined ty | Just r <- stripRTypeBase ty = not $ F.isTauto r | otherwise = False hasInnerRefinement :: F.Reftable r => RType c tv r -> Bool hasInnerRefinement (RFun _ _ rIn rOut _) = isRefined rIn || isRefined rOut hasInnerRefinement (RAllT _ ty _) = isRefined ty hasInnerRefinement (RAllP _ ty) = isRefined ty hasInnerRefinement (RApp _ args _ _) = any isRefined args hasInnerRefinement (RAllE _ allarg ty) = isRefined allarg || isRefined ty hasInnerRefinement (REx _ allarg ty) = isRefined allarg || isRefined ty hasInnerRefinement (RAppTy arg res _) = isRefined arg || isRefined res hasInnerRefinement (RRTy env _ _ ty) = isRefined ty || any (isRefined . snd) env hasInnerRefinement _ = False checkRewrites :: TargetSpec -> Diagnostics checkRewrites targetSpec = mkDiagnostics mempty (concatMap getRewriteErrors rwSigs) where rwSigs = filter ((`S.member` rws) . fst) sigs refl = gsRefl targetSpec sig = gsSig targetSpec sigs = gsTySigs sig ++ gsAsmSigs sig rws = S.union (S.map val $ gsRewrites refl) (S.fromList $ concat $ M.elems (gsRewritesWith refl)) checkClassMeasures :: [Measure SpecType DataCon] -> Diagnostics checkClassMeasures measures = mkDiagnostics mempty (mapMaybe checkOne byTyCon) where byName = L.groupBy ((==) `on` (val . msName)) measures byTyCon = concatMap (L.groupBy ((==) `on` (dataConTyCon . ctor . head . msEqns))) byName checkOne [] = impossible Nothing "checkClassMeasures.checkOne on empty measure group" checkOne [_] = Nothing checkOne (m:ms) = Just (ErrDupIMeas (GM.fSrcSpan (msName m)) (pprint (val (msName m))) (pprint ((dataConTyCon . ctor . head . msEqns) m)) (GM.fSrcSpan <$> (m:ms)))