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

Environments

data SEnv a Source #

Instances

Functor SEnv Source #
Methods fmap :: (a -> b) -> SEnv a -> SEnv b # (<$) :: a -> SEnv b -> SEnv a #
Foldable SEnv Source #
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 #
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 #
Methods (==) :: SEnv a -> SEnv a -> Bool # (/=) :: SEnv a -> SEnv a -> Bool #
Data a => Data (SEnv a) Source #
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 #
Methods showsPrec :: Int -> SEnv a -> ShowS # show :: SEnv a -> String # showList :: [SEnv a] -> ShowS #
Generic (SEnv a) Source #
Associated Types type Rep (SEnv a) :: * -> * # Methods from :: SEnv a -> Rep (SEnv a) x # to :: Rep (SEnv a) x -> SEnv a #
Monoid (SEnv a) Source #
Methods mempty :: SEnv a # mappend :: SEnv a -> SEnv a -> SEnv a # mconcat :: [SEnv a] -> SEnv a #
Binary a => Binary (SEnv a) Source #
Methods put :: SEnv a -> Put # get :: Get (SEnv a) # putList :: [SEnv a] -> Put #
NFData a => NFData (SEnv a) Source #
Methods rnf :: SEnv a -> () #
PPrint a => PPrint (SEnv a) Source #
Methods pprintTidy :: Tidy -> SEnv a -> Doc Source # pprintPrec :: Int -> Tidy -> SEnv a -> Doc Source #
Fixpoint a => Fixpoint (SEnv a) Source #
Methods toFix :: SEnv a -> Doc Source # simplify :: SEnv a -> SEnv a Source #
Defunc a => Defunc (SEnv a) Source #
Methods defunc :: SEnv a -> DF (SEnv a) Source #
type Rep (SEnv a) Source #
type Rep (SEnv a) = D1 (MetaData "SEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "SE" PrefixI True) (S1 (MetaSel (Just Symbol "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 #
Methods (==) :: IBindEnv -> IBindEnv -> Bool # (/=) :: IBindEnv -> IBindEnv -> Bool #
Data IBindEnv Source #
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 #
Associated Types type Rep IBindEnv :: * -> * # Methods from :: IBindEnv -> Rep IBindEnv x # to :: Rep IBindEnv x -> IBindEnv #
Monoid IBindEnv Source #	Functions for Indexed Bind Environment
Methods mempty :: IBindEnv # mappend :: IBindEnv -> IBindEnv -> IBindEnv # mconcat :: [IBindEnv] -> IBindEnv #
Binary IBindEnv Source #
Methods put :: IBindEnv -> Put # get :: Get IBindEnv # putList :: [IBindEnv] -> Put #
NFData IBindEnv Source #
Methods rnf :: IBindEnv -> () #
PPrint IBindEnv Source #
Methods pprintTidy :: Tidy -> IBindEnv -> Doc Source # pprintPrec :: Int -> Tidy -> IBindEnv -> Doc Source #
Fixpoint IBindEnv Source #
Methods toFix :: IBindEnv -> Doc Source # simplify :: IBindEnv -> IBindEnv Source #
type Rep IBindEnv Source #
type Rep IBindEnv = D1 (MetaData "IBindEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "FB" PrefixI False) (S1 (MetaSel (Nothing 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 #

Information needed to lookup and update Solutions

data SolEnv Source #

Constructors

SolEnv
Fields soeBinds :: !BindEnv

Instances

Eq SolEnv Source #
Methods (==) :: SolEnv -> SolEnv -> Bool # (/=) :: SolEnv -> SolEnv -> Bool #
Show SolEnv Source #
Methods showsPrec :: Int -> SolEnv -> ShowS # show :: SolEnv -> String # showList :: [SolEnv] -> ShowS #
Generic SolEnv Source #
Associated Types type Rep SolEnv :: * -> * # Methods from :: SolEnv -> Rep SolEnv x # to :: Rep SolEnv x -> SolEnv #
type Rep SolEnv Source #
type Rep SolEnv = D1 (MetaData "SolEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "SolEnv" PrefixI True) (S1 (MetaSel (Just Symbol "soeBinds") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 BindEnv)))

Groups of KVars (needed by eliminate)

newtype Packs Source #

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

Constructors

Packs
Fields packm :: HashMap KVar Int

Instances

Eq Packs Source #
Methods (==) :: Packs -> Packs -> Bool # (/=) :: Packs -> Packs -> Bool #
Show Packs Source #
Methods showsPrec :: Int -> Packs -> ShowS # show :: Packs -> String # showList :: [Packs] -> ShowS #
Generic Packs Source #
Associated Types type Rep Packs :: * -> * # Methods from :: Packs -> Rep Packs x # to :: Rep Packs x -> Packs #
Monoid Packs Source #
Methods mempty :: Packs # mappend :: Packs -> Packs -> Packs # mconcat :: [Packs] -> Packs #
Binary Packs Source #
Methods put :: Packs -> Put # get :: Get Packs # putList :: [Packs] -> Put #
NFData Packs Source #
Methods rnf :: Packs -> () #
PPrint Packs Source #
Methods pprintTidy :: Tidy -> Packs -> Doc Source # pprintPrec :: Int -> Tidy -> Packs -> Doc Source #
Fixpoint Packs Source #
Methods toFix :: Packs -> Doc Source # simplify :: Packs -> Packs Source #
type Rep Packs Source #
type Rep Packs = D1 (MetaData "Packs" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "Packs" PrefixI True) (S1 (MetaSel (Just Symbol "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 #
Methods put :: HashSet a -> Put # get :: Get (HashSet a) # putList :: [HashSet a] -> Put #