{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}

-- TODO: what exactly is the purpose of this module? What do these functions do?

module Language.Haskell.Liquid.Constraint.Constraint (
  constraintToLogic
, addConstraints
) where

import Prelude hiding (error)
import Data.Maybe
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Env
import Language.Fixpoint.Types

--------------------------------------------------------------------------------
addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv
--------------------------------------------------------------------------------
addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv
addConstraints CGEnv
γ [(Symbol, SpecType)]
t = CGEnv
γ {lcs :: LConstraint
lcs = LConstraint -> LConstraint -> LConstraint
forall a. Monoid a => a -> a -> a
mappend ([(Symbol, SpecType)] -> LConstraint
t2c [(Symbol, SpecType)]
t) (CGEnv -> LConstraint
lcs CGEnv
γ)}
  where
    t2c :: [(Symbol, SpecType)] -> LConstraint
t2c [(Symbol, SpecType)]
z          = [[(Symbol, SpecType)]] -> LConstraint
LC [[(Symbol, SpecType)]
z]

--------------------------------------------------------------------------------
constraintToLogic :: REnv -> LConstraint -> Expr
--------------------------------------------------------------------------------
constraintToLogic :: REnv -> LConstraint -> Expr
constraintToLogic REnv
γ (LC [[(Symbol, SpecType)]]
ts) = ListNE Expr -> Expr
pAnd (REnv -> [(Symbol, SpecType)] -> Expr
forall r. Reftable r => REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne REnv
γ ([(Symbol, SpecType)] -> Expr)
-> [[(Symbol, SpecType)]] -> ListNE Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(Symbol, SpecType)]]
ts)

-- RJ: The code below is atrocious. Please fix it!
constraintToLogicOne :: (Reftable r) => REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne :: REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne REnv
γ [(Symbol, RRType r)]
binds
  = ListNE Expr -> Expr
pAnd [[(Symbol, (Symbol, RRType r))]
-> (Symbol, (Symbol, RRType r)) -> Expr
forall (t :: * -> *) r r1 t1 t2 t3 t4.
(Foldable t, Reftable r, Reftable r1) =>
t (Symbol, (Symbol, RType t1 t2 r))
-> (Symbol, (Symbol, RType t3 t4 r1)) -> Expr
subConstraintToLogicOne
          ([Symbol] -> [(Symbol, RRType r)] -> [(Symbol, (Symbol, RRType r))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, RRType r)]
xts)
          ([Symbol] -> Symbol
forall a. [a] -> a
last [Symbol]
xs,
          ([Symbol] -> Symbol
forall a. [a] -> a
last ((Symbol, RRType r) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RRType r) -> Symbol) -> [(Symbol, RRType r)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType r)]
xts), RRType r
r))
          | [(Symbol, RRType r)]
xts <- [[(Symbol, RRType r)]]
xss]
  where
   xts :: [(Symbol, RRType r)]
xts      = [(Symbol, RRType r)] -> [(Symbol, RRType r)]
forall a. [a] -> [a]
init [(Symbol, RRType r)]
binds
   ([Symbol]
xs, [RRType r]
ts) = [(Symbol, RRType r)] -> ([Symbol], [RRType r])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, RRType r)]
xts
   r :: RRType r
r        = (Symbol, RRType r) -> RRType r
forall a b. (a, b) -> b
snd ((Symbol, RRType r) -> RRType r) -> (Symbol, RRType r) -> RRType r
forall a b. (a -> b) -> a -> b
$ [(Symbol, RRType r)] -> (Symbol, RRType r)
forall a. [a] -> a
last [(Symbol, RRType r)]
binds
   xss :: [[(Symbol, RRType r)]]
xss      = [[(Symbol, RRType r)]] -> [[(Symbol, RRType r)]]
forall a. [[a]] -> [[a]]
combinations ((\RRType r
t -> [(Symbol
x, RRType r
t) | Symbol
x <- RRType r -> REnv -> [Symbol]
forall r. RRType r -> REnv -> [Symbol]
localBindsOfType RRType r
t REnv
γ]) (RRType r -> [(Symbol, RRType r)])
-> [RRType r] -> [[(Symbol, RRType r)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType r]
ts)

subConstraintToLogicOne :: (Foldable t, Reftable r, Reftable r1)
                        => t (Symbol, (Symbol, RType t1 t2 r))
                        -> (Symbol, (Symbol, RType t3 t4 r1)) -> Expr
subConstraintToLogicOne :: t (Symbol, (Symbol, RType t1 t2 r))
-> (Symbol, (Symbol, RType t3 t4 r1)) -> Expr
subConstraintToLogicOne t (Symbol, (Symbol, RType t1 t2 r))
xts (Symbol
x', (Symbol
x, RType t3 t4 r1
t)) = Expr -> Expr -> Expr
PImp (ListNE Expr -> Expr
pAnd ListNE Expr
rs) Expr
r
  where
        (ListNE Expr
rs , [(Symbol, Expr)]
su) = ((ListNE Expr, [(Symbol, Expr)])
 -> (Symbol, (Symbol, RType t1 t2 r))
 -> (ListNE Expr, [(Symbol, Expr)]))
-> (ListNE Expr, [(Symbol, Expr)])
-> t (Symbol, (Symbol, RType t1 t2 r))
-> (ListNE Expr, [(Symbol, Expr)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType t1 t2 r))
-> (ListNE Expr, [(Symbol, Expr)])
forall r c tv.
Reftable r =>
(ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr, [(Symbol, Expr)])
go ([], []) t (Symbol, (Symbol, RType t1 t2 r))
xts
        ([Expr
r], [(Symbol, Expr)]
_ ) = (ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType t3 t4 r1))
-> (ListNE Expr, [(Symbol, Expr)])
forall r c tv.
Reftable r =>
(ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr, [(Symbol, Expr)])
go ([], [(Symbol, Expr)]
su) (Symbol
x', (Symbol
x, RType t3 t4 r1
t))
        go :: (ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr, [(Symbol, Expr)])
go (ListNE Expr
acc, [(Symbol, Expr)]
su) (Symbol
x', (Symbol
x, RType c tv r
t)) = let (Reft(Symbol
v, Expr
p)) = r -> Reft
forall r. Reftable r => r -> Reft
toReft (r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe r
forall a. Monoid a => a
mempty (RType c tv r -> Maybe r
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t))
                                        su' :: [(Symbol, Expr)]
su'          = (Symbol
x', Symbol -> Expr
EVar Symbol
x)(Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
:(Symbol
v, Symbol -> Expr
EVar Symbol
x) (Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
: [(Symbol, Expr)]
su
                                    in
                                     (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
su') Expr
p Expr -> ListNE Expr -> ListNE Expr
forall a. a -> [a] -> [a]
: ListNE Expr
acc, [(Symbol, Expr)]
su')

combinations :: [[a]] -> [[a]]
combinations :: [[a]] -> [[a]]
combinations []           = [[]]
combinations ([]:[[a]]
_)       = []
combinations ((a
y:[a]
ys):[[a]]
yss) = [a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs | [a]
xs <- [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combinations [[a]]
yss] [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combinations ([a]
ys[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
yss)