Safe Haskell	None
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 #

Orphan instances

Show SortedReft Source #
Instance details Methods showsPrec :: Int -> SortedReft -> ShowS # show :: SortedReft -> String # showList :: [SortedReft] -> ShowS #
Show Reft Source #
Instance details Methods showsPrec :: Int -> Reft -> ShowS # show :: Reft -> String # showList :: [Reft] -> ShowS #
Semigroup SortedReft Source #
Instance details Methods (<>) :: SortedReft -> SortedReft -> SortedReft # sconcat :: NonEmpty SortedReft -> SortedReft # stimes :: Integral b => b -> SortedReft -> SortedReft #
Semigroup Reft Source #
Instance details Methods (<>) :: Reft -> Reft -> Reft # sconcat :: NonEmpty Reft -> Reft # stimes :: Integral b => b -> Reft -> Reft #
Semigroup Expr Source #
Instance details Methods (<>) :: Expr -> Expr -> Expr # sconcat :: NonEmpty Expr -> Expr # stimes :: Integral b => b -> Expr -> Expr #
Semigroup Subst Source #
Instance details Methods (<>) :: Subst -> Subst -> Subst # sconcat :: NonEmpty Subst -> Subst # stimes :: Integral b => b -> Subst -> Subst #
Monoid SortedReft Source #
Instance details Methods mempty :: SortedReft # mappend :: SortedReft -> SortedReft -> SortedReft # mconcat :: [SortedReft] -> SortedReft #
Monoid Reft Source #
Instance details Methods mempty :: Reft # mappend :: Reft -> Reft -> Reft # mconcat :: [Reft] -> Reft #
Monoid Expr Source #
Instance details Methods mempty :: Expr # mappend :: Expr -> Expr -> Expr # mconcat :: [Expr] -> Expr #
Monoid Subst Source #
Instance details Methods mempty :: Subst # mappend :: Subst -> Subst -> Subst # mconcat :: [Subst] -> Subst #
PPrint SortedReft Source #
Instance details Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
PPrint Reft Source #
Instance details Methods pprintTidy :: Tidy -> Reft -> Doc Source # pprintPrec :: Int -> Tidy -> Reft -> Doc Source #
Fixpoint SortedReft Source #
Instance details Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
Fixpoint Reft Source #
Instance details Methods toFix :: Reft -> Doc Source # simplify :: Reft -> Reft 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 #
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 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 #
Subable () Source #
Instance details Methods syms :: () -> [Symbol] Source # substa :: (Symbol -> Symbol) -> () -> () Source # substf :: (Symbol -> Expr) -> () -> () Source # subst :: Subst -> () -> () Source # subst1 :: () -> (Symbol, Expr) -> () 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 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 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 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 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 #
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 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 #
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 #
Expression (Symbol, SortedReft) Source #
Instance details Methods expr :: (Symbol, SortedReft) -> Expr Source #