| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Environments
Contents
- data SEnv a
- data SESearch a
- emptySEnv :: SEnv a
- toListSEnv :: SEnv a -> [(Symbol, a)]
- fromListSEnv :: [(Symbol, a)] -> SEnv a
- mapSEnvWithKey :: ((Symbol, a1) -> (Symbol, a)) -> SEnv a1 -> SEnv a
- mapSEnv :: (a1 -> a) -> SEnv a1 -> SEnv a
- insertSEnv :: Symbol -> a -> SEnv a -> SEnv a
- deleteSEnv :: Symbol -> SEnv a -> SEnv a
- memberSEnv :: Symbol -> SEnv a -> Bool
- lookupSEnv :: Symbol -> SEnv v -> Maybe v
- unionSEnv :: SEnv a -> HashMap Symbol a -> SEnv a
- intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
- differenceSEnv :: SEnv a -> SEnv w -> SEnv a
- filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a
- lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a
- envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
- data IBindEnv
- type BindId = Int
- type BindMap a = HashMap BindId a
- emptyIBindEnv :: IBindEnv
- insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
- deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
- elemsIBindEnv :: IBindEnv -> [BindId]
- type BindEnv = SizedEnv (Symbol, SortedReft)
- beBinds :: SizedEnv a -> BindMap a
- insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
- emptyBindEnv :: BindEnv
- lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
- mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
- adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv
- bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
- bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]
- unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
- diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
Environments
Instances
| Functor SEnv Source | |
| Foldable SEnv Source | |
| Traversable SEnv Source | |
| Eq a => Eq (SEnv a) Source | |
| Data a => Data (SEnv a) Source | |
| Fixpoint (SEnv a) => Show (SEnv a) Source | |
| Generic (SEnv a) Source | |
| Monoid (SEnv a) Source | |
| Binary a => Binary (SEnv a) Source | |
| NFData a => NFData (SEnv a) Source | |
| Fixpoint a => Fixpoint (SEnv a) Source | |
| type Rep (SEnv a) Source |
toListSEnv :: SEnv a -> [(Symbol, a)] Source
fromListSEnv :: [(Symbol, a)] -> SEnv a Source
insertSEnv :: Symbol -> a -> SEnv a -> SEnv a Source
deleteSEnv :: Symbol -> SEnv a -> SEnv a Source
memberSEnv :: Symbol -> SEnv a -> Bool Source
lookupSEnv :: Symbol -> SEnv v -> Maybe v Source
intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a Source
differenceSEnv :: SEnv a -> SEnv w -> SEnv a Source
filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a Source
lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a Source
emptyIBindEnv :: IBindEnv Source
Functions for Indexed Bind Environment
insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv Source
deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv Source
elemsIBindEnv :: IBindEnv -> [BindId] Source
type BindEnv = SizedEnv (Symbol, SortedReft) Source
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv) Source
Functions for Global Binder Environment
lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft) Source
mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv Source
adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv Source
bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv Source
bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)] Source
unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source
diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source