module Language.Haskell.Liquid.Simplify (simplifyBounds) where
import Language.Haskell.Liquid.Types
import Language.Fixpoint.Types
import Control.Applicative ((<$>))
simplifyLen = 5
simplifyBounds :: SpecType -> SpecType
simplifyBounds = fmap go
where
go x = x{ur_reft = go' $ ur_reft x}
go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)
isBoundLike (RConc pred) = isBoundLikePred pred
isBoundLike (RKvar _ _) = False
isBoundLikePred (PAnd ps)
= moreThan simplifyLen (isImp <$> ps)
isBoundLikePred _ = False
isImp (PImp _ _) = True
isImp _ = False
moreThan 0 _ = True
moreThan _ [] = False
moreThan i (True:xs) = moreThan (i1) xs
moreThan i (False:xs) = moreThan i xs