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

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


simplifyBounds :: SpecType -> SpecType
simplifyBounds :: SpecType -> SpecType
simplifyBounds = (RReft -> RReft) -> SpecType -> SpecType
forall a b.
(a -> b)
-> RTypeV Symbol RTyCon RTyVar a -> RTypeV Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
forall {v}. UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
go
  where
    go :: UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
go UReftV v (ReftV Symbol)
x       = UReftV v (ReftV Symbol)
x { ur_reft = go' $ ur_reft x }
    -- OLD go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)
    go' :: ReftV Symbol -> ReftV Symbol
go' (Reft (Symbol
v, ExprV Symbol
p)) = (Symbol, ExprV Symbol) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft(Symbol
v, ExprV Symbol -> ExprV Symbol
dropBoundLike ExprV Symbol
p)

dropBoundLike :: Expr -> Expr
dropBoundLike :: ExprV Symbol -> ExprV Symbol
dropBoundLike ExprV Symbol
p
  | ExprV Symbol -> Bool
forall {v}. ExprV v -> Bool
isKvar ExprV Symbol
p          = ExprV Symbol
p
  | ExprV Symbol -> Bool
isBoundLikePred ExprV Symbol
p = ExprV Symbol
forall v. ExprV v
PTrue
  | Bool
otherwise         = ExprV Symbol
p
  where
    isKvar :: ExprV v -> Bool
isKvar            = Bool -> Bool
not (Bool -> Bool) -> (ExprV v -> Bool) -> ExprV v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [KVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([KVar] -> Bool) -> (ExprV v -> [KVar]) -> ExprV v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV v -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr

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

isImp :: Expr -> Bool
isImp :: ExprV Symbol -> Bool
isImp (PImp ExprV Symbol
_ ExprV Symbol
_) = Bool
True
isImp ExprV Symbol
_          = 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