Language.Fixpoint.Types.Substitutions

This module contains the various instances for Subable, which (should) depend on the visitors, and hence cannot be in the same place as the Term definitions.

Documentation

mkSubst :: [(Symbol, Expr)] -> Subst

isEmptySubst :: Subst -> Bool

substExcept :: Subst -> [Symbol] -> Subst

substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr

subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a

targetSubstSyms :: Subst -> [Symbol]

filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst

Orphan instances

Show SortedReft

Methods

showsPrec :: Int -> SortedReft -> ShowS

show :: SortedReft -> String

showList :: [SortedReft] -> ShowS

Show Reft

Methods

showsPrec :: Int -> Reft -> ShowS

show :: Reft -> String

showList :: [Reft] -> ShowS

Semigroup SortedReft

Methods

(<>) :: SortedReft -> SortedReft -> SortedReft

sconcat :: NonEmpty SortedReft -> SortedReft

stimes :: Integral b => b -> SortedReft -> SortedReft

Semigroup Reft

Methods

(<>) :: Reft -> Reft -> Reft

sconcat :: NonEmpty Reft -> Reft

stimes :: Integral b => b -> Reft -> Reft

Semigroup Expr

Methods

(<>) :: Expr -> Expr -> Expr

sconcat :: NonEmpty Expr -> Expr

stimes :: Integral b => b -> Expr -> Expr

Semigroup Subst

Methods

(<>) :: Subst -> Subst -> Subst

sconcat :: NonEmpty Subst -> Subst

stimes :: Integral b => b -> Subst -> Subst

Monoid SortedReft

Methods

mempty :: SortedReft

mappend :: SortedReft -> SortedReft -> SortedReft

mconcat :: [SortedReft] -> SortedReft

Monoid Reft

Methods

mempty :: Reft

mappend :: Reft -> Reft -> Reft

mconcat :: [Reft] -> Reft

Monoid Expr

Methods

mempty :: Expr

mappend :: Expr -> Expr -> Expr

mconcat :: [Expr] -> Expr

Monoid Subst

Methods

mempty :: Subst

mappend :: Subst -> Subst -> Subst

mconcat :: [Subst] -> Subst

PPrint SortedReft

Methods

pprintTidy :: Tidy -> SortedReft -> Doc

pprintPrec :: Int -> Tidy -> SortedReft -> Doc

PPrint Reft

Methods

pprintTidy :: Tidy -> Reft -> Doc

pprintPrec :: Int -> Tidy -> Reft -> Doc

Fixpoint SortedReft

Methods

toFix :: SortedReft -> Doc

simplify :: SortedReft -> SortedReft

Fixpoint Reft

Methods

toFix :: Reft -> Doc

simplify :: Reft -> Reft

Reftable ()

Methods

isTauto :: () -> Bool

ppTy :: () -> Doc -> Doc

top :: () -> ()

bot :: () -> ()

meet :: () -> () -> ()

toReft :: () -> Reft

ofReft :: Reft -> ()

params :: () -> [Symbol]

Reftable SortedReft

Methods

isTauto :: SortedReft -> Bool

ppTy :: SortedReft -> Doc -> Doc

top :: SortedReft -> SortedReft

bot :: SortedReft -> SortedReft

meet :: SortedReft -> SortedReft -> SortedReft

toReft :: SortedReft -> Reft

ofReft :: Reft -> SortedReft

params :: SortedReft -> [Symbol]

Reftable Reft

Methods

isTauto :: Reft -> Bool

ppTy :: Reft -> Doc -> Doc

top :: Reft -> Reft

bot :: Reft -> Reft

meet :: Reft -> Reft -> Reft

toReft :: Reft -> Reft

ofReft :: Reft -> Reft

params :: Reft -> [Symbol]

Subable ()

Methods

syms :: () -> [Symbol]

substa :: (Symbol -> Symbol) -> () -> ()

substf :: (Symbol -> Expr) -> () -> ()

subst :: Subst -> () -> ()

subst1 :: () -> (Symbol, Expr) -> ()

Subable Symbol

Methods

syms :: Symbol -> [Symbol]

substa :: (Symbol -> Symbol) -> Symbol -> Symbol

substf :: (Symbol -> Expr) -> Symbol -> Symbol

subst :: Subst -> Symbol -> Symbol

subst1 :: Symbol -> (Symbol, Expr) -> Symbol

Subable SortedReft

Methods

syms :: SortedReft -> [Symbol]

substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft

substf :: (Symbol -> Expr) -> SortedReft -> SortedReft

subst :: Subst -> SortedReft -> SortedReft

subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft

Subable Reft

Methods

syms :: Reft -> [Symbol]

substa :: (Symbol -> Symbol) -> Reft -> Reft

substf :: (Symbol -> Expr) -> Reft -> Reft

subst :: Subst -> Reft -> Reft

subst1 :: Reft -> (Symbol, Expr) -> Reft

Subable Expr

Methods

syms :: Expr -> [Symbol]

substa :: (Symbol -> Symbol) -> Expr -> Expr

substf :: (Symbol -> Expr) -> Expr -> Expr

subst :: Subst -> Expr -> Expr

subst1 :: Expr -> (Symbol, Expr) -> Expr

Subable a => Subable [a]

Methods

syms :: [a] -> [Symbol]

substa :: (Symbol -> Symbol) -> [a] -> [a]

substf :: (Symbol -> Expr) -> [a] -> [a]

subst :: Subst -> [a] -> [a]

subst1 :: [a] -> (Symbol, Expr) -> [a]

Subable a => Subable (Maybe a)

Methods

syms :: Maybe a -> [Symbol]

substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a

substf :: (Symbol -> Expr) -> Maybe a -> Maybe a

subst :: Subst -> Maybe a -> Maybe a

subst1 :: Maybe a -> (Symbol, Expr) -> Maybe a

(Subable a, Subable b) => Subable (a, b)

Methods

syms :: (a, b) -> [Symbol]

substa :: (Symbol -> Symbol) -> (a, b) -> (a, b)

substf :: (Symbol -> Expr) -> (a, b) -> (a, b)

subst :: Subst -> (a, b) -> (a, b)

subst1 :: (a, b) -> (Symbol, Expr) -> (a, b)

Subable a => Subable (HashMap k a)

Methods

syms :: HashMap k a -> [Symbol]

substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a

substf :: (Symbol -> Expr) -> HashMap k a -> HashMap k a

subst :: Subst -> HashMap k a -> HashMap k a

subst1 :: HashMap k a -> (Symbol, Expr) -> HashMap k a

Expression (Symbol, SortedReft)

Methods

expr :: (Symbol, SortedReft) -> Expr