{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}

module Language.Fixpoint.Types.Environments (

  -- * Environments
    SEnv(..)
  , SESearch(..)
  , emptySEnv, toListSEnv, fromListSEnv, fromMapSEnv
  , mapSEnvWithKey, mapSEnv, mapMSEnv
  , insertSEnv, deleteSEnv, memberSEnv, lookupSEnv, unionSEnv, unionSEnv'
  , intersectWithSEnv
  , differenceSEnv
  , filterSEnv
  , lookupSEnvWithDistance
  , envCs

  -- * Local Constraint Environments
  , IBindEnv, BindId, BindMap
  , emptyIBindEnv
  , insertsIBindEnv
  , deleteIBindEnv
  , elemsIBindEnv
  , fromListIBindEnv
  , memberIBindEnv
  , unionIBindEnv
  , unionsIBindEnv
  , diffIBindEnv
  , intersectionIBindEnv
  , nullIBindEnv
  , filterIBindEnv

  -- * Global Binder Environments
  , BindEnv, beBinds
  , emptyBindEnv
  , fromListBindEnv
  , insertBindEnv, lookupBindEnv
  , filterBindEnv, mapBindEnv, mapWithKeyMBindEnv, adjustBindEnv
  , bindEnvFromList, bindEnvToList, deleteBindEnv, elemsBindEnv
  , EBindEnv, splitByQuantifiers

  -- * Information needed to lookup and update Solutions
  -- , SolEnv (..)

  -- * Groups of KVars (needed by eliminate)
  , Packs (..)
  , getPack
  , makePack
  ) where

-- import qualified Data.Store as S
import qualified Data.Store as S
import qualified Data.List   as L
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as S
import           Data.Maybe
import           Data.Function             (on)
import           Text.PrettyPrint.HughesPJ.Compat
import           Control.DeepSeq

import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Refinements
import           Language.Fixpoint.Types.Substitutions ()
import           Language.Fixpoint.Misc

type BindId        = Int
type BindMap a     = M.HashMap BindId a

newtype IBindEnv   = FB (S.HashSet BindId) deriving (IBindEnv -> IBindEnv -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IBindEnv -> IBindEnv -> Bool
$c/= :: IBindEnv -> IBindEnv -> Bool
== :: IBindEnv -> IBindEnv -> Bool
$c== :: IBindEnv -> IBindEnv -> Bool
Eq, Typeable IBindEnv
IBindEnv -> DataType
IBindEnv -> Constr
(forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
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) -> IBindEnv -> u
forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IBindEnv
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IBindEnv)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
gmapT :: (forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
$cgmapT :: (forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IBindEnv)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IBindEnv)
dataTypeOf :: IBindEnv -> DataType
$cdataTypeOf :: IBindEnv -> DataType
toConstr :: IBindEnv -> Constr
$ctoConstr :: IBindEnv -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IBindEnv
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IBindEnv
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
Data, Int -> IBindEnv -> ShowS
[IBindEnv] -> ShowS
IBindEnv -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IBindEnv] -> ShowS
$cshowList :: [IBindEnv] -> ShowS
show :: IBindEnv -> String
$cshow :: IBindEnv -> String
showsPrec :: Int -> IBindEnv -> ShowS
$cshowsPrec :: Int -> IBindEnv -> ShowS
Show, Typeable, forall x. Rep IBindEnv x -> IBindEnv
forall x. IBindEnv -> Rep IBindEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IBindEnv x -> IBindEnv
$cfrom :: forall x. IBindEnv -> Rep IBindEnv x
Generic)

instance PPrint IBindEnv where
  pprintTidy :: Tidy -> IBindEnv -> Doc
pprintTidy Tidy
_ = forall a. PPrint a => a -> Doc
pprint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> [Int]
elemsIBindEnv

