{-# 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, bindEnvSize
  , filterBindEnv, mapBindEnv, mapWithKeyMBindEnv, adjustBindEnv
  , bindEnvFromList, bindEnvToList, deleteBindEnv, elemsBindEnv
  , EBindEnv, splitByQuantifiers

  , coerceBindEnv

  -- * 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.Config
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Sorts
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
$c== :: IBindEnv -> IBindEnv -> Bool
== :: IBindEnv -> IBindEnv -> Bool
$c/= :: IBindEnv -> IBindEnv -> Bool
/= :: IBindEnv -> IBindEnv -> Bool
Eq, Typeable IBindEnv
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 -> Constr
IBindEnv -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IBindEnv -> c IBindEnv
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IBindEnv
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IBindEnv
$ctoConstr :: IBindEnv -> Constr
toConstr :: IBindEnv -> Constr
$cdataTypeOf :: IBindEnv -> DataType
dataTypeOf :: IBindEnv -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IBindEnv)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IBindEnv)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv)
$cgmapT :: (forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
gmapT :: (forall b. Data b => b -> b) -> IBindEnv -> IBindEnv
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IBindEnv -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> IBindEnv -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IBindEnv -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv
Data, Int -> IBindEnv -> ShowS
[IBindEnv] -> ShowS
IBindEnv -> String
(Int -> IBindEnv -> ShowS)
-> (IBindEnv -> String) -> ([IBindEnv] -> ShowS) -> Show IBindEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IBindEnv -> ShowS
showsPrec :: Int -> IBindEnv -> ShowS
$cshow :: IBindEnv -> String
show :: IBindEnv -> String
$cshowList :: [IBindEnv] -> ShowS
showList :: [IBindEnv] -> ShowS
Show, 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
$cfrom :: forall x. IBindEnv -> Rep IBindEnv x
from :: forall x. IBindEnv -> Rep IBindEnv x
$cto :: forall x. Rep IBindEnv x -> IBindEnv
to :: forall x. Rep IBindEnv x -> IBindEnv
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 { forall a. 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
$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
/= :: SEnv a -> SEnv a -> Bool
Eq, Typeable (SEnv a)
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 -> Constr
SEnv a -> DataType
(forall b. Data b => b -> b) -> SEnv a -> SEnv a
forall a. Data a => Typeable (SEnv a)
forall a. Data a => SEnv a -> Constr
forall a. Data a => SEnv a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SEnv a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SEnv a)
$ctoConstr :: forall a. Data a => SEnv a -> Constr
toConstr :: SEnv a -> Constr
$cdataTypeOf :: forall a. Data a => SEnv a -> DataType
dataTypeOf :: SEnv a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SEnv a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> SEnv a -> SEnv a
gmapT :: (forall b. Data b => b -> b) -> SEnv a -> SEnv a
$cgmapQl :: 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
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> SEnv a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SEnv a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SEnv a -> m (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
$cfrom :: forall a x. SEnv a -> Rep (SEnv a) x
from :: forall x. SEnv a -> Rep (SEnv a) x
$cto :: forall a x. Rep (SEnv a) x -> SEnv a
to :: forall x. Rep (SEnv a) x -> SEnv a
Generic, (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
$cfold :: forall m. Monoid m => SEnv m -> m
fold :: forall m. Monoid m => SEnv m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> SEnv a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> SEnv a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldr1 :: forall a. (a -> a -> a) -> SEnv a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SEnv a -> a
foldl1 :: forall a. (a -> a -> a) -> SEnv a -> a
$ctoList :: forall a. SEnv a -> [a]
toList :: forall a. SEnv a -> [a]
$cnull :: forall a. SEnv a -> Bool
null :: forall a. SEnv a -> Bool
$clength :: forall a. SEnv a -> Int
length :: forall a. SEnv a -> Int
$celem :: forall a. Eq a => a -> SEnv a -> Bool
elem :: forall a. Eq a => a -> SEnv a -> Bool
$cmaximum :: forall a. Ord a => SEnv a -> a
maximum :: forall a. Ord a => SEnv a -> a
$cminimum :: forall a. Ord a => SEnv a -> a
minimum :: forall a. Ord a => SEnv a -> a
$csum :: forall a. Num a => SEnv a -> a
sum :: forall a. Num a => SEnv a -> a
$cproduct :: forall a. Num a => SEnv a -> a
product :: forall a. Num a => SEnv a -> a
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
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SEnv a -> f (SEnv b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
sequenceA :: forall (f :: * -> *) a. Applicative f => SEnv (f a) -> f (SEnv a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
$csequence :: forall (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a)
sequence :: forall (m :: * -> *) a. Monad m => SEnv (m a) -> m (SEnv a)
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
(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
$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
/= :: 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
$cshowsPrec :: forall a. Show a => Int -> SizedEnv a -> ShowS
showsPrec :: Int -> SizedEnv a -> ShowS
$cshow :: forall a. Show a => SizedEnv a -> String
show :: SizedEnv a -> String
$cshowList :: forall a. Show a => [SizedEnv a] -> ShowS
showList :: [SizedEnv a] -> ShowS
Show, (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
$cfmap :: forall a b. (a -> b) -> SizedEnv a -> SizedEnv b
fmap :: forall a b. (a -> b) -> SizedEnv a -> SizedEnv b
$c<$ :: forall a b. a -> SizedEnv b -> SizedEnv a
<$ :: forall a b. a -> SizedEnv b -> SizedEnv a
Functor, (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
$cfold :: forall m. Monoid m => SizedEnv m -> m
fold :: forall m. Monoid m => SizedEnv m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> SizedEnv a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> SizedEnv a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
foldr1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
foldl1 :: forall a. (a -> a -> a) -> SizedEnv a -> a
$ctoList :: forall a. SizedEnv a -> [a]
toList :: forall a. SizedEnv a -> [a]
$cnull :: forall a. SizedEnv a -> Bool
null :: forall a. SizedEnv a -> Bool
$clength :: forall a. SizedEnv a -> Int
length :: forall a. SizedEnv a -> Int
$celem :: forall a. Eq a => a -> SizedEnv a -> Bool
elem :: forall a. Eq a => a -> SizedEnv a -> Bool
$cmaximum :: forall a. Ord a => SizedEnv a -> a
maximum :: forall a. Ord a => SizedEnv a -> a
$cminimum :: forall a. Ord a => SizedEnv a -> a
minimum :: forall a. Ord a => SizedEnv a -> a
$csum :: forall a. Num a => SizedEnv a -> a
sum :: forall a. Num a => SizedEnv a -> a
$cproduct :: forall a. Num a => SizedEnv a -> a
product :: forall a. Num a => SizedEnv a -> a
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
$cfrom :: forall a x. SizedEnv a -> Rep (SizedEnv a) x
from :: forall x. SizedEnv a -> Rep (SizedEnv a) x
$cto :: forall a x. Rep (SizedEnv a) x -> SizedEnv a
to :: forall x. Rep (SizedEnv a) x -> SizedEnv a
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
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizedEnv a -> f (SizedEnv b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizedEnv a -> f (SizedEnv b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizedEnv (f a) -> f (SizedEnv a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizedEnv (f a) -> f (SizedEnv a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
$csequence :: forall (m :: * -> *) a. Monad m => SizedEnv (m a) -> m (SizedEnv a)
sequence :: forall (m :: * -> *) a. Monad m => SizedEnv (m a) -> m (SizedEnv a)
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 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 = ( Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
i (BindMap (Symbol, SortedReft, a)
 -> SizedEnv (Symbol, SortedReft, a))
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a b. (a -> b) -> a -> b
$ (Int -> (Symbol, SortedReft, a) -> Bool)
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft, a)
_ -> Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Int
k [Int]
ebs) BindMap (Symbol, SortedReft, a)
bs
                                   , SizedEnv (Symbol, SortedReft, a) -> EBindEnv a
forall a. BindEnv a -> EBindEnv a
EB (SizedEnv (Symbol, SortedReft, a) -> EBindEnv a)
-> SizedEnv (Symbol, SortedReft, a) -> EBindEnv a
forall a b. (a -> b) -> a -> b
$ Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
i (BindMap (Symbol, SortedReft, a)
 -> SizedEnv (Symbol, SortedReft, a))
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a b. (a -> b) -> a -> b
$ (Int -> (Symbol, SortedReft, a) -> Bool)
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Int
k (Symbol, SortedReft, a)
_ -> Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 = 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

{-# SCC toListSEnv #-}
toListSEnv              ::  SEnv a -> [(Symbol, a)]
toListSEnv :: forall a. 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 :: forall a. [(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 :: forall a. 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 :: forall a b. (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 a b. (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 :: forall (m :: * -> *) a b.
Monad m =>
(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 :: forall a b. ((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 a b. (a -> b) -> [a] -> [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 :: forall a. 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 :: forall a. 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)

{-# SCC lookupSEnv #-}
lookupSEnv :: Symbol -> SEnv a -> Maybe a
lookupSEnv :: forall a. 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 :: forall a. 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 :: forall a. 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 :: 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) = 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 =>
(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) = 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 :: forall a. (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 :: forall a. 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 => 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)    = 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 => 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 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 {a} {a}. Ord a => [(a, 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 b c a. (b -> c) -> (a -> b) -> a -> c
. (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 :: [(a, a)] -> [a]
takeMin [(a, a)]
xs = [a
z | (a
d, a
z) <- [(a, a)]
xs, a
d a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [(a, a)] -> a
forall {t :: * -> *} {c} {b}.
(Foldable t, Ord c, Functor t) =>
t (c, b) -> c
getMin [(a, a)]
xs]
    getMin :: t (c, b) -> c
getMin     = t c -> c
forall a. Ord a => t a -> a
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]
  deriving Int -> SESearch a -> ShowS
[SESearch a] -> ShowS
SESearch a -> String
(Int -> SESearch a -> ShowS)
-> (SESearch a -> String)
-> ([SESearch a] -> ShowS)
-> Show (SESearch a)
forall a. Show a => Int -> SESearch a -> ShowS
forall a. Show a => [SESearch a] -> ShowS
forall a. Show a => SESearch a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> SESearch a -> ShowS
showsPrec :: Int -> SESearch a -> ShowS
$cshow :: forall a. Show a => SESearch a -> String
show :: SESearch a -> String
$cshowList :: forall a. Show a => [SESearch a] -> ShowS
showList :: [SESearch a] -> ShowS
Show

-- | 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 a b. (a -> b -> b) -> b -> [a] -> b
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 -> 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, Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
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, a)
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
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))

bindEnvSize :: BindEnv a -> Int
bindEnvSize :: forall a. BindEnv a -> Int
bindEnvSize (BE Int
n BindMap (Symbol, SortedReft, a)
_) = Int
n

fromListBindEnv :: [(BindId, (Symbol, SortedReft, a))] -> BindEnv a
fromListBindEnv :: forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
fromListBindEnv [(Int, (Symbol, SortedReft, a))]
xs = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE ([(Int, (Symbol, SortedReft, a))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, (Symbol, SortedReft, a))]
xs) ([(Int, (Symbol, SortedReft, a))] -> BindMap (Symbol, SortedReft, a)
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 = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
0 BindMap (Symbol, SortedReft, a)
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) = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n ((Int -> (Symbol, SortedReft, a) -> Bool)
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
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 [] = BindEnv a
forall a. BindEnv a
emptyBindEnv
bindEnvFromList [(Int, (Symbol, SortedReft, a))]
bs = Int -> BindMap (Symbol, SortedReft, a) -> BindEnv a
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, a)
be
  where
    maxId :: Int
maxId          = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Int
n | (Int
n,(Symbol
_,SortedReft
_,a
_)) <- [(Int, (Symbol, SortedReft, a))]
bs ]
    be :: BindMap (Symbol, SortedReft, a)
be             = [(Int, (Symbol, SortedReft, a))] -> BindMap (Symbol, SortedReft, a)
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 = (Int, (Symbol, SortedReft, a)) -> Int
forall a b. (a, b) -> a
fst ((Int, (Symbol, SortedReft, a)) -> Int)
-> [(Int, (Symbol, SortedReft, a))] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindEnv a -> [(Int, (Symbol, SortedReft, a))]
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) = BindMap (Symbol, SortedReft, a) -> [(Int, (Symbol, SortedReft, a))]
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) = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n ((Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
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) = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (BindMap (Symbol, SortedReft, a)
 -> SizedEnv (Symbol, SortedReft, a))
-> ([(Int, (Symbol, SortedReft, a))]
    -> BindMap (Symbol, SortedReft, a))
-> [(Int, (Symbol, SortedReft, a))]
-> SizedEnv (Symbol, SortedReft, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, (Symbol, SortedReft, a))] -> BindMap (Symbol, SortedReft, a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Int, (Symbol, SortedReft, a))]
 -> SizedEnv (Symbol, SortedReft, a))
-> m [(Int, (Symbol, SortedReft, a))]
-> m (SizedEnv (Symbol, SortedReft, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, (Symbol, SortedReft, a))
 -> m (Int, (Symbol, SortedReft, a)))
-> [(Int, (Symbol, SortedReft, a))]
-> m [(Int, (Symbol, SortedReft, a))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int, (Symbol, SortedReft, a)) -> m (Int, (Symbol, SortedReft, a))
f' (BindMap (Symbol, SortedReft, a) -> [(Int, (Symbol, SortedReft, a))]
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)) ; (Int, (Symbol, SortedReft, a)) -> m (Int, (Symbol, SortedReft, a))
forall a. a -> m a
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) = (Symbol, SortedReft, a)
-> Maybe (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
forall a. a -> Maybe a -> a
fromMaybe (Symbol, SortedReft, a)
err (Int
-> BindMap (Symbol, SortedReft, a) -> Maybe (Symbol, SortedReft, a)
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                  = String -> (Symbol, SortedReft, a)
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> (Symbol, SortedReft, a))
-> String -> (Symbol, SortedReft, a)
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 => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Int
m2

unionsIBindEnv :: [IBindEnv] -> IBindEnv
unionsIBindEnv :: [IBindEnv] -> IBindEnv
unionsIBindEnv = (IBindEnv -> IBindEnv -> IBindEnv)
-> IBindEnv -> [IBindEnv] -> IBindEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
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 (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 => 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 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) = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (((Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> Int
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
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) = Int
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a. Int -> BindMap a -> SizedEnv a
BE Int
n (BindMap (Symbol, SortedReft, a)
 -> SizedEnv (Symbol, SortedReft, a))
-> BindMap (Symbol, SortedReft, a)
-> SizedEnv (Symbol, SortedReft, a)
forall a b. (a -> b) -> a -> b
$ Int
-> BindMap (Symbol, SortedReft, a)
-> BindMap (Symbol, SortedReft, a)
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 = (a -> b) -> SEnv a -> SEnv b
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Int, (Symbol, SortedReft, a)) -> Doc)
-> [(Int, (Symbol, SortedReft, a))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Symbol, SortedReft, a)) -> Doc
forall {a} {a} {c}.
(Fixpoint a, Fixpoint a) =>
(a, (a, SortedReft, c)) -> Doc
toFixBind ([(Int, (Symbol, SortedReft, a))] -> [Doc])
-> [(Int, (Symbol, SortedReft, a))] -> [Doc]
forall a b. (a -> b) -> a -> b
$ BindMap (Symbol, SortedReft, a) -> [(Int, (Symbol, SortedReft, a))]
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
<+> 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 a) where
  toFix :: BindEnv a -> Doc
toFix (BE Int
_ BindMap (Symbol, SortedReft, a)
m) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Int, (Symbol, SortedReft, a)) -> Doc)
-> [(Int, (Symbol, SortedReft, a))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Symbol, SortedReft, a)) -> Doc
forall {a} {a} {a} {c}.
(Fixpoint a, Fixpoint a, Fixpoint a) =>
(a, (a, a, c)) -> Doc
toFixBind ([(Int, (Symbol, SortedReft, a))] -> [Doc])
-> [(Int, (Symbol, SortedReft, a))] -> [Doc]
forall a b. (a -> b) -> a -> b
$ BindMap (Symbol, SortedReft, a) -> [(Int, (Symbol, SortedReft, a))]
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
<+> 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 => 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 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
_        = String -> BindEnv a
forall a. (?callStack::CallStack) => String -> a
errorstar String
"mappend on non-trivial BindEnvs"

instance Monoid (BindEnv a) where
  mempty :: BindEnv a
mempty  = Int -> BindMap (Symbol, SortedReft, a) -> BindEnv a
forall a. Int -> BindMap a -> SizedEnv a
BE Int
0 BindMap (Symbol, SortedReft, a)
forall k v. HashMap k v
M.empty
  mappend :: BindEnv a -> BindEnv a -> BindEnv a
mappend = BindEnv a -> BindEnv a -> BindEnv a
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
_) = Int -> BindEnv a -> (Symbol, SortedReft, 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
<+> HashSet Int -> 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
(Packs -> Packs -> Bool) -> (Packs -> Packs -> Bool) -> Eq Packs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Packs -> Packs -> Bool
== :: Packs -> Packs -> Bool
$c/= :: Packs -> Packs -> Bool
/= :: 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
$cshowsPrec :: Int -> Packs -> ShowS
showsPrec :: Int -> Packs -> ShowS
$cshow :: Packs -> String
show :: Packs -> String
$cshowList :: [Packs] -> ShowS
showList :: [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
$cfrom :: forall x. Packs -> Rep Packs x
from :: forall x. Packs -> Rep Packs x
$cto :: forall x. Rep Packs x -> Packs
to :: forall x. Rep Packs x -> Packs
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 => 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 a b. (a -> b) -> [a] -> [b]
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

coerceBindEnv :: ElabFlags -> BindEnv a -> BindEnv a
coerceBindEnv :: forall a. ElabFlags -> BindEnv a -> BindEnv a
coerceBindEnv ElabFlags
ef BindEnv a
be = BindEnv a
be { beBinds = M.map (\(Symbol
s, SortedReft
sr, a
a) ->
                                                let srs :: Sort
srs = Sort -> Sort
coerceMapToArray (SortedReft -> Sort
sr_sort SortedReft
sr) in
                                                (Symbol
s, SortedReft
sr { sr_sort = if elabSetBag ef then coerceSetBagToArray srs else srs } , a
a))
                                            (beBinds be) }