liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Substitutions

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

subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a 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

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

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

Fixpoint Reft Source # 
Instance details

Fixpoint SortedReft Source # 
Instance details

PPrint Reft Source # 
Instance details

PPrint SortedReft Source # 
Instance details

Reftable Reft Source # 
Instance details

Reftable SortedReft Source # 
Instance details

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

Subable Expr Source # 
Instance details

Subable Reft Source # 
Instance details

Subable SortedReft Source # 
Instance details

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 #