module Language.Haskell.Liquid.Constraint.Constraint where
import Data.Monoid
import Data.Maybe
import Control.Applicative
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Constraint.Types
import Language.Fixpoint.Types
instance Monoid LConstraint where
mempty = LC []
mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)
typeToConstraint t = LC [t]
addConstraints t γ = γ {lcs = mappend (typeToConstraint t) (lcs γ)}
constraintToLogic γ (LC ts) = pAnd (constraintToLogicOne γ <$> ts)
constraintToLogicOne γ t
= pAnd [subConstraintToLogicOne (zip xs xts) (last xs, (last $ (fst <$> xts), r)) | xts <- xss]
where rep = toRTypeRep t
ts = ty_args rep
r = ty_res rep
xs = ty_binds rep
xss = combinations ((\t -> [(x, t) | x <- grapBindsWithType t γ]) <$> ts)
subConstraintToLogicOne xts (x', (x, t)) = PImp (pAnd rs) r
where
(rs , su) = foldl go ([], []) xts
([r], _ ) = go ([], su) (x', (x, t))
go (acc, su) (x', (x, t)) = let (Reft(v, rr)) = toReft (fromMaybe mempty (stripRTypeBase t)) in
let su' = (x', EVar x):(v, EVar x):su in
(subst (mkSubst su') (pAnd [p | RConc p <- rr]):acc, su')
combinations :: [[a]] -> [[a]]
combinations [] = [[]]
combinations ([]:_) = []
combinations ((y:ys):yss) = [y:xs | xs <- combinations yss] ++ combinations (ys:yss)