{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE TupleSections      #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable  #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE DerivingVia        #-}
{-# LANGUAGE NamedFieldPuns     #-}

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

module Language.Haskell.Liquid.Types.Bounds (

    Bound(..),

    RBound, RRBound, RRBoundV,

    RBEnv, RRBEnv, RRBEnvV,

    makeBound,
    emapBoundM,
    mapBoundTy

    ) 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 as Bifunctor
import Data.Data
import qualified Data.Binary         as B
import Data.Traversable
import qualified Data.HashMap.Strict as M

import qualified Language.Fixpoint.Types as F
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.Types


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 (Typeable (Bound t e)
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 -> Constr
Bound t e -> DataType
(forall b. Data b => b -> b) -> Bound t e -> 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 -> Constr
forall t e. (Data t, Data e) => Bound t e -> DataType
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))
$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)
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)
$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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Bound t e)
$ctoConstr :: forall t e. (Data t, Data e) => Bound t e -> Constr
toConstr :: Bound t e -> Constr
$cdataTypeOf :: forall t e. (Data t, Data e) => Bound t e -> DataType
dataTypeOf :: Bound t e -> DataType
$cdataCast1 :: forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Bound t e))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Bound t e))
$cgmapT :: forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Bound t e -> Bound t e
gmapT :: (forall b. Data b => b -> b) -> Bound t e -> Bound t e
$cgmapQl :: 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
$cgmapQr :: forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Bound t e -> r
$cgmapQ :: forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Bound t e -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bound t e -> u
$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)
gmapM :: forall (m :: * -> *).
Monad 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)
gmapMp :: 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bound t e -> m (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
$cfrom :: forall t e x. Bound t e -> Rep (Bound t e) x
from :: forall x. Bound t e -> Rep (Bound t e) x
$cto :: forall t e x. Rep (Bound t e) x -> Bound t e
to :: forall x. Rep (Bound t e) x -> Bound t e
Generic, (forall a b. (a -> b) -> Bound t a -> Bound t b)
-> (forall a b. a -> Bound t b -> Bound t a) -> Functor (Bound t)
forall a b. a -> Bound t b -> Bound t a
forall a b. (a -> b) -> Bound t a -> Bound t b
forall t a b. a -> Bound t b -> Bound t a
forall t a b. (a -> b) -> Bound t a -> Bound t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t a b. (a -> b) -> Bound t a -> Bound t b
fmap :: forall a b. (a -> b) -> Bound t a -> Bound t b
$c<$ :: forall t a b. a -> Bound t b -> Bound t a
<$ :: forall a b. a -> Bound t b -> Bound t a
Functor, (forall m. Monoid m => Bound t m -> m)
-> (forall m a. Monoid m => (a -> m) -> Bound t a -> m)
-> (forall m a. Monoid m => (a -> m) -> Bound t a -> m)
-> (forall a b. (a -> b -> b) -> b -> Bound t a -> b)
-> (forall a b. (a -> b -> b) -> b -> Bound t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Bound t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Bound t a -> b)
-> (forall a. (a -> a -> a) -> Bound t a -> a)
-> (forall a. (a -> a -> a) -> Bound t a -> a)
-> (forall a. Bound t a -> [a])
-> (forall a. Bound t a -> Bool)
-> (forall a. Bound t a -> Int)
-> (forall a. Eq a => a -> Bound t a -> Bool)
-> (forall a. Ord a => Bound t a -> a)
-> (forall a. Ord a => Bound t a -> a)
-> (forall a. Num a => Bound t a -> a)
-> (forall a. Num a => Bound t a -> a)
-> Foldable (Bound t)
forall a. Eq a => a -> Bound t a -> Bool
forall a. Num a => Bound t a -> a
forall a. Ord a => Bound t a -> a
forall m. Monoid m => Bound t m -> m
forall a. Bound t a -> Bool
forall a. Bound t a -> Int
forall a. Bound t a -> [a]
forall a. (a -> a -> a) -> Bound t a -> a
forall t a. Eq a => a -> Bound t a -> Bool
forall t a. Num a => Bound t a -> a
forall t a. Ord a => Bound t a -> a
forall t m. Monoid m => Bound t m -> m
forall m a. Monoid m => (a -> m) -> Bound t a -> m
forall t a. Bound t a -> Bool
forall t a. Bound t a -> Int
forall t a. Bound t a -> [a]
forall b a. (b -> a -> b) -> b -> Bound t a -> b
forall a b. (a -> b -> b) -> b -> Bound t a -> b
forall t a. (a -> a -> a) -> Bound t a -> a
forall t m a. Monoid m => (a -> m) -> Bound t a -> m
forall t b a. (b -> a -> b) -> b -> Bound t a -> b
forall t a b. (a -> b -> b) -> b -> Bound t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall t m. Monoid m => Bound t m -> m
fold :: forall m. Monoid m => Bound t m -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Bound t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Bound t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Bound t a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Bound t a -> m
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Bound t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Bound t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Bound t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Bound t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Bound t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Bound t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Bound t a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Bound t a -> b
$cfoldr1 :: forall t a. (a -> a -> a) -> Bound t a -> a
foldr1 :: forall a. (a -> a -> a) -> Bound t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Bound t a -> a
foldl1 :: forall a. (a -> a -> a) -> Bound t a -> a
$ctoList :: forall t a. Bound t a -> [a]
toList :: forall a. Bound t a -> [a]
$cnull :: forall t a. Bound t a -> Bool
null :: forall a. Bound t a -> Bool
$clength :: forall t a. Bound t a -> Int
length :: forall a. Bound t a -> Int
$celem :: forall t a. Eq a => a -> Bound t a -> Bool
elem :: forall a. Eq a => a -> Bound t a -> Bool
$cmaximum :: forall t a. Ord a => Bound t a -> a
maximum :: forall a. Ord a => Bound t a -> a
$cminimum :: forall t a. Ord a => Bound t a -> a
minimum :: forall a. Ord a => Bound t a -> a
$csum :: forall t a. Num a => Bound t a -> a
sum :: forall a. Num a => Bound t a -> a
$cproduct :: forall t a. Num a => Bound t a -> a
product :: forall a. Num a => Bound t a -> a
Foldable, Functor (Bound t)
Foldable (Bound t)
(Functor (Bound t), Foldable (Bound t)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Bound t a -> f (Bound t b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Bound t (f a) -> f (Bound t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Bound t a -> m (Bound t b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Bound t (m a) -> m (Bound t a))
-> Traversable (Bound t)
forall t. Functor (Bound t)
forall t. Foldable (Bound t)
forall t (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
forall t (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
forall (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bound t a -> f (Bound t b)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Bound t (f a) -> f (Bound t a)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound t a -> m (Bound t b)
$csequence :: forall t (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
sequence :: forall (m :: * -> *) a. Monad m => Bound t (m a) -> m (Bound t a)
Traversable)
  deriving Get (Bound t e)
[Bound t e] -> Put
Bound t e -> Put
(Bound t e -> Put)
-> Get (Bound t e) -> ([Bound t e] -> Put) -> Binary (Bound t e)
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall t e. (Binary t, Binary e) => Get (Bound t e)
forall t e. (Binary t, Binary e) => [Bound t e] -> Put
forall t e. (Binary t, Binary e) => Bound t e -> Put
$cput :: forall t e. (Binary t, Binary e) => Bound t e -> Put
put :: Bound t e -> Put
$cget :: forall t e. (Binary t, Binary e) => Get (Bound t e)
get :: Get (Bound t e)
$cputList :: forall t e. (Binary t, Binary e) => [Bound t e] -> Put
putList :: [Bound t e] -> Put
B.Binary via Generically (Bound t e)

type RBound        = RRBound RSort
type RRBound tv    = RRBoundV F.Symbol tv
type RRBoundV v tv = Bound tv (F.ExprV v)
type RBEnv         = M.HashMap LocSymbol RBound
type RRBEnv tv     = M.HashMap LocSymbol (RRBound tv)
type RRBEnvV v tv     = M.HashMap LocSymbol (RRBoundV v tv)

emapBoundM
  :: Monad m
  => ([F.Symbol] -> t0 -> m t1)
  -> ([F.Symbol] -> e0 -> m e1)
  -> Bound t0 e0
  -> m (Bound t1 e1)
emapBoundM :: forall (m :: * -> *) t0 t1 e0 e1.
Monad m =>
([Symbol] -> t0 -> m t1)
-> ([Symbol] -> e0 -> m e1) -> Bound t0 e0 -> m (Bound t1 e1)
emapBoundM [Symbol] -> t0 -> m t1
f [Symbol] -> e0 -> m e1
g Bound t0 e0
b = do
    tyvars <- (t0 -> m t1) -> [t0] -> m [t1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol] -> t0 -> m t1
f []) ([t0] -> m [t1]) -> [t0] -> m [t1]
forall a b. (a -> b) -> a -> b
$ Bound t0 e0 -> [t0]
forall t e. Bound t e -> [t]
tyvars Bound t0 e0
b
    (e1, bparams) <- mapAccumM (\[Symbol]
e -> ((LocSymbol, t1) -> ([Symbol], (LocSymbol, t1)))
-> m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Symbol]
e,) (m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1)))
-> ((LocSymbol, t0) -> m (LocSymbol, t1))
-> (LocSymbol, t0)
-> m ([Symbol], (LocSymbol, t1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t0 -> m t1) -> (LocSymbol, t0) -> m (LocSymbol, t1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (LocSymbol, a) -> f (LocSymbol, b)
traverse ([Symbol] -> t0 -> m t1
f [Symbol]
e)) [] (bparams b)
    (e2, bargs) <- mapAccumM (\[Symbol]
e -> ((LocSymbol, t1) -> ([Symbol], (LocSymbol, t1)))
-> m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Symbol]
e,) (m (LocSymbol, t1) -> m ([Symbol], (LocSymbol, t1)))
-> ((LocSymbol, t0) -> m (LocSymbol, t1))
-> (LocSymbol, t0)
-> m ([Symbol], (LocSymbol, t1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t0 -> m t1) -> (LocSymbol, t0) -> m (LocSymbol, t1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (LocSymbol, a) -> f (LocSymbol, b)
traverse ([Symbol] -> t0 -> m t1
f [Symbol]
e)) e1 (bargs b)
    bbody <- g e2 (bbody b)
    return b{tyvars, bparams, bargs, bbody}

mapBoundTy :: (t0 -> t1) -> Bound t0 e -> Bound t1 e
mapBoundTy :: forall t0 t1 e. (t0 -> t1) -> Bound t0 e -> Bound t1 e
mapBoundTy t0 -> t1
f Bound{e
[t0]
[(LocSymbol, t0)]
LocSymbol
bname :: forall t e. Bound t e -> LocSymbol
tyvars :: forall t e. Bound t e -> [t]
bparams :: forall t e. Bound t e -> [(LocSymbol, t)]
bargs :: forall t e. Bound t e -> [(LocSymbol, t)]
bbody :: forall t e. Bound t e -> e
bname :: LocSymbol
tyvars :: [t0]
bparams :: [(LocSymbol, t0)]
bargs :: [(LocSymbol, t0)]
bbody :: e
..} = do
    Bound
      { tyvars :: [t1]
tyvars = (t0 -> t1) -> [t0] -> [t1]
forall a b. (a -> b) -> [a] -> [b]
map t0 -> t1
f [t0]
tyvars
      , bparams :: [(LocSymbol, t1)]
bparams = ((LocSymbol, t0) -> (LocSymbol, t1))
-> [(LocSymbol, t0)] -> [(LocSymbol, t1)]
forall a b. (a -> b) -> [a] -> [b]
map ((t0 -> t1) -> (LocSymbol, t0) -> (LocSymbol, t1)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t0 -> t1
f) [(LocSymbol, t0)]
bparams
      , bargs :: [(LocSymbol, t1)]
bargs = ((LocSymbol, t0) -> (LocSymbol, t1))
-> [(LocSymbol, t0)] -> [(LocSymbol, t1)]
forall a b. (a -> b) -> [a] -> [b]
map ((t0 -> t1) -> (LocSymbol, t0) -> (LocSymbol, t1)
forall a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t0 -> t1
f) [(LocSymbol, t0)]
bargs
      , e
LocSymbol
bname :: LocSymbol
bbody :: e
bname :: LocSymbol
bbody :: e
..
      }

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)]
ys 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)]
ys) 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 :: forall t0 t1 e. (t0 -> t1) -> Bound t0 e -> Bound t1 e
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 a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 a b. (a -> b) -> (LocSymbol, a) -> (LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 :: forall b c a. (b -> c) -> Bound a b -> Bound a c
second = (b -> c) -> Bound a b -> Bound a c
forall a b. (a -> b) -> Bound a a -> Bound a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

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 ExprV Symbol
expr) [RRType r]
ts [Symbol]
qs
         = [(Symbol, RRType r)] -> r -> Oblig -> RRType r -> RRType r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v 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, RType RTyCon RTyVar (), RRType r)
 -> RRType r -> RRType r)