newtype SEnv a     = SE { forall a. SEnv a -> HashMap Symbol a
seBinds :: M.HashMap Symbol a }
                     deriving (SEnv a -> SEnv a -> Bool
forall a. Eq a => SEnv a -> SEnv a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SEnv a -> SEnv a -> Bool
$c/= :: forall a. Eq a => SEnv a -> SEnv a -> Bool
== :: SEnv a -> SEnv a -> Bool
$c== :: forall a. Eq a => SEnv a -> SEnv a -> Bool
Eq, SEnv a -> DataType
SEnv a -> Constr
forall {a}. Data a => Typeable (SEnv a)
forall a. Data a => SEnv a -> DataType
forall a. Data a => SEnv a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> SEnv a -> SEnv a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> SEnv a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> SEnv a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> c (SEnv a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a))
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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> c (SEnv a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SEnv a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> SEnv a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SEnv a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> SEnv a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
gmapT :: (forall b. Data b => b -> b) -> SEnv a -> SEnv a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> SEnv a -> SEnv a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
dataTypeOf :: SEnv a -> DataType
$cdataTypeOf :: forall a. Data a => SEnv a -> DataType
toConstr :: SEnv a -> Constr
$ctoConstr :: forall a. Data a => SEnv a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> c (SEnv a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> c (SEnv a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SEnv a) x -> SEnv a
forall a x. SEnv a -> Rep (SEnv a) x
$cto :: forall a x. Rep (SEnv a) x -> SEnv a
$cfrom :: forall a x. SEnv a -> Rep (SEnv a) x
Generic, forall a. Eq a => a -> SEnv a -> Bool
forall a. Num a => SEnv a -> a
forall a. Ord a => SEnv a -> a
forall m. Monoid m => SEnv m -> m
forall a. SEnv a -> Bool
forall a. SEnv a -> Int
forall a. SEnv a -> [a]
forall a. (a -> a -> a) -> SEnv a -> a
forall m a. Monoid m => (a -> m) -> SEnv a -> m
forall b a. (b -> a -> b) -> b -> SEnv a -> b
forall a b. (a -> b -> b) -> b -> SEnv 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
product :: forall a. Num a => SEnv a -> a
$cproduct :: forall a. Num a => SEnv a -> a
sum :: forall a. Num a => SEnv a -> a
$csum :: forall a. Num a => SEnv a -> a
minimum :: forall a. Ord a => SEnv a -> a
$cminimum :: forall a. Ord a => SEnv a -> a
maximum :: forall a. Ord a => SEnv a -> a
$cmaximum :: forall a. Ord a => SEnv a -> a
elem :: forall a. Eq a => a -> SEnv a -> Bool
$celem :: forall a. Eq a => a -> SEnv a -> Bool
length :: forall a. SEnv a -> Int
$clength :: forall a. SEnv a -> Int
null :: forall a. SEnv a -> Bool
$cnull :: forall a. SEnv a -> Bool
toList :: forall a. SEnv a -> [a]
$ctoList :: forall a. SEnv a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SEnv a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldr1 :: forall a. (a -> a -> a) -> SEnv a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
fold :: forall m. Monoid m => SEnv m -> m
$cfold :: forall m. Monoid m => SEnv m -> m
Foldable, Functor SEnv
Foldable SEnv
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 => SEnv (m a) -> m (SEnv a)
forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
sequence :: forall (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a)
$csequence :: forall (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
sequenceA :: forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
Traversable)

data SizedEnv a    = BE { forall a. SizedEnv a -> Int
_beSize  :: !Int
                        , forall a. SizedEnv a -> BindMap a
beBinds :: !(BindMap a)
                        } deriving (SizedEnv a -> SizedEnv a -> Bool
forall a. Eq a => SizedEnv a -> SizedEnv a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SizedEnv a -> SizedEnv a -> Bool
$c/= :: forall a. Eq a => SizedEnv a -> SizedEnv a -> Bool
== :: SizedEnv a -> SizedEnv a -> Bool
$c== :: forall a. Eq a => SizedEnv a -> SizedEnv a -> Bool
Eq, Int -> SizedEnv a -> ShowS
forall a. Show a => Int -> SizedEnv a -> ShowS
forall a. Show a => [SizedEnv a] -> ShowS
forall a. Show a => SizedEnv a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SizedEnv a] -> ShowS
$cshowList :: forall a. Show a => [SizedEnv a] -> ShowS
show :: SizedEnv a -> String
$cshow :: forall a. Show a => SizedEnv a -> String
showsPrec :: Int -> SizedEnv a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SizedEnv a -> ShowS
Show, forall a b. a -> SizedEnv b -> SizedEnv a
forall a b. (a -> b) -> SizedEnv a -> SizedEnv b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SizedEnv b -> SizedEnv a
$c<$ :: forall a b. a -> SizedEnv b -> SizedEnv a
fmap :: forall a b. (a -> b) -> SizedEnv a -> SizedEnv b
$cfmap :: forall a b. (a -> b) -> SizedEnv a -> SizedEnv b
Functor, forall a. Eq a => a -> SizedEnv a -> Bool
forall a. Num a => SizedEnv a -> a
forall a. Ord a => SizedEnv a -> a
forall m. Monoid m => SizedEnv m -> m
forall a. SizedEnv a -> Bool
forall a. SizedEnv a -> Int
forall a. SizedEnv a -> [a]
forall a. (a -> a -> a) -> SizedEnv a -> a
forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
forall a b. (a -> b -> b) -> b -> SizedEnv 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
product :: forall a. Num a => SizedEnv a -> a
$cproduct :: forall a. Num a => SizedEnv a -> a
sum :: forall a. Num a => SizedEnv a -> a
$csum :: forall a. Num a => SizedEnv a -> a
minimum :: forall a. Ord a => SizedEnv a -> a
$cminimum :: forall a. Ord a => SizedEnv a -> a
maximum :: forall a. Ord a => SizedEnv a -> a
$cmaximum :: forall a. Ord a => SizedEnv a -> a
elem :: forall a. Eq a => a -> SizedEnv a -> Bool
$celem :: forall a. Eq a => a -> SizedEnv a -> Bool
length :: forall a. SizedEnv a -> Int
$clength :: forall a. SizedEnv a -> Int
null :: forall a. SizedEnv a -> Bool
$cnull :: forall a. SizedEnv a -> Bool
toList :: forall a. SizedEnv a -> [a]
$ctoList :: forall a. SizedEnv a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
foldr1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SizedEnv a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SizedEnv a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SizedEnv a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SizedEnv a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
fold :: forall m. Monoid m => SizedEnv m -> m
$cfold :: forall m. Monoid m => SizedEnv m -> m
Foldable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SizedEnv a) x -> SizedEnv a
forall a x. SizedEnv a -> Rep (SizedEnv a) x
$cto :: forall a x. Rep (SizedEnv a) x -> SizedEnv a
$cfrom :: forall a x. SizedEnv a -> Rep (SizedEnv a) x
Generic, Functor SizedEnv
Foldable SizedEnv
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 => SizedEnv (m a) -> m (SizedEnv a)
forall (f :: * -> *) a.
Applicative f =>
SizedEnv (f a) -> f (SizedEnv a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizedEnv a -> f (SizedEnv b)
sequence :: forall (m :: * -> *) a. Monad m => SizedEnv (m a) -> m (SizedEnv a)
$csequence :: forall (m :: * -> *) a. Monad m => SizedEnv (m a) -> m (SizedEnv a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizedEnv (f a) -> f (SizedEnv a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizedEnv (f a) -> f (SizedEnv a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizedEnv a -> f (SizedEnv b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizedEnv a -> f (SizedEnv b)
Traversable)

instance PPrint a => PPrint (SizedEnv a) where
  pprintTidy :: Tidy -> SizedEnv a -> Doc
pprintTidy Tidy
k (BE Int
_ BindMap a
m) = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k BindMap a
m

-- Invariant: All BindIds in the map are less than beSize
type BindEnv a     = SizedEnv (Symbol, SortedReft, a)
newtype EBindEnv a = EB (BindEnv a)

splitByQuantifiers :: BindEnv a -> [BindId] -> (BindEnv a, EBindEnv a)
splitByQuantifiers :: forall a. BindEnv a -> [Int] -> (BindEnv a, EBindEnv a)
splitByQuantifiers (BE Int
i BindMap (Symbol, SortedReft, a)
bs) [Int]
ebs = ( forall a. Int -> BindMap a -> SizedEnv a
BE Int
i forall a b. (a -> b) -> a -> b
$ forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft, a)
_ -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Int
k [Int]
ebs) BindMap (Symbol, SortedReft, a)
bs
                                   , forall a. BindEnv a -> EBindEnv a
EB forall a b. (a -> b) -> a -> b
$ forall a. Int -> BindMap a -> SizedEnv a
BE Int
i forall a b. (a -> b) -> a -> b
$ forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft, a)
_ -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
k [Int]
ebs) BindMap (Symbol, SortedReft, a)
bs
                                   )

-- data SolEnv        = SolEnv { soeBinds :: !BindEnv }
--                     deriving (Eq, Show, Generic)

instance PPrint a => PPrint (SEnv a) where
  pprintTidy :: Tidy -> SEnv a -> Doc
pprintTidy Tidy
k = forall k v. (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
pprintKVs Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
toListSEnv

{-# SCC toListSEnv #-}
toListSEnv              ::  SEnv a -> [(Symbol, a)]
toListSEnv :: forall a. SEnv a -> [(Symbol, a)]
toListSEnv (SE HashMap Symbol a
env)     = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol a
env

fromListSEnv            ::  [(Symbol, a)] -> SEnv a
fromListSEnv :: forall a. [(Symbol, a)] -> SEnv a
fromListSEnv            = forall a. HashMap Symbol a -> SEnv a
SE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList

fromMapSEnv             ::  M.HashMap Symbol a -> SEnv a
fromMapSEnv :: forall a. HashMap Symbol a -> SEnv a
fromMapSEnv             = forall a. HashMap Symbol a -> SEnv a
SE

mapSEnv                 :: (a -> b) -> SEnv a -> SEnv b
mapSEnv :: forall a b. (a -> b) -> SEnv a -> SEnv b
mapSEnv a -> b
f (SE HashMap Symbol a
env)      = forall a. HashMap Symbol a -> SEnv a
SE (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f HashMap Symbol a
env)

mapMSEnv                :: (Monad m) => (a -> m b) -> SEnv a -> m (SEnv b)
mapMSEnv :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
mapMSEnv a -> m b
f SEnv a
env          = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
secondM a -> m b
f) (forall a. SEnv a -> [(Symbol, a)]
toListSEnv SEnv a
env)

mapSEnvWithKey          :: ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b
mapSEnvWithKey :: forall a b. ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b
mapSEnvWithKey (Symbol, a) -> (Symbol, b)
f        = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol, a) -> (Symbol, b)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
toListSEnv

deleteSEnv :: Symbol -> SEnv a -> SEnv a
deleteSEnv :: forall a. Symbol -> SEnv a -> SEnv a
deleteSEnv Symbol
x (SE HashMap Symbol a
env)   = forall a. HashMap Symbol a -> SEnv a
SE (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Symbol
x HashMap Symbol a
env)

insertSEnv :: Symbol -> a -> SEnv a -> SEnv a
insertSEnv :: forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x a
v (SE HashMap Symbol a
env) = forall a. HashMap Symbol a -> SEnv a
SE (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
x a
v HashMap Symbol a
env)

{-# SCC lookupSEnv #-}
lookupSEnv :: Symbol -> SEnv a -> Maybe a
lookupSEnv :: forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x (SE HashMap Symbol a
env)   = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol a
env

emptySEnv :: SEnv a
emptySEnv :: forall a. SEnv a
emptySEnv               = forall a. HashMap Symbol a -> SEnv a
SE forall k v. HashMap k v
M.empty

memberSEnv :: Symbol -> SEnv a -> Bool
memberSEnv :: forall a. Symbol -> SEnv a -> Bool
memberSEnv Symbol
x (SE HashMap Symbol a
env)   = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
x HashMap Symbol a
env

intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
intersectWithSEnv :: forall v1 v2 a. (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
intersectWithSEnv v1 -> v2 -> a
f (SE HashMap Symbol v1
m1) (SE HashMap Symbol v2
m2) = forall a. HashMap Symbol a -> SEnv a
SE (forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
M.intersectionWith v1 -> v2 -> a
f HashMap Symbol v1
m1 HashMap Symbol v2
m2)

differenceSEnv :: SEnv a -> SEnv w -> SEnv a
differenceSEnv :: forall a w. SEnv a -> SEnv w -> SEnv a
differenceSEnv (SE HashMap Symbol a
m1) (SE HashMap Symbol w
m2) = forall a. HashMap Symbol a -> SEnv a
SE (forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
M.difference HashMap Symbol a
m1 HashMap Symbol w
m2)

filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a
filterSEnv :: forall a. (a -> Bool) -> SEnv a -> SEnv a
filterSEnv a -> Bool
f (SE HashMap Symbol a
m)     = forall a. HashMap Symbol a -> SEnv a
SE (forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter a -> Bool
f HashMap Symbol a
m)

unionSEnv :: SEnv a -> M.HashMap Symbol a -> SEnv a
unionSEnv :: forall a. SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv (SE HashMap Symbol a
m1) HashMap Symbol a
m2    = forall a. HashMap Symbol a -> SEnv a
SE (forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap Symbol a
m1 HashMap Symbol a
m2)

unionSEnv' :: SEnv a -> SEnv a -> SEnv a
unionSEnv' :: forall a. SEnv a -> SEnv a -> SEnv a
unionSEnv' (SE HashMap Symbol a
m1) (SE HashMap Symbol a
m2)    = forall a. HashMap Symbol a -> SEnv a
SE (forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap Symbol a
m1 HashMap Symbol a
m2)

{-# SCC lookupSEnvWithDistance #-}
lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a
lookupSEnvWithDistance :: forall a. Symbol -> SEnv a -> SESearch a
lookupSEnvWithDistance Symbol
x (SE HashMap Symbol a
env)
  = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol a
env of
     Just a
z  -> forall a. a -> SESearch a
Found a
z
     Maybe a
Nothing -> forall a. [Symbol] -> SESearch a
Alts forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
alts
  where
    alts :: [String]
alts       = forall {a} {a}. Ord a => [(a, a)] -> [a]
takeMin forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Eq a => [a] -> [a] -> Int
editDistance String
x' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ss) [String]
ss
    ss :: [String]
ss         = Symbol -> String
symbolString 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
<$> forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol a
env
    x' :: String
x'         = Symbol -> String
symbolString Symbol
x
    takeMin :: [(a, a)] -> [a]
takeMin [(a, a)]
xs = [a
z | (a
d, a
z) <- [(a, a)]
xs, a
d forall a. Eq a => a -> a -> Bool
== forall {t :: * -> *} {c} {b}.
(Foldable t, Ord c, Functor t) =>
t (c, b) -> c
getMin [(a, a)]
xs]
    getMin :: t (c, b) -> c
getMin     = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum 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
<$>)


data SESearch a = Found a | Alts [Symbol]

-- | Functions for Indexed Bind Environment

instance Semigroup IBindEnv where
  (FB HashSet Int
e1) <> :: IBindEnv -> IBindEnv -> IBindEnv
<> (FB HashSet Int
e2) = HashSet Int -> IBindEnv
FB (HashSet Int
e1 forall a. Semigroup a => a -> a -> a
<> HashSet Int
e2)

instance Monoid IBindEnv where
  mempty :: IBindEnv
mempty  = IBindEnv
emptyIBindEnv
  mappend :: IBindEnv -> IBindEnv -> IBindEnv
mappend = forall a. Semigroup a => a -> a -> a
(<>)

emptyIBindEnv :: IBindEnv
emptyIBindEnv :: IBindEnv
emptyIBindEnv = HashSet Int -> IBindEnv
FB forall a. HashSet a
S.empty

deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
deleteIBindEnv :: Int -> IBindEnv -> IBindEnv
deleteIBindEnv Int
i (FB HashSet Int
s) = HashSet Int -> IBindEnv
FB (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.delete Int
i HashSet Int
s)

memberIBindEnv :: BindId -> IBindEnv -> Bool
memberIBindEnv :: Int -> IBindEnv -> Bool
memberIBindEnv Int
i (FB HashSet Int
s) = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Int
i HashSet Int
s

insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv :: [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int]
is (FB HashSet Int
s) = HashSet Int -> IBindEnv
FB (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert HashSet Int
s [Int]
is)

elemsIBindEnv :: IBindEnv -> [BindId]
elemsIBindEnv :: IBindEnv -> [Int]
elemsIBindEnv (FB HashSet Int
s) = forall a. HashSet a -> [a]
S.toList HashSet Int
s

fromListIBindEnv :: [BindId] -> IBindEnv
fromListIBindEnv :: [Int] -> IBindEnv
fromListIBindEnv = HashSet Int -> IBindEnv
FB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList

-- | Functions for Global Binder Environment
insertBindEnv :: Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv :: forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
insertBindEnv Symbol
x SortedReft
r a
a (BE Int
n BindMap (Symbol, SortedReft, a)
m) = (Int
n, forall a. Int -> BindMap a -> SizedEnv a
BE (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Int
n (Symbol
x, SortedReft
r, a
a) BindMap (Symbol, SortedReft, a)
m))

fromListBindEnv :: [(BindId, (Symbol, SortedReft, a))] -> BindEnv a
fromListBindEnv :: forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
fromListBindEnv [(Int, (Symbol, SortedReft, a))]
xs = forall a. Int -> BindMap a -> SizedEnv a
BE (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, (Symbol, SortedReft, a))]
xs) (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int, (Symbol, SortedReft, a))]
xs)

