diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs index 0a73c6867c..5fe93c24c0 100644 --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -515,6 +515,13 @@ mkC = Just . ECon . (`F.L` F.charSort) . repr ignoreVar :: Id -> Bool ignoreVar i = simpleSymbolVar i `elem` ["I#", "D#"] +isBangInteger :: [C.CoreAlt] -> Bool +isBangInteger [(C.DataAlt s, _, _), (C.DataAlt jp,_,_), (C.DataAlt jn,_,_)] + = symbol s == "GHC.Integer.Type.S#" + && symbol jp == "GHC.Integer.Type.Jp#" + && symbol jn == "GHC.Integer.Type.Jn#" +isBangInteger _ = False + isErasable :: Id -> Bool isErasable v = F.notracepp msg $ isGhcSplId v && not (isDCId v) where @@ -570,7 +577,10 @@ instance Simplify C.CoreExpr where = simplify e simplify (C.Let xes e) = C.Let (simplify xes) (simplify e) - simplify (C.Case e x t alts) + simplify (C.Case e x t alts@[(_,_,ee),_,_]) | isBangInteger alts + = Misc.traceShow ("To simplify case") $ + sub (M.singleton x (simplify e)) (simplify ee) + simplify ce@(C.Case e x t alts) = C.Case (simplify e) x t (filter (not . isUndefined) (simplify <$> alts)) simplify (C.Cast e c) = C.Cast (simplify e) c diff --git a/tests/pos/T1363.hs b/tests/pos/T1363.hs new file mode 100644 index 0000000000..e681e111bb --- /dev/null +++ b/tests/pos/T1363.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE BangPatterns #-} +{-@ LIQUID "--exact-data-cons" @-} + +{-@ mySum :: Integer -> xs:[Integer] -> Integer / [len xs] @-} +mySum :: Integer -> [Integer] -> Integer +mySum z [] = z +mySum z (x:xs) = mySum (z + x) xs + +{-@ reflect mySum @-} + +{-@ mySum' :: Integer -> xs:[Integer] -> Integer / [len xs] @-} +mySum' :: Integer -> [Integer] -> Integer +mySum' z [] = z +mySum' z (x:xs) = let !z' = z + x + in mySum' z' xs + +{-@ reflect mySum' @-} \ No newline at end of file