-> RRType r
-> [(RTyVar, RType RTyCon RTyVar (), RRType r)]
-> RRType r
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (RTyVar, RType RTyCon RTyVar (), 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
subsTyVarMeet RRType r
t [(RTyVar, RType RTyCon RTyVar (), 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)]
-> [ExprV Symbol]
-> [(LocSymbol, RType RTyCon RTyVar ())]
-> [(Symbol, RRType r)]
forall r.
(PPrint r, UReftable r) =>
[(Symbol, Symbol)]
-> [ExprV Symbol]
-> [(LocSymbol, RType RTyCon RTyVar ())]
-> [(Symbol, RRType r)]
makeBoundType [(Symbol, Symbol)]
penv [ExprV Symbol]
rs [(LocSymbol, RType RTyCon RTyVar ())]
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, RType RTyCon RTyVar ()) -> LocSymbol)
-> (LocSymbol, RType RTyCon RTyVar ())
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol, RType RTyCon RTyVar ()) -> LocSymbol
forall a b. (a, b) -> a
fst ((LocSymbol, RType RTyCon RTyVar ()) -> Symbol)
-> [(LocSymbol, RType RTyCon RTyVar ())] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, RType RTyCon RTyVar ())]
ps) [Symbol]
qs
    rs :: [ExprV Symbol]