emptyBindEnv :: BindEnv a
emptyBindEnv :: forall a. BindEnv a
emptyBindEnv = forall a. Int -> BindMap a -> SizedEnv a
BE Int
0 forall k v. HashMap k v
M.empty

filterBindEnv   :: (BindId -> Symbol -> SortedReft -> Bool) -> BindEnv a -> BindEnv a
filterBindEnv :: forall a.
(Int -> Symbol -> SortedReft -> Bool) -> BindEnv a -> BindEnv a
filterBindEnv Int -> Symbol -> SortedReft -> Bool
f (BE Int
n BindMap (Symbol, SortedReft, a)
be) = forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\ Int
n' (Symbol
x, SortedReft
r, a
_) -> Int -> Symbol -> SortedReft -> Bool
f Int
n' Symbol
x SortedReft
r) BindMap (Symbol, SortedReft, a)
be)

bindEnvFromList :: [(BindId, (Symbol, SortedReft, a))] -> BindEnv a
bindEnvFromList :: forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
bindEnvFromList [] = forall a. BindEnv a
emptyBindEnv
bindEnvFromList [(Int, (Symbol, SortedReft, a))]
bs = forall a. Int -> BindMap a -> SizedEnv a
BE (Int
1 forall a. Num a => a -> a -> a
+ Int
maxId) HashMap Int (Symbol, SortedReft, a)
be
  where
    maxId :: Int
