liquid-fixpoint-0.7.0.5: 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 # 
Show Reft Source # 

Methods

showsPrec :: Int -> Reft -> ShowS #

show :: Reft -> String #

showList :: [Reft] -> ShowS #

Monoid SortedReft Source # 
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 # 
PPrint Reft Source # 
Fixpoint SortedReft Source # 
Fixpoint 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 # 
Reftable Reft 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 # 
Subable SortedReft Source # 
Subable Reft Source # 
Subable 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 #