liquid-fixpoint-0.9.6.3.4: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Refinements

Description

This module has the types for representing terms in the refinement logic.

Synopsis

Representing Terms

newtype SymConst Source #

Expressions ---------------------------------------------------------------

Uninterpreted constants that are embedded as "constant symbol : Str"

Constructors

SL Text 

Instances

Instances details
FromJSON SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser SymConst #

parseJSONList :: Value -> Parser [SymConst] #

omittedField :: Maybe SymConst #

ToJSON SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: SymConst -> Value #

toEncoding :: SymConst -> Encoding #

toJSONList :: [SymConst] -> Value #

toEncodingList :: [SymConst] -> Encoding #

omitField :: SymConst -> Bool #

Data SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymConst -> c SymConst #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymConst #

toConstr :: SymConst -> Constr #

dataTypeOf :: SymConst -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymConst) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst) #

gmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymConst -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymConst -> r #

gmapQ :: (forall d. Data d => d -> u) -> SymConst -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymConst -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

Generic SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SymConst 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SymConst = D1 ('MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

Methods

from :: SymConst -> Rep SymConst x #

to :: Rep SymConst x -> SymConst #

Show SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> SymConst -> ShowS #

show :: SymConst -> String #

showList :: [SymConst] -> ShowS #

Binary SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SymConst -> Put #

get :: Get SymConst #

putList :: [SymConst] -> Put #

NFData SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SymConst -> () #

Eq SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: SymConst -> SymConst -> Bool #

(/=) :: SymConst -> SymConst -> Bool #

Ord SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: SymConst -> SymConst -> Ordering #

(<) :: SymConst -> SymConst -> Bool #

(<=) :: SymConst -> SymConst -> Bool #

(>) :: SymConst -> SymConst -> Bool #

(>=) :: SymConst -> SymConst -> Bool #

max :: SymConst -> SymConst -> SymConst #

min :: SymConst -> SymConst -> SymConst #

Hashable SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> SymConst -> Int #

hash :: SymConst -> Int #

SMTLIB2 SymConst Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymConst -> SymM Builder Source #

Symbolic SymConst Source #

String Constants ----------------------------------------------------------

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

symbol :: SymConst -> Symbol Source #

Fixpoint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: SymConst -> Doc Source #

simplify :: SymConst -> SymConst Source #

PPrint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SymConst -> Doc Source #

pprintPrec :: Int -> Tidy -> SymConst -> Doc Source #

Store SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size SymConst #

poke :: SymConst -> Poke () #

peek :: Peek SymConst #

type Rep SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SymConst = D1 ('MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

data Constant Source #

Constructors

I !Integer 
R !Double 
L !Text !Sort 

Instances

Instances details
FromJSON Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser Constant #

parseJSONList :: Value -> Parser [Constant] #

omittedField :: Maybe Constant #

ToJSON Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: Constant -> Value #

toEncoding :: Constant -> Encoding #

toJSONList :: [Constant] -> Value #

toEncodingList :: [Constant] -> Encoding #

omitField :: Constant -> Bool #

Data Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constant -> c Constant #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constant #

toConstr :: Constant -> Constr #

dataTypeOf :: Constant -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constant) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant) #

gmapT :: (forall b. Data b => b -> b) -> Constant -> Constant #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constant -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constant -> r #

gmapQ :: (forall d. Data d => d -> u) -> Constant -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constant -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

Generic Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Constant 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Constant = D1 ('MetaData "Constant" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer)) :+: (C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Double)) :+: C1 ('MetaCons "L" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

Methods

from :: Constant -> Rep Constant x #

to :: Rep Constant x -> Constant #

Show Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Constant -> ShowS #

show :: Constant -> String #

showList :: [Constant] -> ShowS #

Binary Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Constant -> Put #

get :: Get Constant #

putList :: [Constant] -> Put #

NFData Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Constant -> () #

Eq Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Constant -> Constant -> Bool #

(/=) :: Constant -> Constant -> Bool #

Ord Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Constant -> Constant -> Ordering #

(<) :: Constant -> Constant -> Bool #

(<=) :: Constant -> Constant -> Bool #

(>) :: Constant -> Constant -> Bool #

(>=) :: Constant -> Constant -> Bool #

max :: Constant -> Constant -> Constant #

min :: Constant -> Constant -> Constant #

Hashable Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Constant -> Int #

hash :: Constant -> Int #

Inputable Constant Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Constant Source #

rr' :: String -> String -> Constant Source #

SMTLIB2 Constant Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Constant -> SymM Builder Source #

Fixpoint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Constant -> Doc Source #

simplify :: Constant -> Constant Source #

PPrint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Constant -> Doc Source #

pprintPrec :: Int -> Tidy -> Constant -> Doc Source #

Store Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Constant #

poke :: Constant -> Poke () #

peek :: Peek Constant #

type Rep Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Constant = D1 ('MetaData "Constant" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer)) :+: (C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Double)) :+: C1 ('MetaCons "L" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

data Bop Source #

Constructors

Plus 
Minus 
Times 
Div 
Mod 
RTimes 
RDiv 

Instances

Instances details
FromJSON Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser Bop #

parseJSONList :: Value -> Parser [Bop] #

omittedField :: Maybe Bop #

ToJSON Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: Bop -> Value #

toEncoding :: Bop -> Encoding #

toJSONList :: [Bop] -> Value #

toEncodingList :: [Bop] -> Encoding #

omitField :: Bop -> Bool #

Data Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Bop -> c Bop #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Bop #

toConstr :: Bop -> Constr #

dataTypeOf :: Bop -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Bop) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop) #

gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r #

gmapQ :: (forall d. Data d => d -> u) -> Bop -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Bop -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

Generic Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Bop 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Bop = D1 ('MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((C1 ('MetaCons "Plus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Minus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Times" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTimes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RDiv" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: Bop -> Rep Bop x #

to :: Rep Bop x -> Bop #

Show Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Bop -> ShowS #

show :: Bop -> String #

showList :: [Bop] -> ShowS #

Binary Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Bop -> Put #

get :: Get Bop #

putList :: [Bop] -> Put #

NFData Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Bop -> () #

Eq Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Bop -> Bop -> Bool #

(/=) :: Bop -> Bop -> Bool #

Ord Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Bop -> Bop -> Ordering #

(<) :: Bop -> Bop -> Bool #

(<=) :: Bop -> Bop -> Bool #

(>) :: Bop -> Bop -> Bool #

(>=) :: Bop -> Bop -> Bool #

max :: Bop -> Bop -> Bop #

min :: Bop -> Bop -> Bop #

Hashable Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Bop -> Int #

hash :: Bop -> Int #

SMTLIB2 Bop Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Bop -> SymM Builder Source #

Fixpoint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Bop -> Doc Source #

simplify :: Bop -> Bop Source #

PPrint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Bop -> Doc Source #

pprintPrec :: Int -> Tidy -> Bop -> Doc Source #

Store Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Bop #

poke :: Bop -> Poke () #

peek :: Peek Bop #

type Rep Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Bop = D1 ('MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((C1 ('MetaCons "Plus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Minus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Times" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTimes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RDiv" 'PrefixI 'False) (U1 :: Type -> Type))))

data Brel Source #

Constructors

Eq 
Ne 
Gt 
Ge 
Lt 
Le 
Ueq 
Une 

Instances

Instances details
FromJSON Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser Brel #

parseJSONList :: Value -> Parser [Brel] #

omittedField :: Maybe Brel #

ToJSON Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: Brel -> Value #

toEncoding :: Brel -> Encoding #

toJSONList :: [Brel] -> Value #

toEncodingList :: [Brel] -> Encoding #

omitField :: Brel -> Bool #

Data Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Brel -> c Brel #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Brel #

toConstr :: Brel -> Constr #

dataTypeOf :: Brel -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Brel) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel) #

gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r #

gmapQ :: (forall d. Data d => d -> u) -> Brel -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Brel -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