maxId          = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Int
n | (Int
n,(Symbol
_,SortedReft
_,a
_)) <- [(Int, (Symbol, SortedReft, a))]
bs ]
    be :: HashMap Int (Symbol, SortedReft, a)
be             = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int, (Symbol, SortedReft, a))]
bs

elemsBindEnv :: BindEnv a -> [BindId]
elemsBindEnv :: forall a. BindEnv a -> [Int]
elemsBindEnv BindEnv a
be = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
bindEnvToList BindEnv a
be

bindEnvToList :: BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
bindEnvToList :: forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
bindEnvToList (BE Int
_ BindMap (Symbol, SortedReft, a)
be) = forall k v. HashMap k v -> [(k, v)]
M.toList BindMap (Symbol, SortedReft, a)
be

mapBindEnv :: (BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)) -> BindEnv a -> BindEnv a
mapBindEnv :: forall a.
(Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f (BE Int
n BindMap (Symbol, SortedReft, a)
m) = forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f BindMap (Symbol, SortedReft, a)
m)
  -- where
    -- f' k (x, y, a) = let (x', y') = f k (x, y) in (x', y', a)

-- (\i z -> tracepp (msg i z) $ f z) m
--  where
--    msg i z = "beMap " ++ show i ++ " " ++ show z

mapWithKeyMBindEnv :: (Monad m) => ((BindId, (Symbol, SortedReft)) -> m (BindId, (Symbol, SortedReft))) -> BindEnv a -> m (BindEnv a)
mapWithKeyMBindEnv :: forall (m :: * -> *) a.
Monad m =>
((Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft)))
-> BindEnv a -> m (BindEnv a)
mapWithKeyMBindEnv (Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft))
f (BE Int
n BindMap (Symbol, SortedReft, a)
m) = forall a. Int -> BindMap a -> SizedEnv a
BE Int
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int, (Symbol, SortedReft, a)) -> m (Int, (Symbol, SortedReft, a))
f' (forall k v. HashMap k v -> [(k, v)]
M.toList BindMap (Symbol, SortedReft, a)
m)
  where
    f' :: (Int, (Symbol, SortedReft, a)) -> m (Int, (Symbol, SortedReft, a))
