{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE TupleSections      #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}

module Language.Haskell.Liquid.Types.Bounds (

    Bound(..),

    RBound, RRBound,

    RBEnv, RRBEnv,

    makeBound,

    ) where

import Prelude hiding (error)
import Text.PrettyPrint.HughesPJ
import GHC.Generics
import Data.List (partition)
import Data.Maybe
import Data.Hashable
import Data.Bifunctor
import Data.Data
import qualified Data.Binary         as B
import qualified Data.HashMap.Strict as M

import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Misc  as Misc -- (mapFst, mapSnd)
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.RefType


data Bound t e = Bound
  { Bound t e -> LocSymbol
bname   :: LocSymbol         -- ^ The name of the bound
  , Bound t e -> [t]
tyvars  :: [t]               -- ^ Type variables that appear in the bounds
  , Bound t e -> [(LocSymbol, t)]
bparams :: [(LocSymbol, t)]  -- ^ These are abstract refinements, for now
  , Bound t e -> [(LocSymbol, t)]
bargs   :: [(LocSymbol, t)]  -- ^ These are value variables
  , Bound t e -> e
bbody   :: e                 -- ^ The body of the bound
  } deriving (Typeable (Bound t e)
DataType
Constr
Typeable (Bound t e)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Bound t e -> c (Bound t e))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Bound t e))
-> (Bound t e -> Constr)
-> (Bound t e -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Bound t e)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Bound t e)))
-> ((forall b. Data b => b -> b) -> Bound t e -> Bound t e)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Bound t e -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Bound t e -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bound t e -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Bound t e -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e))
-> Data (Bound t e)
Bound t e -> DataType
Bound t e -> Constr
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Bound t e -> u
forall u. (forall d. Data d => d -> u) -> Bound t e -> [u]
forall t e. (Data t, Data e) => Typeable (Bound t e)
forall t e. (Data t, Data e) => Bound t e -> DataType
forall t e. (Data t, Data e) => Bound t e -> Constr
forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Bound t e -> u
forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Bound t e -> [u]
forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
$cBound :: Constr
$tBound :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
$cgmapMo :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapMp :: (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
$cgmapMp :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapM :: (forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
$cgmapM :: forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Bound t e -> m (Bound t e)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Bound t e -> u
$cgmapQi :: forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Bound t e -> u
gmapQ :: (forall d. Data d => d -> u) -> Bound t e -> [u]
$cgmapQ :: forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Bound t e -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
$cgmapQr :: forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
$cgmapQl :: forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
gmapT :: (forall b. Data b => b -> b) -> Bound t e -> Bound t e
$cgmapT :: forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
$cdataCast2 :: forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
$cdataCast1 :: forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
dataTypeOf :: Bound t e -> DataType
$cdataTypeOf :: forall t e. (Data t, Data e) => Bound t e -> DataType
toConstr :: Bound t e -> Constr
$ctoConstr :: forall t e. (Data t, Data e) => Bound t e -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
$cgunfold :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
$cgfoldl :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bound t e -> c (Bound t e)
$cp1Data :: forall t e. (Data t, Data e) => Typeable (Bound t e)
Data, Typeable, (forall x. Bound t e -> Rep (Bound t e) x)
-> (forall x. Rep (Bound t e) x -> Bound t e)
-> Generic (Bound t e)
forall x. Rep (Bound t e) x -> Bound t e
forall x. Bound t e -> Rep (Bound t e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t e x. Rep (Bound t e) x -> Bound t e
forall t e x. Bound t e -> Rep (Bound t e) x
$cto :: forall t e x. Rep (Bound t e) x -> Bound t e
$cfrom :: forall t e x. Bound t e -> Rep (Bound t e) x
Generic)

instance (B.Binary t, B.Binary e) => B.Binary (Bound t e)

type RBound        = RRBound RSort
type RRBound tv    = Bound tv F.Expr
type RBEnv         = M.HashMap LocSymbol RBound
type RRBEnv tv     = M.HashMap LocSymbol (RRBound tv)


instance Hashable (Bound t e) where
  hashWithSalt :: Int -> Bound t e -> Int
hashWithSalt Int
i = Int -> LocSymbol -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i (LocSymbol -> Int) -> (Bound t e -> LocSymbol) -> Bound t e -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname

instance Eq (Bound t e) where
  Bound t e
b1 == :: Bound t e -> Bound t e -> Bool
== Bound t e
b2 = Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname Bound t e
b1 LocSymbol -> LocSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== Bound t e -> LocSymbol
forall t e. Bound t e -> LocSymbol
bname Bound t e
b2

instance (PPrint e, PPrint t) => (Show (Bound t e)) where
  show :: Bound t e -> String
show = Bound t e -> String
forall a. PPrint a => a -> String
showpp


instance (PPrint e, PPrint t) => (PPrint (Bound t e)) where
  pprintTidy :: Tidy -> Bound t e -> Doc
pprintTidy Tidy
k (Bound LocSymbol
s [t]
vs [(LocSymbol, t)]
ps [(LocSymbol, t)]
xs e
e) = Doc
"bound" Doc -> Doc -> Doc
<+> Tidy -> LocSymbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k LocSymbol
s Doc -> Doc -> Doc
<+>
                                      Doc
"forall" Doc -> Doc -> Doc
<+> Tidy -> [t] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [t]
vs Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+>
                                      Tidy -> [LocSymbol] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ((LocSymbol, t) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, t) -> LocSymbol) -> [(LocSymbol, t)] -> [LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
ps) Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+>
                                      Tidy -> [LocSymbol] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
ppBsyms Tidy
k ((LocSymbol, t) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, t) -> LocSymbol) -> [(LocSymbol, t)] -> [LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
xs) Doc -> Doc -> Doc
<+> Tidy -> e -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k e
e
    where
      ppBsyms :: Tidy -> [a] -> Doc
