liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Substitutions

Contents

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

Show SortedReft Source # 
Instance details

Show Reft Source # 
Instance details

Methods

showsPrec :: Int -> Reft -> ShowS #

show :: Reft -> String #

showList :: [Reft] -> ShowS #

Semigroup SortedReft Source # 
Instance details

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

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

PPrint Reft Source # 
Instance details

Fixpoint SortedReft Source # 
Instance details

Fixpoint Reft 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 #

Reftable SortedReft Source # 
Instance details

Reftable Reft 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 Symbol Source # 
Instance details

Subable SortedReft Source # 
Instance details

Subable Reft Source # 
Instance details

Subable Expr Source # 
Instance details

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 #