{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeOperators        #-}

{-# 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.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Env
import Language.Fixpoint.Types hiding (trueReft)

--------------------------------------------------------------------------------
addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv
--------------------------------------------------------------------------------
addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv
addConstraints CGEnv
γ [(Symbol, SpecType)]
t = CGEnv
γ {lcs = mappend (t2c t) (lcs γ)}
  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
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd (REnv -> [(Symbol, SpecType)] -> Expr
forall r.
(IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
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 :: (IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne :: forall r.
(IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
REnv -> [(Symbol, RRType r)] -> Expr
constraintToLogicOne REnv
γ [(Symbol, RRType r)]
binds
  = ListNE Expr -> Expr
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd [[(Symbol, (Symbol, RRType r))]
-> (Symbol, (Symbol, RRType r)) -> Expr
forall (t :: * -> *) r c tv.
(Foldable t, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
t (Symbol, (Symbol, RType c tv r))
-> (Symbol, (Symbol, RType c tv r)) -> 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. HasCallStack => [a] -> a
last [Symbol]
xs,
          ([Symbol] -> Symbol
forall a. HasCallStack => [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
   symRts :: [(Symbol, RRType r)]
symRts   = [(Symbol, RRType r)] -> [(Symbol, RRType r)]
forall a. HasCallStack => [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)]
symRts
   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. HasCallStack => [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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol)
                        => t (Symbol, (Symbol, RType c tv r))
                        -> (Symbol, (Symbol, RType c tv r)) -> Expr
subConstraintToLogicOne :: forall (t :: * -> *) r c tv.
(Foldable t, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) =>
t (Symbol, (Symbol, RType c tv r))
-> (Symbol, (Symbol, RType c tv r)) -> Expr
subConstraintToLogicOne t (Symbol, (Symbol, RType c tv r))
xts (Symbol
sym', (Symbol
sym, RType c tv r
rt)) = Expr -> Expr -> Expr
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
PImp (ListNE Expr -> Expr
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd ListNE Expr
rs) Expr
r
  where
        (ListNE Expr
rs , [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
symExprs) = ((ListNE Expr,
  [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
 -> (Symbol, (Symbol, RType c tv r))
 -> (ListNE Expr,
     [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> t (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (Symbol, (Symbol, RType c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
(ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (ReftBind r, (Variable Expr, RType c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
forall {b} {v} {c} {tv}.
(ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (ReftBind r, (Variable Expr, RTypeBV b v c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
go ([], []) t (Symbol, (Symbol, RType c tv r))
xts
        ([Expr
r], [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
_ ) = (ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (ReftBind r, (Variable Expr, RType c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
forall {b} {v} {c} {tv}.
(ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (ReftBind r, (Variable Expr, RTypeBV b v c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
go ([], [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
symExprs) (Symbol
ReftBind r
sym', (Symbol
Variable Expr
sym, RType c tv r
rt))
        go :: (ListNE Expr,
 [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
-> (ReftBind r, (Variable Expr, RTypeBV b v c tv r))
-> (ListNE Expr,
    [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))])
go (ListNE Expr
acc, [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
su) (ReftBind r
x', (Variable Expr
x, RTypeBV b v c tv r
t)) = let (Reft(ReftBind r
v, ExprBV (ReftBind r) (ReftVar r)
p)) = r -> ReftBV (ReftBind r) (ReftVar r)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft (r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe r
forall r. IsReft r => r
trueReft (RTypeBV b v c tv r -> Maybe r
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase RTypeBV b v c tv r
t))
                                        su' :: [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
su'          = (ReftBind r
x', Variable Expr -> ExprBV (Variable Expr) (Variable Expr)
forall b v. v -> ExprBV b v
EVar Variable Expr
x)(ReftBind r, ExprBV (Variable Expr) (Variable Expr))
-> [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
-> [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
forall a. a -> [a] -> [a]
:(ReftBind r
v, Variable Expr -> ExprBV (Variable Expr) (Variable Expr)
forall b v. v -> ExprBV b v
EVar Variable Expr
x) (ReftBind r, ExprBV (Variable Expr) (Variable Expr))
-> [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
-> [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
forall a. a -> [a] -> [a]
: [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
su
                                    in
                                     (SubstV (Variable Expr) -> Expr -> Expr
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
subst ([(Variable Expr, ExprBV (Variable Expr) (Variable Expr))]
-> SubstV (Variable Expr)
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
mkSubst [(Variable Expr, ExprBV (Variable Expr) (Variable Expr))]
[(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
su') Expr
ExprBV (ReftBind r) (ReftVar r)
p Expr -> ListNE Expr -> ListNE Expr
forall a. a -> [a] -> [a]
: ListNE Expr
acc, [(ReftBind r, ExprBV (Variable Expr) (Variable Expr))]
su')

combinations :: [[a]] -> [[a]]
combinations :: forall a. [[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)