ppBsyms Tidy
_ [] = Doc
""
      ppBsyms Tidy
k [a]
xs = Doc
"\\" Doc -> Doc -> Doc
<+> Tidy -> [a] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [a]
xs Doc -> Doc -> Doc
<+> Doc
"->"

instance Bifunctor Bound where
  first :: (a -> b) -> Bound a c -> Bound b c
first  a -> b
f (Bound LocSymbol
s [a]
vs [(LocSymbol, a)]
ps [(LocSymbol, a)]
xs c
e) = LocSymbol
-> [b] -> [(LocSymbol, b)] -> [(LocSymbol, b)] -> c -> Bound b c
forall t e.
LocSymbol
-> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e
Bound LocSymbol
s (a -> b
f (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
vs) ((a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd a -> b
f ((LocSymbol, a) -> (LocSymbol, b))
-> [(LocSymbol, a)] -> [(LocSymbol, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
ps) ((a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd a -> b
f ((LocSymbol, a) -> (LocSymbol, b))
-> [(LocSymbol, a)] -> [(LocSymbol, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
xs) c
e
  second :: (b -> c) -> Bound a b -> Bound a c
second b -> c
f (Bound LocSymbol
s [a]
vs [(LocSymbol, a)]
ps [(LocSymbol, a)]
xs b
e) = LocSymbol
-> [a] -> [(LocSymbol, a)] -> [(LocSymbol, a)] -> c -> Bound a c
forall t e.
LocSymbol
-> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e
Bound LocSymbol
s [a]
vs [(LocSymbol, a)]
ps [(LocSymbol, a)]
xs (b -> c
f b
e)

makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r)
          => RRBound RSort -> [RRType r] -> [F.Symbol] -> RRType r -> RRType r
makeBound :: RRBound RSort -> [RRType r] -> [Symbol] -> RRType r -> RRType r
makeBound (Bound LocSymbol
_  [RSort]
vs [(LocSymbol, RSort)]
ps [(LocSymbol, RSort)]
xs Expr
p) [RRType r]
ts [Symbol]
qs
         = [(Symbol, RRType r)] -> r -> Oblig -> RRType r -> RRType r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RRType r)]
cts r
forall a. Monoid a => a
mempty Oblig
OCons
  where
    cts :: [(Symbol, RRType r)]
cts  = (\(Symbol
x, RRType r
t) -> (Symbol
x, ((RTyVar, RSort, RRType r) -> RRType r -> RRType r)
-> RRType r -> [(RTyVar, RSort, RRType r)] -> RRType r
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (RTyVar, RSort, RRType r) -> RRType r -> RRType r
forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVar_meet RRType r
t [(RTyVar, RSort, RRType r)]
su)) ((Symbol, RRType r) -> (Symbol, RRType r))
-> [(Symbol, RRType r)] -> [(Symbol, RRType r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType r)]
cts'

    cts' :: [(Symbol, RRType r)]
cts' = [(Symbol, Symbol)]
-> [Expr] -> [(LocSymbol, RSort)] -> [(Symbol, RRType r)]
forall r.
(PPrint r, UReftable r) =>
[(Symbol, Symbol)]
-> [Expr] -> [(LocSymbol, RSort)] -> [(Symbol, RRType r)]
makeBoundType [(Symbol, Symbol)]
penv [Expr]
rs [(LocSymbol, RSort)]
xs

    penv :: [(Symbol, Symbol)]
penv = [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol)
-> ((LocSymbol, RSort) -> LocSymbol)
-> (LocSymbol, RSort)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol, RSort) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, RSort) -> Symbol) -> [(LocSymbol, RSort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, RSort)]
ps) [Symbol]
qs
    rs :: [Expr]