f' (Int
k, (Symbol
x, SortedReft
y, a
a)) = do { (Int
k', (Symbol
x', SortedReft
y')) <- (Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft))
f (Int
k, (Symbol
x, SortedReft
y)) ; forall (m :: * -> *) a. Monad m => a -> m a
return (Int
k', (Symbol
x', SortedReft
y', a
a)) }

lookupBindEnv :: BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv :: forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
k (BE Int
_ BindMap (Symbol, SortedReft, a)
m) = forall a. a -> Maybe a -> a
fromMaybe (Symbol, SortedReft, a)
err (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
k BindMap (Symbol, SortedReft, a)
m)
  where
    err :: (Symbol, SortedReft, a)
err                  = forall a. (?callStack::CallStack) => String -> a
errorstar forall a b. (a -> b) -> a -> b
$ String
"lookupBindEnv: cannot find binder" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
k

filterIBindEnv :: (BindId -> Bool) -> IBindEnv -> IBindEnv
filterIBindEnv :: (Int -> Bool) -> IBindEnv -> IBindEnv
filterIBindEnv Int -> Bool
f (FB HashSet Int
m) = HashSet Int -> IBindEnv
FB (forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter Int -> Bool
f HashSet Int
m)

unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv (FB HashSet Int
m1) (FB HashSet Int
m2) = HashSet Int -> IBindEnv
FB forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Int
m2

