diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,9 @@ # Revision history for inspection-testing +## 0.6.1 -- 2025-06-11 + +* Improve presentation of term inequalities (thanks Oleg Grenrus) + ## 0.6 -- 2025-01-01 * Support GHC 9.10.1 (thanks Andre Van Der Merwe) diff --git a/inspection-testing.cabal b/inspection-testing.cabal --- a/inspection-testing.cabal +++ b/inspection-testing.cabal @@ -1,5 +1,5 @@ name: inspection-testing -version: 0.6 +version: 0.6.1 synopsis: GHC plugin to do inspection testing description: Some carefully crafted libraries make promises to their users beyond functionality and performance. diff --git a/src/Test/Inspection/Core.hs b/src/Test/Inspection/Core.hs --- a/src/Test/Inspection/Core.hs +++ b/src/Test/Inspection/Core.hs @@ -1,11 +1,12 @@ -- | This module implements some analyses of Core expressions necessary for -- "Test.Inspection". Normally, users of this package can ignore this module. -{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf #-} +{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf, ViewPatterns #-} module Test.Inspection.Core ( slice , pprSlice , pprSliceDifference , eqSlice + , eqSlice' , freeOfType , freeOfTerm , doesNotAllocate @@ -61,20 +62,26 @@ #endif import qualified Data.Set as S -import Control.Monad (guard, unless, mzero) -import Control.Monad.Trans.Class (lift) -import Control.Monad.State.Strict (StateT, runStateT, execState, modify, modify', put, get, gets) +import Control.Monad (unless) +import Control.Monad.State.Strict (execState, modify', gets) import Data.List (nub, intercalate) -import Data.Maybe +import Data.Maybe (listToMaybe, fromJust) +import Data.Either (isRight) import Test.Inspection (Equivalence (..)) -- Uncomment to enable debug traces --- import Debug.Trace +-- #define DEBUG_TRACE +#ifdef DEBUG_TRACE +import Debug.Trace + tracePut :: Monad m => Int -> String -> String -> m () --- tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg +tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg +#else +tracePut :: Monad m => Int -> String -> String -> m () tracePut _ _ _ = return () +#endif #if !MIN_VERSION_ghc(9,2,0) pattern Alt :: a -> b -> c -> (a, b, c) @@ -99,7 +106,7 @@ goV v | v `S.member` local = do seen <- gets (v `S.member`) unless seen $ do - modify (S.insert v) + modify' (S.insert v) let e = fromJust $ lookup v binds go e | otherwise = return () @@ -180,21 +187,22 @@ withLessDetail sdoc = withPprStyle defaultUserStyle sdoc #endif -type VarPair = (Var, Var) -type VarPairSet = S.Set VarPair - -- | This is a heuristic, which only works if both slices -- have auxiliary variables in the right order. -- (This is mostly to work-around the buggy CSE in GHC-8.0) -- It also breaks if there is shadowing. eqSlice :: Equivalence -> Slice -> Slice -> Bool -eqSlice _ [] [] = True -eqSlice _ _ [] = False -eqSlice _ [] _ = False +eqSlice eqv l r = isRight (eqSlice' eqv l r) + +-- | Like 'eqSlice' but also returns an explanation of inequality. +eqSlice' :: Equivalence -> Slice -> Slice -> Either SDoc () +eqSlice' _ [] [] = Right () +eqSlice' _ ((v,_) : _) [] = Left $ ppr v +eqSlice' _ [] ((v,_) : _) = Left $ ppr v -- Mostly defensive programming (slices should not be empty) -eqSlice eqv slice1@((head1, _) : _) slice2@((head2, _) : _) - -- slices are equal if there exist any result with no "unification" obligations left. - = any (S.null . snd) results +eqSlice' eqv slice1@((head1, def1) : _) slice2@((head2, def2) : _) = do + let env = mkRnEnv2 emptyInScopeSet + goSliceVars [] 0 env head1 def1 head2 def2 where -- ignore types and hpc ticks it :: Bool @@ -210,58 +218,27 @@ IgnoreTypesAndTicksEquiv -> False UnorderedLetsEquiv -> True - -- results. If there are no pairs to be equated, all is fine. - results :: [((), VarPairSet)] - results = runStateT (loop' (mkRnEnv2 emptyInScopeSet) S.empty head1 head2) S.empty - - -- while there are obligations left, try to equate them. - loop :: RnEnv2 -> VarPairSet -> StateT VarPairSet [] () - loop env done = do - vars <- get - case S.minView vars of - Nothing -> return () -- nothing to do, done. - Just ((x, y), vars') -> do - put vars' - if (x, y) `S.member` done - then loop env done - else loop' env done x y - - loop' :: RnEnv2 -> VarPairSet -> Var -> Var -> StateT VarPairSet [] () - loop' env done x y = do - tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y) - tracePut 0 "DONESET" (showVarPairSet done) + goSliceVars :: [SDoc] -> Int -> RnEnv2 -> Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc () + goSliceVars ctx lv env x e1 y e2 = do + tracePut lv "SLICEVAR" (varToString x ++ " =?= " ++ varToString y) -- if x or y expressions are essentially a variable x' or y' respectively -- add an obligation to check x' = y (or x = y'). - if | Just e1 <- lookup x slice1 - , Just x' <- essentiallyVar e1 - , x' `elem` map fst slice1 - -> do modify' (S.insert (x', y)) - loop env done + if | Just x' <- essentiallyVar e1 + , Just e1' <- lookup x' slice1 + -> goSliceVars ctx lv env x' e1' y e2 - | Just e2 <- lookup y slice2 - , Just y' <- essentiallyVar e2 - , y' `elem` map fst slice2 - -> do modify' (S.insert (x, y')) - loop env done + | Just y' <- essentiallyVar e2 + , Just e2' <- lookup y' slice2 + -> goSliceVars ctx lv env x e1 y' e2' -- otherwise if neither x and y expressions are variables -- 1. compare the expressions (already assuming that x and y are equal) -- 2. comparison may create new obligations, loop. - | Just e1 <- lookup x slice1 - , Just e2 <- lookup y slice2 - -> do - let env' = rnBndr2 env x y - done' = S.insert (x, y) done - - go 0 env' e1 e2 - loop env' done' - - -- and finally, if x or y are not in the slice, we abort. | otherwise -> do - tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y ++ " NOT IN SLICES") - mzero + let env' = rnBndr2 env x y + go ctx lv env' e1 e2 essentiallyVar :: CoreExpr -> Maybe Var essentiallyVar (App e a) | it, isTyCoArg a = essentiallyVar e @@ -275,93 +252,122 @@ essentiallyVar (Tick SourceNote{} e) = essentiallyVar e essentiallyVar _ = Nothing - go :: Int -> RnEnv2 -> CoreExpr -> CoreExpr -> StateT VarPairSet [] () - go lv env (Var v1) (Var v2) = do + -- report inequality + inequality :: [SDoc] -> SDoc -> Either SDoc a + inequality [] err = Left err + inequality ctx err = Left $ err $$ hang (text "in") 2 (vcat ctx) + + go :: [SDoc] -> Int -> RnEnv2 -> CoreExpr -> CoreExpr -> Either SDoc () + go ctx lv env (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do if | v1 == v2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") return () | rnOccL env v1 == rnOccR env v2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV") return () - | otherwise -> do + | Just e1 <- lookup v1 slice1 + , Just e2 <- lookup v2 slice2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " OBLIGATION") - modify (S.insert (v1, v2)) + goSliceVars ctx lv env v1 e1 v2 e2 + | otherwise -> do + inequality ctx $ hsep [ text "inequal variables", ppr v1, text "and", ppr v2 ] - go lv _ (Lit lit1) (Lit lit2) = do + go ctx lv _ (Lit lit1) (Lit lit2) = do tracePut lv "LIT" "???" -- no Show for Literal :( - guard $ lit1 == lit2 + unless (lit1 == lit2) $ inequality ctx $ sep [ text "inequal literals", ppr lit1, text "and", ppr lit2 ] - go _ env (Type t1) (Type t2) = guard $ eqTypeX env t1 t2 - go _ env (Coercion co1) (Coercion co2) = guard $ eqCoercionX env co1 co2 + go ctx _ env (Type t1) (Type t2) = + goTypes ctx env t1 t2 - go lv env (Cast e1 _) e2 | it = go lv env e1 e2 - go lv env e1 (Cast e2 _) | it = go lv env e1 e2 + go ctx _ env (Coercion co1) (Coercion co2) = + goCoercions ctx env co1 co2 + + go ctx lv env (Cast e1 _) e2 | it = go ctx lv env e1 e2 + go ctx lv env e1 (Cast e2 _) | it = go ctx lv env e1 e2 #if MIN_VERSION_ghc(9,0,0) - go lv env (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go lv env e1 e2 - go lv env e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go lv env e1 e2 + go ctx lv env (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2 + go ctx lv env e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2 #endif - go lv env (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do - guard (eqCoercionX env co1 co2) - go lv env e1 e2 + go ctx lv env (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do + goCoercions ctx env co1 co2 + go ctx lv env e1 e2 - go lv env (App e1 a) e2 | it, isTyCoArg a = go lv env e1 e2 - go lv env e1 (App e2 a) | it, isTyCoArg a = go lv env e1 e2 - go lv env (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do - go lv env f1 f2 - go lv env a1 a2 - go lv env (Tick HpcTick{} e1) e2 | it = go lv env e1 e2 - go lv env e1 (Tick HpcTick{} e2) | it = go lv env e1 e2 - go lv env (Tick SourceNote{} e1) e2 = go lv env e1 e2 - go lv env e1 (Tick SourceNote{} e2) = go lv env e1 e2 - go lv env (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do - guard (go_tick env n1 n2) - go lv env e1 e2 + go ctx lv env (App e1 a) e2 | it, isTyCoArg a = go ctx lv env e1 e2 + go ctx lv env e1 (App e2 a) | it, isTyCoArg a = go ctx lv env e1 e2 + go ctx lv env (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do + go ctx lv env f1 f2 + go ctx lv env a1 a2 + go ctx lv env (Tick HpcTick{} e1) e2 | it = go ctx lv env e1 e2 + go ctx lv env e1 (Tick HpcTick{} e2) | it = go ctx lv env e1 e2 + go ctx lv env (Tick SourceNote{} e1) e2 = go ctx lv env e1 e2 + go ctx lv env e1 (Tick SourceNote{} e2) = go ctx lv env e1 e2 + go ctx lv env (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do + unless (go_tick env n1 n2) $ inequality ctx $ text "inequal ticks" + go ctx lv env e1 e2 - go lv env (Lam b e1) e2 | it, isTyCoVar b = go lv env e1 e2 - go lv env e1 (Lam b e2) | it, isTyCoVar b = go lv env e1 e2 - go lv env (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do - guard (it || eqTypeX env (varType b1) (varType b2)) - go lv (rnBndr2 env b1 b2) e1 e2 + go ctx lv env (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env e1 e2 + go ctx lv env e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env e1 e2 + go ctx lv env (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do + -- guard (it || eqTypeX env (varType b1) (varType b2)) -- TODO + go ctx lv (rnBndr2 env b1 b2) e1 e2 - go lv env e1@(Let _ _) e2@(Let _ _) + go ctx lv env e1@(Let _ _) e2@(Let _ _) | ul , (ps1, e1') <- peelLets e1 , (ps2, e2') <- peelLets e2 = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do - guard $ equalLength ps1 ps2 - env' <- goBinds lv env ps1 ps2 - go lv env' e1' e2' + let ctx' = text "let bindings:" <+> pprVars ps1 <+> pprVars ps2 : ctx + unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in let" + env' <- goBinds ctx' lv env ps1 ps2 - go lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) - = do go lv env r1 r2 -- No need to check binder types, since RHSs match - go lv (rnBndr2 env v1 v2) e1 e2 + go ctx lv env' e1' e2' - go lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2) - = do guard $ equalLength ps1 ps2 - sequence_ $ zipWith (go lv env') rs1 rs2 - go lv env' e1 e2 + go ctx lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) + = do go ctx lv env r1 r2 -- No need to check binder types, since RHSs match + go ctx lv (rnBndr2 env v1 v2) e1 e2 + + go ctx lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2) + = do + unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in recursive let" + sequence_ $ zipWith (go ctx lv env') rs1 rs2 + go ctx lv env' e1 e2 where + bs1, bs2 :: [CoreBndr] + rs1, rs2 :: [CoreExpr] + (bs1,rs1) = unzip ps1 (bs2,rs2) = unzip ps2 env' = rnBndrs2 env bs1 bs2 - go lv env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) + go ctx lv env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) | null a1 -- See Note [Empty case alternatives] in TrieMap - = do guard (null a2) - go lv env e1 e2 - guard (it || eqTypeX env t1 t2) + , null a2 + = do + go ctx lv env e1 e2 + unless it $ goTypes ctx env t1 t2 + | otherwise - = do guard $ equalLength a1 a2 - go lv env e1 e2 - sequence_ $ zipWith (go_alt lv (rnBndr2 env b1 b2)) a1 a2 + = do unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case" + go ctx lv env e1 e2 + sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2)) a1 a2 - go lv _ e1 e2 = do + go ctx lv _ e1 e2 = do tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2) - mzero + inequality ctx $ sep [ text "inequal terms:", ppr e1, text "and", ppr e2] + goCoercions ctx env t1 t2 + | eqCoercionX env t1 t2 = return () + | otherwise = inequality ctx $ sep [ text "inequal coercions:", ppr t1, text "and", ppr t2 ] + + goTypes ctx env t1 t2 + | eqTypeX env t1 t2 = return () + | otherwise = inequality ctx $ sep [ text "inequal types:", ppr t1, text "and", ppr t2 ] + ----------- - go_alt lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2) - = guard (c1 == c2) >> go lv (rnBndrs2 env bs1 bs2) e1 e2 + go_alt :: [SDoc] -> Int -> RnEnv2 -> CoreAlt -> CoreAlt -> Either SDoc () + go_alt ctx lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2) + = do unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ] + go ctx lv (rnBndrs2 env bs1 bs2) e1 e2 go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool go_tick env Breakpoint{ breakpointId = lid, breakpointFVs = lids } Breakpoint{ breakpointId = rid, breakpointFVs = rids } @@ -372,21 +378,40 @@ peelLets (Let (Rec bs) e) = let (xs, e') = peelLets e in (bs ++ xs, e') peelLets e = ([], e) - goBinds :: Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> StateT VarPairSet [] RnEnv2 - goBinds _ env [] [] = return env - goBinds _ _ [] (_:_) = mzero - goBinds lv env ((v1,b1):xs) ys' = do + goBinds :: [SDoc] -> Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Either SDoc RnEnv2 + goBinds _ _ env [] [] = return env + goBinds ctx _ _ [] (_:_) = inequality ctx $ text "goBinds: missing binding" + goBinds ctx _ _ (_:_) [] = inequality ctx $ text "goBinds: missing binding" + goBinds ctx lv env [(v1,b1)] [(v2, b2)] = do + -- special case of singleton let bindings: + -- there is no choice, so we can save ourselves transforming sub-errors. + go ctx lv env b1 b2 + return (rnBndr2 env v1 v2) + + goBinds ctx lv env ((v1,b1):xs) ys' = findRight (v1 : map fst xs) (map fst ys') $ do -- select a binding - ((v2,b2), ys) <- lift (choices ys') + ((v2,b2), ys) <- choices ys' + return $ do + let ctx' = hsep [text "trying", ppr v1, text "=", ppr v2] : ctx + traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv -> + go ctx' lv env b1 b2 - traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv -> - go lv env b1 b2 + -- continue with the rest of bindings, adding a pair as matching one. + goBinds ctx' lv (rnBndr2 env v1 v2) xs ys - -- if match succeeds, delete it from the obligations - modify (S.delete (v1, v2)) - -- continue with the rest of bindings, adding a pair as matching one. - goBinds lv (rnBndr2 env v1 v2) xs ys +--TODO: rename +findRight :: [Var] -> [Var] -> [Either SDoc a] -> Either SDoc a +findRight ls rs = go [] + where + go errs [] = Left $ hang (text "Cannot align let bindings:" <+> pprVars ls <+> pprVars rs) 2 (vcatBullet errs) + go _ (x@(Right _) : _) = x + go errs (Left err : xs) = go (err : errs) xs + pprVars = braces . hsep . map ppr + +vcatBullet :: [SDoc] -> SDoc +vcatBullet = vcat . map (text "*" <+>) + #if !MIN_VERSION_ghc(9,9,0) && MIN_VERSION_ghc(9,0,0) isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr isUnsafeEqualityCase scrut _bndr [Alt _ _ rhs] @@ -407,8 +432,8 @@ showVars :: [(Var, a)] -> String showVars xs = intercalate ", " [ varToString x | (x, _) <- xs ] -showVarPairSet :: VarPairSet -> String -showVarPairSet xs = intercalate ", " [ varToString x ++ " ~ " ++ varToString y | (x, y) <- S.toList xs ] +pprVars :: [(Var, a)] -> SDoc +pprVars = braces . hsep . map (ppr . fst) varToString :: Var -> String varToString v = occNameString (occName (tyVarName v)) ++ "_" ++ show (getUnique v) diff --git a/src/Test/Inspection/Plugin.hs b/src/Test/Inspection/Plugin.hs --- a/src/Test/Inspection/Plugin.hs +++ b/src/Test/Inspection/Plugin.hs @@ -229,11 +229,11 @@ , Just (v2, _) <- p2 , let slice1 = slice binds v1 , let slice2 = slice binds v2 - -> if eqSlice ignore_types slice1 slice2 - -- OK if they have the same expression - then pure ResSuccess + -> case eqSlice' ignore_types slice1 slice2 of + -- OK if they have the same expression + Right _ -> pure ResSuccess -- Not ok if the expression differ - else pure . ResFailure $ pprSliceDifference slice1 slice2 + Left err -> pure . ResFailure $ err $$ pprSliceDifference slice1 slice2 -- Not ok if both names are bound externally | Nothing <- p1 , Nothing <- p2