rs   = [ExprV Symbol] -> ExprV Symbol -> [ExprV Symbol]
forall {v}. [ExprV v] -> ExprV v -> [ExprV v]
bkImp [] ExprV Symbol
expr

    bkImp :: [ExprV v] -> ExprV v -> [ExprV v]
bkImp [ExprV v]
acc (F.PImp ExprV v
p ExprV v
q) = [ExprV v] -> ExprV v -> [ExprV v]
bkImp (ExprV v
pExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc) ExprV v
q
    bkImp [ExprV v]
acc ExprV v
p          = ExprV v
pExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc

    su :: [(RTyVar, RType RTyCon RTyVar (), RRType r)]
su  = [(RTyVar
α, RRType r -> RType RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort RRType r
t, RRType r
t) | (RVar RTyVar
α ()
_, RRType r
t) <-  [RType RTyCon RTyVar ()]
-> [RRType r] -> [(RType RTyCon RTyVar (), RRType r)]
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)]
-> [ExprV Symbol]
-> [(LocSymbol, RType RTyCon RTyVar ())]
-> [(Symbol, RRType r)]
makeBoundType [(Symbol, Symbol)]
penv (ExprV Symbol
q:[ExprV Symbol]
qs) [(LocSymbol, RType RTyCon RTyVar ())]
xts = [(LocSymbol, RType RTyCon RTyVar ())]
-> [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
forall {r} {c} {tv}.
UReftable r =>
[(LocSymbol, RType c tv ())] -> [(Symbol, RTypeV Symbol c tv r)]
go [(LocSymbol, RType RTyCon RTyVar ())]
xts
  where
    -- NV TODO: Turn this into a proper error
    go :: [(LocSymbol, RType c tv ())] -> [(Symbol, RTypeV Symbol c tv r)]
go [] = Maybe SrcSpan -> String -> [(Symbol, RTypeV Symbol c tv r)]
forall a. HasCallStack => 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 -> RTypeV Symbol c tv r
forall {r} {c} {tv}.
UReftable r =>
RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
tp RType c tv ()
t LocSymbol
x), (Symbol
F.dummySymbol, RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
forall {r} {c} {tv}.
UReftable r =>
RType c tv () -> LocSymbol -> RTypeV Symbol 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 -> RTypeV Symbol c tv r
forall {r} {c} {tv}.
UReftable r =>
RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
mkt RType c tv ()
t LocSymbol
x) (Symbol, RTypeV Symbol c tv r)
-> [(Symbol, RTypeV Symbol c tv r)]
-> [(Symbol, RTypeV Symbol c tv r)]
forall a. a -> [a] -> [a]
: [(LocSymbol, RType c tv ())] -> [(Symbol, RTypeV Symbol c tv r)]
go [(LocSymbol, RType c tv ())]
xtss

    mkt :: RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
