diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs index 6f966c509a..c415eb568e 100644 --- a/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -178,7 +178,7 @@ axiomType s t = AT to (reverse xts) res (to, (_,xts, Just res)) = runState (go t) (1,[], Nothing) go (RAllT a t r) = RAllT a <$> go t <*> return r go (RAllP p t) = RAllP p <$> go t - go (RFun x tx t r) | isClassType tx = (\t' -> RFun x tx t' r) <$> go t + go (RFun x tx t r) | isEmbeddedClass tx = (\t' -> RFun x tx t' r) <$> go t go (RFun x tx t r) = do (i,bs,res) <- get let x' = unDummy x i diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index aeeefbbad2..291f8ef086 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -318,7 +318,7 @@ consCBSizedTys γ xes let rts = (recType autoenv <$>) <$> xeets let xts = zip xs ts γ' <- foldM extender γ xts - let γs = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isPredVar) <$> vs) + let γs = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isEmbeddedDictVar) <$> vs) let xets' = zip3 xs es ts mapM_ (uncurry $ consBind True) (zip γs xets') return γ' @@ -724,7 +724,7 @@ splitConstraints :: TyConable c => RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r) splitConstraints (RRTy cs _ OCons t) = let (css, t') = splitConstraints t in (cs:css, t') -splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isClass c +splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c = let (css, t') = splitConstraints t in (css, RFun x tx t' r) splitConstraints t = ([], t) @@ -1122,7 +1122,7 @@ dropExists γ (REx x tx t) = (, t) <$> γ += ("dropExists", x, tx) dropExists γ t = return (γ, t) dropConstraints :: CGEnv -> SpecType -> CG SpecType -dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isClass c +dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c = (flip (RFun x tx)) r <$> dropConstraints γ t dropConstraints γ (RRTy cts _ OCons t) = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts @@ -1161,7 +1161,7 @@ caseEnv γ x _ (DataAlt c) ys pIs = do tdc <- (γ ??= (dataConWorkId c) >>= refreshVV) let (rtd,yts',_) = unfoldR tdc xt ys yts <- projectTypes pIs yts' - let ys'' = F.symbol <$> filter (not . GM.isPredVar) ys + let ys'' = F.symbol <$> filter (not . GM.isEmbeddedDictVar) ys let r1 = dataConReft c ys'' let r2 = dataConMsReft rtd ys'' let xt = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2)) @@ -1305,7 +1305,7 @@ lamExpr γ (Lit c) = snd $ literalConst (emb γ) c lamExpr γ (Tick _ e) = lamExpr γ e lamExpr γ (App e (Type _)) = lamExpr γ e lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of - (Just p1, Just p2) | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2) + (Just p1, Just p2) | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2) -> Just $ F.EApp p1 p2 (Just p1, Just _ ) -> Just p1 _ -> Nothing @@ -1357,7 +1357,7 @@ makeSingleton γ e t | higherOrderFlag γ, App f x <- simplify e = case (funExpr γ f, argForAllExpr x) of (Just f', Just x') - | not (GM.isPredExpr x) -- (isClassPred $ exprType x) + | not (GM.isEmbeddedDictExpr x) -- (isClassPred $ exprType x) -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x')) (Just f', Just _) -> strengthenMeet t (uTop $ F.exprReft f') @@ -1390,7 +1390,7 @@ funExpr γ (Var v) | S.member v (fargs γ) || GM.isDataConId v funExpr γ (App e1 e2) = case (funExpr γ e1, argExpr γ e2) of - (Just e1', Just e2') | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2) + (Just e1', Just e2') | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2) -> Just (F.EApp e1' e2') (Just e1', Just _) -> Just e1' diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs index ce971bf37d..99fb282ed7 100644 --- a/src/Language/Haskell/Liquid/Constraint/Split.hs +++ b/src/Language/Haskell/Liquid/Constraint/Split.hs @@ -249,7 +249,7 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _)) (Just (x1, _), Just (x2, _)) -> F.mkSubst [(x1, F.EVar x2)] _ -> F.mkSubst [] -splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 +splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isEmbeddedDict c1 && c1 == c2 = return [] splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index bf26ce94c3..3ddc506df9 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -184,7 +184,7 @@ specTypeToLogic es e t su = F.mkSubst $ zip xs es - (cls, nocls) = L.partition (isClassType.snd) $ zip (ty_binds trep) (ty_args trep) + (cls, nocls) = L.partition (isEmbeddedClass.snd) $ zip (ty_binds trep) (ty_args trep) :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)]) (xs, ts) = unzip nocls :: ([F.Symbol], [SpecType]) diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs index 7bef43171a..f71de9332b 100644 --- a/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -19,7 +19,7 @@ module Language.Haskell.Liquid.GHC.Misc where import Class (classKey) import Data.String import qualified Data.List as L -import PrelNames (fractionalClassKeys) +import PrelNames (fractionalClassKeys, itName, ordClassKey, numericClassKeys, eqClassKey) import FamInstEnv import Debug.Trace -- import qualified ConLike as Ghc @@ -56,7 +56,7 @@ import TcRnDriver import RdrName -import Type (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind) +import Type (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind, tyConAppTyCon_maybe) import TyCoRep import Var import IdInfo @@ -219,6 +219,9 @@ unTickExpr x = x isFractionalClass :: Class -> Bool isFractionalClass clas = classKey clas `elem` fractionalClassKeys +isOrdClass :: Class -> Bool +isOrdClass clas = classKey clas == ordClassKey + -------------------------------------------------------------------------------- -- | Pretty Printers ----------------------------------------------------------- -------------------------------------------------------------------------------- @@ -802,6 +805,47 @@ binders (Rec xes) = fst <$> xes expandVarType :: Var -> Type expandVarType = expandTypeSynonyms . varType + +-------------------------------------------------------------------------------- +-- | The following functions test if a `CoreExpr` or `CoreVar` can be +-- embedded in logic. With type-class support, we can no longer erase +-- such expressions arbitrarily. +-------------------------------------------------------------------------------- +isEmbeddedDictExpr :: CoreExpr -> Bool +isEmbeddedDictExpr = isEmbeddedDictType . CoreUtils.exprType + +isEmbeddedDictVar :: Var -> Bool +isEmbeddedDictVar v = F.notracepp msg . isEmbeddedDictType . varType $ v + where + msg = "isGoodCaseBind v = " ++ show v + +isEmbeddedDictType :: Type -> Bool +isEmbeddedDictType = anyF [isOrdPred, isNumericPred, isEqPred, isPrelEqPred] + +-- unlike isNumCls, isFracCls, these two don't check if the argument's +-- superclass is Ord or Num. I believe this is the more predictable behavior + +isPrelEqPred :: Type -> Bool +isPrelEqPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> isPrelEqTyCon tyCon + _ -> False + + +isPrelEqTyCon :: TyCon -> Bool +isPrelEqTyCon tc = tc `hasKey` eqClassKey + +isOrdPred :: Type -> Bool +isOrdPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> tyCon `hasKey` ordClassKey + _ -> False + +-- Not just Num, but Fractional, Integral as well +isNumericPred :: Type -> Bool +isNumericPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> getUnique tyCon `elem` numericClassKeys + _ -> False + + -------------------------------------------------------------------------------- -- | The following functions test if a `CoreExpr` or `CoreVar` are just types -- in disguise, e.g. have `PredType` (in the GHC sense of the word), and so diff --git a/src/Language/Haskell/Liquid/LawInstances.hs b/src/Language/Haskell/Liquid/LawInstances.hs index f01a877bee..071bdc4244 100644 --- a/src/Language/Haskell/Liquid/LawInstances.hs +++ b/src/Language/Haskell/Liquid/LawInstances.hs @@ -90,6 +90,6 @@ splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.S splitTypeConstraints = go [] where go cs (b@(_x, RApp c _ _ _):ts) - | isClass c + | isEmbeddedDict c = go (b:cs) ts go cs r = (reverse cs, map (\(x, t) -> (x, shiftVV t x)) r) diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs index 2e8a67a580..1dbe95df88 100644 --- a/src/Language/Haskell/Liquid/Measure.hs +++ b/src/Language/Haskell/Liquid/Measure.hs @@ -261,7 +261,7 @@ mapArgumens lc t1 t2 = go xts1' xts2' xts1' = dropWhile canDrop xts1 xts2' = dropWhile canDrop xts2 - canDrop (_, t) = isClassType t || isEqType t + canDrop (_, t) = isEmbeddedClass t go xs ys | length xs == length ys && and (zipWith (==) (toRSort . snd <$> xts1') (toRSort . snd <$> xts2')) diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs index 0a7f26a8b2..d47ed04028 100644 --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -63,7 +63,7 @@ logicType :: (Reftable r) => Type -> RRType r logicType τ = fromRTypeRep $ t { ty_binds = bs, ty_args = as, ty_refts = rs} where t = toRTypeRep $ ofType τ - (bs, as, rs) = unzip3 $ dropWhile (isClassType . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t) + (bs, as, rs) = unzip3 $ dropWhile (isEmbeddedClass . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t) {- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not: CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)} @@ -77,7 +77,7 @@ inlineSpecType v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds = rep = toRTypeRep t res = ty_res rep xs = intSymbol (symbol ("x" :: String)) <$> [1..length $ ty_binds rep] - vxs = dropWhile (isClassType . snd) $ zip xs (ty_args rep) + vxs = dropWhile (isEmbeddedClass . snd) $ zip xs (ty_args rep) f = dummyLoc (symbol v) t = ofType (GM.expandVarType v) :: SpecType mkA = EVar . fst @@ -104,7 +104,7 @@ measureSpecType v = go mkT [] [1..] t go f args i (RAllT a t r) = RAllT a (go f args i t) r go f args i (RAllP p t) = RAllP p $ go f args i t go f args i (RFun x t1 t2 r) - | isClassType t1 = RFun x t1 (go f args i t2) r + | isEmbeddedClass t1 = RFun x t1 (go f args i t2) r go f args i t@(RFun _ t1 t2 r) | hasRApps t = RFun x' t1 (go f (x':args) (tail i) t2) r where x' = intSymbol (symbol ("x" :: String)) (head i) @@ -127,7 +127,7 @@ weakenResult v t = F.notracepp msg t' rep = toRTypeRep t weaken x = pAnd . filter ((Just vE /=) . isSingletonExpr x) . conjuncts vE = mkEApp vF xs - xs = EVar . fst <$> dropWhile (isClassType . snd) xts + xs = EVar . fst <$> dropWhile (isEmbeddedClass . snd) xts xts = zip (ty_binds rep) (ty_args rep) vF = dummyLoc (symbol v) diff --git a/src/Language/Haskell/Liquid/Types/Fresh.hs b/src/Language/Haskell/Liquid/Types/Fresh.hs index a28a2b1dd3..622773282d 100644 --- a/src/Language/Haskell/Liquid/Types/Fresh.hs +++ b/src/Language/Haskell/Liquid/Types/Fresh.hs @@ -91,7 +91,7 @@ trueRefType (RImpF _ t t' _) trueRefType (RFun _ t t' _) = rFun <$> fresh <*> true t <*> true t' -trueRefType (RApp c ts _ _) | isClass c +trueRefType (RApp c ts _ _) | isEmbeddedDict c = rRCls c <$> mapM true ts trueRefType (RApp c ts rs r) @@ -144,7 +144,7 @@ refreshRefType (RFun b t t' _) | b == F.dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t' | otherwise = rFun b <$> refresh t <*> refresh t' -refreshRefType (RApp rc ts _ _) | isClass rc +refreshRefType (RApp rc ts _ _) | isEmbeddedDict rc = return $ rRCls rc ts refreshRefType (RApp rc ts rs r) diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs index 65f1244eee..efadeaaf5e 100644 --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -150,7 +150,7 @@ dataConArgs trep = unzip [ (x, t) | (x, t) <- zip xs ts, isValTy t] where xs = ty_binds trep ts = ty_args trep - isValTy = not . GM.isPredType . toType + isValTy = not . GM.isEmbeddedDictType . toType pdVar :: PVar t -> Predicate diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs index 32f61ec947..8c5eedf850 100644 --- a/src/Language/Haskell/Liquid/Types/Types.hs +++ b/src/Language/Haskell/Liquid/Types/Types.hs @@ -52,7 +52,7 @@ module Language.Haskell.Liquid.Types.Types ( , rTyConPVs , rTyConPropVs -- , isClassRTyCon - , isClassType, isEqType, isRVar, isBool + , isClassType, isEqType, isRVar, isBool, isEmbeddedClass -- * Refinement Types , RType (..), Ref(..), RTProp, rPropP @@ -616,6 +616,11 @@ isClassType :: TyConable c => RType c t t1 -> Bool isClassType (RApp c _ _ _) = isClass c isClassType _ = False +isEmbeddedClass :: TyConable c => RType c t t1 -> Bool +isEmbeddedClass (RApp c _ _ _) = isEmbeddedDict c +isEmbeddedClass _ = False + + -- rTyConPVHPs = filter isHPropPV . rtc_pvars -- isHPropPV = not . isPropPV @@ -896,15 +901,20 @@ class (Eq c) => TyConable c where isTuple :: c -> Bool ppTycon :: c -> Doc isClass :: c -> Bool + isEmbeddedDict :: c -> Bool isEqual :: c -> Bool isNumCls :: c -> Bool isFracCls :: c -> Bool + isOrdCls :: c -> Bool + isEqCls :: c -> Bool - isClass = const False - isEqual = const False - isNumCls = const False - isFracCls = const False + isClass = const False + isEmbeddedDict c = isNumCls c || isEqual c || isOrdCls c || isEqCls c + isEqual = const False + isNumCls = const False + isFracCls = const False + isOrdCls = const False -- Should just make this a @Pretty@ instance but its too damn tedious @@ -929,10 +939,13 @@ instance TyConable RTyCon where isEqual = isEqual . rtc_tc ppTycon = F.toFix - isNumCls c = maybe False (isClassOrSubClass isNumericClass) + isNumCls c = maybe False isNumericClass + (tyConClass_maybe $ rtc_tc c) + isFracCls c = maybe False isFractionalClass (tyConClass_maybe $ rtc_tc c) - isFracCls c = maybe False (isClassOrSubClass isFractionalClass) + isOrdCls c = maybe False isOrdClass (tyConClass_maybe $ rtc_tc c) + isEqCls c = isEqCls (rtc_tc c) instance TyConable TyCon where @@ -943,10 +956,13 @@ instance TyConable TyCon where isEqual c = c == eqPrimTyCon || c == eqReprPrimTyCon ppTycon = text . showPpr - isNumCls c = maybe False (isClassOrSubClass isNumericClass) - (tyConClass_maybe $ c) - isFracCls c = maybe False (isClassOrSubClass isFractionalClass) - (tyConClass_maybe $ c) + isNumCls c = maybe False isNumericClass + (tyConClass_maybe c) + isFracCls c = maybe False isFractionalClass + (tyConClass_maybe c) + isOrdCls c = maybe False isOrdClass + (tyConClass_maybe c) + isEqCls c = isPrelEqTyCon c isClassOrSubClass :: (Class -> Bool) -> Class -> Bool @@ -1665,7 +1681,7 @@ efoldReft logicBind cb dty g f fp = go go γ z (RAllP p t) = go (fp p γ) z t go γ z (RImpF x t t' r) = go γ z (RFun x t t' r) go γ z me@(RFun _ (RApp c ts _ _) t' r) - | isClass c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') + | isEmbeddedDict c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') go γ z me@(RFun x t t' r) | logicBind x t = f γ (Just me) r (go γ' (go γ z t) t') | otherwise = f γ (Just me) r (go γ (go γ z t) t')