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