Language.Fixpoint.Types.Environments

Environments

data SEnv a

Instances

Functor SEnv

Defined in Language.Fixpoint.Types.Environments

Methods

fmap :: (a -> b) -> SEnv a -> SEnv b

(<$) :: a -> SEnv b -> SEnv a

Foldable SEnv

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

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)

Defined in Language.Fixpoint.Types.Environments

Methods

(==) :: SEnv a -> SEnv a -> Bool

(/=) :: SEnv a -> SEnv a -> Bool

Data a => Data (SEnv a)

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)

Defined in Language.Fixpoint.Types.Environments

Methods

showsPrec :: Int -> SEnv a -> ShowS

show :: SEnv a -> String

showList :: [SEnv a] -> ShowS

Generic (SEnv a)

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)

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)

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)

Defined in Language.Fixpoint.Types.Environments

Methods

put :: SEnv a -> Put

get :: Get (SEnv a)

putList :: [SEnv a] -> Put

NFData a => NFData (SEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: SEnv a -> ()

PPrint a => PPrint (SEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> SEnv a -> Doc

pprintPrec :: Int -> Tidy -> SEnv a -> Doc

Fixpoint a => Fixpoint (SEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: SEnv a -> Doc

simplify :: SEnv a -> SEnv a

Defunc a => Defunc (SEnv a)

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: SEnv a -> DF (SEnv a)

type Rep (SEnv a)

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

Constructors

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)]

Local Constraint Environments

data IBindEnv

Instances

Eq IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

(==) :: IBindEnv -> IBindEnv -> Bool

(/=) :: IBindEnv -> IBindEnv -> Bool

Data IBindEnv

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

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

Functions for Indexed Bind Environment

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: IBindEnv -> IBindEnv -> IBindEnv

sconcat :: NonEmpty IBindEnv -> IBindEnv

stimes :: Integral b => b -> IBindEnv -> IBindEnv

Monoid IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: IBindEnv

mappend :: IBindEnv -> IBindEnv -> IBindEnv

mconcat :: [IBindEnv] -> IBindEnv

Binary IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

put :: IBindEnv -> Put

get :: Get IBindEnv

putList :: [IBindEnv] -> Put

NFData IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: IBindEnv -> ()

PPrint IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> IBindEnv -> Doc

pprintPrec :: Int -> Tidy -> IBindEnv -> Doc

Fixpoint IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: IBindEnv -> Doc

simplify :: IBindEnv -> IBindEnv

type Rep IBindEnv

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

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

Global Binder Environments

type BindEnv = SizedEnv (Symbol, SortedReft)

beBinds :: SizedEnv a -> BindMap a

emptyBindEnv :: BindEnv

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

Functions for Global Binder Environment

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

Instances

Fixpoint EBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: EBindEnv -> Doc

simplify :: EBindEnv -> EBindEnv

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

Information needed to lookup and update Solutions

Groups of KVars (needed by eliminate)

newtype Packs

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

Constructors

Packs

Fields

• packm :: HashMap KVar Int

Instances

Eq Packs

Defined in Language.Fixpoint.Types.Environments

Methods

(==) :: Packs -> Packs -> Bool

(/=) :: Packs -> Packs -> Bool

Show Packs

Defined in Language.Fixpoint.Types.Environments

Methods

showsPrec :: Int -> Packs -> ShowS

show :: Packs -> String

showList :: [Packs] -> ShowS

Generic Packs

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

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: Packs -> Packs -> Packs

sconcat :: NonEmpty Packs -> Packs

stimes :: Integral b => b -> Packs -> Packs

Monoid Packs

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: Packs

mappend :: Packs -> Packs -> Packs

mconcat :: [Packs] -> Packs

Binary Packs

Defined in Language.Fixpoint.Types.Environments

Methods

put :: Packs -> Put

get :: Get Packs

putList :: [Packs] -> Put

NFData Packs

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: Packs -> ()

PPrint Packs

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> Packs -> Doc

pprintPrec :: Int -> Tidy -> Packs -> Doc

Fixpoint Packs

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: Packs -> Doc

simplify :: Packs -> Packs

type Rep Packs

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

makePack :: [HashSet KVar] -> Packs

Orphan instances

(Hashable a, Eq a, Binary a) => Binary (HashSet a)

Methods

put :: HashSet a -> Put

get :: Get (HashSet a)

putList :: [HashSet a] -> Put