Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Substitutions

Contents

Orphan instances

Description

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

isEmptySubst :: Subst -> Bool Source #

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

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

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

targetSubstSyms :: Subst -> [Symbol] Source #

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

catSubst :: Subst -> Subst -> Subst Source #

exprSymbolsSet :: Expr -> HashSet Symbol Source #

Orphan instances

Monoid Expr Source #
Instance details Methods mempty :: Expr # mappend :: Expr -> Expr -> Expr # mconcat :: [Expr] -> Expr #
Monoid Reft Source #
Instance details Methods mempty :: Reft # mappend :: Reft -> Reft -> Reft # mconcat :: [Reft] -> Reft #
Monoid SortedReft Source #
Instance details Methods mempty :: SortedReft # mappend :: SortedReft -> SortedReft -> SortedReft # mconcat :: [SortedReft] -> SortedReft #
Monoid Subst Source #
Instance details Methods mempty :: Subst # mappend :: Subst -> Subst -> Subst # mconcat :: [Subst] -> Subst #
Semigroup Expr Source #
Instance details Methods (<>) :: Expr -> Expr -> Expr # sconcat :: NonEmpty Expr -> Expr # stimes :: Integral b => b -> Expr -> Expr #
Semigroup Reft Source #
Instance details Methods (<>) :: Reft -> Reft -> Reft # sconcat :: NonEmpty Reft -> Reft # stimes :: Integral b => b -> Reft -> Reft #
Semigroup SortedReft Source #
Instance details Methods (<>) :: SortedReft -> SortedReft -> SortedReft # sconcat :: NonEmpty SortedReft -> SortedReft # stimes :: Integral b => b -> SortedReft -> SortedReft #
Semigroup Subst Source #
Instance details Methods (<>) :: Subst -> Subst -> Subst # sconcat :: NonEmpty Subst -> Subst # stimes :: Integral b => b -> Subst -> Subst #
Show Reft Source #
Instance details Methods showsPrec :: Int -> Reft -> ShowS # show :: Reft -> String # showList :: [Reft] -> ShowS #
Show SortedReft Source #
Instance details Methods showsPrec :: Int -> SortedReft -> ShowS # show :: SortedReft -> String # showList :: [SortedReft] -> ShowS #
Fixpoint Reft Source #
Instance details Methods toFix :: Reft -> Doc Source # simplify :: Reft -> Reft Source #
Fixpoint SortedReft Source #
Instance details Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
PPrint Reft Source #
Instance details Methods pprintTidy :: Tidy -> Reft -> Doc Source # pprintPrec :: Int -> Tidy -> Reft -> Doc Source #
PPrint SortedReft Source #
Instance details Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
Reftable Reft Source #
Instance details Methods isTauto :: Reft -> Bool Source # ppTy :: Reft -> Doc -> Doc Source # top :: Reft -> Reft Source # bot :: Reft -> Reft Source # meet :: Reft -> Reft -> Reft Source # toReft :: Reft -> Reft Source # ofReft :: Reft -> Reft Source # params :: Reft -> [Symbol] Source #
Reftable SortedReft Source #
Instance details Methods isTauto :: SortedReft -> Bool Source # ppTy :: SortedReft -> Doc -> Doc Source # top :: SortedReft -> SortedReft Source # bot :: SortedReft -> SortedReft Source # meet :: SortedReft -> SortedReft -> SortedReft Source # toReft :: SortedReft -> Reft Source # ofReft :: Reft -> SortedReft Source # params :: SortedReft -> [Symbol] Source #
Reftable () Source #
Instance details Methods isTauto :: () -> Bool Source # ppTy :: () -> Doc -> Doc Source # top :: () -> () Source # bot :: () -> () Source # meet :: () -> () -> () Source # toReft :: () -> Reft Source # ofReft :: Reft -> () Source # params :: () -> [Symbol] Source #
Subable Symbol Source #
Instance details Methods syms :: Symbol -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Symbol -> Symbol Source # substf :: (Symbol -> Expr) -> Symbol -> Symbol Source # subst :: Subst -> Symbol -> Symbol Source # subst1 :: Symbol -> (Symbol, Expr) -> Symbol Source #
Subable Expr Source #
Instance details Methods syms :: Expr -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Expr -> Expr Source # substf :: (Symbol -> Expr) -> Expr -> Expr Source # subst :: Subst -> Expr -> Expr Source # subst1 :: Expr -> (Symbol, Expr) -> Expr Source #
Subable Reft Source #
Instance details Methods syms :: Reft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Reft -> Reft Source # substf :: (Symbol -> Expr) -> Reft -> Reft Source # subst :: Subst -> Reft -> Reft Source # subst1 :: Reft -> (Symbol, Expr) -> Reft Source #
Subable SortedReft Source #
Instance details Methods syms :: SortedReft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft Source # substf :: (Symbol -> Expr) -> SortedReft -> SortedReft Source # subst :: Subst -> SortedReft -> SortedReft Source # subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft Source #
Subable () Source #
Instance details Methods syms :: () -> [Symbol] Source # substa :: (Symbol -> Symbol) -> () -> () Source # substf :: (Symbol -> Expr) -> () -> () Source # subst :: Subst -> () -> () Source # subst1 :: () -> (Symbol, Expr) -> () Source #
Subable a => Subable (Maybe a) Source #
Instance details Methods syms :: Maybe a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a Source # substf :: (Symbol -> Expr) -> Maybe a -> Maybe a Source # subst :: Subst -> Maybe a -> Maybe a Source # subst1 :: Maybe a -> (Symbol, Expr) -> Maybe a Source #
Subable a => Subable [a] Source #
Instance details Methods syms :: [a] -> [Symbol] Source # substa :: (Symbol -> Symbol) -> [a] -> [a] Source # substf :: (Symbol -> Expr) -> [a] -> [a] Source # subst :: Subst -> [a] -> [a] Source # subst1 :: [a] -> (Symbol, Expr) -> [a] Source #
Expression (Symbol, SortedReft) Source #
Instance details Methods expr :: (Symbol, SortedReft) -> Expr Source #
Subable a => Subable (HashMap k a) Source #
Instance details Methods syms :: HashMap k a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a Source # substf :: (Symbol -> Expr) -> HashMap k a -> HashMap k a Source # subst :: Subst -> HashMap k a -> HashMap k a Source # subst1 :: HashMap k a -> (Symbol, Expr) -> HashMap k a Source #
(Subable a, Subable b) => Subable (a, b) Source #
Instance details Methods syms :: (a, b) -> [Symbol] Source # substa :: (Symbol -> Symbol) -> (a, b) -> (a, b) Source # substf :: (Symbol -> Expr) -> (a, b) -> (a, b) Source # subst :: Subst -> (a, b) -> (a, b) Source # subst1 :: (a, b) -> (Symbol, Expr) -> (a, b) Source #