module Language.Haskell.Liquid.Transforms.Simplify (simplifyBounds) where

import Prelude hiding (error)
import Language.Haskell.Liquid.Types
import Language.Fixpoint.Types
import Language.Fixpoint.Types.Visitor
-- import Control.Applicative                 ((<$>))


simplifyBounds :: SpecType -> SpecType
simplifyBounds :: SpecType -> SpecType
simplifyBounds = (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UReft Reft -> UReft Reft
go
  where
    go :: UReft Reft -> UReft Reft
go UReft Reft
x       = UReft Reft
x { ur_reft :: Reft
ur_reft = Reft -> Reft
go' (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ UReft Reft -> Reft
forall r. UReft r -> r
ur_reft UReft Reft
x }
    -- OLD go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)
    go' :: Reft -> Reft
go' (Reft (Symbol
v, Expr
p)) = (Symbol, Expr) -> Reft
Reft(Symbol
v, Expr -> Expr
dropBoundLike Expr
p)

dropBoundLike :: Expr -> Expr
dropBoundLike :: Expr -> Expr
dropBoundLike Expr
p
  | Expr -> Bool
isKvar Expr
p          = Expr
p
  | Expr -> Bool
isBoundLikePred Expr
p = Expr
forall a. Monoid a => a
mempty
  | Bool
otherwise         = Expr
p
  where
    isKvar :: Expr -> Bool
isKvar            = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([KVar] -> Bool) -> (Expr -> [KVar]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [KVar]
forall t. Visitable t => t -> [KVar]
kvars

isBoundLikePred :: Expr -> Bool
isBoundLikePred :: Expr -> Bool
isBoundLikePred (PAnd [Expr]
ps) = Int
simplifyLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr
p | Expr
p <- [Expr]
ps, Expr -> Bool
isImp Expr
p ]
isBoundLikePred Expr
_         = Bool
False

isImp :: Expr -> Bool
isImp :: Expr -> Bool
isImp (PImp Expr
_ Expr
_) = Bool
True
isImp Expr
_          = Bool
False

-- OLD isBoundLike (RConc pred)  = isBoundLikePred pred
-- OLD isBoundLike (RKvar _ _)   = False


-- OLD moreThan 0 _            = True
-- OLD moreThan _ []           = False
-- OLD moreThan i (True  : xs) = moreThan (i-1) xs
-- OLD moreThan i (False : xs) = moreThan i xs

simplifyLen :: Int
simplifyLen :: Int
simplifyLen = Int
5