mkt RType c tv ()
t LocSymbol
x = RType c tv () -> RTypeV Symbol c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x, ExprV Symbol
forall v. ExprV v
F.PTrue))
                                                ([UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr ([UsedPVarV Symbol] -> PredicateV Symbol)
-> [UsedPVarV Symbol] -> PredicateV Symbol
forall a b. (a -> b) -> a -> b
$ [UsedPVarV Symbol]
-> Symbol
-> HashMap Symbol [UsedPVarV Symbol]
-> [UsedPVarV Symbol]
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 [UsedPVarV Symbol]
ps))
    tp :: RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
tp RType c tv ()
t LocSymbol
x  = RType c tv () -> RTypeV Symbol c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x, [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ExprV Symbol]
rs))
                                                ([UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr ([UsedPVarV Symbol] -> PredicateV Symbol)
-> [UsedPVarV Symbol] -> PredicateV Symbol
forall a b. (a -> b) -> a -> b
$ [UsedPVarV Symbol]
-> Symbol
-> HashMap Symbol [UsedPVarV Symbol]
-> [UsedPVarV Symbol]
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 [UsedPVarV Symbol]
ps))
    tq :: RType c tv () -> LocSymbol -> RTypeV Symbol c tv r
tq RType c tv ()
t LocSymbol
x  = RType c tv () -> RTypeV Symbol c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` [(Symbol, Symbol)] -> LocSymbol -> ExprV Symbol -> r
forall r.
UReftable r =>
[(Symbol, Symbol)] -> LocSymbol -> ExprV Symbol -> r
makeRef [(Symbol, Symbol)]
penv LocSymbol
x ExprV Symbol
q

    (HashMap Symbol [UsedPVarV Symbol]
ps, [ExprV Symbol]
rs) = [(Symbol, Symbol)]
-> [ExprV Symbol]
-> (HashMap Symbol [UsedPVarV Symbol], [ExprV Symbol])
partitionPs [(Symbol, Symbol)]
penv [ExprV Symbol]
qs


-- NV TODO: Turn this into a proper error
makeBoundType [(Symbol, Symbol)]
_ [ExprV Symbol]
_ [(LocSymbol, RType RTyCon RTyVar ())]
_           = Maybe SrcSpan
-> String -> [(Symbol, RTypeV Symbol RTyCon RTyVar r)]
forall a. HasCallStack => 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)]
-> [ExprV Symbol]
-> (HashMap Symbol [UsedPVarV Symbol], [ExprV Symbol])
partitionPs [(Symbol, Symbol)]
penv [ExprV Symbol]
qs = ([ExprV Symbol] -> HashMap Symbol [UsedPVarV Symbol])
-> ([ExprV Symbol], [ExprV Symbol])
-> (HashMap Symbol [UsedPVarV Symbol], [ExprV Symbol])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
Bifunctor.first [ExprV Symbol] -> HashMap Symbol [UsedPVarV Symbol]
makeAR (([ExprV Symbol], [ExprV Symbol])
 -> (HashMap Symbol [UsedPVarV Symbol], [ExprV Symbol]))
-> ([ExprV Symbol], [ExprV Symbol])
-> (HashMap Symbol [UsedPVarV Symbol], [ExprV Symbol])
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> Bool)
-> [ExprV Symbol] -> ([ExprV Symbol], [ExprV Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([(Symbol, Symbol)] -> ExprV Symbol -> Bool
forall a. [(Symbol, a)] -> ExprV Symbol -> Bool
isPApp [(Symbol, Symbol)]
penv) [ExprV Symbol]
qs
  where
    makeAR :: [ExprV Symbol] -> HashMap Symbol [UsedPVarV Symbol]
makeAR [ExprV Symbol]
ps       = ([UsedPVarV Symbol] -> [UsedPVarV Symbol] -> [UsedPVarV Symbol])
-> [(Symbol, [UsedPVarV Symbol])]
-> HashMap Symbol [UsedPVarV Symbol]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith [UsedPVarV Symbol] -> [UsedPVarV Symbol] -> [UsedPVarV Symbol]
forall a. [a] -> [a] -> [a]
(++) ([(Symbol, [UsedPVarV Symbol])]
 -> HashMap Symbol [UsedPVarV Symbol])
-> [(Symbol, [UsedPVarV Symbol])]
-> HashMap Symbol [UsedPVarV Symbol]
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> (Symbol, [UsedPVarV Symbol]))
-> [ExprV Symbol] -> [(Symbol, [UsedPVarV Symbol])]
forall a b. (a -> b) -> [a] -> [b]
map ([(Symbol, Symbol)] -> ExprV Symbol -> (Symbol, [UsedPVarV Symbol])
toUsedPVars [(Symbol, Symbol)]
penv) [ExprV Symbol]
ps

isPApp :: [(F.Symbol, a)] -> F.Expr -> Bool
isPApp :: forall a. [(Symbol, a)] -> ExprV Symbol -> Bool
isPApp [(Symbol, a)]
penv (F.EApp (F.EVar Symbol
p) ExprV Symbol
_)  = 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 ExprV Symbol
e ExprV Symbol
_)         = [(Symbol, a)] -> ExprV Symbol -> Bool
forall a. [(Symbol, a)] -> ExprV Symbol -> Bool
isPApp [(Symbol, a)]
penv ExprV Symbol
e
isPApp [(Symbol, a)]
_    ExprV Symbol
_                  = Bool
False

toUsedPVars :: [(F.Symbol, F.Symbol)] -> F.Expr -> (F.Symbol, [PVar ()])
toUsedPVars :: [(Symbol, Symbol)] -> ExprV Symbol -> (Symbol, [UsedPVarV Symbol])
toUsedPVars [(Symbol, Symbol)]
penv q :: ExprV Symbol
q@(F.EApp ExprV Symbol
_ ExprV Symbol
expr) = (Symbol
sym, [[(Symbol, Symbol)] -> ExprV Symbol -> UsedPVarV Symbol
toUsedPVar [(Symbol, Symbol)]
penv ExprV Symbol
q])
  where
    -- NV : TODO make this a better error
    sym :: Symbol
sym = case {- unProp -} ExprV Symbol
expr of {F.EVar Symbol
x -> Symbol
x; ExprV Symbol
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]
++ ExprV Symbol -> String
forall a. Show a => a -> String
show ExprV Symbol
e) }
toUsedPVars [(Symbol, Symbol)]
_ ExprV Symbol
_ = Maybe SrcSpan -> String -> (Symbol, [UsedPVarV Symbol])
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)] -> ExprV Symbol -> UsedPVarV Symbol
toUsedPVar [(Symbol, Symbol)]
penv ee :: ExprV Symbol
ee@(F.EApp ExprV Symbol
_ ExprV Symbol
_)
  = Symbol
-> () -> Symbol -> [((), Symbol, ExprV Symbol)] -> UsedPVarV Symbol
forall v t.
Symbol -> t -> Symbol -> [(t, Symbol, ExprV v)] -> PVarV v t
PV Symbol
q () Symbol
e (((), Symbol
F.dummySymbol,) (ExprV Symbol -> ((), Symbol, ExprV Symbol))
-> [ExprV Symbol] -> [((), Symbol, ExprV Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es')
   where
     F.EVar Symbol
e = {- unProp $ -} [ExprV Symbol] -> ExprV Symbol
forall a. HasCallStack => [a] -> a
last [ExprV Symbol]
es
     es' :: [ExprV Symbol]
es'    = [ExprV Symbol] -> [ExprV Symbol]
forall a. HasCallStack => [a] -> [a]
init [ExprV Symbol]
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, [ExprV Symbol]
es) = ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
ee

toUsedPVar [(Symbol, Symbol)]
_ ExprV Symbol
_ = Maybe SrcSpan -> String -> UsedPVarV Symbol
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 :: forall r.
UReftable r =>
[(Symbol, Symbol)] -> LocSymbol -> ExprV Symbol -> r
makeRef [(Symbol, Symbol)]
penv LocSymbol
v (F.PAnd [ExprV Symbol]
rs) = UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
v, [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ExprV Symbol]
rrs)) PredicateV Symbol
r)
  where
    r :: PredicateV Symbol
r                    = [UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr  ([(Symbol, Symbol)] -> ExprV Symbol -> UsedPVarV Symbol
toUsedPVar [(Symbol, Symbol)]
penv (ExprV Symbol -> UsedPVarV Symbol)
-> [ExprV Symbol] -> [UsedPVarV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
pps)
    ([ExprV Symbol]
pps, [ExprV Symbol]
rrs)           = (ExprV Symbol -> Bool)
-> [ExprV Symbol] -> ([ExprV Symbol], [ExprV Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([(Symbol, Symbol)] -> ExprV Symbol -> Bool
forall a. [(Symbol, a)] -> ExprV Symbol -> Bool
isPApp [(Symbol, Symbol)]
penv) [ExprV Symbol]
rs

makeRef [(Symbol, Symbol)]
penv LocSymbol
v ExprV Symbol
rr
  | [(Symbol, Symbol)] -> ExprV Symbol -> Bool
forall a. [(Symbol, a)] -> ExprV Symbol -> Bool
isPApp [(Symbol, Symbol)]
penv ExprV Symbol
rr       = UReft Reft -> r
forall r. UReftable r => UReft Reft -> r
ofUReft (Reft -> PredicateV Symbol -> UReft Reft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft(LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
v, ExprV Symbol
forall v. ExprV v
F.PTrue)) PredicateV Symbol
r)
  where
    r :: PredicateV Symbol
r                    = [UsedPVarV Symbol] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr [[(Symbol, Symbol)] -> ExprV Symbol -> UsedPVarV Symbol
toUsedPVar [(Symbol, Symbol)]
penv ExprV Symbol
rr]

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