unionsIBindEnv :: [IBindEnv] -> IBindEnv
unionsIBindEnv :: [IBindEnv] -> IBindEnv
unionsIBindEnv = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv IBindEnv
emptyIBindEnv

intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv (FB HashSet Int
m1) (FB HashSet Int
m2) = HashSet Int -> IBindEnv
FB forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.intersection` HashSet Int
m2

nullIBindEnv :: IBindEnv -> Bool
nullIBindEnv :: IBindEnv -> Bool
nullIBindEnv (FB HashSet Int
m) = forall a. HashSet a -> Bool
S.null HashSet Int
m

diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
diffIBindEnv (FB HashSet Int
m1) (FB HashSet Int
m2) = HashSet Int -> IBindEnv
FB forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` HashSet Int
m2

adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv a -> BindEnv a
adjustBindEnv :: forall a.
((Symbol, SortedReft) -> (Symbol, SortedReft))
-> Int -> BindEnv a -> BindEnv a
adjustBindEnv (Symbol, SortedReft) -> (Symbol, SortedReft)
f Int
i (BE Int
n BindMap (Symbol, SortedReft, a)
m) = forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f' Int
i BindMap (Symbol, SortedReft, a)
m)
  where
    f' :: (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f'  (Symbol
x, SortedReft
y, a
a) = let (Symbol
x', SortedReft
y') = (Symbol, SortedReft) -> (Symbol, SortedReft)
f (Symbol
x, SortedReft
y) in (Symbol
x', SortedReft
y', a
a)


deleteBindEnv :: BindId -> BindEnv a -> BindEnv a
deleteBindEnv :: forall a. Int -> BindEnv a -> BindEnv a
deleteBindEnv Int
i (BE Int
n BindMap (Symbol, SortedReft, a)
m) = forall a. Int -> BindMap a -> SizedEnv a
BE Int
n forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Int
i BindMap (Symbol, SortedReft, a)
m

instance Functor SEnv where
  fmap :: forall a b. (a -> b) -> SEnv a -> SEnv b
fmap = forall a b. (a -> b) -> SEnv a -> SEnv b
mapSEnv

instance Fixpoint (EBindEnv a) where
  toFix :: EBindEnv a -> Doc
toFix (EB (BE Int
_ BindMap (Symbol, SortedReft, a)
m)) = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {c}.
(Fixpoint a, Fixpoint a) =>
(a, (a, SortedReft, c)) -> Doc
toFixBind forall a b. (a -> b) -> a -> b
$ forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList BindMap (Symbol, SortedReft, a)
m
    where
      toFixBind :: (a, (a, SortedReft, c)) -> Doc
toFixBind (a
i, (a
x, SortedReft
r, c
_)) = Doc
"ebind" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
i Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
x Doc -> Doc -> Doc
<+> Doc
": { " Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (SortedReft -> Sort
sr_sort SortedReft
r) Doc -> Doc -> Doc
<+> Doc
" }"

instance Fixpoint (BindEnv a) where
  toFix :: BindEnv a -> Doc
toFix (BE Int
_ BindMap (Symbol, SortedReft, a)
m) = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {a} {c}.
(Fixpoint a, Fixpoint a, Fixpoint a) =>
(a, (a, a, c)) -> Doc
toFixBind forall a b. (a -> b) -> a -> b
$ forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList BindMap (Symbol, SortedReft, a)
m
    where
      toFixBind :: (a, (a, a, c)) -> Doc
toFixBind (a
i, (a
x, a
r, c
_)) = Doc
"bind" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
i Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
r

instance (Fixpoint a) => Fixpoint (SEnv a) where
   toFix :: SEnv a -> Doc
toFix (SE HashMap Symbol a
m)   = forall a. Fixpoint a => a -> Doc
toFix (forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList HashMap Symbol a
m)

instance Fixpoint (SEnv a) => Show (SEnv a) where
  show :: SEnv a -> String
show = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix

instance Semigroup (SEnv a) where
  SEnv a
s1 <> :: SEnv a -> SEnv a -> SEnv a
<> SEnv a
s2 = forall a. HashMap Symbol a -> SEnv a
SE forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union (forall a. SEnv a -> HashMap Symbol a
seBinds SEnv a
s1) (forall a. SEnv a -> HashMap Symbol a
seBinds SEnv a
s2)

instance Monoid (SEnv a) where
  mempty :: SEnv a
mempty        = forall a. HashMap Symbol a -> SEnv a
SE forall k v. HashMap k v
M.empty

instance Semigroup (BindEnv a) where
  (BE Int
0 BindMap (Symbol, SortedReft, a)
_) <> :: BindEnv a -> BindEnv a -> BindEnv a
<> BindEnv a
b        = BindEnv a
b
  BindEnv a
b        <> (BE Int
0 BindMap (Symbol, SortedReft, a)
_) = BindEnv a
b
  BindEnv a
_        <> BindEnv a
_        = forall a. (?callStack::CallStack) => String -> a
errorstar String
"mappend on non-trivial BindEnvs"

instance Monoid (BindEnv a) where
  mempty :: BindEnv a
mempty  = forall a. Int -> BindMap a -> SizedEnv a
BE Int
0 forall k v. HashMap k v
M.empty
  mappend :: BindEnv a -> BindEnv a -> BindEnv a
mappend = forall a. Semigroup a => a -> a -> a
(<>)

envCs :: BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs :: forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be IBindEnv
env = [(Symbol
x, SortedReft
y) | Int
i <- IBindEnv -> [Int]
elemsIBindEnv IBindEnv
env, let (Symbol
x, SortedReft
y, a
_) = forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
be]

instance Fixpoint IBindEnv where
  toFix :: IBindEnv -> Doc
toFix (FB HashSet Int
ids) = String -> Doc
text String
"env" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix HashSet Int
ids

--------------------------------------------------------------------------------

instance NFData Packs
instance NFData IBindEnv
instance NFData a => NFData (BindEnv a)
instance (NFData a) => NFData (SEnv a)

instance S.Store Packs
instance S.Store IBindEnv
instance (S.Store a) => S.Store (BindEnv a)
instance (S.Store a) => S.Store (SEnv a)
-- instance (Hashable a, Eq a, S.Store a) => S.Store (S.HashSet a) where
--   put = B.put . S.toList
--   get = S.fromList <$> B.get

--------------------------------------------------------------------------------
-- | Constraint Pack Sets ------------------------------------------------------
--------------------------------------------------------------------------------

newtype Packs = Packs { Packs -> HashMap KVar Int
packm :: M.HashMap KVar Int }
               deriving (Packs -> Packs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Packs -> Packs -> Bool
$c/= :: Packs -> Packs -> Bool
== :: Packs -> Packs -> Bool
$c== :: Packs -> Packs -> Bool
Eq, Int -> Packs -> ShowS
[Packs] -> ShowS
Packs -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Packs] -> ShowS
$cshowList :: [Packs] -> ShowS
show :: Packs -> String
$cshow :: Packs -> String
showsPrec :: Int -> Packs -> ShowS
$cshowsPrec :: Int -> Packs -> ShowS
Show, forall x. Rep Packs x -> Packs
forall x. Packs -> Rep Packs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Packs x -> Packs
$cfrom :: forall x. Packs -> Rep Packs x
Generic)

