{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# 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
  , diffIBindEnv
  , intersectionIBindEnv
  , nullIBindEnv
  , filterIBindEnv

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

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

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

-- import qualified Data.Binary as B
import qualified Data.Binary as B
import qualified Data.List   as L
import           Data.Generics             (Data)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import           Data.Hashable
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
(IBindEnv -> IBindEnv -> Bool)
-> (IBindEnv -> IBindEnv -> Bool) -> Eq IBindEnv
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
DataType
Constr
Typeable IBindEnv
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> IBindEnv -> c IBindEnv)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c IBindEnv)
-> (IBindEnv -> Constr)
-> (IBindEnv -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> IBindEnv -> IBindEnv)
-> (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 u. (forall d. Data d => d -> u) -> IBindEnv -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv)
-> Data IBindEnv
IBindEnv -> DataType
IBindEnv -> Constr
(forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cFB :: Constr
$tIBindEnv :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
gmapQ :: (forall d. Data d => d -> u) -> IBindEnv -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable IBindEnv
Data, Typeable, (forall x. IBindEnv -> Rep IBindEnv x)
-> (forall x. Rep IBindEnv x -> IBindEnv) -> Generic IBindEnv
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
_ = [Int] -> Doc
forall a. PPrint a => a -> Doc
pprint ([Int] -> Doc) -> (IBindEnv -> [Int]) -> IBindEnv -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort ([Int] -> [Int]) -> (IBindEnv -> [Int]) -> IBindEnv -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> [Int]
elemsIBindEnv

newtype SEnv a     = SE { SEnv a -> HashMap Symbol a
seBinds :: M.HashMap Symbol a }
                     deriving (SEnv a -> SEnv a -> Bool
(SEnv a -> SEnv a -> Bool)
-> (SEnv a -> SEnv a -> Bool) -> Eq (SEnv a)
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, Typeable (SEnv a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SEnv a))
-> (SEnv a -> Constr)
-> (SEnv a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SEnv a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a)))
-> ((forall b. Data b => b -> b) -> SEnv a -> SEnv a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SEnv a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SEnv a -> r)
-> (forall u. (forall d. Data d => d -> u) -> SEnv a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SEnv a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a))
-> Data (SEnv a)
SEnv a -> DataType
SEnv a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
(forall b. Data b => b -> b) -> SEnv a -> SEnv a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> c (SEnv a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
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 u. Int -> (forall d. Data d => d -> u) -> SEnv a -> u
forall u. (forall d. Data d => d -> u) -> SEnv a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a))
$cSE :: Constr
$tSEnv :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> SEnv a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> SEnv a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (SEnv a)
Data, Typeable, (forall x. SEnv a -> Rep (SEnv a) x)
-> (forall x. Rep (SEnv a) x -> SEnv a) -> Generic (SEnv a)
forall x. Rep (SEnv a) x -> SEnv a
forall x. SEnv a -> Rep (SEnv a) x
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, a -> SEnv a -> Bool
SEnv m -> m
SEnv a -> [a]
SEnv a -> Bool
SEnv a -> Int
SEnv a -> a
SEnv a -> a
SEnv a -> a
SEnv a -> a
(a -> m) -> SEnv a -> m
(a -> m) -> SEnv a -> m
(a -> b -> b) -> b -> SEnv a -> b
(a -> b -> b) -> b -> SEnv a -> b
(b -> a -> b) -> b -> SEnv a -> b
(b -> a -> b) -> b -> SEnv a -> b
(a -> a -> a) -> SEnv a -> a
(a -> a -> a) -> SEnv a -> a
(forall m. Monoid m => SEnv m -> m)
-> (forall m a. Monoid m => (a -> m) -> SEnv a -> m)
-> (forall m a. Monoid m => (a -> m) -> SEnv a -> m)
-> (forall a b. (a -> b -> b) -> b -> SEnv a -> b)
-> (forall a b. (a -> b -> b) -> b -> SEnv a -> b)
-> (forall b a. (b -> a -> b) -> b -> SEnv a -> b)
-> (forall b a. (b -> a -> b) -> b -> SEnv a -> b)
-> (forall a. (a -> a -> a) -> SEnv a -> a)
-> (forall a. (a -> a -> a) -> SEnv a -> a)
-> (forall a. SEnv a -> [a])
-> (forall a. SEnv a -> Bool)
-> (forall a. SEnv a -> Int)
-> (forall a. Eq a => a -> SEnv a -> Bool)
-> (forall a. Ord a => SEnv a -> a)
-> (forall a. Ord a => SEnv a -> a)
-> (forall a. Num a => SEnv a -> a)
-> (forall a. Num a => SEnv a -> a)
-> Foldable SEnv
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 :: SEnv a -> a
$cproduct :: forall a. Num a => SEnv a -> a
sum :: SEnv a -> a
$csum :: forall a. Num a => SEnv a -> a
minimum :: SEnv a -> a
$cminimum :: forall a. Ord a => SEnv a -> a
maximum :: SEnv a -> a
$cmaximum :: forall a. Ord a => SEnv a -> a
elem :: a -> SEnv a -> Bool
$celem :: forall a. Eq a => a -> SEnv a -> Bool
length :: SEnv a -> Int
$clength :: forall a. SEnv a -> Int
null :: SEnv a -> Bool
$cnull :: forall a. SEnv a -> Bool
toList :: SEnv a -> [a]
$ctoList :: forall a. SEnv a -> [a]
foldl1 :: (a -> a -> a) -> SEnv a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldr1 :: (a -> a -> a) -> SEnv a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldl' :: (b -> a -> b) -> b -> SEnv a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
foldl :: (b -> a -> b) -> b -> SEnv a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
foldr' :: (a -> b -> b) -> b -> SEnv a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
foldr :: (a -> b -> b) -> b -> SEnv a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SEnv a -> b
foldMap' :: (a -> m) -> SEnv a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
foldMap :: (a -> m) -> SEnv a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
fold :: SEnv m -> m
$cfold :: forall m. Monoid m => SEnv m -> m
Foldable, Functor SEnv
Foldable SEnv
Functor SEnv
-> Foldable SEnv
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SEnv a -> f (SEnv b))
-> (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 (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a))
-> Traversable SEnv
(a -> f b) -> SEnv a -> f (SEnv 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 => 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 :: SEnv (m a) -> m (SEnv a)
$csequence :: forall (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a)
mapM :: (a -> m b) -> SEnv a -> m (SEnv b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
sequenceA :: SEnv (f a) -> f (SEnv a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
traverse :: (a -> f b) -> SEnv a -> f (SEnv b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
$cp2Traversable :: Foldable SEnv
$cp1Traversable :: Functor SEnv
Traversable)

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

instance PPrint a => PPrint (SizedEnv a) where
  pprintTidy :: Tidy -> SizedEnv a -> Doc
pprintTidy Tidy
k (BE Int
_ BindMap a
m) = Tidy -> BindMap a -> Doc
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       = SizedEnv (Symbol, SortedReft)
newtype EBindEnv   = EB BindEnv

splitByQuantifiers :: BindEnv -> [BindId] -> (BindEnv, EBindEnv)
splitByQuantifiers :: BindEnv -> [Int] -> (BindEnv, EBindEnv)
splitByQuantifiers (BE Int
i BindMap (Symbol, SortedReft)
bs) [Int]
ebs = ( Int -> BindMap (Symbol, SortedReft) -> BindEnv
forall a. Int -> BindMap a -> SizedEnv a
BE Int
i (BindMap (Symbol, SortedReft) -> BindEnv)
-> BindMap (Symbol, SortedReft) -> BindEnv
forall a b. (a -> b) -> a -> b
$ (Int -> (Symbol, SortedReft) -> Bool)
-> BindMap (Symbol, SortedReft) -> BindMap (Symbol, SortedReft)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft)
_ -> Bool -> Bool
not (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
k [Int]
ebs)) BindMap (Symbol, SortedReft)
bs
                                   , BindEnv -> EBindEnv
EB (BindEnv -> EBindEnv) -> BindEnv -> EBindEnv
forall a b. (a -> b) -> a -> b
$ Int -> BindMap (Symbol, SortedReft) -> BindEnv
forall a. Int -> BindMap a -> SizedEnv a
BE Int
i (BindMap (Symbol, SortedReft) -> BindEnv)
-> BindMap (Symbol, SortedReft) -> BindEnv
forall a b. (a -> b) -> a -> b
$ (Int -> (Symbol, SortedReft) -> Bool)
-> BindMap (Symbol, SortedReft) -> BindMap (Symbol, SortedReft)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft)
_ -> Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
k [Int]
ebs) BindMap (Symbol, SortedReft)
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 = Tidy -> [(Symbol, a)] -> Doc
forall k v. (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
pprintKVs Tidy
k ([(Symbol, a)] -> Doc)
-> (SEnv a -> [(Symbol, a)]) -> SEnv a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, a) -> (Symbol, a) -> Ordering)
-> [(Symbol, a)] -> [(Symbol, a)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Symbol -> Symbol -> Ordering)
-> ((Symbol, a) -> Symbol)
-> (Symbol, a)
-> (Symbol, a)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Symbol, a) -> Symbol
forall a b. (a, b) -> a
fst) ([(Symbol, a)] -> [(Symbol, a)])
-> (SEnv a -> [(Symbol, a)]) -> SEnv a -> [(Symbol, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv a -> [(Symbol, a)]
forall a. SEnv a -> [(Symbol, a)]
toListSEnv

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

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

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

mapSEnv                 :: (a -> b) -> SEnv a -> SEnv b
mapSEnv :: (a -> b) -> SEnv a -> SEnv b
mapSEnv a -> b
f (SE HashMap Symbol a
env)      = HashMap Symbol b -> SEnv b
forall a. HashMap Symbol a -> SEnv a
SE ((a -> b) -> HashMap Symbol a -> HashMap Symbol b
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 :: (a -> m b) -> SEnv a -> m (SEnv b)
mapMSEnv a -> m b
f SEnv a
env          = [(Symbol, b)] -> SEnv b
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, b)] -> SEnv b) -> m [(Symbol, b)] -> m (SEnv b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, a) -> m (Symbol, b)) -> [(Symbol, a)] -> m [(Symbol, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((a -> m b) -> (Symbol, a) -> m (Symbol, b)
forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
secondM a -> m b
f) (SEnv a -> [(Symbol, a)]
forall a. SEnv a -> [(Symbol, a)]
toListSEnv SEnv a
env)

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

deleteSEnv :: Symbol -> SEnv a -> SEnv a
deleteSEnv :: Symbol -> SEnv a -> SEnv a
deleteSEnv Symbol
x (SE HashMap Symbol a
env)   = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE (Symbol -> HashMap Symbol a -> HashMap Symbol a
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 :: Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x a
v (SE HashMap Symbol a
env) = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE (Symbol -> a -> HashMap Symbol a -> HashMap Symbol a
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)

lookupSEnv :: Symbol -> SEnv a -> Maybe a
lookupSEnv :: Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x (SE HashMap Symbol a
env)   = Symbol -> HashMap Symbol a -> Maybe a
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 :: SEnv a
emptySEnv               = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE HashMap Symbol a
forall k v. HashMap k v
M.empty

memberSEnv :: Symbol -> SEnv a -> Bool
memberSEnv :: Symbol -> SEnv a -> Bool
memberSEnv Symbol
x (SE HashMap Symbol a
env)   = Symbol -> HashMap Symbol a -> Bool
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 :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
intersectWithSEnv v1 -> v2 -> a
f (SE HashMap Symbol v1
m1) (SE HashMap Symbol v2
m2) = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE ((v1 -> v2 -> a)
-> HashMap Symbol v1 -> HashMap Symbol v2 -> HashMap Symbol a
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 :: SEnv a -> SEnv w -> SEnv a
differenceSEnv (SE HashMap Symbol a
m1) (SE HashMap Symbol w
m2) = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE (HashMap Symbol a -> HashMap Symbol w -> HashMap Symbol a
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 :: (a -> Bool) -> SEnv a -> SEnv a
filterSEnv a -> Bool
f (SE HashMap Symbol a
m)     = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE ((a -> Bool) -> HashMap Symbol a -> HashMap Symbol a
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 :: SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv (SE HashMap Symbol a
m1) HashMap Symbol a
m2    = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE (HashMap Symbol a -> HashMap Symbol a -> HashMap Symbol a
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' :: SEnv a -> SEnv a -> SEnv a
unionSEnv' (SE HashMap Symbol a
m1) (SE HashMap Symbol a
m2)    = HashMap Symbol a -> SEnv a
forall a. HashMap Symbol a -> SEnv a
SE (HashMap Symbol a -> HashMap Symbol a -> HashMap Symbol a
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)

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

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

emptyIBindEnv :: IBindEnv
emptyIBindEnv :: IBindEnv
emptyIBindEnv = HashSet Int -> IBindEnv
FB HashSet Int
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 (Int -> HashSet Int -> HashSet Int
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) = Int -> HashSet Int -> Bool
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 ((Int -> HashSet Int -> HashSet Int)
-> HashSet Int -> [Int] -> HashSet Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Int -> HashSet Int -> HashSet Int
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) = HashSet Int -> [Int]
forall a. HashSet a -> [a]
S.toList HashSet Int
s

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

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

emptyBindEnv :: BindEnv
emptyBindEnv :: BindEnv
emptyBindEnv = Int -> BindMap (Symbol, SortedReft) -> BindEnv
forall a. Int -> BindMap a -> SizedEnv a
BE Int
0 BindMap (Symbol, SortedReft)
forall k v. HashMap k v
M.empty

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

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

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

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

mapBindEnv :: (BindId -> (Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
mapBindEnv :: (Int -> (Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindEnv -> BindEnv
mapBindEnv Int -> (Symbol, SortedReft) -> (Symbol, SortedReft)
f (BE Int
n BindMap (Symbol, SortedReft)
m) = Int -> BindMap (Symbol, SortedReft) -> BindEnv
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (BindMap (Symbol, SortedReft) -> BindEnv)
-> BindMap (Symbol, SortedReft) -> BindEnv
forall a b. (a -> b) -> a -> b
$ (Int -> (Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindMap (Symbol, SortedReft) -> BindMap (Symbol, SortedReft)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey Int -> (Symbol, SortedReft) -> (Symbol, SortedReft)
f BindMap (Symbol, SortedReft)
m
-- (\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 -> m BindEnv
mapWithKeyMBindEnv :: ((Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft)))
-> BindEnv -> m BindEnv
mapWithKeyMBindEnv (Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft))
f (BE Int
n BindMap (Symbol, SortedReft)
m) = (Int -> BindMap (Symbol, SortedReft) -> BindEnv
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (BindMap (Symbol, SortedReft) -> BindEnv)
-> ([(Int, (Symbol, SortedReft))] -> BindMap (Symbol, SortedReft))
-> [(Int, (Symbol, SortedReft))]
-> BindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, (Symbol, SortedReft))] -> BindMap (Symbol, SortedReft)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList) ([(Int, (Symbol, SortedReft))] -> BindEnv)
-> m [(Int, (Symbol, SortedReft))] -> m BindEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft)))
-> [(Int, (Symbol, SortedReft))] -> m [(Int, (Symbol, SortedReft))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft))
f (BindMap (Symbol, SortedReft) -> [(Int, (Symbol, SortedReft))]
forall k v. HashMap k v -> [(k, v)]
M.toList BindMap (Symbol, SortedReft)
m)

lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv :: Int -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv Int
k (BE Int
_ BindMap (Symbol, SortedReft)
m) = (Symbol, SortedReft)
-> Maybe (Symbol, SortedReft) -> (Symbol, SortedReft)
forall a. a -> Maybe a -> a
fromMaybe (Symbol, SortedReft)
err (Int -> BindMap (Symbol, SortedReft) -> Maybe (Symbol, SortedReft)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
k BindMap (Symbol, SortedReft)
m)
  where
    err :: (Symbol, SortedReft)
err                  = String -> (Symbol, SortedReft)
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> (Symbol, SortedReft)) -> String -> (Symbol, SortedReft)
forall a b. (a -> b) -> a -> b
$ String
"lookupBindEnv: cannot find binder" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
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 ((Int -> Bool) -> HashSet Int -> HashSet Int
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 (HashSet Int -> IBindEnv) -> HashSet Int -> IBindEnv
forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 HashSet Int -> HashSet Int -> HashSet Int
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Int
m2

intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv (FB HashSet Int
m1) (FB HashSet Int
m2) = HashSet Int -> IBindEnv
FB (HashSet Int -> IBindEnv) -> HashSet Int -> IBindEnv
forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 HashSet Int -> HashSet Int -> HashSet Int
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) = HashSet Int -> Bool
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 (HashSet Int -> IBindEnv) -> HashSet Int -> IBindEnv
forall a b. (a -> b) -> a -> b
$ HashSet Int
m1 HashSet Int -> HashSet Int -> HashSet Int
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` HashSet Int
m2

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

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

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

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

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

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

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

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

envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv
be IBindEnv
env = [Int -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv Int
i BindEnv
be | Int
i <- IBindEnv -> [Int]
elemsIBindEnv IBindEnv
env]

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

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

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

instance B.Binary Packs
instance B.Binary IBindEnv
instance B.Binary BindEnv
instance (B.Binary a) => B.Binary (SEnv a)
instance (Hashable a, Eq a, B.Binary a) => B.Binary (S.HashSet a) where
  put :: HashSet a -> Put
put = [a] -> Put
forall t. Binary t => t -> Put
B.put ([a] -> Put) -> (HashSet a -> [a]) -> HashSet a -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> [a]
forall a. HashSet a -> [a]
S.toList
  get :: Get (HashSet a)
get = [a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([a] -> HashSet a) -> Get [a] -> Get (HashSet a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [a]
forall t. Binary t => Get t
B.get

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

newtype Packs = Packs { Packs -> HashMap KVar Int
packm :: M.HashMap KVar Int }
               deriving (Packs -> Packs -> Bool
(Packs -> Packs -> Bool) -> (Packs -> Packs -> Bool) -> Eq Packs
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
(Int -> Packs -> ShowS)
-> (Packs -> String) -> ([Packs] -> ShowS) -> Show Packs
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. Packs -> Rep Packs x)
-> (forall x. Rep Packs x -> Packs) -> Generic Packs
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Doc
"pack" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> ((KVar, Int) -> Doc) -> (KVar, Int) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, Int) -> Doc
forall a. Fixpoint a => a -> Doc
toFix) ((KVar, Int) -> Doc) -> [(KVar, Int)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, Int)]
kIs
    where
      kIs :: [(KVar, Int)]
kIs = ((KVar, Int) -> (KVar, Int) -> Ordering)
-> [(KVar, Int)] -> [(KVar, Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((KVar, Int) -> Int) -> (KVar, Int) -> (KVar, Int) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (KVar, Int) -> Int
forall a b. (a, b) -> b
snd) ([(KVar, Int)] -> [(KVar, Int)])
-> (HashMap KVar Int -> [(KVar, Int)])
-> HashMap KVar Int
-> [(KVar, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap KVar Int -> [(KVar, Int)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap KVar Int -> [(KVar, Int)])
-> HashMap KVar Int -> [(KVar, Int)]
forall a b. (a -> b) -> a -> b
$ HashMap KVar Int
m

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

instance Semigroup Packs where
  Packs
m1 <> :: Packs -> Packs -> Packs
<> Packs
m2 = HashMap KVar Int -> Packs
Packs (HashMap KVar Int -> Packs) -> HashMap KVar Int -> Packs
forall a b. (a -> b) -> a -> b
$ HashMap KVar Int -> HashMap KVar Int -> HashMap KVar Int
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 HashMap KVar Int
forall a. Monoid a => a
mempty
  mappend :: Packs -> Packs -> Packs
mappend = Packs -> Packs -> Packs
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) = KVar -> HashMap KVar Int -> Maybe Int
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 ([(KVar, Int)] -> HashMap KVar Int
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    = [Int] -> [ListNE KVar] -> [(Int, ListNE KVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([ListNE KVar] -> [(Int, ListNE KVar)])
-> ([HashSet KVar] -> [ListNE KVar])
-> [HashSet KVar]
-> [(Int, ListNE KVar)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ListNE KVar] -> [ListNE KVar]
forall v. EqHash v => [ListNE v] -> [ListNE v]
coalesce ([ListNE KVar] -> [ListNE KVar])
-> ([HashSet KVar] -> [ListNE KVar])
-> [HashSet KVar]
-> [ListNE KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashSet KVar -> ListNE KVar) -> [HashSet KVar] -> [ListNE KVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HashSet KVar -> ListNE KVar
forall a. HashSet a -> [a]
S.toList ([HashSet KVar] -> [(Int, ListNE KVar)])
-> [HashSet KVar] -> [(Int, ListNE KVar)]
forall a b. (a -> b) -> a -> b
$ [HashSet KVar]
kvss