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

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

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
  { forall t e. Bound t e -> LocSymbol
bname   :: LocSymbol         -- ^ The name of the bound
  , forall t e. Bound t e -> [t]
tyvars  :: [t]               -- ^ Type variables that appear in the bounds
  , forall t e. Bound t e -> [(LocSymbol, t)]
bparams :: [(LocSymbol, t)]  -- ^ These are abstract refinements, for now
  , forall t e. Bound t e -> [(LocSymbol, t)]
bargs   :: [(LocSymbol, t)]  -- ^ These are value variables
  , forall t e. Bound t e -> e
bbody   :: e                 -- ^ The body of the bound
  } deriving (Bound t e -> DataType
Bound t e -> Constr
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 {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 (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 e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, Typeable, 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 = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall t e. Bound t e -> LocSymbol
bname Bound t e
b1 forall a. Eq a => a -> a -> Bool
== 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 = 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)]
ys e
e) = Doc
"bound" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k LocSymbol
s Doc -> Doc -> Doc
<+>
                                      Doc
"forall" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [t]
vs Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+>
                                      forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
ps) Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+>
                                      forall {a}. PPrint a => Tidy -> [a] -> Doc
ppBsyms Tidy
k (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, t)]
ys) Doc -> Doc -> 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
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k' [a]
xs Doc -> Doc -> Doc
<+> Doc
"->"

instance Bifunctor Bound where
  first :: forall a b c. (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) = forall t e.
LocSymbol
-> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e
Bound LocSymbol
s (a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
vs) (forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
ps) (forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, a)]
xs) c
e
  second :: forall b c a. (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) = 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 :: forall r.
(PPrint r, UReftable r,
 SubsTy RTyVar (RType RTyCon RTyVar ()) r) =>
RRBound (RType RTyCon RTyVar ())
-> [RRType r] -> [Symbol] -> RRType r -> RRType r
makeBound (Bound LocSymbol
_  [RType RTyCon RTyVar ()]
vs [(LocSymbol, RType RTyCon RTyVar ())]
ps [(LocSymbol, RType RTyCon RTyVar ())]
xs Expr
expr) [RRType r]
ts [Symbol]
qs
         = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RRType r)]
cts forall a. Monoid a => a
mempty Oblig
OCons
  where
    cts :: [(Symbol, RRType r)]
cts  = (\(Symbol
x, RRType r
t) -> (Symbol
x, forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 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
subsTyVarMeet RRType r
t [(RTyVar, RType RTyCon RTyVar (), RRType r)]
su)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType r)]
cts'

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

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

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

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

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

    go [(LocSymbol
x, RType c tv ()
t)]      = [(Symbol
F.dummySymbol, forall {r} {c} {tv}.
UReftable r =>
RType c tv () -> LocSymbol -> RType c tv r
tp RType c tv ()
t LocSymbol
x), (Symbol
F.dummySymbol, 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) = (forall a. Located a -> a
val LocSymbol
x, forall {r} {c} {tv}.
UReftable r =>
RType c tv () -> LocSymbol -> RType c tv r
mkt RType c tv ()
t LocSymbol
x) 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 = forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. UReftable r => UReft Reft -> r
ofUReft (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (forall a. Located a -> a
val LocSymbol
x, forall a. Monoid a => a
mempty))
                                                ([UsedPVar] -> Predicate
Pr forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] (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  = forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. UReftable r => UReft Reft -> r
ofUReft (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (forall a. Located a -> a
val LocSymbol
x, [Expr] -> Expr
F.pAnd [Expr]
rs))
                                                ([UsedPVar] -> Predicate
Pr forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] (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  = forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` 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, RType RTyCon RTyVar ())]
_           = forall a. Maybe SrcSpan -> String -> a
panic 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 = forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst [Expr] -> HashMap Symbol [UsedPVar]
makeAR forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv) [Expr]
qs
  where
    makeAR :: [Expr] -> HashMap Symbol [UsedPVar]
makeAR [Expr]
ps       = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$ 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 :: forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, a)]
penv (F.EApp (F.EVar Symbol
p) Expr
_)  = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ 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
_)         = 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
expr) = (Symbol
sym, [[(Symbol, Symbol)] -> Expr -> UsedPVar
toUsedPVar [(Symbol, Symbol)]
penv Expr
q])
  where
    -- NV : TODO make this a better error
    sym :: Symbol
sym = case {- unProp -} Expr
expr of {F.EVar Symbol
x -> Symbol
x; Expr
e -> forall a. Maybe SrcSpan -> String -> a
todo forall a. Maybe a
Nothing (String
"Bound fails in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Expr
e) }
toUsedPVars [(Symbol, Symbol)]
_ Expr
_ = forall a. Maybe SrcSpan -> String -> a
impossible 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
_)
  = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
q (forall t. t -> PVKind t
PVProp ()) Symbol
e (((), Symbol
F.dummySymbol,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es')
   where
     F.EVar Symbol
e = {- unProp $ -} forall a. [a] -> a
last [Expr]
es
     es' :: [Expr]
es'    = forall a. [a] -> [a]
init [Expr]
es
     Just Symbol
q = 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
_ = forall a. Maybe SrcSpan -> String -> a
impossible 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 :: forall r.
UReftable r =>
[(Symbol, Symbol)] -> LocSymbol -> Expr -> r
makeRef [(Symbol, Symbol)]
penv LocSymbol
v (F.PAnd [Expr]
rs) = forall r. UReftable r => UReft Reft -> r
ofUReft (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
pps)
    ([Expr]
pps, [Expr]
rrs)           = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv) [Expr]
rs

makeRef [(Symbol, Symbol)]
penv LocSymbol
v Expr
rr
  | forall a. [(Symbol, a)] -> Expr -> Bool
isPApp [(Symbol, Symbol)]
penv Expr
rr       = forall r. UReftable r => UReft Reft -> r
ofUReft (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft(forall a. Located a -> a
val LocSymbol
v, 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         = forall r. Reftable r => Reft -> r
F.ofReft ((Symbol, Expr) -> Reft
F.Reft (forall a. Located a -> a
val LocSymbol
v, Expr
p))