{-# LANGUAGE FlexibleInstances    #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

-- 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 = 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 (forall r. Reftable r => REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne REnv
γ 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 :: forall r. Reftable r => REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne REnv
γ [(Symbol, RRType r)]
binds
  = ListNE Expr -> Expr
pAnd [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
          (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [(Symbol, RRType r)]
xts)
          (forall a. [a] -> a
last [Symbol]
xs,
          (forall a. [a] -> a
last (forall a b. (a, b) -> a
fst 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
   symRts :: [(Symbol, RRType r)]
symRts   = forall a. [a] -> [a]
init [(Symbol, RRType r)]
binds
   ([Symbol]
xs, [RRType r]
ts) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, RRType r)]
symRts
   r :: RRType r
r        = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last [(Symbol, RRType r)]
binds
   xss :: [[(Symbol, RRType r)]]
xss      = forall a. [[a]] -> [[a]]
combinations ((\RRType r
t -> [(Symbol
x, RRType r
t) | Symbol
x <- forall r. RRType r -> REnv -> [Symbol]
localBindsOfType RRType r
t REnv
γ]) 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 :: 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 t (Symbol, (Symbol, RType t1 t2 r))
xts (Symbol
sym', (Symbol
sym, RType t3 t4 r1
rt)) = Expr -> Expr -> Expr
PImp (ListNE Expr -> Expr
pAnd ListNE Expr
rs) Expr
r
  where
        (ListNE Expr
rs , [(Symbol, Expr)]
symExprs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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)]
_ ) = forall {r} {c} {tv}.
Reftable r =>
(ListNE Expr, [(Symbol, Expr)])
-> (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr, [(Symbol, Expr)])
go ([], [(Symbol, Expr)]
symExprs) (Symbol
sym', (Symbol
sym, RType t3 t4 r1
rt))
        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)) = forall r. Reftable r => r -> Reft
toReft (forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty (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)forall a. a -> [a] -> [a]
:(Symbol
v, Symbol -> Expr
EVar Symbol
x) forall a. a -> [a] -> [a]
: [(Symbol, Expr)]
su
                                    in
                                     (forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
su') Expr
p forall a. a -> [a] -> [a]
: ListNE Expr
acc, [(Symbol, Expr)]
su')

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