rs   = [Expr] -> Expr -> [Expr]
bkImp [] Expr
p

    bkImp :: [Expr] -> Expr -> [Expr]
bkImp [Expr]
acc (F.PImp Expr
p Expr
q) = [Expr] -> Expr -> [Expr]
bkImp (Expr
pExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
acc) Expr
q
    bkImp [Expr]
acc Expr
p          = Expr
pExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
acc

    su :: [(RTyVar, RSort, RRType r)]
su  = [(RTyVar
α, RRType r -> RSort
forall c tv r. RType c tv r -> RType c tv ()
toRSort RRType r
t, RRType r
t) | (RVar RTyVar
α ()
_, RRType r
t) <-  [RSort] -> [RRType r] -> [(RSort, RRType r)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RSort]
vs [RRType r]
ts ]

makeBoundType :: (PPrint r, UReftable r)
              => [(F.Symbol, F.Symbol)]
              -> [F.Expr]
              -> [(LocSymbol, RSort)]
              -> [(F.Symbol, RRType r)]
makeBoundType :: [(Symbol, Symbol)]
-> [Expr] -> [(LocSymbol, RSort)] -> [(Symbol, RRType r)]
makeBoundType [(Symbol, Symbol)]
penv (Expr
q:[Expr]
qs) [(LocSymbol, RSort)]
xts = [(LocSymbol, RSort)] -> [(Symbol, RRType r)]
forall r c tv.
UReftable r =>
[(LocSymbol, RType c tv ())] -> [(Symbol, RType c tv r)]
go [(LocSymbol, RSort)]
xts
  where
    -- NV TODO: Turn this into a proper error
    go :: [(LocSymbol, RType c tv ())] -> [(Symbol, RType c tv r)]
go [] = Maybe SrcSpan -> String -> [(Symbol, RType c tv r)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Bound with empty symbols"

    go [(LocSymbol
x, RType c tv ()
t)]      = [(Symbol
F.dummySymbol, RType c tv () -> LocSymbol -> RType c tv r
forall r c tv.
UReftable r =>
RType c tv () -> LocSymbol -> RType c tv r
tp RType c tv ()
t LocSymbol
x), (Symbol
F.dummySymbol, RType c tv () -> LocSymbol -> RType c tv r
forall r c tv.
UReftable r =>
RType c tv () -> LocSymbol -> RType c tv r
tq RType c tv ()
t LocSymbol
x)]
    go ((LocSymbol
x, RType c tv ()
t):[(LocSymbol, RType c tv ())]
xtss) = (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x, RType c tv () -> LocSymbol -> RType c tv r
forall r c tv.
UReftable r =>
RType c tv () -> LocSymbol -> RType c tv r
mkt RType c tv ()
t LocSymbol
x) (Symbol, RType c tv r)
-> [(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall a. a -> [a] -> [a]
: [(LocSymbol, RType c tv ())] -> [(Symbol, RType c tv r)]
go [(LocSymbol, RType c tv ())]
xtss

    mkt :: RType c tv () -> LocSymbol -> RType c tv r
mkt RType c tv ()
t LocSymbol
x = RType c tv () -> RType c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x, Expr
forall a. Monoid a => a
mempty))
                                                ([UsedPVar] -> Predicate
Pr ([UsedPVar] -> Predicate) -> [UsedPVar] -> Predicate
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> Symbol -> HashMap Symbol [UsedPVar] -> [UsedPVar]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) HashMap Symbol [UsedPVar]
ps))
    tp :: RType c tv () -> LocSymbol -> RType c tv r