instance Fixpoint Packs where
  toFix :: Packs -> Doc
toFix (Packs HashMap KVar Int
m) = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ (Doc
"pack" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, Int)]
kIs
    where
      kIs :: [(KVar, Int)]
kIs = forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ HashMap KVar Int
m

instance PPrint Packs where
  pprintTidy :: Tidy -> Packs -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix

instance Semigroup Packs where
  Packs
m1 <> :: Packs -> Packs -> Packs
<> Packs
m2 = HashMap KVar Int -> Packs
Packs forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union (Packs -> HashMap KVar Int
packm Packs
m1) (Packs -> HashMap KVar Int
packm Packs
m2)

instance Monoid Packs where
  mempty :: Packs
mempty  = HashMap KVar Int -> Packs
Packs forall a. Monoid a => a
mempty
  mappend :: Packs -> Packs -> Packs
mappend = forall a. Semigroup a => a -> a -> a
(<>)

getPack :: KVar -> Packs -> Maybe Int
getPack :: KVar -> Packs -> Maybe Int
getPack KVar
k (Packs HashMap KVar Int
m) = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k HashMap KVar Int
m

makePack :: [S.HashSet KVar] -> Packs
makePack :: [HashSet KVar] -> Packs
makePack [HashSet KVar]
kvss = HashMap KVar Int -> Packs
Packs (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, Int)]
kIs)
  where
    kIs :: [(KVar, Int)]
kIs       = [ (KVar
k, Int
i) | (Int
i, ListNE KVar
ks) <- [(Int, ListNE KVar)]
kPacks, KVar
k <- ListNE KVar
ks ]
    kPacks :: [(Int, ListNE KVar)]
kPacks    = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. EqHash v => [ListNE v] -> [ListNE v]
coalesce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HashSet a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ [HashSet KVar]
kvss