liquid-fixpoint-0.8.10.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Environments

Synopsis

Environments

data SEnv a Source #

Instances

Instances details
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 #

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 :: forall r r'. (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.10.2-inplace" '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] 

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

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 #

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

Local Constraint Environments

data IBindEnv Source #

Instances

Instances details
Eq IBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

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 :: forall r r'. (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

Monoid IBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

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

Fixpoint IBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

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.10.2-inplace" 'True) (C1 ('MetaCons "FB" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet BindId))))

type BindMap a = HashMap BindId a Source #

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

data EBindEnv Source #

Instances

Instances details
Fixpoint EBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Information needed to lookup and update Solutions

Groups of KVars (needed by eliminate)

newtype Packs Source #

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

Constructors

Packs 

Fields

Instances

Instances details
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

Fixpoint Packs Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

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.10.2-inplace" 'True) (C1 ('MetaCons "Packs" 'PrefixI 'True) (S1 ('MetaSel ('Just "packm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap KVar Int))))

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 #