Generic Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Brel 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Brel = D1 ('MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (((C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ne" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ge" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ueq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Une" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: Brel -> Rep Brel x #

to :: Rep Brel x -> Brel #

Show Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Brel -> ShowS #

show :: Brel -> String #

showList :: [Brel] -> ShowS #

Binary Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Brel -> Put #

get :: Get Brel #

putList :: [Brel] -> Put #

NFData Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Brel -> () #

Eq Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Brel -> Brel -> Bool #

(/=) :: Brel -> Brel -> Bool #

Ord Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Brel -> Brel -> Ordering #

(<) :: Brel -> Brel -> Bool #

(<=) :: Brel -> Brel -> Bool #

(>) :: Brel -> Brel -> Bool #

(>=) :: Brel -> Brel -> Bool #

max :: Brel -> Brel -> Brel #

min :: Brel -> Brel -> Brel #

Hashable Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Brel -> Int #

hash :: Brel -> Int #

SMTLIB2 Brel Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Brel -> SymM Builder Source #

Fixpoint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Brel -> Doc Source #

simplify :: Brel -> Brel Source #

PPrint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Brel -> Doc Source #

pprintPrec :: Int -> Tidy -> Brel -> Doc Source #

Store Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Brel #

poke :: Brel -> Poke () #

peek :: Peek Brel #

type Rep Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Brel = D1 ('MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (((C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ne" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ge" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ueq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Une" 'PrefixI 'False) (U1 :: Type -> Type))))

data ExprV v Source #

Constructors

ESym !SymConst 
ECon !Constant 
EVar !v 
EApp !(ExprV v) !(ExprV v) 
ENeg !(ExprV v) 
EBin !Bop !(ExprV v) !(ExprV v) 
ELet !Symbol !(ExprV v) !(ExprV v) 
EIte !(ExprV v) !(ExprV v) !(ExprV v) 
ECst !(ExprV v) !Sort 
ELam !(Symbol, Sort) !(ExprV v) 
ETApp !(ExprV v) !Sort 
ETAbs !(ExprV v) !Symbol 
PAnd ![ExprV v] 
POr ![ExprV v] 
PNot !(ExprV v) 
PImp !(ExprV v) !(ExprV v) 
PIff !(ExprV v) !(ExprV v) 
PAtom !Brel !(ExprV v) !(ExprV v) 
PKVar !KVar !(SubstV v) 
PAll ![(Symbol, Sort)] !(ExprV v) 
PExist ![(Symbol, Sort)] !(ExprV v) 
ECoerc !Sort !Sort !(ExprV v) 

Instances

Instances details
FromJSON Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser Expr #

parseJSONList :: Value -> Parser [Expr] #

omittedField :: Maybe Expr #

ToJSON Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: Expr -> Value #

toEncoding :: Expr -> Encoding #

toJSONList :: [Expr] -> Value #

toEncodingList :: [Expr] -> Encoding #

omitField :: Expr -> Bool #

Foldable ExprV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fold :: Monoid m => ExprV m -> m #

foldMap :: Monoid m => (a -> m) -> ExprV a -> m #

foldMap' :: Monoid m => (a -> m) -> ExprV a -> m #

foldr :: (a -> b -> b) -> b -> ExprV a -> b #

foldr' :: (a -> b -> b) -> b -> ExprV a -> b #

foldl :: (b -> a -> b) -> b -> ExprV a -> b #

foldl' :: (b -> a -> b) -> b -> ExprV a -> b #

foldr1 :: (a -> a -> a) -> ExprV a -> a #

foldl1 :: (a -> a -> a) -> ExprV a -> a #

toList :: ExprV a -> [a] #

null :: ExprV a -> Bool #

length :: ExprV a -> Int #

elem :: Eq a => a -> ExprV a -> Bool #

maximum :: Ord a => ExprV a -> a #

minimum :: Ord a => ExprV a -> a #

sum :: Num a => ExprV a -> a #

product :: Num a => ExprV a -> a #

Traversable ExprV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

traverse :: Applicative f => (a -> f b) -> ExprV a -> f (ExprV b) #

sequenceA :: Applicative f => ExprV (f a) -> f (ExprV a) #

mapM :: Monad m => (a -> m b) -> ExprV a -> m (ExprV b) #

sequence :: Monad m => ExprV (m a) -> m (ExprV a) #

Functor ExprV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fmap :: (a -> b) -> ExprV a -> ExprV b #

(<$) :: a -> ExprV b -> ExprV a #

Defunc Expr Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Expr -> DF Expr Source #

Inputable Expr Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Expr Source #

rr' :: String -> String -> Expr Source #

SMTLIB2 Expr Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Expr -> SymM Builder Source #

Simplifiable Expr Source # 
Instance details

Defined in Language.Fixpoint.Solver.Interpreter

Methods

simplify :: Knowledge -> ICtx -> Expr -> Expr Source #

Elaborate Expr Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: ElabParam -> Expr -> Expr Source #

Expression Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr Source #

Predicate Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr Source #

Subable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 #

ToHornSMT Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.SMTPrint

Methods

toHornSMT :: Expr -> Doc Source #

Foldable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

foldE :: Monoid a => Folder a c -> c -> Expr -> FoldM a Expr Source #

SymConsts Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Expr -> [SymConst] Source #

Visitable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

transE :: (Expr -> Expr) -> Expr -> Expr Source #

Store Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Expr #

poke :: Expr -> Poke () #

peek :: Peek Expr #

Data v => Data (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExprV v -> c (ExprV v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ExprV v) #

toConstr :: ExprV v -> Constr #

dataTypeOf :: ExprV v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ExprV v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v)) #

gmapT :: (forall b. Data b => b -> b) -> ExprV v -> ExprV v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprV v -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprV v -> r #

gmapQ :: (forall d. Data d => d -> u) -> ExprV v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprV v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) #

