module Language.Fixpoint.Types.Environments (
SEnv, SESearch(..)
, emptySEnv, toListSEnv, fromListSEnv
, mapSEnvWithKey, mapSEnv
, insertSEnv, deleteSEnv, memberSEnv, lookupSEnv, unionSEnv
, intersectWithSEnv
, differenceSEnv
, filterSEnv
, lookupSEnvWithDistance
, envCs
, IBindEnv, BindId, BindMap
, emptyIBindEnv, insertsIBindEnv, deleteIBindEnv, elemsIBindEnv
, BindEnv, beBinds
, insertBindEnv, emptyBindEnv, lookupBindEnv, mapBindEnv, adjustBindEnv
, bindEnvFromList, bindEnvToList
, unionIBindEnv, diffIBindEnv
) where
import qualified Data.Binary as B
import Data.Generics (Data)
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 Text.PrettyPrint.HughesPJ
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 (Eq, Data, Typeable, Generic)
newtype SEnv a = SE { seBinds :: M.HashMap Symbol a }
deriving (Eq, Data, Typeable, Generic, Foldable, Traversable)
data SizedEnv a = BE { _beSize :: Int
, beBinds :: BindMap a
} deriving (Eq, Show, Functor, Foldable, Generic, Traversable)
type BindEnv = SizedEnv (Symbol, SortedReft)
toListSEnv :: SEnv a -> [(Symbol, a)]
toListSEnv (SE env) = M.toList env
fromListSEnv :: [(Symbol, a)] -> SEnv a
fromListSEnv = SE . M.fromList
mapSEnv f (SE env) = SE (fmap f env)
mapSEnvWithKey f = fromListSEnv . fmap f . toListSEnv
deleteSEnv x (SE env) = SE (M.delete x env)
insertSEnv x y (SE env) = SE (M.insert x y env)
lookupSEnv x (SE env) = M.lookup x env
emptySEnv = SE M.empty
memberSEnv x (SE env) = M.member x env
intersectWithSEnv f (SE m1) (SE m2) = SE (M.intersectionWith f m1 m2)
differenceSEnv (SE m1) (SE m2) = SE (M.difference m1 m2)
filterSEnv f (SE m) = SE (M.filter f m)
unionSEnv (SE m1) m2 = SE (M.union m1 m2)
lookupSEnvWithDistance x (SE env)
= case M.lookup x env of
Just z -> Found z
Nothing -> Alts $ symbol <$> alts
where
alts = takeMin $ zip (editDistance x' <$> ss) ss
ss = symbolString <$> fst <$> M.toList env
x' = symbolString x
takeMin xs = [z | (d, z) <- xs, d == getMin xs]
getMin = minimum . (fst <$>)
data SESearch a = Found a | Alts [Symbol]
emptyIBindEnv :: IBindEnv
emptyIBindEnv = FB S.empty
deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
deleteIBindEnv i (FB s) = FB (S.delete i s)
insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv is (FB s) = FB (foldr S.insert s is)
elemsIBindEnv :: IBindEnv -> [BindId]
elemsIBindEnv (FB s) = S.toList s
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
insertBindEnv x r (BE n m) = (n, BE (n + 1) (M.insert n (x, r) m))
emptyBindEnv :: BindEnv
emptyBindEnv = BE 0 M.empty
bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
bindEnvFromList [] = emptyBindEnv
bindEnvFromList bs = BE (1 + maxId) be
where
maxId = maximum $ fst3 <$> bs
be = M.fromList [(n, (x, r)) | (n, x, r) <- bs]
bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]
bindEnvToList (BE _ be) = [(n, x, r) | (n, (x, r)) <- M.toList be]
mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
mapBindEnv f (BE n m) = BE n $ M.map f m
lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv k (BE _ m) = fromMaybe err (M.lookup k m)
where
err = errorstar $ "lookupBindEnv: cannot find binder" ++ show k
unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv (FB m1) (FB m2) = FB $ m1 `S.union` m2
diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
diffIBindEnv (FB m1) (FB m2) = FB $ m1 `S.difference` m2
adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv
adjustBindEnv f i (BE n m) = BE n $ M.adjust f i m
instance Functor SEnv where
fmap = mapSEnv
instance Fixpoint BindEnv where
toFix (BE _ m) = vcat $ map toFixBind $ hashMapToAscList m
toFixBind (i, (x, r)) = text "bind" <+> toFix i <+> toFix x <+> text ":" <+> toFix r
instance (Fixpoint a) => Fixpoint (SEnv a) where
toFix (SE m) = toFix (hashMapToAscList m)
instance Fixpoint (SEnv a) => Show (SEnv a) where
show = render . toFix
instance Monoid (SEnv a) where
mempty = SE M.empty
mappend s1 s2 = SE $ M.union (seBinds s1) (seBinds s2)
instance Monoid BindEnv where
mempty = BE 0 M.empty
mappend (BE 0 _) b = b
mappend b (BE 0 _) = b
mappend _ _ = errorstar "mappend on non-trivial BindEnvs"
envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs be env = [lookupBindEnv i be | i <- elemsIBindEnv env]
instance Fixpoint (IBindEnv) where
toFix (FB ids) = text "env" <+> toFix ids
instance NFData IBindEnv
instance NFData BindEnv
instance (NFData a) => NFData (SEnv a)
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 = B.put . S.toList
get = S.fromList <$> B.get