tp RType c tv ()
t LocSymbol
x  = RType c tv () -> RType c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x, [Expr] -> Expr
F.pAnd [Expr]
rs))
                                                ([UsedPVar] -> Predicate
Pr ([UsedPVar] -> Predicate) -> [UsedPVar] -> Predicate
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> Symbol -> HashMap Symbol [UsedPVar] -> [UsedPVar]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) HashMap Symbol [UsedPVar]
ps))
    tq :: RType c tv () -> LocSymbol -> RType c tv r
tq RType c tv ()
t LocSymbol
x  = RType c tv () -> RType c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` [(Symbol, Symbol)] -> LocSymbol -> Expr -> r
forall r.
UReftable r =>
[(Symbol, Symbol)] -> LocSymbol -> Expr -> r
makeRef [(Symbol, Symbol)]
penv LocSymbol
x Expr
q

    (HashMap Symbol [UsedPVar]
ps, [Expr]
rs) = [(Symbol, Symbol)] -> [Expr] -> (HashMap Symbol [UsedPVar], [Expr])
partitionPs [(Symbol, Symbol)]
penv [Expr]
qs


-- NV TODO: Turn this into a proper error
makeBoundType [(Symbol, Symbol)]
_ [Expr]
_ [(LocSymbol, RSort)]
_           = Maybe SrcSpan -> String -> [(Symbol, RRType r)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Bound with empty predicates"


partitionPs :: [(F.Symbol, F.Symbol)] -> [F.Expr] -> (M.HashMap F.Symbol [UsedPVar], [F.Expr])
partitionPs :: [(Symbol, Symbol)] -> [Expr] -> (HashMap Symbol [UsedPVar], [Expr])
partitionPs [(Symbol, Symbol)]
penv [Expr]
qs = ([Expr] -> HashMap Symbol [UsedPVar])
-> ([Expr], [Expr]) -> (HashMap Symbol [UsedPVar], [Expr])
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst [Expr] -> HashMap Symbol [UsedPVar]
makeAR (([Expr], [Expr]) -> (HashMap Symbol [UsedPVar], [Expr]))
-> ([Expr], [Expr]) -> (HashMap Symbol [UsedPVar], [Expr])
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> ([Expr], [Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([(Symbol, Symbol)] -> Expr -> Bool
forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv) [Expr]
qs
  where
    makeAR :: [Expr] -> HashMap Symbol [UsedPVar]
makeAR [Expr]
ps       = ([UsedPVar] -> [UsedPVar] -> [UsedPVar])
-> [(Symbol, [UsedPVar])] -> HashMap Symbol [UsedPVar]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith [UsedPVar] -> [UsedPVar] -> [UsedPVar]
forall a. [a] -> [a] -> [a]
(++) ([(Symbol, [UsedPVar])] -> HashMap Symbol [UsedPVar])
-> [(Symbol, [UsedPVar])] -> HashMap Symbol [UsedPVar]
forall a b. (a -> b) -> a -> b
$ (Expr -> (Symbol, [UsedPVar])) -> [Expr] -> [(Symbol, [UsedPVar])]
forall a b. (a -> b) -> [a] -> [b]
map ([(Symbol, Symbol)] -> Expr -> (Symbol, [UsedPVar])
toUsedPVars [(Symbol, Symbol)]
penv) [Expr]
ps

isPApp :: [(F.Symbol, a)] -> F.Expr -> Bool
isPApp :: [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, a)]
penv (F.EApp (F.EVar Symbol
p) Expr
_)  = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> Maybe a -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
p [(Symbol, a)]
penv
isPApp [(Symbol, a)]
penv (F.EApp Expr
e Expr
_)         = [(Symbol, a)] -> Expr -> Bool
forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, a)]
penv Expr
e
isPApp [(Symbol, a)]
_    Expr
_                  = Bool
False

toUsedPVars :: [(F.Symbol, F.Symbol)] -> F.Expr -> (F.Symbol, [PVar ()])
toUsedPVars :: [(Symbol, Symbol)] -> Expr -> (Symbol, [UsedPVar])
toUsedPVars [(Symbol, Symbol)]
penv q :: Expr
q@(F.EApp Expr
_ Expr
e) = (Symbol
x, [[(Symbol, Symbol)] -> Expr -> UsedPVar
toUsedPVar [(Symbol, Symbol)]
penv Expr
q])
  where
    -- NV : TODO make this a better error
    x :: Symbol
x = case {- unProp -} Expr
e of {F.EVar Symbol
x -> Symbol
x; Expr
e -> Maybe SrcSpan -> String -> Symbol
forall a. Maybe SrcSpan -> String -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing (String
"Bound fails in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e) }
toUsedPVars [(Symbol, Symbol)]
_ Expr
_ = Maybe SrcSpan -> String -> (Symbol, [UsedPVar])
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"This cannot happen"

toUsedPVar :: [(F.Symbol, F.Symbol)] -> F.Expr -> PVar ()
toUsedPVar :: [(Symbol, Symbol)] -> Expr -> UsedPVar
toUsedPVar [(Symbol, Symbol)]
penv ee :: Expr
ee@(F.EApp Expr
_ Expr
_)
  = Symbol -> PVKind () -> Symbol -> [((), Symbol, Expr)] -> UsedPVar
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
q (() -> PVKind ()
forall t. t -> PVKind t
PVProp ()) Symbol
e (((), Symbol
F.dummySymbol,) (Expr -> ((), Symbol, Expr)) -> [Expr] -> [((), Symbol, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es')
   where
     F.EVar Symbol
e = {- unProp $ -} [Expr] -> Expr
forall a. [a] -> a
last [Expr]
es
     es' :: [Expr]
es'    = [Expr] -> [Expr]
forall a. [a] -> [a]
init [Expr]
es
     Just Symbol
q = Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
p [(Symbol, Symbol)]
penv
     (F.EVar Symbol
p, [Expr]
es) = Expr -> (Expr, [Expr])
F.splitEApp Expr
ee

toUsedPVar [(Symbol, Symbol)]
_ Expr
_ = Maybe SrcSpan -> String -> UsedPVar
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"This cannot happen"

-- `makeRef` is used to make the refinement of the last implication,
-- thus it can contain both concrete and abstract refinements

makeRef :: (UReftable r) => [(F.Symbol, F.Symbol)] -> LocSymbol -> F.Expr -> r
makeRef :: [(Symbol, Symbol)] -> LocSymbol -> Expr -> r
makeRef [(Symbol, Symbol)]
penv LocSymbol
v (F.PAnd [Expr]
rs) = UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
v, [Expr] -> Expr
F.pAnd [Expr]
rrs)) Predicate
r)
  where
    r :: Predicate
r                    = [UsedPVar] -> Predicate
Pr  ([(Symbol, Symbol)] -> Expr -> UsedPVar
toUsedPVar [(Symbol, Symbol)]
penv (Expr -> UsedPVar) -> [Expr] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
pps)
    ([Expr]
pps, [Expr]
rrs)           = (Expr -> Bool) -> [Expr] -> ([Expr], [Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([(Symbol, Symbol)] -> Expr -> Bool
forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv) [Expr]
rs

makeRef [(Symbol, Symbol)]
penv LocSymbol
v Expr
rr
  | [(Symbol, Symbol)] -> Expr -> Bool
forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv Expr
rr       = UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> Predicate -> UReft Reft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft(LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
v, Expr
forall a. Monoid a => a
mempty)) Predicate
r)
  where
    r :: Predicate
r                    = [UsedPVar] -> Predicate
Pr [[(Symbol, Symbol)] -> Expr -> UsedPVar
toUsedPVar [(Symbol, Symbol)]
penv Expr
rr]

makeRef [(Symbol, Symbol)]
_    LocSymbol
v Expr
p         = Reft -> r
forall r. Reftable r => Reft -> r
F.ofReft ((Symbol, Expr) -> Reft
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
v, Expr
p))