Generic (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep (ExprV v) 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (ExprV v) = D1 ('MetaData "ExprV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((((C1 ('MetaCons "ESym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymConst)) :+: C1 ('MetaCons "ECon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Constant))) :+: (C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 v)) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ENeg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "EBin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bop) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: (C1 ('MetaCons "ELet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: C1 ('MetaCons "EIte" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: (C1 ('MetaCons "ECst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :+: (C1 ('MetaCons "ELam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Symbol, Sort)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v]))) :+: (C1 ('MetaCons "POr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v])) :+: (C1 ('MetaCons "PNot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "PImp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "PIff" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "PAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Brel) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: C1 ('MetaCons "PKVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SubstV v))))) :+: (C1 ('MetaCons "PAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "PExist" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ECoerc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))))))

Methods

from :: ExprV v -> Rep (ExprV v) x #

to :: Rep (ExprV v) x -> ExprV v #

(Show v, Fixpoint v, Ord v) => Show (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> ExprV v -> ShowS #

show :: ExprV v -> String #

showList :: [ExprV v] -> ShowS #

Binary v => Binary (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: ExprV v -> Put #

get :: Get (ExprV v) #

putList :: [ExprV v] -> Put #

NFData v => NFData (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: ExprV v -> () #

Eq v => Eq (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: ExprV v -> ExprV v -> Bool #

(/=) :: ExprV v -> ExprV v -> Bool #

Ord v => Ord (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: ExprV v -> ExprV v -> Ordering #

(<) :: ExprV v -> ExprV v -> Bool #

(<=) :: ExprV v -> ExprV v -> Bool #

(>) :: ExprV v -> ExprV v -> Bool #

(>=) :: ExprV v -> ExprV v -> Bool #

max :: ExprV v -> ExprV v -> ExprV v #

min :: ExprV v -> ExprV v -> ExprV v #

Hashable v => Hashable (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> ExprV v -> Int #

hash :: ExprV v -> Int #

SMTLIB2 (Triggered Expr) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Triggered Expr -> SymM Builder Source #

(Ord v, Fixpoint v) => Fixpoint (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: ExprV v -> Doc Source #

simplify :: ExprV v -> ExprV v Source #

(Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> ExprV v -> Doc Source #

pprintPrec :: Int -> Tidy -> ExprV v -> Doc Source #

SMTLIB2 (Symbol, Expr) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: (Symbol, Expr) -> SymM Builder Source #

type Rep (ExprV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (ExprV v) = D1 ('MetaData "ExprV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((((C1 ('MetaCons "ESym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymConst)) :+: C1 ('MetaCons "ECon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Constant))) :+: (C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 v)) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ENeg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "EBin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bop) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: (C1 ('MetaCons "ELet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: C1 ('MetaCons "EIte" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: (C1 ('MetaCons "ECst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :+: (C1 ('MetaCons "ELam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Symbol, Sort)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)))))) :+: (((C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v]))) :+: (C1 ('MetaCons "POr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v])) :+: (C1 ('MetaCons "PNot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "PImp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "PIff" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "PAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Brel) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: C1 ('MetaCons "PKVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SubstV v))))) :+: (C1 ('MetaCons "PAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "PExist" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ECoerc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))))))

type Pred = Expr Source #

type Expr = ExprV Symbol Source #

pattern PTrue :: ExprV v Source #

pattern PTop :: ExprV v Source #

pattern PFalse :: ExprV v Source #

pattern EBot :: ExprV v Source #

pattern ETimes :: ExprV v -> ExprV v -> ExprV v Source #

pattern ERTimes :: ExprV v -> ExprV v -> ExprV v Source #

pattern EDiv :: ExprV v -> ExprV v -> ExprV v Source #

pattern ERDiv :: ExprV v -> ExprV v -> ExprV v Source #

pattern EEq :: ExprV v -> ExprV v -> ExprV v Source #

newtype KVar Source #

Kvars ---------------------------------------------------------------------

Constructors

KV 

Fields

Instances

Instances details
FromJSON KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser KVar #

parseJSONList :: Value -> Parser [KVar] #

omittedField :: Maybe KVar #

ToJSON KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: KVar -> Value #

toEncoding :: KVar -> Encoding #

toJSONList :: [KVar] -> Value #

toEncodingList :: [KVar] -> Encoding #

omitField :: KVar -> Bool #

ToJSONKey KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSONKey :: ToJSONKeyFunction KVar #

toJSONKeyList :: ToJSONKeyFunction [KVar] #

Data KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVar -> c KVar #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVar #

toConstr :: KVar -> Constr #

dataTypeOf :: KVar -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVar) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar) #

gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r #

gmapQ :: (forall d. Data d => d -> u) -> KVar -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KVar -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

IsString KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fromString :: String -> KVar #

