liquid-fixpoint-0.7.0.7: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Environments

Contents

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.7-DC7X7gzBmY2Ic8PTKxWTVg" 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] 

toListSEnv :: SEnv a -> [(Symbol, 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 #

unionSEnv' :: SEnv a -> SEnv a -> SEnv a Source #

intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a Source #

filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a Source #

Local Constraint Environments

data IBindEnv Source #

Instances

Eq IBindEnv Source # 
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

Binary IBindEnv Source # 

Methods

put :: IBindEnv -> Put #

get :: Get IBindEnv #

putList :: [IBindEnv] -> Put #

NFData IBindEnv Source # 

Methods

rnf :: IBindEnv -> () #

PPrint IBindEnv Source # 
Fixpoint IBindEnv Source # 
type Rep IBindEnv Source # 
type Rep IBindEnv = D1 * (MetaData "IBindEnv" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" True) (C1 * (MetaCons "FB" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (HashSet BindId))))

Global Binder Environments

type BindEnv = SizedEnv (Symbol, SortedReft) Source #

beBinds :: SizedEnv a -> BindMap a Source #

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

Functions for Global Binder Environment

Information needed to lookup and update Solutions

data SolEnv Source #

Constructors

SolEnv 

Fields

Instances

Eq SolEnv Source # 

Methods

(==) :: SolEnv -> SolEnv -> Bool #

(/=) :: SolEnv -> SolEnv -> Bool #

Show SolEnv Source # 
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.7-DC7X7gzBmY2Ic8PTKxWTVg" 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

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 # 
Fixpoint Packs Source # 
type Rep Packs Source # 
type Rep Packs = D1 * (MetaData "Packs" "Language.Fixpoint.Types.Environments" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" True) (C1 * (MetaCons "Packs" PrefixI True) (S1 * (MetaSel (Just Symbol "packm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (HashMap KVar Int))))

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 #