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)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RReft -> RReft
forall {b} {v}.
UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
go
  where
    go :: UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
go UReftBV b v (ReftBV Symbol Symbol)
x       = UReftBV b v (ReftBV Symbol Symbol)
x { ur_reft = go' $ ur_reft x }
    -- OLD go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)
    go' :: ReftBV Symbol Symbol -> ReftBV Symbol Symbol
go' (Reft (Symbol
v, ExprBV Symbol Symbol
p)) = (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
Reft(Symbol
v, ExprBV Symbol Symbol -> ExprBV Symbol Symbol
dropBoundLike ExprBV Symbol Symbol
p)

dropBoundLike :: Expr -> Expr
dropBoundLike :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
dropBoundLike ExprBV Symbol Symbol
p
  | ExprBV Symbol Symbol -> Bool
forall {v}. ExprBV Symbol v -> Bool
isKvar ExprBV Symbol Symbol
p          = ExprBV Symbol Symbol
p
  | ExprBV Symbol Symbol -> Bool
isBoundLikePred ExprBV Symbol Symbol
p = ExprBV Symbol Symbol
forall b v. ExprBV b v
PTrue
  | Bool
otherwise         = ExprBV Symbol Symbol
p
  where
    isKvar :: ExprBV Symbol v -> Bool
isKvar            = Bool -> Bool
not (Bool -> Bool)
-> (ExprBV Symbol v -> Bool) -> ExprBV Symbol 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)
-> (ExprBV Symbol v -> [KVar]) -> ExprBV Symbol v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBV Symbol v -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr

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

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