Generic KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVar 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "KV" 'PrefixI 'True) (S1 ('MetaSel ('Just "kv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

Methods

from :: KVar -> Rep KVar x #

to :: Rep KVar x -> KVar #

Show KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVar -> ShowS #

show :: KVar -> String #

showList :: [KVar] -> ShowS #

Binary KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: KVar -> Put #

get :: Get KVar #

putList :: [KVar] -> Put #

NFData KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: KVar -> () #

Eq KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: KVar -> KVar -> Bool #

(/=) :: KVar -> KVar -> Bool #

Ord KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: KVar -> KVar -> Ordering #

(<) :: KVar -> KVar -> Bool #

(<=) :: KVar -> KVar -> Bool #

(>) :: KVar -> KVar -> Bool #

(>=) :: KVar -> KVar -> Bool #

max :: KVar -> KVar -> KVar #

min :: KVar -> KVar -> KVar #

Hashable KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> KVar -> Int #

hash :: KVar -> Int #

Fixpoint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: KVar -> Doc Source #

simplify :: KVar -> KVar Source #

PPrint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVar -> Doc Source #

pprintPrec :: Int -> Tidy -> KVar -> Doc Source #

ToHornSMT KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.SMTPrint

Methods

toHornSMT :: KVar -> Doc Source #

Store KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size KVar #

poke :: KVar -> Poke () #

peek :: Peek KVar #

type Rep KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "KV" 'PrefixI 'True) (S1 ('MetaSel ('Just "kv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

type Subst = SubstV Symbol Source #

Substitutions -------------------------------------------------------------

newtype SubstV v Source #

Constructors

Su (HashMap Symbol (ExprV v)) 

Instances

Instances details
FromJSON Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

parseJSON :: Value -> Parser Subst #

parseJSONList :: Value -> Parser [Subst] #

omittedField :: Maybe Subst #

ToJSON Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toJSON :: Subst -> Value #

toEncoding :: Subst -> Encoding #

toJSONList :: [Subst] -> Value #

toEncodingList :: [Subst] -> Encoding #

omitField :: Subst -> Bool #

Foldable SubstV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fold :: Monoid m => SubstV m -> m #

foldMap :: Monoid m => (a -> m) -> SubstV a -> m #

foldMap' :: Monoid m => (a -> m) -> SubstV a -> m #

foldr :: (a -> b -> b) -> b -> SubstV a -> b #

foldr' :: (a -> b -> b) -> b -> SubstV a -> b #

foldl :: (b -> a -> b) -> b -> SubstV a -> b #

foldl' :: (b -> a -> b) -> b -> SubstV a -> b #

foldr1 :: (a -> a -> a) -> SubstV a -> a #

foldl1 :: (a -> a -> a) -> SubstV a -> a #

toList :: SubstV a -> [a] #

null :: SubstV a -> Bool #

length :: SubstV a -> Int #

elem :: Eq a => a -> SubstV a -> Bool #

maximum :: Ord a => SubstV a -> a #

minimum :: Ord a => SubstV a -> a #

sum :: Num a => SubstV a -> a #

product :: Num a => SubstV a -> a #

Traversable SubstV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

traverse :: Applicative f => (a -> f b) -> SubstV a -> f (SubstV b) #

sequenceA :: Applicative f => SubstV (f a) -> f (SubstV a) #

mapM :: Monad m => (a -> m b) -> SubstV a -> m (SubstV b) #

sequence :: Monad m => SubstV (m a) -> m (SubstV a) #

Functor SubstV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fmap :: (a -> b) -> SubstV a -> SubstV b #

(<$) :: a -> SubstV b -> SubstV a #

Monoid Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Subst #

mappend :: Subst -> Subst -> Subst #

mconcat :: [Subst] -> Subst #

Semigroup Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Subst -> Subst -> Subst #

sconcat :: NonEmpty Subst -> Subst #

stimes :: Integral b => b -> Subst -> Subst #

ToHornSMT Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.SMTPrint

Methods

toHornSMT :: Subst -> Doc Source #

Store Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Subst #

poke :: Subst -> Poke () #

peek :: Peek Subst #

Data v => Data (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SubstV v -> c (SubstV v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SubstV v) #

toConstr :: SubstV v -> Constr #

dataTypeOf :: SubstV v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SubstV v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v)) #

gmapT :: (forall b. Data b => b -> b) -> SubstV v -> SubstV v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SubstV v -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SubstV v -> r #

gmapQ :: (forall d. Data d => d -> u) -> SubstV v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SubstV v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) #

Generic (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep (SubstV v) 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (SubstV v) = D1 ('MetaData "SubstV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "Su" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol (ExprV v)))))

Methods

from :: SubstV v -> Rep (SubstV v) x #

to :: Rep (SubstV v) x -> SubstV v #

(Fixpoint v, Ord v, Show v) => Show (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> SubstV v -> ShowS #

show :: SubstV v -> String #

showList :: [SubstV v] -> ShowS #

Binary v => Binary (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SubstV v -> Put #

get :: Get (SubstV v) #

putList :: [SubstV v] -> Put #

NFData v => NFData (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SubstV v -> () #

Eq v => Eq (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: SubstV v -> SubstV v -> Bool #

(/=) :: SubstV v -> SubstV v -> Bool #

Ord v => Ord (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: SubstV v -> SubstV v -> Ordering #

(<) :: SubstV v -> SubstV v -> Bool #

(<=) :: SubstV v -> SubstV v -> Bool #

(>) :: SubstV v -> SubstV v -> Bool #

(>=) :: SubstV v -> SubstV v -> Bool #

max :: SubstV v -> SubstV v -> SubstV v #

min :: SubstV v -> SubstV v -> SubstV v #

Hashable v => Hashable (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> SubstV v -> Int #

hash :: SubstV v -> Int #

(Ord v, Fixpoint v) => Fixpoint (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: SubstV v -> Doc Source #

simplify :: SubstV v -> SubstV v Source #

(Ord v, Fixpoint v) => PPrint (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SubstV v -> Doc Source #

pprintPrec :: Int -> Tidy -> SubstV v -> Doc Source #

type Rep (SubstV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (SubstV v) = D1 ('MetaData "SubstV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "Su" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol (ExprV v)))))

data KVSub Source #

Constructors

KVS 

Fields

Instances

Instances details
Data KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVSub -> c KVSub #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVSub #

toConstr :: KVSub -> Constr #

dataTypeOf :: KVSub -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVSub) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub) #

gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r #

gmapQ :: (forall d. Data d => d -> u) -> KVSub -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KVSub -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

Generic KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVSub 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVSub = D1 ('MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "KVS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ksuVV") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ksuSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "ksuKVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KVar) :*: S1 ('MetaSel ('Just "ksuSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Subst))))

Methods

from :: KVSub -> Rep KVSub x #

to :: Rep KVSub x -> KVSub #

Show KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVSub -> ShowS #

show :: KVSub -> String #

showList :: [KVSub] -> ShowS #

Eq KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: KVSub -> KVSub -> Bool #

(/=) :: KVSub -> KVSub -> Bool #

PPrint KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVSub -> Doc Source #

pprintPrec :: Int -> Tidy -> KVSub -> Doc Source #

type Rep KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVSub = D1 ('MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "KVS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ksuVV") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ksuSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "ksuKVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KVar) :*: S1 ('MetaSel ('Just "ksuSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Subst))))

type Reft = ReftV Symbol Source #

newtype ReftV v Source #

Refinement of v satisfying a predicate e.g. in '{x: _ | e }' x is the Symbol and e the ExprV v

Constructors

Reft (Symbol, ExprV v) 

Instances

Instances details
Foldable ReftV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fold :: Monoid m => ReftV m -> m #

foldMap :: Monoid m => (a -> m) -> ReftV a -> m #

foldMap' :: Monoid m => (a -> m) -> ReftV a -> m #

foldr :: (a -> b -> b) -> b -> ReftV a -> b #

foldr' :: (a -> b -> b) -> b -> ReftV a -> b #

foldl :: (b -> a -> b) -> b -> ReftV a -> b #

foldl' :: (b -> a -> b) -> b -> ReftV a -> b #

foldr1 :: (a -> a -> a) -> ReftV a -> a #

foldl1 :: (a -> a -> a) -> ReftV a -> a #

toList :: ReftV a -> [a] #

null :: ReftV a -> Bool #

length :: ReftV a -> Int #

elem :: Eq a => a -> ReftV a -> Bool #

maximum :: Ord a => ReftV a -> a #

minimum :: Ord a => ReftV a -> a #

sum :: Num a => ReftV a -> a #

product :: Num a => ReftV a -> a #

Traversable ReftV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

traverse :: Applicative f => (a -> f b) -> ReftV a -> f (ReftV b) #

sequenceA :: Applicative f => ReftV (f a) -> f (ReftV a) #

mapM :: Monad m => (a -> m b) -> ReftV a -> m (ReftV b) #

sequence :: Monad m => ReftV (m a) -> m (ReftV a) #

Functor ReftV Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fmap :: (a -> b) -> ReftV a -> ReftV b #

(<$) :: a -> ReftV b -> ReftV a #

Show Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

showsPrec :: Int -> Reft -> ShowS #

show :: Reft -> String #

showList :: [Reft] -> ShowS #

Defunc Reft Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Reft -> DF Reft Source #

Fixpoint Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

toFix :: Reft -> Doc Source #

simplify :: Reft -> Reft Source #

Expression Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr Source #

Subable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 #

Foldable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

foldE :: Monoid a => Folder a c -> c -> Reft -> FoldM a Reft Source #

SymConsts Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Reft -> [SymConst] Source #

Visitable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

transE :: (Expr -> Expr) -> Reft -> Reft Source #

Store Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Reft #

poke :: Reft -> Poke () #

peek :: Peek Reft #

Data v => Data (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ReftV v -> c (ReftV v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ReftV v) #

toConstr :: ReftV v -> Constr #

dataTypeOf :: ReftV v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ReftV v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v)) #

gmapT :: (forall b. Data b => b -> b) -> ReftV v -> ReftV v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ReftV v -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ReftV v -> r #

gmapQ :: (forall d. Data d => d -> u) -> ReftV v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ReftV v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) #

Generic (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep (ReftV v) 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (ReftV v) = D1 ('MetaData "ReftV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, ExprV v))))

Methods

from :: ReftV v -> Rep (ReftV v) x #

to :: Rep (ReftV v) x -> ReftV v #

Binary v => Binary (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: ReftV v -> Put #

get :: Get (ReftV v) #

putList :: [ReftV v] -> Put #

NFData v => NFData (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: ReftV v -> () #

Eq v => Eq (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: ReftV v -> ReftV v -> Bool #

(/=) :: ReftV v -> ReftV v -> Bool #

Ord v => Ord (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: ReftV v -> ReftV v -> Ordering #

(<) :: ReftV v -> ReftV v -> Bool #

(<=) :: ReftV v -> ReftV v -> Bool #

(>) :: ReftV v -> ReftV v -> Bool #

(>=) :: ReftV v -> ReftV v -> Bool #

max :: ReftV v -> ReftV v -> ReftV v #

min :: ReftV v -> ReftV v -> ReftV v #

Hashable v => Hashable (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> ReftV v -> Int #

hash :: ReftV v -> Int #

(PPrint v, Fixpoint v, Ord v) => PPrint (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

pprintTidy :: Tidy -> ReftV v -> Doc Source #

pprintPrec :: Int -> Tidy -> ReftV v -> Doc Source #

type Rep (ReftV v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep (ReftV v) = D1 ('MetaData "ReftV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, ExprV v))))

data SortedReft Source #

Constructors

RR 

Fields

Instances

Instances details
Data SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SortedReft -> c SortedReft #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SortedReft #

toConstr :: SortedReft -> Constr #

dataTypeOf :: SortedReft -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SortedReft) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft) #

gmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SortedReft -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SortedReft -> r #

gmapQ :: (forall d. Data d => d -> u) -> SortedReft -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SortedReft -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

Generic SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SortedReft 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SortedReft = D1 ('MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "RR" 'PrefixI 'True) (S1 ('MetaSel ('Just "sr_sort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "sr_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Reft)))

Methods

from :: SortedReft -> Rep SortedReft x #

to :: Rep SortedReft x -> SortedReft #

Show SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

showsPrec :: Int -> SortedReft -> ShowS #

show :: SortedReft -> String #

showList :: [SortedReft] -> ShowS #

NFData SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SortedReft -> () #

Eq SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: SortedReft -> SortedReft -> Bool #

(/=) :: SortedReft -> SortedReft -> Bool #

Ord SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: SortedReft -> SortedReft -> Ordering #

(<) :: SortedReft -> SortedReft -> Bool #

(<=) :: SortedReft -> SortedReft -> Bool #

(>) :: SortedReft -> SortedReft -> Bool #

(>=) :: SortedReft -> SortedReft -> Bool #

max :: SortedReft -> SortedReft -> SortedReft #

min :: SortedReft -> SortedReft -> SortedReft #

Hashable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> SortedReft -> Int #

hash :: SortedReft -> Int #

Defunc SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: SortedReft -> DF SortedReft Source #

Elaborate SortedReft Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: ElabParam -> SortedReft -> SortedReft Source #

Fixpoint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

toFix :: SortedReft -> Doc Source #

simplify :: SortedReft -> SortedReft Source #

PPrint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

pprintTidy :: Tidy -> SortedReft -> Doc Source #

pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #

Expression SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr Source #

Subable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 #

Foldable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

foldE :: Monoid a => Folder a c -> c -> SortedReft -> FoldM a SortedReft Source #

SymConsts SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SortedReft -> [SymConst] Source #

Visitable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

transE :: (Expr -> Expr) -> SortedReft -> SortedReft Source #

Store SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size SortedReft #

poke :: SortedReft -> Poke () #

peek :: Peek SortedReft #

Monoid (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: BindEnv a #

mappend :: BindEnv a -> BindEnv a -> BindEnv a #

mconcat :: [BindEnv a] -> BindEnv a #

Semigroup (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: BindEnv a -> BindEnv a -> BindEnv a #

sconcat :: NonEmpty (BindEnv a) -> BindEnv a #

stimes :: Integral b => b -> BindEnv a -> BindEnv a #

NFData a => NFData (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv a -> () #

Defunc (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv a -> DF (BindEnv a) Source #

Loc a => Elaborate (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: ElabParam -> BindEnv a -> BindEnv a Source #

Fixpoint (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: BindEnv a -> Doc Source #

simplify :: BindEnv a -> BindEnv a Source #

Foldable (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

foldE :: Monoid a0 => Folder a0 c -> c -> BindEnv a -> FoldM a0 (BindEnv a) Source #

SymConsts (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv a -> [SymConst] Source #

Visitable (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

transE :: (Expr -> Expr) -> BindEnv a -> BindEnv a Source #

Store a => Store (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

size :: Size (BindEnv a) #

poke :: BindEnv a -> Poke () #

peek :: Peek (BindEnv a) #

Defunc (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) Source #

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr Source #

Foldable (Symbol, SortedReft, a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

foldE :: Monoid a0 => Folder a0 c -> c -> (Symbol, SortedReft, a) -> FoldM a0 (Symbol, SortedReft, a) Source #

Visitable (Symbol, SortedReft, a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

transE :: (Expr -> Expr) -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a) Source #

type Rep SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SortedReft = D1 ('MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "RR" 'PrefixI 'True) (S1 ('MetaSel ('Just "sr_sort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "sr_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Reft)))

Constructing Terms

eVar :: Symbolic a => a -> Expr Source #

elit :: Located Symbol -> Sort -> Expr Source #

eProp :: Symbolic a => a -> Expr Source #

conj :: [Pred] -> Pred Source #

conj is a fast version of pAnd needed for the ebind tests

pAnd :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v Source #

NOTE: pAnd-SLOW
pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

pOr :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v Source #

NOTE: pAnd-SLOW
pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v Source #

pAndNoDedup :: ListNE Pred -> Pred Source #

(&.&) :: Pred -> Pred -> Pred infixl 9 Source #

(|.|) :: Pred -> Pred -> Pred infixl 9 Source #

pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v Source #

mkEApp :: LocSymbol -> [Expr] -> Expr Source #

mkProp :: Expr -> Pred Source #

intKvar :: Integer -> KVar Source #

vv_ :: Symbol Source #

Generalizing Embedding with Typeclasses

class Expression a where Source #

Generalizing Symbol, Expression, Predicate into Classes -----------

Values that can be viewed as Constants

Values that can be viewed as Expressions

Methods

expr :: a -> Expr Source #

Instances

Instances details
Expression Symbol Source #

The symbol may be an encoding of a SymConst.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr Source #

Expression Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr Source #

Expression Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr Source #

Expression SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr Source #

Expression Text Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Text -> Expr Source #

Expression Integer Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Integer -> Expr Source #

Expression Int Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Int -> Expr Source #

Expression a => Expression (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr Source #

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr Source #

class Predicate a where Source #

Values that can be viewed as Predicates

Methods

prop :: a -> Expr Source #

Instances

Instances details
Predicate Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr Source #

Predicate Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr Source #

Predicate Bool Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Bool -> Expr Source #

class Subable a where Source #

Class Predicates for Valid Refinements -----------------------------

Minimal complete definition

syms, substa, substf, subst

Methods

syms Source #

Arguments

:: a 
-> [Symbol]

free symbols of a

substa :: (Symbol -> Symbol) -> a -> a Source #

substf :: (Symbol -> Expr) -> a -> a Source #

subst :: Subst -> a -> a Source #

subst1 :: a -> (Symbol, Expr) -> a Source #

Instances

Instances details
Subable Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Pred -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Pred -> Pred Source #

substf :: (Symbol -> Expr) -> Pred -> Pred Source #

subst :: Subst -> Pred -> Pred Source #

subst1 :: Pred -> (Symbol, Expr) -> Pred Source #

Subable Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

syms :: Equation -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Equation -> Equation Source #

substf :: (Symbol -> Expr) -> Equation -> Equation Source #

subst :: Subst -> Equation -> Equation Source #

subst1 :: Equation -> (Symbol, Expr) -> Equation Source #

Subable Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

syms :: Qualifier -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier Source #

substf :: (Symbol -> Expr) -> Qualifier -> Qualifier Source #

subst :: Subst -> Qualifier -> Qualifier Source #

subst1 :: Qualifier -> (Symbol, Expr) -> Qualifier Source #

Subable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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

Defined in Language.Fixpoint.Types.Substitutions

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 SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 () Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: () -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> () -> () Source #

substf :: (Symbol -> Expr) -> () -> () Source #

subst :: Subst -> () -> () Source #

subst1 :: () -> (Symbol, Expr) -> () Source #

Subable (Bind a) Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Bind a -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Bind a -> Bind a Source #

substf :: (Symbol -> Expr) -> Bind a -> Bind a Source #

subst :: Subst -> Bind a -> Bind a Source #

subst1 :: Bind a -> (Symbol, Expr) -> Bind a Source #

Subable a => Subable (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

syms :: Located a -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Located a -> Located a Source #

substf :: (Symbol -> Expr) -> Located a -> Located a Source #

subst :: Subst -> Located a -> Located a Source #

subst1 :: Located a -> (Symbol, Expr) -> Located a Source #

Subable a => Subable (Maybe a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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

Defined in Language.Fixpoint.Types.Substitutions

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 (HashMap k a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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

Defined in Language.Fixpoint.Types.Substitutions

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 #

Constructors

reft :: Symbol -> ExprV v -> ReftV v Source #

trueSortedReft :: Sort -> SortedReft Source #

trueReft :: ReftV v Source #

falseReft :: ReftV v Source #

exprReft :: Expression a => a -> Reft Source #

notExprReft :: Expression a => a -> Reft Source #

uexprReft :: Expression a => a -> Reft Source #

symbolReft :: Symbolic a => a -> Reft Source #

Generally Useful Refinements --------------------------

usymbolReft :: Symbolic a => a -> Reft Source #

propReft :: Predicate a => a -> Reft Source #

predReft :: Predicate a => a -> Reft Source #

reftPred :: ReftV v -> ExprV v Source #

reftBind :: ReftV v -> Symbol Source #

Predicates

isFunctionSortedReft :: SortedReft -> Bool Source #

Refinements ----------------------------------------------

functionSort :: Sort -> Maybe ([Int], [Sort], Sort) Source #

isNonTrivial :: SortedReft -> Bool Source #

isContraPred :: Eq v => ExprV v -> Bool Source #

isTautoPred :: Eq v => ExprV v -> Bool Source #

isTautoReft :: Eq v => ReftV v -> Bool Source #

isSingletonExpr :: Symbol -> Expr -> Maybe Expr Source #

isSingletonReft :: Reft -> Maybe Expr Source #

Predicates ----------------------------------------------------------------

isFalse :: Falseable a => a -> Bool Source #

Destructing

flattenRefas :: [ExprV v] -> [ExprV v] Source #

conjuncts :: Eq v => ExprV v -> [ExprV v] Source #

concConjuncts :: Expr -> [Expr] Source #

dropECst :: Expr -> Expr Source #

eApps :: ExprV v -> [ExprV v] -> ExprV v Source #

eAppC :: Sort -> Expr -> Expr -> Expr Source #

eCst :: Expr -> Sort -> Expr Source #

Eliminates redundant casts

exprKVars :: Expr -> HashMap KVar [Subst] Source #

exprSymbolsSet :: Expr -> HashSet Symbol Source #

splitEApp :: ExprV v -> (ExprV v, [ExprV v]) Source #

splitEAppThroughECst :: Expr -> (Expr, [Expr]) Source #

splitPAnd :: Expr -> [Expr] Source #

reftConjuncts :: Reft -> [Reft] Source #

sortedReftSymbols :: SortedReft -> HashSet Symbol Source #

substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr Source #

sortSubstInExpr :: SortSubst -> Expr -> Expr Source #

Transforming

mapPredReft :: (Expr -> Expr) -> Reft -> Reft Source #

onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr Source #

pprintReft :: (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc Source #

debruijnIndex :: Expr -> Int Source #

Orphan instances

Fixpoint Doc Source # 
Instance details

Methods

toFix :: Doc -> Doc Source #

simplify :: Doc -> Doc Source #

(Hashable a, Eq a, Binary a) => Binary (HashSet a) Source # 
Instance details

Methods

put :: HashSet a -> Put #

get :: Get (HashSet a) #

putList :: [HashSet a] -> Put #

(Hashable k, Eq k, Binary k, Binary v) => Binary (HashMap k v) Source # 
Instance details

Methods

put :: HashMap k v -> Put #

get :: Get (HashMap k v) #

putList :: [HashMap k v] -> Put #