{-# LANGUAGE ParallelListComp #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} module Language.Haskell.Liquid.Bare.Check ( checkGhcSpec , checkBareSpec ) where import Language.Haskell.Liquid.GHC.API as Ghc hiding (Located) import Language.Haskell.Liquid.GHC.TypeRep (Type(TyConApp, TyVarTy)) import Control.Applicative ((<|>)) import Control.Arrow ((&&&)) import Data.Maybe import Data.Function (on) import Text.PrettyPrint.HughesPJ 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.Misc (condNull, snd4) import Language.Haskell.Liquid.Types.PredType (pvarRType) import Language.Haskell.Liquid.Types.PrettyPrint (pprintSymbol) import Language.Haskell.Liquid.Types.RefType (classBinds, ofType, rTypeSort, rTypeSortedReft, subsTyVars_meet, toType) 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 import Debug.Trace (trace) ---------------------------------------------------------------------------------------------- -- | Checking BareSpec ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- checkBareSpec :: ModName -> Ms.BareSpec -> Either [Error] Ms.BareSpec checkBareSpec _ sp = Misc.applyNonNull (Right sp) Left $ concat [ checkUnique "measure" measures , checkUnique "field" fields , checkDisjoints [ inlines , hmeasures , S.fromList measures , reflects , S.fromList fields ] ] where 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 . 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] -> [Error] checkUnique _ = 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] -- mkErr <$> dups where -- mkErr (n, ls@(l:_)) = ErrDupSpecs l (pprint n) ls dups = [ z | z@(_, _:_:_) <- Misc.groupList nts ] nts = [ (n, l) | t <- ts, let n = nameF t, let l = locF t ] checkDisjoints :: [S.HashSet F.LocSymbol] -> [Error] checkDisjoints [] = [] checkDisjoints [_] = [] checkDisjoints (s:ss) = checkDisjoint s (S.unions ss) ++ checkDisjoints ss checkDisjoint :: S.HashSet F.LocSymbol -> S.HashSet F.LocSymbol -> [Error] checkDisjoint s1 s2 = checkUnique "disjoint" (S.toList s1 ++ S.toList s2) ---------------------------------------------------------------------------------------------- -- | Checking GhcSpec ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- checkGhcSpec :: [(ModName, Ms.BareSpec)] -> GhcSrc -> F.SEnv F.SortedReft -> [CoreBind] -> GhcSpec -> Either [Error] GhcSpec checkGhcSpec specs src env cbs sp = Misc.applyNonNull (Right sp) Left errors where errors = mapMaybe (checkBind allowHO "measure" emb tcEnv env) (gsMeas (gsData sp)) ++ condNull noPrune (mapMaybe (checkBind allowHO "constructor" emb tcEnv env) (txCtors $ gsCtors (gsData sp))) ++ mapMaybe (checkBind allowHO "assume" emb tcEnv env) (gsAsmSigs (gsSig sp)) ++ checkTySigs allowHO cbs emb tcEnv env (gsSig sp) -- ++ mapMaybe (checkTerminationExpr emb env) (gsTexprs (gsSig sp)) ++ mapMaybe (checkBind allowHO "class method" emb tcEnv env) (clsSigs (gsSig sp)) ++ mapMaybe (checkInv allowHO emb tcEnv env) (gsInvariants (gsData sp)) ++ checkIAl allowHO emb tcEnv env (gsIaliases (gsData sp)) ++ checkMeasures emb env ms ++ checkClassMeasures (gsMeasures (gsData sp)) ++ checkClassMethods (gsCls src) (gsCMethods (gsVars sp)) (gsTySigs (gsSig sp)) ++ mapMaybe checkMismatch sigs ++ checkDuplicate (gsTySigs (gsSig sp)) -- TODO-REBARE ++ checkQualifiers env (gsQualifiers (gsQual sp)) ++ checkDuplicate (gsAsmSigs (gsSig sp)) ++ checkDupIntersect (gsTySigs (gsSig sp)) (gsAsmSigs (gsSig sp)) ++ 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 sp)) ++ checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig sp) ]) ++ checkLawInstances (gsLaws sp) _rClasses = concatMap (Ms.classes . snd) specs _rInsts = concatMap (Ms.rinstance . snd) specs tAliases = concat [Ms.aliases sp | (_, sp) <- specs] eAliases = concat [Ms.ealiases sp | (_, sp) <- specs] emb = gsTcEmbeds (gsName sp) tcEnv = gsTyconEnv (gsName sp) ms = gsMeasures (gsData sp) clsSigs sp = [ (v, t) | (v, t) <- gsTySigs sp, isJust (isClassOpId_maybe v) ] sigs = gsTySigs (gsSig sp) ++ gsAsmSigs (gsSig sp) ++ gsCtors (gsData sp) allowHO = higherOrderFlag sp noPrune = not (pruneFlag sp) txCtors ts = [(v, fmap (fmap (fmap (F.filterUnMatched temps))) t) | (v, t) <- ts] temps = F.makeTemplates $ gsUnsorted $ gsData sp -- env' = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms checkPlugged :: PPrint v => [(v, LocSpecType)] -> [Error] checkPlugged xs = mkErr <$> filter (hasHoleTy . val . snd) xs where mkErr (x,t) = ErrBadData (GM.sourcePosSrcSpan $ loc t) (pprint x) msg msg = "Cannot resolve type hole `_`. Use explicit type instead." -------------------------------------------------------------------------------- checkTySigs :: Bool -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> GhcSpecSig -> [Error] -------------------------------------------------------------------------------- checkTySigs allowHO cbs emb tcEnv env sig = 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 env [] cbs where check env = checkSigTExpr allowHO 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) [Error] 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 -> [] Just t -> check env (v, t) checkSigTExpr :: Bool -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Var, (LocSpecType, Maybe [Located F.Expr])) -> [Error] checkSigTExpr allowHO emb tcEnv env (x, (t, es)) = catMaybes [mbErr1, mbErr2] where mbErr1 = checkBind allowHO empty emb tcEnv env (x, t) 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) checkSizeFun :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [TyConP] -> [Error] checkSizeFun emb env tys = 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." $+$ msg) (pprint (tcpCon tcp)) go tcp = case tcpSizeFun tcp of Nothing -> Nothing 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 ()) _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 = mkErr l d <$> _firstDuplicate xs mkErr 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 -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Maybe Error checkInv allowHO emb tcEnv env (_, t) = checkTy allowHO err emb tcEnv env t where err = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t) checkIAl :: Bool -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> [Error] checkIAl allowHO emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne allowHO emb tcEnv env) ials checkIAlOne :: Bool -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (LocSpecType, LocSpecType) -> [Maybe (TError SpecType)] checkIAlOne allowHO emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2]) where tcheck t = checkTy allowHO (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 Nothing else Just 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)] -> [Error] checkRTAliases msg _ as = err1s where err1s = checkDuplicateRTAlias msg as checkBind :: (PPrint v) => Bool -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Maybe Error checkBind allowHO s emb tcEnv env (v, t) = checkTy allowHO 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]) -> Maybe Error checkTerminationExpr emb env (v, Loc l _ t, les) = (mkErr "ill-sorted" <$> go les) <|> (mkErr "non-numeric" <$> go' les) where -- es = val <$> les mkErr k = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) k e t d) -- 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 = L.foldl' (\err e -> err <|> (val e,) <$> checkSorted (F.srcSpan e) env' (val e)) Nothing 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 mkClass $ zip (ty_binds trep) (ty_args trep) trep = toRTypeRep t mkClass (_, RApp c ts _ _) | isClass c = classBinds emb (rRCls c ts) mkClass (x, t) = [(x, rSort t)] rSort = rTypeSortedReft emb cmpZero e = F.PAtom F.Le (F.expr (0 :: Int)) (val e) checkTy :: Bool -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Error checkTy allowHO mkE emb tcEnv env t = mkE <$> checkRType allowHO emb env (Bare.txRefSort tcEnv emb t) where _msg = "CHECKTY: " ++ showpp (val t) checkDupIntersect :: [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> [Error] checkDupIntersect xts asmSigs = concatMap mkWrn {- trace msg -} dups where mkWrn (x, t) = pprWrn x (GM.sourcePosSrcSpan $ loc t) dups = L.intersectBy ((==) `on` fst) asmSigs xts pprWrn v l = trace ("WARNING: Assume Overwrites Specifications for "++ show v ++ " : " ++ GM.showPpr l) [] -- msg = "CHECKDUPINTERSECT:" ++ msg1 ++ msg2 -- msg1 = "\nCheckd-SIGS:\n" ++ showpp (M.fromList xts) -- msg2 = "\nAssume-SIGS:\n" ++ showpp (M.fromList asmSigs) checkDuplicate :: [(Var, LocSpecType)] -> [Error] checkDuplicate = checkUnique' fst (GM.fSrcSpan . snd) checkClassMethods :: Maybe [ClsInst] -> [Var] -> [(Var, LocSpecType)] -> [Error] checkClassMethods Nothing _ _ = [] checkClassMethods (Just clsis) cms xts = [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 -- checkDuplicate xts = mkErr <$> dups -- where -- mkErr (x, ts) = ErrDupSpecs (getSrcSpan x) (pprint x) (GM.fSrcSpan <$> ts) -- dups = [z | z@(_, _:_:_) <- M.toList $ group xts ] checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> [Error] checkDuplicateRTAlias s tas = mkErr <$> dups where mkErr xs@(x:_) = ErrDupAlias (GM.fSrcSpan x) (text s) (pprint . rtName . val $ x) (GM.fSrcSpan <$> xs) mkErr [] = panic Nothing "mkError: called on empty list" dups = [z | z@(_:_:_) <- L.groupBy ((==) `on` (rtName . val)) tas] checkMismatch :: (Var, LocSpecType) -> Maybe Error checkMismatch (x, t) = if ok then Nothing else Just err where ok = tyCompat x (val t') err = errTypeMismatch x t' t' = dropImplicits <$> t tyCompat :: Var -> RType RTyCon RTyVar r -> Bool tyCompat x t = F.notracepp msg (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 $ val t lqSp = GM.fSrcSpan t hsSp = getSrcSpan x ------------------------------------------------------------------------------------------------ -- | @checkRType@ determines if a type is malformed in a given environment --------------------- ------------------------------------------------------------------------------------------------ checkRType :: Bool -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc ------------------------------------------------------------------------------------------------ checkRType allowHO emb env lt = checkAppTys t <|> checkAbstractRefs t <|> efoldReft farg cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv env Nothing t where t = 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 (RAllS _ t) = go t go (RApp rtc ts _ _) = checkTcArity rtc (length ts) <|> L.foldl' (\merr t -> merr <|> go t) Nothing ts go (RImpF _ t1 t2 _)= go t1 <|> go t2 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 = tyConArity tc {- checkFunRefs t = go t where go (RAllT _ t) = go t go (RAllP _ t) = go t go (RAllS _ t) = go t go (RApp _ ts _ _) = foldl (\merr t -> merr <|> go t) Nothing ts 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 _) = Nothing go (RHole _) = Nothing go (RFun _ t1 t2 r) | isTauto r = go t1 <|> go t2 | otherwise = Just $ text "Function types cannot have refinements:" <+> (pprint r) -} 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 t = go t where penv = mkPEnv t go (RAllT _ t) = go t go (RAllP _ t) = go t go (RAllS _ t) = go t go t@(RApp c ts rs r) = check (toRSort t :: RSort) r <|> efold go ts <|> go' c rs go t@(RImpF _ t1 t2 r)= check (toRSort t :: RSort) r <|> go t1 <|> go t2 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 t) [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] -> [Error] --------------------------------------------------------------------------------------------------- checkMeasures emb env = concatMap (checkMeasure emb env) checkMeasure :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> Measure SpecType DataCon -> [Error] checkMeasure emb γ (M name@(Loc src _ n) sort body _ _) = [ 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 γ 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 γ) γ xts xts = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVars_meet su <$> ty_args trep trep = toRTypeRep ct su = checkMBodyUnify (ty_res trep) (last txs) txs = snd4 $ bkArrowDeep sort ct = ofType $ dataConUserType 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_args = ts, ty_refts = rs} where xs = drop i $ ty_binds trep ts = drop i $ ty_args trep rs = drop i $ ty_refts trep trep = toRTypeRep t checkClassMeasures :: [Measure SpecType DataCon] -> [Error] checkClassMeasures ms = mapMaybe checkOne byTyCon where byName = L.groupBy ((==) `on` (val . msName)) ms 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)))