Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Environments

Contents

Environments
Local Constraint Environments
Global Binder Environments
Information needed to lookup and update Solutions
Groups of KVars (needed by eliminate)
Orphan instances

Synopsis

data SEnv a
data SESearch a
- = Found a
- | Alts [Symbol]
emptySEnv :: SEnv a
toListSEnv :: SEnv a -> [(Symbol, a)]
fromListSEnv :: [(Symbol, a)] -> SEnv a
fromMapSEnv :: HashMap Symbol a -> SEnv a
mapSEnvWithKey :: ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b
mapSEnv :: (a -> b) -> SEnv a -> SEnv b
mapMSEnv :: Monad m => (a -> m b) -> SEnv a -> m (SEnv b)
insertSEnv :: Symbol -> a -> SEnv a -> SEnv a
deleteSEnv :: Symbol -> SEnv a -> SEnv a
memberSEnv :: Symbol -> SEnv a -> Bool
lookupSEnv :: Symbol -> SEnv a -> Maybe a
unionSEnv :: SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv' :: SEnv a -> SEnv 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]
fromListIBindEnv :: [BindId] -> IBindEnv
memberIBindEnv :: BindId -> IBindEnv -> Bool
unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
nullIBindEnv :: IBindEnv -> Bool
filterIBindEnv :: (BindId -> Bool) -> IBindEnv -> IBindEnv
type BindEnv = SizedEnv (Symbol, SortedReft)
beBinds :: SizedEnv a -> BindMap a
emptyBindEnv :: BindEnv
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
filterBindEnv :: (BindId -> Symbol -> SortedReft -> Bool) -> BindEnv -> BindEnv
mapBindEnv :: (BindId -> (Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
mapWithKeyMBindEnv :: Monad m => ((BindId, (Symbol, SortedReft)) -> m (BindId, (Symbol, SortedReft))) -> BindEnv -> m BindEnv
adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv
bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]
elemsBindEnv :: BindEnv -> [BindId]
data EBindEnv
splitByQuantifiers :: BindEnv -> [BindId] -> (BindEnv, EBindEnv)
newtype Packs = Packs {
- packm :: HashMap KVar Int
}
getPack :: KVar -> Packs -> Maybe Int
makePack :: [HashSet KVar] -> Packs

Environments

data SEnv a Source #

Instances

Functor SEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods fmap :: (a -> b) -> SEnv a -> SEnv b # (<$) :: a -> SEnv b -> SEnv a #
Foldable SEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods fold :: Monoid m => SEnv m -> m # foldMap :: Monoid m => (a -> m) -> SEnv a -> m # foldr :: (a -> b -> b) -> b -> SEnv a -> b # foldr' :: (a -> b -> b) -> b -> SEnv a -> b # foldl :: (b -> a -> b) -> b -> SEnv a -> b # foldl' :: (b -> a -> b) -> b -> SEnv a -> b # foldr1 :: (a -> a -> a) -> SEnv a -> a # foldl1 :: (a -> a -> a) -> SEnv a -> a # toList :: SEnv a -> [a] # null :: SEnv a -> Bool # length :: SEnv a -> Int # elem :: Eq a => a -> SEnv a -> Bool # maximum :: Ord a => SEnv a -> a # minimum :: Ord a => SEnv a -> a # sum :: Num a => SEnv a -> a # product :: Num a => SEnv a -> a #
Traversable SEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods traverse :: Applicative f => (a -> f b) -> SEnv a -> f (SEnv b) # sequenceA :: Applicative f => SEnv (f a) -> f (SEnv a) # mapM :: Monad m => (a -> m b) -> SEnv a -> m (SEnv b) # sequence :: Monad m => SEnv (m a) -> m (SEnv a) #
Eq a => Eq (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (==) :: SEnv a -> SEnv a -> Bool # (/=) :: SEnv a -> SEnv a -> Bool #
Data a => Data (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SEnv a -> c (SEnv a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SEnv a) # toConstr :: SEnv a -> Constr # dataTypeOf :: SEnv a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SEnv a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SEnv a)) # gmapT :: (forall b. Data b => b -> b) -> SEnv a -> SEnv a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SEnv a -> r # gmapQ :: (forall d. Data d => d -> u) -> SEnv a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SEnv a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SEnv a -> m (SEnv a) #
Fixpoint (SEnv a) => Show (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods showsPrec :: Int -> SEnv a -> ShowS # show :: SEnv a -> String # showList :: [SEnv a] -> ShowS #
Generic (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Associated Types type Rep (SEnv a) :: Type -> Type # Methods from :: SEnv a -> Rep (SEnv a) x # to :: Rep (SEnv a) x -> SEnv a #
Semigroup (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (<>) :: SEnv a -> SEnv a -> SEnv a # sconcat :: NonEmpty (SEnv a) -> SEnv a # stimes :: Integral b => b -> SEnv a -> SEnv a #
Monoid (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: SEnv a # mappend :: SEnv a -> SEnv a -> SEnv a # mconcat :: [SEnv a] -> SEnv a #
Binary a => Binary (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods put :: SEnv a -> Put # get :: Get (SEnv a) # putList :: [SEnv a] -> Put #
NFData a => NFData (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods rnf :: SEnv a -> () #
PPrint a => PPrint (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> SEnv a -> Doc Source # pprintPrec :: Int -> Tidy -> SEnv a -> Doc Source #
Fixpoint a => Fixpoint (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: SEnv a -> Doc Source # simplify :: SEnv a -> SEnv a Source #
Defunc a => Defunc (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SEnv a -> DF (SEnv a) Source #
type Rep (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments type Rep (SEnv a) = D1 (MetaData "SEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" True) (C1 (MetaCons "SE" PrefixI True) (S1 (MetaSel (Just "seBinds") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (HashMap Symbol a))))

data SESearch a Source #

Constructors

Found a
Alts [Symbol]

emptySEnv :: SEnv a Source #

toListSEnv :: SEnv a -> [(Symbol, a)] Source #

fromListSEnv :: [(Symbol, a)] -> SEnv a Source #

fromMapSEnv :: HashMap Symbol a -> SEnv a Source #

mapSEnvWithKey :: ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b Source #

mapSEnv :: (a -> b) -> SEnv a -> SEnv b Source #

mapMSEnv :: Monad m => (a -> m b) -> SEnv a -> m (SEnv b) 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 a -> Maybe a Source #

unionSEnv :: SEnv a -> HashMap Symbol a -> SEnv a Source #

unionSEnv' :: SEnv a -> SEnv a -> SEnv a 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 #

envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)] Source #

Local Constraint Environments

data IBindEnv Source #

Instances

Eq IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (==) :: IBindEnv -> IBindEnv -> Bool # (/=) :: IBindEnv -> IBindEnv -> Bool #
Data IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IBindEnv -> c IBindEnv # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IBindEnv # toConstr :: IBindEnv -> Constr # dataTypeOf :: IBindEnv -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IBindEnv) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IBindEnv) # gmapT :: (forall b. Data b => b -> b) -> IBindEnv -> IBindEnv # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IBindEnv -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IBindEnv -> r # gmapQ :: (forall d. Data d => d -> u) -> IBindEnv -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IBindEnv -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IBindEnv -> m IBindEnv #
Generic IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Associated Types type Rep IBindEnv :: Type -> Type # Methods from :: IBindEnv -> Rep IBindEnv x # to :: Rep IBindEnv x -> IBindEnv #
Semigroup IBindEnv Source #	Functions for Indexed Bind Environment
Instance details Defined in Language.Fixpoint.Types.Environments Methods (<>) :: IBindEnv -> IBindEnv -> IBindEnv # sconcat :: NonEmpty IBindEnv -> IBindEnv # stimes :: Integral b => b -> IBindEnv -> IBindEnv #
Monoid IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: IBindEnv # mappend :: IBindEnv -> IBindEnv -> IBindEnv # mconcat :: [IBindEnv] -> IBindEnv #
Binary IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods put :: IBindEnv -> Put # get :: Get IBindEnv # putList :: [IBindEnv] -> Put #
NFData IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods rnf :: IBindEnv -> () #
PPrint IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> IBindEnv -> Doc Source # pprintPrec :: Int -> Tidy -> IBindEnv -> Doc Source #
Fixpoint IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: IBindEnv -> Doc Source # simplify :: IBindEnv -> IBindEnv Source #
type Rep IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments type Rep IBindEnv = D1 (MetaData "IBindEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" True) (C1 (MetaCons "FB" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (HashSet BindId))))

type BindId = Int Source #

type BindMap a = HashMap BindId a Source #

emptyIBindEnv :: IBindEnv Source #

insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv Source #

deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv Source #

elemsIBindEnv :: IBindEnv -> [BindId] Source #

fromListIBindEnv :: [BindId] -> IBindEnv Source #

memberIBindEnv :: BindId -> IBindEnv -> Bool Source #

unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source #

diffIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source #

intersectionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source #

nullIBindEnv :: IBindEnv -> Bool Source #

filterIBindEnv :: (BindId -> Bool) -> IBindEnv -> IBindEnv Source #

Global Binder Environments

type BindEnv = SizedEnv (Symbol, SortedReft) Source #

beBinds :: SizedEnv a -> BindMap a Source #

emptyBindEnv :: BindEnv Source #

insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv) Source #

Functions for Global Binder Environment

lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft) Source #

filterBindEnv :: (BindId -> Symbol -> SortedReft -> Bool) -> BindEnv -> BindEnv Source #

mapBindEnv :: (BindId -> (Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv Source #

mapWithKeyMBindEnv :: Monad m => ((BindId, (Symbol, SortedReft)) -> m (BindId, (Symbol, SortedReft))) -> BindEnv -> m BindEnv Source #

adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv Source #

bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv Source #

bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)] Source #

elemsBindEnv :: BindEnv -> [BindId] Source #

data EBindEnv Source #

Instances

Fixpoint EBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: EBindEnv -> Doc Source # simplify :: EBindEnv -> EBindEnv Source #

splitByQuantifiers :: BindEnv -> [BindId] -> (BindEnv, EBindEnv) Source #

Information needed to lookup and update Solutions

Groups of KVars (needed by eliminate)

newtype Packs Source #

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

Constructors

Packs
Fields packm :: HashMap KVar Int

Instances

Eq Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (==) :: Packs -> Packs -> Bool # (/=) :: Packs -> Packs -> Bool #
Show Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods showsPrec :: Int -> Packs -> ShowS # show :: Packs -> String # showList :: [Packs] -> ShowS #
Generic Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Associated Types type Rep Packs :: Type -> Type # Methods from :: Packs -> Rep Packs x # to :: Rep Packs x -> Packs #
Semigroup Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (<>) :: Packs -> Packs -> Packs # sconcat :: NonEmpty Packs -> Packs # stimes :: Integral b => b -> Packs -> Packs #
Monoid Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: Packs # mappend :: Packs -> Packs -> Packs # mconcat :: [Packs] -> Packs #
Binary Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods put :: Packs -> Put # get :: Get Packs # putList :: [Packs] -> Put #
NFData Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods rnf :: Packs -> () #
PPrint Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> Packs -> Doc Source # pprintPrec :: Int -> Tidy -> Packs -> Doc Source #
Fixpoint Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: Packs -> Doc Source # simplify :: Packs -> Packs Source #
type Rep Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments type Rep Packs = D1 (MetaData "Packs" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" True) (C1 (MetaCons "Packs" PrefixI True) (S1 (MetaSel (Just "packm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (HashMap KVar Int))))

getPack :: KVar -> Packs -> Maybe Int Source #

makePack :: [HashSet KVar] -> Packs Source #

Orphan instances

(Hashable a, Eq a, Binary a) => Binary (HashSet a) Source #
Instance details Methods put :: HashSet a -> Put # get :: Get (HashSet a) # putList :: [HashSet a] -> Put #